diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-15 15:54:04 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-15 16:37:43 -0500 |
commit | a4d92de5f34bffcad05a6de04c52478f93029e26 (patch) | |
tree | c670d02103e7f6efdb04dfb04cb122e9b427ca78 /src/main/driver_unified.cpp | |
parent | 814526633b07146d4f0f9e6d24583bd6e645d8cd (diff) |
make incremental+portfolio experimental
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r-- | src/main/driver_unified.cpp | 22 |
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; |