Single driver for both sequential and portfolio

A "command executer" layer between parsing commands and invoking them.

New implementation of portfolio driver splits only when check-sat or query
command is encountered, and then switches back to sequential till the next
one. As side effect, restores functionality of interactive mode and
push/pops.

15 files changed, 944 insertions, 913 deletions

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index b058292f3..1e4a266a5 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -419,7 +419,9 @@ CommandSequence::const_iterator CommandSequence::begin() const throw() {
 Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
   CommandSequence* seq = new CommandSequence();
   for(iterator i = begin(); i != end(); ++i) {
-    seq->addCommand((*i)->exportTo(exprManager, variableMap));
+    Command* cmd_to_export = *i;
+    Command* cmd = cmd_to_export->exportTo(exprManager, variableMap);
+    seq->addCommand(cmd);
   }
   seq->d_index = d_index;
   return seq;
@@ -1197,8 +1199,12 @@ void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
 }
 
 Command* DatatypeDeclarationCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  Warning() << "We currently do not support exportTo with Datatypes" << std::endl;
-  return NULL;
+  throw ExportToUnsupportedException();
+  // vector<DatatypeType> params;
+  // transform(d_datatypes.begin(), d_datatypes.end(), back_inserter(params),
+  //           ExportTransformer(exprManager, variableMap));
+  // DatatypeDeclarationCommand* c = new DatatypeDeclarationCommand(params);
+  // return c;
 }
 
 Command* DatatypeDeclarationCommand::clone() const {
diff --git a/src/expr/command.h b/src/expr/command.h
index 0f517e7f2..3c919c374 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -50,6 +50,14 @@ std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
 
+class ExportToUnsupportedException : public Exception {
+public:
+  ExportToUnsupportedException() throw() :
+    Exception("exportTo unsupported for command") {
+  }
+};/* class NoMoreValuesException */
+
+
 /** The status an SMT benchmark can have */
 enum BenchmarkStatus {
   /** Benchmark is satisfiable */
@@ -233,7 +241,8 @@ public:
    * variableMap for the translation and extending it with any new
    * mappings.
    */
-  virtual Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) = 0;
+  virtual Command* exportTo(ExprManager* exprManager,
+                            ExprManagerMapCollection& variableMap) = 0;
 
   /**
    * Clone this Command (make a shallow copy).
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index a6f9f2cf6..4009bc610 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -131,7 +131,19 @@ Node exportInternal(TNode n, ExprManager* from, ExprManager* to, ExprManagerMapC
         // temporarily set the node manager to NULL; this gets around
         // a check that mkVar isn't called internally
         NodeManagerScope nullScope(NULL);
-        to_e = to->mkVar(name, type);// FIXME thread safety
+
+        if(n.getKind() == kind::BOUND_VAR_LIST) {
+          to_e = to->mkBoundVar(name, type);// FIXME thread safety
+        } else if(n.getKind() == kind::VARIABLE) {
+          to_e = to->mkVar(name, type);// FIXME thread safety
+        } else if(n.getKind() == kind::SKOLEM) {
+          Assert(false, "Skolem exporting not yet supported properly.");
+          // to fix this, get the node manager and do the appropriate
+          to_e = to->mkVar(name, type);// FIXME thread safety
+        } else {
+          Unhandled();
+        }
+
         Debug("export") << "+ exported var `" << from_e << "'[" << from_e.getId() << "] with name `" << name << "' and type `" << from_e.getType() << "' to `" << to_e << "'[" << to_e.getId() << "] with type `" << type << "'" << std::endl;
       } else {
         // temporarily set the node manager to NULL; this gets around
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index c1291e7ec..9b0200231 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -19,14 +19,17 @@ pcvc4_SOURCES = \
 	main.cpp \
 	portfolio.cpp \
 	portfolio.h \
-	driver_portfolio.cpp
+	portfolio_util.cpp \
+	command_executer.cpp \
+	command_executer_portfolio.cpp \
+	driver_unified.cpp
 pcvc4_LDADD = \
 	libmain.a \
 	@builddir@/../parser/libcvc4parser.la \
 	@builddir@/../libcvc4.la \
 	@builddir@/../lib/libreplacements.la \
 	$(READLINE_LIBS)
-pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS)
+pcvc4_CPPFLAGS = $(AM_CPPFLAGS) $(BOOST_CPPFLAGS) -DPORTFOLIO_BUILD
 pcvc4_LDADD += $(BOOST_THREAD_LIBS) -lpthread
 pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS)
 
@@ -39,7 +42,8 @@ endif
 
 cvc4_SOURCES = \
 	main.cpp \
-	driver.cpp
+	command_executer.cpp \
+	driver_unified.cpp
 cvc4_LDADD = \
 	libmain.a \
 	@builddir@/../parser/libcvc4parser.la \
diff --git a/src/main/command_executer.cpp b/src/main/command_executer.cpp
new file mode 100644
index 000000000..039ab664c
--- /dev/null
+++ b/src/main/command_executer.cpp
@@ -0,0 +1,93 @@
+/*********************                                                        */
+/*! \file command_executer.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** Minor contributors (to current version): 
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An additional layer between commands and invoking them.
+ **/
+
+#include <iostream>
+
+#include "main/command_executer.h"
+#include "expr/command.h"
+
+#include "main/main.h"
+
+namespace CVC4 {
+namespace main {
+
+
+CommandExecuter::CommandExecuter(ExprManager &exprMgr, Options &options):
+  d_exprMgr(exprMgr),
+  d_smtEngine(SmtEngine(&exprMgr)),
+  d_options(options) {
+  
+  // signal handlers need access
+  main::pStatistics = d_smtEngine.getStatisticsRegistry();
+  d_exprMgr.getStatisticsRegistry()->setName("ExprManager");
+  main::pStatistics->registerStat_(d_exprMgr.getStatisticsRegistry());
+}
+
+bool CommandExecuter::doCommand(Command* cmd)
+{
+  if( d_options[options::parseOnly] ) {
+    return true;
+  }
+
+  CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
+  if(seq != NULL) {
+    // assume no error
+    bool status = true;
+
+    for(CommandSequence::iterator subcmd = seq->begin();
+        status && subcmd != seq->end();
+        ++subcmd) {
+      status = doCommand(*subcmd);
+    }
+
+    return status;
+  } else {
+    if(d_options[options::verbosity] > 0) {
+      *d_options[options::out] << "Invoking: " << *cmd << std::endl;
+    }
+
+    return doCommandSingleton(cmd);
+  }
+}
+
+bool CommandExecuter::doCommandSingleton(Command *cmd)
+{
+  bool status = true;
+  if(d_options[options::verbosity] >= 0) {
+    status = smtEngineInvoke(&d_smtEngine, cmd, d_options[options::out]);
+  } else {
+    status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
+  }
+  return status;
+}
+
+std::string CommandExecuter::getSmtEngineStatus()
+{
+  return d_smtEngine.getInfo("status").getValue();
+}
+
+bool smtEngineInvoke(SmtEngine* smt, Command* cmd, std::ostream *out)
+{
+  if(out == NULL) {
+    cmd->invoke(smt);
+  } else {
+    cmd->invoke(smt, *out);
+  }
+  return !cmd->fail();
+}
+
+}/*main namespace*/
+}/*CVC4 namespace*/
diff --git a/src/main/command_executer.h b/src/main/command_executer.h
new file mode 100644
index 000000000..245857c04
--- /dev/null
+++ b/src/main/command_executer.h
@@ -0,0 +1,69 @@
+/*********************                                                        */
+/*! \file command_executer.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): 
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An additional layer between commands and invoking them.
+ **/
+
+#ifndef __CVC4__COMMAND_EXECUTER_H
+#define __CVC4__COMMAND_EXECUTER_H
+
+#include "expr/expr_manager.h"
+#include "smt/smt_engine.h"
+
+namespace CVC4 {
+
+namespace main {
+
+class CommandExecuter {
+
+protected:
+  ExprManager& d_exprMgr;
+  SmtEngine d_smtEngine;
+  Options& d_options;
+
+public:
+  // Note: though the options are not cached (instead a reference is
+  // used), the portfolio command executer currently parses them
+  // during initalization, creating thread-specific options and
+  // storing them
+  CommandExecuter(ExprManager &exprMgr, Options &options);
+
+  ~CommandExecuter() {}
+
+  /**
+   * Executes a command. Recursively handles if cmd is a command
+   * sequence.  Eventually uses doCommandSingleton (which can be
+   * overridden by a derived class).
+   */
+  bool doCommand(CVC4::Command* cmd);
+
+  virtual std::string getSmtEngineStatus();
+
+protected:
+  /** Executes treating cmd as a singleton */
+  virtual bool doCommandSingleton(CVC4::Command* cmd);
+
+private:
+  CommandExecuter();
+
+};
+
+bool smtEngineInvoke(SmtEngine* smt,
+                     Command* cmd,
+                     std::ostream *out);
+
+
+}/*main namespace*/
+}/*CVC4 namespace*/
+
+#endif  /* __CVC4__COMMAND_EXECUTER_H */
diff --git a/src/main/command_executer_portfolio.cpp b/src/main/command_executer_portfolio.cpp
new file mode 100644
index 000000000..85180c9a9
--- /dev/null
+++ b/src/main/command_executer_portfolio.cpp
@@ -0,0 +1,314 @@
+/*********************                                                        */
+/*! \file command_executer_portfolio.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: mdeters, taking
+ ** Minor contributors (to current version): 
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An additional layer between commands and invoking them.
+ **
+ ** The portfolio executer branches check-sat queries to several
+ ** threads.
+ **/
+
+#include <boost/thread.hpp>
+#include <boost/thread/condition.hpp>
+#include <boost/exception_ptr.hpp>
+#include <boost/lexical_cast.hpp>
+
+#include "expr/command.h"
+#include "expr/pickler.h"
+#include "main/command_executer_portfolio.h"
+#include "main/main.h"
+#include "main/options.h"
+#include "main/portfolio.h"
+#include "options/options.h"
+#include "smt/options.h"
+
+using namespace std;
+
+namespace CVC4 {
+namespace main {
+
+CommandExecuterPortfolio::CommandExecuterPortfolio
+(ExprManager &exprMgr, Options &options, vector<Options>& tOpts):
+  CommandExecuter(exprMgr, options),
+  d_numThreads(options[options::threads]),
+  d_smts(),
+  d_seq(new CommandSequence()),
+  d_threadOptions(tOpts),
+  d_vmaps(),
+  d_lastWinner(0),
+  d_channelsOut(),
+  d_channelsIn(),
+  d_ostringstreams()
+{
+  Assert(d_threadOptions.size() == d_numThreads);
+
+  /* Duplication, Individualisation */
+  d_exprMgrs.push_back(&d_exprMgr);
+  for(unsigned i = 1; i < d_numThreads; ++i) {
+    d_exprMgrs.push_back(new ExprManager(d_threadOptions[i]));
+  }
+
+  // Create the SmtEngine(s)
+  d_smts.push_back(&d_smtEngine);
+  for(unsigned i = 1; i < d_numThreads; ++i) {
+    d_smts.push_back(new SmtEngine(d_exprMgrs[i]));
+  }
+
+  for(unsigned i = 1; i < d_numThreads; ++i) {
+    // Register the statistics registry of the thread
+    string emTag = "ExprManager thread #" 
+      + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+    string smtTag = "SmtEngine thread #" 
+      + boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+    d_exprMgrs[i]->getStatisticsRegistry()->setName(emTag);
+    d_smts[i]->getStatisticsRegistry()->setName(smtTag);
+    pStatistics->registerStat_
+      (d_exprMgrs[i]->getStatisticsRegistry() );
+    pStatistics->registerStat_
+      (d_smts[i]->getStatisticsRegistry() );
+  }
+
+  Assert(d_vmaps.size() == 0);
+  for(unsigned i = 0; i < d_numThreads; ++i) {
+    d_vmaps.push_back(new ExprManagerMapCollection());
+  }
+
+
+}
+
+CommandExecuterPortfolio::~CommandExecuterPortfolio()
+{
+  Assert(d_seq != NULL);
+  delete d_seq;
+
+  Assert(d_smts.size() == d_numThreads);
+  for(unsigned i = 1; i < d_numThreads; ++i) {
+    // the 0-th one is responsibility of parent class
+
+    delete d_exprMgrs[i];
+    delete d_smts[i];
+  }
+  d_exprMgrs.clear();
+  d_smts.clear();
+}
+
+void CommandExecuterPortfolio::lemmaSharingInit()
+{
+  /* Sharing channels */
+  Assert(d_channelsIn.size() == 0);
+  Assert(d_channelsOut.size() == 0);
+
+  if(d_numThreads == 1) {
+    // Disable sharing
+    d_threadOptions[0].set(options::sharingFilterByLength, 0);
+  } else {
+    // Setup sharing channels
+    const unsigned int sharingChannelSize = 1000000;
+
+    for(unsigned i = 0; i < d_numThreads; ++i){
+      if(Debug.isOn("channel-empty")) {
+        d_channelsOut.push_back 
+          (new EmptySharedChannel<ChannelFormat>(sharingChannelSize));
+        d_channelsIn.push_back
+          (new EmptySharedChannel<ChannelFormat>(sharingChannelSize));
+        continue;
+      }
+      d_channelsOut.push_back
+        (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
+      d_channelsIn.push_back
+        (new SynchronizedSharedChannel<ChannelFormat>(sharingChannelSize));
+    }
+
+    /* Lemma I/O channels */
+    for(unsigned i = 0; i < d_numThreads; ++i) {
+      string tag = "thread #" +
+        boost::lexical_cast<string>(d_threadOptions[i][options::thread_id]);
+      d_threadOptions[i].set
+        (options::lemmaOutputChannel,
+         new PortfolioLemmaOutputChannel(tag, d_channelsOut[i], d_exprMgrs[i],
+                                         d_vmaps[i]->d_from, d_vmaps[i]->d_to));
+      d_threadOptions[i].set
+        (options::lemmaInputChannel,
+         new PortfolioLemmaInputChannel(tag, d_channelsIn[i], d_exprMgrs[i],
+                                        d_vmaps[i]->d_from, d_vmaps[i]->d_to));
+    }
+
+    /* Output to string stream  */
+    if(d_options[options::verbosity] == 0 
+       || d_options[options::separateOutput]) {
+      Assert(d_ostringstreams.size() == 0);
+      for(unsigned i = 0; i < d_numThreads; ++i) {
+        d_ostringstreams.push_back(new ostringstream);
+        d_threadOptions[i].set(options::out, d_ostringstreams[i]);
+      }
+    }
+  }
+}
+
+void CommandExecuterPortfolio::lemmaSharingCleanup()
+{
+  Assert(d_numThreads == d_options[options::threads]);
+
+  // Channel cleanup
+  Assert(d_channelsIn.size() == d_numThreads);
+  Assert(d_channelsOut.size() == d_numThreads);
+  for(unsigned i = 0; i < d_numThreads; ++i) {
+    delete d_channelsIn[i];
+    delete d_channelsOut[i];
+    d_threadOptions[i].set(options::lemmaInputChannel, NULL);
+    d_threadOptions[i].set(options::lemmaOutputChannel, NULL);
+  }
+  d_channelsIn.clear();
+  d_channelsOut.clear();
+
+  // sstreams cleanup (if used)
+  if(d_ostringstreams.size() != 0) {
+    Assert(d_ostringstreams.size() == d_numThreads);
+    for(unsigned i = 0; i < d_numThreads; ++i) {
+      d_threadOptions[i].set(options::out, d_options[options::out]);
+      delete d_ostringstreams[i];
+    }
+    d_ostringstreams.clear();
+  }
+
+}
+
+bool CommandExecuterPortfolio::doCommandSingleton(Command* cmd)
+{
+  /**
+   * save the command and if check sat or query command, run a
+   * porfolio of SMT solvers.
+   */
+
+  int mode = 0;
+  // mode = 0 : run the first thread
+  // mode = 1 : run a porfolio
+  // mode = 2 : run the last winner
+
+  // if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
+  //    dynamic_cast<QueryCommand*>(cmd) != NULL) {
+  //   mode = 1;
+  // } else if(dynamic_cast<GetValueCommand*>(cmd) != NULL) {
+  //   mode = 2;
+  // }
+  
+  if(mode == 0) {
+    d_seq->addCommand(cmd->clone());
+    return CommandExecuter::doCommandSingleton(cmd);
+  } else if(mode == 1) {               // portfolio
+    d_seq->addCommand(cmd->clone());
+
+    // We currently don't support changing number of threads for each
+    // command, but things have been architected in a way so that this
+    // can be acheived with not a lot of work
+    Command *seqs[d_numThreads];
+
+    seqs[0] = cmd;
+
+    /* variable maps and exporting */
+    for(unsigned i = 1; i < d_numThreads; ++i) {
+      /**
+       * vmaps[i].d_from [x] = y means
+       *    that in thread #0's expr manager id is y
+       *    and  in thread #i's expr manager id is x
+       * opposite for d_to
+       *
+       * d_from[x] : in a sense gives the id if converting *from* it to
+       *             first thread
+       */
+      try {
+        seqs[i] = d_seq->exportTo(d_exprMgrs[i], *(d_vmaps[i]) );
+      }catch(ExportToUnsupportedException& e){
+        return CommandExecuter::doCommandSingleton(cmd);
+      }
+    }
+
+    /**
+     * Create identity variable map for the first thread, with only
+     * those variables which have a corresponding variable in
+     * another thread. (TODO: Also assert, all threads have the same
+     * set of variables mapped.)
+     */
+    if(d_numThreads >= 2) {
+      for(typeof(d_vmaps[1]->d_to.begin()) i=d_vmaps[1]->d_to.begin();
+          i!=d_vmaps[1]->d_to.end(); ++i) {
+        (d_vmaps[0]->d_from)[i->first] = i->first;
+      }
+      d_vmaps[0]->d_to = d_vmaps[0]->d_from;
+    }
+
+    lemmaSharingInit();
+
+    /* Portfolio */
+    boost::function<bool()> fns[d_numThreads];
+    for(unsigned i = 0; i < d_numThreads; ++i) {
+      fns[i] = boost::bind(smtEngineInvoke,
+                           d_smts[i],
+                           seqs[i],
+                           d_threadOptions[i][options::out]
+                           );
+    }
+
+    Assert(d_channelsIn.size() == d_numThreads);
+    Assert(d_channelsOut.size() == d_numThreads);
+    Assert(d_smts.size() == d_numThreads);
+    boost::function<void()>
+      smFn = boost::bind(sharingManager<ChannelFormat>,
+                         d_numThreads,
+                         &d_channelsOut[0],
+                         &d_channelsIn[0],
+                         &d_smts[0]);
+
+    pair<int, bool> portfolioReturn =
+        runPortfolio(d_numThreads, smFn, fns, true);
+
+    d_seq = NULL;
+    delete d_seq;
+    d_seq = new CommandSequence();
+
+    d_lastWinner = portfolioReturn.first;
+
+    // *d_options[options::out]
+    //   << "Winner = "
+    //   << portfolioReturn.first
+    //   << std::endl;
+
+    if(d_ostringstreams.size() != 0) {
+      Assert(d_numThreads == d_options[options::threads]);
+      Assert(portfolioReturn.first >= 0);
+      Assert(unsigned(portfolioReturn.first) < d_numThreads);
+
+      *d_options[options::out]
+        << d_ostringstreams[portfolioReturn.first]->str();
+    }
+    
+    /* cleanup this check sat specific stuff */
+    lemmaSharingCleanup();
+
+    return portfolioReturn.second;
+  } else if(mode == 2) {
+    return smtEngineInvoke(d_smts[d_lastWinner],
+                           cmd,
+                           d_threadOptions[d_lastWinner][options::out]);
+  } else {
+    Unreachable();
+  }
+
+}
+
+std::string CommandExecuterPortfolio::getSmtEngineStatus()
+{
+  return d_smts[d_lastWinner]->getInfo("status").getValue();
+}
+
+}/*main namespace*/
+}/*CVC4 namespace*/
diff --git a/src/main/command_executer_portfolio.h b/src/main/command_executer_portfolio.h
new file mode 100644
index 000000000..db9db6509
--- /dev/null
+++ b/src/main/command_executer_portfolio.h
@@ -0,0 +1,69 @@
+/*********************                                                        */
+/*! \file command_executer_portfolio.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** Minor contributors (to current version): 
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief An additional layer between commands and invoking them.
+ **
+ ** The portfolio executer branches check-sat queries to several
+ ** threads.
+ **/
+
+#ifndef __CVC4__COMMAND_EXECUTER_PORTFOLIO_H
+#define __CVC4__COMMAND_EXECUTER_PORTFOLIO_H
+
+#include "main/command_executer.h"
+#include "main/portfolio_util.h"
+
+namespace CVC4 {
+
+class CommandSequence;
+
+namespace main {
+
+class CommandExecuterPortfolio : public CommandExecuter {
+
+  // These shall be created/deleted during initalization
+  std::vector<ExprManager*> d_exprMgrs;
+  const unsigned d_numThreads;   // Currently const, but designed so it is
+                                 // not too hard to support this changing
+  std::vector<SmtEngine*> d_smts;
+  CommandSequence* d_seq;
+  std::vector<Options>& d_threadOptions;
+  std::vector<ExprManagerMapCollection*> d_vmaps;
+
+  int d_lastWinner;
+
+  // These shall be reset for each check-sat
+  std::vector< SharedChannel<ChannelFormat>* > d_channelsOut;
+  std::vector< SharedChannel<ChannelFormat>* > d_channelsIn;
+  std::vector<std::ostringstream*> d_ostringstreams;
+
+public:
+  CommandExecuterPortfolio(ExprManager &exprMgr,
+                           Options &options,
+                           std::vector<Options>& tOpts);
+
+  ~CommandExecuterPortfolio();
+
+  std::string getSmtEngineStatus();
+protected:
+  bool doCommandSingleton(Command* cmd);
+private:
+  CommandExecuterPortfolio();
+  void lemmaSharingInit();
+  void lemmaSharingCleanup();
+};
+
+}/*main namespace*/
+}/*CVC4 namespace*/
+
+#endif  /* __CVC4__COMMAND_EXECUTER_PORTFOLIO_H */
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
deleted file mode 100644
index 648c6c9f9..000000000
--- a/src/main/driver_portfolio.cpp
+++ /dev/null
@@ -1,833 +0,0 @@
-/*********************                                                        */
-/*! \file driver_portfolio.cpp
- ** \verbatim
- ** Original author: kshitij
- ** Major contributors: taking, mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Driver for portfolio CVC4 executable (pcvc4)
- **
- ** Driver for portfolio CVC4 executable (pcvc4).
- **/
-
-#include <cstdio>
-#include <cstdlib>
-#include <iostream>
-#include <sys/time.h>           // for gettimeofday()
-
-#include <queue>
-
-#include <boost/thread.hpp>
-#include <boost/thread/condition.hpp>
-#include <boost/exception_ptr.hpp>
-#include <boost/lexical_cast.hpp>
-
-#include "cvc4autoconfig.h"
-#include "main/main.h"
-#include "main/interactive_shell.h"
-#include "parser/parser.h"
-#include "parser/parser_builder.h"
-#include "parser/parser_exception.h"
-#include "expr/expr_manager.h"
-#include "expr/variable_type_map.h"
-#include "smt/smt_engine.h"
-#include "expr/command.h"
-#include "util/Assert.h"
-#include "util/configuration.h"
-#include "options/options.h"
-#include "main/options.h"
-#include "smt/options.h"
-#include "prop/options.h"
-#include "theory/uf/options.h"
-#include "util/output.h"
-#include "util/dump.h"
-#include "util/result.h"
-#include "util/stats.h"
-#include "util/lemma_input_channel.h"
-#include "util/lemma_output_channel.h"
-
-#include "expr/pickler.h"
-#include "util/channel.h"
-
-#include "main/portfolio.h"
-
-using namespace std;
-using namespace CVC4;
-using namespace CVC4::parser;
-using namespace CVC4::main;
-
-/* Global variables */
-
-namespace CVC4 {
-  namespace main {
-
-    StatisticsRegistry theStatisticsRegistry;
-
-    /** A pointer to the StatisticsRegistry (the signal handlers need it) */
-    CVC4::StatisticsRegistry* pStatistics;
-
-  }/* CVC4::main namespace */
-}/* CVC4 namespace */
-
-/* Function declarations */
-
-static bool doCommand(SmtEngine&, Command*, Options&);
-
-Result doSmt(SmtEngine &smt, Command *cmd, Options &options);
-
-template<typename T>
-void sharingManager(unsigned numThreads,
-                    SharedChannel<T>* channelsOut[],
-                    SharedChannel<T>* channelsIn[],
-                    SmtEngine* smts[]);
-
-
-/* To monitor for activity on shared channels */
-bool global_activity;
-bool global_activity_true() { return global_activity; }
-bool global_activity_false() { return not global_activity; }
-boost::condition global_activity_cond;
-
-typedef expr::pickle::Pickle channelFormat; /* Remove once we are using Pickle */
-
-template <typename T>
-class EmptySharedChannel: public SharedChannel<T> {
-public:
-  EmptySharedChannel(int) {}
-  bool push(const T&) { return true; }
-  T pop() { return T(); }
-  bool empty() { return true; }
-  bool full() { return false; }
-};
-
-class PortfolioLemmaOutputChannel : public LemmaOutputChannel {
-private:
-  string d_tag;
-  SharedChannel<channelFormat>* d_sharedChannel;
-  expr::pickle::MapPickler d_pickler;
-
-public:
-  int cnt;
-  PortfolioLemmaOutputChannel(string tag,
-                              SharedChannel<channelFormat> *c,
-                              ExprManager* em,
-                              VarMap& to,
-                              VarMap& from) :
-    d_tag(tag),
-    d_sharedChannel(c),
-    d_pickler(em, to, from)
-    ,cnt(0)
-  {}
-
-  void notifyNewLemma(Expr lemma) {
-    if(Debug.isOn("disable-lemma-sharing")) {
-      return;
-    }
-    if(options::sharingFilterByLength() >= 0) { // 0 would mean no-sharing effectively
-      if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) {
-        return;
-      }
-    }
-    ++cnt;
-    Trace("sharing") << d_tag << ": " << lemma << endl;
-    expr::pickle::Pickle pkl;
-    try {
-      d_pickler.toPickle(lemma, pkl);
-      d_sharedChannel->push(pkl);
-      if(Trace.isOn("showSharing") && options::thread_id() == 0) {
-        *options::out() << "thread #0: notifyNewLemma: " << lemma << endl;
-      }
-    } catch(expr::pickle::PicklingException& p){
-      Trace("sharing::blocked") << lemma << endl;
-    }
-  }
-
-};
-
-/* class PortfolioLemmaInputChannel */
-class PortfolioLemmaInputChannel : public LemmaInputChannel {
-private:
-  string d_tag;
-  SharedChannel<channelFormat>* d_sharedChannel;
-  expr::pickle::MapPickler d_pickler;
-
-public:
-  PortfolioLemmaInputChannel(string tag,
-                             SharedChannel<channelFormat>* c,
-                             ExprManager* em,
-                             VarMap& to,
-                             VarMap& from) :
-    d_tag(tag),
-    d_sharedChannel(c),
-    d_pickler(em, to, from){
-  }
-
-  bool hasNewLemma(){
-    Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << endl;
-    return !d_sharedChannel->empty();
-  }
-
-  Expr getNewLemma() {
-    Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << endl;
-    expr::pickle::Pickle pkl = d_sharedChannel->pop();
-
-    Expr e = d_pickler.fromPickle(pkl);
-    if(Trace.isOn("showSharing") && options::thread_id() == 0) {
-      *options::out() << "thread #0: getNewLemma: " << e << endl;
-    }
-    return e;
-  }
-
-};/* class PortfolioLemmaInputChannel */
-
-
-
-int runCvc4(int argc, char *argv[], Options& opts) {
-
-#ifdef CVC4_CLN_IMP
-  Warning() << "WARNING:" << endl
-            << "WARNING: This build of portfolio-CVC4 uses the CLN library" << endl
-            << "WARNING: which is not thread-safe!  Expect crashes and" << endl
-            << "WARNING: incorrect answers." << endl
-            << "WARNING:" << endl;
-#endif /* CVC4_CLN_IMP */
-
-  /**************************************************************************
-   * runCvc4 outline:
-   * -> Start a couple of timers
-   * -> Processing of options, including thread specific ones
-   * -> Statistics related stuff
-   * -> Create ExprManager, parse commands, duplicate exprMgrs using export
-   * -> Create smtEngines
-   * -> Lemma sharing init
-   * -> Run portfolio, exit/print stats etc.
-   * (This list might become outdated, a timestamp might be good: 7 Dec '11.)
-   **************************************************************************/
-
-  // Timer statistic
-  TimerStat s_totalTime("totalTime");
-  TimerStat s_beforePortfolioTime("beforePortfolioTime");
-  s_totalTime.start();
-  s_beforePortfolioTime.start();
-
-  // For the signal handlers' benefit
-  pOptions = &opts;
-
-  // Initialize the signal handlers
-  cvc4_init();
-
-  progPath = argv[0];
-
-
-  /****************************** Options Processing ************************/
-
-  // Parse the options
-  int firstArgIndex = opts.parseOptions(argc, argv);
-
-  progName = opts[options::binary_name].c_str();
-
-  if( opts[options::help] ) {
-    printUsage(opts, true);
-    exit(1);
-  } else if( opts[options::languageHelp] ) {
-    Options::printLanguageHelp(*opts[options::out]);
-    exit(1);
-  } else if( opts[options::version] ) {
-    *opts[options::out] << Configuration::about().c_str() << flush;
-    exit(0);
-  }
-
-  unsigned numThreads = opts[options::threads];
-
-  if(opts[options::threadArgv].size() > size_t(numThreads)) {
-    stringstream ss;
-    ss << "--thread" << (opts[options::threadArgv].size() - 1)
-       << " configuration string seen but this portfolio will only contain "
-       << numThreads << " thread(s)!";
-    throw OptionException(ss.str());
-  }
-
-  segvNoSpin = opts[options::segvNoSpin];
-
-  // If in competition mode, set output stream option to flush immediately
-#ifdef CVC4_COMPETITION_MODE
-  *opts[options::out] << unitbuf;
-#endif /* CVC4_COMPETITION_MODE */
-
-  // We only accept one input file
-  if(argc > firstArgIndex + 1) {
-    throw Exception("Too many input files specified.");
-  }
-
-  // If no file supplied we will read from standard input
-  const bool inputFromStdin =
-    firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
-
-  // if we're reading from stdin on a TTY, default to interactive mode
-  if(!opts.wasSetByUser(options::interactive)) {
-    opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin)));
-  }
-
-  // Auto-detect input language by filename extension
-  const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
-
-  if(opts[options::inputLanguage] == language::input::LANG_AUTO) {
-    if( inputFromStdin ) {
-      // We can't do any fancy detection on stdin
-      opts.set(options::inputLanguage, language::input::LANG_CVC4);
-    } else {
-      unsigned len = strlen(filename);
-      if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
-      } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
-        opts.set(options::inputLanguage, language::input::LANG_SMTLIB);
-      } else if((len >= 2 && !strcmp(".p", filename + len - 2))
-                || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
-        opts.set(options::inputLanguage, language::input::LANG_TPTP);
-      } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
-                || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        opts.set(options::inputLanguage, language::input::LANG_CVC4);
-      }
-    }
-  }
-
-  // Determine which messages to show based on smtcomp_mode and verbosity
-  if(Configuration::isMuzzledBuild()) {
-    Debug.setStream(CVC4::null_os);
-    Trace.setStream(CVC4::null_os);
-    Notice.setStream(CVC4::null_os);
-    Chat.setStream(CVC4::null_os);
-    Message.setStream(CVC4::null_os);
-    Warning.setStream(CVC4::null_os);
-    Dump.setStream(CVC4::null_os);
-  } else {
-    if(opts[options::verbosity] < 2) {
-      Chat.setStream(CVC4::null_os);
-    }
-    if(opts[options::verbosity] < 1) {
-      Notice.setStream(CVC4::null_os);
-    }
-    if(opts[options::verbosity] < 0) {
-      Message.setStream(CVC4::null_os);
-      Warning.setStream(CVC4::null_os);
-    }
-
-    OutputLanguage language = language::toOutputLanguage(opts[options::inputLanguage]);
-    Debug.getStream() << Expr::setlanguage(language);
-    Trace.getStream() << Expr::setlanguage(language);
-    Notice.getStream() << Expr::setlanguage(language);
-    Chat.getStream() << Expr::setlanguage(language);
-    Message.getStream() << Expr::setlanguage(language);
-    Warning.getStream() << Expr::setlanguage(language);
-    Dump.getStream() << Expr::setlanguage(language)
-                     << Expr::setdepth(-1)
-                     << Expr::printtypes(false);
-  }
-
-  // important even for muzzled builds (to get result output right)
-  *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
-
-  vector<Options> threadOptions;
-  for(unsigned i = 0; i < numThreads; ++i) {
-    threadOptions.push_back(opts);
-    Options& tOpts = threadOptions.back();
-
-    // Set thread identifier
-    tOpts.set(options::thread_id, i);
-
-    // If the random-seed is negative, pick a random seed randomly
-    if(opts[options::satRandomSeed] < 0) {
-      tOpts.set(options::satRandomSeed, (double)rand());
-    }
-
-    if(i < opts[options::threadArgv].size() && !opts[options::threadArgv][i].empty()) {
-      // separate out the thread's individual configuration string
-      stringstream optidss;
-      optidss << "--thread" << i;
-      string optid = optidss.str();
-      int targc = 1;
-      char* tbuf = strdup(opts[options::threadArgv][i].c_str());
-      char* p = tbuf;
-      // string length is certainly an upper bound on size needed
-      char** targv = new char*[opts[options::threadArgv][i].size()];
-      char** vp = targv;
-      *vp++ = strdup(optid.c_str());
-      p = strtok(p, " ");
-      while(p != NULL) {
-        *vp++ = p;
-        ++targc;
-        p = strtok(NULL, " ");
-      }
-      *vp++ = NULL;
-      if(targc > 1) { // this is necessary in case you do e.g. --thread0="  "
-        try {
-          tOpts.parseOptions(targc, targv);
-        } catch(OptionException& e) {
-          stringstream ss;
-          ss << optid << ": " << e.getMessage();
-          throw OptionException(ss.str());
-        }
-        if(optind != targc) {
-          stringstream ss;
-          ss << "unused argument `" << targv[optind]
-             << "' in thread configuration " << optid << " !";
-          throw OptionException(ss.str());
-        }
-        if(tOpts[options::threads] != numThreads || tOpts[options::threadArgv] != opts[options::threadArgv]) {
-          stringstream ss;
-          ss << "not allowed to set thread options in " << optid << " !";
-          throw OptionException(ss.str());
-        }
-      }
-      free(targv[0]);
-      delete targv;
-      free(tbuf);
-    }
-  }
-
-  // Some more options related stuff
-
-  /* Use satRandomSeed for generating random numbers, in particular satRandomSeed-s */
-  srand((unsigned int)(-opts[options::satRandomSeed]));
-
-  assert(numThreads >= 1);      //do we need this?
-
-  /* Output to string stream  */
-  vector<stringstream*> ss_out(numThreads);
-  if(opts[options::verbosity] == 0 || opts[options::separateOutput]) {
-    for(unsigned i = 0; i < numThreads; ++i) {
-      ss_out[i] = new stringstream;
-      threadOptions[i].set(options::out, ss_out[i]);
-    }
-  }
-
-  /****************************** Driver Statistics *************************/
-
-  // Statistics init
-  pStatistics = &theStatisticsRegistry;
-
-  StatisticsRegistry driverStatisticsRegistry("driver");
-  theStatisticsRegistry.registerStat_((&driverStatisticsRegistry));
-
-  // Timer statistic
-  RegisterStatistic* statTotalTime =
-    new RegisterStatistic(&driverStatisticsRegistry, &s_totalTime);
-  RegisterStatistic* statBeforePortfolioTime =
-    new RegisterStatistic(&driverStatisticsRegistry, &s_beforePortfolioTime);
-
-  // Filename statistics
-  ReferenceStat< const char* > s_statFilename("filename", filename);
-  RegisterStatistic* statFilenameReg =
-    new RegisterStatistic(&driverStatisticsRegistry, &s_statFilename);
-
-
-  /****************** ExprManager + CommandParsing + Export *****************/
-
-  // Create the expression manager
-  ExprManager* exprMgrs[numThreads];
-  exprMgrs[0] = new ExprManager(threadOptions[0]);
-  ExprManager* exprMgr = exprMgrs[0]; // to avoid having to change code which uses that
-
-  // Parse commands until we are done
-  Command* cmd;
-  // bool status = true;           // Doesn't seem to be use right now: commenting it out
-  CommandSequence* seq = new CommandSequence();
-  if( opts[options::interactive] ) {
-    InteractiveShell shell(*exprMgr, opts);
-    Message() << Configuration::getPackageName()
-              << " " << Configuration::getVersionString();
-    if(Configuration::isSubversionBuild()) {
-      Message() << " [subversion " << Configuration::getSubversionBranchName()
-                << " r" << Configuration::getSubversionRevision()
-                << (Configuration::hasSubversionModifications() ?
-                    " (with modifications)" : "")
-                << "]";
-    }
-    Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
-              << " assertions:"
-              << (Configuration::isAssertionBuild() ? "on" : "off")
-              << endl;
-    while((cmd = shell.readCommand())) {
-      seq->addCommand(cmd);
-    }
-  } else {
-    ParserBuilder parserBuilder =
-      ParserBuilder(exprMgr, filename).
-        withOptions(opts);
-
-    if( inputFromStdin ) {
-#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
-      parserBuilder.withStreamInput(cin);
-#else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
-      parserBuilder.withLineBufferedStreamInput(cin);
-#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
-    }
-
-    Parser *parser = parserBuilder.build();
-    while((cmd = parser->nextCommand())) {
-      seq->addCommand(cmd);
-      // doCommand(smt, cmd, opts);
-      // delete cmd;
-    }
-    // Remove the parser
-    delete parser;
-  }
-
-  if(opts[options::parseOnly]) {
-    return 0;
-  }
-
-  exprMgr = NULL;               // don't want to use that variable
-                                // after this point
-
-  /* Duplication, Individualisation */
-  ExprManagerMapCollection* vmaps[numThreads]; // vmaps[0] is generally empty
-  Command *seqs[numThreads];
-  seqs[0] = seq;   seq = NULL;
-  for(unsigned i = 1; i < numThreads; ++i) {
-    vmaps[i] = new ExprManagerMapCollection();
-    exprMgrs[i] = new ExprManager(threadOptions[i]);
-    seqs[i] = seqs[0]->exportTo(exprMgrs[i], *(vmaps[i]) );
-  }
-  /**
-   * vmaps[i].d_from [x] = y means
-   *    that in thread #0's expr manager id is y
-   *    and  in thread #i's expr manager id is x
-   * opposite for d_to
-   *
-   * d_from[x] : in a sense gives the id if converting *from* it to
-   *             first thread
-   */
-
-  /**
-   * Create identity variable map for the first thread, with only
-   * those variables which have a corresponding variable in another
-   * thread. (TODO:Also assert, all threads have the same set of
-   * variables mapped.)
-   */
-  if(numThreads >= 2) {
-    // Get keys from the first thread
-    //Set<uint64_t> s = vmaps[1]->d_to.keys();
-    vmaps[0] = new ExprManagerMapCollection(); // identity be default?
-    for(typeof(vmaps[1]->d_to.begin()) i=vmaps[1]->d_to.begin(); i!=vmaps[1]->d_to.end(); ++i) {
-      (vmaps[0]->d_from)[i->first] = i->first;
-    }
-    vmaps[0]->d_to = vmaps[0]->d_from;
-  }
-
-  // Create the SmtEngine(s)
-  SmtEngine *smts[numThreads];
-  for(unsigned i = 0; i < numThreads; ++i) {
-    smts[i] = new SmtEngine(exprMgrs[i]);
-
-    // Register the statistics registry of the thread
-    string emTag = "ExprManager thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]);
-    string smtTag = "SmtEngine thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]);
-    exprMgrs[i]->getStatisticsRegistry()->setName(emTag);
-    smts[i]->getStatisticsRegistry()->setName(smtTag);
-    theStatisticsRegistry.registerStat_( exprMgrs[i]->getStatisticsRegistry() );
-    theStatisticsRegistry.registerStat_( smts[i]->getStatisticsRegistry() );
-  }
-
-  /************************* Lemma sharing init ************************/
-
-  /* Sharing channels */
-  SharedChannel<channelFormat> *channelsOut[numThreads], *channelsIn[numThreads];
-
-  if(numThreads == 1) {
-    // Disable sharing
-    threadOptions[0].set(options::sharingFilterByLength, 0);
-  } else {
-    // Setup sharing channels
-    const unsigned int sharingChannelSize = 1000000;
-
-    for(unsigned i = 0; i < numThreads; ++i){
-      if(Debug.isOn("channel-empty")) {
-        channelsOut[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize);
-        channelsIn[i] = new EmptySharedChannel<channelFormat>(sharingChannelSize);
-        continue;
-      }
-      channelsOut[i] = new SynchronizedSharedChannel<channelFormat>(sharingChannelSize);
-      channelsIn[i] = new SynchronizedSharedChannel<channelFormat>(sharingChannelSize);
-    }
-
-    /* Lemma output channel */
-    for(unsigned i = 0; i < numThreads; ++i) {
-      string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i][options::thread_id]);
-      threadOptions[i].set(options::lemmaOutputChannel,
-        new PortfolioLemmaOutputChannel(tag, channelsOut[i], exprMgrs[i],
-                                        vmaps[i]->d_from, vmaps[i]->d_to));
-      threadOptions[i].set(options::lemmaInputChannel,
-        new PortfolioLemmaInputChannel(tag, channelsIn[i], exprMgrs[i],
-                                       vmaps[i]->d_from, vmaps[i]->d_to));
-    }
-  }
-
-  /************************** End of initialization ***********************/
-
-  /* Portfolio */
-  boost::function<Result()> fns[numThreads];
-
-  for(unsigned i = 0; i < numThreads; ++i) {
-    fns[i] = boost::bind(doSmt, boost::ref(*smts[i]), seqs[i], boost::ref(threadOptions[i]));
-  }
-
-  boost::function<void()>
-    smFn = boost::bind(sharingManager<channelFormat>, numThreads, channelsOut, channelsIn, smts);
-
-  s_beforePortfolioTime.stop();
-  pair<int, Result> portfolioReturn = runPortfolio(numThreads, smFn, fns, true);
-  int winner = portfolioReturn.first;
-  Result result = portfolioReturn.second;
-
-  cout << result << endl;
-
-  /************************* Post printing answer ***********************/
-
-  if(opts[options::printWinner]){
-    cout << "The winner is #" << winner << endl;
-  }
-
-  Result satRes = result.asSatisfiabilityResult();
-  int returnValue;
-  if(satRes.isSat() == Result::SAT) {
-    returnValue = 10;
-  } else if(satRes.isSat() == Result::UNSAT) {
-    returnValue = 20;
-  } else {
-    returnValue = 0;
-  }
-
-#ifdef CVC4_COMPETITION_MODE
-  // exit, don't return
-  // (don't want destructors to run)
-  exit(returnValue);
-#endif /* CVC4_COMPETITION_MODE */
-
-  // ReferenceStat< Result > s_statSatResult("sat/unsat", result);
-  // RegisterStatistic statSatResultReg(*exprMgr, &s_statSatResult);
-
-  // Stop timers, enough work done
-  s_totalTime.stop();
-
-  if(opts[options::statistics]) {
-    pStatistics->flushInformation(*opts[options::err]);
-  }
-
-  if(opts[options::separateOutput]) {
-    for(unsigned i = 0; i < numThreads; ++i) {
-      *opts[options::out] << "--- Output from thread #" << i << " ---" << endl;
-      *opts[options::out] << ss_out[i]->str();
-    }
-  }
-
-  /*if(opts[options::statistics]) {
-    double totalTime = double(s_totalTime.getData().tv_sec) +
-        double(s_totalTime.getData().tv_nsec)/1000000000.0;
-    cout.precision(6);
-    *opts[options::err] << "real time: " << totalTime << "s\n";
-    int th0_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(opts[options::lemmaOutputChannel])).cnt;
-    int th1_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(threadOptions[1].lemmaOutputChannel)).cnt;
-    *opts[options::err] << "lemmas shared by thread #0: " << th0_lemcnt << endl;
-    *opts[options::err] << "lemmas shared by thread #1: " << th1_lemcnt << endl;
-    *opts[options::err] << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime)
-                 << " lem/sec" << endl;
-    *opts[options::err] << "winner: #" << (winner == 0 ? 0 : 1) << endl;
-  }*/
-
-  // destruction is causing segfaults, let us just exit
-  exit(returnValue);
-
-  //delete vmaps;
-
-  delete statTotalTime;
-  delete statBeforePortfolioTime;
-  delete statFilenameReg;
-
-  // delete seq;
-  // delete exprMgr;
-
-  // delete seq2;
-  // delete exprMgr2;
-
-  return returnValue;
-}
-
-/**** Code shared with driver.cpp ****/
-
-namespace CVC4 {
-  namespace main {/* Global options variable */
-    CVC4_THREADLOCAL(Options*) pOptions;
-
-    /** Full argv[0] */
-    const char *progPath;
-
-    /** Just the basename component of argv[0] */
-    const char *progName;
-  }
-}
-
-void printUsage(Options& opts, bool full) {
-  stringstream ss;
-  ss << "usage: " << opts[options::binary_name] << " [options] [input-file]" << endl
-      << endl
-      << "Without an input file, or with `-', CVC4 reads from standard input." << endl
-      << endl
-      << "CVC4 options:" << endl;
-  if(full) {
-    Options::printUsage( ss.str(), *opts[options::out] );
-  } else {
-    Options::printShortUsage( ss.str(), *opts[options::out] );
-  }
-}
-
-/** Executes a command. Deletes the command after execution. */
-static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) {
-  if( opts[options::parseOnly] ) {
-    return true;
-  }
-
-  // assume no error
-  bool status = true;
-
-  CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
-  if(seq != NULL) {
-    for(CommandSequence::iterator subcmd = seq->begin();
-        subcmd != seq->end();
-        ++subcmd) {
-      status = doCommand(smt, *subcmd, opts) && status;
-    }
-  } else {
-    if(opts[options::verbosity] > 0) {
-      *opts[options::out] << "Invoking: " << *cmd << endl;
-    }
-
-    if(opts[options::verbosity] >= 0) {
-      cmd->invoke(&smt, *opts[options::out]);
-    } else {
-      cmd->invoke(&smt);
-    }
-    status = status && cmd->ok();
-  }
-
-  return status;
-}
-
-/**** End of code shared with driver.cpp ****/
-
-/** Create the SMT engine and execute the commands */
-Result doSmt(SmtEngine &smt, Command *cmd, Options &opts) {
-
-  try {
-    // For the signal handlers' benefit
-    pOptions = &opts;
-
-    // Execute the commands
-    bool status = doCommand(smt, cmd, opts);
-
-    // if(opts[options::statistics]) {
-    //   smt.getStatisticsRegistry()->flushInformation(*opts[options::err]);
-    //   *opts[options::err] << "Statistics printing of my thread complete " << endl;
-    // }
-
-    return status ? smt.getStatusOfLastCommand() : Result::SAT_UNKNOWN;
-  } catch(OptionException& e) {
-    *(*pOptions)[options::out] << "unknown" << endl;
-    cerr << "CVC4 Error:" << endl << e << endl;
-    printUsage(*pOptions);
-  } catch(Exception& e) {
-#ifdef CVC4_COMPETITION_MODE
-    *(*pOptions)[options::out] << "unknown" << endl;
-#endif
-    *(*pOptions)[options::err] << "CVC4 Error:" << endl << e << endl;
-    if((*pOptions)[options::statistics]) {
-      pStatistics->flushInformation(*(*pOptions)[options::err]);
-    }
-  }
-  return Result::SAT_UNKNOWN;
-}
-
-template<typename T>
-void sharingManager(unsigned numThreads,
-                    SharedChannel<T> *channelsOut[], // out and in with respect
-                    SharedChannel<T> *channelsIn[],
-                    SmtEngine *smts[])  // to smt engines
-{
-  Trace("sharing") << "sharing: thread started " << endl;
-  vector <int> cnt(numThreads); // Debug("sharing")
-
-  vector< queue<T> > queues;
-  for(unsigned i = 0; i < numThreads; ++i){
-    queues.push_back(queue<T>());
-  }
-
-  const unsigned int sharingBroadcastInterval = 1;
-
-  boost::mutex mutex_activity;
-
-  /* Disable interruption, so that we can check manually */
-  boost::this_thread::disable_interruption di;
-
-  while(not boost::this_thread::interruption_requested()) {
-
-    boost::this_thread::sleep(boost::posix_time::milliseconds(sharingBroadcastInterval));
-
-    for(unsigned t = 0; t < numThreads; ++t) {
-
-      if(channelsOut[t]->empty()) continue;      /* No activity on this channel */
-
-      /* Alert if channel full, so that we increase sharingChannelSize
-         or decrease sharingBroadcastInterval */
-      Assert(not channelsOut[t]->full());
-
-      T data = channelsOut[t]->pop();
-
-      if(Trace.isOn("sharing")) {
-        ++cnt[t];
-        Trace("sharing") << "sharing: Got data. Thread #" << t
-                         << ". Chunk " << cnt[t] << std :: endl;
-      }
-
-      for(unsigned u = 0; u < numThreads; ++u) {
-        if(u != t){
-          Trace("sharing") << "sharing: adding to queue " << u << endl;
-          queues[u].push(data);
-        }
-      }/* end of inner for: broadcast activity */
-
-    } /* end of outer for: look for activity */
-
-    for(unsigned t = 0; t < numThreads; ++t){
-      /* Alert if channel full, so that we increase sharingChannelSize
-         or decrease sharingBroadcastInterval */
-      Assert(not channelsIn[t]->full());
-
-      while(!queues[t].empty() && !channelsIn[t]->full()){
-        Trace("sharing") << "sharing: pushing on channel " << t << endl;
-        T data = queues[t].front();
-        channelsIn[t]->push(data);
-        queues[t].pop();
-      }
-    }
-  } /* end of infinite while */
-
-  Trace("interrupt") << "sharing thread interrupted, interrupting all smtEngines" << endl;
-
-  for(unsigned t = 0; t < numThreads; ++t) {
-    Trace("interrupt") << "Interrupting thread #" << t << endl;
-    try{
-      smts[t]->interrupt();
-    }catch(ModalException &e){
-      // It's fine, the thread is probably not there.
-      Trace("interrupt") << "Could not interrupt thread #" << t << endl;
-    }
-  }
-
-  Trace("sharing") << "sharing: Interrupted, exiting." << endl;
-}
diff --git a/src/main/driver.cpp b/src/main/driver_unified.cpp
index 1e6f87d24..061e34223 100644
--- a/src/main/driver.cpp
+++ b/src/main/driver_unified.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file driver.cpp
+/*! \file driver_unified.cpp
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: cconway
@@ -11,9 +11,8 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Driver for (sequential) CVC4 executable (cvc4)
- **
- ** Driver for (sequential) CVC4 executable (cvc4).
+ ** \brief Driver for CVC4 executable (cvc4) unified for both
+ ** sequential and portfolio versions
  **/
 
 #include <cstdlib>
