Skip to content

Latest commit

 

History

History
 
 

examples

Examples

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

  1. basic.py : First example of the README
  2. puzzle.py : Hello World word puzzle
  3. infix_notation.py : Hello World word puzzle using infix-notation
  4. combine_solvers.py : Combine multiple solvers to solve the same
  5. model_checking.py : Model-Checking an infinite state system (BMC+K-Induction) in ~150 lines
  6. allsat.py : How to access functionalities of solvers not currently wrapped by pySMT.
  7. generic_smtlib.py : Shows how to use any SMT-LIB complaint SMT solver
  8. efsmt.py : Shows how to combine two different solvers to solve an Exists Forall problem.
  9. allsmt.py : 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. parallel.py : Shows how to use multi-processing to perform parallel and asynchronous solving
  12. smtlib.py : Demonstrates how to perform SMT-LIB parsing, dumping and extension
  13. einstein.py : Shows the use of UNSAT Core as debugging tools
  14. xor.py : Equivalence checking of XOR rewriting using BitVectors
  15. qe.py : Quantifier Elimination of an LRA formula
  16. theory_combination.py : Combine multiple theories (Array, BitVectors, Integer, and Reals) in the same formula
  17. portfolio.py : Portfolio solving
  18. strings.py : Example on the theory of Strings