Fetching contributors…
Cannot retrieve contributors at this time
23 lines (20 sloc) 1.78 KB


This directory contains examples to get you started using pySMT. Suggested order:

  1. : First example of the README
  2. : Hello World word puzzle
  3. : Hello World word puzzle using infix-notation
  4. : Combine multiple solvers to solve the same
  5. : Model-Checking an infinite state system (BMC+K-Induction) in ~150 lines
  6. : How to access functionalities of solvers not currently wrapped by pySMT.
  7. : Shows how to use any SMT-LIB complaint SMT solver
  8. : Shows how to combine two different solvers to solve an Exists Forall problem.
  9. : How to detect the logic of a formula and perform model enumeration.
  10. sudoku/ : Solves sudoku problems using a simple encoding using either QF_LIA or QF_BV
  11. : Shows how to use multi-processing to perform parallel and asynchronous solving
  12. : Demonstrates how to perform SMT-LIB parsing, dumping and extension
  13. : Shows the use of UNSAT Core as debugging tools
  14. : Equivalence checking of XOR rewriting using BitVectors
  15. : Quantifier Elimination of an LRA formula
  16. : Combine multiple theories (Array, BitVectors, Integer, and Reals) in the same formula
  17. : Portfolio solving