diff options
| -rw-r--r-- | src/CMakeLists.txt | 2 | ||||
| -rw-r--r-- | src/theory/ee_manager.cpp | 31 | ||||
| -rw-r--r-- | src/theory/ee_manager.h | 90 | ||||
| -rw-r--r-- | src/theory/ee_manager_distributed.cpp | 53 | ||||
| -rw-r--r-- | src/theory/ee_manager_distributed.h | 77 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 13 | ||||
| -rw-r--r-- | src/theory/theory_model.cpp | 38 | ||||
| -rw-r--r-- | src/theory/theory_model.h | 16 |
8 files changed, 239 insertions, 81 deletions
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<TheoryId, EeTheoryInfo>::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 <map> +#include <memory> + +#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<eq::EqualityEngine> 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<TheoryId, EeTheoryInfo> 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<TheoryId, EeTheoryInfo>::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 <map> #include <memory> -#include "theory/ee_setup_info.h" -#include "theory/theory.h" +#include "theory/ee_manager.h" #include "theory/uf/equality_engine.h" namespace CVC4 { @@ -32,38 +31,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<eq::EqualityEngine> 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<TheoryId, EeTheoryInfo> 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<MasterNotifyClass> d_masterEENotify; /** The master equality engine. */ std::unique_ptr<eq::EqualityEngine> 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<eq::EqualityEngine> 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) */ |