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.

1 files changed, 104 insertions, 0 deletions

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 */