diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | src/options/theory_options.toml | 24 | ||||
| -rw-r--r-- | src/theory/combination_care_graph.cpp | 88 | ||||
| -rw-r--r-- | src/theory/combination_care_graph.h | 51 | ||||
| -rw-r--r-- | src/theory/combination_engine.cpp | 120 | ||||
| -rw-r--r-- | src/theory/combination_engine.h | 122 | ||||
| -rw-r--r-- | src/theory/ee_manager.h | 3 | ||||
| -rw-r--r-- | src/theory/ee_manager_distributed.cpp | 5 | ||||
| -rw-r--r-- | src/theory/ee_manager_distributed.h | 3 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 3 | ||||
| -rw-r--r-- | src/theory/theory_engine.h | 28 |
11 files changed, 434 insertions, 17 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 83cd363f6..f6c5187c7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -465,6 +465,10 @@ libcvc4_add_sources( theory/bv/theory_bv_utils.h theory/bv/type_enumerator.h theory/care_graph.h + theory/combination_care_graph.cpp + theory/combination_care_graph.h + theory/combination_engine.cpp + theory/combination_engine.h theory/datatypes/datatypes_rewriter.cpp theory/datatypes/datatypes_rewriter.h theory/datatypes/sygus_datatype_utils.cpp diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml index 6ec9d8854..388333124 100644 --- a/src/options/theory_options.toml +++ b/src/options/theory_options.toml @@ -42,3 +42,27 @@ header = "options/theory_options.h" type = "bool" default = "false" help = "enable analysis of relevance of asserted literals with respect to the input formula" + +[[option]] + name = "eeMode" + category = "expert" + long = "ee-mode=MODE" + type = "EqEngineMode" + default = "DISTRIBUTED" + help = "mode for managing equalities across theory solvers" + help_mode = "Defines mode for managing equalities across theory solvers." +[[option.mode.DISTRIBUTED]] + name = "distributed" + help = "Each theory maintains its own equality engine." + +[[option]] + name = "tcMode" + category = "expert" + long = "tc-mode=MODE" + type = "TcMode" + default = "CARE_GRAPH" + help = "mode for theory combination" + help_mode = "Defines mode for theory combination." +[[option.mode.CARE_GRAPH]] + name = "care-graph" + help = "Use care graphs for theory combination." diff --git a/src/theory/combination_care_graph.cpp b/src/theory/combination_care_graph.cpp new file mode 100644 index 000000000..9374e7ecb --- /dev/null +++ b/src/theory/combination_care_graph.cpp @@ -0,0 +1,88 @@ +/********************* */ +/*! \file combination_care_graph.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 Management of a care graph based approach for theory combination. + **/ + +#include "theory/combination_care_graph.h" + +#include "expr/node_visitor.h" +#include "theory/care_graph.h" +#include "theory/theory_engine.h" + +namespace CVC4 { +namespace theory { + +CombinationCareGraph::CombinationCareGraph( + TheoryEngine& te, const std::vector<Theory*>& paraTheories) + : CombinationEngine(te, paraTheories) +{ +} + +CombinationCareGraph::~CombinationCareGraph() {} + +void CombinationCareGraph::combineTheories() +{ + Trace("combineTheories") << "TheoryEngine::combineTheories()" << std::endl; + + // Care graph we'll be building + CareGraph careGraph; + + // get the care graph from the parametric theories + for (Theory* t : d_paraTheories) + { + t->getCareGraph(&careGraph); + } + + Trace("combineTheories") + << "TheoryEngine::combineTheories(): care graph size = " + << careGraph.size() << std::endl; + + // Now add splitters for the ones we are interested in + prop::PropEngine* propEngine = d_te.getPropEngine(); + for (const CarePair& carePair : careGraph) + { + Debug("combineTheories") + << "TheoryEngine::combineTheories(): checking " << carePair.d_a << " = " + << carePair.d_b << " from " << carePair.d_theory << std::endl; + + // The equality in question (order for no repetition) + Node equality = carePair.d_a.eqNode(carePair.d_b); + + // We need to split on it + Debug("combineTheories") + << "TheoryEngine::combineTheories(): requesting a split " << std::endl; + + Node split = equality.orNode(equality.notNode()); + sendLemma(split, carePair.d_theory); + + // Could check the equality status here: + // EqualityStatus es = getEqualityStatus(carePair.d_a, carePair.d_b); + // and only require true phase below if: + // es == EQUALITY_TRUE || es == EQUALITY_TRUE_IN_MODEL + // and require false phase below if: + // es == EQUALITY_FALSE_IN_MODEL + // This is supposed to force preference to follow what the theory models + // already have but it doesn't seem to make a big difference - need to + // explore more -Clark + Node e = d_te.ensureLiteral(equality); + propEngine->requirePhase(e, true); + } +} + +bool CombinationCareGraph::buildModel() +{ + // building the model happens as a separate step + return d_mmanager->buildModel(); +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/combination_care_graph.h b/src/theory/combination_care_graph.h new file mode 100644 index 000000000..0fbefb16a --- /dev/null +++ b/src/theory/combination_care_graph.h @@ -0,0 +1,51 @@ +/********************* */ +/*! \file combination_care_graph.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 Management of a care graph based approach for theory combination. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__COMBINATION_CARE_GRAPH__H +#define CVC4__THEORY__COMBINATION_CARE_GRAPH__H + +#include <vector> + +#include "theory/combination_engine.h" + +namespace CVC4 { + +class TheoryEngine; + +namespace theory { + +/** + * Manager for doing theory combination using care graphs. This is typically + * done via a distributed equality engine architecture. + */ +class CombinationCareGraph : public CombinationEngine +{ + public: + CombinationCareGraph(TheoryEngine& te, + const std::vector<Theory*>& paraTheories); + ~CombinationCareGraph(); + + bool buildModel() override; + /** + * Combine theories using a care graph. + */ + void combineTheories() override; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__COMBINATION_DISTRIBUTED__H */ diff --git a/src/theory/combination_engine.cpp b/src/theory/combination_engine.cpp new file mode 100644 index 000000000..83aae3f54 --- /dev/null +++ b/src/theory/combination_engine.cpp @@ -0,0 +1,120 @@ +/********************* */ +/*! \file combination_engine.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 Management of a care graph based approach for theory combination. + **/ + +#include "theory/combination_engine.h" + +#include "expr/node_visitor.h" +#include "theory/care_graph.h" +#include "theory/ee_manager_distributed.h" +#include "theory/model_manager_distributed.h" +#include "theory/shared_terms_database.h" +#include "theory/term_registration_visitor.h" +#include "theory/theory_engine.h" + +namespace CVC4 { +namespace theory { + +CombinationEngine::CombinationEngine(TheoryEngine& te, + const std::vector<Theory*>& paraTheories) + : d_te(te), + d_logicInfo(te.getLogicInfo()), + d_paraTheories(paraTheories), + d_eemanager(nullptr), + d_mmanager(nullptr) +{ +} + +CombinationEngine::~CombinationEngine() {} + +void CombinationEngine::finishInit() +{ + // create the equality engine, model manager, and shared solver + if (options::eeMode() == options::EqEngineMode::DISTRIBUTED) + { + // make the distributed equality engine manager + std::unique_ptr<EqEngineManagerDistributed> eeDistributed( + new EqEngineManagerDistributed(d_te)); + // make the distributed model manager + d_mmanager.reset(new ModelManagerDistributed(d_te, *eeDistributed.get())); + d_eemanager = std::move(eeDistributed); + } + else + { + Unhandled() << "CombinationEngine::finishInit: equality engine mode " + << options::eeMode() << " not supported"; + } + + Assert(d_eemanager != nullptr); + + // initialize equality engines in all theories, including quantifiers engine + // and the (provided) shared solver + d_eemanager->initializeTheories(); + + Assert(d_mmanager != nullptr); + // initialize the model manager + d_mmanager->finishInit(); + + // initialize equality engine of the model using the equality engine manager + TheoryModel* m = d_mmanager->getModel(); + eq::EqualityEngineNotify* meen = getModelEqualityEngineNotify(); + d_eemanager->initializeModel(m, meen); +} + +const EeTheoryInfo* CombinationEngine::getEeTheoryInfo(TheoryId tid) const +{ + return d_eemanager->getEeTheoryInfo(tid); +} + +eq::EqualityEngine* CombinationEngine::getCoreEqualityEngine() +{ + return d_eemanager->getCoreEqualityEngine(); +} + +void CombinationEngine::resetModel() { d_mmanager->resetModel(); } + +void CombinationEngine::postProcessModel(bool incomplete) +{ + // should have a consistent core equality engine + eq::EqualityEngine* mee = d_eemanager->getCoreEqualityEngine(); + if (mee != nullptr) + { + AlwaysAssert(mee->consistent()); + } + // postprocess with the model + d_mmanager->postProcessModel(incomplete); +} + +theory::TheoryModel* CombinationEngine::getModel() +{ + return d_mmanager->getModel(); +} + +eq::EqualityEngineNotify* CombinationEngine::getModelEqualityEngineNotify() +{ + // by default, no notifications from model's equality engine + return nullptr; +} + +void CombinationEngine::sendLemma(TNode node, TheoryId atomsTo) +{ + d_te.lemma(node, RULE_INVALID, false, LemmaProperty::NONE, atomsTo); +} + +void CombinationEngine::resetRound() +{ + // do nothing +} + +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/combination_engine.h b/src/theory/combination_engine.h new file mode 100644 index 000000000..cfe6562d4 --- /dev/null +++ b/src/theory/combination_engine.h @@ -0,0 +1,122 @@ +/********************* */ +/*! \file combination_engine.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 Abstract interface for theory combination. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__COMBINATION_ENGINE__H +#define CVC4__THEORY__COMBINATION_ENGINE__H + +#include <vector> +#include <memory> + +#include "theory/ee_manager.h" +#include "theory/model_manager.h" + +namespace CVC4 { + +class TheoryEngine; + +namespace theory { + +/** + * Manager for doing theory combination. This class is responsible for: + * (1) Initializing the various components of theory combination (equality + * engine manager, model manager, shared solver) based on the equality engine + * mode, and + * (2) Implementing the main combination method (combineTheories). + */ +class CombinationEngine +{ + public: + CombinationEngine(TheoryEngine& te, const std::vector<Theory*>& paraTheories); + virtual ~CombinationEngine(); + + /** Finish initialization */ + void finishInit(); + + //-------------------------- equality engine + /** Get equality engine theory information for theory with identifier tid. */ + const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const; + /** + * Get the "core" equality engine. This is the equality engine that + * quantifiers should use. + */ + eq::EqualityEngine* getCoreEqualityEngine(); + //-------------------------- end equality engine + //-------------------------- model + /** + * Reset the model maintained by this class. This resets all local information + * that is unique to each check. + */ + void resetModel(); + /** + * Build the model maintained by this class. + * + * @return true if model building was successful. + */ + virtual bool buildModel() = 0; + /** + * Post process the model maintained by this class. This is called after + * a successful call to buildModel. This does any theory-specific + * postprocessing of the model. + * + * @param incomplete Whether we are answering "unknown" instead of "sat". + */ + void postProcessModel(bool incomplete); + /** + * Get the model object maintained by this class. + */ + TheoryModel* getModel(); + //-------------------------- end model + /** + * Called at the beginning of full effort + */ + virtual void resetRound(); + /** + * Combine theories, called after FULL effort passes with no lemmas + * and before LAST_CALL effort is run. This adds necessary lemmas for + * theory combination (e.g. splitting lemmas) to the parent TheoryEngine. + */ + virtual void combineTheories() = 0; + + protected: + /** + * Get model equality engine notify. Return the notification object for + * who listens to the model's equality engine (if any). + */ + virtual eq::EqualityEngineNotify* getModelEqualityEngineNotify(); + /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */ + void sendLemma(TNode node, TheoryId atomsTo); + /** Reference to the theory engine */ + TheoryEngine& d_te; + /** Logic info of theory engine (cached) */ + const LogicInfo& d_logicInfo; + /** List of parametric theories of theory engine */ + const std::vector<Theory*> d_paraTheories; + /** + * The equality engine manager we are using. This class is responsible for + * configuring equality engines for each theory. + */ + std::unique_ptr<EqEngineManager> d_eemanager; + /** + * The model manager we are using. This class is responsible for building the + * model. + */ + std::unique_ptr<ModelManager> d_mmanager; +}; + +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__COMBINATION_DISTRIBUTED__H */ diff --git a/src/theory/ee_manager.h b/src/theory/ee_manager.h index 3c82e43de..aa4bcc66c 100644 --- a/src/theory/ee_manager.h +++ b/src/theory/ee_manager.h @@ -66,7 +66,8 @@ class EqEngineManager * This method is context-independent, and is applied once during * the lifetime of TheoryEngine (during finishInit). */ - virtual void initializeModel(TheoryModel* m) = 0; + virtual void initializeModel(TheoryModel* m, + eq::EqualityEngineNotify* notify) = 0; /** * Get the equality engine theory information for theory with the given id. */ diff --git a/src/theory/ee_manager_distributed.cpp b/src/theory/ee_manager_distributed.cpp index 39275dd2d..ea618fcae 100644 --- a/src/theory/ee_manager_distributed.cpp +++ b/src/theory/ee_manager_distributed.cpp @@ -96,13 +96,16 @@ void EqEngineManagerDistributed::initializeTheories() } } -void EqEngineManagerDistributed::initializeModel(TheoryModel* m) +void EqEngineManagerDistributed::initializeModel( + TheoryModel* m, eq::EqualityEngineNotify* notify) { Assert(m != nullptr); // initialize the model equality engine EeSetupInfo esim; if (m->needsEqualityEngine(esim)) { + // use the provided notification object + esim.d_notify = notify; d_modelEqualityEngine.reset( allocateEqualityEngine(esim, &d_modelEeContext)); m->setEqualityEngine(d_modelEqualityEngine.get()); diff --git a/src/theory/ee_manager_distributed.h b/src/theory/ee_manager_distributed.h index 693466867..dd4608c9a 100644 --- a/src/theory/ee_manager_distributed.h +++ b/src/theory/ee_manager_distributed.h @@ -59,7 +59,8 @@ class EqEngineManagerDistributed : public EqEngineManager * Initialize model. This method allocates a new equality engine for the * model. */ - void initializeModel(TheoryModel* m) override; + void initializeModel(TheoryModel* m, + eq::EqualityEngineNotify* notify) 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 diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index cf29039ff..647a40999 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -167,7 +167,8 @@ void TheoryEngine::finishInit() { } // Initialize the model - d_eeDistributed->initializeModel(d_curr_model); + // !!!! temporary, will be part of combination engine initialization + d_eeDistributed->initializeModel(d_curr_model, nullptr); // set the core equality engine on quantifiers engine if (d_logicInfo.isQuantified()) diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 549f4078e..ff4c3bdf9 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -87,23 +87,24 @@ struct NodeTheoryPairHashFunction { /* Forward declarations */ namespace theory { - class TheoryModel; - class TheoryEngineModelBuilder; - class EqEngineManagerDistributed; +class CombinationEngine; +class TheoryModel; +class TheoryEngineModelBuilder; +class EqEngineManagerDistributed; - class DecisionManager; - class RelevanceManager; +class DecisionManager; +class RelevanceManager; - namespace eq { - class EqualityEngine; - }/* CVC4::theory::eq namespace */ +namespace eq { +class EqualityEngine; +} // namespace eq - namespace quantifiers { - class TermDb; - } +namespace quantifiers { +class TermDb; +} - class EntailmentCheckParameters; - class EntailmentCheckSideEffects; +class EntailmentCheckParameters; +class EntailmentCheckSideEffects; }/* CVC4::theory namespace */ class RemoveTermFormulas; @@ -118,6 +119,7 @@ class TheoryEngine { /** Shared terms database can use the internals notify the theories */ friend class SharedTermsDatabase; + friend class theory::CombinationEngine; friend class theory::quantifiers::TermDb; friend class theory::EngineOutputChannel; |