make incremental+portfolio experimental

2 files changed, 16 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;
diff --git a/src/main/options b/src/main/options
index 53c04a2c4..caea63f5a 100644
--- a/src/main/options
+++ b/src/main/options
@@ -37,6 +37,8 @@ option sharingFilterByLength --filter-lemma-length=N int :default -1 :read-write
  don't share (among portfolio threads) lemmas strictly longer than N
 option fallbackSequential  --fallback-sequential bool :default false
  Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode
+option incrementalParallel --incremental-parallel bool :default false :link --incremental
+ Use parallel solver even in incremental mode (may print 'unknown's at times)
 
 expert-option waitToJoin --wait-to-join bool :default true
  wait for other threads to join before quitting