First, create a cvc5 :cpp:class:`Solver <cvc5::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".
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``:
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``.
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:
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:
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.
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:
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:
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:
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"``.
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``:
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``.
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:
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.
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:
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:
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:
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"``.
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``:
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``.
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:
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:
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:
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:
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:
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``:
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:
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:
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
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.
``(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``:
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.
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 `(<term> <value>)` one after the other:
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.
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)
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.
// 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:
//
// (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.
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();
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<int64_t, uint64_t> xPair = xVal.getReal64Value();
std::pair<int64_t, uint64_t> yPair = yVal.getReal64Value();
std::pair<int64_t, uint64_t> 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<int64_t, uint64_t> xMinusYComputed = {
xPair.first * yPair.second - xPair.second * yPair.first,
xPair.second * yPair.second
{
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<Term> unsatCore = solver.getUnsatCore();
std::cout << "unsat core size: " << unsatCore.size() << std::endl;
std::cout << "unsat core: " << std::endl;
{
std::cout << t << std::endl;
}
+ //! [docs-cpp-quickstart-18 end]
return 0;
}
{
// 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.
// 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:
//
// (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.
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<BigInteger, BigInteger> xPair = xVal.getRealValue();
Pair<BigInteger, BigInteger> yPair = yVal.getRealValue();
Pair<BigInteger, BigInteger> xMinusYPair = xMinusYVal.getRealValue();
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<BigInteger, BigInteger> xMinusYComputed =
new Pair(xPair.first.multiply(yPair.second).subtract(xPair.second.multiply(yPair.first)),
xPair.second.multiply(yPair.second));
{
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<Term> unsatCore = Arrays.asList(solver.getUnsatCore());
System.out.println("unsat core size: " + unsatCore.size());
System.out.println("unsat core: ");
{
System.out.println(t);
}
+ //! [docs-java-quickstart-15 end]
}
}
-}
\ No newline at end of file
+}
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
# * 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]
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.
# 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:
#
# (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.
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();
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]
+;! [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
(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]
projects / cvc5.git / commitdiff