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.

5 files changed, 437 insertions, 0 deletions

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<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
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 <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 */
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 <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 */