Using C++ APIs, how can you extract the decimal value of a bit-vector constant from a model.

CodePlexProject Hosting for Open Source Software

Wednesday, April 23, 2014 | From active questions tagged z3 - Stack Overflow

Using C++ APIs, how can you extract the decimal value of a bit-vector constant from a model.

Tuesday, April 22, 2014 | From active questions tagged z3 - Stack Overflow

Using C++ APIs, how can you extract the decimal value of a bit-vector constant from a model.

Tuesday, April 22, 2014 | From active questions tagged z3 - Stack Overflow

In the expr_vector example from example.cpp, can we quantify over the expr_vector index. For example, if we have the following code fragment :

```
expr_vector steps(c);
expr b = c.bool_val(true);
for(unsigned i = 0; i<N ; i++ )
{ expr step = c.int_const(...)
if( i == 0 ) b = b && step == 0 ;
else b = b && step == steps[i-1] + 1 ;
steps.push_back(step);
}
```

can we express something like

```
expr choice = c.int_const("choice);
b = b && 0 <= choice && choice < N;
b = b && steps[choice] > 5 ;
```

Tuesday, April 22, 2014 | From active questions tagged z3 - Stack Overflow

I want to use Z3 for reasoning over bit vectors. In addition with the satisfiability decision I also want the symbolic representations of the bit vectors so that I can apply my own computations on them as needed. For example:

Let,

- X[3:0], Y[3:0], Z[4:0] are declared as bit vectors without initializing any value
- print X[3:0]
- X[3:0] <- X[3:0] >> 1 (logical shift)
- print X[3:0]
- Z[4:0] <- X[3:0] + Y[3:0]
- print Z[4:0]
- .......

Desired output (something symbolic like this):

```
> 2. [x3 x2 x1 x0]
> 4. [0 x3 x2 x1]
> 6. [s4 s3 s2 s1 s0]
```

Is it possible to have this using Z3?

Tuesday, April 22, 2014 | From active questions tagged z3 - Stack Overflow

I have installed the Z3 API for Java and I am trying to use it but I can't find any tutorial or documentation that explains how to use this API.

The only resource I have found so far is the source code and the example program, so I wanted to know if anyone was aware of any other documentation/tutorial for the Z3 Java API.

Monday, April 21, 2014 | From active questions tagged z3 - Stack Overflow

I try to make a simple substitution of a variable x (set variable if important) with another variable y. From the post here (Substitution in Z3 java), I presume that substitute works fine in Java. However I get the same expression object (when printed) as return. Is substitution correctly implemented or I am making a mistake? The below is the code snippet on how I define my variable and call substitute method in case it is relevant.

```
EnumSort xSort = ctx.mkEnumSort(xs, ctx.mkSymbol("A"),ctx.mkSymbol("B"));
SetSort xSet = ctx.mkSetSort(xSort);
Expr x = ctx.mkConst("x",xSet);
/*Construct the formula "formOld".....*/
Expr y = ctx.mkConst("y",x.getSort());
BoolExpr form_sub = (BoolExpr)formOld.substitute(x, y);
```

The formula formSub seems unchanged when I print. Couldn't find any hint from debugging.

Thanks.

Monday, April 21, 2014 | From active questions tagged z3 - Stack Overflow

I want to use Z3 for reasoning over bit vectors. In addition with the satisfiability decision I also want the symbolic representations of the bit vectors so that I can apply my own computations on them as needed. For example:

Let,

1. X[3:0], Y[3:0], Z[4:0] are declared as bit vectors without initializing any value

2. print X[3:0]

3. X[3:0] <- X[3:0] >> 1 (logical shift)

4. print X[3:0]

5. Z[4:0] <- X[3:0] + Y[3:0]

6. print Z[4:0]

7. .......

Desired output (something symbolic like this):

- [x3 x2 x1 x0]
- [0 x3 x2 x1]
- [s4 s3 s2 s1 s0]

Is it possible to have this using Z3?

Monday, April 21, 2014 | From active questions tagged z3 - Stack Overflow

Please consider the follow statements.

y := 10

z := x + y

After these two statements are executed "z" has the value "x + 10" where "x" represents a symbolic value; such symbolic values are important in program verification -- for example, to compute the path characteristics using Dijkstra'a weakest pre-condition method.

Now, consider the following code for Z3.

```
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= y 10))
(assert (= z (+ x y)))
(check-sat)
(get-value (z))
```

It produces the following output since it consider the interpretation where "y" has the 10 and "x" has the value 0.

