From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 21 Aug 2020 22:53:46 +0000 (-0500)
Subject: Limit trigger terms to shared terms in arrays (#4932)
X-Git-Tag: cvc5-1.0.0~2966
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9ea213066b989a8154b1ebd40ebea3bc7e18c42d;p=cvc5.git

Limit trigger terms to shared terms in arrays (#4932)

There is a non-standard use of trigger terms in the array theory via `EqualityEngine::addTriggerTerm`.

Trigger terms are only supposed to be shared terms, and are added to the equality engine for the sake of propagating equalities between shared terms.  The array theory does two non-standard things:
(1) it registers (possibly) non-shared terms as triggers in its `preRegisterInternal` method,
(2) it filters propagations between anything except non-shared arrays in its `eqNotifyTriggerTermEquality` method.

The latter is only necessary because of the former.  It is unnecessary to do *either* of these things. Instead, the array theory should simply add the terms to the equality engine (as non-triggers) during preRegisterInternal.  Note that it additionally correctly adds trigger terms in its `notifySharedTerm` method.

With this commit, the array theory uses the equality engine (wrt propagation) in a standard way.
---

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index d659aff11..34c4fd156 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -721,7 +721,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     if (node.getType().isArray())
     {
       d_mayEqualEqualityEngine.addTerm(node);
-      d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
+      d_equalityEngine->addTerm(node);
     }
     else
     {
@@ -765,7 +765,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     {
       break;
     }
-    d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
+    d_equalityEngine->addTerm(node);
 
     TNode a = d_equalityEngine->getRepresentative(node[0]);
 
@@ -828,7 +828,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     d_infoMap.setConstArr(node, node);
     d_mayEqualEqualityEngine.addTerm(node);
     Assert(d_mayEqualEqualityEngine.getRepresentative(node) == node);
-    d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
+    d_equalityEngine->addTerm(node);
     d_defValues[node] = defaultValue;
     break;
   }
@@ -837,7 +837,7 @@ void TheoryArrays::preRegisterTermInternal(TNode node)
     if (node.getType().isArray()) {
       // The may equal needs the node
       d_mayEqualEqualityEngine.addTerm(node);
-      d_equalityEngine->addTriggerTerm(node, THEORY_ARRAYS);
+      d_equalityEngine->addTerm(node);
       Assert(d_equalityEngine->getSize(node) == 1);
     }
     else {
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 24ebb4916..a1fa19631 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -317,22 +317,10 @@ class TheoryArrays : public Theory {
     {
       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
-        if (t1.getType().isArray()) {
-          if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
-            return true;
-          }
-        }
         // Propagate equality between shared terms
         return d_arrays.propagateLit(t1.eqNode(t2));
-      } else {
-        if (t1.getType().isArray()) {
-          if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
-            return true;
-          }
-        }
-        return d_arrays.propagateLit(t1.eqNode(t2).notNode());
       }
-      return true;
+      return d_arrays.propagateLit(t1.eqNode(t2).notNode());
     }
 
     void eqNotifyConstantTermMerge(TNode t1, TNode t2) override