From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 28 Jul 2021 21:50:08 +0000 (-0500)
Subject: Minor changes to arrays in preparation for central equality engine (#6917)
X-Git-Tag: cvc5-1.0.0~1433
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=48a58687cd7a5b3d1e69153b2178ba535f1e6724;p=cvc5.git

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 8fa7e0fd3..7a764feba 100644
--- 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 c85b382e4..772fc1b79 100644
--- 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()) {