diff options
author | Gereon Kremer <nafur42@gmail.com> | 2021-05-26 08:30:45 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-26 06:30:45 +0000 |
commit | 7440f0568b99842d87cb1f86eec21aed9f46b92a (patch) | |
tree | 1fa6a41efcf4bb0946bac7ea43abc8cdcbd2a0c8 /examples | |
parent | 14b4666bec5cf6a8058254d740e94eda388f4760 (diff) |
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)
Diffstat (limited to 'examples')
-rw-r--r-- | examples/CMakeLists.txt | 2 | ||||
-rw-r--r-- | examples/api/cpp/CMakeLists.txt (renamed from examples/api/CMakeLists.txt) | 0 | ||||
-rw-r--r-- | examples/api/cpp/bitvectors.cpp (renamed from examples/api/bitvectors.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/bitvectors_and_arrays.cpp (renamed from examples/api/bitvectors_and_arrays.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/combination.cpp (renamed from examples/api/combination.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/datatypes.cpp (renamed from examples/api/datatypes.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/extract.cpp (renamed from examples/api/extract.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/helloworld.cpp (renamed from examples/api/helloworld.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/linear_arith.cpp (renamed from examples/api/linear_arith.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/sequences.cpp (renamed from examples/api/sequences.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/sets.cpp (renamed from examples/api/sets.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/strings.cpp (renamed from examples/api/strings.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/sygus-fun.cpp (renamed from examples/api/sygus-fun.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/sygus-grammar.cpp (renamed from examples/api/sygus-grammar.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/sygus-inv.cpp (renamed from examples/api/sygus-inv.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/utils.cpp (renamed from examples/api/utils.cpp) | 0 | ||||
-rw-r--r-- | examples/api/cpp/utils.h (renamed from examples/api/utils.h) | 0 | ||||
-rw-r--r-- | examples/api/smtlib/helloworld.smt2 | 4 | ||||
-rw-r--r-- | examples/api/smtlib/linear_arith.smt2 | 21 |
19 files changed, 26 insertions, 1 deletions
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 index bff7caa4d..bff7caa4d 100644 --- a/examples/api/CMakeLists.txt +++ b/examples/api/cpp/CMakeLists.txt diff --git a/examples/api/bitvectors.cpp b/examples/api/cpp/bitvectors.cpp index 8768bd996..8768bd996 100644 --- a/examples/api/bitvectors.cpp +++ b/examples/api/cpp/bitvectors.cpp diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/cpp/bitvectors_and_arrays.cpp index 547b294a0..547b294a0 100644 --- a/examples/api/bitvectors_and_arrays.cpp +++ b/examples/api/cpp/bitvectors_and_arrays.cpp diff --git a/examples/api/combination.cpp b/examples/api/cpp/combination.cpp index d47897a7c..d47897a7c 100644 --- a/examples/api/combination.cpp +++ b/examples/api/cpp/combination.cpp diff --git a/examples/api/datatypes.cpp b/examples/api/cpp/datatypes.cpp index 76c6da0f0..76c6da0f0 100644 --- a/examples/api/datatypes.cpp +++ b/examples/api/cpp/datatypes.cpp diff --git a/examples/api/extract.cpp b/examples/api/cpp/extract.cpp index d21c59d59..d21c59d59 100644 --- a/examples/api/extract.cpp +++ b/examples/api/cpp/extract.cpp diff --git a/examples/api/helloworld.cpp b/examples/api/cpp/helloworld.cpp index 21eb8e8fc..21eb8e8fc 100644 --- a/examples/api/helloworld.cpp +++ b/examples/api/cpp/helloworld.cpp diff --git a/examples/api/linear_arith.cpp b/examples/api/cpp/linear_arith.cpp index 02ddd956c..02ddd956c 100644 --- a/examples/api/linear_arith.cpp +++ b/examples/api/cpp/linear_arith.cpp diff --git a/examples/api/sequences.cpp b/examples/api/cpp/sequences.cpp index 5ee66048f..5ee66048f 100644 --- a/examples/api/sequences.cpp +++ b/examples/api/cpp/sequences.cpp diff --git a/examples/api/sets.cpp b/examples/api/cpp/sets.cpp index 5c9652707..5c9652707 100644 --- a/examples/api/sets.cpp +++ b/examples/api/cpp/sets.cpp diff --git a/examples/api/strings.cpp b/examples/api/cpp/strings.cpp index a952b31d1..a952b31d1 100644 --- a/examples/api/strings.cpp +++ b/examples/api/cpp/strings.cpp diff --git a/examples/api/sygus-fun.cpp b/examples/api/cpp/sygus-fun.cpp index 0f96e72a7..0f96e72a7 100644 --- a/examples/api/sygus-fun.cpp +++ b/examples/api/cpp/sygus-fun.cpp diff --git a/examples/api/sygus-grammar.cpp b/examples/api/cpp/sygus-grammar.cpp index ce5a1bc8b..ce5a1bc8b 100644 --- a/examples/api/sygus-grammar.cpp +++ b/examples/api/cpp/sygus-grammar.cpp diff --git a/examples/api/sygus-inv.cpp b/examples/api/cpp/sygus-inv.cpp index f658fa33a..f658fa33a 100644 --- a/examples/api/sygus-inv.cpp +++ b/examples/api/cpp/sygus-inv.cpp diff --git a/examples/api/utils.cpp b/examples/api/cpp/utils.cpp index 69676819a..69676819a 100644 --- a/examples/api/utils.cpp +++ b/examples/api/cpp/utils.cpp diff --git a/examples/api/utils.h b/examples/api/cpp/utils.h index 69cddee26..69cddee26 100644 --- a/examples/api/utils.h +++ b/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) |