Merge pull request #5 from kbansal/1.0.x

make incremental+portfolio experimental

1 files changed, 14 insertions, 8 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index c27179ee5..624573391 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -26,6 +26,7 @@
 #include "cvc4autoconfig.h"
 #include "main/main.h"
 #include "main/interactive_shell.h"
+#include "main/options.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
@@ -187,17 +188,22 @@ int runCvc4(int argc, char* argv[], Options& opts) {
   DumpChannel.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
 
   // Create the expression manager using appropriate options
+  ExprManager* exprMgr;
 # ifndef PORTFOLIO_BUILD
-  ExprManager* exprMgr = new ExprManager(opts);
-# else
-  vector<Options> threadOpts = parseThreadSpecificOptions(opts);
-  ExprManager* exprMgr = new ExprManager(threadOpts[0]);
-# endif
-
-# ifndef PORTFOLIO_BUILD
+  exprMgr = new ExprManager(opts);
   pExecutor = new CommandExecutor(*exprMgr, opts);
 # else
-  pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
+  vector<Options> threadOpts = parseThreadSpecificOptions(opts);
+  if(opts[options::incrementalSolving] && !opts[options::incrementalParallel]) {
+    Warning() << "WARNING: In --incremental mode, using the sequential solver unless forced by...\n"
+              << "WARNING: ...the experimental --incremental-parallel option.\n";
+    exprMgr = new ExprManager(opts);
+    pExecutor = new CommandExecutor(*exprMgr, opts);
+  }
+  else {
+    exprMgr = new ExprManager(threadOpts[0]);
+    pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
+  }
 # endif
 
   Parser* replayParser = NULL;