active questions tagged z3 - Stack Overflow News Feed 
Sunday, October 19, 2014  |  From active questions tagged z3 - Stack Overflow




I am writing a code in c#.



In the code there are various IF conditions. I want to pass these conditions to z3 constraint solver and check its satisfiability and get the values that makes it satifiable. (I make use of these values further in my code)



If I take a IF condition in the code and write its equivalent assert in z3 syntax then it works fine. But I want to generalize means given a statement in c# I want to generate its corresponding statement in z3 syntax.



Is there anyway I can do that?



Thursday, October 16, 2014  |  From active questions tagged z3 - Stack Overflow




I am starting to collaborate in a Boogie project of a colleague, which is based on an older version of Boogie that uses Z3 3.2. My infrastructure is Linux-based and, hence, it seems that I need to compile Z3 and the C# bindings myself as the Z3 website offers older binaries only for Windows.



Unfortunately, I cannot find pre-4.1 sources on the web. Are they no longer available? Can someone point me to them?



Thursday, October 16, 2014  |  From active questions tagged z3 - Stack Overflow




The below Python snippet illustrates a strage performance behavior of Z3. Without push() call, the z3 checks the formula in 0.1s. With push() (and no extra assertions), z3 takes 0.8s. A similar outcome occurs even after swapping s.append(f) and s.push().



import time
import z3
f = z3.parse_smt2_file("smt-lib/QF_BV/RWS/Example_1.txt.smt2")
s = z3.Solver()
s.append(f)
t1 = time.time()
s.check()  # 0.10693597793579102 seconds
print(time.time() - t1)

s = z3.Solver()
t1 = time.time()
s.append(f)
s.push()
s.check()  # 0.830916166305542 seconds
print(time.time() - t1)


Any idea why does this slowdown occur? And, how can it be addressed?



I'm using z3-4.3.2.bb56885147e4-x64-osx-10.9.2.



Thursday, October 16, 2014  |  From active questions tagged z3 - Stack Overflow




The below Python snippet illustrates a strage performance behavior of Z3. Without push() call, the z3 checks the formula in 0.1s. With push() (and no extra assertions), z3 takes 0.8s. A similar outcome occurs even after swapping s.append(f) and s.push().



import time
import z3
f = z3.parse_smt2_file("smt-lib/QF_BV/RWS/Example_1.txt.smt2")
s = z3.Solver()
s.append(f)
t1 = time.time()
s.check()  # 0.10693597793579102 seconds
print(time.time() - t1)

s = z3.Solver()
t1 = time.time()
s.append(f)
s.push()
s.check()  # 0.830916166305542 seconds
print(time.time() - t1)


Any idea why does this slowdown occur? And, how can it be addressed?



I'm using z3-4.3.2.bb56885147e4-x64-osx-10.9.2.



Thursday, October 16, 2014  |  From active questions tagged z3 - Stack Overflow




The below Python snippet illustrates a strage performance behavior of Z3. Without push() call, the z3 checks the formula in 0.1s. With push() (and no extra assertions), z3 takes 0.8s. A similar outcome occurs even after swapping s.append(f) and s.push().



import time
import z3
f = z3.parse_smt2_file("smt-lib/QF_BV/RWS/Example_1.txt.smt2")
s = z3.Solver()
s.append(f)
t1 = time.time()
s.check()  # 0.10693597793579102 seconds
print(time.time() - t1)

s = z3.Solver()
t1 = time.time()
s.append(f)
s.push()
s.check()  # 0.830916166305542 seconds
print(time.time() - t1)


Any idea why does this slowdown occur? And, how can it be addressed?



Thursday, October 16, 2014  |  From active questions tagged z3 - Stack Overflow




I am starting to collaborate in a Boogie project of a colleague, which is based on an older version of Boogie that uses Z3 3.2. My infrastructure is Linux-based and, hence, it seems that I need to compile Z3 and the C# bindings myself as the Z3 website offers older binaries only for Windows.



Unfortunately, I cannot find pre-4.1 sources on the web. Are they no longer available? Can someone point me to them?



Wednesday, October 15, 2014  |  From active questions tagged z3 - Stack Overflow




I am using Z3 Python bindings to create an And expression via z3.And(exprs) where exprs is a python list of 48000 equality constraints over boolean variables. This operation takes 2 seconds on a MBP with 2.6GHz processor.



