In this section we will see how to install pySMT and how to solve a simple problem using it.
To run pySMT you need Python 3.5+ or Python 2.7 installed. If no solver is installed, pySMT can still create and dump the SMT problem in SMT-LIB format. pySMT works with any SMT-LIB compatible solver. Moreover, pySMT can leverage the API of the following solvers:
- MathSAT (http://mathsat.fbk.eu/)
- Z3 (https://github.com/Z3Prover/z3/)
- CVC4 (http://cvc4.cs.nyu.edu/web/)
- Yices 2 (http://yices.csl.sri.com/)
- CUDD (http://vlsi.colorado.edu/~fabio/CUDD/)
- PicoSAT (http://fmv.jku.at/picosat/)
- Boolector (http://fmv.jku.at/boolector/)
The Python binding for the SMT Solvers must be installed and
accessible from your
To check which solvers are visible to pySMT, you can use the command
install.py in the sources):
$ pysmt-install --check
provides the list of installed solvers (and version). Solvers can be installed with the same script: e.g.,
$ pysmt-install --msat
installs the MathSAT5 solver.
By default the solvers are downloaded, unpacked and built in your home directory
.smt_solvers folder. Compiled libraries and actual solver packages are
installed in the relevant
site-packages directory (e.g. virtual environment’s
packages root or local user-site).
If you specified a custom
--bindings-path during install, you
can use the
--env option to obtain a string to update your
PYTHONPATH. When defaults are used, there’s not need to update
pysmt-install has many options to
customize its behavior.
PySMT supports the use of the
gmpy2 library (version
2.0.8 or later)
to handle multi-precision numbers. This provides an efficient way to
perform operations on big numbers, especially when fractions are
involved. The gmpy library is used by default if it is installed,
fractions module from Python’s standard library is
used. The use of the gmpy library can be controlled by setting the
system environment variables
False. If this is set to true and the gmpy library cannot be
imported, an exception will be thrown.
PySMT supports the use of Cython in order to
improve the performances of some internal component. If Cython is
installed, this will be used (by default) to compile the SMT-LIB
parser. The use of Cython can be controlled by setting the environment
False. If set to false,
the default pure python implementation will be used.
Any decent tutorial starts with a Hello World example. We will encode a problem as an SMT problem, and then invoke a solver to solve it. After digesting this example, you will be able to perform the most common operations using pySMT.
The problem that we are going to solve is the following:
Lets consider the letters composing the words HELLO and WORLD, with a possible integer value between 1 and 10 to each of them.
Is there a value for each letter so that H+E+L+L+O = W+O+R+L+D = 25?
pysmt.shortcuts provides the most used functions of the
library. These are simple wrappers around functionalities provided by
other objects, therefore, this represents a good starting point if you
are interested in learning more about pySMT.
from pysmt.shortcuts import Symbol from pysmt.typing import INT h = Symbol("H", INT) domain = (1 <= h) & (10 >= h)
pysmt.shortcuts, the infix notation is
enabled by default. Infix notation makes it very easy to experiment
with pySMT expressions (e.g., on the shell), however, it tends to make
complex code less clear, since it blurs the line between Python
operators and SMT operators. In the rest of the example, we will use
the textual operators by importing them from
from pysmt.shortcuts import Symbol, LE, GE, And, Int from pysmt.typing import INT h = Symbol("H", INT) # domain = (1 <= h) & (10 >= h) domain = And(LE(Int(1), h), GE(Int(10), h))
Instead of defining one variable at the time, we will use Python’s
comprehension to apply the same operation to multiple
symbols. Comprehensions are so common in pySMT that n-ary operators
Plus()) can accept am iterable object
(e.g. lists or generator).
from pysmt.shortcuts import Symbol, LE, GE, Int, And, Equals, Plus, Solver from pysmt.typing import INT hello = [Symbol(s, INT) for s in "hello"] world = [Symbol(s, INT) for s in "world"] letters = set(hello+world) domains = And(And(LE(Int(1), l), GE(Int(10), l)) for l in letters) sum_hello = Plus(hello) sum_world = Plus(world) problem = And(Equals(sum_hello, sum_world), Equals(sum_hello, Int(36))) formula = And(domains, problem) print("Serialization of the formula:") print(formula)
By default printing of a string is limited in depth. For big
formulas, you will see something like
(x & (y | ... )),
where deep levels of nestings are replaced with the ellipses
.... This generally provides you with an idea of how the
structure of the formula looks like, without flooding the
output when formulas are huge. If you want to print the
whole formula, you need to call the
print(formula) # (x & (y | ... )) print(formula.serialize()) # (x & (y | (z | y)))
Defaults methods for formula allow for simple printing. Checking satisfiability can also be done with a one-liner.
print("Checking Satisfiability:") print(is_sat(formula))
print("Serialization of the formula:") print(formula) print("Checking Satisfiability:") print(is_sat(formula))
Shortcuts are very useful for one off operations. In many cases,
however, you want to create an instance of a
Solver and operate on it
incrementally. This can be done using the
pysmt.shortcuts.Solver() factory. This factory can be used
within a context (
with statement) to automatically handle
destruction of the solver and associated resources. After creating the
solver, we can assert parts of the formula and check their
satisfiability. In the following snippet, we first check that the
domain formula is satisfiable, and if so, we continue to solve the
with Solver(name="z3") as solver: solver.add_assertion(domains) if not solver.solve(): print("Domain is not SAT!!!") exit() solver.add_assertion(problem) if solver.solve(): for l in letters: print("%s = %s" %(l, solver.get_value(l))) else: print("No solution found")
Incrementality and Model Construction
Many solvers can perform aggressive simplifications if
incrementality or model construction are not required. Therefore,
if you do not need incrementality and model construction, it is
better to call
is_sat(), rather than instantiating a
solver. Similarly, if you need only one model, you should use
With pySMT it is possible to run the same code by using different
solvers. In our example, we can specify which solver we want to run by
changing the way we instantiate it. If any other solver is installed,
you can try it by simply changing
name="z3" to its codename (e.g.,
You can also not specify the solver, and simply state which Logic must
be supported by the solver, this will look into the installed solvers
and pick one that supports the logic. This might raise an exception
NoSolverAvailableError), if no logic for
the logic is available.
Here is the complete example for reference using the logic QF_LIA:
from pysmt.shortcuts import Symbol, LE, GE, Int, And, Equals, Plus, Solver from pysmt.typing import INT hello = [Symbol(s, INT) for s in "hello"] world = [Symbol(s, INT) for s in "world"] letters = set(hello+world) domains = And(And(LE(Int(1), l), GE(Int(10), l)) for l in letters) sum_hello = Plus(hello) sum_world = Plus(world) problem = And(Equals(sum_hello, sum_world), Equals(sum_hello, Int(36))) formula = And(domains, problem) print("Serialization of the formula:") print(formula) with Solver(logic="QF_LIA") as solver: solver.add_assertion(domains) if not solver.solve(): print("Domain is not SAT!!!") exit() solver.add_assertion(problem) if solver.solve(): for l in letters: print("%s = %s" %(l, solver.get_value(l))) else: print("No solution found")
This simple example provides the basic ideas of how to work with
pySMT. The best place to understand more about pySMT is the
pysmt.shortcuts module. All the important functionalities are exported
there with a simple to use interface.
To understand more about other functionalities of pySMT, you can take a look at the examples/ folder .