From e5e727c868e169028bb24ca4547ba7078d366161 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 7 Oct 2021 11:26:31 -0700 Subject: [PATCH] Add a binary / SMT-LIB quickstart (#7315) This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example. --- CMakeLists.txt | 2 +- docs/api/cpp/quickstart.rst | 1 + docs/api/python/quickstart.rst | 1 + docs/binary/binary.rst | 5 +- docs/binary/quickstart.rst | 125 ++++++++++++++++++++++++++++ examples/api/smtlib/quickstart.smt2 | 8 +- 6 files changed, 136 insertions(+), 6 deletions(-) create mode 100644 docs/binary/quickstart.rst diff --git a/CMakeLists.txt b/CMakeLists.txt index 8f646e50a..2a72cf2c3 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -131,7 +131,7 @@ option(BUILD_BINDINGS_PYTHON "Build Python bindings based on new C++ API ") option(BUILD_BINDINGS_JAVA "Build Java bindings based on new C++ API ") # Api documentation -cvc5_option(BUILD_DOCS "Build Api documentation") +option(BUILD_DOCS "Build Api documentation") #-----------------------------------------------------------------------------# # Internal cmake variables diff --git a/docs/api/cpp/quickstart.rst b/docs/api/cpp/quickstart.rst index dec07c5f0..d171edda9 100644 --- a/docs/api/cpp/quickstart.rst +++ b/docs/api/cpp/quickstart.rst @@ -182,5 +182,6 @@ Example .. api-examples:: ../../../examples/api/cpp/quickstart.cpp + ../../../examples/api/java/QuickStart.java ../../../examples/api/python/quickstart.py ../../../examples/api/smtlib/quickstart.smt2 diff --git a/docs/api/python/quickstart.rst b/docs/api/python/quickstart.rst index ac71fa76c..22a947010 100644 --- a/docs/api/python/quickstart.rst +++ b/docs/api/python/quickstart.rst @@ -170,5 +170,6 @@ Example .. api-examples:: ../../../examples/api/cpp/quickstart.cpp + ../../../examples/api/java/QuickStart.java ../../../examples/api/python/quickstart.py ../../../examples/api/smtlib/quickstart.smt2 diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst index d28beab14..d583c82d7 100644 --- a/docs/binary/binary.rst +++ b/docs/binary/binary.rst @@ -1,7 +1,10 @@ Binary Documentation ==================== + + .. toctree:: :maxdepth: 2 - options + quickstart + options \ No newline at end of file diff --git a/docs/binary/quickstart.rst b/docs/binary/quickstart.rst new file mode 100644 index 000000000..67280ca45 --- /dev/null +++ b/docs/binary/quickstart.rst @@ -0,0 +1,125 @@ +Quickstart Guide +================ + +The primary input language for cvc5 is +`SMT-LIB v2 `_. +We give a short explanation of the SMT-LIB v2 quickstart +example here. + +First, 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/smtlib/quickstart.smt2 + :language: smtlib + :lines: 1 + +We will ask the solver to produce models and unsat cores in the following, +and for this we have to enable the following options. +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 + +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 + +We define the following constraints regarding ``x`` and ``y``: + +.. math:: + + (0 < x) \wedge (0 < y) \wedge (x + y < 1) \wedge (x \leq 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 + +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 + +The result we get from this satisfiability check is either ``sat``, ``unsat`` +or ``unknown``, and it is printed to standard output. +In this case, it will print ``sat``. + +Now, we query the solver for the values for ``x`` and ``y`` that satisfy +the constraints. +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 + +This will print the values of `x`, `y`, and `x-y`, in a key-value format `( )` one after the other: + +.. code:: text + + ((x (/ 1 6)) (y (/ 1 6)) ((- x y) 0.0)) + +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 and declare fresh +integer variables ``a`` and ``b``. + +.. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 + :language: smtlib + :lines: 28-32 + +Next, we assert the same assertions as above, but with integers. + +.. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 + :language: smtlib + :lines: 33-36 + +Now, we check whether the revised query is satisfiable. + +.. literalinclude:: ../../examples/api/smtlib/quickstart.smt2 + :language: smtlib + :lines: 38 + +This time the asserted formula is unsatisfiable and ``unsat`` is printed. + +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 + +This will print: + +.. code:: text + + ( + (< 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/smtlib/quickstart.smt2 `_. + +.. api-examples:: + ../../examples/api/cpp/quickstart.cpp + ../../examples/api/java/QuickStart.java + ../../examples/api/python/quickstart.py + ../../examples/api/smtlib/quickstart.smt2 diff --git a/examples/api/smtlib/quickstart.smt2 b/examples/api/smtlib/quickstart.smt2 index c1597aa5c..b5dc87d2b 100644 --- a/examples/api/smtlib/quickstart.smt2 +++ b/examples/api/smtlib/quickstart.smt2 @@ -1,11 +1,11 @@ (set-logic ALL) (set-option :produce-models true) -(set-option :produce-unsat-cores true) (set-option :incremental true) -; necessary to print in the unsat core assertions that do not have names +; 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) -; Declare real constanst x,y +; Declare real constants x,y (declare-const x Real) (declare-const y Real) @@ -27,7 +27,7 @@ (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 constanst a,b +; Declare integer constants a,b (declare-const a Int) (declare-const b Int) (assert (< 0 a)) -- 2.30.2