```
sat
((z 10))
```

Is there some way I can make Z3 produce the output "x + 10"? i.e., I am interested in getting the symbolic values in terms of variables that have not been instantiated with any specific values.

Monday, April 21, 2014 | From active questions tagged z3 - Stack Overflow

I have installed the Z3 API for Java and I am trying to use it but I can't find any tutorial or documentation that explains how to use this API.

The only resource I have found so far is the source code and the example program, so I wanted to know if anyone was aware of any other documentation/tutorial for the Z3 Java API.

Sunday, April 20, 2014 | From active questions tagged z3 - Stack Overflow

Please consider the follow statements.

y := 10

z := x + y

After these two statements are executed "z" has the value "x + 10" where "x" represents a symbolic value; such symbolic values are important in program verification -- for example, to compute the path characteristics using Dijkstra'a weakest pre-condition method.

Now, consider the following code for Z3.

```
(declare-const x Int)
(declare-const y Int)
(declare-const z Int)
(assert (= y 10))
(assert (= z (+ x y)))
(check-sat)
(get-value (z))
```

It produces the following output since it consider the interpretation where "y" has the 10 and "x" has the value 0.

```
sat
((z 10))
```

Is there some way I can make Z3 produce the output "x + 10"? i.e., I am interested in getting the symbolic values in terms of variables that have not been instantiated with any specific values.

Sunday, April 20, 2014 | From active questions tagged z3 - Stack Overflow

I have installed the Z3 API for Java and I am trying to use it but I can't find any tutorial or documentation that explains how to use this API.

The only resource I have found so far is the source code and the example program, so I wanted to know if anyone was aware of any other documentation/tutorial for the Z3 Java API.

Sunday, April 20, 2014 | From active questions tagged z3 - Stack Overflow

In Complex numbers in Z3 Leonardo de Moura was able to introduce and to compute with complex numbers in Z3.

Using the code proposed by Leonardo I am introducing and computing with quaternion numbers in Z3 according with the code presented here . Using this "quaternion " code I am solving the following problem:

```
x = Quaternion("x")
s = Tactic('qfnra-nlsat').solver()
s.add(x*x + 30 == 0, x.i3 > 0, x.i2 >0, x.i1 > 0)
print(s.check())
m = s.model()
print m
```

and the corresponding output is:

```
sat
[x.r = 0, x.i1 = 1, x.i2 = 1, x.i3 = 5.2915026221?]
```

This result was verified using Maple.

Other example:

```
x = Quaternion("x")
y = Quaternion("y")
z = Quaternion("z")
s = Tactic('qfnra-nlsat').solver()
s.add(x*y + 30 + x + y*z == 0, x - y + z == 10)
print(s.check())
m = s.model()
print m
```

and the output is:

```
sat
[y.r = 1/8,
z.r = 2601/64,
y.i1 = 1/2,
z.i1 = 45/8,
y.i2 = -1/2,
z.i2 = -45/8,
y.i3 = -1/2,
z.i3 = -45/8,
x.i3 = 41/8,
x.i2 = 41/8,
x.i1 = -41/8,
x.r = -1953/64]
```

Other example:

Proving that

```
x * y != y * x
```

Code:

```
x = Quaternion("x")
y = Quaternion("y")
a1, b1, c1, d1 = Reals('a1 b1 c1 d1')
a2, b2, c2, d2 = Reals('a2 b2 c2 d2')
x.r = a1
x.i1 = b1
x.i2 = c1
x.i3 = d1
y.r = a2
y.i1 = b2
y.i2 = c2
y.i3 = d2
print simplify((x * y - y * x).r)
print simplify((x * y - y * x).i1)
print simplify((x * y - y * x).i2)
print simplify((x * y - y * x).i3)
```

Output:

```
0
2·c2·d1 + -2·c1·d2
-2·b2·d1 + 2·b1·d2
2·b2·c1 + -2·b1·c2
```

Other example : Proving that the quaternions

```
A = (1+ I)/sqrt(2),
B =(1 + J)/sqrt(2),
C = (1 + K)/sqrt(2)
```

generate a representation of the Braid Group, it is to say, we have that

```
ABA = BAB, ACA = CAC, BCB = CBC.
```

Code:

```
A = Quaternion('A')
B = Quaternion('B')
C = Quaternion('C')
A.r = 1/Sqrt(2)
A.i1 = 1/Sqrt(2)
A.i2 = 0
A.i3 = 0
B.r = 1/Sqrt(2)
B.i1 = 0
B.i2 = 1/Sqrt(2)
B.i3 = 0
C.r = 1/Sqrt(2)
C.i1 = 0
C.i2 = 0
C.i3 = 1/Sqrt(2)
print simplify((A*B*A-B*A*B).r)
print simplify((A*B*A-B*A*B).i1)
print simplify((A*B*A-B*A*B).i2)
print simplify((A*B*A-B*A*B).i3)
print "Proved : ABA = BAB:"
print simplify((A*C*A-C*A*C).r)
print simplify((A*C*A-C*A*C).i1)
print simplify((A*C*A-C*A*C).i2)
print simplify((A*C*A-C*A*C).i3)
print "Proved : ACA = CAC:"
print simplify((B*C*B-C*B*C).r)
print simplify((B*C*B-C*B*C).i1)
print simplify((B*C*B-C*B*C).i2)
print simplify((B*C*B-C*B*C).i3)
print "Proved : BCB = CBC:"
```

Output:

```
0
0
0
0
Proved : ABA = BAB.
0
0
0
0
Proved : ACA = CAC.
0
0
0
0
Proved : BCB = CBC.
```

Other example: Proving that

```
x / x = 1
```

for all invertible quaternion:

Code:

```
x = Quaternion("x")
a, a1, a2, a3 = Reals('a a1 a2 a3')
x.r = a
x.i1 = a1
x.i2 = a2
x.i3 = a3
s = Solver()
s.add(Or(a != 0, a1 != 0, a2 != 0, a3 != 0), Not((x/x).r == 1))
print s.check()
s1 = Solver()
s1.add(Or(a != 0, a1 != 0, a2 != 0, a3 != 0), Not((x/x).i1 == 0))
print s1.check()
s2 = Solver()
s2.add(Or(a != 0, a1 != 0, a2 != 0, a3 != 0), Not((x/x).i2 == 0))
print s2.check()
s3 = Solver()
s3.add(Or(a != 0, a1 != 0, a2 != 0, a3 != 0), Not((x/x).i3 == 0))
print s3.check()
```

Output:

```
unsat
unsat
unsat
unsat
```

Please let me know what do you think about the "quaternion" code and how the "quaternion" code can be improved. Many thanks.

Sunday, April 20, 2014 | From active questions tagged z3 - Stack Overflow

In the expr_vector example from example.cpp, can we quantify over the expr_vector index. For example, if we have the following code fragment :

```
expr_vector steps(c);
expr b = c.bool_val(true);
for(unsigned i = 0; i<N ; i++ )
{ expr step = c.int_const(...)
if( i == 0 ) b = b && step == 0 ;
else b = b && step == steps[i-1] + 1 ;
steps.push_back(step);
}
```

can we express something like

```
expr choice = c.int_const("choice);
b = b && 0 <= choice && choice < N;
b = b && steps[choice] > 5 ;
```

Saturday, April 19, 2014 | From active questions tagged z3 - Stack Overflow

I am trying to prove a theorem in group theory using the following Z3 SMT-LIB code

```
(declare-sort S)
(declare-fun identity () S)
(declare-fun product (S S S) Bool)
(declare-fun inverse (S) S)
(declare-fun multiply (S S) S)
(assert (forall ((X S)) (product identity X X) ))
(assert (forall ((X S)) (product X identity X) ))
(assert (forall ((X S)) (product (inverse X) X identity) ))
(assert (forall ((X S)) (product X (inverse X) identity) ))
(assert (forall ((X S) (Y S)) (product X Y (multiply X Y)) ))
;;(assert (forall ((X S) (Y S) (Z S) (W S)) (or (not (product X Y Z))
;; (not (product X Y W))
;; (= Z W))))
(assert (forall ((X S) (Y S) (Z S) (U S) (V S) (W S)) (or (not (product X Y U))
(not (product Y Z V))
(not (product U Z W) )
(product X V W))))
(assert (forall ((X S) (Y S) (Z S) (U S) (V S) (W S)) (or (not (product X Y U))
(not (product Y Z V))
(not (product X V W) )
(product U Z W))))
(check-sat)
(push)
;; File : GRP001-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Group Theory
;; Problem : X^2 = identity => commutativity
;; Version : [MOW76] axioms.
;; English : If the square of every element is the identity, the system
;; is commutative.
(declare-fun a () S)
(declare-fun b () S)
(declare-fun c () S)
(assert (forall ((X S)) (product X X identity) ))
(assert (product a b c))
(assert (not (product b a c)))
(check-sat)
(pop)
```