What could I be doing wrong? Is this an issue with z3 Python bindings? Any ideas on how to optimize such constructions?



Incidentally, in my experiments, the constructions of such expressions is taking more time than solving the resulting formulae :)



Tuesday, October 14, 2014  |  From active questions tagged z3 - Stack Overflow




I am using Z3 Python bindings to create an And expression via z3.And(exprs) where exprs is a python list of 48000 equality constraints over boolean variables. This operation takes 2 seconds on a MBP with 2.6GHz processor.



What could I be doing wrong? Is this an issue with z3 Python bindings? Any ideas on how to optimize such constructions?



Incidentally, in my experiments, the constructions of such expressions is taking more time than solving the resulting formulae :)



Monday, October 13, 2014  |  From active questions tagged z3 - Stack Overflow




Given a Z3 Sort and a string s I am trying to create a Z3 constant of that sort named s.



For instance, given IntSort() and the name "x" I'd like to get an integer constant named "x".



I know I can get it calling Int('x') but since I am creating this variables dynamically I cannot predict what sort a given variable will have. What I have to do is to create a variable of the same sort of the one provided by the system but with a new name (which I have to be able to specify at runtime).



To be more specific,



1. I get a model for a user defined formula calling the Z3 Solver on it, 
2. I save it in a database (recording for each assignment in such a model the variable name, the value to be assigned to it and the sort of that variable)
3. I retrieve that assignment after a while from the database and I try it o a new formula having the same variables of the original one. 


In order to do so I turn each assignment into a clause of the form var == value, I add them to the solver together with the target formula and I check for satisfiability.



Up to now I only worked with the integer sort so I hardcoded the transformation of string to constants using the Int function. Now I am trying to generalize the approach to different logics and different datatypes so I need something to create the right constant out of what I saved in my database.



Is this approach reasonable in your opinion? Do you think there any trick to do it better?



Monday, October 13, 2014  |  From active questions tagged z3 - Stack Overflow




Given a Z3 Sort and a string s I am trying to create a Z3 constant of that sort named s.



For instance, given IntSort() and the name "x" I'd like to get an integer constant named "x".



I know I can get it calling Int('x') but since I am creating this variables dynamically I cannot predict what sort a given variable will have. What I have to do is to create a variable of the same sort of the one provided by the system but with a new name (which I have to be able to specify at runtime).



To be more specific,



1. I get a model for a user defined formula calling the Z3 Solver on it, 
2. I save it in a database (recording for each assignment in such a model the variable name, the value to be assigned to it and the sort of that variable)
3. I retrieve that assignment after a while from the database and I try it o a new formula having the same variables of the original one. 


In order to do so I turn each assignment into a clause of the form var == value, I add them to the solver together with the target formula and I check for satisfiability.



Up to now I only worked with the integer sort so I hardcoded the transformation of string to constants using the Int function. Now I am trying to generalize the approach to different logics and different datatypes so I need something to create the right constant out of what I saved in my database.



Is this approach reasonable in your opinion? Do you think there any trick to do it better?



Sunday, October 12, 2014  |  From active questions tagged z3 - Stack Overflow




Using Z3 it is possible to prove that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t)))   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (t Real) (s Real)) (distinct (h s (h t (carte x y))) 
                                                                 (h (+ t s) (carte x y)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y)) 
                                               (carte x y))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run the code online here.



Other example: proving that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ( (x Real) (y Real) (z Real) (t Real)) (= (h t (carte x y z)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t))  (+ z (* c t))   )   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real) (s Real)) (distinct (h s (h t (carte x y z))) 
                                                                 (h (+ t s) (carte x y z)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z)) 
                                               (carte x y z))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run this code online here



Other example: To prove that



enter image description here



forms a one-parameter group.



The proof is given online here and the four-dimensional extension is given online here



A last couple of examples: Prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



Prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



More in general, prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



One three-dimensional extension: prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



One example with hyperbolic functions: Prove that



enter image description here



forms a one-parameter group.



The proof is given online here



My questions are:



  1. It is possible to make the proofs for higher dimensions using arrays?

  2. I claim that Z3 is the only system that is able to perform these proofs. Do you agree?


Sunday, October 12, 2014  |  From active questions tagged z3 - Stack Overflow




Using Z3 it is possible to prove that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t)))   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (t Real) (s Real)) (distinct (h s (h t (carte x y))) 
                                                                 (h (+ t s) (carte x y)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y)) 
                                               (carte x y))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run the code online here.



