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