From 9c176f263b977cf3e3b1beaf8fea971b7a159a5d Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Mon, 2 May 2022 13:13:00 -0700 Subject: [PATCH] docs: Do not use explicit line numbers in literalinclude. (#8690) --- docs/api/cpp/quickstart.rst | 108 +++++++++++++------- docs/api/java/quickstart.rst | 105 +++++++++++--------- docs/api/python/base/quickstart.rst | 110 +++++++++++++++------ docs/api/python/pythonic/quickstart.rst | 36 ++++--- docs/binary/quickstart.rst | 52 ++++++---- examples/api/cpp/quickstart.cpp | 45 ++++++++- examples/api/java/QuickStart.java | 32 +++++- examples/api/python/pythonic/quickstart.py | 12 +++ examples/api/python/quickstart.py | 41 +++++++- examples/api/smtlib/quickstart.smt2 | 20 ++++ 10 files changed, 410 insertions(+), 151 deletions(-) diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst index 4a844f0c4..c524c8607 100644 --- a/docs/api/cpp/quickstart.rst +++ b/docs/api/cpp/quickstart.rst @@ -4,15 +4,19 @@ Quickstart Guide First, create a cvc5 :cpp:class:`Solver ` instance: .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 27 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-1 start + :end-before: docs-cpp-quickstart-1 end 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/cpp/quickstart.cpp - :language: cpp - :lines: 31-32 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-2 start + :end-before: docs-cpp-quickstart-2 end Next we set the logic. The simplest way to set a logic for the solver is to choose "ALL". @@ -22,23 +26,29 @@ 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/cpp/quickstart.cpp - :language: cpp - :lines: 41 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-3 start + :end-before: docs-cpp-quickstart-3 end 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/cpp/quickstart.cpp - :language: cpp - :lines: 45-46 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-4 start + :end-before: docs-cpp-quickstart-4 end 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/cpp/quickstart.cpp - :language: cpp - :lines: 51-54 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-5 start + :end-before: docs-cpp-quickstart-5 end We define the following constraints regarding ``x`` and ``y``: @@ -49,16 +59,20 @@ We define the following constraints regarding ``x`` and ``y``: We construct the required terms and assert them as follows: .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 64-88 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-6 start + :end-before: docs-cpp-quickstart-6 end 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/cpp/quickstart.cpp - :language: cpp - :lines: 92 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-7 start + :end-before: docs-cpp-quickstart-7 end The result we get from this satisfiability check is either ``sat``, ``unsat`` or ``unknown``. @@ -69,8 +83,10 @@ It's status can be queried via Alternatively, it can also be printed. .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 96-97 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-8 start + :end-before: docs-cpp-quickstart-8 end This will print: @@ -83,21 +99,27 @@ Now, we query the solver for the values for ``x`` and ``y`` that satisfy the constraints. .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 100-101 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-9 start + :end-before: docs-cpp-quickstart-9 end It is also possible to get values for terms that do not appear in the original formula. .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 105-106 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-10 start + :end-before: docs-cpp-quickstart-10 end We can retrieve the string representation of these values as follows. .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 109-115 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-11 start + :end-before: docs-cpp-quickstart-11 end This will print the following: @@ -110,8 +132,10 @@ This will print the following: We can convert these values to C++ types. .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 117-124 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-12 start + :end-before: docs-cpp-quickstart-12 end Another way to independently compute the value of ``x - y`` would be to perform the (rational) arithmetic manually. @@ -119,8 +143,10 @@ However, for more complex terms, it is easier to let the solver do the evaluation. .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 130-143 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-13 start + :end-before: docs-cpp-quickstart-13 end This will print: @@ -133,22 +159,34 @@ only this time over integer variables ``a`` and ``b``. For this, we first reset the assertions added to the solver. .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 149 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-14 start + :end-before: docs-cpp-quickstart-14 end 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/cpp/quickstart.cpp - :language: cpp - :lines: 154-158 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-15 start + :end-before: docs-cpp-quickstart-15 end Now, we check whether the revised assertion is satisfiable. .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 161, 164-165 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-16 start + :end-before: docs-cpp-quickstart-16 end + +.. literalinclude:: ../../../examples/api/cpp/quickstart.cpp + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-17 start + :end-before: docs-cpp-quickstart-17 end This time the asserted formula is unsatisfiable: @@ -161,8 +199,10 @@ We can query the solver for an unsatisfiable core, that is, a subset of the assertions that is already unsatisfiable. .. literalinclude:: ../../../examples/api/cpp/quickstart.cpp - :language: cpp - :lines: 169-175 + :language: cpp + :dedent: 2 + :start-after: docs-cpp-quickstart-18 start + :end-before: docs-cpp-quickstart-18 end This will print: diff --git a/docs/api/java/quickstart.rst b/docs/api/java/quickstart.rst index 921b1b0bb..8d0be15d7 100644 --- a/docs/api/java/quickstart.rst +++ b/docs/api/java/quickstart.rst @@ -14,9 +14,10 @@ instance using try with resources: To produce models and unsat cores, we have to enable the following options. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 32-33 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-1 start + :end-before: docs-java-quickstart-1 end Next we set the logic. The simplest way to set a logic for the solver is to choose ``"ALL"``. @@ -26,26 +27,29 @@ 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/java/QuickStart.java - :language: java - :lines: 42 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-2 start + :end-before: docs-java-quickstart-2 end In the following, we will define real and integer constraints. For this, we first query the solver for the corresponding sorts. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 46-47 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-3 start + :end-before: docs-java-quickstart-3 end 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, not actual values. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 52-55 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-4 start + :end-before: docs-java-quickstart-4 end We define the following constraints regarding ``x`` and ``y``: @@ -56,18 +60,20 @@ We define the following constraints regarding ``x`` and ``y``: We construct the required terms and assert them as follows: .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 65-89 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-5 start + :end-before: docs-java-quickstart-5 end 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/java/QuickStart.java - :language: java - :lines: 93 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-6 start + :end-before: docs-java-quickstart-6 end The result we get from this satisfiability check is either ``sat``, ``unsat`` or ``unknown``. @@ -78,9 +84,10 @@ It's status can be queried via Alternatively, it can also be printed. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 97-98 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-7 start + :end-before: docs-java-quickstart-7 end This will print: @@ -93,24 +100,27 @@ Now, we query the solver for the values for ``x`` and ``y`` that satisfy the constraints. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 101-102 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-8 start + :end-before: docs-java-quickstart-8 end It is also possible to get values for terms that do not appear in the original formula. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 106-107 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-9 start + :end-before: docs-java-quickstart-9 end We can convert these values to Java types. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 109-116 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-10 start + :end-before: docs-java-quickstart-10 end Another way to independently compute the value of ``x - y`` would be to perform the (rational) arithmetic manually. @@ -118,9 +128,10 @@ However, for more complex terms, it is easier to let the solver do the evaluation. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 122-134 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-11 start + :end-before: docs-java-quickstart-11 end This will print: @@ -133,25 +144,28 @@ only this time over integer variables ``a`` and ``b``. For this, we first reset the assertions added to the solver. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 140 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-12 start + :end-before: docs-java-quickstart-12 end Next, we assert the same assertions as above, but with integers. This time, we inline the construction of terms in the assertion command. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 145-149 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-13 start + :end-before: docs-java-quickstart-13 end Now, we check whether the revised assertion is satisfiable. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 152-156 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-14 start + :end-before: docs-java-quickstart-14 end This time the asserted formula is unsatisfiable: @@ -164,9 +178,10 @@ We can query the solver for an unsatisfiable core, that is, a subset of the assertions that is already unsatisfiable. .. literalinclude:: ../../../examples/api/java/QuickStart.java - :language: java - :lines: 160-166 - :dedent: 6 + :language: java + :dedent: 6 + :start-after: docs-java-quickstart-15 start + :end-before: docs-java-quickstart-15 end This will print: diff --git a/docs/api/python/base/quickstart.rst b/docs/api/python/base/quickstart.rst index 53b674b03..ffa5f3df5 100644 --- a/docs/api/python/base/quickstart.rst +++ b/docs/api/python/base/quickstart.rst @@ -4,15 +4,19 @@ Quickstart Guide First, create a cvc5 solver instance: .. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 22 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-1 start + :end-before: docs-python-quickstart-1 end 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 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-2 start + :end-before: docs-python-quickstart-2 end Next we set the logic. The simplest way to set a logic for the solver is to choose ``"ALL"``. @@ -22,23 +26,29 @@ 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 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-3 start + :end-before: docs-python-quickstart-3 end 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 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-4 start + :end-before: docs-python-quickstart-4 end 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 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-5 start + :end-before: docs-python-quickstart-5 end We define the following constraints regarding ``x`` and ``y``: @@ -49,16 +59,20 @@ We define the following constraints regarding ``x`` and ``y``: We construct the required terms and assert them as follows: .. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 59-81 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-6 start + :end-before: docs-python-quickstart-6 end 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 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-7 start + :end-before: docs-python-quickstart-7 end The result we get from this satisfiability check is either ``sat``, ``unsat`` or ``unknown``. @@ -66,8 +80,10 @@ 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 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-8 start + :end-before: docs-python-quickstart-8 end This will print: @@ -80,21 +96,27 @@ 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 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-9 start + :end-before: docs-python-quickstart-9 end 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 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-10 start + :end-before: docs-python-quickstart-10 end We can retrieve the Python representation of these values as follows. .. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 102-108 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-11 start + :end-before: docs-python-quickstart-11 end This will print the following: @@ -110,8 +132,10 @@ 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 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-12 start + :end-before: docs-python-quickstart-12 end This will print: @@ -119,27 +143,47 @@ This will print: computed correctly +Further, we can convert these values to strings: + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-13 start + :end-before: docs-python-quickstart-13 end + 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 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-14 start + :end-before: docs-python-quickstart-14 end 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-140 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-15 start + :end-before: docs-python-quickstart-15 end Now, we check whether the revised assertion is satisfiable. .. literalinclude:: ../../../../examples/api/python/quickstart.py - :language: python - :lines: 143, 146-147 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-16 start + :end-before: docs-python-quickstart-16 end + +.. literalinclude:: ../../../../examples/api/python/quickstart.py + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-17 start + :end-before: docs-python-quickstart-17 end This time the asserted formula is unsatisfiable: @@ -152,8 +196,10 @@ 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: 151-153 + :language: python + :dedent: 2 + :start-after: docs-python-quickstart-18 start + :end-before: docs-python-quickstart-18 end This will print: diff --git a/docs/api/python/pythonic/quickstart.rst b/docs/api/python/pythonic/quickstart.rst index 53a48d5f8..ac72f31e5 100644 --- a/docs/api/python/pythonic/quickstart.rst +++ b/docs/api/python/pythonic/quickstart.rst @@ -6,8 +6,10 @@ and two constants ``a`` and ``b`` of sort ``Integer``. Notice that these are *symbolic* constants, but not actual values. .. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py - :language: python - :lines: 6-7 + :language: python + :dedent: 4 + :start-after: docs-pythonic-quickstart-1 start + :end-before: docs-pythonic-quickstart-1 end We define the following constraints regarding ``x`` and ``y``: @@ -18,8 +20,10 @@ We define the following constraints regarding ``x`` and ``y``: We check whether there is a solution to these constraints: .. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py - :language: python - :lines: 15 + :language: python + :dedent: 4 + :start-after: docs-pythonic-quickstart-2 start + :end-before: docs-pythonic-quickstart-2 end In this case, there is, so we get output: @@ -30,14 +34,18 @@ In this case, there is, so we get output: We can also get an explicit model (assignment) for the constraints. .. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py - :language: python - :lines: 19-22 + :language: python + :dedent: 4 + :start-after: docs-pythonic-quickstart-3 start + :end-before: docs-pythonic-quickstart-3 end With the model, we can evaluate variables and terms: .. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py - :language: python - :lines: 24-26 + :language: python + :dedent: 4 + :start-after: docs-pythonic-quickstart-4 start + :end-before: docs-pythonic-quickstart-4 end This will print: @@ -51,16 +59,20 @@ This will print: We can also get these values in other forms: .. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py - :language: python - :lines: 29-32 + :language: python + :dedent: 4 + :start-after: docs-pythonic-quickstart-5 start + :end-before: docs-pythonic-quickstart-5 end Next, we assert the same assertions as above, but with integers. This time, there is no solution, so "no solution" is printed. .. literalinclude:: ../../../../examples/api/python/pythonic/quickstart.py - :language: python - :lines: 36 + :language: python + :dedent: 4 + :start-after: docs-pythonic-quickstart-6 start + :end-before: docs-pythonic-quickstart-6 end Example diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst index efddd001b..83338b635 100644 --- a/docs/binary/quickstart.rst +++ b/docs/binary/quickstart.rst @@ -14,8 +14,9 @@ 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/smtlib/quickstart.smt2 - :language: smtlib - :lines: 1 + :language: smtlib + :start-after: docs-smt2-quickstart-1 start + :end-before: docs-smt2-quickstart-1 end We will ask the solver to produce models and unsat cores in the following, and for this we have to enable the following options. @@ -23,15 +24,17 @@ Furthermore, we enable incremental solving so that we can use the ``(reset-assertions)`` command later on. .. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 - :language: smtlib - :lines: 2-6 + :language: smtlib + :start-after: docs-smt2-quickstart-2 start + :end-before: docs-smt2-quickstart-2 end Now, we create two constants ``x`` and ``y`` of sort ``Real``. Notice that these are *symbolic* constants, but not actual values. .. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 - :language: smtlib - :lines: 8-10 + :language: smtlib + :start-after: docs-smt2-quickstart-3 start + :end-before: docs-smt2-quickstart-3 end We define the following constraints regarding ``x`` and ``y``: @@ -42,16 +45,18 @@ We define the following constraints regarding ``x`` and ``y``: We assert them as follows. Notice that in SMT-LIB v2, terms are written in prefix notation, e.g., we write `(+ x y)` instead of `(x + y)`. .. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 - :language: smtlib - :lines: 12-22 + :language: smtlib + :start-after: docs-smt2-quickstart-4 start + :end-before: docs-smt2-quickstart-4 end 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/smtlib/quickstart.smt2 - :language: smtlib - :lines: 24 + :language: smtlib + :start-after: docs-smt2-quickstart-5 start + :end-before: docs-smt2-quickstart-5 end The result we get from this satisfiability check is either ``sat``, ``unsat`` or ``unknown``, and it is printed to standard output. @@ -63,8 +68,9 @@ It is also possible to get values for terms that do not appear in the original formula. .. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 - :language: smtlib - :lines: 25-26 + :language: smtlib + :start-after: docs-smt2-quickstart-6 start + :end-before: docs-smt2-quickstart-6 end This will print the values of `x`, `y`, and `x-y`, in a key-value format `( )` one after the other: @@ -78,20 +84,23 @@ For this, we first reset the assertions added to the solver and declare fresh integer variables ``a`` and ``b``. .. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 - :language: smtlib - :lines: 28-32 + :language: smtlib + :start-after: docs-smt2-quickstart-7 start + :end-before: docs-smt2-quickstart-7 end Next, we assert the same assertions as above, but with integers. .. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 - :language: smtlib - :lines: 33-36 + :language: smtlib + :start-after: docs-smt2-quickstart-8 start + :end-before: docs-smt2-quickstart-8 end Now, we check whether the revised query is satisfiable. .. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 - :language: smtlib - :lines: 38 + :language: smtlib + :start-after: docs-smt2-quickstart-9 start + :end-before: docs-smt2-quickstart-9 end This time the asserted formula is unsatisfiable and ``unsat`` is printed. @@ -99,13 +108,14 @@ We can query the solver for an unsatisfiable core, that is, a subset of the assertions that is already unsatisfiable. .. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 - :language: smtlib - :lines: 39 + :language: smtlib + :start-after: docs-smt2-quickstart-10 start + :end-before: docs-smt2-quickstart-10 end This will print: .. code:: text - + ( (< 0 a) (< 0 b) diff --git a/examples/api/cpp/quickstart.cpp b/examples/api/cpp/quickstart.cpp index f79da4580..9a8bb1abe 100644 --- a/examples/api/cpp/quickstart.cpp +++ b/examples/api/cpp/quickstart.cpp @@ -24,12 +24,16 @@ using namespace cvc5; int main() { // Create a solver + //! [docs-cpp-quickstart-1 start] Solver solver; + //! [docs-cpp-quickstart-1 end] // We will ask the solver to produce models and unsat cores, // hence these options should be turned on. + //! [docs-cpp-quickstart-2 start] solver.setOption("produce-models", "true"); solver.setOption("produce-unsat-cores", "true"); + //! [docs-cpp-quickstart-2 end] // The simplest way to set a logic for the solver is to choose "ALL". // This enables all logics in the solver. @@ -38,20 +42,26 @@ int main() // use the logic name, e.g. "QF_BV" or "QF_AUFBV". // Set the logic + //! [docs-cpp-quickstart-3 start] solver.setLogic("ALL"); + //! [docs-cpp-quickstart-3 end] // In this example, we will define constraints over reals and integers. // Hence, we first obtain the corresponding sorts. + //! [docs-cpp-quickstart-4 start] Sort realSort = solver.getRealSort(); Sort intSort = solver.getIntegerSort(); + //! [docs-cpp-quickstart-4 end] // x and y will be real variables, while a and b will be integer variables. // Formally, their cpp type is Term, // and they are called "constants" in SMT jargon: + //! [docs-cpp-quickstart-5 start] Term x = solver.mkConst(realSort, "x"); Term y = solver.mkConst(realSort, "y"); Term a = solver.mkConst(intSort, "a"); Term b = solver.mkConst(intSort, "b"); + //! [docs-cpp-quickstart-5 end] // Our constraints regarding x and y will be: // @@ -61,6 +71,7 @@ int main() // (4) x <= y // + //! [docs-cpp-quickstart-6 start] // Formally, constraints are also terms. Their sort is Boolean. // We will construct these constraints gradually, // by defining each of their components. @@ -86,26 +97,36 @@ int main() solver.assertFormula(constraint2); solver.assertFormula(constraint3); solver.assertFormula(constraint4); + //! [docs-cpp-quickstart-6 end] // Check if the formula is satisfiable, that is, // are there real values for x and y that satisfy all the constraints? + //! [docs-cpp-quickstart-7 start] Result r1 = solver.checkSat(); + //! [docs-cpp-quickstart-7 end] // The result is either SAT, UNSAT, or UNKNOWN. // In this case, it is SAT. + //! [docs-cpp-quickstart-8 start] std::cout << "expected: sat" << std::endl; std::cout << "result: " << r1 << std::endl; + //! [docs-cpp-quickstart-8 end] // We can get the values for x and y that satisfy the constraints. + //! [docs-cpp-quickstart-9 start] Term xVal = solver.getValue(x); Term yVal = solver.getValue(y); + //! [docs-cpp-quickstart-9 end] // It is also possible to get values for compound terms, // even if those did not appear in the original formula. + //! [docs-cpp-quickstart-10 start] Term xMinusY = solver.mkTerm(SUB, {x, y}); Term xMinusYVal = solver.getValue(xMinusY); + //! [docs-cpp-quickstart-10 end] // We can now obtain the string representations of the values. + //! [docs-cpp-quickstart-11 start] std::string xStr = xVal.getRealValue(); std::string yStr = yVal.getRealValue(); std::string xMinusYStr = xMinusYVal.getRealValue(); @@ -113,20 +134,27 @@ int main() std::cout << "value for x: " << xStr << std::endl; std::cout << "value for y: " << yStr << std::endl; std::cout << "value for x - y: " << xMinusYStr << std::endl; + //! [docs-cpp-quickstart-11 end] + //! [docs-cpp-quickstart-12 start] // Further, we can convert the values to cpp types std::pair xPair = xVal.getReal64Value(); std::pair yPair = yVal.getReal64Value(); std::pair xMinusYPair = xMinusYVal.getReal64Value(); - std::cout << "value for x: " << xPair.first << "/" << xPair.second << std::endl; - std::cout << "value for y: " << yPair.first << "/" << yPair.second << std::endl; - std::cout << "value for x - y: " << xMinusYPair.first << "/" << xMinusYPair.second << std::endl; + std::cout << "value for x: " << xPair.first << "/" << xPair.second + << std::endl; + std::cout << "value for y: " << yPair.first << "/" << yPair.second + << std::endl; + std::cout << "value for x - y: " << xMinusYPair.first << "/" + << xMinusYPair.second << std::endl; + //! [docs-cpp-quickstart-12 end] // Another way to independently compute the value of x - y would be // to perform the (rational) arithmetic manually. // However, for more complex terms, // it is easier to let the solver do the evaluation. + //! [docs-cpp-quickstart-13 start] std::pair xMinusYComputed = { xPair.first * yPair.second - xPair.second * yPair.first, xPair.second * yPair.second @@ -141,31 +169,41 @@ int main() { std::cout << "computed incorrectly" << std::endl; } + //! [docs-cpp-quickstart-13 end] // Next, we will check satisfiability of the same formula, // only this time over integer variables a and b. // We start by resetting assertions added to the solver. + //! [docs-cpp-quickstart-14 start] solver.resetAssertions(); + //! [docs-cpp-quickstart-14 end] // Next, we assert the same assertions above with integers. // This time, we inline the construction of terms // to the assertion command. + //! [docs-cpp-quickstart-15 start] solver.assertFormula(solver.mkTerm(LT, {solver.mkInteger(0), a})); solver.assertFormula(solver.mkTerm(LT, {solver.mkInteger(0), b})); solver.assertFormula( solver.mkTerm(LT, {solver.mkTerm(ADD, {a, b}), solver.mkInteger(1)})); solver.assertFormula(solver.mkTerm(LEQ, {a, b})); + //! [docs-cpp-quickstart-15 end] // We check whether the revised assertion is satisfiable. + //! [docs-cpp-quickstart-16 start] Result r2 = solver.checkSat(); + //! [docs-cpp-quickstart-16 end] // This time the formula is unsatisfiable + //! [docs-cpp-quickstart-17 start] std::cout << "expected: unsat" << std::endl; std::cout << "result: " << r2 << std::endl; + //! [docs-cpp-quickstart-17 end] // We can query the solver for an unsatisfiable core, i.e., a subset // of the assertions that is already unsatisfiable. + //! [docs-cpp-quickstart-18 start] std::vector unsatCore = solver.getUnsatCore(); std::cout << "unsat core size: " << unsatCore.size() << std::endl; std::cout << "unsat core: " << std::endl; @@ -173,6 +211,7 @@ int main() { std::cout << t << std::endl; } + //! [docs-cpp-quickstart-18 end] return 0; } diff --git a/examples/api/java/QuickStart.java b/examples/api/java/QuickStart.java index 0dd87cac2..b3324e156 100644 --- a/examples/api/java/QuickStart.java +++ b/examples/api/java/QuickStart.java @@ -29,8 +29,10 @@ public class QuickStart { // We will ask the solver to produce models and unsat cores, // hence these options should be turned on. + //! [docs-java-quickstart-1 start] solver.setOption("produce-models", "true"); solver.setOption("produce-unsat-cores", "true"); + //! [docs-java-quickstart-1 end] // The simplest way to set a logic for the solver is to choose "ALL". // This enables all logics in the solver. @@ -39,20 +41,26 @@ public class QuickStart // use the logic name, e.g. "QF_BV" or "QF_AUFBV". // Set the logic + //! [docs-java-quickstart-2 start] solver.setLogic("ALL"); + //! [docs-java-quickstart-2 end] // In this example, we will define constraints over reals and integers. // Hence, we first obtain the corresponding sorts. + //! [docs-java-quickstart-3 start] Sort realSort = solver.getRealSort(); Sort intSort = solver.getIntegerSort(); + //! [docs-java-quickstart-3 end] // x and y will be real variables, while a and b will be integer variables. // Formally, their cpp type is Term, // and they are called "constants" in SMT jargon: + //! [docs-java-quickstart-4 start] Term x = solver.mkConst(realSort, "x"); Term y = solver.mkConst(realSort, "y"); Term a = solver.mkConst(intSort, "a"); Term b = solver.mkConst(intSort, "b"); + //! [docs-java-quickstart-4 end] // Our constraints regarding x and y will be: // @@ -62,6 +70,7 @@ public class QuickStart // (4) x <= y // + //! [docs-java-quickstart-5 start] // Formally, constraints are also terms. Their sort is Boolean. // We will construct these constraints gradually, // by defining each of their components. @@ -87,26 +96,36 @@ public class QuickStart solver.assertFormula(constraint2); solver.assertFormula(constraint3); solver.assertFormula(constraint4); + //! [docs-java-quickstart-5 end] // Check if the formula is satisfiable, that is, // are there real values for x and y that satisfy all the constraints? + //! [docs-java-quickstart-6 start] Result r1 = solver.checkSat(); + //! [docs-java-quickstart-6 end] // The result is either SAT, UNSAT, or UNKNOWN. // In this case, it is SAT. + //! [docs-java-quickstart-7 start] System.out.println("expected: sat"); System.out.println("result: " + r1); + //! [docs-java-quickstart-7 end] // We can get the values for x and y that satisfy the constraints. + //! [docs-java-quickstart-8 start] Term xVal = solver.getValue(x); Term yVal = solver.getValue(y); + //! [docs-java-quickstart-8 end] // It is also possible to get values for compound terms, // even if those did not appear in the original formula. + //! [docs-java-quickstart-9 start] Term xMinusY = solver.mkTerm(Kind.SUB, x, y); Term xMinusYVal = solver.getValue(xMinusY); + //! [docs-java-quickstart-9 end] // Further, we can convert the values to java types + //! [docs-java-quickstart-10 start] Pair xPair = xVal.getRealValue(); Pair yPair = yVal.getRealValue(); Pair xMinusYPair = xMinusYVal.getRealValue(); @@ -114,11 +133,13 @@ public class QuickStart System.out.println("value for x: " + xPair.first + "/" + xPair.second); System.out.println("value for y: " + yPair.first + "/" + yPair.second); System.out.println("value for x - y: " + xMinusYPair.first + "/" + xMinusYPair.second); + //! [docs-java-quickstart-10 end] // Another way to independently compute the value of x - y would be // to perform the (rational) arithmetic manually. // However, for more complex terms, // it is easier to let the solver do the evaluation. + //! [docs-java-quickstart-11 start] Pair xMinusYComputed = new Pair(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)), xPair.second.multiply(yPair.second)); @@ -132,31 +153,39 @@ public class QuickStart { System.out.println("computed incorrectly"); } + //! [docs-java-quickstart-11 end] // Next, we will check satisfiability of the same formula, // only this time over integer variables a and b. // We start by resetting assertions added to the solver. + //! [docs-java-quickstart-12 start] solver.resetAssertions(); + //! [docs-java-quickstart-12 end] // Next, we assert the same assertions above with integers. // This time, we inline the construction of terms // to the assertion command. + //! [docs-java-quickstart-13 start] solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a)); solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b)); solver.assertFormula( solver.mkTerm(Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1))); solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b)); + //! [docs-java-quickstart-13 end] // We check whether the revised assertion is satisfiable. + //! [docs-java-quickstart-14 start] Result r2 = solver.checkSat(); // This time the formula is unsatisfiable System.out.println("expected: unsat"); System.out.println("result: " + r2); + //! [docs-java-quickstart-14 end] // We can query the solver for an unsatisfiable core, i.e., a subset // of the assertions that is already unsatisfiable. + //! [docs-java-quickstart-15 start] List unsatCore = Arrays.asList(solver.getUnsatCore()); System.out.println("unsat core size: " + unsatCore.size()); System.out.println("unsat core: "); @@ -164,6 +193,7 @@ public class QuickStart { System.out.println(t); } + //! [docs-java-quickstart-15 end] } } -} \ No newline at end of file +} diff --git a/examples/api/python/pythonic/quickstart.py b/examples/api/python/pythonic/quickstart.py index 570c9422a..80b954874 100644 --- a/examples/api/python/pythonic/quickstart.py +++ b/examples/api/python/pythonic/quickstart.py @@ -3,8 +3,10 @@ from cvc5.pythonic import * if __name__ == '__main__': # Let's introduce some variables + #! [docs-pythonic-quickstart-1 start] x, y = Reals('x y') a, b = Ints('a b') + #! [docs-pythonic-quickstart-1 end] # We will confirm that # * 0 < x @@ -12,28 +14,38 @@ if __name__ == '__main__': # * x + y < 1 # * x <= y # are satisfiable + #! [docs-pythonic-quickstart-2 start] solve(0 < x, 0 < y, x + y < 1, x <= y) + #! [docs-pythonic-quickstart-2 end] # If we get the model (the satisfying assignment) explicitly, we can # evaluate terms under it. + #! [docs-pythonic-quickstart-3 start] s = Solver() s.add(0 < x, 0 < y, x + y < 1, x <= y) assert sat == s.check() m = s.model() + #! [docs-pythonic-quickstart-3 end] + #! [docs-pythonic-quickstart-4 start] print('x:', m[x]) print('y:', m[y]) print('x - y:', m[x - y]) + #! [docs-pythonic-quickstart-4 end] # We can also get these values in other forms: + #! [docs-pythonic-quickstart-5 start] print('string x:', str(m[x])) print('decimal x:', m[x].as_decimal(4)) print('fraction x:', m[x].as_fraction()) print('float x:', float(m[x].as_fraction())) + #! [docs-pythonic-quickstart-5 end] # The above constraints are *UNSAT* for integer variables. # This reports "no solution" + #! [docs-pythonic-quickstart-6 start] solve(0 < a, 0 < b, a + b < 1, a <= b) + #! [docs-pythonic-quickstart-6 end] diff --git a/examples/api/python/quickstart.py b/examples/api/python/quickstart.py index 52c172b5a..c2308226f 100644 --- a/examples/api/python/quickstart.py +++ b/examples/api/python/quickstart.py @@ -19,12 +19,16 @@ from cvc5 import Kind if __name__ == "__main__": # Create a solver + #! [docs-python-quickstart-1 start] solver = cvc5.Solver() + #! [docs-python-quickstart-1 end] # We will ask the solver to produce models and unsat cores, # hence these options should be turned on. + #! [docs-python-quickstart-2 start] solver.setOption("produce-models", "true"); solver.setOption("produce-unsat-cores", "true"); + #! [docs-python-quickstart-2 end] # The simplest way to set a logic for the solver is to choose "ALL". # This enables all logics in the solver. @@ -33,20 +37,26 @@ if __name__ == "__main__": # use the logic name, e.g. "QF_BV" or "QF_AUFBV". # Set the logic + #! [docs-python-quickstart-3 start] solver.setLogic("ALL"); + #! [docs-python-quickstart-3 end] # In this example, we will define constraints over reals and integers. # Hence, we first obtain the corresponding sorts. + #! [docs-python-quickstart-4 start] realSort = solver.getRealSort(); intSort = solver.getIntegerSort(); + #! [docs-python-quickstart-4 end] # x and y will be real variables, while a and b will be integer variables. # Formally, their python type is Term, # and they are called "constants" in SMT jargon: + #! [docs-python-quickstart-5 start] x = solver.mkConst(realSort, "x"); y = solver.mkConst(realSort, "y"); a = solver.mkConst(intSort, "a"); b = solver.mkConst(intSort, "b"); + #! [docs-python-quickstart-5 end] # Our constraints regarding x and y will be: # @@ -56,6 +66,7 @@ if __name__ == "__main__": # (4) x <= y # + #! [docs-python-quickstart-6 start] # Formally, constraints are also terms. Their sort is Boolean. # We will construct these constraints gradually, # by defining each of their components. @@ -79,26 +90,36 @@ if __name__ == "__main__": solver.assertFormula(constraint2); solver.assertFormula(constraint3); solver.assertFormula(constraint4); + #! [docs-python-quickstart-6 end] # Check if the formula is satisfiable, that is, # are there real values for x and y that satisfy all the constraints? + #! [docs-python-quickstart-7 start] r1 = solver.checkSat(); + #! [docs-python-quickstart-7 end] # The result is either SAT, UNSAT, or UNKNOWN. # In this case, it is SAT. + #! [docs-python-quickstart-8 start] print("expected: sat") print("result: ", r1) + #! [docs-python-quickstart-8 end] # We can get the values for x and y that satisfy the constraints. + #! [docs-python-quickstart-9 start] xVal = solver.getValue(x); yVal = solver.getValue(y); + #! [docs-python-quickstart-9 end] # It is also possible to get values for compound terms, # even if those did not appear in the original formula. + #! [docs-python-quickstart-10 start] xMinusY = solver.mkTerm(Kind.SUB, x, y); xMinusYVal = solver.getValue(xMinusY); - + #! [docs-python-quickstart-10 end] + # We can now obtain the values as python values + #! [docs-python-quickstart-11 start] xPy = xVal.getRealValue(); yPy = yVal.getRealValue(); xMinusYPy = xMinusYVal.getRealValue(); @@ -106,48 +127,62 @@ if __name__ == "__main__": print("value for x: ", xPy) print("value for y: ", yPy) print("value for x - y: ", xMinusYPy) + #! [docs-python-quickstart-11 end] # 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. + #! [docs-python-quickstart-12 start] xMinusYComputed = xPy - yPy; if xMinusYComputed == xMinusYPy: - print("computed correctly") + print("computed correctly") else: print("computed incorrectly") + #! [docs-python-quickstart-12 end] # Further, we can convert the values to strings + #! [docs-python-quickstart-13 start] xStr = str(xPy); yStr = str(yPy); xMinusYStr = str(xMinusYPy); - + #! [docs-python-quickstart-13 end] # Next, we will check satisfiability of the same formula, # only this time over integer variables a and b. # We start by resetting assertions added to the solver. + #! [docs-python-quickstart-14 start] solver.resetAssertions(); + #! [docs-python-quickstart-14 end] # Next, we assert the same assertions above with integers. # This time, we inline the construction of terms # to the assertion command. + #! [docs-python-quickstart-15 start] solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a)); solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b)); solver.assertFormula( solver.mkTerm( Kind.LT, solver.mkTerm(Kind.ADD, a, b), solver.mkInteger(1))); solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b)); + #! [docs-python-quickstart-15 end] # We check whether the revised assertion is satisfiable. + #! [docs-python-quickstart-16 start] r2 = solver.checkSat(); + #! [docs-python-quickstart-16 end] # This time the formula is unsatisfiable + #! [docs-python-quickstart-17 start] print("expected: unsat") print("result:", r2) + #! [docs-python-quickstart-17 end] # We can query the solver for an unsatisfiable core, i.e., a subset # of the assertions that is already unsatisfiable. + #! [docs-python-quickstart-18 start] unsatCore = solver.getUnsatCore(); print("unsat core size:", len(unsatCore)) print("unsat core:", unsatCore) + #! [docs-python-quickstart-18 end] diff --git a/examples/api/smtlib/quickstart.smt2 b/examples/api/smtlib/quickstart.smt2 index b5dc87d2b..28cea8a9d 100644 --- a/examples/api/smtlib/quickstart.smt2 +++ b/examples/api/smtlib/quickstart.smt2 @@ -1,14 +1,21 @@ +;! [docs-smt2-quickstart-1 start] (set-logic ALL) +;! [docs-smt2-quickstart-1 end] +;! [docs-smt2-quickstart-2 start] (set-option :produce-models true) (set-option :incremental true) ; print unsat cores, include assertions in the unsat core that have not been named (set-option :produce-unsat-cores true) (set-option :dump-unsat-cores-full true) +;! [docs-smt2-quickstart-2 end] +;! [docs-smt2-quickstart-3 start] ; Declare real constants x,y (declare-const x Real) (declare-const y Real) +;! [docs-smt2-quickstart-3 end] +;! [docs-smt2-quickstart-4 start] ; Our constraints regarding x and y will be: ; ; (1) 0 < x @@ -20,20 +27,33 @@ (assert (< 0 y)) (assert (< (+ x y) 1)) (assert (<= x y)) +;! [docs-smt2-quickstart-4 end] +;! [docs-smt2-quickstart-5 start] (check-sat) +;! [docs-smt2-quickstart-5 end] +;! [docs-smt2-quickstart-6 start] (echo "Values of declared real constants and of compound terms built with them.") (get-value (x y (- x y))) +;! [docs-smt2-quickstart-6 end] +;! [docs-smt2-quickstart-7 start] (echo "We will reset the solver with the (reset-assertions) command and check satisfiability of the same assertions but with the integers constants rather than with the real ones.") (reset-assertions) ; Declare integer constants a,b (declare-const a Int) (declare-const b Int) +;! [docs-smt2-quickstart-7 end] +;! [docs-smt2-quickstart-8 start] (assert (< 0 a)) (assert (< 0 b)) (assert (< (+ a b) 1)) (assert (<= a b)) +;! [docs-smt2-quickstart-8 end] +;! [docs-smt2-quickstart-9 start] (check-sat) +;! [docs-smt2-quickstart-9 end] +;! [docs-smt2-quickstart-10 start] (get-unsat-core) +;! [docs-smt2-quickstart-10 end] -- 2.30.2