Other example: proving that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ( (x Real) (y Real) (z Real) (t Real)) (= (h t (carte x y z)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t))  (+ z (* c t))   )   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real) (s Real)) (distinct (h s (h t (carte x y z))) 
                                                                 (h (+ t s) (carte x y z)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z)) 
                                               (carte x y z))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run this code online here



Other example: To prove that



enter image description here



forms a one-parameter group.



The proof is given online here and the four-dimensional extension is given online here



A last couple of examples: Prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



Prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



More in general, prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



One three-dimensional extension: prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



My questions are:



  1. It is possible to make the proofs for higher dimensions using arrays?

  2. I claim that Z3 is the only system that is able to perform these proofs. Do you agree?


Saturday, October 11, 2014  |  From active questions tagged z3 - Stack Overflow




Using Z3 it is possible to prove that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t)))   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (t Real) (s Real)) (distinct (h s (h t (carte x y))) 
                                                                 (h (+ t s) (carte x y)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y)) 
                                               (carte x y))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run the code online here.



Other example: proving that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ( (x Real) (y Real) (z Real) (t Real)) (= (h t (carte x y z)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t))  (+ z (* c t))   )   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real) (s Real)) (distinct (h s (h t (carte x y z))) 
                                                                 (h (+ t s) (carte x y z)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z)) 
                                               (carte x y z))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run this code online here



Other example: To prove that



enter image description here



forms a one-parameter group.



The proof is given online here and the four-dimensional extension is given online here



A last couple of examples: Prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



Prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



More in general, prove that



enter image description here



forms a one-parameter group.



The proof is given online here



My questions are:



  1. It is possible to make the proofs for higher dimensions using arrays?

  2. I claim that Z3 is the only system that is able to perform these proofs. Do you agree?


Saturday, October 11, 2014  |  From active questions tagged z3 - Stack Overflow




Using Z3 it is possible to prove that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t)))   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (t Real) (s Real)) (distinct (h s (h t (carte x y))) 
                                                                 (h (+ t s) (carte x y)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y)) 
                                               (carte x y))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run the code online here.



Other example: proving that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ( (x Real) (y Real) (z Real) (t Real)) (= (h t (carte x y z)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t))  (+ z (* c t))   )   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real) (s Real)) (distinct (h s (h t (carte x y z))) 
                                                                 (h (+ t s) (carte x y z)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z)) 
                                               (carte x y z))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run this code online here



Other example: To prove that



enter image description here



forms a one-parameter group.



The proof is given online here and the four-dimensional extension is given online here



A last couple of examples: Prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



Prove that



enter image description here



forms a one-parameter group.



The proof is given online here



My questions are:



  1. It is possible to make the proofs for higher dimensions using arrays?

  2. I claim that Z3 is the only system that is able to perform these proofs. Do you agree?


Saturday, October 11, 2014  |  From active questions tagged z3 - Stack Overflow




Using Z3 it is possible to prove that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t)))   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (t Real) (s Real)) (distinct (h s (h t (carte x y))) 
                                                                 (h (+ t s) (carte x y)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y)) 
                                               (carte x y))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run the code online here.



Other example: proving that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ( (x Real) (y Real) (z Real) (t Real)) (= (h t (carte x y z)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t))  (+ z (* c t))   )   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real) (s Real)) (distinct (h s (h t (carte x y z))) 
                                                                 (h (+ t s) (carte x y z)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z)) 
                                               (carte x y z))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run this code online here



Other example: To prove that



enter image description here



forms a one-parameter group.



The proof is given online here and the four-dimensional extension is given online here



Last example: Prove that



enter image description here



forms a one-parameter group.



The proof is given online here.



My questions are:



  1. It is possible to make the proofs for higher dimensions using arrays?

  2. I claim that Z3 is the only system that is able to perform these proofs. Do you agree?


Saturday, October 11, 2014  |  From active questions tagged z3 - Stack Overflow




Using Z3 it is possible to prove that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t)))   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (t Real) (s Real)) (distinct (h s (h t (carte x y))) 
                                                                 (h (+ t s) (carte x y)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y)) 
                                               (carte x y))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run the code online here.



