active questions tagged z3 - Stack Overflow News Feed 
Friday, October 24, 2014  |  From active questions tagged z3 - Stack Overflow




I tried the following code in http://rise4fun.com/z3/tutorial



(declare-const a Int)
(assert (> a 100))
(check-sat)
(get-model)


the result is always a=101. I need some randomness in the answer that it produce a random number in the range [101,MAXINT). for example gets a seed=1000 and offers the a=12344. for seed=2323 offers a=9088765 and ... .



what should i add to this simple code?



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




There are versions of the Z3 SMT solver that support Craig interpolation. Methods of the API where, for example, Z3_interpolate, Z3_write_interpolation_problem, or Z3_mk_interpolation_context.



Microsoft Research provides a website with the description of the Z3 C API! The methods that are listed above cannot be found in this documentation. Have this methods been removed? Can they be found in a specific branch of Z3?



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




There are versions of the Z3 SMT solver that support Craig interpolation. Methods of the API where, for example, Z3_interpolate, Z3_write_interpolation_problem, or Z3_mk_interpolation_context.



Microsoft Research provides a website with the description of the Z3 C API! The methods that are listed above cannot be found in this documentation. Have this methods been removed? Can they be found in a specific branch of Z3?



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




There are versions of the Z3 SMT solver that support Craig interpolation. Methods of the API where, for example, Z3_interpolate, Z3_write_interpolation_problem, or Z3_mk_interpolation_context.



Microsoft Research provides a website with the description of the Z3 C API! The methods that are listed above cannot be found in this documentation. Have this methods been removed? Can they be found in a specific branch of Z3?



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




I would like to ask how do I download a stable version of Z3 for using Java API?
In the master branch in codeplex, the source does not contain directory src/api/java.



This is present in some branches like cade24 or rc and others.
I do not have an idea which one to choose from. Could someone help?



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




I would like to ask how do I download a stable version of Z3 for using Java API?
In the master branch in codeplex, the source does not contain directory src/api/java.



This is present in some branches like cade24 or rc and others.
I do not have an idea which one to choose from. Could someone help?



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?


 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.