From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 22 Jul 2021 13:59:17 +0000 (-0500)
Subject: Miscellaneous changes in preparation for central equality engine (#6900)
X-Git-Tag: cvc5-1.0.0~1464
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d21afb82b4b2dec2e67c454cbc76cc5f5b00df36;p=cvc5.git

Miscellaneous changes in preparation for central equality engine (#6900)
---

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 42e317402..4ac74d76c 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -85,7 +85,7 @@ void TheorySetsPrivate::eqNotifyNewClass(TNode t)
 
 void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
 {
-  if (!d_state.isInConflict())
+  if (!d_state.isInConflict() && t1.getType().isSet())
   {
     Trace("sets-prop-debug")
         << "Merge " << t1 << " and " << t2 << "..." << std::endl;
diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp
index f2266c236..b020a3938 100644
--- a/src/theory/shared_solver.cpp
+++ b/src/theory/shared_solver.cpp
@@ -57,13 +57,17 @@ void SharedSolver::preRegister(TNode atom)
   // See term_registration_visitor.h for more details.
   if (d_logicInfo.isSharingEnabled())
   {
-    // register it with the shared terms database if sharing is enabled
-    preRegisterSharedInternal(atom);
     // Collect the shared terms in atom, as well as calling preregister on the
     // appropriate theories in atom.
     // This calls Theory::preRegisterTerm and Theory::addSharedTerm, possibly
     // multiple times.
     NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, atom);
+    // Register it with the shared terms database if sharing is enabled.
+    // Notice that this must come *after* the above call, since we must ensure
+    // that all subterms of atom have already been added to the central
+    // equality engine before atom is added. This avoids spurious notifications
+    // from the equality engine.
+    preRegisterSharedInternal(atom);
   }
   else
   {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index bf196273e..f98f1cb6c 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -899,7 +899,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
           Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
           Trace("dtview::conflict")
               << ":THEORY-CONFLICT: " << assertion << std::endl;
-          d_inConflict = true;
+          markInConflict();
         } else {
           return;
         }
@@ -954,7 +954,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo
             << endl;
         Trace("dtview::conflict")
             << ":THEORY-CONFLICT: " << assertion << std::endl;
-        d_inConflict = true;
+        markInConflict();
       }
     }
     return;