portfolio merge

9 files changed, 1360 insertions, 338 deletions

diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 78d468000..ae7764e32 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -4,16 +4,42 @@ AM_CPPFLAGS = \
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas
 
 bin_PROGRAMS = cvc4
+
 noinst_LIBRARIES = libmain.a
 
 libmain_a_SOURCES = \
 	interactive_shell.h \
 	interactive_shell.cpp \
 	main.h \
-	main.cpp \
 	util.cpp
 
-cvc4_SOURCES =
+if CVC4_HAS_THREADS
+bin_PROGRAMS += pcvc4
+pcvc4_SOURCES = \
+	main.cpp \
+	portfolio.cpp \
+	portfolio.h \
+	driver_portfolio.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_LDADD += $(BOOST_THREAD_LIBS) -lpthread
+pcvc4_LDADD += $(BOOST_THREAD_LDFLAGS)
+
+if STATIC_BINARY
+pcvc4_LINK = $(CXXLINK) -all-static
+else
+pcvc4_LINK = $(CXXLINK)
+endif
+endif
+
+cvc4_SOURCES = \
+	main.cpp \
+	driver.cpp
 cvc4_LDADD = \
 	libmain.a \
 	@builddir@/../parser/libcvc4parser.la \
@@ -44,3 +70,4 @@ cvc4_LINK = $(CXXLINK) -all-static
 else
 cvc4_LINK = $(CXXLINK)
 endif
