Move decision manager into theory inference manager (#6231)

This makes it so that the decision manager is accessible from TheoryInferenceManager.

This is work towards breaking circular dependencies in quantifiers, and also helps simplify several other dependencies in e.g. UF and datatypes.

1 files changed, 11 insertions, 2 deletions

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 549d81c16..dca11524b 100644
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -36,6 +36,7 @@ namespace theory {
 
 class Theory;
 class TheoryState;
+class DecisionManager;
 namespace eq {
 class EqualityEngine;
 class ProofEqEngine;
@@ -90,16 +91,22 @@ class TheoryInferenceManager
                          const std::string& name,
                          bool cacheLemmas = true);
   virtual ~TheoryInferenceManager();
+  //--------------------------------------- initialization
   /**
    * Set equality engine, ee is a pointer to the official equality engine
    * of theory.
    */
   void setEqualityEngine(eq::EqualityEngine* ee);
+  /** Set the decision manager */
+  void setDecisionManager(DecisionManager* dm);
+  //--------------------------------------- end initialization
   /**
    * Are proofs enabled in this inference manager? Returns true if the proof
    * node manager pnm provided to the constructor of this class was non-null.
    */
   bool isProofEnabled() const;
+  /** Get the underlying proof equality engine */
+  eq::ProofEqEngine* getProofEqEngine();
   /**
    * Reset, which resets counters regarding the number of added lemmas and
    * internal facts. This method should be manually called by the theory at
@@ -116,8 +123,6 @@ class TheoryInferenceManager
    * since the last call to reset.
    */
   bool hasSent() const;
-  /** Get the underlying proof equality engine */
-  eq::ProofEqEngine* getProofEqEngine();
   //--------------------------------------- propagations
   /**
    * T-propagate literal lit, possibly encountered by equality engine,
@@ -344,6 +349,8 @@ class TheoryInferenceManager
   /** Have we added a internal fact since the last call to reset? */
   bool hasSentFact() const;
   //--------------------------------------- phase requirements
+  /** Get the decision manager, which manages decision strategies. */
+  DecisionManager* getDecisionManager();
   /**
    * Set that literal n has SAT phase requirement pol, that is, it should be
    * decided with polarity pol, for details see OutputChannel::requirePhase.
@@ -418,6 +425,8 @@ class TheoryInferenceManager
   OutputChannel& d_out;
   /** Pointer to equality engine of the theory. */
   eq::EqualityEngine* d_ee;
+  /** Pointer to the decision manager */
+  DecisionManager* d_decManager;
   /** A proof equality engine */
   std::unique_ptr<eq::ProofEqEngine> d_pfee;
   /** The proof node manager of the theory */