From 78a3406dbd7495daea1c85d92129f738302dc700 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Wed, 23 Jun 2021 12:08:21 -0700 Subject: [PATCH] docs: Add quickstart guide. (#6782) --- docs/api/cpp/cpp.rst | 3 +- docs/api/cpp/quickstart.rst | 185 ++++++++++++++++++++++++++++ docs/ext/smtliblexer.py | 5 + examples/api/cpp/quickstart.cpp | 10 +- examples/api/smtlib/quickstart.smt2 | 21 ++++ 5 files changed, 218 insertions(+), 6 deletions(-) create mode 100644 docs/api/cpp/quickstart.rst create mode 100644 examples/api/smtlib/quickstart.smt2 diff --git a/docs/api/cpp/cpp.rst b/docs/api/cpp/cpp.rst index 17e121a2c..91e9f4619 100644 --- a/docs/api/cpp/cpp.rst +++ b/docs/api/cpp/cpp.rst @@ -4,8 +4,9 @@ C++ API Documentation ===================== .. toctree:: - :maxdepth: 2 + :maxdepth: 1 + quickstart class_hierarchy .. container:: hide-toctree diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst new file mode 100644 index 000000000..08d25b205 --- /dev/null +++ b/docs/api/cpp/quickstart.rst @@ -0,0 +1,185 @@ +Quickstart Guide +================ + +First, create a cvc5 :cpp:class:`Solver ` instance: + +.. literalinclude:: ../../../examples/api/cpp/quickstart.cpp + :language: cpp + :lines: 27 + +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 + +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/cpp/quickstart.cpp + :language: cpp + :lines: 41 + +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 + +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 + +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/cpp/quickstart.cpp + :language: cpp + :lines: 64-88 + +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 + +The result we get from this satisfiability check is either ``sat``, ``unsat`` +or ``unknown``. +It's status can be queried via +:cpp:func:`cvc5::api::Result::isSat`, +:cpp:func:`cvc5::api::Result::isUnsat` and +:cpp:func:`cvc5::api::Result::isSatUnknown`. +Alternatively, it can also be printed. + +.. literalinclude:: ../../../examples/api/cpp/quickstart.cpp + :language: cpp + :lines: 96-97 + +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/cpp/quickstart.cpp + :language: cpp + :lines: 100-101 + +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 + +We can retrieve the string representation of these values as follows. + +.. literalinclude:: ../../../examples/api/cpp/quickstart.cpp + :language: cpp + :lines: 109-115 + +This will print the following: + +.. code:: text + + value for x: 1/6 + value for y: 1/6 + value for x - y: 0 + +We can convert these values to C++ types using standard conversion functions. + +.. literalinclude:: ../../../examples/api/cpp/quickstart.cpp + :language: cpp + :lines: 119-121 + +Another way to independently compute the value of ``x - y`` would be to +use the C++ 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/cpp/quickstart.cpp + :language: cpp + :lines: 127-135 + +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/cpp/quickstart.cpp + :language: cpp + :lines: 141 + +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: 146-150 + +Now, we check whether the revised assertion is satisfiable. + +.. literalinclude:: ../../../examples/api/cpp/quickstart.cpp + :language: cpp + :lines: 153, 156-157 + +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/cpp/quickstart.cpp + :language: cpp + :lines: 161-167 + +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/cpp/quickstart.cpp `_. + +.. api-examples:: + ../../../examples/api/cpp/quickstart.cpp + ../../../examples/api/smtlib/quickstart.smt2 diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py index e796e2404..eaa010e56 100644 --- a/docs/ext/smtliblexer.py +++ b/docs/ext/smtliblexer.py @@ -29,6 +29,8 @@ class SmtLibLexer(RegexLexer): (r'get-model', token.Keyword), (r'get-unsat-assumptions', token.Keyword), (r'get-unsat-core', token.Keyword), + (r'get-value', token.Keyword), + (r'reset-assertions', token.Keyword), (r'push', token.Keyword), (r'pop', token.Keyword), (r'as', token.Name.Attribute), @@ -51,6 +53,9 @@ class SmtLibLexer(RegexLexer): (r'distinct', token.Operator), (r'=', token.Operator), (r'>', token.Operator), + (r'<', token.Operator), + (r'<=', token.Operator), + (r'\+', token.Operator), (r'\*', token.Operator), (r'and', token.Operator), (r'bvadd', token.Operator), diff --git a/examples/api/cpp/quickstart.cpp b/examples/api/cpp/quickstart.cpp index 5d4849bc0..6bd661554 100644 --- a/examples/api/cpp/quickstart.cpp +++ b/examples/api/cpp/quickstart.cpp @@ -88,13 +88,13 @@ int main() solver.assertFormula(constraint4); // Check if the formula is satisfiable, that is, - // are there real values for x,y,z that satisfy all the constraints? + // are there real values for x and y that satisfy all the constraints? Result r1 = solver.checkSat(); // The result is either SAT, UNSAT, or UNKNOWN. // In this case, it is SAT. std::cout << "expected: sat" << std::endl; - std::cout << "result:" << r1 << std::endl; + std::cout << "result: " << r1 << std::endl; // We can get the values for x and y that satisfy the constraints. Term xVal = solver.getValue(x); @@ -105,7 +105,7 @@ int main() Term xMinusY = solver.mkTerm(MINUS, x, y); Term xMinusYVal = solver.getValue(xMinusY); - // We can now obtain thestring representations of the values. + // We can now obtain the string representations of the values. std::string xStr = xVal.getRealValue(); std::string yStr = yVal.getRealValue(); std::string xMinusYStr = xMinusYVal.getRealValue(); @@ -120,8 +120,8 @@ int main() double yDouble = std::stod(yStr); double xMinusYDouble = std::stod(xMinusYStr); - // Another way to independently compute the value of x and y would be using - // the ordinary cpp minus operator instead of asking the solver. + // Another way to independently compute the value of x - y would be + // to use the cpp minus operator instead of asking the solver. // However, for more complex terms, // it is easier to let the solver do the evaluation. double xMinusYComputed = xDouble - yDouble; diff --git a/examples/api/smtlib/quickstart.smt2 b/examples/api/smtlib/quickstart.smt2 new file mode 100644 index 000000000..a708edfd9 --- /dev/null +++ b/examples/api/smtlib/quickstart.smt2 @@ -0,0 +1,21 @@ +(set-logic ALL) +(set-option :produce-models true) +(set-option :produce-unsat-cores true) +(set-option :incremental true) +(declare-const x Real) +(declare-const y Real) +(assert (< 0 x)) +(assert (< 0 y)) +(assert (< (+ x y) 1)) +(assert (<= x y)) +(check-sat) +(get-value (x y (- x y))) +(reset-assertions) +(declare-const a Int) +(declare-const b Int) +(assert (! (< 0 a) :named a0)) +(assert (! (< 0 b) :named a1)) +(assert (! (< (+ a b) 1) :named a2)) +(assert (! (<= a b) :named a3)) +(check-sat) +(get-unsat-core) -- 2.30.2