SyGuS examples will come later.
../../examples/api/cpp/bitvectors.cpp
../../examples/api/java/BitVectors.java
../../examples/api/python/bitvectors.py
+ ../../examples/api/smtlib/bitvectors.smt2
../../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
../../examples/api/cpp/combination.cpp
../../examples/api/java/Combination.java
../../examples/api/python/combination.py
+ ../../examples/api/smtlib/combination.smt2
../../examples/api/cpp/datatypes.cpp
../../examples/api/java/Datatypes.java
../../examples/api/python/datatypes.py
+ ../../examples/api/smtlib/datatypes.smt2
.. api-examples::
../../examples/api/cpp/extract.cpp
../../examples/api/python/extract.py
+ ../../examples/api/smtlib/extract.smt2
.. api-examples::
../../examples/api/cpp/sequences.cpp
../../examples/api/python/sequences.py
+ ../../examples/api/smtlib/sequences.smt2
../../examples/api/cpp/strings.cpp
../../examples/api/java/Strings.java
../../examples/api/python/strings.py
+ ../../examples/api/smtlib/strings.smt2
--- /dev/null
+(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)
--- /dev/null
+(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)))
--- /dev/null
+(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))))
--- /dev/null
+(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)
--- /dev/null
+(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
(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)
--- /dev/null
+(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))
(union (singleton 2) (singleton 3))))
)
)
+
+(echo "A member: ")
+(get-value (x))
\ No newline at end of file
--- /dev/null
+(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)
projects / cvc5.git / commitdiff