skip to navigation
skip to content

pySMT 0.6.1

A solver-agnostic library for SMT Formulae manipulation and solving

pySMT makes working with Satisfiability Modulo Theory simple.

Among others, you can:

  • Define formulae in a solver independent way in a simple and inutitive way,
  • Write ad-hoc simplifiers and operators,
  • Dump your problems in the SMT-Lib format,
  • Solve them using one of the native solvers, or by wrapping any SMT-Lib complaint solver.

Supported Theories and Solvers

pySMT provides methods to define a formula in Linear Real Arithmetic (LRA), Real Difference Logic (RDL), their combination (LIRA), Equalities and Uninterpreted Functions (EUF), Bit-Vectors (BV), and Arrays (A). 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 and Python 2.

Wanna know more?


File Type Py Version Uploaded on Size
PySMT-0.6.1.tar.gz (md5) Source 2016-12-03 200KB