Merge branch 'master' into includesincludes

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)