From d21afb82b4b2dec2e67c454cbc76cc5f5b00df36 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 22 Jul 2021 08:59:17 -0500 Subject: [PATCH] Miscellaneous changes in preparation for central equality engine (#6900) --- src/theory/sets/theory_sets_private.cpp | 2 +- src/theory/shared_solver.cpp | 8 ++++++-- src/theory/theory_engine.cpp | 4 ++-- 3 files changed, 9 insertions(+), 5 deletions(-) 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::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; -- 2.30.2