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: :ref:`Installation <getting-started>` and :ref:`Hello World <gs-hello-world>`;
- :doc:`Tutorials <tutorials>`: Simple examples showing how to perform common operations using pySMT.
- Full :ref:`API Reference <api-ref>`
- :ref:`Extending pySMT <development>`
.. toctree:: :maxdepth: 2 getting_started tutorials CHANGES development api_ref