active questions tagged z3 - Stack Overflow News Feed 
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.



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.



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




I am getting timeout on the following example.
http://rise4fun.com/Z3/zbOcW



Is there any trick to make this work (eg.by reformulating the problem or using triggers)?



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




I am getting timeout on the following example.
http://rise4fun.com/Z3/zbOcW



Is there any trick to make this work (eg.by reformulating the problem or using triggers)?



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




I want to get the solution from Z3 C API for the constraint followed:



   2^x < a < 2^(x+1)


expression for 2^x is :



    t_x=Z3_mk_power(ctx,two,x), two is the expression of "2";

    2^(x+1) is similar,


"a" is a int const ,which value is 10:



   a=Z3_mk_int(ctx,10);


the constraints are:



   c1=Z3_mk_lt(ctx,t_x,a);

   c2=Z3_mk_lt(ctx,a,t_x_plus_one);


then I get the model is "unknown", Z3 C API cannot get a model like this?



Tuesday, April 15, 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.



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




I want to get the solution from Z3 C API for the constraint followed:



   2^x < a < 2^(x+1)


expression for 2^x is :



    t_x=Z3_mk_power(ctx,two,x), two is the expression of "2";

    2^(x+1) is similar,


"a" is a int const ,which value is 10:



   a=Z3_mk_int(ctx,10);


the constraints are:



   c1=Z3_mk_lt(ctx,t_x,a);

   c2=Z3_mk_lt(ctx,a,t_x_plus_one);


then I get the model is "unknown", Z3 C API cannot get a model like this?



Tuesday, April 15, 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 14, 2014  |  From active questions tagged z3 - Stack Overflow




I want to develop with Z3 c api, and I install z3 as the steps in Readme file under the src of Z3, as followed:



python scripts/mk_make.py
cd build
nmake


then I get many files under the "build" but not the libz3.lib. I want to use the example under the src, and the compiled binaries from the Z3' homepage cannot be used.



then ,my question is how to get the libz3.lib from the source or where I can find tutorials of using Z3 as C API.



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




I am trying to multiply 2 matrices of 2*2 order. One of the matrix contains an unknown parameter "k1". I want to check a satisfiable solution that for which value of k1. The product of two matrices will be equal to the third one.
Note: I dont want to convert the multiplication into a linear relation or set of equation I want to manipulate it as matrices.



Here is where I am stuck.



k1 = Int ('k1')

x = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(2) ] 
     for i in range(2) ]

a =((1,k1),(3,4))

b =((1,1),(1,1))

c= ((3,3),(7,7))

s = Solver()
s.add(a[0][1]>0)
s.add(a*b==c)
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(x[i][j]) for j in range(2) ] 
      for i in range(2) ]
print_matrix(r)
else:
print "failed to solve"


Any way Out?



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




I am trying to multiply 2 matrices of 2*2 order. One of the matrix contains an unknown parameter "k1". I want to check a satisfiable solution that for which value of k1. The product of two matrices will be equal to the third one.
Note: I dont want to convert the multiplication into a linear relation or set of equation I want to manipulate it as matrices.



Here is where I am stuck.



k1 = Int ('k1')

x = [ [ Int("x_%s_%s" % (i+1, j+1)) for j in range(2) ] 
     for i in range(2) ]

a =((1,k1),(3,4))

b =((1,1),(1,1))

c= ((3,3),(7,7))

s = Solver()
s.add(a[0][1]>0)
s.add(a*b==c)
if s.check() == sat:
m = s.model()
r = [ [ m.evaluate(x[i][j]) for j in range(2) ] 
      for i in range(2) ]
print_matrix(r)
else:
print "failed to solve"


Any way Out?



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




In the previous question solve nonlinear constraints, I asked whether z3 could give a sound and complete result when using nlsat solver to handle polynomial constraints on nonlinear real arithmetic. As Taylor answered, the nksat solver is complete and sound.



Z3 supports unsat core extraction when solving constraints on LRA. I want to know that whether
it possible to extract an unsat core when using the nlsat solver? If z3 does not support,
can I implement it on top of z3? A further question is how large problem it can handle.



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




Let's say I have a user-defined commutative and associative operator op. The code below is invalid because I'm using op with more than two arguments. Let's suppose for a moment that it is valid and that it means "the way op is applied is irrelevant".



(declare-sort T 0)
(declare-fun op (T T) T)
(declare-fun P (T) Bool)
(declare-const a T)
(declare-const b T)
(declare-const c T)
(declare-const d T)
(declare-const k T)
; associativity
(assert (forall ((x T) (y T)) (z T)) 
                (= (op x (op y z)) 
                   (op (op x y) z))))
