This class is responsible for model building when using a distributed approach for equality engines.
This PR defines the class but does not yet activate it in TheoryEngine.
This includes some model-specific things from TheoryEngine which will be migrated to this class on the next PR.
theory/interrupted.h
theory/logic_info.cpp
theory/logic_info.h
+ theory/model_manager.cpp
+ theory/model_manager.h
+ theory/model_manager_distributed.cpp
+ theory/model_manager_distributed.h
theory/output_channel.cpp
theory/output_channel.h
theory/quantifiers/alpha_equivalence.cpp
--- /dev/null
+/********************* */
+/*! \file model_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 Abstract management of models for TheoryEngine.
+ **/
+
+#include "theory/model_manager.h"
+
+#include "options/theory_options.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/theory_engine.h"
+
+namespace CVC4 {
+namespace theory {
+
+ModelManager::ModelManager(TheoryEngine& te)
+ : d_te(te),
+ d_logicInfo(te.getLogicInfo()),
+ d_model(nullptr),
+ d_modelBuilder(nullptr),
+ d_modelBuilt(false),
+ d_modelBuiltSuccess(false)
+{
+}
+
+ModelManager::~ModelManager() {}
+
+void ModelManager::finishInit()
+{
+ // construct the model
+ const LogicInfo& logicInfo = d_te.getLogicInfo();
+ // Initialize the model and model builder.
+ if (logicInfo.isQuantified())
+ {
+ QuantifiersEngine* qe = d_te.getQuantifiersEngine();
+ Assert(qe != nullptr);
+ d_modelBuilder = qe->getModelBuilder();
+ d_model = qe->getModel();
+ }
+ else
+ {
+ context::Context* u = d_te.getUserContext();
+ d_alocModel.reset(
+ new TheoryModel(u, "DefaultModel", options::assignFunctionValues()));
+ d_model = d_alocModel.get();
+ }
+
+ // make the default builder, e.g. in the case that the quantifiers engine does
+ // not have a model builder
+ if (d_modelBuilder == nullptr)
+ {
+ d_alocModelBuilder.reset(new TheoryEngineModelBuilder(&d_te));
+ d_modelBuilder = d_alocModelBuilder.get();
+ }
+ // notice that the equality engine of the model has yet to be assigned.
+}
+
+void ModelManager::resetModel()
+{
+ d_modelBuilt = false;
+ d_modelBuiltSuccess = false;
+ // Reset basic information on the model object
+ d_model->reset();
+}
+
+bool ModelManager::buildModel()
+{
+ if (d_modelBuilt)
+ {
+ // already computed
+ return d_modelBuiltSuccess;
+ }
+ // reset the flags now
+ d_modelBuilt = true;
+ d_modelBuiltSuccess = false;
+
+ // prepare the model, which is specific to the manager
+ if (!prepareModel())
+ {
+ Trace("model-builder") << "ModelManager: fail prepare model" << std::endl;
+ return false;
+ }
+
+ // now, finish building the model
+ d_modelBuiltSuccess = finishBuildModel();
+ return d_modelBuiltSuccess;
+}
+
+bool ModelManager::isModelBuilt() const { return d_modelBuilt; }
+
+void ModelManager::postProcessModel(bool incomplete)
+{
+ if (!d_modelBuilt)
+ {
+ // model not built, nothing to do
+ return;
+ }
+ Trace("model-builder") << "ModelManager: post-process model..." << std::endl;
+ // model construction should always succeed unless lemmas were added
+ AlwaysAssert(d_modelBuiltSuccess);
+ if (!options::produceModels())
+ {
+ return;
+ }
+ // Do post-processing of model from the theories (used for THEORY_SEP
+ // to construct heap model)
+ for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
+ ++theoryId)
+ {
+ Theory* t = d_te.theoryOf(theoryId);
+ if (t == nullptr)
+ {
+ // theory not active, skip
+ continue;
+ }
+ Trace("model-builder-debug")
+ << " PostProcessModel on theory: " << theoryId << std::endl;
+ t->postProcessModel(d_model);
+ }
+ // also call the model builder's post-process model
+ d_modelBuilder->postProcessModel(incomplete, d_model);
+}
+
+theory::TheoryModel* ModelManager::getModel() { return d_model; }
+
+bool ModelManager::collectModelBooleanVariables()
+{
+ Trace("model-builder") << " CollectModelInfo boolean variables" << std::endl;
+ // Get value of the Boolean variables
+ prop::PropEngine* propEngine = d_te.getPropEngine();
+ std::vector<TNode> boolVars;
+ propEngine->getBooleanVariables(boolVars);
+ std::vector<TNode>::iterator it, iend = boolVars.end();
+ bool hasValue, value;
+ for (it = boolVars.begin(); it != iend; ++it)
+ {
+ TNode var = *it;
+ hasValue = propEngine->hasValue(var, value);
+ // Should we assert that hasValue is true?
+ if (!hasValue)
+ {
+ Trace("model-builder-assertions")
+ << " has no value : " << var << std::endl;
+ value = false;
+ }
+ Trace("model-builder-assertions")
+ << "(assert" << (value ? " " : " (not ") << var
+ << (value ? ");" : "));") << std::endl;
+ if (!d_model->assertPredicate(var, value))
+ {
+ return false;
+ }
+ }
+ return true;
+}
+
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file model_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 Abstract management of models for TheoryEngine.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__MODEL_MANAGER__H
+#define CVC4__THEORY__MODEL_MANAGER__H
+
+#include <memory>
+
+#include "theory/theory_model.h"
+#include "theory/theory_model_builder.h"
+
+namespace CVC4 {
+
+class TheoryEngine;
+
+namespace theory {
+
+/**
+ * A base class for managing models. Its main feature is to implement a
+ * buildModel command. Overall, its behavior is specific to the kind of equality
+ * engine management mode we are using. In particular, the prepare model
+ * method is a manager-specific way for setting up the equality engine of the
+ * model in preparation for model building.
+ */
+class ModelManager
+{
+ public:
+ ModelManager(TheoryEngine& te);
+ virtual ~ModelManager();
+ /** Finish initializing this class. */
+ void finishInit();
+ /** Reset model, called during full effort check before the model is built */
+ void resetModel();
+ /**
+ * Build the model. If we have yet to build the model on this round, this
+ * method calls the (manager-specific) prepareModel method and then calls
+ * finishBuildModel.
+ *
+ * @return true if model building was successful.
+ */
+ bool buildModel();
+ /**
+ * Have we called buildModel this round? Note this returns true whether or
+ * not the model building was successful.
+ */
+ bool isModelBuilt() const;
+ /**
+ * Post process model, which is used as a way of each theory adding additional
+ * information to the model after successfully building a model.
+ */
+ void postProcessModel(bool incomplete);
+ /** Get a pointer to model object maintained by this class. */
+ theory::TheoryModel* getModel();
+ //------------------------ finer grained control over model building
+ /**
+ * Prepare model, which is the manager-specific method for setting up the
+ * equality engine of the model. This should assert all relevant information
+ * about the model into the equality engine of d_model.
+ *
+ * @return true if we are in conflict (i.e. the equality engine of the model
+ * equality engine is inconsistent).
+ */
+ virtual bool prepareModel() = 0;
+ /**
+ * Finish build model, which calls the theory model builder to assign values
+ * to all equivalence classes. This should be run after prepareModel.
+ *
+ * @return true if model building was successful.
+ */
+ virtual bool finishBuildModel() const = 0;
+ //------------------------ end finer grained control over model building
+ protected:
+ /**
+ * Collect model Boolean variables.
+ * This asserts the values of all boolean variables to the equality engine of
+ * the model, based on their value in the prop engine.
+ *
+ * @return true if we are in conflict.
+ */
+ bool collectModelBooleanVariables();
+ /** Reference to the theory engine */
+ TheoryEngine& d_te;
+ /** Logic info of theory engine (cached) */
+ const LogicInfo& d_logicInfo;
+ /** The model object we are using */
+ theory::TheoryModel* d_model;
+ /** The model object we have allocated (if one exists) */
+ std::unique_ptr<theory::TheoryModel> d_alocModel;
+ /** The model builder object we are using */
+ theory::TheoryEngineModelBuilder* d_modelBuilder;
+ /** The model builder object we have allocated (if one exists) */
+ std::unique_ptr<theory::TheoryEngineModelBuilder> d_alocModelBuilder;
+ /** 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;
+};
+
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__MODEL_MANAGER__H */
--- /dev/null
+/********************* */
+/*! \file model_manager_distributed.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 distributed approach for model generation.
+ **/
+
+#include "theory/model_manager_distributed.h"
+
+#include "theory/theory_engine.h"
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+namespace theory {
+
+ModelManagerDistributed::ModelManagerDistributed(
+ TheoryEngine& te, EqEngineManagerDistributed& eem)
+ : ModelManager(te), d_eem(eem)
+{
+}
+
+ModelManagerDistributed::~ModelManagerDistributed() {}
+
+bool ModelManagerDistributed::prepareModel()
+{
+ Trace("model-builder") << "ModelManagerDistributed: reset model..."
+ << std::endl;
+
+ // push/pop to clear the equality engine of the model
+ context::Context* meec = d_eem.getModelEqualityEngineContext();
+ meec->pop();
+ meec->push();
+
+ // Collect model info from the theories
+ Trace("model-builder") << "ModelManagerDistributed: Collect model info..."
+ << std::endl;
+ // Consult each active theory to get all relevant information concerning the
+ // model, which includes both dump their equality information and assigning
+ // values. Notice the order of theories here is important and is the same
+ // as the list in CVC4_FOR_EACH_THEORY in theory_engine.cpp.
+ for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
+ ++theoryId)
+ {
+ if (!d_logicInfo.isTheoryEnabled(theoryId))
+ {
+ // theory not active, skip
+ continue;
+ }
+ Theory* t = d_te.theoryOf(theoryId);
+ Trace("model-builder") << " CollectModelInfo on theory: " << theoryId
+ << std::endl;
+ if (!t->collectModelInfo(d_model))
+ {
+ Trace("model-builder")
+ << "ModelManagerDistributed: fail collect model info" << std::endl;
+ return false;
+ }
+ }
+
+ if (!collectModelBooleanVariables())
+ {
+ Trace("model-builder") << "ModelManagerDistributed: fail Boolean variables"
+ << std::endl;
+ return false;
+ }
+
+ return true;
+}
+
+bool ModelManagerDistributed::finishBuildModel() const
+{
+ if (!d_modelBuilder->buildModel(d_model))
+ {
+ Trace("model-builder") << "ModelManager: fail build model" << std::endl;
+ return false;
+ }
+ return true;
+}
+
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file model_manager_distributed.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 distributed approach for model generation.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H
+#define CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H
+
+#include <memory>
+
+#include "theory/ee_manager_distributed.h"
+#include "theory/model_manager.h"
+
+namespace CVC4 {
+
+class TheoryEngine;
+
+namespace theory {
+
+/**
+ * Manager for building models in a distributed architecture. Its prepare
+ * model method uses collectModelInfo to assert all equalities from the equality
+ * engine of each theory into the equality engine of the model. It additionally
+ * uses the model equality engine context to clear the information from
+ * the model's equality engine, as maintained by the distributed equality
+ * engine manager.
+ */
+class ModelManagerDistributed : public ModelManager
+{
+ public:
+ ModelManagerDistributed(TheoryEngine& te, EqEngineManagerDistributed& eem);
+ ~ModelManagerDistributed();
+
+ /** Prepare the model, as described above. */
+ bool prepareModel() override;
+ /**
+ * Assign values to all equivalence classes in the equality engine of the
+ * model, return true if successful.
+ */
+ bool finishBuildModel() const override;
+
+ protected:
+ /**
+ * Distributed equality engine manager, which maintains the context of the
+ * model's equality engine.
+ */
+ EqEngineManagerDistributed& d_eem;
+};
+
+} // namespace theory
+} // namespace CVC4
+
+#endif /* CVC4__THEORY__MODEL_MANAGER_DISTRIBUTED__H */
projects / cvc5.git / commitdiff