Remove portfolio leftovers (#3821)

Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.

1 files changed, 14 insertions, 10 deletions

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index efbd82947..42b3ce65f 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -28,7 +28,6 @@
 #include "expr/node.h"
 #include "options/options.h"
 #include "proof/proof_manager.h"
-#include "smt_util/lemma_channels.h"
 #include "util/resource_manager.h"
 #include "util/result.h"
 #include "util/unsafe_interrupt_exception.h"
@@ -94,14 +93,16 @@ class PropEngine {
   /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
 
-public:
-
+ public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext,
-             context::Context* userContext, std::ostream* replayLog,
-             ExprStream* replayStream, LemmaChannels* channels);
+  PropEngine(TheoryEngine*,
+             DecisionEngine*,
+             context::Context* satContext,
+             context::Context* userContext,
+             std::ostream* replayLog,
+             ExprStream* replayStream);
 
   /**
    * Destructor.
@@ -115,7 +116,7 @@ public:
    * PropEngine and Theory).  For now, there's nothing to do here in
    * the PropEngine.
    */
-  void shutdown() { }
+  void shutdown() {}
 
   /**
    * Converts the given formula to CNF and assert the CNF to the SAT solver.
@@ -135,7 +136,11 @@ public:
    * @param removable whether this lemma can be quietly removed based
    * on an activity heuristic (or not)
    */
-  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null());
+  void assertLemma(TNode node,
+                   bool negated,
+                   bool removable,
+                   ProofRule rule,
+                   TNode from = TNode::null());
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
@@ -243,8 +248,7 @@ public:
    */
   bool properExplanation(TNode node, TNode expl) const;
 
-};/* class PropEngine */
-
+}; /* class PropEngine */
 
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */