active questions tagged z3 - Stack Overflow News Feed
Tuesday, November 24, 2015  |

Suppose I want to check the trace information of "random_split". I wrote

enable_trace("random_split")


in my python script that is using z3 python api, but nothing shows up.

I wonder how should I check trace information when using z3py?

Monday, November 23, 2015  |

This is a follow-up question of What is the importance of the order of the assertions in Z3?

Given that Z3 uses DPLL algorithms. Suppose I have some knowledge about which variables are more critical. Is it possible that I make Z3 solver to branch on these variables first when evaluating my logic problem so as to boost the performance or efficiency?

Sunday, November 22, 2015  |

I have seen that Z3 supports optimization via e.g. assert-soft. From what I understood, if given sufficient time, Z3 will report the optimal solution for a given SMT formula.

However, I am interested if it is possible to run Z3 for a limited amount of time and have it report the best solution it can find (which does not necessarily mean it is the optimal solution).

If I run Z3 on a SMT formula and restrict the time (via parameter -T), it will just report 'timeout' if it did not solve it optimally. I read that the default wmax solver uses a simple procedure to bounds weights and am curious to whether it is possible to bound the weights from an upper bound, rather than a lower bound.

Regards,
Emir

Sunday, November 22, 2015  |

I'm modifying a tool which uses Z3 (specifically the Python API) to solve bitvector constraints. I need to use a particular external SAT solver instead of the internal Z3 one, so I'm first bit-blasting using the tactic

Then('simplify', 'bit-blast', 'tseitin-cnf')


after which I can relatively easily dump the clauses to a DIMACS file. The problem is mapping the resulting propositional model back to a model of the original constraints: as far as I can tell, the Python API doesn't provide a way to access the model converter corresponding to a tactic. Is this true? If so, can it be done using a different API, or is there an easier way altogether? Basically I just need to know how the propositional variables in the final CNF clauses correspond to the original bitvector variables.

Thursday, November 19, 2015  |

Is it possible to update an enumerated sort by adding (or removing) a symbol to it? What I would like to do is to add a new value to the list of symbols (see below) even after a variable, say "X", is created from that sort.

EnumSort eSort = con.mkEnumSort(name,symbols);
SetSort eSetSort = con.mkSetSort(eSort);


If I create a new enumerated sort and get a value "v" then I get an error "domain sort and parameter do not match" for the expression v \in X (membership).

Thursday, November 19, 2015  |

I build the formula in z3 using the java API.
However, I have some formula that are difficult to solve, and I want to investigate why. Therefore, I want to print the formula in SMTLIB2 format.

Is it possible to get that from a Solver object. Currently, what I can get is only an array of assertions. Thank you.

Thursday, November 19, 2015  |

I've tried to find the number of the variables in Z3 statistics but I couldn't find any indications.Can any one help about which one of the following statistics is number of the variables.

Please note I'm looking for precisely the number of the variables not the number of clauses.

(:added-eqs                   9977
:binary-propagations         9922
:conflicts                   367
:decisions                   132793
:del-clause                  244104
:final-checks                30
:lazy-quant-instantiations   334
:max-generation              11
:max-memory                  15.36
:memory                      4.29
:minimized-lits              2
:missed-quant-instantiations 49
:mk-clause                   245835
:num-allocs                  2987116.00
:propagations                108837
:quant-instantiations        124407
:restarts                    17
:rlimit-count                13420765)


Wednesday, November 18, 2015  |

I am using z3 in visual studio and I want to do a simple check with the following
x > 3
After I run my code, I only get one result back in my model. Why do I only get one result back and how would I do model completion in C#?

Tuesday, November 17, 2015  |

I am working on a component of a research tool;
I am interested in retrieving (for QF_LRA)

-multiple (minimal or otherwise) UNSAT cores and

-multiple SAT assignments

I have checked the forum for earlier discussions on this topic e.g.,
How to get different unsat cores when using z3 on logic QF_LRA

They refer to the z3 Python tutorial(s)
e.g, http://rise4fun.com/Z3Py/tutorial/musmss

which seems to be offline for now. I have tried other suggestions of github etc to find the mentioned tutorial, but have had no luck.

I am using the z3 Java API; but happy to switch to alternatives.

Tuesday, November 17, 2015  |

I've tried to find the number of the variables in Z3 statistics but I couldn't find any indications.Can any one help about which one of the following statistics is number of the variables.

