I’m new to z3 smt solver.I’m using the python API z3py.
I have a quick question concerning the output of the z3.solve() function.what does it mean when I call z3.solve() on some constraints and I get [] as an output? Also could someone refer me to a good documentation please
Advertisement
Answer
You really need to provide an input that causes this, as it really depends on your constraints. But here’s the simplest way to illustrate this behavior:
from z3 import * z3.solve([])
When I run this, I get:
[]
which is what you’re seeing, I presume. This essentially means that your system is trivially satisfiable for all variables; i.e., either you have no constraints, or they do not constrain the model in any particular way. In the above, there are no constraints, so we have the “trivial” model. If you do something more interesting, say:
from z3 import *
a, b = Ints('a b')
z3.solve([a > b, b > 3])
then you’ll see a more interesting model:
[b = 4, a = 5]
There’s plenty of documentation on z3, z3py, and SMTLib in general (which describes the underlying language all SMT solvers speak):
- For z3, start with https://rise4fun.com/z3/tutorial
- For z3 python bindings, use: https://ericpony.github.io/z3py-tutorial/guide-examples.htm
- General SMTLib info: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf
Note that z3 is scriptable from many other languages as well, including C, C++, Java, Scala, and Haskell to name a few. Usually it’s much easier to work in a higher-level language than directly with SMTLib or the bare-bones C-bindings. Python and Haskell (in my opinion) provide the highest-level of abstractions to simplify programming z3, but which environment you should choose really depends on what your overall goals are. (While most bindings support general constraint programming, they have different levels of automation and access to different z3 facilities.)