# pySMT: one Python API over seven SMT solvers and any SMT-Lib compliant binary

> pySMT is a solver-agnostic library for building and solving Satisfiability Modulo Theory formulae in Python, supporting MathSAT, Z3, cvc5, Yices, CUDD, PicoSAT and Boolector natively plus any SMT-Lib 2 solver through a generic adapter. The point is that a formula you build stays the same object no matter which engine answers it.

**pysmt/pysmt** — pySMT: A library for SMT formulae manipulation and solving

- Repository: https://github.com/pysmt/pysmt
- Stars: 641 · Forks: 150
- Language: Python
- License: Apache-2.0
- Published: 2026-10-21 · Updated: 2026-10-21 · Language: en
- Canonical page: https://hysenlabs.com/projects/pysmt-pysmt

## The formula is the object, the solver is a parameter

pySMT makes working with Satisfiability Modulo Theory simple, and the four capabilities it lists are the clearest statement of what that means.

Define formulae in a simple, intuitive, and solver independent way. Solve your formulae using one of the native solvers, or by wrapping any SMT-Lib compliant solver. Dump your problems in the SMT-Lib format. And more.

Solver independence is the load-bearing word. A pySMT formula is not a Z3 expression or a MathSAT expression. It is a pySMT object, and it is translated to whatever the target engine needs at solve time. That is the architectural decision, and everything else in the library follows from it.

The first example in the README shows the whole model in six lines.

```python
>>> from pysmt.shortcuts import Symbol, And, Not, is_sat
>>> varA = Symbol("A") # Default type is Boolean
>>> varB = Symbol("B")
>>> f = And(varA, Not(varB))
>>> f
(A & (! B))
>>> is_sat(f)
True
```

A symbol is created with a name and, implicitly, a type. The default is Boolean. The formula is built with And and Not, and its printed form is a readable infix-ish representation rather than a solver's internal node dump, which is the kind of detail that determines whether you can debug a model by looking at it.

Then substitution.

```python
>>> g = f.substitute({varB: varA})
>>> g
(A & (! A))
>>> is_sat(g)
False
```

Substitute rewrites the formula with a mapping, and the result is a new formula that the library can reason about symbolically rather than only hand to a solver. That distinction is the difference between a formula library and a thin wrapper over one engine.

The shortcuts module is the front door, and is_sat is the one call most scripts need.

## Typing is explicit, and the theory coverage is broad

The typing model is where the library earns its keep on real problems, and the more complex example in the README is worth reading closely because it shows the pieces working together.

The example asks whether there is a value for each letter between 1 and 9 so that the letters in HELLO and WORLD sum to the same value, and that value is 25. The first line of the code imports the operators and the typing module.

```python
from pysmt.shortcuts import Symbol, And, GE, LT, Plus, Equals, Int, get_model
from pysmt.typing import INT
```

Symbols are created per character with an explicit INT type, the set of letters is taken from the union of the two words, and the domain constraint is built as a conjunction of per-letter bounds.

```python
  domains = And([And(GE(l, Int(1)),
                     LT(l, Int(10))) for l in letters])
```

The arithmetic is expressed with Plus and Equals, and the n-ary operators take lists directly, which the README calls out explicitly with a comment.

```python
  sum_hello = Plus(hello) # n-ary operators can take lists
  sum_world = Plus(world) # as arguments
  problem = And(Equals(sum_hello, sum_world),
                Equals(sum_hello, Int(25)))
  formula = And(domains, problem)
```

So the formula is a conjunction of a domain constraint and a problem constraint, and get_model either returns a model or nothing. The library supports Linear Real Arithmetic, Real Difference Logic, Equalities and Uninterpreted Functions, Bit-Vectors, Arrays, Strings and their combinations.

Strings are worth pausing on, because they are the newest addition in that list and the one that changes what the library is for. A solver for arithmetic constraints over integers is a verification tool. A solver that also handles string theory is a tool for symbolic reasoning about programs that manipulate text, and the examples directory has a strings.py file and a sudoku/ directory, which suggests the library is being pushed towards constraint puzzles as well as formal verification.

The type discipline is what makes combinations possible. A formula mixing integers and strings has to be rejected somewhere, and the typing module is where that check lives.

## Seven native solvers and a generic path for everything else

The solver coverage comes in two tiers, and the distinction matters because it determines how much setup you are signing up for.

The native tier is MathSAT, Z3, cvc5, Yices 2, CUDD, PicoSAT and Boolector. A native binding means pySMT talks to the engine through its own Python API, which is faster than going through a text format and lets you use features the SMT-Lib interface does not expose.

The generic tier is any SMT-LIB 2 compliant solver, and the README documents how to register one.

