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.

4 files changed, 46 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 690135b54..bb0f311d1 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -473,6 +473,9 @@ set(regress_0_tests
   regress0/distinct.smtv1.smt2
   regress0/dump-unsat-core-full.smt2
   regress0/simple-dump-model.smt2
+  regress0/eqrange1.smt2
+  regress0/eqrange2.smt2
+  regress0/eqrange3.smt2
   regress0/expect/scrub.01.smtv1.smt2
   regress0/expect/scrub.03.smt2
   regress0/expect/scrub.06.cvc
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)
+