Welcome to pySMT’s documentation!


pySMT makes working with Satisfiability Modulo Theory simple. pySMT provides an intermediate step between the SMT-LIB (that is universal but not programmable) and solvers API (that are programmable, but specific).

Among others, you can:

  • Define formulae in a solver independent way
  • Run the same code using multiple solvers
  • Easily perform quantifier elimination, interpolation and unsat-core extraction
  • Write ad-hoc simplifiers and operators
  • and more…

Please let us know of any problem or possible improvements by opening an issue on github or by writing to pysmt@googlegroups.com .

Where to go from here:

Table of Contents

Indices and tables