Getting Started¶
In this section we will see how to install pySMT and how to solve a simple problem using it.
Installation¶
To run pySMT you need Python 3.5+ 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 PYTHONPATH
.
To check which solvers are visible to pySMT, you can use the command
pysmt-install
(simply 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
in the .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
the PYTHONPATH
. pysmt-install
has many options to
customize its behavior.
GMPY2¶
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,
otherwise the fractions
module from Python’s standard library is
used. The use of the gmpy library can be controlled by setting the
system environment variables PYSMT_GMPY2
to True
or
False
. If this is set to true and the gmpy library cannot be
imported, an exception will be thrown.
Cython¶
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
variable PYSMT_CYTHON
to True
or False
. If set to false,
the default pure python implementation will be used.
Hello World¶
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¶
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?
The Basics¶
The module 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.
We include the methods to create a new
Symbol()
(i.e., variables), and
typing information (the domain of the variable), that is defined in
pysmt.typing
, and we can write the following:
from pysmt.shortcuts import Symbol
from pysmt.typing import INT
h = Symbol("H", INT)
domain = (1 <= h) & (10 >= h)
When importing 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
pysmt.shortcuts
.
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
(such as
And()
,
Or()
,
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(25)))
formula = And(domains, problem)
print("Serialization of the formula:")
print(formula)
Note
Limited serialization
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
serialize()
method:
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))
Model extraction is provided by the get_model()
shortcut: if the
formula is unsatisfiable, it will return None
, otherwise a
Model
, that is a dict-like structure
mapping each Symbol to its value.
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
problem.
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")
In the example, we access the value of each symbol
(get_value()
), however, we can
also obtain a model object using get_model()
.
Note
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
get_model()
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., msat
):
Solver | pySMT name |
---|---|
MathSAT | msat |
Z3 | z3 |
CVC4 | cvc4 |
Yices | yices |
Boolector | btor |
Picosat | picosat |
CUDD | bdd |
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(25)))
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")
What’s Next?¶
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 .