From 63ad6f0ce1f936e7bd041ce984ad1307221cb5e4 Mon Sep 17 00:00:00 2001 From: yoni206 Date: Fri, 20 Aug 2021 02:32:57 +0300 Subject: [PATCH] Add python quick start guide (#7024) --- docs/api/python/python.rst | 3 +- docs/api/python/quickstart.rst | 174 +++++++++++++++++++++++++++++++++ 2 files changed, 176 insertions(+), 1 deletion(-) create mode 100644 docs/api/python/quickstart.rst diff --git a/docs/api/python/python.rst b/docs/api/python/python.rst index c3e425a7f..28443a7d6 100644 --- a/docs/api/python/python.rst +++ b/docs/api/python/python.rst @@ -10,6 +10,7 @@ Python API Documentation This documentation was built while python bindings were disabled. This part of the documentation is likely either empty or outdated. Please enable :code:`BUILD_BINDINGS_PYTHON` in :code:`cmake` and build the documentation again. .. toctree:: - :maxdepth: 2 + :maxdepth: 1 datatype + quickstart diff --git a/docs/api/python/quickstart.rst b/docs/api/python/quickstart.rst new file mode 100644 index 000000000..ac71fa76c --- /dev/null +++ b/docs/api/python/quickstart.rst @@ -0,0 +1,174 @@ +Quickstart Guide +================ + +First, create a cvc5 solver instance: + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 22 + +We will ask the solver to produce models and unsat cores in the following, +and for this we have to enable the following options. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 26-27 + +Next we set the logic. +The simplest way to set a logic for the solver is to choose ``"ALL"``. +This enables all logics in the solver. +Alternatively, ``"QF_ALL"`` enables all logics without quantifiers. +To optimize the solver's behavior for a more specific logic, +use the logic name, e.g. ``"QF_BV"`` or ``"QF_AUFBV"``. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 36 + +In the following, we will define constraints of reals and integers. +For this, we first query the solver for the corresponding sorts. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 40-41 + +Now, we create two constants ``x`` and ``y`` of sort ``Real``, +and two constants ``a`` and ``b`` of sort ``Integer``. +Notice that these are *symbolic* constants, but not actual values. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 46-49 + +We define the following constraints regarding ``x`` and ``y``: + +.. math:: + + (0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq y) + +We construct the required terms and assert them as follows: + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 59-81 + +Now we check if the asserted formula is satisfiable, that is, we check if +there exist values of sort ``Real`` for ``x`` and ``y`` that satisfy all +the constraints. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 85 + +The result we get from this satisfiability check is either ``sat``, ``unsat`` +or ``unknown``. +It's status can be queried via `isSat`, `isUnsat` and `isSatUnknown` functions. +Alternatively, it can also be printed. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 89-90 + +This will print: + +.. code:: text + + expected: sat + result: sat + +Now, we query the solver for the values for ``x`` and ``y`` that satisfy +the constraints. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 93-94 + +It is also possible to get values for terms that do not appear in the original +formula. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 98-99 + +We can retrieve the Python representation of these values as follows. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 102-108 + +This will print the following: + +.. code:: text + + value for x: 1/6 + value for y: 1/6 + value for x - y: 0 + +Another way to independently compute the value of ``x - y`` would be to +use the Python minus operator instead of asking the solver. +However, for more complex terms, it is easier to let the solver do the +evaluation. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 114-118 + +This will print: + +.. code:: text + + computed correctly + +Next, we will check satisfiability of the same formula, +only this time over integer variables ``a`` and ``b``. +For this, we first reset the assertions added to the solver. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 130 + +Next, we assert the same assertions as above, but with integers. +This time, we inline the construction of terms +to the assertion command. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 135-139 + +Now, we check whether the revised assertion is satisfiable. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 142, 145-146 + +This time the asserted formula is unsatisfiable: + +.. code:: text + + expected: unsat + result: unsat + +We can query the solver for an unsatisfiable core, that is, a subset +of the assertions that is already unsatisfiable. + +.. literalinclude:: ../../../examples/api/python/quickstart.py + :language: python + :lines: 150-152 + +This will print: + +.. code:: text + + unsat core size: 3 + unsat core: [(< 0 a), (< 0 b), (< (+ a b) 1)] + +Example +------- + +| The SMT-LIB input for this example can be found at `examples/api/smtlib/quickstart.smt2 `_. +| The source code for this example can be found at `examples/api/python/quickstart.py `_. + +.. api-examples:: + ../../../examples/api/cpp/quickstart.cpp + ../../../examples/api/python/quickstart.py + ../../../examples/api/smtlib/quickstart.smt2 -- 2.30.2