```python
   from pysmt.shortcuts import Symbol, get_env, Solver
   from pysmt.logics import QF_UFLRA

   name = "mathsat-smtlib" # Note: The API version is called 'msat'

   # Path to the solver. The solver needs to take the smtlib file from
   # stdin. This might require creating a tiny shell script to set the
   # solver options.
   path = ["/tmp/mathsat"]
   logics = [QF_UFLRA,]    # List of the supported logics

   # Add the solver to the environment
   env = get_env()
   env.factory.add_generic_solver(name, path, logics)
```

The mechanism is that you register a name, a path and the list of logics the solver supports, and from then on that name works anywhere pySMT would accept an API solver name. The comment about the solver taking the SMT-Lib file from stdin is the practical detail, and the suggestion to write a tiny shell script to set options is the escape hatch for solvers whose command line does not line up with what the interface expects.

The logic is declared as a pySMT object rather than a string, with QF_UFLRA imported from pysmt.logics. That is how pySMT knows what fragment it is allowed to put in front of the solver, and declaring it is a correctness step rather than documentation.

Three of the native solvers are not native in the usual sense. For Yices, picosat and CUDD, pySMT uses external wrappers: yicespy, repycudd and pyPicoSAT, each a separate project under the pysmt organisation. The main library therefore does not carry the bindings for those three, which is why installation is more involved for them.

## Portfolio solving runs several engines and configurations at once

Portfolio solving consists of running multiple solvers in parallel, and pySMT provides a simple interface to perform portfolio solving using multiple solvers and multiple solver configurations.

The example shows why multiple configurations of the same solver is the interesting case.

```python
   from pysmt.shortcuts import Portfolio, Symbol, Not

   x, y = Symbol("x"), Symbol("y")
   f = x.Implies(y)

   with Portfolio(["cvc5",
                   "yices",
                   ("msat", {"random_seed": 1}),
                   ("msat", {"random_seed": 17}),
                   ("msat", {"random_seed": 42})],
                  logic="QF_UFLIRA",
                  incremental=False,
                  generate_models=False) as s:
     s.add_assertion(f)
     s.push()
     s.add_assertion(x)
     res = s.solve()
     v_y = s.get_value(y)
     print(v_y) # TRUE

     s.pop()
     s.add_assertion(Not(y))
     res = s.solve()
     v_x = s.get_value(x)
     print(v_x) # FALSE
```

Five entries, two of them plain solver names and three the same MathSAT solver with different random seeds. The portfolio races them and takes the first answer. That is a well-known technique for hard instances, since a solver's performance on a particular formula is often a coin flip decided by its internal heuristics and seed.

The interface is also incremental, and the example exercises push and pop around it. You add an assertion, push a scope, add another, solve, pop back, and the state is restored. That is the API you need for a bounded model check or a reachability query, where you ask whether a state is reachable and then want to explore the next state without rebuilding the formula.

Note the logic declaration of QF_UFLIRA and the two flags. incremental=False and generate_models=False say what the portfolio is and is not allowed to do: it will answer satisfiable or unsatisfiable but will not produce models or maintain scope. The examples directory has parallel.py and portfolio.py alongside allsat.py and allsmt.py, which cover the enumeration cases where you want every model rather than one.

The formulas use the method form too, x.Implies(y), rather than the functional style, which is a pySMT convenience for binary operators.

## Installing means installing a solver too, and that is where it gets awkward

The installation story has two halves and the second half is the one people hit.

The library itself is a pip install.

```bash
$ pip install pysmt
```

That additionally installs the pysmt-install command, which is used to install the solvers. Checking what is already reachable is one command.

```bash
$ pysmt-install --check
```

It will show you which solvers have been found in your PYTHONPATH. PySMT does not depend directly on any solver, but if you want to perform solving, you need to have at least one solver installed, and that can be used by pySMT via its native API or by passing through an SMT-Lib file.

So a working pySMT install is two things: the library and an engine. Installing MathSAT is another single command.

```bash
$ pysmt-install --msat
```

By default the solvers are downloaded, unpacked and built in your home directory in the .smt_solvers folder, with compiled libraries and the actual solver packages installed in the relevant site-packages directory, for example a virtual environment's packages root or the local user-site.

The limitation is stated in a note that deserves reading. This script does not install required dependencies for building the solver, for example make or gcc, and it has been tested mainly on Linux Debian and Ubuntu systems. The suggestion is to refer to the documentation of each solver for how to install it with its Python bindings.

So on a Mac, on Windows, or on a locked-down Linux box without a build toolchain, pysmt-install will not get you a working solver on its own. The documented path there is to install the engine's own Python bindings yourself and make sure they are importable, since pySMT assumes that the python bindings for the SMT Solver are installed and accessible from your PYTHONPATH.

