1Tutorials 2========= 3 4This page is under-construction. For now, it contains a copy of the 5files within the `examples/ folder 6<https://github.com/pysmt/pysmt/blob/master/examples/README.rst>`_ of 7the pySMT repository and a basic tutorial on Boolean logic. 8 9If you are interested in helping us create better tutorials, please 10let us know at info@pysmt.org . 11 12 13.. contents:: 14 :local: 15 16 17Boolean Logic in PySMT 18---------------------- 19An introductory basic example on how to use pySMT for Booean satisfiability: :ref:`pysmt-tutorials-booleanlogic`. 20 21First example 22------------- 23.. literalinclude:: ../examples/basic.py 24 25Hello World word puzzle 26----------------------- 27.. literalinclude:: ../examples/puzzle.py 28 29Hello World word puzzle using infix-notation 30-------------------------------------------- 31.. literalinclude:: ../examples/infix_notation.py 32 33Combine multiple solvers 34------------------------------------------ 35.. literalinclude:: ../examples/combine_solvers.py 36 37Model-Checking an infinite state system (BMC+K-Induction) in ~150 lines 38----------------------------------------------------------------------- 39.. literalinclude:: ../examples/model_checking.py 40 41How to access functionalities of solvers not currently wrapped by pySMT 42----------------------------------------------------------------------- 43.. literalinclude:: ../examples/allsat.py 44 45How to use any SMT-LIB compliant SMT solver 46-------------------------------------------- 47.. literalinclude:: ../examples/generic_smtlib.py 48 49How to combine two different solvers to solve an Exists Forall problem 50---------------------------------------------------------------------- 51.. literalinclude:: ../examples/efsmt.py 52 53How to detect the logic of a formula and perform model enumeration 54------------------------------------------------------------------ 55.. literalinclude:: ../examples/allsmt.py 56 57Shows how to use multi-processing to perform parallel and asynchronous solving 58------------------------------------------------------------------------------ 59.. literalinclude:: ../examples/parallel.py 60 61Demonstrates how to perform SMT-LIB parsing, dumping and extension 62------------------------------------------------------------------ 63.. literalinclude:: ../examples/smtlib.py 64 65Shows the use of UNSAT Core as debugging tools 66---------------------------------------------- 67.. literalinclude:: ../examples/einstein.py 68