# 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+ 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 `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. Once the installation is complete, you
can use the option `--env`

to obtain a string to update your
`PYTHONPATH`

:

```
$ pysmt-install --env
export PYTHONPATH="/home/pysmt/.smt_solvers/python-bindings-2.7:${PYTHONPATH}"
```

By default the solvers are installed in your home directory in the
folder `.smt_solvers`

. `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

HELLOandWORLD, 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(36)))
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(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")
```

## 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 .