Minor changes to arrays in preparation for central equality engine (#6917)

Makes arrays more robust to the order in which terms can be added to the equality engine vs. when they are preregistered.

We should probably performance test this.

FYI @barrettcw

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 8fa7e0fd38cd6e30b5299b3022cfc4c6f293c81a..7a764feba503bf11494833ebc606e16e6055d5d0 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -646,7 +646,9 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
   {
     return;
   }
-  Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
+  Debug("arrays") << spaces(getSatContext()->getLevel())
+                  << "TheoryArrays::preRegisterTerm(" << node << ")"
+                  << std::endl;
   Kind nk = node.getKind();
   if (nk == kind::EQUAL)
   {
@@ -655,13 +657,6 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     d_equalityEngine->addTriggerPredicate(node);
     return;
   }
-  else if (d_equalityEngine->hasTerm(node))
-  {
-    // Invariant: array terms should be preregistered before being added to the equality engine
-    Assert(nk != kind::SELECT
-           || d_isPreRegistered.find(node) != d_isPreRegistered.end());
-    return;
-  }
   // add to equality engine and the may equality engine
   TypeNode nodeType = node.getType();
   if (nodeType.isArray())
@@ -676,6 +671,15 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     }
     d_mayEqualEqualityEngine.addTerm(node);
   }
+  if (d_equalityEngine->hasTerm(node))
+  {
+    // Notice that array terms may be added to its equality engine before
+    // being preregistered in the central equality engine architecture.
+    // Prior to this, an assertion in this case was:
+    // Assert(nk != kind::SELECT
+    //         || d_isPreRegistered.find(node) != d_isPreRegistered.end());
+    return;
+  }
   d_equalityEngine->addTerm(node);
 
   switch (node.getKind())

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index c85b382e4d259c4672b8401f8786d4e4393ce499..772fc1b790b1e6823fe7e913c1fed17cb53d7227 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -334,7 +334,10 @@ class TheoryArrays : public Theory {
       d_arrays.conflict(t1, t2);
     }
 
-    void eqNotifyNewClass(TNode t) override {}
+    void eqNotifyNewClass(TNode t) override
+    {
+      d_arrays.preRegisterTermInternal(t);
+    }
     void eqNotifyMerge(TNode t1, TNode t2) override
     {
       if (t1.getType().isArray()) {