active questions tagged z3  Stack Overflow News Feed
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?
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
Last example: 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
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
My questions are:

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

I claim that Z3 is the only system that is able to perform the proof. 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
My questions are:

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

I claim that Z3 is the only system that is able to perform the proof. Do you agree?
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 homebrewed 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?
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
My questions are:

It is possible to make the proof using arrays.

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