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 42e31740201211ac74438815e5ff1ae1961ad042..4ac74d76c9201629c6172fe9fe118017b02d6270 100644 (file)
--- 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 f2266c23696107b9adef8166f4c28d5c776d5cbf..b020a39386cff8fa5077e0fef236c176be55cf45 100644 (file)
--- 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 bf196273e5242ff74b3d2df5547579a5c93c7288..f98f1cb6cc4fdae6901f7da518e51788db593119 100644 (file)
--- 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;