From 7440f0568b99842d87cb1f86eec21aed9f46b92a Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 26 May 2021 08:30:45 +0200 Subject: [PATCH] Add more examples to the documentation (#6569) This PR adds (most of) the existing examples to the documentation, and does some other minor updates on the documentation. Some details: - for consistency, all cpp examples are moved from examples/api to examples/api/cpp - add capabilities for SMT-LIB examples, and two simple smt2 examples - more docs/examples/*.rst files - two new documentation categories: installation (how to obtain, compile and install cvc5) and binary (about the cvc5 binary) --- docs/binary/binary.rst | 7 +++++++ docs/{ => binary}/options.rst | 0 docs/conf.py.in | 1 + docs/cpp/cpp.rst | 2 ++ docs/examples/bitvectors.rst | 8 +++++++ docs/examples/bitvectors_and_arrays.rst | 8 +++++++ docs/examples/combination.rst | 8 +++++++ docs/examples/datatypes.rst | 6 +++--- docs/examples/examples.rst | 18 +++++++++++++++- docs/examples/exceptions.rst | 7 +++++++ docs/examples/extract.rst | 7 +++++++ docs/examples/floatingpoint.rst | 7 +++++++ docs/examples/helloworld.rst | 3 ++- docs/examples/lineararith.rst | 11 +++++++--- docs/examples/sequences.rst | 7 +++++++ docs/examples/sets.rst | 7 +++++++ docs/examples/strings.rst | 8 +++++++ docs/examples/sygus-fun.rst | 7 +++++++ docs/examples/sygus-grammar.rst | 7 +++++++ docs/examples/sygus-inv.rst | 7 +++++++ docs/ext/examples.py | 1 + docs/genindex.rst | 2 ++ docs/index.rst | 12 ++++------- docs/installation/installation.rst | 2 ++ docs/python/python.rst | 2 ++ examples/CMakeLists.txt | 2 +- examples/api/{ => cpp}/CMakeLists.txt | 0 examples/api/{ => cpp}/bitvectors.cpp | 0 .../api/{ => cpp}/bitvectors_and_arrays.cpp | 0 examples/api/{ => cpp}/combination.cpp | 0 examples/api/{ => cpp}/datatypes.cpp | 0 examples/api/{ => cpp}/extract.cpp | 0 examples/api/{ => cpp}/helloworld.cpp | 0 examples/api/{ => cpp}/linear_arith.cpp | 0 examples/api/{ => cpp}/sequences.cpp | 0 examples/api/{ => cpp}/sets.cpp | 0 examples/api/{ => cpp}/strings.cpp | 0 examples/api/{ => cpp}/sygus-fun.cpp | 0 examples/api/{ => cpp}/sygus-grammar.cpp | 0 examples/api/{ => cpp}/sygus-inv.cpp | 0 examples/api/{ => cpp}/utils.cpp | 0 examples/api/{ => cpp}/utils.h | 0 examples/api/smtlib/helloworld.smt2 | 4 ++++ examples/api/smtlib/linear_arith.smt2 | 21 +++++++++++++++++++ 44 files changed, 165 insertions(+), 17 deletions(-) create mode 100644 docs/binary/binary.rst rename docs/{ => binary}/options.rst (100%) create mode 100644 docs/examples/bitvectors.rst create mode 100644 docs/examples/bitvectors_and_arrays.rst create mode 100644 docs/examples/combination.rst create mode 100644 docs/examples/exceptions.rst create mode 100644 docs/examples/extract.rst create mode 100644 docs/examples/floatingpoint.rst create mode 100644 docs/examples/sequences.rst create mode 100644 docs/examples/sets.rst create mode 100644 docs/examples/strings.rst create mode 100644 docs/examples/sygus-fun.rst create mode 100644 docs/examples/sygus-grammar.rst create mode 100644 docs/examples/sygus-inv.rst create mode 100644 docs/genindex.rst create mode 100644 docs/installation/installation.rst rename examples/api/{ => cpp}/CMakeLists.txt (100%) rename examples/api/{ => cpp}/bitvectors.cpp (100%) rename examples/api/{ => cpp}/bitvectors_and_arrays.cpp (100%) rename examples/api/{ => cpp}/combination.cpp (100%) rename examples/api/{ => cpp}/datatypes.cpp (100%) rename examples/api/{ => cpp}/extract.cpp (100%) rename examples/api/{ => cpp}/helloworld.cpp (100%) rename examples/api/{ => cpp}/linear_arith.cpp (100%) rename examples/api/{ => cpp}/sequences.cpp (100%) rename examples/api/{ => cpp}/sets.cpp (100%) rename examples/api/{ => cpp}/strings.cpp (100%) rename examples/api/{ => cpp}/sygus-fun.cpp (100%) rename examples/api/{ => cpp}/sygus-grammar.cpp (100%) rename examples/api/{ => cpp}/sygus-inv.cpp (100%) rename examples/api/{ => cpp}/utils.cpp (100%) rename examples/api/{ => cpp}/utils.h (100%) create mode 100644 examples/api/smtlib/helloworld.smt2 create mode 100644 examples/api/smtlib/linear_arith.smt2 diff --git a/docs/binary/binary.rst b/docs/binary/binary.rst new file mode 100644 index 000000000..d28beab14 --- /dev/null +++ b/docs/binary/binary.rst @@ -0,0 +1,7 @@ +Binary Documentation +==================== + +.. toctree:: + :maxdepth: 2 + + options diff --git a/docs/options.rst b/docs/binary/options.rst similarity index 100% rename from docs/options.rst rename to docs/binary/options.rst diff --git a/docs/conf.py.in b/docs/conf.py.in index 9dc5255bd..6a23ff759 100644 --- a/docs/conf.py.in +++ b/docs/conf.py.in @@ -70,6 +70,7 @@ html_css_files = ['custom.css'] # -- Breathe configuration --------------------------------------------------- breathe_default_project = "cvc5" breathe_domain_by_extension = {"h" : "cpp"} +cpp_index_common_prefix = ["cvc5::api::"] # where to look for include-build-file ibf_folders = ['${CMAKE_CURRENT_BINARY_DIR}'] diff --git a/docs/cpp/cpp.rst b/docs/cpp/cpp.rst index a2e928927..8d302d60c 100644 --- a/docs/cpp/cpp.rst +++ b/docs/cpp/cpp.rst @@ -1,3 +1,5 @@ +.. _cpp-api: + C++ API Documentation ===================== diff --git a/docs/examples/bitvectors.rst b/docs/examples/bitvectors.rst new file mode 100644 index 000000000..354c86751 --- /dev/null +++ b/docs/examples/bitvectors.rst @@ -0,0 +1,8 @@ +Theory of Bit-Vectors +===================== + + +.. api-examples:: + ../../examples/api/cpp/bitvectors.cpp + ../../examples/api/java/BitVectors.java + ../../examples/api/python/bitvectors.py diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst new file mode 100644 index 000000000..9d63f36bd --- /dev/null +++ b/docs/examples/bitvectors_and_arrays.rst @@ -0,0 +1,8 @@ +Theory of Bit-Vectors and Arrays +================================ + + +.. api-examples:: + ../../examples/api/cpp/bitvectors_and_arrays.cpp + ../../examples/api/java/BitVectorsAndArrays.java + ../../examples/api/python/bitvectors_and_arrays.py diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst new file mode 100644 index 000000000..5f301a14f --- /dev/null +++ b/docs/examples/combination.rst @@ -0,0 +1,8 @@ +Theory Combination +================== + + +.. api-examples:: + ../../examples/api/cpp/combination.cpp + ../../examples/api/java/Combination.java + ../../examples/api/python/combination.py diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst index 8200ebb14..abbb16964 100644 --- a/docs/examples/datatypes.rst +++ b/docs/examples/datatypes.rst @@ -1,8 +1,8 @@ -Datatypes -=========== +Theory of Datatypes +=================== .. api-examples:: - ../../examples/api/datatypes.cpp + ../../examples/api/cpp/datatypes.cpp ../../examples/api/java/Datatypes.java ../../examples/api/python/datatypes.py diff --git a/docs/examples/examples.rst b/docs/examples/examples.rst index ff3651857..528566a3e 100644 --- a/docs/examples/examples.rst +++ b/docs/examples/examples.rst @@ -1,9 +1,25 @@ Examples =========== +The following examples show how the APIs (:ref:`cpp-api`, :ref:`python-api`) and input languages can be used. +For every example, the same problem is constructed and solved using different input mechanisms. + + .. toctree:: :maxdepth: 2 helloworld + exceptions + bitvectors + bitvectors_and_arrays + extract datatypes - lineararith \ No newline at end of file + floatingpoint + lineararith + sequences + sets + strings + combination + sygus-fun + sygus-grammar + sygus-inv \ No newline at end of file diff --git a/docs/examples/exceptions.rst b/docs/examples/exceptions.rst new file mode 100644 index 000000000..6598e8fb0 --- /dev/null +++ b/docs/examples/exceptions.rst @@ -0,0 +1,7 @@ +Exception Handling +====================================== + + +.. api-examples:: + ../../examples/api/java/Exceptions.java + ../../examples/api/python/exceptions.py diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst new file mode 100644 index 000000000..0108de948 --- /dev/null +++ b/docs/examples/extract.rst @@ -0,0 +1,7 @@ +Theory of Bit-Vectors: :code:`extract` +====================================== + + +.. api-examples:: + ../../examples/api/cpp/extract.cpp + ../../examples/api/python/extract.py diff --git a/docs/examples/floatingpoint.rst b/docs/examples/floatingpoint.rst new file mode 100644 index 000000000..1b09102b2 --- /dev/null +++ b/docs/examples/floatingpoint.rst @@ -0,0 +1,7 @@ +Theory of Floating-Points +====================================== + + +.. api-examples:: + ../../examples/api/java/FloatingPointArith.java + ../../examples/api/python/floating_point.py diff --git a/docs/examples/helloworld.rst b/docs/examples/helloworld.rst index 202952bb6..cdc424dfa 100644 --- a/docs/examples/helloworld.rst +++ b/docs/examples/helloworld.rst @@ -5,6 +5,7 @@ This example shows the very basic usage of the API. We create a solver, declare a Boolean variable and check whether it is entailed (by ``true``, as nothing has been asserted to the solver). .. api-examples:: - ../../examples/api/helloworld.cpp + ../../examples/api/cpp/helloworld.cpp ../../examples/api/java/HelloWorld.java ../../examples/api/python/helloworld.py + ../../examples/api/smtlib/helloworld.smt2 diff --git a/docs/examples/lineararith.rst b/docs/examples/lineararith.rst index d772edbb3..29d84cae5 100644 --- a/docs/examples/lineararith.rst +++ b/docs/examples/lineararith.rst @@ -1,8 +1,13 @@ -Linear Arithmetic -================= +Theory of Linear Arithmetic +=========================== +This example asserts three constraints over an integer variable :code:`x` and a real variable :code:`y`. +Firstly, it checks that these constraints entail an upper bound on the difference :code:`y - x <= 2/3`. +Secondly, it checks that this bound is tight by asserting :code:`y - x = 2/3` and checking for satisfiability. +The two checks are separated by using :code:`push` and :code:`pop`. .. api-examples:: - ../../examples/api/linear_arith.cpp + ../../examples/api/cpp/linear_arith.cpp ../../examples/api/java/LinearArith.java ../../examples/api/python/linear_arith.py + ../../examples/api/smtlib/linear_arith.smt2 diff --git a/docs/examples/sequences.rst b/docs/examples/sequences.rst new file mode 100644 index 000000000..a6f9e2238 --- /dev/null +++ b/docs/examples/sequences.rst @@ -0,0 +1,7 @@ +Theory of Sequences +=================== + + +.. api-examples:: + ../../examples/api/cpp/sequences.cpp + ../../examples/api/python/sequences.py diff --git a/docs/examples/sets.rst b/docs/examples/sets.rst new file mode 100644 index 000000000..71a6843c3 --- /dev/null +++ b/docs/examples/sets.rst @@ -0,0 +1,7 @@ +Theory of Sets +================= + + +.. api-examples:: + ../../examples/api/cpp/sets.cpp + ../../examples/api/python/sets.py diff --git a/docs/examples/strings.rst b/docs/examples/strings.rst new file mode 100644 index 000000000..87f566363 --- /dev/null +++ b/docs/examples/strings.rst @@ -0,0 +1,8 @@ +Theory of Strings +================= + + +.. api-examples:: + ../../examples/api/cpp/strings.cpp + ../../examples/api/java/Strings.java + ../../examples/api/python/strings.py diff --git a/docs/examples/sygus-fun.rst b/docs/examples/sygus-fun.rst new file mode 100644 index 000000000..3d5bddff1 --- /dev/null +++ b/docs/examples/sygus-fun.rst @@ -0,0 +1,7 @@ +SyGuS: Functions +=================== + + +.. api-examples:: + ../../examples/api/cpp/sygus-fun.cpp + ../../examples/api/python/sygus-fun.py diff --git a/docs/examples/sygus-grammar.rst b/docs/examples/sygus-grammar.rst new file mode 100644 index 000000000..3733fe2c3 --- /dev/null +++ b/docs/examples/sygus-grammar.rst @@ -0,0 +1,7 @@ +SyGuS: Grammars +=================== + + +.. api-examples:: + ../../examples/api/cpp/sygus-grammar.cpp + ../../examples/api/python/sygus-grammar.py diff --git a/docs/examples/sygus-inv.rst b/docs/examples/sygus-inv.rst new file mode 100644 index 000000000..f9698a720 --- /dev/null +++ b/docs/examples/sygus-inv.rst @@ -0,0 +1,7 @@ +SyGuS: Invariants +=================== + + +.. api-examples:: + ../../examples/api/cpp/sygus-inv.cpp + ../../examples/api/python/sygus-inv.py diff --git a/docs/ext/examples.py b/docs/ext/examples.py index befb6c175..003726de4 100644 --- a/docs/ext/examples.py +++ b/docs/ext/examples.py @@ -22,6 +22,7 @@ class APIExamples(Directive): '.cpp': {'title': 'C++', 'lang': 'c++'}, '.java': {'title': 'Java', 'lang': 'java'}, '.py': {'title': 'Python', 'lang': 'python'}, + '.smt2': {'title': 'SMT-LIBv2', 'lang': 'lisp'}, } # The "arguments" are actually the content of the directive diff --git a/docs/genindex.rst b/docs/genindex.rst new file mode 100644 index 000000000..9e530fa2f --- /dev/null +++ b/docs/genindex.rst @@ -0,0 +1,2 @@ +Index +===== diff --git a/docs/index.rst b/docs/index.rst index 8d77790fb..fc82111e2 100644 --- a/docs/index.rst +++ b/docs/index.rst @@ -6,17 +6,13 @@ cvc5 API Documentation ====================== - -* :ref:`genindex` - - ---------------- - .. toctree:: :maxdepth: 1 + installation/installation + binary/binary cpp/cpp python/python - references examples/examples - options + references + genindex diff --git a/docs/installation/installation.rst b/docs/installation/installation.rst new file mode 100644 index 000000000..e50cd8d4b --- /dev/null +++ b/docs/installation/installation.rst @@ -0,0 +1,2 @@ +Installation +============ \ No newline at end of file diff --git a/docs/python/python.rst b/docs/python/python.rst index 50d9077df..c3e425a7f 100644 --- a/docs/python/python.rst +++ b/docs/python/python.rst @@ -1,3 +1,5 @@ +.. _python-api: + Python API Documentation ======================== diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt index a7ca31a7a..076715f2e 100644 --- a/examples/CMakeLists.txt +++ b/examples/CMakeLists.txt @@ -78,7 +78,7 @@ cvc5_add_example(simple_vc_quant_cxx "" "") # # argument to binary (for testing) # ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2) -add_subdirectory(api) +add_subdirectory(api/cpp) # TODO(project issue $206): Port example to new API # add_subdirectory(nra-translate) # add_subdirectory(sets-translate) diff --git a/examples/api/CMakeLists.txt b/examples/api/cpp/CMakeLists.txt similarity index 100% rename from examples/api/CMakeLists.txt rename to examples/api/cpp/CMakeLists.txt diff --git a/examples/api/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp similarity index 100% rename from examples/api/bitvectors.cpp rename to examples/api/cpp/bitvectors.cpp diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/cpp/bitvectors_and_arrays.cpp similarity index 100% rename from examples/api/bitvectors_and_arrays.cpp rename to examples/api/cpp/bitvectors_and_arrays.cpp diff --git a/examples/api/combination.cpp b/examples/api/cpp/combination.cpp similarity index 100% rename from examples/api/combination.cpp rename to examples/api/cpp/combination.cpp diff --git a/examples/api/datatypes.cpp b/examples/api/cpp/datatypes.cpp similarity index 100% rename from examples/api/datatypes.cpp rename to examples/api/cpp/datatypes.cpp diff --git a/examples/api/extract.cpp b/examples/api/cpp/extract.cpp similarity index 100% rename from examples/api/extract.cpp rename to examples/api/cpp/extract.cpp diff --git a/examples/api/helloworld.cpp b/examples/api/cpp/helloworld.cpp similarity index 100% rename from examples/api/helloworld.cpp rename to examples/api/cpp/helloworld.cpp diff --git a/examples/api/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp similarity index 100% rename from examples/api/linear_arith.cpp rename to examples/api/cpp/linear_arith.cpp diff --git a/examples/api/sequences.cpp b/examples/api/cpp/sequences.cpp similarity index 100% rename from examples/api/sequences.cpp rename to examples/api/cpp/sequences.cpp diff --git a/examples/api/sets.cpp b/examples/api/cpp/sets.cpp similarity index 100% rename from examples/api/sets.cpp rename to examples/api/cpp/sets.cpp diff --git a/examples/api/strings.cpp b/examples/api/cpp/strings.cpp similarity index 100% rename from examples/api/strings.cpp rename to examples/api/cpp/strings.cpp diff --git a/examples/api/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp similarity index 100% rename from examples/api/sygus-fun.cpp rename to examples/api/cpp/sygus-fun.cpp diff --git a/examples/api/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp similarity index 100% rename from examples/api/sygus-grammar.cpp rename to examples/api/cpp/sygus-grammar.cpp diff --git a/examples/api/sygus-inv.cpp b/examples/api/cpp/sygus-inv.cpp similarity index 100% rename from examples/api/sygus-inv.cpp rename to examples/api/cpp/sygus-inv.cpp diff --git a/examples/api/utils.cpp b/examples/api/cpp/utils.cpp similarity index 100% rename from examples/api/utils.cpp rename to examples/api/cpp/utils.cpp diff --git a/examples/api/utils.h b/examples/api/cpp/utils.h similarity index 100% rename from examples/api/utils.h rename to examples/api/cpp/utils.h diff --git a/examples/api/smtlib/helloworld.smt2 b/examples/api/smtlib/helloworld.smt2 new file mode 100644 index 000000000..b33689bb7 --- /dev/null +++ b/examples/api/smtlib/helloworld.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_UF) +(declare-const |Hello World!| Bool) +(assert (not |Hello World!|)) +(check-sat) diff --git a/examples/api/smtlib/linear_arith.smt2 b/examples/api/smtlib/linear_arith.smt2 new file mode 100644 index 000000000..ede655b0e --- /dev/null +++ b/examples/api/smtlib/linear_arith.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_LIRA) +(declare-const x Int) +(declare-const y Real) +(assert + (and + (>= x (* 3 y)) + (<= x y) + (< (- 2) x) + ) +) +(push 1) +(echo "Checking entailement by asserting the negation") +(echo "Unsat == ENTAILED") +(assert (not (<= (- y x) (/ 2 3)))) +(check-sat) +(pop 1) +(push 1) +(echo "Checking that the assertions are consistent") +(assert (= (- y x) (/ 2 3))) +(check-sat) +(pop 1) -- 2.30.2