Welcome to pySMT’s documentation!¶
Introduction¶
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:
Getting Started: Installation and Hello World;
Tutorials: Simple examples showing how to perform common operations using pySMT.
Full API Reference
Table of Contents¶
- Getting Started
- Tutorials
- Boolean Logic in PySMT
- First example
- Hello World word puzzle
- Hello World word puzzle using infix-notation
- Combine multiple solvers
- Model-Checking an infinite state system (BMC+K-Induction) in ~150 lines
- How to access functionalities of solvers not currently wrapped by pySMT
- How to use any SMT-LIB compliant SMT solver
- How to combine two different solvers to solve an Exists Forall problem
- How to detect the logic of a formula and perform model enumeration
- Shows how to use multi-processing to perform parallel and asynchronous solving
- Demonstrates how to perform SMT-LIB parsing, dumping and extension
- Shows the use of UNSAT Core as debugging tools
- Change Log
- 0.9.6: 2022-06-24 – CVC5 and upgraded solvers
- 0.9.5: 2022-05-28 – 2 years of bugfixes
- 0.9.0: 2020-04-26 – PySMT as module
- 0.8.0: 2019-01-27 – Better Install and Great Community
- 0.7.5: 2018-05-29 – Strings and Cython Parser
- 0.7.0: 2017-08-12 – Class Based Walkers and Sorts
- 0.6.1: 2016-12-02 – Portfolio and Coverage
- 0.6.0: 2016-10-09 – GMPY2 and Goodbye Recursion
- 0.5.1: 2016-08-17 – NIRA and Python 3.5
- 0.5.0: 2016-06-09 – Arrays
- 0.4.4: 2016-05-07 – Minor
- 0.4.3: 2015-12-28 – Installers and HR Parsing
- 0.4.2: 2015-10-12 – Boolector
- 0.4.1: 2015-07-13 – BitVectors Extension
- 0.4.0: 2015-06-15 – Interpolation and BDDs
- 0.3.0: 2015-05-01 – BitVectors/UnsatCores
- 0.2.4: 2015-03-15 – PicoSAT
- 0.2.3: 2015-03-12 – Logics Refactoring
- 0.2.2: 2015-02-07 – BDDs
- 0.2.1: 2014-11-29 – SMT-LIB
- 0.2.0: 2014-10-02 – Beta release.
- 0.1.0: 2014-03-10 – Alpha release.
- 0.0.1: 2014-02-01 – Initial release.
- Developing in pySMT
- API Reference