diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2020-06-23 09:55:01 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-23 09:55:01 -0700 |
commit | 0539b0342b46e9fb96467a23f703bf2317692bb2 (patch) | |
tree | 1c2d54f7791ee472daa40efc63ce88e13b9e4cc8 /test/regress/regress0 | |
parent | bea30aa5dd6b36fc5a206c4742abadf8c3fab5c1 (diff) |
Add support for eqrange predicate (#4562)
This commit adds support for an eqrange predicate. (eqrange a b i j) is true if arrays a and b are equal on all indices within indices i and j, i.e., \forall k . i <= k <= j --> a[k] = b[k]. Requires option --arrays-exp to be enabled.
Diffstat (limited to 'test/regress/regress0')
-rw-r--r-- | test/regress/regress0/eqrange1.smt2 | 15 | ||||
-rw-r--r-- | test/regress/regress0/eqrange2.smt2 | 12 | ||||
-rw-r--r-- | test/regress/regress0/eqrange3.smt2 | 16 |
3 files changed, 43 insertions, 0 deletions
diff --git a/test/regress/regress0/eqrange1.smt2 b/test/regress/regress0/eqrange1.smt2 new file mode 100644 index 000000000..90eb7a22a --- /dev/null +++ b/test/regress/regress0/eqrange1.smt2 @@ -0,0 +1,15 @@ +(set-logic QF_AUFBV) +(set-option :arrays-exp true) +(set-option :quiet true) ; Suppress check-model warnings involving quantifiers +(set-info :status sat) +(declare-fun a1 () (Array (_ BitVec 2) (_ BitVec 2))) +(declare-fun a2 () (Array (_ BitVec 2) (_ BitVec 2))) +(declare-fun e1 () (_ BitVec 2)) +(declare-fun e2 () (_ BitVec 2)) +(assert (distinct e1 e2)) +(assert (= a1 (store (store (store (store a1 #b00 e1) #b01 e1) #b10 e1) #b11 e1))) +(assert (= a2 (store (store (store (store a2 #b00 e1) #b01 e1) #b10 e2) #b11 e1))) +(assert (eqrange a1 a2 #b00 #b01)) +(assert (eqrange a1 a2 #b11 #b11)) +(check-sat) +(exit) diff --git a/test/regress/regress0/eqrange2.smt2 b/test/regress/regress0/eqrange2.smt2 new file mode 100644 index 000000000..efddbc88b --- /dev/null +++ b/test/regress/regress0/eqrange2.smt2 @@ -0,0 +1,12 @@ +(set-logic AUFBV) +(set-option :arrays-exp true) +(set-info :status unsat) +(declare-sort Element 0) +(declare-const a (Array (_ BitVec 3) Element)) +(declare-const b (Array (_ BitVec 3) Element)) +(declare-const j (_ BitVec 3)) +(assert (eqrange a b (_ bv0 3) j)) +(assert (eqrange a b (bvadd j (_ bv1 3)) (_ bv7 3))) +(assert (exists ((i (_ BitVec 3))) (not (= (select a i) (select b i))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/eqrange3.smt2 b/test/regress/regress0/eqrange3.smt2 new file mode 100644 index 000000000..54e9d0386 --- /dev/null +++ b/test/regress/regress0/eqrange3.smt2 @@ -0,0 +1,16 @@ +(set-logic QF_AUFLIA) +(set-option :arrays-exp true) +(set-option :quiet true) ; Suppress Warning +(set-info :status sat) +(declare-fun a1 () (Array Int Int)) +(declare-fun a2 () (Array Int Int)) +(declare-fun e1 () Int) +(declare-fun e2 () Int) +(assert (distinct e1 e2)) +(assert (= a1 (store (store (store (store a1 0 e1) 1 e1) 2 e1) 3 e1))) +(assert (= a2 (store (store (store (store a2 1 e1) 0 e1) 2 e2) 3 e1))) +(assert (eqrange a1 a2 (- 1) 1)) +(assert (eqrange a1 a2 3 3)) +(check-sat) +(exit) + |