Please note I'm looking for precisely the number of the variables not the number of clauses.

(:added-eqs                   9977
:binary-propagations         9922
:conflicts                   367
:decisions                   132793
:del-clause                  244104
:final-checks                30
:lazy-quant-instantiations   334
:max-generation              11
:max-memory                  15.36
:memory                      4.29
:minimized-lits              2
:missed-quant-instantiations 49
:mk-clause                   245835
:num-allocs                  2987116.00
:propagations                108837
:quant-instantiations        124407
:restarts                    17
:rlimit-count                13420765)


Monday, November 16, 2015  |

I've tried to find the number of the variables in Z3 statistics but I couldn't find any indications.Can any one help about which one of the following statistics is number of the variables.

Please note I'm looking for precisely the number of the variables not the number of clauses.

(:added-eqs                   9977
:binary-propagations         9922
:conflicts                   367
:decisions                   132793
:del-clause                  244104
:final-checks                30
:lazy-quant-instantiations   334
:max-generation              11
:max-memory                  15.36
:memory                      4.29
:minimized-lits              2
:missed-quant-instantiations 49
:mk-clause                   245835
:num-allocs                  2987116.00
:propagations                108837
:quant-instantiations        124407
:restarts                    17
:rlimit-count                13420765)


Thanks

Monday, November 16, 2015  |

I am currently writing an automatic Verifier for my programming language on top of Z3 as a fun project and I am trying to use it to prove that a fibonacci implementation using a loop is equivalent to one with recursion.

It seems to work if the input program is correct, i.e. it generates reasonable input for Z3 and Z3 says it is unsatisfiable, which means in my context, that the program is correct. But when I changed one variable initialization and thereby render the program incorrect, my verifier came up with the following Z3 formula which doesn't seem too complicated to me, but Z3 says "unknown".

(set-option :smt.auto-config false)
(set-option :smt.mbqi false)
(declare-fun fib (Int) Int)
(declare-fun fakeFib (Int) Int)
(declare-fun n () Int)
(assert (forall ((n Int))
(! (= (fib n)
(ite (= n 0) 0
(ite (= n 1) 1
(+ (fakeFib (- n 1)) (fakeFib (- n 2))))))
:pattern ((fib n)))))
(assert (forall ((n Int))
(! (= (fib n) (fakeFib n)) :pattern ((fib n)))))
(assert (>= n 0))
(assert (not (and (<= 0 n) (= 1 (fib 1)) (= 1 (fib 0)))))
(check-sat)


Note that the two quantifiers represent the recursive definition of fibonacci. A friend of mine told me this trick to avoid a matching loop: Instead of defining fib as a recursive function, I introduce another function fakeFib for which I don't provide the definition and I use that one in the recursive definition of fib. Also, I tell the verifier that they are equal, but that quantifier only gets a pattern for fib, not for fakeFib. Because of the restrictive patterns, it is incomplete, i.e., it can only prove the correctness of the program as long as looking at one level of recursion suffices to prove it (but it can easily be extended to k levels). But I can live with that restriction in order to avoid matching loops.

The "bug" of the code was that I initialized a variable incorrectly and this eventually lead to the incorrect component (= 1 (fib 0)) in the last assertion. For the correct program, it would be (= 0 (fib 0)).

Some observations:

• If I replace (= 1 (fib 0)) by (= 0 (fib 0)), then Z3 immediately finds that it is unsatisfiable.
• Previously, I did not have the options (set-option :smt.auto-config false) and (set-option :smt.mbqi false) set and then it ran out of memory on my machine and out of time on rise4fun.
• Setting (set-option :smt.macro-finder true) which seems to have worked for people with similar questions didn't work for me. I am guessing that this is caused by the fact that I have two quantifiers for fib and not just one.
• I tried using cvc4 as a comparison and it said "unknown" immediately. So my problems don't seem to be Z3 specific.
• The formula is clearly satisfiable. (= 1 (fib 0)) is false, therefore the whole last assertion is automatically true. (>= n 0) is also easy to satisfy.

Monday, November 16, 2015  |

I am working on a component of a research tool;
I am interested in retrieving (for QF_LRA)

-multiple (minimal or otherwise) UNSAT cores and

-multiple SAT assignments

I have checked the forum for earlier discussions on this topic e.g.,
How to get different unsat cores when using z3 on logic QF_LRA