Other example: proving that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ( (x Real) (y Real) (z Real) (t Real)) (= (h t (carte x y z)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t))  (+ z (* c t))   )   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real) (s Real)) (distinct (h s (h t (carte x y z))) 
                                                                 (h (+ t s) (carte x y z)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z)) 
                                               (carte x y z))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run this code online here



Other example: To prove that



enter image description here



forms a one-parameter group.



The proof is given online here and the four-dimensional extension is given online here



My questions are:



  1. It is possible to make the proofs for higher dimensions using arrays?

  2. I claim that Z3 is the only system that is able to perform these proofs. Do you agree?


Saturday, October 11, 2014  |  From active questions tagged z3 - Stack Overflow




Using Z3 it is possible to prove that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t)))   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (t Real) (s Real)) (distinct (h s (h t (carte x y))) 
                                                                 (h (+ t s) (carte x y)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y)) 
                                               (carte x y))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run the code online here.



Other example: proving that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ( (x Real) (y Real) (z Real) (t Real)) (= (h t (carte x y z)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t))  (+ z (* c t))   )   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real) (s Real)) (distinct (h s (h t (carte x y z))) 
                                                                 (h (+ t s) (carte x y z)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z)) 
                                               (carte x y z))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run this code online here



My questions are:



  1. It is possible to make the proof for higher dimension using arrays?

  2. I claim that Z3 is the only system that is able to perform the proof. Do you agree?


Friday, October 10, 2014  |  From active questions tagged z3 - Stack Overflow




Using Z3 it is possible to prove that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t)))   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (t Real) (s Real)) (distinct (h s (h t (carte x y))) 
                                                                 (h (+ t s) (carte x y)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y)) 
                                               (carte x y))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run the code online here.



Other example: proving that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ( (x Real) (y Real) (z Real) (t Real)) (= (h t (carte x y z)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t))  (+ z (* c t))   )   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real) (s Real)) (distinct (h s (h t (carte x y z))) 
                                                                 (h (+ t s) (carte x y z)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z)) 
                                               (carte x y z))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (z Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y z))) 
                                                       (carte x y z))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run this code online here



My questions are:



  1. It is possible to make the proof for higher dimension using arrays?

  2. I claim that Z3 is the only system that is able to perform the proof. Do you agree?


Friday, October 10, 2014  |  From active questions tagged z3 - Stack Overflow




I am writing a static analysis tools that needs to perform some queries to an oracle solving linear integer arithmetic problems. For my first version, I implemented a decision procedure for Presburger arithmetic in OCaml (for fun, and profit). On big programs my decision procedure becomes the bottleneck so I decided to move to Z3.



My first results are disappointing, so I think I am doing something wrong with the Z3 API. I observe that, on simple programs, the analysis is more than 100 times slower with Z3 than with my naive home-brewed implementation. After some trivial benchmarking I think the culprit is:



let unsat ps =
  let open Z3.Solver in
  let solver = mk_solver ctx None in
  add solver [ps];
  check solver [] <> SATISFIABLE


I use this function hundreds of times (thousands on big programs). The problem, encoded in ps is of the form (not (implies (and X X X X X) Y)) where the conjunction has very often less than 10 conjuncts, X and Y are simple linear inequalities. These problems are easy to solve so I reckon my performance issue has more to do with scaffolding code.



My question is, how to reduce the cost of each call to this unsat function?



Thursday, October 9, 2014  |  From active questions tagged z3 - Stack Overflow




Using Z3 it is possible to prove that



enter image description here



forms a one-parameter group.



The proof is performed using the following Z3 code:



(declare-sort S)
(declare-fun carte (Real Real) S)
(declare-fun h (Real S) S)

(declare-fun a () Real)
(declare-fun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y)) 
                                                 (carte (+ x (* a t)) 
                                                      (+ y (* b t)))   )   ) )

(check-sat)

(push)
(assert (forall ((x Real) (y Real) (t Real) (s Real)) (distinct (h s (h t (carte x y))) 
                                                                 (h (+ t s) (carte x y)))  ))
(check-sat)
(pop)

(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y)) 
                                               (carte x y))    ))
(check-sat)
(pop)



(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h (- 0 t) (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h (- 0 t) (h t (carte x y))) 
                                                       (carte x y))    ))
(check-sat)
(pop)


and the corresponding output is



sat
unsat
unsat
unsat
unsat


Please run the code online here



My questions are:



  1. It is possible to make the proof using arrays.

  2. I claim that Z3 is the only system that is able to perform the proof. Do you agree?


 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.