From 6d53928cd9f16385d81124916311c372ec20b5ed Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 24 Aug 2020 13:16:04 -0500 Subject: [PATCH] Add the distributed model manager (#4934) 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. --- src/CMakeLists.txt | 4 + src/theory/model_manager.cpp | 166 +++++++++++++++++++++++ src/theory/model_manager.h | 115 ++++++++++++++++ src/theory/model_manager_distributed.cpp | 88 ++++++++++++ src/theory/model_manager_distributed.h | 64 +++++++++ 5 files changed, 437 insertions(+) create mode 100644 src/theory/model_manager.cpp create mode 100644 src/theory/model_manager.h create mode 100644 src/theory/model_manager_distributed.cpp create mode 100644 src/theory/model_manager_distributed.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index c9eaede9a..83cd363f6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -508,6 +508,10 @@ libcvc4_add_sources( 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 diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp new file mode 100644 index 000000000..1451b6ab0 --- /dev/null +++ b/src/theory/model_manager.cpp @@ -0,0 +1,166 @@ +/********************* */ +/*! \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 boolVars; + propEngine->getBooleanVariables(boolVars); + std::vector::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 diff --git a/src/theory/model_manager.h b/src/theory/model_manager.h new file mode 100644 index 000000000..12b99dc18 --- /dev/null +++ b/src/theory/model_manager.h @@ -0,0 +1,115 @@ +/********************* */ +/*! \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 + +#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 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 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 */ diff --git a/src/theory/model_manager_distributed.cpp b/src/theory/model_manager_distributed.cpp new file mode 100644 index 000000000..c2e1d6521 --- /dev/null +++ b/src/theory/model_manager_distributed.cpp @@ -0,0 +1,88 @@ +/********************* */ +/*! \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 diff --git a/src/theory/model_manager_distributed.h b/src/theory/model_manager_distributed.h new file mode 100644 index 000000000..2f86c0b00 --- /dev/null +++ b/src/theory/model_manager_distributed.h @@ -0,0 +1,64 @@ +/********************* */ +/*! \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 + +#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 */ -- 2.30.2