They refer to the z3 Python tutorial(s)
e.g, http://rise4fun.com/Z3Py/tutorial/musmss

which seems to be offline for now. I have tried other suggestions of github etc to find the mentioned tutorial, but have had no luck.

If someone can please answer my question or point me to the location of this tutorial.

I am using the z3 Java API; but happy to switch to alternatives.

Sunday, November 15, 2015  |

I am working on a component of a research tool;
I am interested in retrieving (for QF_LRA)

-multiple (minimal or otherwise) UNSAT cores and

-multiple SAT assignments

I have checked the forum for earlier discussions on this topic e.g.,
How to get different unsat cores when using z3 on logic QF_LRA

They refer to the z3 Python tutorial(s)
e.g, http://rise4fun.com/Z3Py/tutorial/musmss

which seems to be offline for now. I have tried other suggestions of github etc to find the mentioned tutorial, but have had no luck.

If someone can please answer my question or point me to the location of this tutorial.

I am using the z3 Java API; but happy to switch to alternatives.

Sunday, November 15, 2015  |

I am currently writing an automatic Verifier for my programming language on top of Z3 as a fun project and I am trying to use it to prove that a fibonacci implementation using a loop is equivalent to one with recursion.

It seems to work if the input program is correct, i.e. it generates reasonable input for Z3 and Z3 says it is unsatisfiable, which means in my context, that the program is correct. But when I changed one variable initialization and thereby render the program incorrect, my verifier came up with the following Z3 formula which doesn't seem too complicated to me, but Z3 says "unknown".

(set-option :smt.auto-config false)
(set-option :smt.mbqi false)
(declare-fun fib (Int) Int)
(declare-fun fakeFib (Int) Int)
(declare-fun n () Int)
(assert (forall ((n Int))
(! (= (fib n)
(ite (= n 0) 0
(ite (= n 1) 1
(+ (fakeFib (- n 1)) (fakeFib (- n 2))))))
:pattern ((fib n)))))
(assert (forall ((n Int))
(! (= (fib n) (fakeFib n)) :pattern ((fib n)))))
(assert (>= n 0))
(assert (not (and (<= 0 n) (= 1 (fib 1)) (= 1 (fib 0)))))
(check-sat)


Note that the two quantifiers represent the recursive definition of fibonacci. A friend of mine told me this trick to avoid a matching loop: Instead of defining fib as a recursive function, I introduce another function fakeFib for which I don't provide the definition and I use that one in the recursive definition of fib. Also, I tell the verifier that they are equal, but that quantifier only gets a pattern for fib, not for fakeFib. Because of the restrictive patterns, it is incomplete, i.e., it can only prove the correctness of the program as long as looking at one level of recursion suffices to prove it (but it can easily be extended to k levels). But I can live with that restriction in order to avoid matching loops.

The "bug" of the code was that I initialized a variable incorrectly and this eventually lead to the incorrect component (= 1 (fib 0)) in the last assertion. For the correct program, it would be (= 0 (fib 0)).

Some observations:

• If I replace (= 1 (fib 0)) by (= 0 (fib 0)), then Z3 immediately finds that it is unsatisfiable.
• Previously, I did not have the options (set-option :smt.auto-config false) and (set-option :smt.mbqi false) set and then it ran out of memory on my machine and out of time on rise4fun.
• Setting (set-option :smt.macro-finder true) which seems to have worked for people with similar questions didn't work for me. I am guessing that this is caused by the fact that I have two quantifiers for fib and not just one.
• I tried using cvc4 as a comparison and it said "unknown" immediately. So my problems don't seem to be Z3 specific.
• The formula is clearly satisfiable. (= 1 (fib 0)) is false, therefore the whole last assertion is automatically true. (>= n 0) is also easy to satisfy.

Sunday, November 15, 2015  |

I'm having trouble getting the z3 datalog engine to work. I copied the example from the tutorial

Z 64

P0(x: Z) input
Gt0(x : Z, y : Z) input
R(x : Z) printtuples
S(x : Z) printtuples
Gt(x : Z, y : Z) printtuples
Gt(x,y) :- Gt0(x,y).
Gt(x,y) :- Gt(x,z), Gt(z,y).
R(x) :- Gt(x,_).
S(x) :- Gt(x,x0), Gt0(x,y), Gt0(y,z), P0(z).
Gt0("a","b").
Gt0("b","c").
Gt0("c","d").
Gt0("a1","b").
Gt0("b","a1").
Gt0("d","d1").
Gt0("d1","d").
P0("a1").


