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.
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
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."
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
* 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.
*/
}
}
-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());
* 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
}
// 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())
/* 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;
/** 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;
projects / cvc5.git / commitdiff