Connect combination engine to theory engine (#4940)

This connects the implementation of CombinationEngine into TheoryEngine. By default, the combination engine of theory engine is CombinationCareGraph.

This PR also consolidates and simplifies how models are built, note that:

The TheoryModel object no longer tracks whether it is built, instead that is the job of ModelManager,
The TheoryModelBuilder object is no longer responsible for calling TheoryEngine's collect model info method.
Quantifiers engine uses a simpler interface for ensuring that TheoryEngine's model is built.
This PR also makes some minor simplifications to TheoryEngine from the centralEe branch.

Note that no significant behavior changes are intended in this PR.

1 files changed, 12 insertions, 9 deletions

diff --git a/src/theory/theory_model_builder.h b/src/theory/theory_model_builder.h
index 0be92c95c..898ca7dbc 100644
--- a/src/theory/theory_model_builder.h
+++ b/src/theory/theory_model_builder.h
@@ -46,19 +46,22 @@ class TheoryEngineModelBuilder
  public:
   TheoryEngineModelBuilder(TheoryEngine* te);
   virtual ~TheoryEngineModelBuilder() {}
-  /** Build model function.
-   *
-   * Should be called only on TheoryModels m.
+  /**
+   * Should be called only on models m after they have been prepared
+   * (e.g. using ModelManager). In other words, the equality engine of model
+   * m contains all relevant information from each theory that is needed
+   * for building a model. This class is responsible simply for ensuring
+   * that all equivalence classes of the equality engine of m are assigned
+   * constants.
    *
    * This constructs the model m, via the following steps:
-   * (1) call TheoryEngine::collectModelInfo,
-   * (2) builder-specified pre-processing,
-   * (3) find the equivalence classes of m's
+   * (1) builder-specified pre-processing,
+   * (2) find the equivalence classes of m's
    *     equality engine that initially contain constants,
-   * (4) assign constants to all equivalence classes
+   * (3) assign constants to all equivalence classes
    *     of m's equality engine, through alternating
    *     iterations of evaluation and enumeration,
-   * (5) builder-specific processing, which includes assigning total
+   * (4) builder-specific processing, which includes assigning total
    *     interpretations to uninterpreted functions.
    *
    * This function returns false if any of the above
@@ -67,7 +70,7 @@ class TheoryEngineModelBuilder
    * builder in steps (2) or (5), for instance, if the model we
    * are building fails to satisfy a quantified formula.
    */
-  bool buildModel(Model* m);
+  bool buildModel(TheoryModel* m);
 
   /** postprocess model
    *