arrays: Use EnvObj::rewrite and EnvObj::options. (#7217)

This does not yet clean up the usage of Rewriter::rewrite in the arrays
type enumerator yet. Will be cleaned up in a follow-up PR.

3 files changed, 81 insertions, 54 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 774c5db3f..cf31f0cb6 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -29,7 +29,6 @@
 #include "theory/arrays/skolem_cache.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/decision_manager.h"
-#include "theory/rewriter.h"
 #include "theory/theory_model.h"
 #include "theory/trust_substitutions.h"
 #include "theory/valuation.h"
@@ -80,7 +79,7 @@ TheoryArrays::TheoryArrays(Env& env,
           name + "number of setModelVal conflicts")),
       d_ppEqualityEngine(userContext(), name + "pp", true),
       d_ppFacts(userContext()),
-      d_rewriter(d_pnm),
+      d_rewriter(env.getRewriter(), d_pnm),
       d_state(env, valuation),
       d_im(env, *this, d_state, d_pnm),
       d_literalsToPropagate(context()),
@@ -172,8 +171,8 @@ bool TheoryArrays::ppDisequal(TNode a, TNode b) {
   bool termsExist = d_ppEqualityEngine.hasTerm(a) && d_ppEqualityEngine.hasTerm(b);
   Assert(!termsExist || !a.isConst() || !b.isConst() || a == b
          || d_ppEqualityEngine.areDisequal(a, b, false));
-  return ((termsExist && d_ppEqualityEngine.areDisequal(a, b, false)) ||
-          Rewriter::rewrite(a.eqNode(b)) == d_false);
+  return ((termsExist && d_ppEqualityEngine.areDisequal(a, b, false))
+          || rewrite(a.eqNode(b)) == d_false);
 }
 
 
@@ -701,7 +700,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
 
       // Record read in sharing data structure
       TNode index = d_equalityEngine->getRepresentative(node[1]);