One more practical note: if you have multiple versions of python in your system, the recommended syntax is python -m pysmt install, which pins the script to the interpreter running it.

## Where pySMT is the wrong tool

The first wrong-tool case is a project that wants a single engine and no abstraction. If your verification effort targets Z3 specifically, using Z3's Python API directly gives you its full surface, its own tactics, its own diagnostic output and its own error handling. pySMT deliberately keeps a common subset so it can drive seven engines plus an unbounded number of SMT-Lib binaries, and anything engine specific is outside that subset by construction. The wrapper is a cost you pay for portability, and if you do not need portability it is a cost with no return.

The second case is a heavy performance workload. Going through a translation layer and a text format has a price. The native bindings are there partly to reduce it, but the library is not where you would go for throughput on a single hard instance; the portfolio mode exists precisely because a single engine's performance is unreliable.

The third case is a solver that is not SMT-Lib 2 compliant and has no Python bindings. The generic path requires the solver to speak SMT-Lib on stdin, so a solver that only offers a C API or a bespoke RPC interface cannot be plugged in without writing something yourself.

The fourth case is a team that needs the library to be quiet. pySMT assumes the solver bindings are importable from the PYTHONPATH, and pysmt-install builds solvers in your home directory and installs them into site-packages. That is a deliberate convenience, and in a locked-down environment with a read-only home and a restricted pip it is an obstacle. The README does not document a fully manual, no-download install path beyond pointing you at each solver's own documentation.

On the practical side, the repository is in a steady state rather than a fast-moving one. The release history shows v0.9.6 from 2024-06-24, v0.9.5 from 2022-05-28 and v0.9.0 from 2020-04-26, and the last push was on 2026-10-06. A version below 1.0 also signals that the API is not promised to be stable, which matters if you are building a service on top of it. The licence is Apache-2.0, with the LICENSE and NOTICE files at the repository root and a release_checklist-style setup.py that reads the version from the package itself, so packaging is conventional.

What you get is a formula layer that keeps your model independent of your engine, and the examples directory, which includes a sudoku/ directory, model_checking.py, ltl.py, qe.py and efsmt.py, shows the range of problems people have used it for.

## Conclusion

pySMT suits a researcher or verification engineer who writes formulae once and wants to try several engines against them, or who wants to swap a solver without rewriting the model, since the formula objects are solver independent and the portfolio interface runs several configurations in parallel. It does not suit someone who wants a self-contained install, because no solver is bundled and pysmt-install assumes a Linux machine with a build toolchain. Before adopting, run pysmt-install --check to see which solvers are already reachable on your PYTHONPATH, and decide whether to bind to the native API of one engine or to write against the SMT-Lib interface so the engine stays replaceable.

## FAQ

### What is pySMT?

pySMT is a solver-agnostic Python library for manipulating and solving SMT formulae. You define formulae in a solver independent way, solve them with a native solver or any SMT-Lib compliant solver, and dump problems in the SMT-Lib format.

### How do I install pySMT and a solver?

Run pip install pysmt, which also installs the pysmt-install command. Use pysmt-install --check to see which solvers are already on your PYTHONPATH, and pysmt-install --msat to install MathSAT 5. The script does not install build dependencies such as make or gcc and has been tested mainly on Linux Debian and Ubuntu.

### Which solvers does pySMT support?

MathSAT, Z3, cvc5, Yices 2, CUDD, PicoSAT and Boolector are supported through native APIs, and any SMT-LIB 2 compliant solver can be registered as a generic solver with a name, a path and a list of supported logics. Yices, PicoSAT and CUDD are reached through external wrappers.

### What does the pySMT portfolio feature do?

Portfolio solving runs multiple solvers in parallel, including multiple configurations of the same solver such as MathSAT with different random seeds, and takes the first result. The Portfolio interface also supports push and pop for incremental use.

### What theories does pySMT support?

Linear Real Arithmetic, Real Difference Logic, Equalities and Uninterpreted Functions, Bit-Vectors, Arrays, Strings and their combinations. The typing module is used to declare symbol types, with INT imported from pysmt.typing in the examples.

### What license is pySMT released under?

pySMT is released under the Apache 2.0 license, with the LICENSE and NOTICE files at the root of the repository and license declared as APACHE in the package metadata. The most recent release tag is v0.9.6 and the last push was on 2026-10-06.

## Sources

- [Issues](https://github.com/pysmt/pysmt/issues)
- [License: Apache-2.0](https://github.com/pysmt/pysmt/blob/master/LICENSE)
- [pysmt/pysmt on GitHub](https://github.com/pysmt/pysmt)
- [README](https://github.com/pysmt/pysmt/blob/master/README.md)
- [Releases](https://github.com/pysmt/pysmt/releases)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/pysmt-pysmt