; commutativity
(assert (forall ((x T) (y T))) 
                (= (op x y) 
                   (op y x))))
; assumption 1
(assert (forall ((x T) (y T)) (= (op x y) k)))
; assumption 2
(assert (P (op a c k)))
; conjecture
(assert (not (P (op a b c d))))


What would be the best way to ensure that assumption 1 be instantiated with x, y := b, d and that assumption 2 become applicable to prove the conjecture?



One solution that I am considering is to generate all possible binary trees that would correspond to (op a b c d). That is pretty expensive however: there are 5 different binary trees with 4 leaves and 24 different permutations of the leaves for a total 120 different binary trees. I can also hold back and hope that z3 uses associativity and commutativity on its own and trigger the right instantiation of assumption 1.



The problem becomes even more hairy if we consider that chains like (op a b c) can appear inside a universal quantification. We could probably use patterns (op a (op b c)), (op b (op a c)), etc to maximize the chances of the quantification being instantiated but the pattern has to emerge somewhere and z3 probably doesn't have the guidance to make it appear on its own.



Is there anything better I could do?



Thanks!
Simon



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




I am trying to prove with Z3 the theorem in general topology given at



TPTP-Topology



I am translating the code given there using the following Z3-SMT-LIB code



;; File     : TOP001-2 : TPTP v6.0.0. Released v1.0.0.
;; Domain   : Topology
;; Problem  : Topology generated by a basis forms a topological space, part 1

(declare-sort S)
(declare-sort Q)
(declare-sort P)

(declare-fun elemcoll (S Q) Bool)
(declare-fun elemset (P S) Bool)
(declare-fun unionmemb (Q) S)

(declare-fun f1 (Q P) S)

(declare-fun f11 (Q S) P)
(declare-fun basis (S Q) Bool)
(declare-fun Subset (S S) Bool)
(declare-fun topbasis (Q) Q)

;; union of members axiom 1.
(assert (forall ((U P) (Vf Q)) (or (not (elemset U (unionmemb Vf))) 
                                    (elemset U (f1 Vf U) ) )   ))
;; union of members axiom 2.

(assert (forall ((U P) (Vf Q)) (or (not (elemset U (unionmemb Vf))) 
                                   (elemcoll (f1 Vf U) Vf ) )   ))


;; basis for topology, axiom 28

(assert (forall ((X S) (Vf Q)) (or (not (basis X Vf)) (= (unionmemb Vf) X )  )   ))

;; Topology generated by a basis, axiom 40.

(assert (forall ((Vf Q) (U S)) (or (elemcoll U (topbasis Vf))   
                               (elemset (f11 Vf U) U))   ))

;; Set theory, axiom 7.

(assert (forall ((X S) (Y Q)) (or (not (elemcoll X Y)) (Subset X (unionmemb Y) ) )  ))

;; Set theory, axiom 8.
(assert (forall ((X S) (Y S) (U P)) (or (not (Subset X Y)) (not (elemset U X))
                                                                (elemset U Y)     )))

;; Set theory, axiom 9.
(assert (forall ((X S)) (Subset X X )  ))

;; Set theory, axiom 10.
(assert (forall ((X S) (Y S) (Z S)) (or (not (= X Y)) (not (Subset Z X)) (Subset Z Y) )  ))

;; Set theory, axiom 11.
(assert (forall ((X S) (Y S) (Z S)) (or (not (= X Y)) (not (Subset X Z)) (Subset Y Z) )  ))

(check-sat)

(push)
(declare-fun cx () S)
(declare-fun f () Q)
(assert (basis cx f))
(assert (not (elemcoll cx (topbasis f))))   
(check-sat)
(pop)

(push)
(assert (basis cx f))
(assert (elemcoll cx (topbasis f)))  
(check-sat)
(pop)


The corresponding output is



sat
sat
sat


Please run this example online here



The first sat is correct; but the second sat is wrong, it must be unsat. In other words, Z3 is saying that the theorem and its negation are true simultaneously.



Please let me know what happens in this case. Many thanks. All the best.



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




I am trying to express the sum of the range of an unbounded Array in z3. For instance in Python:



IntArray = ArraySort(IntSort(), IntSort())

sum = Function('sum', IntArray, IntSort())

........


Is there any way to complete the definition of 'sum'? Otherwise, is there a more plausible alternative?



Thanks!



 active questions tagged z3 - Stack Overflow News Feed 

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

Comments

No comments yet.