-      if (!options::arraysWeakEquivalence() && index.isConst())
+      if (!options().arrays.arraysWeakEquivalence && index.isConst())
       {
         CTNodeList* temp;
         CNodeNListMap::iterator it = d_constReads.find(index);
@@ -767,7 +766,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
       d_infoMap.setModelRep(node, node);
 
       // Add-Store for Weak Equivalence
-      if (options::arraysWeakEquivalence())
+      if (options().arrays.arraysWeakEquivalence)
       {
         Assert(weakEquivGetRep(node[0]) == weakEquivGetRep(a));
         Assert(weakEquivGetRep(node) == node);
@@ -1223,8 +1222,11 @@ Node TheoryArrays::getSkolem(TNode ref)
 
 void TheoryArrays::postCheck(Effort level)
 {
-  if ((options::arraysEagerLemmas() || fullEffort(level))
-      && !d_state.isInConflict() && options::arraysWeakEquivalence())
+  bool eagerLemmas = options().arrays.arraysEagerLemmas;
+  bool weakEquiv = options().arrays.arraysWeakEquivalence;
+
+  if ((eagerLemmas || fullEffort(level)) && !d_state.isInConflict()
+      && weakEquiv)
   {
     // Replay all array merges to update weak equivalence data structures
     context::CDList<Node>::iterator it = d_arrayMerges.begin(), iend = d_arrayMerges.end();
@@ -1287,9 +1289,9 @@ void TheoryArrays::postCheck(Effort level)
         if (weakEquivGetRepIndex(r[0], r[1]) == weakEquivGetRepIndex(r2[0], r[1])) {
           // add lemma: r[1] = r2[1] /\ cond(r[0],r2[0]) => r = r2
           vector<TNode> conjunctions;
-          Assert(d_equalityEngine->areEqual(r, Rewriter::rewrite(r)));
-          Assert(d_equalityEngine->areEqual(r2, Rewriter::rewrite(r2)));
-          Node lemma = Rewriter::rewrite(r).eqNode(Rewriter::rewrite(r2)).negate();
+          Assert(d_equalityEngine->areEqual(r, rewrite(r)));
+          Assert(d_equalityEngine->areEqual(r2, rewrite(r2)));
+          Node lemma = rewrite(r).eqNode(rewrite(r2)).negate();
           d_permRef.push_back(lemma);
           conjunctions.push_back(lemma);
           if (r[1] != r2[1]) {
@@ -1314,8 +1316,8 @@ void TheoryArrays::postCheck(Effort level)
     d_readTableContext->pop();
   }
 
-  if (!options::arraysEagerLemmas() && fullEffort(level)
-      && !d_state.isInConflict() && !options::arraysWeakEquivalence())
+  if (!eagerLemmas && fullEffort(level) && !d_state.isInConflict()
+      && !weakEquiv)
   {
     // generate the lemmas on the worklist
     Trace("arrays-lem")<< "Arrays::discharging lemmas. Number of queued lemmas: " << d_RowQueue.size() << "\n";
@@ -1378,7 +1380,7 @@ void TheoryArrays::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
       Node eq = ak.eqNode(bk);
       Node lemma = fact[0].orNode(eq.notNode());
 
-      if (options::arraysPropagate() > 0 && d_equalityEngine->hasTerm(ak)
+      if (options().arrays.arraysPropagate > 0 && d_equalityEngine->hasTerm(ak)
           && d_equalityEngine->hasTerm(bk))
       {
         // Propagate witness disequality - might produce a conflict
@@ -1465,7 +1467,7 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions, bool invert, unsigned
 
 void TheoryArrays::setNonLinear(TNode a)
 {
-  if (options::arraysWeakEquivalence()) return;
+  if (options().arrays.arraysWeakEquivalence) return;
   if (d_infoMap.isNonLinear(a)) return;
 
   Trace("arrays") << spaces(context()->getLevel()) << "Arrays::setNonLinear ("
@@ -1519,6 +1521,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
   }
 
   d_mergeInProgress = true;
+  bool optLinear = options().arrays.arraysOptimizeLinear;
+  bool weakEquiv = options().arrays.arraysWeakEquivalence;
 
   Node n;
   while (true) {
@@ -1530,7 +1534,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
     Trace("arrays-merge") << spaces(context()->getLevel()) << "Arrays::merge: ("
                           << a << ", " << b << ")\n";
 
-    if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) {
+    if (optLinear && !weakEquiv)
+    {
       bool aNL = d_infoMap.isNonLinear(a);
       bool bNL = d_infoMap.isNonLinear(b);
       if (aNL) {
@@ -1606,7 +1611,8 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
     // merge info adds the list of the 2nd argument to the first
     d_infoMap.mergeInfo(a, b);
 
-    if (options::arraysWeakEquivalence()) {
+    if (weakEquiv)
+    {
       d_arrayMerges.push_back(a.eqNode(b));
     }
 
@@ -1625,9 +1631,10 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
   d_mergeInProgress = false;
 }
 
+void TheoryArrays::checkStore(TNode a)
+{
+  if (options().arrays.arraysWeakEquivalence) return;
 
-void TheoryArrays::checkStore(TNode a) {
-  if (options::arraysWeakEquivalence()) return;
   Trace("arrays-cri")<<"Arrays::checkStore "<<a<<"\n";
 
   if(Trace.isOn("arrays-cri")) {
@@ -1640,7 +1647,8 @@ void TheoryArrays::checkStore(TNode a) {
 
   TNode brep = d_equalityEngine->getRepresentative(b);
 
-  if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(brep)) {
+  if (!options().arrays.arraysOptimizeLinear || d_infoMap.isNonLinear(brep))
+  {
     const CTNodeList* js = d_infoMap.getIndices(brep);
     size_t it = 0;
     RowLemmaType lem;
@@ -1656,10 +1664,10 @@ void TheoryArrays::checkStore(TNode a) {
   }
 }
 
-
 void TheoryArrays::checkRowForIndex(TNode i, TNode a)
 {
-  if (options::arraysWeakEquivalence()) return;
+  if (options().arrays.arraysWeakEquivalence) return;
+
   Trace("arrays-cri")<<"Arrays::checkRowForIndex "<<a<<"\n";
   Trace("arrays-cri")<<"                   index "<<i<<"\n";
 
@@ -1703,7 +1711,8 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
     queueRowLemma(lem);
   }
 
-  if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(a)) {
+  if (!options().arrays.arraysOptimizeLinear || d_infoMap.isNonLinear(a))
+  {
     it = 0;
     for(; it < instores->size(); ++it) {
       TNode instore = (*instores)[it];
@@ -1724,7 +1733,8 @@ void TheoryArrays::checkRowForIndex(TNode i, TNode a)
 // look for new ROW lemmas
 void TheoryArrays::checkRowLemmas(TNode a, TNode b)
 {
-  if (options::arraysWeakEquivalence()) return;
+  if (options().arrays.arraysWeakEquivalence) return;
+
   Trace("arrays-crl")<<"Arrays::checkLemmas begin \n"<<a<<"\n";
   if(Trace.isOn("arrays-crl"))
     d_infoMap.getInfo(a)->print();
@@ -1768,7 +1778,8 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
     }
   }
 
-  if (!options::arraysOptimizeLinear() || d_infoMap.isNonLinear(b)) {
+  if (!options().arrays.arraysOptimizeLinear || d_infoMap.isNonLinear(b))
+  {
     for(it = 0 ; it < i_a->size(); ++it ) {
       TNode i = (*i_a)[it];
       its = 0;
@@ -1790,8 +1801,9 @@ void TheoryArrays::checkRowLemmas(TNode a, TNode b)
 
 void TheoryArrays::propagateRowLemma(RowLemmaType lem)
 {
-  Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. options::arraysPropagate() = "
-                     << options::arraysPropagate() << std::endl;
+  Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. "
+                        "options::arraysPropagate() = "
+                     << options().arrays.arraysPropagate << std::endl;
 
   TNode a, b, i, j;
   std::tie(a, b, i, j) = lem;
@@ -1812,7 +1824,7 @@ void TheoryArrays::propagateRowLemma(RowLemmaType lem)
   bool bothExist = ajExists && bjExists;
 
   // If propagating, check propagations
-  int prop = options::arraysPropagate();
+  int64_t prop = options().arrays.arraysPropagate;
   if (prop > 0) {
     if (d_equalityEngine->areDisequal(i, j, true) && (bothExist || prop > 1))
     {
@@ -1877,13 +1889,14 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   bool bothExist = ajExists && bjExists;
 
   // If propagating, check propagations
-  int prop = options::arraysPropagate();
+  int64_t prop = options().arrays.arraysPropagate;
+
   if (prop > 0) {
     propagateRowLemma(lem);
   }
 
   // Prefer equality between indexes so as not to introduce new read terms
-  if (options::arraysEagerIndexSplitting() && !bothExist
+  if (options().arrays.arraysEagerIndexSplitting && !bothExist
       && !d_equalityEngine->areDisequal(i, j, false))
   {
     Node i_eq_j;
@@ -1897,10 +1910,10 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
   // TODO: maybe add triggers here
 
-  if (options::arraysEagerLemmas() || bothExist)
+  if (options().arrays.arraysEagerLemmas || bothExist)
   {
     // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
-    Node aj2 = Rewriter::rewrite(aj);
+    Node aj2 = rewrite(aj);
     if (aj != aj2) {
       if (!ajExists) {
         preRegisterTermInternal(aj);
@@ -1915,7 +1928,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
                            d_true,
                            PfRule::MACRO_SR_PRED_INTRO);
     }
-    Node bj2 = Rewriter::rewrite(bj);
+    Node bj2 = rewrite(bj);
     if (bj != bj2) {
       if (!bjExists) {
         preRegisterTermInternal(bj);
@@ -1936,7 +1949,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
     // construct lemma
     Node eq1 = aj2.eqNode(bj2);
-    Node eq1_r = Rewriter::rewrite(eq1);
+    Node eq1_r = rewrite(eq1);
     if (eq1_r == d_true) {
       if (!d_equalityEngine->hasTerm(aj2))
       {
@@ -1955,7 +1968,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
     }
 
     Node eq2 = i.eqNode(j);
-    Node eq2_r = Rewriter::rewrite(eq2);
+    Node eq2_r = rewrite(eq2);
     if (eq2_r == d_true) {
       d_im.assertInference(eq2,
                            true,
@@ -1992,9 +2005,11 @@ Node TheoryArrays::getNextDecisionRequest()
 
 bool TheoryArrays::dischargeLemmas()
 {
+  bool reduceSharing = options().arrays.arraysReduceSharing;
   bool lemmasAdded = false;
-  size_t sz = d_RowQueue.size();
-  for (unsigned count = 0; count < sz; ++count) {
+
+  for (size_t count = 0, sz = d_RowQueue.size(); count < sz; ++count)
+  {
     RowLemmaType l = d_RowQueue.front();
     d_RowQueue.pop();
     if (d_RowAlreadyAdded.contains(l)) {
@@ -2021,7 +2036,7 @@ bool TheoryArrays::dischargeLemmas()
       continue;
     }
 
-    int prop = options::arraysPropagate();
+    int64_t prop = options().arrays.arraysPropagate;
     if (prop > 0) {
       propagateRowLemma(l);
       if (d_state.isInConflict())
@@ -2031,7 +2046,7 @@ bool TheoryArrays::dischargeLemmas()
     }
 
     // Make sure that any terms introduced by rewriting are appropriately stored in the equality database
-    Node aj2 = Rewriter::rewrite(aj);
+    Node aj2 = rewrite(aj);
     if (aj != aj2) {
       if (!ajExists) {
         preRegisterTermInternal(aj);
@@ -2046,7 +2061,7 @@ bool TheoryArrays::dischargeLemmas()
                            d_true,
                            PfRule::MACRO_SR_PRED_INTRO);
     }
-    Node bj2 = Rewriter::rewrite(bj);
+    Node bj2 = rewrite(bj);
     if (bj != bj2) {
       if (!bjExists) {
         preRegisterTermInternal(bj);
@@ -2067,7 +2082,7 @@ bool TheoryArrays::dischargeLemmas()
 
     // construct lemma
     Node eq1 = aj2.eqNode(bj2);
-    Node eq1_r = Rewriter::rewrite(eq1);
+    Node eq1_r = rewrite(eq1);
     if (eq1_r == d_true) {
       if (!d_equalityEngine->hasTerm(aj2))
       {
@@ -2086,7 +2101,7 @@ bool TheoryArrays::dischargeLemmas()
     }
 
     Node eq2 = i.eqNode(j);
-    Node eq2_r = Rewriter::rewrite(eq2);
+    Node eq2_r = rewrite(eq2);
     if (eq2_r == d_true) {
       d_im.assertInference(eq2,
                            true,
@@ -2105,7 +2120,8 @@ bool TheoryArrays::dischargeLemmas()
         aj.eqNode(bj), InferenceId::ARRAYS_READ_OVER_WRITE, eq2.notNode(), PfRule::ARRAYS_READ_OVER_WRITE);
     ++d_numRow;
     lemmasAdded = true;
-    if (options::arraysReduceSharing()) {
+    if (reduceSharing)
+    {
       return true;
     }
   }
diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp
index dd7a56d33..4f11e323e 100644
--- a/src/theory/arrays/theory_arrays_rewriter.cpp
+++ b/src/theory/arrays/theory_arrays_rewriter.cpp
@@ -30,9 +30,13 @@ namespace theory {
 namespace arrays {
 
 namespace attr {
-  struct ArrayConstantMostFrequentValueTag { };
-  struct ArrayConstantMostFrequentValueCountTag { };
-  }  // namespace attr
+struct ArrayConstantMostFrequentValueTag
+{
+};
+struct ArrayConstantMostFrequentValueCountTag
+{
+};
+}  // namespace attr
 
 typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
 typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
@@ -51,8 +55,9 @@ void setMostFrequentValueCount(TNode store, uint64_t count) {
   return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
 }
 
-TheoryArraysRewriter::TheoryArraysRewriter(ProofNodeManager* pnm)
-    : d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
+TheoryArraysRewriter::TheoryArraysRewriter(Rewriter* rewriter,
+                                           ProofNodeManager* pnm)
+    : d_rewriter(rewriter), d_epg(pnm ? new EagerProofGenerator(pnm) : nullptr)
 {
 }
 
@@ -345,7 +350,7 @@ RewriteResponse TheoryArraysRewriter::postRewrite(TNode node)
         }
         else
         {
-          n = Rewriter::rewrite(mkEqNode(store[1], index));
+          n = d_rewriter->rewrite(mkEqNode(store[1], index));
           if (n.getKind() != kind::CONST_BOOLEAN)
           {
             break;
@@ -417,7 +422,7 @@ RewriteResponse TheoryArraysRewriter::postRewrite(TNode node)
         }
         else
         {
-          Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
+          Node eqRewritten = d_rewriter->rewrite(mkEqNode(store[1], index));
           if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
           {
             Trace("arrays-postrewrite")
@@ -457,7 +462,7 @@ RewriteResponse TheoryArraysRewriter::postRewrite(TNode node)
             }
             else
             {
-              n = Rewriter::rewrite(mkEqNode(store[1], index));
+              n = d_rewriter->rewrite(mkEqNode(store[1], index));
               if (n.getKind() != kind::CONST_BOOLEAN)
               {
                 break;
@@ -557,7 +562,7 @@ RewriteResponse TheoryArraysRewriter::preRewrite(TNode node)
         }
         else
         {
-          n = Rewriter::rewrite(mkEqNode(store[1], index));
+          n = d_rewriter->rewrite(mkEqNode(store[1], index));
           if (n.getKind() != kind::CONST_BOOLEAN)
           {
             break;
@@ -620,7 +625,7 @@ RewriteResponse TheoryArraysRewriter::preRewrite(TNode node)
         }
         else
         {
-          Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
+          Node eqRewritten = d_rewriter->rewrite(mkEqNode(store[1], index));
           if (eqRewritten.getKind() != kind::CONST_BOOLEAN)
           {
             break;
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 95a19004e..2c2da66a8 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -33,6 +33,9 @@ namespace cvc5 {
 class EagerProofGenerator;
 
 namespace theory {
+
+class Rewriter;
+
 namespace arrays {
 
 Node getMostFrequentValue(TNode store);
@@ -47,7 +50,7 @@ static inline Node mkEqNode(Node a, Node b) {
 class TheoryArraysRewriter : public TheoryRewriter
 {
  public:
-  TheoryArraysRewriter(ProofNodeManager* pnm);
+  TheoryArraysRewriter(Rewriter* rewriter, ProofNodeManager* pnm);
 
   /** Normalize a constant whose index type has cardinality indexCard */
   static Node normalizeConstant(TNode node, Cardinality indexCard);
@@ -74,6 +77,9 @@ class TheoryArraysRewriter : public TheoryRewriter
    */
   static Node normalizeConstant(TNode node);
 
+  /** The associated rewriter. */
+  Rewriter* d_rewriter;
+
   std::unique_ptr<EagerProofGenerator> d_epg;
 }; /* class TheoryArraysRewriter */