From: Andrew Reynolds Date: Tue, 25 Aug 2020 12:10:38 +0000 (-0500) Subject: Add the combination engine (#4939) X-Git-Tag: cvc5-1.0.0~2957 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=16578fca1c50d2ca9fce45c9c262db7ff6e2fd92;p=cvc5.git Add the combination engine (#4939) This adds the combination engine, which is the module of TheoryEngine which implements the combineTheories method and owns the various components of theory combination, which includes equality engine manager, model manager, and the "shared solver" (to come later). It will have two variants, CombinationCareGraph and CombinationModelBased, the former is added with this PR. FYI @barrettcw The next PR will connect this module to TheoryEngine and remove a few existing methods from TheoryEngine, as they are implemented in the modules of this class. --- 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& 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 + +#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& 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& 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 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 +#include + +#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& 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 d_paraTheories; + /** + * The equality engine manager we are using. This class is responsible for + * configuring equality engines for each theory. + */ + std::unique_ptr d_eemanager; + /** + * The model manager we are using. This class is responsible for building the + * model. + */ + std::unique_ptr 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;