From c05fe825c6370a3f6bfe8c8264634d11b398567f Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 6 Jul 2021 13:29:25 -0300
Subject: [PATCH] Porting C++ API examples to SMT-LIB examples (#6789)

SyGuS examples will come later.
---
 docs/examples/bitvectors.rst                  |  1 +
 docs/examples/bitvectors_and_arrays.rst       |  1 +
 docs/examples/combination.rst                 |  1 +
 docs/examples/datatypes.rst                   |  1 +
 docs/examples/extract.rst                     |  1 +
 docs/examples/sequences.rst                   |  1 +
 docs/examples/strings.rst                     |  1 +
 examples/api/smtlib/bitvectors.smt2           | 42 ++++++++++++++
 .../api/smtlib/bitvectors_and_arrays.smt2     | 56 +++++++++++++++++++
 examples/api/smtlib/combination.smt2          | 31 ++++++++++
 examples/api/smtlib/datatypes.smt2            | 20 +++++++
 examples/api/smtlib/extract.smt2              | 14 +++++
 examples/api/smtlib/quickstart.smt2           | 26 +++++++--
 examples/api/smtlib/sequences.smt2            | 14 +++++
 examples/api/smtlib/sets.smt2                 |  3 +
 examples/api/smtlib/strings.smt2              | 28 ++++++++++
 16 files changed, 237 insertions(+), 4 deletions(-)
 create mode 100644 examples/api/smtlib/bitvectors.smt2
 create mode 100644 examples/api/smtlib/bitvectors_and_arrays.smt2
 create mode 100644 examples/api/smtlib/combination.smt2
 create mode 100644 examples/api/smtlib/datatypes.smt2
 create mode 100644 examples/api/smtlib/extract.smt2
 create mode 100644 examples/api/smtlib/sequences.smt2
 create mode 100644 examples/api/smtlib/strings.smt2

diff --git a/docs/examples/bitvectors.rst b/docs/examples/bitvectors.rst
index 354c86751..2d6469611 100644
--- a/docs/examples/bitvectors.rst
+++ b/docs/examples/bitvectors.rst
@@ -6,3 +6,4 @@ Theory of Bit-Vectors
     ../../examples/api/cpp/bitvectors.cpp
     ../../examples/api/java/BitVectors.java
     ../../examples/api/python/bitvectors.py
+    ../../examples/api/smtlib/bitvectors.smt2
diff --git a/docs/examples/bitvectors_and_arrays.rst b/docs/examples/bitvectors_and_arrays.rst
index 9d63f36bd..9a9d47bd5 100644
--- a/docs/examples/bitvectors_and_arrays.rst
+++ b/docs/examples/bitvectors_and_arrays.rst
@@ -6,3 +6,4 @@ Theory of Bit-Vectors and Arrays
     ../../examples/api/cpp/bitvectors_and_arrays.cpp
     ../../examples/api/java/BitVectorsAndArrays.java
     ../../examples/api/python/bitvectors_and_arrays.py
+    ../../examples/api/smtlib/bitvectors_and_arrays.smt2
diff --git a/docs/examples/combination.rst b/docs/examples/combination.rst
index 5f301a14f..e5f38e21e 100644
--- a/docs/examples/combination.rst
+++ b/docs/examples/combination.rst
@@ -6,3 +6,4 @@ Theory Combination
     ../../examples/api/cpp/combination.cpp
     ../../examples/api/java/Combination.java
     ../../examples/api/python/combination.py
+    ../../examples/api/smtlib/combination.smt2
diff --git a/docs/examples/datatypes.rst b/docs/examples/datatypes.rst
index abbb16964..4f2cbf176 100644
--- a/docs/examples/datatypes.rst
+++ b/docs/examples/datatypes.rst
@@ -6,3 +6,4 @@ Theory of Datatypes
     ../../examples/api/cpp/datatypes.cpp
     ../../examples/api/java/Datatypes.java
     ../../examples/api/python/datatypes.py
+    ../../examples/api/smtlib/datatypes.smt2
diff --git a/docs/examples/extract.rst b/docs/examples/extract.rst
index 0108de948..61eaa6462 100644
--- a/docs/examples/extract.rst
+++ b/docs/examples/extract.rst
@@ -5,3 +5,4 @@ Theory of Bit-Vectors: :code:`extract`
 .. api-examples::
     ../../examples/api/cpp/extract.cpp
     ../../examples/api/python/extract.py
+    ../../examples/api/smtlib/extract.smt2
diff --git a/docs/examples/sequences.rst b/docs/examples/sequences.rst
index a6f9e2238..569fdfc04 100644
--- a/docs/examples/sequences.rst
+++ b/docs/examples/sequences.rst
@@ -5,3 +5,4 @@ Theory of Sequences
 .. api-examples::
     ../../examples/api/cpp/sequences.cpp
     ../../examples/api/python/sequences.py
+    ../../examples/api/smtlib/sequences.smt2
diff --git a/docs/examples/strings.rst b/docs/examples/strings.rst
index 87f566363..cc6211061 100644
--- a/docs/examples/strings.rst
+++ b/docs/examples/strings.rst
@@ -6,3 +6,4 @@ Theory of Strings
     ../../examples/api/cpp/strings.cpp
     ../../examples/api/java/Strings.java
     ../../examples/api/python/strings.py
+    ../../examples/api/smtlib/strings.smt2
diff --git a/examples/api/smtlib/bitvectors.smt2 b/examples/api/smtlib/bitvectors.smt2
new file mode 100644
index 000000000..ccd8f61da
--- /dev/null
+++ b/examples/api/smtlib/bitvectors.smt2
@@ -0,0 +1,42 @@
+(set-logic QF_BV)
+(set-option :incremental true)
+
+(declare-const x (_ BitVec 32))
+(declare-const a (_ BitVec 32))
+(declare-const b (_ BitVec 32))
+(declare-const new_x (_ BitVec 32))
+(declare-const new_x_ (_ BitVec 32))
+
+(echo "Assert the assumption.")
+(assert (or (= x a) (= x b)))
+
+(echo "Asserting assignment to cvc5.")
+(assert (= new_x (ite (= x a) b a)))
+
+(echo "Pushing a new context.")
+(push 1)
+
+(echo "Asserting another assignment to cvc5.")
+(assert (= new_x_ (bvxor a b x)))
+
+(echo "Check entailment assuming new_x = new_x_.")
+(echo "UNSAT (of negation) == ENTAILED")
+(check-sat-assuming ((not (= new_x new_x_))))
+(echo "Popping context.")
+(pop 1)
+
+(echo "Asserting another assignment to cvc5.")
+(assert (= new_x_ (bvsub (bvadd a b) x)))
+
+(echo "Check entailment assuming new_x = new_x_.")
+(echo "UNSAT (of negation) == ENTAILED")
+(check-sat-assuming ((not (= new_x new_x_))))
+
+(echo "Check entailment assuming [new_x = new_x_, x != x.")
+(echo "UNSAT (of negation) == ENTAILED")
+(check-sat-assuming ((not (= new_x new_x_)) (not (= x x))))
+
+(echo "Assert that a is odd, i.e. lsb is one.")
+(assert (= ((_ extract 0 0) a) (_ bv1 1)))
+(echo "Check satisfiability, expecting sat.")
+(check-sat)
diff --git a/examples/api/smtlib/bitvectors_and_arrays.smt2 b/examples/api/smtlib/bitvectors_and_arrays.smt2
new file mode 100644
index 000000000..06afaf7ee
--- /dev/null
+++ b/examples/api/smtlib/bitvectors_and_arrays.smt2
@@ -0,0 +1,56 @@
+(set-logic QF_AUFBV)
+(set-option :produce-models true)
+
+; Consider the following code (where size is some previously defined constant):
+
+
+;   Assert (current_array[0] > 0);
+;   for (unsigned i = 1; i < k; ++i) {
+;     current_array[i] = 2 * current_array[i - 1];
+;     Assert (current_array[i-1] < current_array[i]);
+;     }
+
+; We want to check whether the assertion in the body of the for loop holds
+; throughout the loop. We will do so for k = 4.
+
+
+(define-sort Index () (_ BitVec 2))
+(define-sort Element () (_ BitVec 32))
+(define-sort ArraySort () (Array Index Element))
+
+; Declaring the array
+(declare-const current_array ArraySort)
+
+; Making utility bit-vector constants
+(define-const zeroI Index (_ bv0 2))
+(define-const oneI Index (_ bv1 2))
+(define-const twoI Index (_ bv2 2))
+(define-const threeI Index (_ bv3 2))
+
+(define-const zeroE Element (_ bv0 32))
+(define-const twoE Element (_ bv2 32))
+
+; Asserting that current_array[0] > 0
+(assert (bvsgt (select current_array zeroI) zeroE))
+
+; Building the formulas representing loop unrolling
+
+; current_array[0] < array [1]
+(define-const unroll1 Bool (bvslt (select current_array zeroI) (bvmul twoE (select current_array zeroI))))
+; current_array[1] = 2 * current_array[0]
+(define-const current_array_ ArraySort (store current_array oneI (bvmul twoE (select current_array zeroI))))
+
+; current_array[1] < array [2]
+(define-const unroll2 Bool (bvslt (select current_array_ oneI) (bvmul twoE (select current_array_ oneI))))
+; current_array[2] = 2 * current_array[1]
+(define-const current_array__ ArraySort (store current_array_ twoI (bvmul twoE (select current_array_ oneI))))
+
+; current_array[2] < array [3]
+(define-const unroll3 Bool (bvslt (select current_array_ twoI) (bvmul twoE (select current_array_ twoI))))
+; current_array[3] = 2 * current_array[2]
+(define-const current_array___ ArraySort (store current_array_ threeI (bvmul twoE (select current_array_ twoI))))
+
+(assert (not (and unroll1 unroll2 unroll3)))
+
+(check-sat)
+(get-value (current_array___ (select current_array___ zeroI)))
diff --git a/examples/api/smtlib/combination.smt2 b/examples/api/smtlib/combination.smt2
new file mode 100644
index 000000000..113a11b7b
--- /dev/null
+++ b/examples/api/smtlib/combination.smt2
@@ -0,0 +1,31 @@
+(set-logic QF_UFLIRA)
+(set-option :produce-models true)
+(set-option :incremental true)
+
+(declare-sort U 0)
+
+(declare-const x U)
+(declare-const y U)
+
+(declare-fun f (U) Int)
+(declare-fun p (Int) Bool)
+
+; 0 <= f(x)
+(assert (<= 0 (f x)))
+; 0 <= f(y)
+(assert (<= 0 (f y)))
+; f(x) + f(y) <= 1
+(assert (<= (+ (f x) (f y)) 1))
+; not p(0)
+(assert (not (p 0)))
+; p(f(y))
+(assert (p (f y)))
+
+(echo "Prove x != y is entailed. UNSAT (of negation) == ENTAILED")
+(check-sat-assuming ((not (distinct x y))))
+
+(echo "Call checkSat to show that the assertions are satisfiable")
+(check-sat)
+
+(echo "Call (getValue (...)) on terms of interest")
+(get-value ((f x) (f y) (+ (f x) (f y)) (p 0) (p (f y))))
diff --git a/examples/api/smtlib/datatypes.smt2 b/examples/api/smtlib/datatypes.smt2
new file mode 100644
index 000000000..b8fc21414
--- /dev/null
+++ b/examples/api/smtlib/datatypes.smt2
@@ -0,0 +1,20 @@
+(set-logic QF_UFDTLIA)
+
+; declaring a List datatype and defining List terms
+(declare-datatype List ((cons (head Int) (tail List)) (nil)))
+
+(define-const t List (cons 0 nil))
+(define-const t2 Int (head t))
+
+; declaring a parameterized datatype. We need the general
+; declare-datatypes command since the singular version is a macro for
+; the (declare-datatypes ((<type> 0)) <declaration>)
+(declare-datatypes ((ParList 1))
+  ((par (T) ((cons (parHead T) (parTail (ParList T))) (nil)))))
+
+(define-sort ParListInt () (ParList Int))
+(declare-const a ParListInt)
+(define-const aHead Int (parHead a))
+
+(assert (< aHead 50))
+(check-sat)
diff --git a/examples/api/smtlib/extract.smt2 b/examples/api/smtlib/extract.smt2
new file mode 100644
index 000000000..8bbabb77a
--- /dev/null
+++ b/examples/api/smtlib/extract.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_BV)
+
+(declare-const a (_ BitVec 32))
+
+(define-const a_31_1 (_ BitVec 31) ((_ extract 31 1) a))
+(define-const a_30_0 (_ BitVec 31) ((_ extract 30 0) a))
+(define-const a_31_31 (_ BitVec 1) ((_ extract 31 31) a))
+(define-const a_0_0 (_ BitVec 1) ((_ extract 0 0) a))
+
+(echo "Asserting a_31_1 = a_30_0")
+(assert (= a_31_1 a_30_0))
+
+(echo "Check unsatisfiability assuming a_31_31 != a_0_0")
+(check-sat (not (= a_31_31 a_0_0)))
\ No newline at end of file
diff --git a/examples/api/smtlib/quickstart.smt2 b/examples/api/smtlib/quickstart.smt2
index a708edfd9..c1597aa5c 100644
--- a/examples/api/smtlib/quickstart.smt2
+++ b/examples/api/smtlib/quickstart.smt2
@@ -2,20 +2,38 @@
 (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
+(set-option :dump-unsat-cores-full true)
+
+; Declare real constanst x,y
 (declare-const x Real)
 (declare-const y Real)
+
+; Our constraints regarding x and y will be:
+;
+;   (1)  0 < x
+;   (2)  0 < y
+;   (3)  x + y < 1
+;   (4)  x <= y
+
 (assert (< 0 x))
 (assert (< 0 y))
 (assert (< (+ x y) 1))
 (assert (<= x y))
+
 (check-sat)
+(echo "Values of declared real constants and of compound terms built with them.")
 (get-value (x y (- x y)))
+
+(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-const a Int)
 (declare-const b Int)
-(assert (! (< 0 a) :named a0))
-(assert (! (< 0 b) :named a1))
-(assert (! (< (+ a b) 1) :named a2))
-(assert (! (<= a b) :named a3))
+(assert (< 0 a))
+(assert (< 0 b))
+(assert (< (+ a b) 1))
+(assert (<= a b))
+
 (check-sat)
 (get-unsat-core)
diff --git a/examples/api/smtlib/sequences.smt2 b/examples/api/smtlib/sequences.smt2
new file mode 100644
index 000000000..2f1a5977e
--- /dev/null
+++ b/examples/api/smtlib/sequences.smt2
@@ -0,0 +1,14 @@
+(set-logic QF_SLIA)
+(set-option :produce-models true)
+
+; create integer sequence constants
+(declare-const x (Seq Int))
+(declare-const y (Seq Int))
+
+; |x.y.empty| > 1
+(assert (> (seq.len (seq.++ x y (as seq.empty (Seq Int)))) 1))
+; x = seq(1)
+(assert (= x (seq.unit 1)))
+
+(check-sat)
+(get-value (x y))
diff --git a/examples/api/smtlib/sets.smt2 b/examples/api/smtlib/sets.smt2
index 437c285e2..2e4b76b46 100644
--- a/examples/api/smtlib/sets.smt2
+++ b/examples/api/smtlib/sets.smt2
@@ -32,3 +32,6 @@
         (union (singleton 2) (singleton 3))))
   )
 )
+
+(echo "A member: ")
+(get-value (x))
\ No newline at end of file
diff --git a/examples/api/smtlib/strings.smt2 b/examples/api/smtlib/strings.smt2
new file mode 100644
index 000000000..fade18c5a
--- /dev/null
+++ b/examples/api/smtlib/strings.smt2
@@ -0,0 +1,28 @@
+(set-logic QF_SLIA)
+(set-option :produce-models true)
+
+(define-const ab String "ab")
+(define-const abc String "abc")
+
+(declare-const x String)
+(declare-const y String)
+(declare-const z String)
+
+; x.ab.y = abc.z
+(assert (= (str.++ x ab y) (str.++ abc z)))
+; |y| >= 0
+(assert (>= (str.len y) 0))
+
+; Regular expression: (ab[c-e]*f)|g|h
+(define-const r RegLan
+  (re.union
+    (re.++ (str.to_re "ab") (re.* (re.range "c" "e")) (str.to_re "f"))
+    (str.to_re "f")
+    (str.to_re "h")
+    )
+  )
+
+; s1.s2 in (ab[c-e]*f)|g|h
+(assert (str.in_re (str.++ "s1" "s2") r))
+
+(check-sat)
-- 
2.30.2