Use InferenceManager in ExtTheory (#7006)

This PR refactors the ExtTheory class to use a given inference manager instead of a given output channel.

1 files changed, 5 insertions, 4 deletions

diff --git a/src/theory/ext_theory.h b/src/theory/ext_theory.h
index f5e08e2f5..01b191e0a 100644
--- a/src/theory/ext_theory.h
+++ b/src/theory/ext_theory.h
@@ -41,6 +41,7 @@
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "theory/theory_inference_manager.h"
 
 namespace cvc5 {
 namespace theory {
@@ -176,7 +177,7 @@ class ExtTheory
   ExtTheory(ExtTheoryCallback& p,
             context::Context* c,
             context::UserContext* u,
-            OutputChannel& out);
+            TheoryInferenceManager& im);
   virtual ~ExtTheory() {}
   /** Tells this class to treat terms with Kind k as extended functions */
   void addFunctionKind(Kind k) { d_extf_kind[k] = true; }
@@ -291,11 +292,11 @@ class ExtTheory
                             bool batch,
                             bool isRed);
   /** send lemma on the output channel */
-  bool sendLemma(Node lem, bool preprocess = false);
+  bool sendLemma(Node lem, InferenceId id, bool preprocess = false);
   /** reference to the callback */
   ExtTheoryCallback& d_parent;
-  /** Reference to the output channel we are using */
-  OutputChannel& d_out;
+  /** inference manager used to send lemmas */
+  TheoryInferenceManager& d_im;
   /** the true node */
   Node d_true;
   /** extended function terms, map to whether they are active */