@@ -32,11 +31,14 @@
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
 #include "expr/expr_manager.h"
-#include "smt/smt_engine.h"
 #include "expr/command.h"
 #include "util/Assert.h"
 #include "util/configuration.h"
 #include "options/options.h"
+#include "main/command_executer.h"
+# ifdef PORTFOLIO_BUILD
+#    include "main/command_executer_portfolio.h"
+# endif
 #include "main/options.h"
 #include "smt/options.h"
 #include "theory/uf/options.h"
@@ -50,8 +52,6 @@ using namespace CVC4;
 using namespace CVC4::parser;
 using namespace CVC4::main;
 
-static bool doCommand(SmtEngine&, Command*, Options&);
-
 namespace CVC4 {
   namespace main {
     /** Global options variable */
@@ -218,12 +218,24 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   // important even for muzzled builds (to get result output right)
   *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
 
-  // Create the expression manager
+  // Create the expression manager using appropriate options
+# ifndef PORTFOLIO_BUILD
   ExprManager exprMgr(opts);
+# else
+  vector<Options> threadOpts   = parseThreadSpecificOptions(opts);
+  ExprManager exprMgr(threadOpts[0]);
+# endif
+
+  CommandExecuter* cmdExecuter = 
+# ifndef PORTFOLIO_BUILD
+    new CommandExecuter(exprMgr, opts);
+# else
+    new CommandExecuterPortfolio(exprMgr, opts, threadOpts);
+#endif
 
   // Create the SmtEngine
   StatisticsRegistry driverStats("driver");
-  SmtEngine smt(&exprMgr);
+  pStatistics->registerStat_(&driverStats);
 
   Parser* replayParser = NULL;
   if( opts[options::replayFilename] != "" ) {
@@ -242,12 +254,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
   }
 
-  // signal handlers need access
-  pStatistics = smt.getStatisticsRegistry();
-  exprMgr.getStatisticsRegistry()->setName("ExprManager");
-  pStatistics->registerStat_(exprMgr.getStatisticsRegistry());
-  pStatistics->registerStat_(&driverStats);
-
   // Timer statistic
   RegisterStatistic statTotalTime(&driverStats, &s_totalTime);
 
@@ -274,7 +280,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       replayParser->useDeclarationsFrom(shell.getParser());
     }
     while((cmd = shell.readCommand())) {
-      status = doCommand(smt,cmd, opts) && status;
+      status = cmdExecuter->doCommand(cmd) && status;
       delete cmd;
     }
   } else {
@@ -298,7 +304,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         delete cmd;
         break;
       }
