diff options
Diffstat (limited to 'examples/api')
-rw-r--r-- | examples/api/smtlib/bitvectors.smt2 | 42 | ||||
-rw-r--r-- | examples/api/smtlib/bitvectors_and_arrays.smt2 | 56 | ||||
-rw-r--r-- | examples/api/smtlib/combination.smt2 | 31 | ||||
-rw-r--r-- | examples/api/smtlib/datatypes.smt2 | 20 | ||||
-rw-r--r-- | examples/api/smtlib/extract.smt2 | 14 | ||||
-rw-r--r-- | examples/api/smtlib/quickstart.smt2 | 26 | ||||
-rw-r--r-- | examples/api/smtlib/sequences.smt2 | 14 | ||||
-rw-r--r-- | examples/api/smtlib/sets.smt2 | 3 | ||||
-rw-r--r-- | examples/api/smtlib/strings.smt2 | 28 |
9 files changed, 230 insertions, 4 deletions
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) |