pySMT: A library for SMT formulae manipulation and solving
Branch: master
Clone or download
Type Name Latest commit message Commit time
Failed to load latest commit information.
SMT-LIB SMTLIB Benchmark: Revised Util Aug 20, 2017
ci Boolector: Upgrade to 3.0.1-pre (7f5d32) (#514) Jan 27, 2019
docs Changes: Add note on test failure on Z3 tactics Jan 28, 2019
examples Examples: Strings Jan 27, 2019
pysmt Bump version to 0.8.1dev1 Jan 28, 2019
.coveragerc Coverage: Omit test/ directory Oct 16, 2016
.gitignore sync Jun 22, 2018
.landscape.yaml Small, syntactic refactoring to improve overall code style and landsc… Jun 10, 2015
.travis.yml Passed all linux tests to xenial for uniformity and to avoid problems… Jan 18, 2019
CONTRIBUTING Minor formatting Oct 13, 2016
LICENSE Imported pySMT version 0.2.1 Dec 1, 2014 Updated to create links to executables pysmt, pysmt-shell an… Mar 7, 2015
NOTICE Imported pySMT version 0.2.1 Dec 1, 2014
README.rst README: Fix malformed table Dec 17, 2018
appveyor.yml Install solvers to a relevant site-package by default (#517) Sep 3, 2018
dev-requirements.txt CI: Adding Appveyor configuration May 24, 2015 Imported pySMT version 0.2.1 Dec 1, 2014 Refactored solver installing architecture following #198. Nov 7, 2015 Dist: Updated version of for pypi pkg. Apr 15, 2016 Imported pySMT version 0.2.1 Dec 1, 2014 BV: Enforcing positive values in BV Numbers. Apr 28, 2015 Change version to 0.6.1 Dec 2, 2016 Fixed binaries in pypi distribution (#48) Mar 15, 2015


pySMT: a Python API for SMT

Build Status Coverage Documentation Status Latest PyPI version Apache License Google groups

pySMT makes working with Satisfiability Modulo Theory simple:

  • 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 complaint solver,
  • Dump your problems in the SMT-Lib format,
  • and more...

PySMT Architecture Overview


>>> 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)
>>> g = f.substitute({varB: varA})
>>> g
(A & (! A))
>>> is_sat(g)

A More Complex Example

Is there a value for each letter (between 1 and 9) so that H+E+L+L+O = W+O+R+L+D = 25?

from pysmt.shortcuts import Symbol, And, GE, LT, Plus, Equals, Int, get_model
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(GE(l, Int(1)),
                   LT(l, Int(10))) for l in letters])

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)

print("Serialization of the formula:")

model = get_model(formula)
if model:
  print("No solution found")


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

from pysmt.shortcuts import Portfolio, Symbol, Not

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

with Portfolio(["cvc4",
                ("msat", {"random_seed": 1}),
                ("msat", {"random_seed": 17}),
                ("msat", {"random_seed": 42})],
               generate_models=False) as s:
  res = s.solve()
  v_y = s.get_value(y)
  print(v_y) # TRUE

  res = s.solve()
  v_x = s.get_value(x)
  print(v_x) # FALSE

Using other SMT-LIB Solvers

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 solver name of the SMT-LIB solver can be now used anywhere
# where pySMT would accept an API solver name
with Solver(name=name, logic="QF_UFLRA") as s:
  print(s.is_sat(Symbol("x"))) # True

Check out more examples in the examples/ directory and the documentation on ReadTheDocs

Supported Theories and Solvers

pySMT provides methods to define a formula in Linear Real Arithmetic (LRA), Real Difference Logic (RDL), Equalities and Uninterpreted Functions (EUF), Bit-Vectors (BV), Arrays (A), Strings (S) and their combinations. The following solvers are supported through native APIs:

Additionally, you can use any SMT-LIB 2 compliant solver.

PySMT assumes that the python bindings for the SMT Solver are installed and accessible from your PYTHONPATH.

pySMT works on both Python 3.5 and Python 2.7.


You can install the latest stable release of pySMT from PyPI:

# pip install pysmt

this will additionally install the pysmt-install command, that can be used to install the solvers: e.g.,

$ pysmt-install --check

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. This can be used by pySMT via its native API, or passing through an SMT-LIB file.

The script pysmt-install can be used to simplify the installation of the solvers:

$ pysmt-install --msat

will install MathSAT 5.

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). pysmt-install has many options to customize its behavior.

Note: This script does not install required dependencies for building the solver (e.g., make or gcc) and has been tested mainly on Linux Debian/Ubuntu systems. We suggest that you refer to the documentation of each solver to understand how to install it with its python bindings.

For Yices, picosat, and CUDD, we use external wrappers:

For instruction on how to use any SMT-LIB complaint solver with pySMT see examples/

For more information, refer to online documentation on ReadTheDocs

Solvers Support

The following table summarizes the features supported via pySMT for each of the available solvers.

Solver pySMT name Supported Theories Quantifiers Quantifier Elimination Unsat Core Interpolation
MathSAT msat UF, LIA, LRA, BV, AX No msat-fm, msat-lw Yes Yes
Z3 z3 UF, LIA, LRA, BV, AX, NRA, NIA z3 z3 Yes Yes
CVC4 cvc4 UF, LIA, LRA, BV, AX, S Yes No No No
Yices yices UF, LIA, LRA, BV No No No No
Boolector btor UF, BV, AX No No No No
SMT-Lib Interface <custom> UF, LIA, LRA, BV, AX Yes No No No
PicoSAT picosat [None] No [No] No No
BDD (CUDD) bdd [None] Yes bdd No No


pySMT is released under the APACHE 2.0 License.

For further questions, feel free to open an issue, or write to (Browse the Archive).

If you use pySMT in your work, please consider citing:

  title={PySMT: a solver-agnostic library for fast prototyping of SMT-based algorithms},
  author={Gario, Marco and Micheli, Andrea},
  booktitle={SMT Workshop 2015},