From 45fd2390beab04e560508d83c99492490c2d8d57 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 21 Aug 2020 18:51:37 -0500 Subject: [PATCH] Dynamic allocation of model equality engine (#4911) This makes the equality engine manager responsible for initializing the equality engine of the model. It also moves the base equality engine manager class to its own file. Notice the code in TheoryEngine will undergo significant cleaning in forthcoming PRs when the "ModelManagerDistributed" is added. This PR adds temporary calls there to preserve the current behavior. --- src/CMakeLists.txt | 2 + src/theory/ee_manager.cpp | 31 +++++++++ src/theory/ee_manager.h | 90 +++++++++++++++++++++++++++ src/theory/ee_manager_distributed.cpp | 53 ++++++++++++---- src/theory/ee_manager_distributed.h | 77 +++++++++-------------- src/theory/theory_engine.cpp | 13 +++- src/theory/theory_model.cpp | 38 ++++++----- src/theory/theory_model.h | 16 ++++- 8 files changed, 239 insertions(+), 81 deletions(-) create mode 100644 src/theory/ee_manager.cpp create mode 100644 src/theory/ee_manager.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index f9d7f833e..c9eaede9a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -486,6 +486,8 @@ libcvc4_add_sources( theory/decision_strategy.h theory/eager_proof_generator.cpp theory/eager_proof_generator.h + theory/ee_manager.cpp + theory/ee_manager.h theory/ee_manager_distributed.cpp theory/ee_manager_distributed.h theory/ee_setup_info.h diff --git a/src/theory/ee_manager.cpp b/src/theory/ee_manager.cpp new file mode 100644 index 000000000..bec355e7d --- /dev/null +++ b/src/theory/ee_manager.cpp @@ -0,0 +1,31 @@ +/********************* */ +/*! \file ee_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utilities for management of equality engines. + **/ + +#include "theory/ee_manager.h" + +namespace CVC4 { +namespace theory { + +const EeTheoryInfo* EqEngineManager::getEeTheoryInfo(TheoryId tid) const +{ + std::map::const_iterator it = d_einfo.find(tid); + if (it != d_einfo.end()) + { + return &it->second; + } + return nullptr; +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/ee_manager.h b/src/theory/ee_manager.h new file mode 100644 index 000000000..3c82e43de --- /dev/null +++ b/src/theory/ee_manager.h @@ -0,0 +1,90 @@ +/********************* */ +/*! \file ee_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Utilities for management of equality engines. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__EE_MANAGER__H +#define CVC4__THEORY__EE_MANAGER__H + +#include +#include + +#include "theory/ee_setup_info.h" +#include "theory/theory.h" +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { + +/** + * This is (theory-agnostic) information associated with the management of + * an equality engine for a single theory. This information is maintained + * by the manager class below. + * + * Currently, this simply is the equality engine itself, for memory + * management purposes. + */ +struct EeTheoryInfo +{ + EeTheoryInfo() : d_usedEe(nullptr) {} + /** Equality engine that is used (if it exists) */ + eq::EqualityEngine* d_usedEe; + /** Equality engine allocated specifically for this theory (if it exists) */ + std::unique_ptr d_allocEe; +}; + +/** Virtual base class for equality engine managers */ +class EqEngineManager +{ + public: + virtual ~EqEngineManager() {} + /** + * Finish initialize, called by TheoryEngine::finishInit after theory + * objects have been created but prior to their final initialization. This + * sets up equality engines for all theories. + * + * This method is context-independent, and is applied once during + * the lifetime of TheoryEngine (during finishInit). + */ + virtual void initializeTheories() = 0; + /** + * Finish initialize, called by TheoryEngine::finishInit after theory + * objects have been created but prior to their final initialization. This + * sets up equality engines for all theories. + * + * This method is context-independent, and is applied once during + * the lifetime of TheoryEngine (during finishInit). + */ + virtual void initializeModel(TheoryModel* m) = 0; + /** + * Get the equality engine theory information for theory with the given id. + */ + const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const; + /** + * Get the core equality engine, which is the equality engine that the + * quantifiers engine should use. This corresponds to the master equality + * engine if eeMode is distributed, or the central equality engine if eeMode + * is central. + */ + virtual eq::EqualityEngine* getCoreEqualityEngine() = 0; + + protected: + /** Information related to the equality engine, per theory. */ + std::map d_einfo; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__EE_MANAGER__H */ diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp index eb12ce893..39275dd2d 100644 --- a/src/theory/ee_manager_distributed.cpp +++ b/src/theory/ee_manager_distributed.cpp @@ -20,26 +20,21 @@ namespace CVC4 { namespace theory { -const EeTheoryInfo* EqEngineManager::getEeTheoryInfo(TheoryId tid) const -{ - std::map::const_iterator it = d_einfo.find(tid); - if (it != d_einfo.end()) - { - return &it->second; - } - return nullptr; -} - EqEngineManagerDistributed::EqEngineManagerDistributed(TheoryEngine& te) : d_te(te), d_masterEENotify(nullptr) { } -EqEngineManagerDistributed::~EqEngineManagerDistributed() {} +EqEngineManagerDistributed::~EqEngineManagerDistributed() +{ + // pop the model context which we pushed on initialization + d_modelEeContext.pop(); +} -void EqEngineManagerDistributed::finishInit() +void EqEngineManagerDistributed::initializeTheories() { context::Context* c = d_te.getSatContext(); + // allocate equality engines per theory for (TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; @@ -61,6 +56,7 @@ void EqEngineManagerDistributed::finishInit() } // allocate the equality engine eet.d_allocEe.reset(allocateEqualityEngine(esi, c)); + // the theory uses the equality engine eet.d_usedEe = eet.d_allocEe.get(); } @@ -100,13 +96,44 @@ void EqEngineManagerDistributed::finishInit() } } +void EqEngineManagerDistributed::initializeModel(TheoryModel* m) +{ + Assert(m != nullptr); + // initialize the model equality engine + EeSetupInfo esim; + if (m->needsEqualityEngine(esim)) + { + d_modelEqualityEngine.reset( + allocateEqualityEngine(esim, &d_modelEeContext)); + m->setEqualityEngine(d_modelEqualityEngine.get()); + } + else + { + AlwaysAssert(false) << "Expected model to use equality engine"; + } + m->finishInit(); + // We push a context during initialization since the model is cleared during + // collectModelInfo using pop/push. + d_modelEeContext.push(); +} + void EqEngineManagerDistributed::MasterNotifyClass::eqNotifyNewClass(TNode t) { // adds t to the quantifiers term database d_quantEngine->eqNotifyNewClass(t); } -eq::EqualityEngine* EqEngineManagerDistributed::getMasterEqualityEngine() +context::Context* EqEngineManagerDistributed::getModelEqualityEngineContext() +{ + return &d_modelEeContext; +} + +eq::EqualityEngine* EqEngineManagerDistributed::getModelEqualityEngine() +{ + return d_modelEqualityEngine.get(); +} + +eq::EqualityEngine* EqEngineManagerDistributed::getCoreEqualityEngine() { return d_masterEqualityEngine.get(); } diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index ededa956e..693466867 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -21,8 +21,7 @@ #include #include -#include "theory/ee_setup_info.h" -#include "theory/theory.h" +#include "theory/ee_manager.h" #include "theory/uf/equality_engine.h" namespace CVC4 { @@ -31,38 +30,6 @@ class TheoryEngine; namespace theory { -/** - * This is (theory-agnostic) information associated with the management of - * an equality engine for a single theory. This information is maintained - * by the manager class below. - * - * Currently, this simply is the equality engine itself, which is a unique_ptr - * for memory management purposes. - */ -struct EeTheoryInfo -{ - EeTheoryInfo() : d_usedEe(nullptr) {} - /** The equality engine that the theory uses (if it exists) */ - eq::EqualityEngine* d_usedEe; - /** The equality engine allocated by this theory (if it exists) */ - std::unique_ptr d_allocEe; -}; - -/** Virtual base class for equality engine managers */ -class EqEngineManager -{ - public: - virtual ~EqEngineManager() {} - /** - * Get the equality engine theory information for theory with the given id. - */ - const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const; - - protected: - /** Information related to the equality engine, per theory. */ - std::map d_einfo; -}; - /** * The (distributed) equality engine manager. This encapsulates an architecture * in which all theories maintain their own copy of an equality engine. @@ -84,18 +51,30 @@ class EqEngineManagerDistributed : public EqEngineManager EqEngineManagerDistributed(TheoryEngine& te); ~EqEngineManagerDistributed(); /** - * Finish initialize, called by TheoryEngine::finishInit after theory - * objects have been created but prior to their final initialization. This - * sets up equality engines for all theories. - * - * This method is context-independent, and is applied once during - * the lifetime of TheoryEngine (during finishInit). + * Initialize theories. This method allocates unique equality engines + * per theories and connects them to a master equality engine. */ - void finishInit(); - /** get the master equality engine */ - eq::EqualityEngine* getMasterEqualityEngine(); + void initializeTheories() override; + /** + * Initialize model. This method allocates a new equality engine for the + * model. + */ + void initializeModel(TheoryModel* m) override; + /** + * Get the model equality engine context. This is a dummy context that is + * used for clearing the contents of the model's equality engine via + * pop/push. + */ + context::Context* getModelEqualityEngineContext(); + /** get the model equality engine */ + eq::EqualityEngine* getModelEqualityEngine(); + /** get the core equality engine */ + eq::EqualityEngine* getCoreEqualityEngine() override; private: + /** Allocate equality engine that is context-dependent on c with info esi */ + eq::EqualityEngine* allocateEqualityEngine(EeSetupInfo& esi, + context::Context* c); /** notify class for master equality engine */ class MasterNotifyClass : public theory::eq::EqualityEngineNotify { @@ -126,15 +105,21 @@ class EqEngineManagerDistributed : public EqEngineManager /** Pointer to quantifiers engine */ QuantifiersEngine* d_quantEngine; }; - /** Allocate equality engine that is context-dependent on c with info esi */ - eq::EqualityEngine* allocateEqualityEngine(EeSetupInfo& esi, - context::Context* c); /** Reference to the theory engine */ TheoryEngine& d_te; /** The master equality engine notify class */ std::unique_ptr d_masterEENotify; /** The master equality engine. */ std::unique_ptr d_masterEqualityEngine; + /** + * A dummy context for the model equality engine, so we can clear it + * independently of search context. + */ + context::Context d_modelEeContext; + /** + * The equality engine of the model. + */ + std::unique_ptr d_modelEqualityEngine; }; } // namespace theory diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index f0966a96d..b88b6158e 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -141,7 +141,7 @@ void TheoryEngine::finishInit() { // Initialize the equality engine architecture for all theories, which // includes the master equality engine. d_eeDistributed.reset(new EqEngineManagerDistributed(*this)); - d_eeDistributed->finishInit(); + d_eeDistributed->initializeTheories(); // Initialize the model and model builder. if (d_logicInfo.isQuantified()) @@ -166,11 +166,14 @@ void TheoryEngine::finishInit() { d_aloc_curr_model_builder = true; } + // Initialize the model + d_eeDistributed->initializeModel(d_curr_model); + // set the core equality engine on quantifiers engine if (d_logicInfo.isQuantified()) { d_quantEngine->setMasterEqualityEngine( - d_eeDistributed->getMasterEqualityEngine()); + d_eeDistributed->getCoreEqualityEngine()); } // finish initializing the theories @@ -525,6 +528,10 @@ void TheoryEngine::check(Theory::Effort effort) { } //checks for theories requiring the model go at last call d_curr_model->reset(); + // !!! temporary, will be part of distributed model manager + context::Context* meec = d_eeDistributed->getModelEqualityEngineContext(); + meec->pop(); + meec->push(); for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { if( theoryId!=THEORY_QUANTIFIERS ){ Theory* theory = d_theoryTable[theoryId]; @@ -566,7 +573,7 @@ void TheoryEngine::check(Theory::Effort effort) { if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) { // case where we are about to answer SAT, the master equality engine, // if it exists, must be consistent. - eq::EqualityEngine* mee = d_eeDistributed->getMasterEqualityEngine(); + eq::EqualityEngine* mee = d_eeDistributed->getCoreEqualityEngine(); if (mee != NULL) { AlwaysAssert(mee->consistent()); diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 4c7600da2..725a932a2 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -29,9 +29,9 @@ namespace theory { TheoryModel::TheoryModel(context::Context* c, std::string name, bool enableFuncModels) - : d_substitutions(c, false), - d_modelBuilt(false), - d_modelBuiltSuccess(false), + : d_name(name), + d_substitutions(c, false), + d_equalityEngine(nullptr), d_using_model_core(false), d_enableFuncModels(enableFuncModels) { @@ -39,10 +39,26 @@ TheoryModel::TheoryModel(context::Context* c, Assert(d_enableFuncModels || !options::ufHo()); d_true = NodeManager::currentNM()->mkConst( true ); d_false = NodeManager::currentNM()->mkConst( false ); +} + +TheoryModel::~TheoryModel() {} + +void TheoryModel::setEqualityEngine(eq::EqualityEngine* ee) +{ + d_equalityEngine = ee; +} - d_eeContext = new context::Context(); - d_equalityEngine = new eq::EqualityEngine(d_eeContext, name, false); +bool TheoryModel::needsEqualityEngine(EeSetupInfo& esi) +{ + // no notifications + esi.d_name = d_name; + esi.d_constantsAreTriggers = false; + return true; +} +void TheoryModel::finishInit() +{ + Assert(d_equalityEngine != nullptr); // The kinds we are treating as function application in congruence d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo()); d_equalityEngine->addFunctionKind(kind::HO_APPLY); @@ -51,21 +67,13 @@ TheoryModel::TheoryModel(context::Context* c, d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR); d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL); d_equalityEngine->addFunctionKind(kind::APPLY_TESTER); - d_eeContext->push(); // do not interpret APPLY_UF if we are not assigning function values - if (!enableFuncModels) + if (!d_enableFuncModels) { setSemiEvaluatedKind(kind::APPLY_UF); } } -TheoryModel::~TheoryModel() -{ - d_eeContext->pop(); - delete d_equalityEngine; - delete d_eeContext; -} - void TheoryModel::reset(){ d_modelBuilt = false; d_modelBuiltSuccess = false; @@ -83,8 +91,6 @@ void TheoryModel::reset(){ d_uf_terms.clear(); d_ho_uf_terms.clear(); d_uf_models.clear(); - d_eeContext->pop(); - d_eeContext->push(); d_using_model_core = false; d_model_core.clear(); } diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h index 2d6bdd2af..f465cec88 100644 --- a/src/theory/theory_model.h +++ b/src/theory/theory_model.h @@ -81,6 +81,17 @@ class TheoryModel : public Model public: TheoryModel(context::Context* c, std::string name, bool enableFuncModels); ~TheoryModel() override; + //---------------------------- initialization + /** Called to set the equality engine. */ + void setEqualityEngine(eq::EqualityEngine* ee); + /** + * Returns true if we need an equality engine, this has the same contract + * as Theory::needsEqualityEngine. + */ + bool needsEqualityEngine(EeSetupInfo& esi); + /** Finish init */ + void finishInit(); + //---------------------------- end initialization /** reset the model */ virtual void reset(); @@ -348,15 +359,14 @@ public: std::vector< Node > getFunctionsToAssign(); //---------------------------- end function values protected: + /** Unique name of this model */ + std::string d_name; /** substitution map for this model */ SubstitutionMap d_substitutions; /** whether we have tried to build this model in the current context */ bool d_modelBuilt; /** whether this model has been built successfully */ bool d_modelBuiltSuccess; - /** special local context for our equalityEngine so we can clear it - * independently of search context */ - context::Context* d_eeContext; /** equality engine containing all known equalities/disequalities */ eq::EqualityEngine* d_equalityEngine; /** approximations (see recordApproximation) */ -- 2.30.2