1 files changed, 5 insertions, 21 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 61c556f34..0d76b473f 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -30,9 +30,6 @@
 #include "expr/expr_stream.h"
 #include "expr/node.h"
 #include "prop/sat_solver.h"
-#include "smt_util/lemma_channels.h"
-#include "smt_util/lemma_input_channel.h"
-#include "smt_util/lemma_output_channel.h"
 #include "theory/theory.h"
 #include "util/resource_manager.h"
 #include "util/statistics_registry.h"
@@ -50,20 +47,19 @@ class CnfStream;
 /**
  * The proxy class that allows the SatSolver to communicate with the theories
  */
-class TheoryProxy {
-public:
+class TheoryProxy
+{
+ public:
   TheoryProxy(PropEngine* propEngine,
               TheoryEngine* theoryEngine,
               DecisionEngine* decisionEngine,
               context::Context* context,
               CnfStream* cnfStream,
               std::ostream* replayLog,
-              ExprStream* replayStream,
-              LemmaChannels* globals);
+              ExprStream* replayStream);
 
   ~TheoryProxy();
 
-
   void theoryCheck(theory::Theory::Effort effort);
 
   void explainPropagation(SatLiteral l, SatClause& explanation);
@@ -87,8 +83,6 @@ public:
 
   void notifyRestart();
 
-  void notifyNewLemma(SatClause& lemma);
-
   SatLiteral getNextReplayDecision();
 
   void logDecision(SatLiteral lit);
@@ -117,22 +111,12 @@ public:
   /** The theory engine we are using. */
   TheoryEngine* d_theoryEngine;
 
-
-  /** Container for inputChannel() and outputChannel(). */
-  LemmaChannels* d_channels;
-
   /** Stream on which to log replay events. */
   std::ostream* d_replayLog;
 
   /** Stream for replaying decisions. */
   ExprStream* d_replayStream;
 
-  /** The lemma input channel we are using. */
-  LemmaInputChannel* inputChannel();
-
-  /** The lemma output channel we are using. */
-  LemmaOutputChannel* outputChannel();
-
   /** Queue of asserted facts */
   context::CDQueue<TNode> d_queue;
 
@@ -147,7 +131,7 @@ public:
    */
   IntStat d_replayedDecisions;
 
-};/* class SatSolver */
+}; /* class SatSolver */
 
 }/* CVC4::prop namespace */