From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 26 Feb 2020 08:08:20 +0000 (-0800)
Subject: Remove portfolio leftovers (#3821)
X-Git-Tag: cvc5-1.0.0~3602
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=50c31e61ab240ccd551a0aea732f8b9a88d7fb32;p=cvc5.git

Remove portfolio leftovers (#3821)

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

diff --git a/configure.sh b/configure.sh
index 611ac54ad..ae9b275aa 100755
--- a/configure.sh
+++ b/configure.sh
@@ -64,8 +64,6 @@ The following flags enable optional packages (disable with --no-<option name>).
   --drat2er                use drat2er (required for eager BV proofs)
   --lfsc                   use the LFSC proof checker
   --symfpu                 use SymFPU for floating point solver
-  --portfolio              build the multithreaded portfolio version of CVC4
-                           (pcvc4)
   --readline               support the readline library
 
 Optional Path to Optional Packages:
@@ -131,7 +129,6 @@ glpk=default
 lfsc=default
 muzzle=default
 optimized=default
-portfolio=default
 proofs=default
 replay=default
 shared=default
@@ -248,9 +245,6 @@ do
     --optimized) optimized=ON;;
     --no-optimized) optimized=OFF;;
 
-    --portfolio) portfolio=ON;;
-    --no-portfolio) portfolio=OFF;;
-
     --proofs) proofs=ON;;
     --no-proofs) proofs=OFF;;
 
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4567f45be..e8c38f39d 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -253,10 +253,6 @@ libcvc4_add_sources(
   smt/update_ostream.h
   smt_util/boolean_simplification.cpp
   smt_util/boolean_simplification.h
-  smt_util/lemma_channels.cpp
-  smt_util/lemma_channels.h
-  smt_util/lemma_input_channel.h
-  smt_util/lemma_output_channel.h
   smt_util/nary_builder.cpp
   smt_util/nary_builder.h
   smt_util/node_visitor.h
@@ -944,12 +940,6 @@ install(FILES
           smt/smt_engine.h
         DESTINATION
           ${INCLUDE_INSTALL_DIR}/cvc4/smt)
-install(FILES
-          smt_util/lemma_channels.h
-          smt_util/lemma_input_channel.h
-          smt_util/lemma_output_channel.h
-        DESTINATION
-          ${INCLUDE_INSTALL_DIR}/cvc4/smt_util)
 install(FILES
           theory/logic_info.h
           theory/theory_id.h
diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index b8452d1aa..344387ed9 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -122,7 +122,6 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Model.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Printer.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__options__InstFormatMode.java
-  ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_LemmaChannels.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_Listener.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_ListenerCollection__Registration.java
   ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_MaybeT_CVC4__Rational_t.java
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index c71f4d7a5..3688f592f 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -85,7 +85,6 @@ public:
   static void printStatsFilterZeros(std::ostream& out,
                                     const std::string& statsString);
 
-  LemmaChannels* channels() { return d_smtEngine->channels(); }
   void flushOutputStreams();
 
   void setReplayStream(ExprStream* replayStream);
diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index 84ac7d955..f373e9836 100644
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -78,25 +78,6 @@ header = "options/main_options.h"
   read_only  = true
   help       = "do not run destructors at exit; default on except in debug builds"
 
-[[option]]
-  name       = "fallbackSequential"
-  category   = "regular"
-  long       = "fallback-sequential"
-  type       = "bool"
-  default    = "false"
-  read_only  = true
-  help       = "Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode"
-
-[[option]]
-  name       = "incrementalParallel"
-  category   = "regular"
-  long       = "incremental-parallel"
-  type       = "bool"
-  default    = "false"
-  links      = ["--incremental"]
-  read_only  = true
-  help       = "Use parallel solver even in incremental mode (may print 'unknown's at times)"
-
 [[option]]
   name       = "interactive"
   category   = "regular"
@@ -135,12 +116,3 @@ header = "options/main_options.h"
   default    = "0"
   read_only  = true
   help       = "implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries"
-
-[[option]]
-  name       = "waitToJoin"
-  category   = "expert"
-  long       = "wait-to-join"
-  type       = "bool"
-  default    = "true"
-  read_only  = true
-  help       = "wait for other threads to join before quitting"
diff --git a/src/options/options.h b/src/options/options.h
index 1493ceac9..fcf99134d 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -205,11 +205,9 @@ public:
   bool getDumpSynth() const;
   bool getDumpUnsatCores() const;
   bool getEarlyExit() const;
-  bool getFallbackSequential() const;
   bool getFilesystemAccess() const;
   bool getForceNoLimitCpuWhileDump() const;
   bool getHelp() const;
-  bool getIncrementalParallel() const;
   bool getIncrementalSolving() const;
   bool getInteractive() const;
   bool getInteractivePrompt() const;
@@ -226,7 +224,6 @@ public:
   bool getStrictParsing() const;
   int getTearDownIncremental() const;
   bool getVersion() const;
-  bool getWaitToJoin() const;
   const std::string& getForceLogicString() const;
   int getVerbosity() const;
   std::istream* getIn() const;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 6548150aa..a556f2152 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -82,10 +82,6 @@ bool Options::getEarlyExit() const{
   return (*this)[options::earlyExit];
 }
 
-bool Options::getFallbackSequential() const{
-  return (*this)[options::fallbackSequential];
-}
-
 bool Options::getFilesystemAccess() const{
   return (*this)[options::filesystemAccess];
 }
@@ -98,10 +94,6 @@ bool Options::getHelp() const{
   return (*this)[options::help];
 }
 
-bool Options::getIncrementalParallel() const{
-  return (*this)[options::incrementalParallel];
-}
-
 bool Options::getIncrementalSolving() const{
   return (*this)[options::incrementalSolving];
 }
@@ -166,10 +158,6 @@ bool Options::getVersion() const{
   return (*this)[options::version];
 }
 
-bool Options::getWaitToJoin() const{
-  return (*this)[options::waitToJoin];
-}
-
 const std::string& Options::getForceLogicString() const{
   return (*this)[options::forceLogicString];
 }
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index a9b786615..6b528bb81 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -31,7 +31,6 @@
 #include "proof/proof_manager.h"
 #include "prop/registrar.h"
 #include "prop/theory_proxy.h"
-#include "smt_util/lemma_channels.h"
 
 namespace CVC4 {
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index bac584236..05704c0fa 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -74,19 +74,22 @@ public:
   }
 };
 
-PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext,
-                       Context* userContext, std::ostream* replayLog,
-                       ExprStream* replayStream, LemmaChannels* channels) :
-  d_inCheckSat(false),
-  d_theoryEngine(te),
-  d_decisionEngine(de),
-  d_context(satContext),
-  d_theoryProxy(NULL),
-  d_satSolver(NULL),
-  d_registrar(NULL),
-  d_cnfStream(NULL),
-  d_interrupted(false),
-  d_resourceManager(NodeManager::currentResourceManager())
+PropEngine::PropEngine(TheoryEngine* te,
+                       DecisionEngine* de,
+                       Context* satContext,
+                       Context* userContext,
+                       std::ostream* replayLog,
+                       ExprStream* replayStream)
+    : d_inCheckSat(false),
+      d_theoryEngine(te),
+      d_decisionEngine(de),
+      d_context(satContext),
+      d_theoryProxy(NULL),
+      d_satSolver(NULL),
+      d_registrar(NULL),
+      d_cnfStream(NULL),
+      d_interrupted(false),
+      d_resourceManager(NodeManager::currentResourceManager())
 {
 
   Debug("prop") << "Constructing the PropEngine" << endl;
@@ -97,9 +100,13 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
   d_cnfStream = new CVC4::prop::TseitinCnfStream(
       d_satSolver, d_registrar, userContext, true);
 
-  d_theoryProxy = new TheoryProxy(
-      this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, replayLog,
-      replayStream, channels);
+  d_theoryProxy = new TheoryProxy(this,
+                                  d_theoryEngine,
+                                  d_decisionEngine,
+                                  d_context,
+                                  d_cnfStream,
+                                  replayLog,
+                                  replayStream);
   d_satSolver->initialize(d_context, d_theoryProxy);
 
   d_decisionEngine->setSatSolver(d_satSolver);
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 */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index cf7c9f0d9..557dcc413 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -25,8 +25,6 @@
 #include "proof/cnf_proof.h"
 #include "smt/command.h"
 #include "smt/smt_statistics_registry.h"
-#include "smt_util/lemma_input_channel.h"
-#include "smt_util/lemma_output_channel.h"
 #include "theory/rewriter.h"
 #include "theory/theory_engine.h"
 #include "util/statistics_registry.h"
@@ -41,13 +39,11 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine,
                          context::Context* context,
                          CnfStream* cnfStream,
                          std::ostream* replayLog,
-                         ExprStream* replayStream,
-                         LemmaChannels* channels)
+                         ExprStream* replayStream)
     : d_propEngine(propEngine),
       d_cnfStream(cnfStream),
       d_decisionEngine(decisionEngine),
       d_theoryEngine(theoryEngine),
-      d_channels(channels),
       d_replayLog(replayLog),
       d_replayStream(replayStream),
       d_queue(context),
@@ -61,17 +57,6 @@ TheoryProxy::~TheoryProxy() {
   smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions);
 }
 
-/** The lemma input channel we are using. */
-LemmaInputChannel* TheoryProxy::inputChannel() {
-  return d_channels->getLemmaInputChannel();
-}
-
-/** The lemma output channel we are using. */
-LemmaOutputChannel* TheoryProxy::outputChannel() {
-  return d_channels->getLemmaOutputChannel();
-}
-
-
 void TheoryProxy::variableNotify(SatVariable var) {
   d_theoryEngine->preRegister(getNode(SatLiteral(var)));
 }
@@ -163,56 +148,6 @@ TNode TheoryProxy::getNode(SatLiteral lit) {
 void TheoryProxy::notifyRestart() {
   d_propEngine->spendResource(ResourceManager::Resource::RestartStep);
   d_theoryEngine->notifyRestart();
-
-  static uint32_t lemmaCount = 0;
-
-  if(inputChannel() != NULL) {
-    while(inputChannel()->hasNewLemma()) {
-      Debug("shared") << "shared" << std::endl;
-      Expr lemma = inputChannel()->getNewLemma();
-      Node asNode = lemma.getNode();
-      asNode = theory::Rewriter::rewrite(asNode);
-
-      if(d_shared.find(asNode) == d_shared.end()) {
-        d_shared.insert(asNode);
-        if(asNode.getKind() == kind::OR) {
-          ++lemmaCount;
-          if(lemmaCount % 1 == 0) {
-            Debug("shared") << "=) " << asNode << std::endl;
-          }
-
-          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID);
-        } else {
-          Debug("shared") << "=(" << asNode << std::endl;
-        }
-      } else {
-        Debug("shared") <<"drop shared " << asNode << std::endl;
-      }
-    }
-  }
-}
-
-void TheoryProxy::notifyNewLemma(SatClause& lemma) {
-  Assert(lemma.size() > 0);
-  if(outputChannel() != NULL) {
-    if(lemma.size() == 1) {
-      // cannot share units yet
-      //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr());
-    } else {
-      NodeBuilder<> b(kind::OR);
-      for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) {
-        b << d_cnfStream->getNode(lemma[i]);
-      }
-      Node n = b;
-
-      if(d_shared.find(n) == d_shared.end()) {
-        d_shared.insert(n);
-        outputChannel()->notifyNewLemma(n.toExpr());
-      } else {
-        Debug("shared") <<"drop new " << n << std::endl;
-      }
-    }
-  }
 }
 
 SatLiteral TheoryProxy::getNextReplayDecision() {
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 */
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 2bfb8353f..081e36953 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -877,8 +877,7 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_replayStream(NULL),
       d_private(NULL),
       d_statisticsRegistry(NULL),
-      d_stats(NULL),
-      d_channels(new LemmaChannels())
+      d_stats(NULL)
 {
   SmtScope smts(this);
   d_originalOptions.copyValues(em->getOptions());
@@ -913,8 +912,7 @@ void SmtEngine::finishInit()
   d_theoryEngine = new TheoryEngine(d_context,
                                     d_userContext,
                                     d_private->d_iteRemover,
-                                    const_cast<const LogicInfo&>(d_logic),
-                                    d_channels);
+                                    const_cast<const LogicInfo&>(d_logic));
 
   // Add the theories
   for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
@@ -941,9 +939,12 @@ void SmtEngine::finishInit()
   d_decisionEngine->init();   // enable appropriate strategies
 
   Trace("smt-debug") << "Making prop engine..." << std::endl;
-  d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context,
-                                d_userContext, d_private->getReplayLog(),
-                                d_replayStream, d_channels);
+  d_propEngine = new PropEngine(d_theoryEngine,
+                                d_decisionEngine,
+                                d_context,
+                                d_userContext,
+                                d_private->getReplayLog(),
+                                d_replayStream);
 
   Trace("smt-debug") << "Setting up theory engine..." << std::endl;
   d_theoryEngine->setPropEngine(d_propEngine);