+
diff --git a/src/main/driver.cpp b/src/main/driver.cpp
new file mode 100644
index 000000000..e9bfde024
--- /dev/null
+++ b/src/main/driver.cpp
@@ -0,0 +1,355 @@
+/*********************                                                        */
+/*! \file driver.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): barrett, dejan, taking
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011, 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 (sequential) CVC4 executable
+ **
+ ** Driver for (sequential) CVC4 executable.
+ **/
+
+#include <cstdlib>
+#include <cstring>
+#include <fstream>
+#include <iostream>
+#include <new>
+
+#include <stdio.h>
+#include <unistd.h>
+
+#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 "smt/smt_engine.h"
+#include "expr/command.h"
+#include "util/Assert.h"
+#include "util/configuration.h"
+#include "util/options.h"
+#include "util/output.h"
+#include "util/result.h"
+#include "util/stats.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::parser;
+using namespace CVC4::main;
+
+static bool doCommand(SmtEngine&, Command*, Options&);
+
+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;
+
+    /** A pointer to the StatisticsRegistry (the signal handlers need it) */
+    CVC4::StatisticsRegistry* pStatistics;
+  }
+}
+
+
+void printUsage(Options& options, bool full) {
+  stringstream ss;
+  ss << "usage: " << 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(), *options.out );
+  } else {
+    Options::printShortUsage( ss.str(), *options.out );
+  }
+}
+
+int runCvc4(int argc, char* argv[], Options& options) {
+
+  // For the signal handlers' benefit
+  pOptions = &options;
+
+  // Initialize the signal handlers
+  cvc4_init();
+
+  progPath = argv[0];
+
+  // Parse the options
+  int firstArgIndex = options.parseOptions(argc, argv);
+
+  progName = options.binary_name.c_str();
+
+  if( options.help ) {
+    printUsage(options, true);
+    exit(1);
+  } else if( options.languageHelp ) {
+    Options::printLanguageHelp(*options.out);
+    exit(1);
+  } else if( options.version ) {
+    *options.out << Configuration::about().c_str() << flush;
+    exit(0);
+  }
+
+  segvNoSpin = options.segvNoSpin;
+
+  // If in competition mode, set output stream option to flush immediately
+#ifdef CVC4_COMPETITION_MODE
+  *options.out << unitbuf;
+#endif
+
+  // 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(!options.interactiveSetByUser) {
+    options.interactive = inputFromStdin && isatty(fileno(stdin));
+  }
+
+  // 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(options.verbosity < 2) {
+      Chat.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 1) {
+      Notice.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 0) {
+      Message.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    }
+  }
+
+  // Create the expression manager
+  ExprManager exprMgr(options);
+
+  // Create the SmtEngine
+  SmtEngine smt(&exprMgr);
+
+  // signal handlers need access
+  pStatistics = smt.getStatisticsRegistry();
+
+  // Auto-detect input language by filename extension
+  const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
+
+  ReferenceStat< const char* > s_statFilename("filename", filename);
+  RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
+
+  if(options.inputLanguage == language::input::LANG_AUTO) {
+    if( inputFromStdin ) {
+      // We can't do any fancy detection on stdin
+      options.inputLanguage = language::input::LANG_CVC4;
+    } else {
+      unsigned len = strlen(filename);
+      if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
+        options.inputLanguage = language::input::LANG_SMTLIB_V2;
+      } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
+        options.inputLanguage = language::input::LANG_SMTLIB;
+      } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
+                || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
+        options.inputLanguage = language::input::LANG_CVC4;
+      }
+    }
+  }
+
+  if(options.outputLanguage == language::output::LANG_AUTO) {
+    options.outputLanguage = language::toOutputLanguage(options.inputLanguage);
+  }
+
+  // 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(options.verbosity < 2) {
+      Chat.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 1) {
+      Notice.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 0) {
+      Message.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    }
+
+    Debug.getStream() << Expr::setlanguage(options.outputLanguage);
+    Trace.getStream() << Expr::setlanguage(options.outputLanguage);
+    Notice.getStream() << Expr::setlanguage(options.outputLanguage);
+    Chat.getStream() << Expr::setlanguage(options.outputLanguage);
+    Message.getStream() << Expr::setlanguage(options.outputLanguage);
+    Warning.getStream() << Expr::setlanguage(options.outputLanguage);
+    Dump.getStream() << Expr::setlanguage(options.outputLanguage)
+                     << Expr::setdepth(-1)
+                     << Expr::printtypes(false);
+  }
+
+  Parser* replayParser = NULL;
+  if( options.replayFilename != "" ) {
+    ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options);
+
+    if( options.replayFilename == "-") {
+      if( inputFromStdin ) {
+        throw OptionException("Replay file and input file can't both be stdin.");
+      }
+      replayParserBuilder.withStreamInput(cin);
+    }
+    replayParser = replayParserBuilder.build();
+    options.replayStream = new Parser::ExprStream(replayParser);
+  }
+  if( options.replayLog != NULL ) {
+    *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
+  }
+
+  // Parse and execute commands until we are done
+  Command* cmd;
+  bool status = true;
+  if( options.interactive ) {
+    InteractiveShell shell(exprMgr, options);
+    Message() << Configuration::getPackageName()
+              << " " << Configuration::getVersionString();
+    if(Configuration::isSubversionBuild()) {
+      Message() << " [" << Configuration::getSubversionId() << "]";
+    }
+    Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
+              << " assertions:"
+              << (Configuration::isAssertionBuild() ? "on" : "off")
+              << endl;
+    if(replayParser != NULL) {
+      // have the replay parser use the declarations input interactively
+      replayParser->useDeclarationsFrom(shell.getParser());
+    }
+    while((cmd = shell.readCommand())) {
+      status = doCommand(smt,cmd, options) && status;
+      delete cmd;
+    }
+  } else {
+    ParserBuilder parserBuilder(&exprMgr, filename, options);
+
+    if( inputFromStdin ) {
+      parserBuilder.withStreamInput(cin);
+    }
+
+    Parser *parser = parserBuilder.build();
+    if(replayParser != NULL) {
+      // have the replay parser use the file's declarations
+      replayParser->useDeclarationsFrom(parser);
+    }
+    while((cmd = parser->nextCommand())) {
+      status = doCommand(smt, cmd, options) && status;
+      delete cmd;
+    }
+    // Remove the parser
+    delete parser;
+  }
+
+  if( options.replayStream != NULL ) {
+    // this deletes the expression parser too
+    delete options.replayStream;
+    options.replayStream = NULL;
+  }
+
+  int returnValue;
+  string result = "unknown";
+  if(status) {
+    result = smt.getInfo(":status").getValue();
+
+    if(result == "sat") {
+      returnValue = 10;
+    } else if(result == "unsat") {
+      returnValue = 20;
+    } else {
+      returnValue = 0;
+    }
+  } else {
+    // there was some kind of error
+    returnValue = 1;
+  }
+
+#ifdef CVC4_COMPETITION_MODE
+  // exit, don't return
+  // (don't want destructors to run)
+  exit(returnValue);
+#endif
+
+  ReferenceStat< Result > s_statSatResult("sat/unsat", result);
+  RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
+
+  if(options.statistics) {
+    pStatistics->flushInformation(*options.err);
+  }
+
+  return returnValue;
+}
+
+/** Executes a command. Deletes the command after execution. */
+static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
+  if( 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, options) && status;
+    }
+  } else {
+    // by default, symmetry breaker is on only for QF_UF
+    if(! options.ufSymmetryBreakerSetByUser) {
+      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
+      if(logic != NULL) {
+        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
+      }
+    }
+
+    if(options.verbosity > 0) {
+      *options.out << "Invoking: " << *cmd << endl;
+    }
+
+    if(options.verbosity >= 0) {
+      cmd->invoke(&smt, *options.out);
+    } else {
+      cmd->invoke(&smt);
+    }
+    status = status && cmd->ok();
+  }
+
+  return status;
+}
diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
new file mode 100644
index 000000000..5c8f908f8
--- /dev/null
+++ b/src/main/driver_portfolio.cpp
@@ -0,0 +1,808 @@
+#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 "util/options.h"
+#include "util/output.h"
+#include "util/result.h"
+#include "util/stats.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(int 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;
+    const Options *options = Options::current();
+    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") and options->thread_id == 0) {
+        *(Options::current()->out) << "thread #0: notifyNewLemma: " << lemma << endl;
+      }
+    }catch(expr::pickle::PicklingException& p){
+      Trace("sharing::blocked") << lemma << std::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") and Options::current()->thread_id == 0) {
+      *(Options::current()->out) << "thread #0: getNewLemma: " << e << endl;
+    }
+    return e;
+  }
+
+};/* class PortfolioLemmaInputChannel */
+
+
+
+int runCvc4(int argc, char *argv[], Options& options) {
+
+#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 = &options;
+
+  // Initialize the signal handlers
+  cvc4_init();
+
+  progPath = argv[0];
+
+
+  /****************************** Options Processing ************************/
+
+  // Parse the options
+  int firstArgIndex = options.parseOptions(argc, argv);
+
+  progName = options.binary_name.c_str();
+
+  if( options.help ) {
+    printUsage(options, true);
+    exit(1);
+  } else if( options.languageHelp ) {
+    Options::printLanguageHelp(*options.out);
+    exit(1);
+  } else if( options.version ) {
+    *options.out << Configuration::about().c_str() << flush;
+    exit(0);
+  }
+
+  int numThreads = options.threads;
+
+  if(options.threadArgv.size() > size_t(numThreads)) {
+    stringstream ss;
+    ss << "--thread" << (options.threadArgv.size() - 1)
+       << " configuration string seen but this portfolio will only contain "
+       << numThreads << " thread(s)!";
+    throw OptionException(ss.str());
+  }
+
+  segvNoSpin = options.segvNoSpin;
+
+  // If in competition mode, set output stream option to flush immediately
+#ifdef CVC4_COMPETITION_MODE
+  *options.out << unitbuf;
+#endif
+
+  // 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(!options.interactiveSetByUser) {
+    options.interactive = inputFromStdin && isatty(fileno(stdin));
+  }
+
+  // Auto-detect input language by filename extension
+  const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
+
+  if(options.inputLanguage == language::input::LANG_AUTO) {
+    if( inputFromStdin ) {
+      // We can't do any fancy detection on stdin
+      options.inputLanguage = language::input::LANG_CVC4;
+    } else {
+      unsigned len = strlen(filename);
+      if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
+        options.inputLanguage = language::input::LANG_SMTLIB_V2;
+      } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
+        options.inputLanguage = language::input::LANG_SMTLIB;
+      } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
+                || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
+        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);
+  } else {
+    if(options.verbosity < 2) {
+      Chat.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 1) {
+      Notice.setStream(CVC4::null_os);
+    }
+    if(options.verbosity < 0) {
+      Message.setStream(CVC4::null_os);
+      Warning.setStream(CVC4::null_os);
+    }
+
+    OutputLanguage language = language::toOutputLanguage(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);
+  }
+
+  vector<Options> threadOptions;
+  for(int i = 0; i < numThreads; ++i) {
+    threadOptions.push_back(options);
+    Options& opts = threadOptions.back();
+
+    // Set thread identifier
+    opts.thread_id = i;
+
+    // If the random-seed is negative, pick a random seed randomly
+    if(options.satRandomSeed < 0)
+      opts.satRandomSeed = (double)rand();
+
+    if(i < (int)options.threadArgv.size() && !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(options.threadArgv[i].c_str());
+      char* p = tbuf;
+      // string length is certainly an upper bound on size needed
+      char** targv = new char*[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 {
+          opts.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(opts.threads != numThreads || opts.threadArgv != 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)(-options.satRandomSeed));
+
+  assert(numThreads >= 1);      //do we need this?
+
+  /* Output to string stream  */
+  vector<stringstream*> ss_out(numThreads);
+  if(options.verbosity == 0 or options.separateOutput) {
+    for(int i = 0;i <numThreads; ++i) {
+      ss_out[i] = new stringstream;
+      threadOptions[i].out = ss_out[i];
+    }
+  }
+
+  /****************************** Driver Statistics *************************/
+
+  // Statistics init
+  pStatistics = &theStatisticsRegistry;
+
+  StatisticsRegistry driverStatisticsRegistry("driver");
+  theStatisticsRegistry.registerStat_((&driverStatisticsRegistry));
+
+  // Timer statistic
+  RegisterStatistic* statTotatTime =
+    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( options.interactive ) {
+    InteractiveShell shell(*exprMgr, options);
+    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(options);
+
+    if( inputFromStdin ) {
+      parserBuilder.withStreamInput(cin);
+    }
+
+    Parser *parser = parserBuilder.build();
+    while((cmd = parser->nextCommand())) {
+      seq->addCommand(cmd);
+      // doCommand(smt, cmd, options);
+      // delete cmd;
+    }
+    // Remove the parser
+    delete parser;
+  }
+
+  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(int 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(int i = 0; i < numThreads; ++i) {
+    smts[i] = new SmtEngine(exprMgrs[i]);
+
+    // Register the statistics registry of the thread
+    string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id);
+    smts[i]->getStatisticsRegistry()->setName(tag);
+    theStatisticsRegistry.registerStat_( (Stat*)smts[i]->getStatisticsRegistry() );
+  }
+
+  /************************* Lemma sharing init ************************/
+
+  /* Sharing channels */
+  SharedChannel<channelFormat> *channelsOut[numThreads], *channelsIn[numThreads];
+
+  if(numThreads == 1) {
+    // Disable sharing
+    threadOptions[0].sharingFilterByLength = 0;
+  } else {
+    // Setup sharing channels
+    const unsigned int sharingChannelSize = 1000000;
+
+    for(int 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(int i = 0; i<numThreads; ++i) {
+      string tag = "thread #" + boost::lexical_cast<string>(threadOptions[i].thread_id);
+      threadOptions[i].lemmaOutputChannel =
+        new PortfolioLemmaOutputChannel(tag, channelsOut[i], exprMgrs[i],
+                                        vmaps[i]->d_from, vmaps[i]->d_to);
+      threadOptions[i].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(int 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(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
+
+  // ReferenceStat< Result > s_statSatResult("sat/unsat", result);
+  // RegisterStatistic statSatResultReg(*exprMgr, &s_statSatResult);
+
+  // Stop timers, enough work done
+  s_totalTime.stop();
+
+  if(options.statistics) {
+    pStatistics->flushInformation(*options.err);
+  }
+
+  if(options.separateOutput) {
+    for(int i = 0; i < numThreads; ++i) {
+      *options.out << "--- Output from thread #" << i << " ---" << endl;
+      *options.out << ss_out[i]->str();
+    }
+  }
+
+  /*if(options.statistics) {
+    double totalTime = double(s_totalTime.getData().tv_sec) +
+        double(s_totalTime.getData().tv_nsec)/1000000000.0;
+    cout.precision(6);
+    *options.err << "real time: " << totalTime << "s\n";
+    int th0_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(options.lemmaOutputChannel)).cnt;
+    int th1_lemcnt = (*static_cast<PortfolioLemmaOutputChannel*>(threadOptions[1].lemmaOutputChannel)).cnt;
+    *options.err << "lemmas shared by thread #0: " << th0_lemcnt << endl;
+    *options.err << "lemmas shared by thread #1: " << th1_lemcnt << endl;
+    *options.err << "sharing rate: " << double(th0_lemcnt+th1_lemcnt)/(totalTime)
+                 << " lem/sec" << endl;
+    *options.err << "winner: #" << (winner == 0 ? 0 : 1) << endl;
+  }*/
+
+  // destruction is causing segfaults, let us just exit
+  exit(returnValue);
+
+  //delete vmaps;
+
+  delete statTotatTime;
+  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& options, bool full) {
+  stringstream ss;
+  ss << "usage: " << 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(), *options.out );
+  } else {
+    Options::printShortUsage( ss.str(), *options.out );
+  }
+}
+
+/** Executes a command. Deletes the command after execution. */
+static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
+  if( 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, options) && status;
+    }
+  } else {
+    // by default, symmetry breaker is on only for QF_UF
+    if(! options.ufSymmetryBreakerSetByUser) {
+      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
+      if(logic != NULL) {
+        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
+      }
+    }
+
+    if(options.verbosity > 0) {
+      *options.out << "Invoking: " << *cmd << endl;
+    }
+
+    if(options.verbosity >= 0) {
+      cmd->invoke(&smt, *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 &options) {
+
+  try {
+    // For the signal handlers' benefit
+    pOptions = &options;
+
+    // Execute the commands
+    bool status = doCommand(smt, cmd, options);
+
+    // if(options.statistics) {
+    //   smt.getStatisticsRegistry()->flushInformation(*options.err);
+    //   *options.err << "Statistics printing of my thread complete " << endl;
+    // }
+
+    return status ? smt.getStatusOfLastCommand() : Result::SAT_UNKNOWN;
+  } catch(OptionException& e) {
+    *pOptions->out << "unknown" << endl;
+    cerr << "CVC4 Error:" << endl << e << endl;
+    printUsage(*pOptions);
+    return Result::SAT_UNKNOWN;
+  } catch(Exception& e) {
+#ifdef CVC4_COMPETITION_MODE
+    *pOptions->out << "unknown" << endl;
+#endif
+    *pOptions->err << "CVC4 Error:" << endl << e << endl;
+    if(pOptions->statistics) {
+      pStatistics->flushInformation(*pOptions->err);
+    }
+    return Result::SAT_UNKNOWN;
+  } catch(bad_alloc) {
+#ifdef CVC4_COMPETITION_MODE
+    *pOptions->out << "unknown" << endl;
+#endif
+    *pOptions->err << "CVC4 ran out of memory." << endl;
+    if(pOptions->statistics) {
+      pStatistics->flushInformation(*pOptions->err);
+    }
+    return Result::SAT_UNKNOWN;
+  } catch(...) {
+#ifdef CVC4_COMPETITION_MODE
+    *pOptions->out << "unknown" << endl;
+#endif
+    *pOptions->err << "CVC4 threw an exception of unknown type." << endl;
+    return Result::SAT_UNKNOWN;
+  }
+}
+
+template<typename T>
+void sharingManager(int numThreads,
+                    SharedChannel<T> *channelsOut[], // out and in with respect
+                    SharedChannel<T> *channelsIn[],
+                    SmtEngine *smts[])  // to smt engines
+{
+  Trace("sharing") << "sharing: thread started " << std::endl;
+  vector <int> cnt(numThreads); // Debug("sharing")
+
+  vector< queue<T> > queues;
+  for(int 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(int 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(int 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(int 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 interuppted, interrupting all smtEngines" << std::endl;
+
+  for(int t = 0; t < numThreads; ++t) {
+    Trace("interrupt") << "Interuppting 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: Interuppted, exiting." << std::endl;
+}
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index dca554330..a63d6c67b 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -85,7 +85,7 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
   d_out(*options.out),
   d_language(options.inputLanguage),
   d_quit(false) {
-  ParserBuilder parserBuilder(&exprManager,INPUT_FILENAME,options);
+  ParserBuilder parserBuilder(&exprManager, INPUT_FILENAME, options);
   /* Create parser with bogus input. */
   d_parser = parserBuilder.withStringInput("").build();
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index ecef7e79f..5d051cdad 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -20,12 +20,10 @@
 #include <cstring>
 #include <fstream>
 #include <iostream>
-#include <new>
 
 #include <stdio.h>
 #include <unistd.h>
 
-#include "cvc4autoconfig.h"
 #include "main/main.h"
 #include "main/interactive_shell.h"
 #include "parser/parser.h"
@@ -43,42 +41,8 @@
 
 using namespace std;
 using namespace CVC4;
-using namespace CVC4::parser;
 using namespace CVC4::main;
 
-static int runCvc4(int argc, char* argv[]);
-static bool doCommand(SmtEngine&, Command*);
-static void printUsage(bool full = false);
-
-namespace CVC4 {
-  namespace main {
-    /** Global options variable */
-    Options options;
-
-    /** Full argv[0] */
-    const char *progPath;
-
-    /** Just the basename component of argv[0] */
-    const char *progName;
-
-    /** A pointer to the StatisticsRegistry (the signal handlers need it) */
-    CVC4::StatisticsRegistry* pStatistics;
-  }
-}
-
-static void printUsage(bool full) {
-  stringstream ss;
-  ss << "usage: " << options.binary_name << " [options] [input-file]" << endl
-      << endl
-      << "Without an input file, or with `-', CVC4 reads from standard input." << endl
-      << endl;
-  if(full) {
-    Options::printUsage( ss.str(), *options.out );
-  } else {
-    Options::printShortUsage( ss.str(), *options.out );
-  }
-}
-
 /**
  * CVC4's main() routine is just an exception-safe wrapper around CVC4.
  * Please don't construct anything here.  Even if the constructor is
@@ -87,14 +51,15 @@ static void printUsage(bool full) {
  * Put everything in runCvc4().
  */
 int main(int argc, char* argv[]) {
+  Options options;
   try {
-    return runCvc4(argc, argv);
+    return runCvc4(argc, argv, options);
   } catch(OptionException& e) {
 #ifdef CVC4_COMPETITION_MODE
     *options.out << "unknown" << endl;
 #endif
     cerr << "CVC4 Error:" << endl << e << endl;
-    printUsage();
+    printUsage(options);
     exit(1);
   } catch(Exception& e) {
 #ifdef CVC4_COMPETITION_MODE
@@ -102,7 +67,7 @@ int main(int argc, char* argv[]) {
 #endif
     *options.err << "CVC4 Error:" << endl << e << endl;
     if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushStatistics(*options.err);
+      pStatistics->flushInformation(*options.err);
     }
     exit(1);
   } catch(bad_alloc&) {
@@ -111,7 +76,7 @@ int main(int argc, char* argv[]) {
 #endif
     *options.err << "CVC4 ran out of memory." << endl;
     if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushStatistics(*options.err);
+      pStatistics->flushInformation(*options.err);
     }
     exit(1);
   } catch(...) {
@@ -122,276 +87,3 @@ int main(int argc, char* argv[]) {
     exit(1);
   }
 }
-
-
-static int runCvc4(int argc, char* argv[]) {
-
-  // Initialize the signal handlers
-  cvc4_init();
-
-  progPath = argv[0];
-
-  // Parse the options
-  int firstArgIndex = options.parseOptions(argc, argv);
-
-  progName = options.binary_name.c_str();
-
-  if( options.help ) {
-    printUsage(true);
-    exit(1);
-  } else if( options.languageHelp ) {
-    Options::printLanguageHelp(*options.out);
-    exit(1);
-  } else if( options.version ) {
-    *options.out << Configuration::about().c_str() << flush;
-    exit(0);
-  }
-
-  segvNoSpin = options.segvNoSpin;
-
-  // If in competition mode, set output stream option to flush immediately
-#ifdef CVC4_COMPETITION_MODE
-  *options.out << unitbuf;
-#endif
-
-  // 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(!options.interactiveSetByUser) {
-    options.interactive = inputFromStdin && isatty(fileno(stdin));
-  }
-
-  // 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(options.verbosity < 2) {
-      Chat.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 1) {
-      Notice.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 0) {
-      Message.setStream(CVC4::null_os);
-      Warning.setStream(CVC4::null_os);
-    }
-  }
-
-  // Create the expression manager
-  ExprManager exprMgr(options);
-
-  // Create the SmtEngine
-  SmtEngine smt(&exprMgr);
-
-  // signal handlers need access
-  pStatistics = smt.getStatisticsRegistry();
-
-  // Auto-detect input language by filename extension
-  const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
-
-  ReferenceStat< const char* > s_statFilename("filename", filename);
-  RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
-
-  if(options.inputLanguage == language::input::LANG_AUTO) {
-    if( inputFromStdin ) {
-      // We can't do any fancy detection on stdin
-      options.inputLanguage = language::input::LANG_CVC4;
-    } else {
-      unsigned len = strlen(filename);
-      if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
-        options.inputLanguage = language::input::LANG_SMTLIB_V2;
-      } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
-        options.inputLanguage = language::input::LANG_SMTLIB;
-      } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
-                || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
-        options.inputLanguage = language::input::LANG_CVC4;
-      }
-    }
-  }
-
-  if(options.outputLanguage == language::output::LANG_AUTO) {
-    options.outputLanguage = language::toOutputLanguage(options.inputLanguage);
-  }
-
-  // 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(options.verbosity < 2) {
-      Chat.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 1) {
-      Notice.setStream(CVC4::null_os);
-    }
-    if(options.verbosity < 0) {
-      Message.setStream(CVC4::null_os);
-      Warning.setStream(CVC4::null_os);
-    }
-
-    Debug.getStream() << Expr::setlanguage(options.outputLanguage);
-    Trace.getStream() << Expr::setlanguage(options.outputLanguage);
-    Notice.getStream() << Expr::setlanguage(options.outputLanguage);
-    Chat.getStream() << Expr::setlanguage(options.outputLanguage);
-    Message.getStream() << Expr::setlanguage(options.outputLanguage);
-    Warning.getStream() << Expr::setlanguage(options.outputLanguage);
-    Dump.getStream() << Expr::setlanguage(options.outputLanguage)
-                     << Expr::setdepth(-1)
-                     << Expr::printtypes(false);
-  }
-
-  Parser* replayParser = NULL;
-  if( options.replayFilename != "" ) {
-    ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options);
-
-    if( options.replayFilename == "-") {
-      if( inputFromStdin ) {
-        throw OptionException("Replay file and input file can't both be stdin.");
-      }
-      replayParserBuilder.withStreamInput(cin);
-    }
-    replayParser = replayParserBuilder.build();
-    options.replayStream = new Parser::ExprStream(replayParser);
-  }
-  if( options.replayLog != NULL ) {
-    *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
-  }
-
-  // Parse and execute commands until we are done
-  Command* cmd;
-  bool status = true;
-  if( options.interactive ) {
-    InteractiveShell shell(exprMgr, options);
-    Message() << Configuration::getPackageName()
-              << " " << Configuration::getVersionString();
-    if(Configuration::isSubversionBuild()) {
-      Message() << " [" << Configuration::getSubversionId() << "]";
-    }
-    Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
-              << " assertions:"
-              << (Configuration::isAssertionBuild() ? "on" : "off")
-              << endl;
-    if(replayParser != NULL) {
-      // have the replay parser use the declarations input interactively
-      replayParser->useDeclarationsFrom(shell.getParser());
-    }
-    while((cmd = shell.readCommand())) {
-      status = doCommand(smt, cmd) && status;
-      delete cmd;
-    }
-  } else {
-    ParserBuilder parserBuilder(&exprMgr, filename, options);
-
-    if( inputFromStdin ) {
-      parserBuilder.withStreamInput(cin);
-    }
-
-    Parser *parser = parserBuilder.build();
-    if(replayParser != NULL) {
-      // have the replay parser use the file's declarations
-      replayParser->useDeclarationsFrom(parser);
-    }
-    while((cmd = parser->nextCommand())) {
-      status = doCommand(smt, cmd) && status;
-      delete cmd;
-    }
-    // Remove the parser
-    delete parser;
-  }
-
-  if( options.replayStream != NULL ) {
-    // this deletes the expression parser too
-    delete options.replayStream;
-    options.replayStream = NULL;
-  }
-
-  int returnValue;
-  string result = "unknown";
-  if(status) {
-    result = smt.getInfo(":status").getValue();
-
-    if(result == "sat") {
-      returnValue = 10;
-    } else if(result == "unsat") {
-      returnValue = 20;
-    } else {
-      returnValue = 0;
-    }
-  } else {
-    // there was some kind of error
-    returnValue = 1;
-  }
-
-#ifdef CVC4_COMPETITION_MODE
-  // exit, don't return
-  // (don't want destructors to run)
-  exit(returnValue);
-#endif
-
-  ReferenceStat< Result > s_statSatResult("sat/unsat", result);
-  RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
-
-  if(options.statistics) {
-    smt.getStatisticsRegistry()->flushStatistics(*options.err);
-  }
-
-  return returnValue;
-}
-
-/** Executes a command. Deletes the command after execution. */
-static bool doCommand(SmtEngine& smt, Command* cmd) {
-  if( 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) && status;
-    }
-  } else {
-    // by default, symmetry breaker is on only for QF_UF
-    if(! options.ufSymmetryBreakerSetByUser) {
-      SetBenchmarkLogicCommand *logic = dynamic_cast<SetBenchmarkLogicCommand*>(cmd);
-      if(logic != NULL) {
-        options.ufSymmetryBreaker = (logic->getLogic() == "QF_UF");
-      }
-    }
-
-    if(options.verbosity > 0) {
-      *options.out << "Invoking: " << *cmd << endl;
-    }
-
-    if(options.verbosity >= 0) {
-      cmd->invoke(&smt, *options.out);
-    } else {
-      cmd->invoke(&smt);
-    }
-    status = status && cmd->ok();
-  }
-
-  return status;
-}
diff --git a/src/main/main.h b/src/main/main.h
index 1771198f4..4df5ccc49 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -22,6 +22,7 @@
 #include "util/options.h"
 #include "util/exception.h"
 #include "util/stats.h"
+#include "util/tls.h"
 #include "cvc4autoconfig.h"
 
 #ifndef __CVC4__MAIN__MAIN_H
@@ -46,8 +47,8 @@ extern CVC4::StatisticsRegistry* pStatistics;
  */
 extern bool segvNoSpin;
 
-/** The options currently in play */
-extern Options options;
+/** A pointer to the options in play */
+extern CVC4_THREADLOCAL(Options*) pOptions;
 
 /** Initialize the driver.  Sets signal handlers for SIGINT and SIGSEGV. */
 void cvc4_init() throw(Exception);
@@ -55,4 +56,8 @@ void cvc4_init() throw(Exception);
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
 
+/** Actual Cvc4 driver functions **/
+int runCvc4(int argc, char* argv[], CVC4::Options&);
+void printUsage(CVC4::Options&, bool full = false);
+
 #endif /* __CVC4__MAIN__MAIN_H */
diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp
new file mode 100644
index 000000000..fc22374cf
--- /dev/null
+++ b/src/main/portfolio.cpp
@@ -0,0 +1,93 @@
+/*********************                                                        */
+/*! \file portfolio.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include <boost/function.hpp>
+#include <boost/thread.hpp>
+#include <boost/bind.hpp>
+#include <boost/thread/condition.hpp>
+#include <boost/exception_ptr.hpp>
+
+#include "smt/smt_engine.h"
+#include "util/result.h"
+#include "util/options.h"
+
+using namespace boost;
+
+namespace CVC4 {
+
+mutex mutex_done;
+mutex mutex_main_wait;
+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) {
+  returnValue = threadFn();
+
+  if( mutex_done.try_lock() ) {
+    if(global_flag_done == false) {
+      global_flag_done = true;
+      global_winner = thread_id;
+    }
+    mutex_done.unlock();
+    condition_var_main_wait.notify_all(); // we want main thread to quit
+  }
+}
+
+template<typename T, typename S>
+std::pair<int, S> runPortfolio(int numThreads,
+                               function<T()> driverFn,
+                               function<S()> threadFns[],
+                               bool optionWaitToJoin) {
+  thread thread_driver;
+  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]) ));
+  }
+
+  if(not driverFn.empty())
+    thread_driver = boost::thread(driverFn);
+
+  while(global_flag_done == false)
+    condition_var_main_wait.wait(mutex_main_wait);
+
+  if(not driverFn.empty()) {
+    thread_driver.interrupt();
+    thread_driver.join();
+  }
+
+  for(int t = 0; t < numThreads; ++t) {
+    if(optionWaitToJoin) {
+      threads[t].join();
+    }
+  }
+
+  return std::pair<int, S>(global_winner,threads_returnValue[global_winner]);
+}
+
+// instantiation
+template
+std::pair<int, Result>
+runPortfolio<void, Result>(int, boost::function<void()>, boost::function<Result()>*, bool);
+
+}/* CVC4 namespace */
diff --git a/src/main/portfolio.h b/src/main/portfolio.h
new file mode 100644
index 000000000..9bc911be3
--- /dev/null
+++ b/src/main/portfolio.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file portfolio.h
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: none
+ ** 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 [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#ifndef __CVC4__PORTFOLIO_H
+#define __CVC4__PORTFOLIO_H
+
+#include <boost/function.hpp>
+#include <utility>
+
+#include "smt/smt_engine.h"
+#include "expr/command.h"
+#include "util/options.h"
+
+namespace CVC4 {
+
+template<typename T, typename S>
+std::pair<int, S> runPortfolio(int numThreads, 
+                              boost::function<T()> driverFn,
+                              boost::function<S()> threadFns[],
+                              bool optionWaitToJoin);
+// as we have defined things, S=void would give compile errors
+// do we want to fix this? yes, no, maybe?
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PORTFOLIO_H */
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 89aa5c6aa..35cff4abd 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -51,8 +51,8 @@ bool segvNoSpin = false;
 /** Handler for SIGXCPU, i.e., timeout. */
 void timeout_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by timeout.\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   abort();
 }
@@ -60,8 +60,8 @@ void timeout_handler(int sig, siginfo_t* info, void*) {
 /** Handler for SIGINT, i.e., when the user hits control C. */
 void sigint_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 interrupted by user.\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   abort();
 }
@@ -85,8 +85,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
 
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushStatistics(cerr);
+    if(pOptions->statistics && pStatistics != NULL) {
+      pStatistics->flushInformation(cerr);
     }
     abort();
   } else {
@@ -105,8 +105,8 @@ void segv_handler(int sig, siginfo_t* info, void* c) {
   } else if(addr < 10*1024) {
     cerr << "Looks like a NULL pointer was dereferenced." << endl;
   }
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   abort();
 #endif /* CVC4_DEBUG */
@@ -118,8 +118,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   fprintf(stderr, "CVC4 executed an illegal instruction in DEBUG mode.\n");
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested, aborting...\n");
-    if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushStatistics(cerr);
+    if(pOptions->statistics && pStatistics != NULL) {
+      pStatistics->flushInformation(cerr);
     }
     abort();
   } else {
@@ -131,8 +131,8 @@ void ill_handler(int sig, siginfo_t* info, void*) {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 executed an illegal instruction.\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   abort();
 #endif /* CVC4_DEBUG */
@@ -155,8 +155,8 @@ void cvc4unexpected() {
   }
   if(segvNoSpin) {
     fprintf(stderr, "No-spin requested.\n");
-    if(options.statistics && pStatistics != NULL) {
-      pStatistics->flushStatistics(cerr);
+    if(pOptions->statistics && pStatistics != NULL) {
+      pStatistics->flushInformation(cerr);
     }
     set_terminate(default_terminator);
   } else {
@@ -168,8 +168,8 @@ void cvc4unexpected() {
   }
 #else /* CVC4_DEBUG */
   fprintf(stderr, "CVC4 threw an \"unexpected\" exception.\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   set_terminate(default_terminator);
 #endif /* CVC4_DEBUG */
@@ -181,16 +181,16 @@ void cvc4terminate() {
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.  "
           "(Don't do that.)\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   default_terminator();
 #else /* CVC4_DEBUG */
   fprintf(stderr,
           "CVC4 was terminated by the C++ runtime.\n"
           "Perhaps an exception was thrown during stack unwinding.\n");
-  if(options.statistics && pStatistics != NULL) {
-    pStatistics->flushStatistics(cerr);
+  if(pOptions->statistics && pStatistics != NULL) {
+    pStatistics->flushInformation(cerr);
   }
   default_terminator();
 #endif /* CVC4_DEBUG */