This directory contains examples to get you started using pySMT. Suggested order:
- basic.py : First example of the README
- puzzle.py : Hello World word puzzle
- infix_notation.py : Hello World word puzzle using infix-notation
- combine_solvers.py : Combine multiple solvers to solve the same
- model_checking.py : Model-Checking an infinite state system (BMC+K-Induction) in ~150 lines
- allsat.py : How to access functionalities of solvers not currently wrapped by pySMT.
- generic_smtlib.py : Shows how to use any SMT-LIB complaint SMT solver
- efsmt.py : Shows how to combine two different solvers to solve an Exists Forall problem.
- allsmt.py : How to detect the logic of a formula and perform model enumeration.
- sudoku/ : Solves sudoku problems using a simple encoding using either QF_LIA or QF_BV
- parallel.py : Shows how to use multi-processing to perform parallel and asynchronous solving
- smtlib.py : Demonstrates how to perform SMT-LIB parsing, dumping and extension
- einstein.py : Shows the use of UNSAT Core as debugging tools
- xor.py : Equivalence checking of XOR rewriting using BitVectors
- qe.py : Quantifier Elimination of an LRA formula
- theory_combination.py : Combine multiple theories (Array, BitVectors, Integer, and Reals) in the same formula
- portfolio.py : Portfolio solving