@@ -1107,9 +1108,6 @@ SmtEngine::~SmtEngine()
     delete d_context;
     d_context = NULL;
 
-    delete d_channels;
-    d_channels = NULL;
-
   } catch(Exception& e) {
     Warning() << "CVC4 threw an exception during cleanup." << endl
               << e << endl;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a91a3a201..0ef22f353 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -32,7 +32,6 @@
 #include "options/options.h"
 #include "proof/unsat_core.h"
 #include "smt/logic_exception.h"
-#include "smt_util/lemma_channels.h"
 #include "theory/logic_info.h"
 #include "util/hash.h"
 #include "util/proof.h"
@@ -798,8 +797,6 @@ class CVC4_PUBLIC SmtEngine
    */
   void beforeSearch();
 
-  LemmaChannels* channels() { return d_channels; }
-
   /**
    * Expermintal feature: Sets the sequence of decisions.
    * This currently requires very fine grained knowledge about literal
@@ -1243,9 +1240,6 @@ class CVC4_PUBLIC SmtEngine
 
   smt::SmtEngineStatistics* d_stats;
 
-  /** Container for the lemma input and output channels for this SmtEngine.*/
-  LemmaChannels* d_channels;
-
   /*---------------------------- sygus commands  ---------------------------*/
 
   /**
diff --git a/src/smt_util/lemma_channels.cpp b/src/smt_util/lemma_channels.cpp
deleted file mode 100644
index d65a2596e..000000000
--- a/src/smt_util/lemma_channels.cpp
+++ /dev/null
@@ -1,54 +0,0 @@
-/*********************                                                        */
-/*! \file lemma_channels.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief This class is a light container for globals that used to live
- ** in options. This is NOT a good long term solution, but is a reasonable
- ** stop gap.
- **
- ** This class is a light container for globals that used to live
- ** in options. This is NOT a good long term solution, but is a reasonable
- ** stop gap.
- **/
-
-#include "smt_util/lemma_channels.h"
-
-#include <cerrno>
-#include <iostream>
-#include <string>
-#include <utility>
-
-#include "cvc4autoconfig.h" // Needed for CVC4_REPLAY
-#include "expr/expr_stream.h"
-#include "options/open_ostream.h"
-#include "options/option_exception.h"
-#include "options/parser_options.h"
-#include "smt_util/lemma_input_channel.h"
-#include "smt_util/lemma_output_channel.h"
-
-namespace CVC4 {
-
-LemmaChannels::LemmaChannels()
-    : d_lemmaInputChannel(NULL)
-    , d_lemmaOutputChannel(NULL)
-{}
-
-LemmaChannels::~LemmaChannels(){}
-
-void LemmaChannels::setLemmaInputChannel(LemmaInputChannel* in) {
-  d_lemmaInputChannel = in;
-}
-
-void LemmaChannels::setLemmaOutputChannel(LemmaOutputChannel* out) {
-  d_lemmaOutputChannel = out;
-}
-
-
-} /* namespace CVC4 */
diff --git a/src/smt_util/lemma_channels.h b/src/smt_util/lemma_channels.h
deleted file mode 100644
index 40c58dd24..000000000
--- a/src/smt_util/lemma_channels.h
+++ /dev/null
@@ -1,77 +0,0 @@
-/*********************                                                        */
-/*! \file lemma_channels.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Tim King, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief LemmaChannels is a light container for a pair of input and output
- ** lemma channels.
- **
- ** LemmaChannels is a light container for a pair of input and output
- ** lemma channels. These contain paramaters for the infrequently
- ** used Portfolio mode. There should be exactly one of these per SmtEngine
- ** with the same lifetime as the SmtEngine. The user directly passes these as
- ** pointers and is resonsible for cleaning up the memory.
- **
- ** Basically, the problem this class is solving is that previously these were
- ** using smt_options.h and the Options class as globals for these same
- ** datastructures.
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__SMT_UTIL__LEMMA_CHANNELS_H
-#define CVC4__SMT_UTIL__LEMMA_CHANNELS_H
-
-#include <iosfwd>
-#include <string>
-#include <utility>
-
-#include "options/option_exception.h"
-#include "smt_util/lemma_input_channel.h"
-#include "smt_util/lemma_output_channel.h"
-
-namespace CVC4 {
-
-/**
- * LemmaChannels is a wrapper around two pointers:
- * - getLemmaInputChannel()
- * - getLemmaOutputChannel()
- *
- * The user can directly set these and is responsible for handling the
- * memory for these. These datastructures are used for Portfolio mode.
- */
-class CVC4_PUBLIC LemmaChannels {
- public:
-  /** Creates an empty LemmaChannels with all 4 pointers initially NULL. */
-  LemmaChannels();
-  ~LemmaChannels();
-
-  void setLemmaInputChannel(LemmaInputChannel* in);
-  LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; }
-
-  void setLemmaOutputChannel(LemmaOutputChannel* out);
-  LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; }
-
- private:
-  // Disable copy constructor.
-  LemmaChannels(const LemmaChannels&) = delete;
-
-  // Disable assignment operator.
-  LemmaChannels& operator=(const LemmaChannels&) = delete;
-
-  /** This captures the old options::lemmaInputChannel .*/
-  LemmaInputChannel* d_lemmaInputChannel;
-
-  /** This captures the old options::lemmaOutputChannel .*/
-  LemmaOutputChannel* d_lemmaOutputChannel;
-}; /* class LemmaChannels */
-
-} /* namespace CVC4 */
-
-#endif /* CVC4__SMT_UTIL__LEMMA_CHANNELS_H */
diff --git a/src/smt_util/lemma_input_channel.h b/src/smt_util/lemma_input_channel.h
deleted file mode 100644
index 16bb457c8..000000000
--- a/src/smt_util/lemma_input_channel.h
+++ /dev/null
@@ -1,38 +0,0 @@
-/*********************                                                        */
-/*! \file lemma_input_channel.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__LEMMA_INPUT_CHANNEL_H
-#define CVC4__LEMMA_INPUT_CHANNEL_H
-
-#include "expr/expr.h"
-
-namespace CVC4 {
-
-class CVC4_PUBLIC LemmaInputChannel {
-public:
- virtual ~LemmaInputChannel() {}
-
- virtual bool hasNewLemma() = 0;
- virtual Expr getNewLemma() = 0;
-
-};/* class LemmaOutputChannel */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__LEMMA_INPUT_CHANNEL_H */
diff --git a/src/smt_util/lemma_output_channel.h b/src/smt_util/lemma_output_channel.h
deleted file mode 100644
index e5c5cffe2..000000000
--- a/src/smt_util/lemma_output_channel.h
+++ /dev/null
@@ -1,45 +0,0 @@
-/*********************                                                        */
-/*! \file lemma_output_channel.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
- ** All rights reserved.  See the file COPYING in the top-level source
- ** directory for licensing information.\endverbatim
- **
- ** \brief Mechanism for communication about new lemmas
- **
- ** This file defines an interface for use by the theory and propositional
- ** engines to communicate new lemmas to the "outside world".
- **/
-
-#include "cvc4_public.h"
-
-#ifndef CVC4__LEMMA_OUTPUT_CHANNEL_H
-#define CVC4__LEMMA_OUTPUT_CHANNEL_H
-
-#include "expr/expr.h"
-
-namespace CVC4 {
-
-/**
- * This interface describes a mechanism for the propositional and theory
- * engines to communicate with the "outside world" about new lemmas being
- * discovered.
- */
-class CVC4_PUBLIC LemmaOutputChannel {
-public:
- virtual ~LemmaOutputChannel() {}
-
- /**
-  * Notifies this output channel that there's a new lemma.
-  * The lemma may or may not be in CNF.
-  */
- virtual void notifyNewLemma(Expr lemma) = 0;
-};/* class LemmaOutputChannel */
-
-}/* CVC4 namespace */
-
-#endif /* CVC4__LEMMA_OUTPUT_CHANNEL_H */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 9ef228865..dec648688 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -37,7 +37,6 @@
 #include "proof/theory_proof.h"
 #include "smt/logic_exception.h"
 #include "smt/term_formula_removal.h"
