active questions tagged z3  Stack Overflow News Feed
I tried the following code in http://rise4fun.com/z3/tutorial
(declareconst a Int)
(assert (> a 100))
(checksat)
(getmodel)
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?
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?
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?
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?
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?
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?
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?
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 Linuxbased 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 pre4.1 sources on the web. Are they no longer available? Can someone point me to them?
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("smtlib/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 z34.3.2.bb56885147e4x64osx10.9.2.
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("smtlib/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 z34.3.2.bb56885147e4x64osx10.9.2.
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("smtlib/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 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 Linuxbased 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 pre4.1 sources on the web. Are they no longer available? Can someone point me to them?
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 :)
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 :)
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?
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?
Using Z3 it is possible to prove that
forms a oneparameter group.
The proof is performed using the following Z3 code:
(declaresort S)
(declarefun carte (Real Real) S)
(declarefun h (Real S) S)
(declarefun a () Real)
(declarefun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y))
(carte (+ x (* a t))
(+ y (* b t))) ) ) )
(checksat)
(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))) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y))
(carte x y)) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h ( 0 t) (carte x y)))
(carte x y)) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h ( 0 t) (h t (carte x y)))
(carte x y)) ))
(checksat)
(pop)
and the corresponding output is
sat
unsat
unsat
unsat
unsat
Please run the code online
here.
Other example: proving that
forms a oneparameter group.
The proof is performed using the following Z3 code:
(declaresort S)
(declarefun carte (Real Real Real) S)
(declarefun h (Real S) S)
(declarefun a () Real)
(declarefun b () Real)
(declarefun 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)) ) ) ) )
(checksat)
(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))) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z))
(carte x y z)) ))
(checksat)
(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)) ))
(checksat)
(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)) ))
(checksat)
(pop)
and the corresponding output is
sat
unsat
unsat
unsat
unsat
Please run this code online
here
Other example: To prove that
forms a oneparameter group.
The proof is given online
here and the fourdimensional extension is given online
here
A last couple of examples: Prove that
forms a oneparameter group.
The proof is given online
here.
Prove that
forms a oneparameter group.
The proof is given online
here.
More in general, prove that
forms a oneparameter group.
The proof is given online
here.
One threedimensional extension: prove that
forms a oneparameter group.
The proof is given online
here.
One example with hyperbolic functions: Prove that
forms a oneparameter group.
The proof is given online
here
My questions are:

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

I claim that Z3 is the only system that is able to perform these proofs. Do you agree?
Using Z3 it is possible to prove that
forms a oneparameter group.
The proof is performed using the following Z3 code:
(declaresort S)
(declarefun carte (Real Real) S)
(declarefun h (Real S) S)
(declarefun a () Real)
(declarefun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y))
(carte (+ x (* a t))
(+ y (* b t))) ) ) )
(checksat)
(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))) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y))
(carte x y)) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h ( 0 t) (carte x y)))
(carte x y)) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h ( 0 t) (h t (carte x y)))
(carte x y)) ))
(checksat)
(pop)
and the corresponding output is
sat
unsat
unsat
unsat
unsat
Please run the code online
here.
Other example: proving that
forms a oneparameter group.
The proof is performed using the following Z3 code:
(declaresort S)
(declarefun carte (Real Real Real) S)
(declarefun h (Real S) S)
(declarefun a () Real)
(declarefun b () Real)
(declarefun 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)) ) ) ) )
(checksat)
(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))) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z))
(carte x y z)) ))
(checksat)
(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)) ))
(checksat)
(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)) ))
(checksat)
(pop)
and the corresponding output is
sat
unsat
unsat
unsat
unsat
Please run this code online
here
Other example: To prove that
forms a oneparameter group.
The proof is given online
here and the fourdimensional extension is given online
here
A last couple of examples: Prove that
forms a oneparameter group.
The proof is given online
here.
Prove that
forms a oneparameter group.
The proof is given online
here.
More in general, prove that
forms a oneparameter group.
The proof is given online
here.
One threedimensional extension: prove that
forms a oneparameter group.
The proof is given online
here.
My questions are:

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

I claim that Z3 is the only system that is able to perform these proofs. Do you agree?
Using Z3 it is possible to prove that
forms a oneparameter group.
The proof is performed using the following Z3 code:
(declaresort S)
(declarefun carte (Real Real) S)
(declarefun h (Real S) S)
(declarefun a () Real)
(declarefun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y))
(carte (+ x (* a t))
(+ y (* b t))) ) ) )
(checksat)
(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))) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y))
(carte x y)) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h ( 0 t) (carte x y)))
(carte x y)) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h ( 0 t) (h t (carte x y)))
(carte x y)) ))
(checksat)
(pop)
and the corresponding output is
sat
unsat
unsat
unsat
unsat
Please run the code online
here.
Other example: proving that
forms a oneparameter group.
The proof is performed using the following Z3 code:
(declaresort S)
(declarefun carte (Real Real Real) S)
(declarefun h (Real S) S)
(declarefun a () Real)
(declarefun b () Real)
(declarefun 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)) ) ) ) )
(checksat)
(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))) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z))
(carte x y z)) ))
(checksat)
(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)) ))
(checksat)
(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)) ))
(checksat)
(pop)
and the corresponding output is
sat
unsat
unsat
unsat
unsat
Please run this code online
here
Other example: To prove that
forms a oneparameter group.
The proof is given online
here and the fourdimensional extension is given online
here
A last couple of examples: Prove that
forms a oneparameter group.
The proof is given online
here.
Prove that
forms a oneparameter group.
The proof is given online
here.
More in general, prove that
forms a oneparameter group.
The proof is given online
here
My questions are:

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

I claim that Z3 is the only system that is able to perform these proofs. Do you agree?
Using Z3 it is possible to prove that
forms a oneparameter group.
The proof is performed using the following Z3 code:
(declaresort S)
(declarefun carte (Real Real) S)
(declarefun h (Real S) S)
(declarefun a () Real)
(declarefun b () Real)
(assert (forall ( (x Real) (y Real) (t Real)) (= (h t (carte x y))
(carte (+ x (* a t))
(+ y (* b t))) ) ) )
(checksat)
(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))) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) ) (distinct (h 0 (carte x y))
(carte x y)) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h t (h ( 0 t) (carte x y)))
(carte x y)) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (t Real)) (distinct (h ( 0 t) (h t (carte x y)))
(carte x y)) ))
(checksat)
(pop)
and the corresponding output is
sat
unsat
unsat
unsat
unsat
Please run the code online
here.
Other example: proving that
forms a oneparameter group.
The proof is performed using the following Z3 code:
(declaresort S)
(declarefun carte (Real Real Real) S)
(declarefun h (Real S) S)
(declarefun a () Real)
(declarefun b () Real)
(declarefun 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)) ) ) ) )
(checksat)
(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))) ))
(checksat)
(pop)
(push)
(assert (forall ((x Real) (y Real) (z Real) ) (distinct (h 0 (carte x y z))
(carte x y z)) ))
(checksat)
(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)) ))
(checksat)
(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)) ))
(checksat)
(pop)
and the corresponding output is
sat
unsat
unsat
unsat
unsat
Please run this code online
here
Other example: To prove that
forms a oneparameter group.
The proof is given online
here and the fourdimensional extension is given online
here
A last couple of examples: Prove that
forms a oneparameter group.
The proof is given online
here.
Prove that
forms a oneparameter group.
The proof is given online
here
My questions are:

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

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