Please run this code online here.

The master branch Z3 is able to prove such theorem but the unstable branch is not able. Please let me know why. Many thanks.

Friday, April 18, 2014 | From active questions tagged z3 - Stack Overflow

I try to make a simple substitution of a variable x (set variable if important) with another variable y. From the post here (Substitution in Z3 java), I presume that substitute works fine in Java. However I get the same expression object (when printed) as return. Is substitution correctly implemented or I am making a mistake? The below is the code snippet on how I define my variable and call substitute method in case it is relevant.

```
EnumSort xSort = ctx.mkEnumSort(xs, ctx.mkSymbol("A"),ctx.mkSymbol("B"));
SetSort xSet = ctx.mkSetSort(xSort);
Expr x = ctx.mkConst("x",xSet);
/*Construct the formula "formOld".....*/
Expr y = ctx.mkConst("y",x.getSort());
BoolExpr form_sub = (BoolExpr)formOld.substitute(x, y);
```

The formula formSub seems unchanged when I print. Couldn't find any hint from debugging.

Thanks.

Friday, April 18, 2014 | From active questions tagged z3 - Stack Overflow

I would like to know if there is some SMT command to get the coefficient values associated to an expression as the following

```
(assert (>= (+ x (* (/ -1 2) y)) 0.0))
```

So getting the values 1 and -0.5.

Thank you for any hint.

Thursday, April 17, 2014 | From active questions tagged z3 - Stack Overflow

I would like to know if there is some SMT command to get the coefficient values associated to an expression as the following

```
(assert (>= (+ x (* (/ -1 2) y)) 0.0))
```

So getting the values 1 and -0.5.

Thank you for any hint.

Thursday, April 17, 2014 | From active questions tagged z3 - Stack Overflow

I am trying to prove some theorems in Set theory using the following code

