Remove arrays lazy rintro option (#4806)

This option has model soundness issues (#4771) and moreover is overall worse performance on SMT-LIB {QF_ABV QF_ABVFP QF_ABVFPLRA QF_ALIA QF_ANIA QF_AUFBV QF_AUFLIA QF_AUFNIA QF_AX}:

                           Configuration  #unsat      time    #sat      time #solved    #total
                         CVC4-072720_def    9428   9405.46   24932   16631.6     34360     35399
                       CVC4-072720_nalr1    9446   9536.41   24924   16146.3     34370     35399
where def = default, nalr1 = --no-arrays-lazy-rintro1.

Fixes #4771.

FYI @barrettcw

2 files changed, 9 insertions, 114 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index f008dc2a1..27e49d2ce 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -54,7 +54,6 @@ const bool d_solveWrite2 = false;
   // These are now options
   //const bool d_propagateLemmas = true;
   //bool d_useNonLinearOpt = true;
-  //bool d_lazyRIntro1 = true;
   //bool d_eagerIndexSplitting = false;
 
 TheoryArrays::TheoryArrays(context::Context* c,
@@ -697,26 +696,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     }
     Assert((d_isPreRegistered.insert(node), true));
 
-    if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) {
-      // Apply RIntro1 rule to any stores equal to store if not done already
-      const CTNodeList* stores = d_infoMap.getStores(store);
-      CTNodeList::const_iterator it = stores->begin();
-      if (it != stores->end()) {
-        NodeManager* nm = NodeManager::currentNM();
-        TNode s = *it;
-        if (!d_infoMap.rIntro1Applied(s)) {
-          d_infoMap.setRIntro1Applied(s);
-          Assert(s.getKind() == kind::STORE);
-          Node ni = nm->mkNode(kind::SELECT, s, s[1]);
-          if (ni != node) {
-            preRegisterTermInternal(ni);
-          }
-          d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, d_reasonRow1);
-          Assert(++it == stores->end());
-        }
-      }
-    }
-
     Assert(d_equalityEngine.getRepresentative(store) == store);
     d_infoMap.addIndex(store, node[1]);
 
@@ -772,19 +751,17 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
       Assert(d_mayEqualEqualityEngine.consistent());
     }
 
-    if (!options::arraysLazyRIntro1() || options::arraysWeakEquivalence()) {
-      TNode i = node[1];
-      TNode v = node[2];
-      NodeManager* nm = NodeManager::currentNM();
-      Node ni = nm->mkNode(kind::SELECT, node, i);
-      if (!d_equalityEngine.hasTerm(ni)) {
-        preRegisterTermInternal(ni);
-      }
-
-      // Apply RIntro1 Rule
-      d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1);
+    TNode i = node[1];
+    TNode v = node[2];
+    NodeManager* nm = NodeManager::currentNM();
+    Node ni = nm->mkNode(kind::SELECT, node, i);
+    if (!d_equalityEngine.hasTerm(ni)) {
+      preRegisterTermInternal(ni);
     }
 
+    // Apply RIntro1 Rule
+    d_equalityEngine.assertEquality(ni.eqNode(v), true, d_true, d_reasonRow1);
+
     d_infoMap.addStore(node, node);
     d_infoMap.addInStore(a, node);
     d_infoMap.setModelRep(node, node);
@@ -1662,82 +1639,6 @@ void TheoryArrays::setNonLinear(TNode a)
 
 }
 
-/*****
- * When two array equivalence classes are merged, we may need to apply RIntro1 to a store in one of the EC's
- * Here, we check the stores in a to see if any need RIntro1 applied
- * We apply RIntro1 whenever:
- * (a) a store becomes equal to another store
- * (b) a store becomes equal to any term t such that read(t,i) exists
- * (c) a store becomes equal to the root array of the store (i.e. store(store(...store(a,i,v)...)) = a)
- */
-void TheoryArrays::checkRIntro1(TNode a, TNode b)
-{
-  const CTNodeList* astores = d_infoMap.getStores(a);
-  // Apply RIntro1 if applicable
-  CTNodeList::const_iterator it = astores->begin();
-
-  if (it == astores->end()) {
-    // No stores in this equivalence class - return
-    return;
-  }
-
-  ++it;
-  if (it != astores->end()) {
-    // More than one store: should have already been applied
-    Assert(d_infoMap.rIntro1Applied(*it));
-    Assert(d_infoMap.rIntro1Applied(*(--it)));
-    return;
-  }
-
-  // Exactly one store - see if we need to apply RIntro1
-  --it;
-  TNode s = *it;
-  Assert(s.getKind() == kind::STORE);
-  if (d_infoMap.rIntro1Applied(s)) {
-    // RIntro1 already applied to s
-    return;
-  }
-
-  // Should be no reads from this EC
-  Assert(d_infoMap.getIndices(a)->begin() == d_infoMap.getIndices(a)->end());
-
-  bool apply = false;
-  if (d_infoMap.getStores(b)->size() > 0) {
-    // Case (a): two stores become equal
-    apply = true;
-  }
-  else {
-    const CTNodeList* i_b = d_infoMap.getIndices(b);
-    if (i_b->begin() != i_b->end()) {
-      // Case (b): there are reads from b
-      apply = true;
-    }
-    else {
-      // Get root array of s
-      TNode e1 = s[0];
-      while (e1.getKind() == kind::STORE) {
-        e1 = e1[0];
-      }
-      Assert(d_equalityEngine.hasTerm(e1));
-      Assert(d_equalityEngine.hasTerm(b));
-      if (d_equalityEngine.areEqual(e1, b)) {
-        apply = true;
-      }
-    }
-  }
-
-  if (apply) {
-    NodeManager* nm = NodeManager::currentNM();
-    d_infoMap.setRIntro1Applied(s);
-    Node ni = nm->mkNode(kind::SELECT, s, s[1]);
-    preRegisterTermInternal(ni);
-    d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true, d_reasonRow1);
-  }
-}
-
-
-
-
 void TheoryArrays::mergeArrays(TNode a, TNode b)
 {
   // Note: a is the new representative
@@ -1760,11 +1661,6 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
     Assert(d_equalityEngine.getRepresentative(b) == a);
     Trace("arrays-merge") << spaces(getSatContext()->getLevel()) << "Arrays::merge: (" << a << ", " << b << ")\n";
 
-    if (options::arraysLazyRIntro1() && !options::arraysWeakEquivalence()) {
-      checkRIntro1(a, b);
-      checkRIntro1(b, a);
-    }
-
     if (options::arraysOptimizeLinear() && !options::arraysWeakEquivalence()) {
       bool aNL = d_infoMap.isNonLinear(a);
       bool bNL = d_infoMap.isNonLinear(b);
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index a4416ab8c..54acf21a5 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -446,7 +446,6 @@ class TheoryArrays : public Theory {
   Node getSkolem(TNode ref, const std::string& name, const TypeNode& type, const std::string& comment, bool makeEqual = true);
   Node mkAnd(std::vector<TNode>& conjunctions, bool invert = false, unsigned startIndex = 0);
   void setNonLinear(TNode a);
-  void checkRIntro1(TNode a, TNode b);
   Node removeRepLoops(TNode a, TNode rep);
   Node expandStores(TNode s, std::vector<TNode>& assumptions, bool checkLoop = false, TNode a = TNode(), TNode b = TNode());
   void mergeArrays(TNode a, TNode b);