From 1fe9c2efe36b126c70097b0f83db5654e0abcabe Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 26 Sep 2020 10:07:42 -0500 Subject: [PATCH] Connect the shared solver to theory engine (#5103) This makes SharedSolver the main communication point for TheoryEngine during solving for combination-related solving tasks. This class is a generalization of SharedTermsDatabase, and in the distributed architecture is a wrapper around shared terms database. It has 5 callbacks in theory engine: for preregistration, preNotifyFact (which calls addSharedTerms on theories), assertSharedEquality, explain, getEqualityStatus. This PR has no intended behavior changes. FYI @barrettcw --- src/theory/combination_engine.cpp | 11 +++- src/theory/combination_engine.h | 11 ++++ src/theory/ee_manager.cpp | 5 +- src/theory/ee_manager.h | 11 +++- src/theory/ee_manager_distributed.cpp | 6 ++- src/theory/ee_manager_distributed.h | 2 +- src/theory/theory_engine.cpp | 77 +++++++-------------------- src/theory/theory_engine.h | 11 +--- 8 files changed, 62 insertions(+), 72 deletions(-) diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp index d972a4d8e..32af15054 100644 --- a/src/theory/combination_engine.cpp +++ b/src/theory/combination_engine.cpp @@ -18,6 +18,7 @@ #include "theory/care_graph.h" #include "theory/ee_manager_distributed.h" #include "theory/model_manager_distributed.h" +#include "theory/shared_solver_distributed.h" #include "theory/theory_engine.h" namespace CVC4 { @@ -31,6 +32,7 @@ CombinationEngine::CombinationEngine(TheoryEngine& te, d_paraTheories(paraTheories), d_eemanager(nullptr), d_mmanager(nullptr), + d_sharedSolver(nullptr), d_cmbsPg(pnm ? new EagerProofGenerator(pnm, te.getUserContext()) : nullptr) { @@ -43,8 +45,11 @@ void CombinationEngine::finishInit() // create the equality engine, model manager, and shared solver if (options::eeMode() == options::EqEngineMode::DISTRIBUTED) { + // use the distributed shared solver + d_sharedSolver.reset(new SharedSolverDistributed(d_te)); // make the distributed equality engine manager - d_eemanager.reset(new EqEngineManagerDistributed(d_te)); + d_eemanager.reset( + new EqEngineManagerDistributed(d_te, *d_sharedSolver.get())); // make the distributed model manager d_mmanager.reset(new ModelManagerDistributed(d_te, *d_eemanager.get())); } @@ -95,6 +100,10 @@ theory::TheoryModel* CombinationEngine::getModel() return d_mmanager->getModel(); } +SharedSolver* CombinationEngine::getSharedSolver() +{ + return d_sharedSolver.get(); +} bool CombinationEngine::isProofEnabled() const { return d_cmbsPg != nullptr; } eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify() diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h index 886bdc71d..daafc1f67 100644 --- a/src/theory/combination_engine.h +++ b/src/theory/combination_engine.h @@ -23,6 +23,7 @@ #include "theory/eager_proof_generator.h" #include "theory/ee_manager.h" #include "theory/model_manager.h" +#include "theory/shared_solver.h" namespace CVC4 { @@ -82,6 +83,11 @@ class CombinationEngine */ TheoryModel* getModel(); //-------------------------- end model + /** + * Get the shared solver, which is the active component of theory combination + * that TheoryEngine interacts with prior to calling combineTheories. + */ + SharedSolver* getSharedSolver(); /** * Called at the beginning of full effort */ @@ -119,6 +125,11 @@ class CombinationEngine * model. */ std::unique_ptr d_mmanager; + /** + * The shared solver. This class is responsible for performing combination + * tasks (e.g. preregistration) during solving. + */ + std::unique_ptr d_sharedSolver; /** * An eager proof generator, if proofs are enabled. This proof generator is * responsible for proofs of splitting lemmas generated in combineTheories. diff --git a/src/theory/ee_manager.cpp b/src/theory/ee_manager.cpp index e473388f0..697689fb9 100644 --- a/src/theory/ee_manager.cpp +++ b/src/theory/ee_manager.cpp @@ -19,7 +19,10 @@ namespace CVC4 { namespace theory { -EqEngineManager::EqEngineManager(TheoryEngine& te) : d_te(te) {} +EqEngineManager::EqEngineManager(TheoryEngine& te, SharedSolver& shs) + : d_te(te), d_sharedSolver(shs) +{ +} const EeTheoryInfo* EqEngineManager::getEeTheoryInfo(TheoryId tid) const { diff --git a/src/theory/ee_manager.h b/src/theory/ee_manager.h index 8d65eb2f1..6e40ceb7b 100644 --- a/src/theory/ee_manager.h +++ b/src/theory/ee_manager.h @@ -30,6 +30,8 @@ class TheoryEngine; namespace theory { +class SharedSolver; + /** * This is (theory-agnostic) information associated with the management of * an equality engine for a single theory. This information is maintained @@ -51,7 +53,12 @@ struct EeTheoryInfo class EqEngineManager { public: - EqEngineManager(TheoryEngine& te); + /** + * @param te Reference to the theory engine + * @param sharedSolver The shared solver that is being used in combination + * with this equality engine manager + */ + EqEngineManager(TheoryEngine& te, SharedSolver& shs); virtual ~EqEngineManager() {} /** * Initialize theories, called during TheoryEngine::finishInit after theory @@ -81,6 +88,8 @@ class EqEngineManager protected: /** Reference to the theory engine */ TheoryEngine& d_te; + /** Reference to the shared solver */ + SharedSolver& d_sharedSolver; /** Information related to the equality engine, per theory. */ std::map d_einfo; }; diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp index 6f6eeb7e7..360b1257b 100644 --- a/src/theory/ee_manager_distributed.cpp +++ b/src/theory/ee_manager_distributed.cpp @@ -15,13 +15,15 @@ #include "theory/ee_manager_distributed.h" #include "theory/quantifiers_engine.h" +#include "theory/shared_solver.h" #include "theory/theory_engine.h" namespace CVC4 { namespace theory { -EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te) - : EqEngineManager(te), d_masterEENotify(nullptr) +EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te, + SharedSolver& shs) + : EqEngineManager(te, shs), d_masterEENotify(nullptr) { } diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index c233216ea..90beb0d3b 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -45,7 +45,7 @@ namespace theory { class EqEngineManagerDistributed : public EqEngineManager { public: - EqEngineManagerDistributed(TheoryEngine& te); + EqEngineManagerDistributed(TheoryEngine& te, SharedSolver& shs); ~EqEngineManagerDistributed(); /** * Initialize theories. This method allocates unique equality engines diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index a425441fd..47dca7d66 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -174,6 +174,8 @@ void TheoryEngine::finishInit() { // initialize the theory combination manager, which decides and allocates the // equality engines to use for all theories. d_tc->finishInit(); + // get pointer to the shared solver + d_sharedSolver = d_tc->getSharedSolver(); // set the core equality engine on quantifiers engine if (d_logicInfo.isQuantified()) @@ -223,17 +225,17 @@ TheoryEngine::TheoryEngine(context::Context* context, d_outMgr(outMgr), d_pnm(nullptr), d_lazyProof( - d_pnm != nullptr ? new LazyCDProof( - d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof") - : nullptr), + d_pnm != nullptr + ? new LazyCDProof( + d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof") + : nullptr), d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)), - d_sharedTerms(this, context), d_tc(nullptr), + d_sharedSolver(nullptr), d_quantEngine(nullptr), d_decManager(new DecisionManager(userContext)), d_relManager(nullptr), d_preRegistrationVisitor(this, context), - d_sharedTermsVisitor(d_sharedTerms), d_eager_model_building(false), d_inConflict(context, false), d_inSatMode(false), @@ -301,11 +303,6 @@ void TheoryEngine::preRegister(TNode preprocessed) { preprocessed = d_preregisterQueue.front(); d_preregisterQueue.pop(); - if (d_logicInfo.isSharingEnabled() && preprocessed.getKind() == kind::EQUAL) { - // When sharing is enabled, we propagate from the shared terms manager also - d_sharedTerms.addEqualityToPropagate(preprocessed); - } - // the atom should not have free variables Debug("theory") << "TheoryEngine::preRegister: " << preprocessed << std::endl; @@ -347,11 +344,11 @@ void TheoryEngine::preRegister(TNode preprocessed) { } } } - if (multipleTheories) { - // Collect the shared terms if there are multiple theories - NodeVisitor::run(d_sharedTermsVisitor, - preprocessed); - } + + // pre-register with the shared solver, which also handles + // calling prepregister on individual theories. + Assert(d_sharedSolver != nullptr); + d_sharedSolver->preRegisterShared(preprocessed, multipleTheories); } // Leaving pre-register @@ -961,7 +958,8 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo Assert(atom.getKind() == kind::EQUAL) << "atom should be an EQUALity, not `" << atom << "'"; if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) { - d_sharedTerms.assertEquality(atom, polarity, assertion); + // assert to the shared solver + d_sharedSolver->assertSharedEquality(atom, polarity, assertion); } return; } @@ -1052,23 +1050,7 @@ void TheoryEngine::assertFact(TNode literal) if (d_logicInfo.isSharingEnabled()) { // If any shared terms, it's time to do sharing work - if (d_sharedTerms.hasSharedTerms(atom)) { - // Notify the theories the shared terms - SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom); - SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom); - for (; it != it_end; ++ it) { - TNode term = *it; - theory::TheoryIdSet theories = - d_sharedTerms.getTheoriesToNotify(atom, term); - for (TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++ id) { - if (TheoryIdSetUtil::setContains(id, theories)) - { - theoryOf(id)->addSharedTerm(term); - } - } - d_sharedTerms.markNotified(term, theories); - } - } + d_sharedSolver->preNotifySharedFact(atom); // If it's an equality, assert it to the shared term manager, even though the terms are not // yet shared. As the terms become shared later, the shared terms manager will then add them @@ -1136,15 +1118,7 @@ const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; } theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) { Assert(a.getType().isComparableTo(b.getType())); - if (d_sharedTerms.isShared(a) && d_sharedTerms.isShared(b)) { - if (d_sharedTerms.areEqual(a,b)) { - return EQUALITY_TRUE_AND_PROPAGATED; - } - else if (d_sharedTerms.areDisequal(a,b)) { - return EQUALITY_FALSE_AND_PROPAGATED; - } - } - return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b); + return d_sharedSolver->getEqualityStatus(a, b); } Node TheoryEngine::getModelValue(TNode var) { @@ -1153,7 +1127,7 @@ Node TheoryEngine::getModelValue(TNode var) { // the model value of a constant must be itself return var; } - Assert(d_sharedTerms.isShared(var)); + Assert(d_sharedSolver->isShared(var)); return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var); } @@ -1768,20 +1742,9 @@ theory::TrustNode TheoryEngine::getExplanation( } } - Node explanation; - if (toExplain.d_theory == THEORY_BUILTIN) - { - explanation = d_sharedTerms.explain(toExplain.d_node); - Debug("theory::explain") << "\tTerm was propagated by THEORY_BUILTIN. Explanation: " << explanation << std::endl; - } - else - { - TrustNode texp = theoryOf(toExplain.d_theory)->explain(toExplain.d_node); - explanation = texp.getNode(); - Debug("theory::explain") << "\tTerm was propagated by owner theory: " - << theoryOf(toExplain.d_theory)->getId() - << ". Explanation: " << explanation << std::endl; - } + TrustNode texp = + d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory); + Node explanation = texp.getNode(); Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 7639afdbf..cfca03515 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -154,14 +154,10 @@ class TheoryEngine { /** The proof generator */ std::shared_ptr d_tepg; //--------------------------------- end new proofs - - /** - * The database of shared terms. - */ - SharedTermsDatabase d_sharedTerms; - /** The combination manager we are using */ std::unique_ptr d_tc; + /** The shared solver of the above combination engine. */ + theory::SharedSolver* d_sharedSolver; /** * The quantifiers engine */ @@ -176,9 +172,6 @@ class TheoryEngine { /** Default visitor for pre-registration */ PreRegisterVisitor d_preRegistrationVisitor; - /** Visitor for collecting shared terms */ - SharedTermsVisitor d_sharedTermsVisitor; - /** are we in eager model building mode? (see setEagerModelBuilding). */ bool d_eager_model_building; -- 2.30.2