proof: Add eqrange expansion rule. (#6936)

Adds proof support for the eqrange operator.

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

8 files changed, 119 insertions, 50 deletions

diff --git a/src/proof/proof_rule.cpp b/src/proof/proof_rule.cpp
index 3991305ca..7e1cdf8d3 100644
--- a/src/proof/proof_rule.cpp
+++ b/src/proof/proof_rule.cpp
@@ -120,6 +120,7 @@ const char* toString(PfRule id)
     case PfRule::ARRAYS_READ_OVER_WRITE_1: return "ARRAYS_READ_OVER_WRITE_1";
     case PfRule::ARRAYS_EXT: return "ARRAYS_EXT";
     case PfRule::ARRAYS_TRUST: return "ARRAYS_TRUST";
+    case PfRule::ARRAYS_EQ_RANGE_EXPAND: return "ARRAYS_EQ_RANGE_EXPAND";
     //================================================= Bit-Vector rules
     case PfRule::BV_BITBLAST: return "BV_BITBLAST";
     case PfRule::BV_BITBLAST_STEP: return "BV_BITBLAST_STEP";
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index 173e4df9a..78e773bdc 100644
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -713,6 +713,15 @@ enum class PfRule : uint32_t
   // Conclusion: (not (= (select a k) (select b k)))
   // where k is arrays::SkolemCache::getExtIndexSkolem((not (= a b))).
   ARRAYS_EXT,
+  // ======== EQ_RANGE expansion
+  // Children: none
+  // Arguments: ((eqrange a b i j))
+  // ----------------------------------------
+  // Conclusion: (=
+  //              (eqrange a b i j)
+  //              (forall ((x T))
+  //               (=> (and (<= i x) (<= x j)) (= (select a x) (select b x)))))
+  ARRAYS_EQ_RANGE_EXPAND,
   // ======== Array Trust
   // Children: (P1 ... Pn)
   // Arguments: (F)
diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp
index f8c5b2669..6d546d746 100644
--- a/src/theory/arrays/proof_checker.cpp
+++ b/src/theory/arrays/proof_checker.cpp
@@ -14,8 +14,10 @@
  */
 
 #include "theory/arrays/proof_checker.h"
+
 #include "expr/skolem_manager.h"
 #include "theory/arrays/skolem_cache.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/rewriter.h"
 
 namespace cvc5 {
@@ -28,6 +30,7 @@ void ArraysProofRuleChecker::registerTo(ProofChecker* pc)
   pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_CONTRA, this);
   pc->registerChecker(PfRule::ARRAYS_READ_OVER_WRITE_1, this);
   pc->registerChecker(PfRule::ARRAYS_EXT, this);
+  pc->registerChecker(PfRule::ARRAYS_EQ_RANGE_EXPAND, this);
   // trusted rules
   pc->registerTrustedChecker(PfRule::ARRAYS_TRUST, this, 2);
 }
@@ -103,6 +106,11 @@ Node ArraysProofRuleChecker::checkInternal(PfRule id,
     Node bs = nm->mkNode(kind::SELECT, b, k);
     return as.eqNode(bs).notNode();
   }
+  if (id == PfRule::ARRAYS_EQ_RANGE_EXPAND)
+  {
+    Node expandedEqRange = TheoryArraysRewriter::expandEqRange(args[0]);
+    return args[0].eqNode(expandedEqRange);
+  }
   if (id == PfRule::ARRAYS_TRUST)
   {
     // "trusted" rules
diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp
index 19ab1aaae..7cf192b7f 100644
--- a/src/theory/arrays/skolem_cache.cpp
+++ b/src/theory/arrays/skolem_cache.cpp
@@ -35,6 +35,14 @@ struct ExtIndexVarAttributeId
 };
 typedef expr::Attribute<ExtIndexVarAttributeId, Node> ExtIndexVarAttribute;
 
+/**
+ * A bound variable corresponding to the index used in the eqrange expansion.
+ */
+struct EqRangeVarAttributeId
+{
+};
+typedef expr::Attribute<EqRangeVarAttributeId, Node> EqRangeVarAttribute;
+
 SkolemCache::SkolemCache() {}
 
 Node SkolemCache::getExtIndexSkolem(Node deq)
@@ -66,6 +74,13 @@ Node SkolemCache::getExtIndexSkolem(Node deq)
       "an extensional lemma index variable from the theory of arrays");
 }
 
