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, 15 insertions, 13 deletions

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 549f4078e..ff4c3bdf9 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -87,23 +87,24 @@ struct NodeTheoryPairHashFunction {
 
 /* Forward declarations */
 namespace theory {
-  class TheoryModel;
-  class TheoryEngineModelBuilder;
-  class EqEngineManagerDistributed;
+class CombinationEngine;
+class TheoryModel;
+class TheoryEngineModelBuilder;
+class EqEngineManagerDistributed;
 
-  class DecisionManager;
-  class RelevanceManager;
+class DecisionManager;
+class RelevanceManager;
 
-  namespace eq {
-    class EqualityEngine;
-  }/* CVC4::theory::eq namespace */
+namespace eq {
+class EqualityEngine;
+}  // namespace eq
 
-  namespace quantifiers {
-    class TermDb;
-  }
+namespace quantifiers {
+class TermDb;
+}
 
-  class EntailmentCheckParameters;
-  class EntailmentCheckSideEffects;
+class EntailmentCheckParameters;
+class EntailmentCheckSideEffects;
 }/* CVC4::theory namespace */
 
 class RemoveTermFormulas;
@@ -118,6 +119,7 @@ class TheoryEngine {
 
   /** Shared terms database can use the internals notify the theories */
   friend class SharedTermsDatabase;
+  friend class theory::CombinationEngine;
   friend class theory::quantifiers::TermDb;
   friend class theory::EngineOutputChannel;