-#include "smt_util/lemma_output_channel.h"
 #include "smt_util/node_visitor.h"
 #include "theory/arith/arith_ite_utils.h"
 #include "theory/bv/theory_bv_utils.h"
@@ -314,8 +313,7 @@ void TheoryEngine::eqNotifyNewClass(TNode t){
 TheoryEngine::TheoryEngine(context::Context* context,
                            context::UserContext* userContext,
                            RemoveTermFormulas& iteRemover,
-                           const LogicInfo& logicInfo,
-                           LemmaChannels* channels)
+                           const LogicInfo& logicInfo)
     : d_propEngine(nullptr),
       d_decisionEngine(nullptr),
       d_context(context),
@@ -349,7 +347,6 @@ TheoryEngine::TheoryEngine(context::Context* context,
       d_false(),
       d_interrupted(false),
       d_resourceManager(NodeManager::currentResourceManager()),
-      d_channels(channels),
       d_inPreregister(false),
       d_factsAsserted(context, false),
       d_preRegistrationVisitor(this, context),
@@ -1867,11 +1864,6 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node,
                      << CheckSatCommand(n.toExpr());
   }
 
-  // Share with other portfolio threads
-  if(d_channels->getLemmaOutputChannel() != NULL) {
-    d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr());
-  }
-
   AssertionPipeline additionalLemmas;
 
   // Run theory preprocessing, maybe
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 0770efc7b..a5631059f 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -34,7 +34,6 @@
 #include "options/theory_options.h"
 #include "prop/prop_engine.h"
 #include "smt/command.h"