```
(declare-sort S)
(declare-sort P)
(declare-fun member (P S) Bool)
(declare-fun subs (S S) Bool)
(declare-fun memb1not2 (S S) P)
(declare-fun unio (S S S) Bool)
(declare-fun intersection (S S S) Bool)
(declare-fun differ (S S S) Bool)
(declare-fun g (S S S) P)
(declare-fun h (S S S) P)
(declare-fun k (S S S) P)
(assert (forall ((Element P) (Subset S) (Superset S)) (or
(not (member Element Subset))
(not (subs Subset Superset))
(member Element Superset ) ) ))
(assert (forall ((Subset S) (Superset S)) (or
(subs Subset Superset)
(member (memb1not2 Subset Superset) Subset ) ) ))
(assert (forall ((Subset S) (Superset S)) (or
(not (member (memb1not2 Subset Superset) Superset) )
(subs Subset Superset ) ) ))
(assert (forall ((Subset S) (Superset S)) (or
(not (= Subset Superset) )
(subs Subset Superset ) ) ))
(assert (forall ((Subset S) (Superset S)) (or
(not (= Superset Subset) )
(subs Subset Superset ) ) ))
(assert (forall ((Set1 S) (Set2 S)) (or
(not (subs Set1 Set2) )
(not (subs Set1 Set1) )
(= Set2 Set1 ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Union S) (Element P)) (or
(not (unio Set1 Set2 Union) )
(not (member Element Union))
(member Element Set1)
(member Element Set2 ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Union S) (Element P)) (or
(not (unio Set1 Set2 Union) )
(not (member Element Set1))
(member Element Union ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Union S) (Element P)) (or
(not (unio Set1 Set2 Union) )
(not (member Element Set2))
(member Element Union ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Union S)) (or
(unio Set1 Set2 Union)
(member (g Set1 Set2 Union) Set1)
(member (g Set1 Set2 Union) Set2)
(member (g Set1 Set2 Union) Union ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Union S)) (or
(not (member (g Set1 Set2 Union) Set1))
(not (member (g Set1 Set2 Union) Union))
(unio Set1 Set2 Union)
) ))
(assert (forall ((Set1 S) (Set2 S) (Union S)) (or
(not (member (g Set1 Set2 Union) Set2))
(not (member (g Set1 Set2 Union) Union))
(unio Set1 Set2 Union)
) ))
(assert (forall ((Set1 S) (Set2 S) (Intersection S) (Element P)) (or
(not (intersection Set1 Set2 Intersection) )
(not (member Element Intersection))
(member Element Set1 ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Intersection S) (Element P)) (or
(not (intersection Set1 Set2 Intersection) )
(not (member Element Intersection))
(member Element Set2 ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Intersection S) (Element P)) (or
(not (intersection Set1 Set2 Intersection) )
(not (member Element Set2))
(not (member Element Set1))
(member Element Intersection ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Intersection S) ) (or
(member (h Set1 Set2 Intersection) Intersection)
(intersection Set1 Set2 Intersection)
(member (h Set1 Set2 Intersection) Set1 ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Intersection S) ) (or
(member (h Set1 Set2 Intersection) Intersection)
(intersection Set1 Set2 Intersection)
(member (h Set1 Set2 Intersection) Set2 ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Intersection S) ) (or
(not (member (h Set1 Set2 Intersection) Intersection))
(not (member (h Set1 Set2 Intersection) Set2))
(not (member (h Set1 Set2 Intersection) Set1))
(intersection Set1 Set2 Intersection ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Difference S) (Element P)) (or
(not (differ Set1 Set2 Difference) )
(not (member Element Difference))
(member Element Set1 ) ) ))
(assert (forall ((Set1 S) (Set2 S) (A S) (Element P)) (or
(not (member Element Set1) )
(not (member Element Set2))
(not (differ A Set1 Set2 )) ) ))
(assert (forall ((Set1 S) (Set2 S) (Difference S) (Element P)) (or
(not (member Element Set1) )
(not (differ Set1 Set2 Difference))
(member Element Difference)
(member Element Set2 ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Difference S)) (or
(differ Set1 Set2 Difference)
(member (k Set1 Set2 Difference) Set1)
(member (k Set1 Set2 Difference) Difference ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Difference S)) (or
(not (member (k Set1 Set2 Difference) Set2))
(member (k Set1 Set2 Difference) Difference)
(differ Set1 Set2 Difference ) ) ))
(assert (forall ((Set1 S) (Set2 S) (Difference S)) (or
(not (member (k Set1 Set2 Difference) Difference))
(not (member (k Set1 Set2 Difference) Set1))
(member (k Set1 Set2 Difference) Set2)
(differ Set1 Set2 Difference ) ) ))
(check-sat)
(push)
;; File : SET001-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : Set members are superset members
;; Version : [LS74] axioms.
;; English : A member of a set is also a member of that set's supersets.
(declare-fun b () S)
(declare-fun bb () S)
(assert (= b bb))
(assert (forall ((elementofb P)) (member elementofb b) ))
(assert (not (forall ((elementofb P)) (member elementofb bb) )))
(check-sat)
(pop)
(push)
;; File : SET002-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : Idempotency of union
(declare-fun a () S)
(declare-fun aUa () S)
(assert (unio a a aUa))
(assert (not (= a aUa)))
(check-sat)
(pop)
(push)
;; File : SET003-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : A set is a subset of the union of itself with itself
(assert (unio a a aUa))
(assert (not (subs a aUa)))
(check-sat)
(pop)
(push)
;; File : SET004-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : A set is a subset of the union of itself and another set
(declare-fun aUb () S)
(assert (unio a b aUb))
(assert (not (subs a aUb)))
(check-sat)
(pop)
(push)
;; File : SET005-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : Associativity of set intersection
(declare-fun c () S)
(declare-fun aIb () S)
(declare-fun bIc () S)
(declare-fun aIbIc () S)
(assert (intersection a b aIb))
(assert (intersection b c bIc))
(assert (intersection a bIc aIbIc))
(assert (not (intersection aIb c aIbIc)))
(check-sat)
(pop)
(push)
;; File : SET006-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : A = A ^ B if A (= B
;; Version : [LS74] axioms.
;; English : If the intersection of two sets is the first of the two sets,
;; then the first is a subset of the second.
(declare-fun d () S)
(assert (intersection d a d))
(assert (not (subs d a)))
(check-sat)
(pop)
(push)
;; File : SET007-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : Intersection distributes over union
(declare-fun bUc () S)
(declare-fun aIc () S)
(declare-fun aIbUc () S)
(assert (unio b c bUc))
(assert (intersection a b aIb))
(assert (intersection a c aIc))
(assert (intersection a bUc aIbUc))
(assert (not (unio aIb aIc aIbUc) ))
(check-sat)
(pop)
(push)
;; File : SET008-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : (X \ Y) ^ Y = the empty set
;; Version : [LS74] axioms.
;; English : The difference of two sets contains no members of the
;; subtracted set.
(declare-fun bDa () S)
(declare-fun aIbDa () S)
(assert (differ b a bDa))
(assert (intersection a bDa aIbDa))
;;(assert (not (forall ((A P)) (not (member A aIbDa)) )))
(assert (exists ((A P)) (member A aIbDa) ))
(check-sat)
(pop)
(push)
;; File : SET009-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : If X is a subset of Y, then Z \ Y is a subset of Z \ X
(declare-fun bDd () S)
(assert (subs d a))
(assert (differ b a bDa))
(assert (differ b d bDd))
(assert (not (subs bDa bDd)))
(check-sat)
(pop)
(push)
;; File : SET010-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : X \ Y ^ Z = (X \ Y) U (X \ Z)
(declare-fun cDa () S)
(declare-fun cDb () S)
(declare-fun cDaIb () S)
(assert (intersection a b aIb))
(assert (differ c a cDa))
(assert (differ c b cDb))
(assert (differ c aIb cDaIb))
(assert (not (unio cDa cDb cDaIb)))
(check-sat)
(pop)
(push)
;; File : SET011-1 : TPTP v6.0.0. Released v1.0.0.
;; Domain : Set Theory
;; Problem : X \ (X \ Y) = X ^ Y
;; Version : [LS74] axioms.
;; English : The difference of a first set and the set which is the
;; difference of the first set and a second set, is the
;; intersection of the two sets.
(declare-fun aDaDb () S)
(declare-fun aDb () S)
(assert (differ a b aDb))
(assert (differ a aDb aDaDb))
(assert (not (intersection a b aDaDb)))
(check-sat)
(pop)
(push)
;; File : SET013-1 : TPTP v6.0.0. Bugfixed v2.1.0.
;; Domain : Set Theory
;; Problem : The intersection of sets is commutative
(declare-fun bIa () S)
(assert (intersection a b aIb))
(assert (intersection b a bIa))
(assert (not (= aIb bIa)))
(check-sat)
(pop)
(push)
;; File : SET014-2 : TPTP v6.0.0. Bugfixed v2.1.0.
;; Domain : Set Theory
;; Problem : Union of subsets is a subset
;; Version : [MOW76] axioms : Especial.
;; English : If A and B are contained in C then the union of A and B is also.
(assert (subs a c))
(assert (subs b c))
(assert (unio a b aUb))
(assert (not (subs aUb c)))
(check-sat)
(pop)
(push)
;; File : SET015-1 : TPTP v6.0.0. Bugfixed v2.1.0.
;; Domain : Set Theory
;; Problem : The union of sets is commutative
(declare-fun bUa () S)
(assert (unio a b aUb))
(assert (unio b a bUa))
(assert (not (= aUb bUa)))
(check-sat)
(pop)
```