-      status = doCommand(smt, cmd, opts);
+      status = cmdExecuter->doCommand(cmd);
       delete cmd;
     }
     // Remove the parser
@@ -314,7 +320,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   int returnValue;
   string result = "unknown";
   if(status) {
-    result = smt.getInfo("status").getValue();
+    result = cmdExecuter->getSmtEngineStatus();
 
     if(result == "sat") {
       returnValue = 10;
@@ -342,38 +348,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   if(opts[options::statistics]) {
     pStatistics->flushInformation(*opts[options::err]);
   }
-
+  exit(returnValue);
   return returnValue;
 }
-
-/** Executes a command. Deletes the command after execution. */
-static bool doCommand(SmtEngine& smt, Command* cmd, Options& opts) {
-  if( opts[options::parseOnly] ) {
-    return true;
-  }
-
-  CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
-  if(seq != NULL) {
-    // assume no error
-    bool status = true;
-
-    for(CommandSequence::iterator subcmd = seq->begin();
-        status && subcmd != seq->end();
-        ++subcmd) {
-      status = doCommand(smt, *subcmd, opts);
-    }
-
-    return status;
-  } else {
-    if(opts[options::verbosity] > 0) {
-      *opts[options::out] << "Invoking: " << *cmd << endl;
-    }
-
-    if(opts[options::verbosity] >= 0) {
-      cmd->invoke(&smt, *opts[options::out]);
-    } else {
-      cmd->invoke(&smt);
-    }
-    return !cmd->fail();
-  }
-}
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
index 10c387b14..90af26458 100644
--- a/src/main/portfolio.cpp
+++ b/src/main/portfolio.cpp
@@ -11,10 +11,8 @@
  ** 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
+ ** \brief Provides (somewhat) generic functionality to simulate a
+ ** (potentially cooperative) race
  **/
 
 #include <boost/function.hpp>
@@ -27,19 +25,18 @@
 #include "util/result.h"
 #include "options/options.h"
 
-using namespace boost;
-
 namespace CVC4 {
 
-mutex mutex_done;
-mutex mutex_main_wait;
-condition condition_var_main_wait;
+boost::mutex mutex_done;
+boost::mutex mutex_main_wait;
+boost::condition condition_var_main_wait;
 
 bool global_flag_done = false;
 int global_winner = -1;
 
 template<typename S>
-void runThread(int thread_id, function<S()> threadFn, S& returnValue) {
+void runThread(int thread_id, boost::function<S()> threadFn, S& returnValue)
+{
   returnValue = threadFn();
 
   if( mutex_done.try_lock() ) {
@@ -54,15 +51,17 @@ void runThread(int thread_id, function<S()> threadFn, S& returnValue) {
 
 template<typename T, typename S>
 std::pair<int, S> runPortfolio(int numThreads,
-                               function<T()> driverFn,
-                               function<S()> threadFns[],
+                               boost::function<T()> driverFn,
+                               boost::function<S()> threadFns[],
                                bool optionWaitToJoin) {
-  thread thread_driver;
-  thread threads[numThreads];
+  boost::thread thread_driver;
+  boost::thread threads[numThreads];
   S threads_returnValue[numThreads];
 
   for(int t = 0; t < numThreads; ++t) {
-    threads[t] = thread(bind(runThread<S>, t, threadFns[t], ref(threads_returnValue[t]) ));
+    threads[t] = 
+      boost::thread(boost::bind(runThread<S>, t, threadFns[t],
+                                boost::ref(threads_returnValue[t]) ) );
   }
 
   if(not driverFn.empty())
@@ -87,7 +86,10 @@ std::pair<int, S> runPortfolio(int numThreads,
 
 // instantiation
 template
-std::pair<int, Result>
-runPortfolio<void, Result>(int, boost::function<void()>, boost::function<Result()>*, bool);
+std::pair<int, bool>
+runPortfolio<void, bool>(int,
+                         boost::function<void()>, 
+                         boost::function<bool()>*,
+                         bool);
 
 }/* CVC4 namespace */
diff --git a/src/main/portfolio.h b/src/main/portfolio.h
index 1a82d651b..341f243d3 100644
--- a/src/main/portfolio.h
+++ b/src/main/portfolio.h
@@ -11,10 +11,8 @@
  ** 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
+ ** \brief Provides (somewhat) generic functionality to simulate a
+ ** (potentially cooperative) race
  **/
 
 #ifndef __CVC4__PORTFOLIO_H
diff --git a/src/main/portfolio_util.cpp b/src/main/portfolio_util.cpp
new file mode 100644
index 000000000..bad532d30
--- /dev/null
+++ b/src/main/portfolio_util.cpp
@@ -0,0 +1,104 @@
+/*********************                                                        */
+/*! \file portfolio_util.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): 
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Code relevant only for portfolio builds
+ **/
+
+#include <vector>
+#include "options/options.h"
+#include "main/options.h"
+#include "prop/options.h"
+#include "smt/options.h"
+
+using namespace std;
+
+namespace CVC4 {
+
+vector<Options> parseThreadSpecificOptions(Options opts)
+{
+  vector<Options> threadOptions;
+
+  unsigned numThreads = opts[options::threads];
+
+  /**
+   * Use satRandomSeed for generating random numbers, in particular
+   * satRandomSeed-s
+   */
+  srand((unsigned int)(-opts[options::satRandomSeed]));
+
+  for(unsigned i = 0; i < numThreads; ++i) {
+    threadOptions.push_back(opts);
+    Options& tOpts = threadOptions.back();
+
+    // Set thread identifier
+    tOpts.set(options::thread_id, i);
+
+    // If the random-seed is negative, pick a random seed randomly
+    if(opts[options::satRandomSeed] < 0) {
+      tOpts.set(options::satRandomSeed, (double)rand());
+    }
+
+    if(i < opts[options::threadArgv].size() && 
+       !opts[options::threadArgv][i].empty()) {
+
+      // separate out the thread's individual configuration string
+      stringstream optidss;
+      optidss << "--thread" << i;
+      string optid = optidss.str();
+      int targc = 1;
+      char* tbuf = strdup(opts[options::threadArgv][i].c_str());
+      char* p = tbuf;
+      // string length is certainly an upper bound on size needed
+      char** targv = new char*[opts[options::threadArgv][i].size()];
+      char** vp = targv;
+      *vp++ = strdup(optid.c_str());
+      p = strtok(p, " ");
+      while(p != NULL) {
+        *vp++ = p;
+        ++targc;
+        p = strtok(NULL, " ");
+      }
+      *vp++ = NULL;
+      if(targc > 1) { // this is necessary in case you do e.g. --thread0="  "
+        try {
+          tOpts.parseOptions(targc, targv);
+        } catch(OptionException& e) {
+          stringstream ss;
+          ss << optid << ": " << e.getMessage();
+          throw OptionException(ss.str());
+        }
+        if(optind != targc) {
+          stringstream ss;
+          ss << "unused argument `" << targv[optind]
+             << "' in thread configuration " << optid << " !";
+          throw OptionException(ss.str());
+        }
+        if(tOpts[options::threads] != numThreads
+           || tOpts[options::threadArgv] != opts[options::threadArgv]) {
+          stringstream ss;
+          ss << "not allowed to set thread options in " << optid << " !";
+          throw OptionException(ss.str());
+        }
+      }
+      free(targv[0]);
+      delete targv;
+      free(tbuf);
+    }
+  }
+
+  Assert(numThreads >= 1);      //do we need this?
+
+  return threadOptions;
+}
+
+}/*CVC4 namespace */
diff --git a/src/main/portfolio_util.h b/src/main/portfolio_util.h
new file mode 100644
index 000000000..eed993b9f
--- /dev/null
+++ b/src/main/portfolio_util.h
@@ -0,0 +1,209 @@
+/*********************                                                        */
+/*! \file portfolio_util.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: taking, mdeters
+ ** Minor contributors (to current version): 
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Code relevant only for portfolio builds
+ **/
+
+#ifndef __CVC4_PORTFOLIO_UTIL_H
+#define __CVC4_PORTFOLIO_UTIL_H
+
+#include <queue>
+
+#include "expr/pickler.h"
+#include "util/channel.h"
+#include "util/lemma_input_channel.h"
+#include "util/lemma_output_channel.h"
+#include "main/options.h"
+
+namespace CVC4 {
+
+typedef expr::pickle::Pickle ChannelFormat;
+
+template <typename T>
+class EmptySharedChannel: public SharedChannel<T> {
+public:
+  EmptySharedChannel(int) {}
+  bool push(const T&) { return true; }
+  T pop() { return T(); }
+  bool empty() { return true; }
+  bool full() { return false; }
+};
+
+class PortfolioLemmaOutputChannel : public LemmaOutputChannel {
+private:
+  std::string d_tag;
+  SharedChannel<ChannelFormat>* d_sharedChannel;
+  expr::pickle::MapPickler d_pickler;
+
+public:
+  int cnt;
+  PortfolioLemmaOutputChannel(std::string tag,
+                              SharedChannel<ChannelFormat> *c,
+                              ExprManager* em,
+                              VarMap& to,
+                              VarMap& from) :
+    d_tag(tag),
+    d_sharedChannel(c),
+    d_pickler(em, to, from),
+    cnt(0)
+  {}
+
+  void notifyNewLemma(Expr lemma) {
+    if(Debug.isOn("disable-lemma-sharing")) {
+      return;
+    }
+    if(options::sharingFilterByLength() >= 0) {
+      // 0 would mean no-sharing effectively
+      if(int(lemma.getNumChildren()) > options::sharingFilterByLength()) {
+        return;
+      }
+    }
+    ++cnt;
+    Trace("sharing") << d_tag << ": " << lemma << std::endl;
+    expr::pickle::Pickle pkl;
+    try {
+      d_pickler.toPickle(lemma, pkl);
+      d_sharedChannel->push(pkl);
+      if(Trace.isOn("showSharing") && options::thread_id() == 0) {
+        *options::out() << "thread #0: notifyNewLemma: " << lemma
+                        << std::endl;
+      }
+    } catch(expr::pickle::PicklingException& p){
+      Trace("sharing::blocked") << lemma << std::endl;
+    }
+  }
+
+};/* class PortfolioLemmaOutputChannel */
+
+class PortfolioLemmaInputChannel : public LemmaInputChannel {
+private:
+  std::string d_tag;
+  SharedChannel<ChannelFormat>* d_sharedChannel;
+  expr::pickle::MapPickler d_pickler;
+
+public:
+  PortfolioLemmaInputChannel(std::string tag,
+                             SharedChannel<ChannelFormat>* c,
+                             ExprManager* em,
+                             VarMap& to,
+                             VarMap& from) :
+    d_tag(tag),
+    d_sharedChannel(c),
+    d_pickler(em, to, from){
+  }
+
+  bool hasNewLemma(){
+    Debug("lemmaInputChannel") << d_tag << ": " << "hasNewLemma" << std::endl;
+    return !d_sharedChannel->empty();
+  }
+
+  Expr getNewLemma() {
+    Debug("lemmaInputChannel") << d_tag << ": " << "getNewLemma" << std::endl;
+    expr::pickle::Pickle pkl = d_sharedChannel->pop();
+
+    Expr e = d_pickler.fromPickle(pkl);
+    if(Trace.isOn("showSharing") && options::thread_id() == 0) {
+      *options::out() << "thread #0: getNewLemma: " << e << std::endl;
+    }
+    return e;
+  }
+
+};/* class PortfolioLemmaInputChannel */
+
+std::vector<Options> parseThreadSpecificOptions(Options opts);
+
+template<typename T>
+void sharingManager(unsigned numThreads,
+                    SharedChannel<T> *channelsOut[], // out and in with respect
+                    SharedChannel<T> *channelsIn[],
+                    SmtEngine *smts[])  // to smt engines
+{
+  Trace("sharing") << "sharing: thread started " << std::endl;
+  std::vector <int> cnt(numThreads); // Debug("sharing")
+
+  std::vector< std::queue<T> > queues;
+  for(unsigned i = 0; i < numThreads; ++i){
+    queues.push_back(std::queue<T>());
+  }
+
+  const unsigned int sharingBroadcastInterval = 1;
+
+  boost::mutex mutex_activity;
+
+  /* Disable interruption, so that we can check manually */
+  boost::this_thread::disable_interruption di;
+
+  while(not boost::this_thread::interruption_requested()) {
+
+    boost::this_thread::sleep
+      (boost::posix_time::milliseconds(sharingBroadcastInterval));
+
+    for(unsigned t = 0; t < numThreads; ++t) {
+
+      /* No activity on this channel */
+      if(channelsOut[t]->empty()) continue;
+
+      /* Alert if channel full, so that we increase sharingChannelSize
+         or decrease sharingBroadcastInterval */
+      Assert(not channelsOut[t]->full());
+
+      T data = channelsOut[t]->pop();
+
+      if(Trace.isOn("sharing")) {
+        ++cnt[t];
+        Trace("sharing") << "sharing: Got data. Thread #" << t
+                         << ". Chunk " << cnt[t] << std::endl;
+      }
+
+      for(unsigned u = 0; u < numThreads; ++u) {
+        if(u != t){
+          Trace("sharing") << "sharing: adding to queue " << u << std::endl;
+          queues[u].push(data);
+        }
+      }/* end of inner for: broadcast activity */
+
+    } /* end of outer for: look for activity */
+
+    for(unsigned t = 0; t < numThreads; ++t){
+      /* Alert if channel full, so that we increase sharingChannelSize
+         or decrease sharingBroadcastInterval */
+      Assert(not channelsIn[t]->full());
+
+      while(!queues[t].empty() && !channelsIn[t]->full()){
+        Trace("sharing") << "sharing: pushing on channel " << t << std::endl;
+        T data = queues[t].front();
+        channelsIn[t]->push(data);
+        queues[t].pop();
+      }
+    }
+  } /* end of infinite while */
+
+  Trace("interrupt")
+    << "sharing thread interrupted, interrupting all smtEngines" << std::endl;
+
+  for(unsigned t = 0; t < numThreads; ++t) {
+    Trace("interrupt") << "Interrupting thread #" << t << std::endl;
+    try{
+      smts[t]->interrupt();
+    }catch(ModalException &e){
+      // It's fine, the thread is probably not there.
+      Trace("interrupt") << "Could not interrupt thread #" << t << std::endl;
+    }
+  }
+
+  Trace("sharing") << "sharing: Interrupted, exiting." << std::endl;
+}
+
+}/*CVC4 namespace*/
+
+#endif   /* __CVC4_PORTFOLIO_UTIL_H */
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 54309cd01..281645317 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -271,6 +271,7 @@ bool PropEngine::isRunning() const {
 
 void PropEngine::interrupt() throw(ModalException) {
   if(! d_inCheckSat) {
+    return;
     throw ModalException("SAT solver is not currently solving anything; "
                          "cannot interrupt it");
   }