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.

1 files changed, 122 insertions, 0 deletions

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