Please run this code online here

Please let me know what do you think about this implementation. Many thanks.

Thursday, April 17, 2014 | From active questions tagged z3 - Stack Overflow

How is it possible to extract the function interpretation of an array in Z3 using the C API? When I query Rise4Fun with, say, the following instance:

```
(declare-fun arr () (Array Int Int))
(assert (= 5 (select arr 3)))
(check-sat)
(get-model)
(exit)
```

, I get:

```
sat
(model
(define-fun arr () (Array Int Int) (_ as-array k!0))
(define-fun k!0 ((x!1 Int)) Int (ite (= x!1 3) 5 5))
)
```

Is it possible to extract the function interpretation of `k!0`

using the C API only? I've tried applying `Z3_model_get_func_interp`

on the array constant declaration, and also on the term that is returned for the array in the SAT model, but always get an `Error: invalid argument`

.

Wednesday, April 16, 2014 | From active questions tagged z3 - Stack Overflow

I am trying to prove the right-cancellation property in group theory using the following code

```
(set-option :macro-finder true)
(declare-sort S)
(declare-fun e () S)
(declare-fun mult (S S) S)
(declare-fun inv (S) S)
(assert (forall ((x S) (y S) (z S)) (= (mult (mult x y) z) (mult x (mult y z)))))
(assert (forall ((x S)) (= (mult e x) x)))
(assert (forall ((x S)) (= (mult (inv x) x) e)))
(assert (forall ((x S)) (= (mult x e) x)))
(assert (forall ((x S)) (= (mult x (inv x)) e)))
(check-sat)
(assert (not (forall ((x S) (y S) (z S)) (=> (= (mult y x) (mult z x)) (= y z)))))
(check-sat)
```

but I am obtaining

```
sat
(error: "out of memory")
```

Please let me know what happens. Many thanks.

Last edited Nov 23, 2012 at 4:52 AM by leodemoura, version 13