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, 112 insertions, 0 deletions

diff --git a/src/theory/arrays/kinds b/src/theory/arrays/kinds
index 1adbdb0b2..659f05ae8 100644
--- a/src/theory/arrays/kinds
+++ b/src/theory/arrays/kinds
@@ -31,6 +31,9 @@ operator SELECT 2 "array select; first parameter is an array term, second is the
 # store a i e  is  a[i] <= e
 operator STORE 3 "array store; first parameter is an array term, second is the store index, third is the term to store at the index"
 
+# eqrange a b i j  \forall k. i <= k <= j -> a[k] = b[k]
+operator EQ_RANGE 4 "equality of two arrays over an index range lower/upper"
+
 # storeall t e  is  \all i in indexType(t) <= e
 constant STORE_ALL \
     ::CVC4::ArrayStoreAll \
@@ -53,6 +56,7 @@ typerule STORE ::CVC4::theory::arrays::ArrayStoreTypeRule
 typerule STORE_ALL ::CVC4::theory::arrays::ArrayStoreTypeRule
 typerule ARR_TABLE_FUN ::CVC4::theory::arrays::ArrayTableFunTypeRule
 typerule ARRAY_LAMBDA ::CVC4::theory::arrays::ArrayLambdaTypeRule
+typerule EQ_RANGE ::CVC4::theory::arrays::ArrayEqRangeTypeRule
 
 operator PARTIAL_SELECT_0 0:2 "partial array select, for internal use only"
 operator PARTIAL_SELECT_1 0:2 "partial array select, for internal use only"
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 0f5d9ec8b..71e040ccc 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -2312,6 +2312,61 @@ std::string TheoryArrays::TheoryArraysDecisionStrategy::identify() const
   return std::string("th_arrays_dec");
 }
 
+Node TheoryArrays::expandDefinition(Node node)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Kind kind = node.getKind();
+
+  /* Expand
+   *
+   *   (eqrange a b i j)
+   *
+   * to
+   *
+   *  forall k . i <= k <= j => a[k] = b[k]
+   *
+   */
+  if (kind == kind::EQ_RANGE)
+  {
+    TNode a = node[0];
+    TNode b = node[1];
+    TNode i = node[2];
+    TNode j = node[3];
+    Node k = nm->mkBoundVar(i.getType());
+    Node bvl = nm->mkNode(kind::BOUND_VAR_LIST, k);
+    TypeNode type = k.getType();
+
+    Kind kle;
+    Node range;
+    if (type.isBitVector())
+    {
+      kle = kind::BITVECTOR_ULE;
+    }
+    else if (type.isFloatingPoint())
+    {
+      kle = kind::FLOATINGPOINT_LEQ;
+    }
+    else if (type.isInteger() || type.isReal())
+    {
+      kle = kind::LEQ;
+    }
+    else
+    {
+      Unimplemented() << "Type " << type << " is not supported for predicate "
+                      << kind;
+    }
+
+    range = nm->mkNode(kind::AND, nm->mkNode(kle, i, k), nm->mkNode(kle, k, j));
+
+    Node eq = nm->mkNode(kind::EQUAL,
+                         nm->mkNode(kind::SELECT, a, k),
+                         nm->mkNode(kind::SELECT, b, k));
+    Node implies = nm->mkNode(kind::IMPLIES, range, eq);
+    return nm->mkNode(kind::FORALL, bvl, implies);
+  }
+  return node;
+}
+
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 8c94f08cd..c5cd24fd3 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -151,6 +151,8 @@ class TheoryArrays : public Theory {
 
   std::string identify() const override { return std::string("TheoryArrays"); }
 
+  Node expandDefinition(Node node) override;
+
   /////////////////////////////////////////////////////////////////////////////
   // PREPROCESSING
   /////////////////////////////////////////////////////////////////////////////
diff --git a/src/theory/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index facc81f43..e5681d50f 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -224,6 +224,57 @@ struct ArrayPartialSelectTypeRule {
   }
 };/* struct ArrayPartialSelectTypeRule */
 
+struct ArrayEqRangeTypeRule
+{
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    Assert(n.getKind() == kind::EQ_RANGE);
+    if (check)
+    {
+      TypeNode n0_type = n[0].getType(check);
+      TypeNode n1_type = n[1].getType(check);
+      if (!n0_type.isArray())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "first operand of eqrange is not an array");
+      }
+      if (!n1_type.isArray())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "second operand of eqrange is not an array");
+      }
+      if (n0_type != n1_type)
+      {
+        throw TypeCheckingExceptionPrivate(n, "array types do not match");
+      }
+      TypeNode indexType = n0_type.getArrayIndexType();
+      TypeNode indexRangeType1 = n[2].getType(check);
+      TypeNode indexRangeType2 = n[3].getType(check);
+      if (!indexRangeType1.isSubtypeOf(indexType))
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "eqrange lower index type does not match array index type");
+      }
+      if (!indexRangeType2.isSubtypeOf(indexType))
+      {
+        throw TypeCheckingExceptionPrivate(
+            n, "eqrange upper index type does not match array index type");
+      }
+      if (!indexType.isBitVector() && !indexType.isFloatingPoint()
+          && !indexType.isInteger() && !indexType.isReal())
+      {
+        throw TypeCheckingExceptionPrivate(
+            n,
+            "eqrange only supports bit-vectors, floating-points, integers, and "
+            "reals as index type");
+      }
+    }
+    return nodeManager->booleanType();
+  }
+}; /* struct ArrayEqRangeTypeRule */
+
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */