--- /dev/null
+Quickstart Guide
+================
+
+First, create a cvc5 :cpp:class:`Solver <cvc5::api::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 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
+| The source code for this example can be found at `examples/api/cpp/quickstart.cpp <https://github.com/cvc5/cvc5/blob/master/examples/api/cpp/quickstart.cpp>`_.
+
+.. api-examples::
+ ../../../examples/api/cpp/quickstart.cpp
+ ../../../examples/api/smtlib/quickstart.smt2
(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),
(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),
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);
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();
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;
projects / cvc5.git / commitdiff