Add a binary / SMT-LIB quickstart (#7315)

This PR adds a binary/SMT-LIBv2 quickstart example, based on the cpp quickstart example.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 8f646e50a38bd3dbc0d6c9322250fd04c397733e..2a72cf2c3b6f17f742ed56faf0307f586646699b 100644 (file)
--- 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 dec07c5f02d99277d0576deab0b8cf9ac72b6c0e..d171edda957baadf6c8e4b8ff64f8137ded74943 100644 (file)
--- 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 ac71fa76c12520809e8fa0ec0198b51b3a507892..22a94701039a486a57bf09795a3afbbdce9e9fce 100644 (file)
--- 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 d28beab1497f8d755504ae70a10bd94cba72148e..d583c82d771d163d44b7dbd3d4e59891adbcfd3a 100644 (file)
--- 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 (file)
index 0000000..67280ca
--- /dev/null
+++ b/docs/binary/quickstart.rst
@@ -0,0 +1,125 @@
+Quickstart Guide
+================
+
+The primary input language for cvc5 is
+`SMT-LIB v2 <http://smtlib.cs.uiowa.edu/language.shtml>`_.
+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 `(<term> <value>)` 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 <https://github.com/cvc5/cvc5/blob/master/examples/api/smtlib/quickstart.smt2>`_.
+| The source code for this example can be found at `examples/api/smtlib/quickstart.smt2 <https://github.com/cvc5/cvc5/blob/master/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 c1597aa5c99b6e6219b98c0478531180a846e0bf..b5dc87d2bb5aa2ec295af9b2dc4d2f4e0cab82d8 100644 (file)
--- 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))