and ran both bddbddb and z3. bddbddb gives the answer

Tuples in S: (2.)
(x=a(0))
(x=a1(4))
Tuples in Gt: (21.)
(x=a(0),y=a1(4))
(x=a1(4),y=a1(4))
(x=a(0),y=c(2))
(x=a1(4),y=c(2))
(x=a(0),y=b(1))
(x=a(0),y=d1(5))
(x=a1(4),y=b(1))
(x=a1(4),y=d1(5))
(x=a(0),y=d(3))
(x=a1(4),y=d(3))
(x=c(2),y=d1(5))
(x=c(2),y=d(3))
(x=b(1),y=a1(4))
(x=b(1),y=c(2))
(x=b(1),y=b(1))
(x=b(1),y=d1(5))
(x=b(1),y=d(3))
(x=d1(5),y=d1(5))
(x=d1(5),y=d(3))
(x=d(3),y=d1(5))
(x=d(3),y=d(3))


z3 doesn't seem to do anything at all

Tuples in Gt:
Tuples in R:
Tuples in S:
--------------
original rules
; rule count: 4
; predicate count: 3
; output: Gt
; output: R
; output: S
Gt(#0,#1) :-
Gt0(#0,#1).
Gt(#0,#1) :-
Gt(#0,#2),
Gt(#2,#1).
R(#0) :-
Gt(#0,#1).
S(#0) :-
Gt(#0,#1),
Gt0(#0,#2),
Gt0(#2,#3),
P0(#3).
---------------
generated rules
; rule count: 0
; predicate count: 0
; output: Gt
; output: R
; output: S
--------------
instructions
--------------
big relations
bytes 0
bytes   rows    annotation
--------------
relation sizes
Relation P0 has size 1
Relation Gt0 has size 7


What am I doing wrong? In particular, how can I obtain the complete relations after saturation?

Tuesday, November 10, 2015  |

I am trying to solve a problem, for example I have a 4 point and each two point has a cost between them. Now I want to find a sequence of nodes which total cost would be less than a bound. I have written a code but it seems not working. The main problem is I have define a python function and trying to call it with in a constraint.

Here is my code: I have a function def getVal(n1,n2): where  n1, n2 are Int Sort. The line Nodes = [ Int("n_%s" % (i)) for i in range(totalNodeNumber) ] defines 4 points as Int sort and when I am adding a constraint s.add(getVal(Nodes[0], Nodes[1]) + getVal(Nodes[1], Nodes[2]) < 100) then it calls getVal function immediately. But I want that, when Z3 will decide a value for Nodes[0], Nodes[1], Nodes[2], Nodes[3] then the function should be called for getting the cost between to points.

from z3 import *
import random

totalNodeNumber = 4
Nodes = [ Int("n_%s" % (i)) for i in range(totalNodeNumber) ]
def getVal(n1,n2):
# I need n1 and n2 values those assigned by Z3
cost = random.randint(1,20)
print cost
return IntVal(cost)

s = Solver()

#constraint: Each Nodes value should be distinct
nodes_index_distinct_constraint  = Distinct(Nodes)
s.add(nodes_index_distinct_constraint)

#constraint: Each Nodes value should be between 0 and totalNodeNumber
def get_node_index_value_constraint(i):
return And(Nodes[i] >= 0, Nodes[i] < totalNodeNumber)
nodes_index_constraint  = [ get_node_index_value_constraint(i) for i in range(totalNodeNumber)]
s.add(nodes_index_constraint)

#constraint: Problem with this constraint
# Here is the problem it's just called python getVal function twice without assiging Nodes[0],Nodes[1],Nodes[2] values
# But I want to implement that - Z3 will call python function during his decission making of variables
s.add(getVal(Nodes[0], Nodes[1]) + getVal(Nodes[1], Nodes[2]) + getVal(Nodes[2], Nodes[3]) < 100)

if s.check() == sat:
print "SAT"
print "Model: "
m = s.model()
nodeIndex = [ m.evaluate(Nodes[i]) for i in range(totalNodeNumber) ]
print nodeIndex
else:
print "UNSAT"
print "No solution found !!"


If this is not a right way to solve the problem then could you please tell me what would be other alternative way to solve it. Can I encode this kind of problem to find optimal sequence of way points using Z3 solver?

Tuesday, November 10, 2015  |

Setting timeout is always a hot topic, and there are many related answers, however, a new warning shows up in the latest unstable-branch of Z3 (4.4.2) (Ubuntu-12.04-64).

Pure C API is used in my project, I use Z3_assert_cnstr() to add a constraint, and Z3_check_and_get_model() to check result.

I set the timeout with:

Z3_set_param_value(cfg, "timeout", "10");

with 10 milliseconds.

When I run the project, there is a warning like:

WARNING: unknown parameter 'timeout'
Legal parameters are:
auto_config (bool) (default: true)
debug_ref_count (bool) (default: false)
dump_models (bool) (default: false)
model (bool) (default: true)
model_validate (bool) (default: false)
proof (bool) (default: false)
rlimit (unsigned int) (default: 4294967295)
smtlib2_compliant (bool) (default: false)
timeout (unsigned int) (default: 4294967295)
trace (bool) (default: false)
trace_file_name (string) (default: z3.log)
type_check (bool) (default: true)
unsat_core (bool) (default: false)
well_sorted_check (bool) (default: false)


and from the specification, "timeout" is a legal parameter.

Is there something I missed?

I tested using "10u" instead of "10" as the third parameter to indicate a unsigned number, however, nothing is changed. Besides, an ASSERTION VIOLATION fixed from master branch is the reason for me to use unstable-branch.

Monday, November 9, 2015  |

Setting timeout is always a hot topic, and there are much related answers, however, a new warning shows up in the latest unstable-branch of Z3 (4.4.2) (Ubuntu-12.04-64).

Pure C API is used in my project, I use Z3_assert_cnstr() to add a constraint, and Z3_check_and_get_model() to check result.

Timeout is set as:

Z3_set_param_value(cfg, "timeout", "10");

with 10 milliseconds.

where run the project, there is a warning like:

WARNING: unknown parameter 'timeout' Legal parameters are: auto_config (bool) (default: true) debug_ref_count (bool) (default: false) dump_models (bool) (default: false) model (bool) (default: true) model_validate (bool) (default: false) proof (bool) (default: false) rlimit (unsigned int) (default: 4294967295) smtlib2_compliant (bool) (default: false) timeout (unsigned int) (default: 4294967295) trace (bool) (default: false) trace_file_name (string) (default: z3.log) type_check (bool) (default: true) unsat_core (bool) (default: false) well_sorted_check (bool) (default: false)

and from the specification, "timeout" is a legal parameter.

is there something I missed?

BTW, I tested using "10u" instead of "10" as the third parameter to indicate a unsigned number, however, nothing is changed. Besides, a ASSERTION VIOLATION fixed from master branch is the reason for me to use unstable-branch.

Sunday, November 8, 2015  |

I am using the following Python function to model Xor constraints with an arbitrary number of variables for Microsoft's Z3 solver with Python API:

#  parity function
#  break up long input lists in two smaller lists
def odd(solver, lits):
length = len(lits)
check(length > 0, "Odd needs argument(s)")
if length == 1:
solver.add(lits[0])
elif length == 2:
solver.add(Xor(lits[0], lits[1]))
elif length == 3:
solver.add(Xor(lits[0], Xor(lits[1], lits[2])))
elif length == 4:
#  this symmetric form is much faster than the chained forms
solver.add(Xor(Xor(lits[0], lits[1]), Xor(lits[2], lits[3])))
else:
aux = get_aux_variable()

#  cf. http://www.gregorybard.com/papers/bard_thesis.pdf
cut_len = 3
odd(solver, lits[:cut_len] + [aux])
odd(solver, [aux] + lits[cut_len:])

auxVariableIdx = 0

def get_aux_variable():
global auxVariableIdx

auxVariableIdx += 1
aux = Bool('t%s' % auxVariableIdx)
return aux


I've noticed that the overall solver performance depends quite a lot on the way, the smaller Xor sub-cases are modelled. Example: I am using "Xor(Xor(a,b), Xor(c,d))" to declare an Xor with four inputs. The alternative "Xor(a,Xor(b,Xor(c,d)))" turned out to be slower by a factor of ten for my examples.

Another example: It makes a big difference if the auxiliary switching variable created to link sub-expressions is added to the inputs lists at the front or at the back of the list.

What is the recommended way to model Xor constraints with many variables in z3py?

active questions tagged z3 - Stack Overflow News Feed

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

No comments yet.