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:

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 .