+Node SkolemCache::getEqRangeVar(TNode eqr)
+{
+  Assert(eqr.getKind() == kind::EQ_RANGE);
+  BoundVarManager* bvm = NodeManager::currentNM()->getBoundVarManager();
+  return bvm->mkBoundVar<EqRangeVarAttribute>(eqr, eqr[2].getType());
+}
+
 Node SkolemCache::getExtIndexVar(Node deq)
 {
   Node a = deq[0][0];
diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h
index 12578c01f..17a5c6975 100644
--- a/src/theory/arrays/skolem_cache.h
+++ b/src/theory/arrays/skolem_cache.h
@@ -43,6 +43,13 @@ class SkolemCache
    */
   static Node getExtIndexSkolem(Node deq);
 
+  /**
+   * Get the bound variable for given EQ_RANGE operator. This bound variable
+   * is unique for `eqr`. Calling this method will always return the same bound
+   * variable over the lifetime of `eqr`.
+   */
+  static Node getEqRangeVar(TNode eqr);
+
  private:
   /**
    * Get the bound variable x of the witness term above for disequality deq
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index be8e1a08e..8fa7e0fd3 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -85,6 +85,7 @@ TheoryArrays::TheoryArrays(context::Context* c,
           name + "number of setModelVal conflicts")),
       d_ppEqualityEngine(u, name + "pp", true),
       d_ppFacts(u),
+      d_rewriter(pnm),
       d_state(c, u, valuation),
       d_im(*this, d_state, pnm),
       d_literalsToPropagate(c),
diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp
index 1072ffaf4..dd7a56d33 100644
--- a/src/theory/arrays/theory_arrays_rewriter.cpp
+++ b/src/theory/arrays/theory_arrays_rewriter.cpp
@@ -20,6 +20,9 @@
 
 #include "expr/array_store_all.h"
 #include "expr/attribute.h"
+#include "proof/conv_proof_generator.h"
+#include "proof/eager_proof_generator.h"
+#include "theory/arrays/skolem_cache.h"
 #include "util/cardinality.h"
 
 namespace cvc5 {
@@ -48,6 +51,11 @@ void setMostFrequentValueCount(TNode store, uint64_t count) {
   return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
 }
 
+TheoryArraysRewriter::TheoryArraysRewriter(ProofNodeManager* pnm)
+    : d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
+{
+}
+
 Node TheoryArraysRewriter::normalizeConstant(TNode node)
 {
   return normalizeConstant(node, node[1].getType().getCardinality());
@@ -271,6 +279,48 @@ Node TheoryArraysRewriter::normalizeConstant(TNode node, Cardinality indexCard)
   return n;
 }
 
+Node TheoryArraysRewriter::expandEqRange(TNode node)
+{
+  Assert(node.getKind() == kind::EQ_RANGE);
+
+  NodeManager* nm = NodeManager::currentNM();
+  TNode a = node[0];
+  TNode b = node[1];
+  TNode i = node[2];
+  TNode j = node[3];
+  Node k = SkolemCache::getEqRangeVar(node);
+  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 "
+                    << node.getKind();
+  }
+
+  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);
+}
+
 RewriteResponse TheoryArraysRewriter::postRewrite(TNode node)
 {
   Trace("arrays-postrewrite")
@@ -610,57 +660,22 @@ RewriteResponse TheoryArraysRewriter::preRewrite(TNode node)
 
 TrustNode TheoryArraysRewriter::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())
+    Node expandedEqRange = expandEqRange(node);
+    if (d_epg)
     {
-      kle = kind::FLOATINGPOINT_LEQ;
+      TrustNode tn = d_epg->mkTrustNode(node.eqNode(expandedEqRange),
+                                        PfRule::ARRAYS_EQ_RANGE_EXPAND,
+                                        {},
+                                        {node});
+      return TrustNode::mkTrustRewrite(node, expandedEqRange, d_epg.get());
     }
-    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);
-    Node ret = nm->mkNode(kind::FORALL, bvl, implies);
-    return TrustNode::mkTrustRewrite(node, ret, nullptr);
+    return TrustNode::mkTrustRewrite(node, expandedEqRange, nullptr);
   }
+
   return TrustNode::null();
 }
 
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 498266ce3..95a19004e 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -29,6 +29,9 @@
 #include "theory/type_enumerator.h"
 
 namespace cvc5 {
+
+class EagerProofGenerator;
+
 namespace theory {
 namespace arrays {
 
@@ -43,16 +46,18 @@ static inline Node mkEqNode(Node a, Node b) {
 
 class TheoryArraysRewriter : public TheoryRewriter
 {
-  /**
-   * Puts array constant node into normal form. This is so that array constants
-   * that are distinct nodes are semantically disequal.
-   */
-  static Node normalizeConstant(TNode node);
-
  public:
+  TheoryArraysRewriter(ProofNodeManager* pnm);
+
   /** Normalize a constant whose index type has cardinality indexCard */
   static Node normalizeConstant(TNode node, Cardinality indexCard);
 
+  /* Expands the eqrange predicate (eqrange a b i j) to the quantified formula
+   * (forall ((x T))
+   *  (=> (and (<= i x) (<= x j)) (= (select a x) (select b x)))).
+   */
+  static Node expandEqRange(TNode node);
+
   RewriteResponse postRewrite(TNode node) override;
 
   RewriteResponse preRewrite(TNode node) override;
@@ -62,6 +67,14 @@ class TheoryArraysRewriter : public TheoryRewriter
   static inline void init() {}
   static inline void shutdown() {}
 
+ private:
+  /**
+   * Puts array constant node into normal form. This is so that array constants
+   * that are distinct nodes are semantically disequal.
+   */
+  static Node normalizeConstant(TNode node);
+
+  std::unique_ptr<EagerProofGenerator> d_epg;
 }; /* class TheoryArraysRewriter */
 
 }  // namespace arrays