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:42:51 -0500 |
commit | 8f93182e0f8c19d741aa2a5eda02c8fef12a04a2 (patch) | |
tree | 88cfa55c944d5b984c21a36c31e1d53ea78c0c85 /src/main | |
parent | 460ee6b1b8f8f2fd93f65d94cb8f614dd406c758 (diff) |
make incremental+portfolio experimental
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/driver_unified.cpp | 22 | ||||
-rw-r--r-- | src/main/options | 2 |
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 |