-#include "smt_util/lemma_channels.h"
 #include "theory/atom_requests.h"
 #include "theory/decision_manager.h"
 #include "theory/interrupted.h"
@@ -468,15 +467,12 @@ class TheoryEngine {
   bool d_interrupted;
   ResourceManager* d_resourceManager;
 
-  /** Container for lemma input and output channels. */
-  LemmaChannels* d_channels;
-
-public:
-
+ public:
   /** Constructs a theory engine */
-  TheoryEngine(context::Context* context, context::UserContext* userContext,
-               RemoveTermFormulas& iteRemover, const LogicInfo& logic,
-               LemmaChannels* channels);
+  TheoryEngine(context::Context* context,
+               context::UserContext* userContext,
+               RemoveTermFormulas& iteRemover,
+               const LogicInfo& logic);
 
   /** Destroys a theory engine */
   ~TheoryEngine();
@@ -491,12 +487,15 @@ public:
    * there is another theory it will be deleted.
    */
   template <class TheoryClass>
-  inline void addTheory(theory::TheoryId theoryId) {
+  inline void addTheory(theory::TheoryId theoryId)
+  {
     Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
     d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId);
-    d_theoryTable[theoryId] =
-        new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId],
-                        theory::Valuation(this), d_logicInfo);
+    d_theoryTable[theoryId] = new TheoryClass(d_context,
+                                              d_userContext,
+                                              *d_theoryOut[theoryId],
+                                              theory::Valuation(this),
+                                              d_logicInfo);
   }
 
   inline void setPropEngine(prop::PropEngine* propEngine) {
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 70357ea1b..62ba6f7da 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -146,7 +146,7 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     d_cnfContext = new context::Context();
     d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine);
     d_cnfStream = new CVC4::prop::TseitinCnfStream(
-        d_satSolver, d_cnfRegistrar, d_cnfContext, d_smt->channels());
+        d_satSolver, d_cnfRegistrar, d_cnfContext);
   }
 
   void tearDown() override