diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-10-11 19:20:16 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-10-11 19:20:16 -0400 |
commit | c79677bdfc6342d4f669b7343a35511334503fdb (patch) | |
tree | 0ae71f14d13493844dad858f393c9ab870536c45 /src | |
parent | 4fd18dee3156a6dd1903b95662034d6e996ff88b (diff) |
fix regression tests, support fallback mode for proofs
Diffstat (limited to 'src')
-rw-r--r-- | src/main/driver_unified.cpp | 26 |
1 files changed, 19 insertions, 7 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index b9e951f7b..7bc711910 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -139,10 +139,6 @@ int runCvc4(int argc, char* argv[], Options& opts) { ! opts[options::threadArgv].empty() ) { throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'."); } -# else - if( opts[options::checkProofs] ) { - throw OptionException("Cannot run portfolio in check-proofs mode."); - } # endif progName = opts[options::binary_name].c_str(); @@ -242,16 +238,32 @@ int runCvc4(int argc, char* argv[], Options& opts) { pExecutor = new CommandExecutor(*exprMgr, opts); # else vector<Options> threadOpts = parseThreadSpecificOptions(opts); + bool useParallelExecutor = true; + // incremental? if(opts.wasSetByUser(options::incrementalSolving) && opts[options::incrementalSolving] && !opts[options::incrementalParallel]) { Notice() << "Notice: In --incremental mode, using the sequential solver unless forced by...\n" << "Notice: ...the experimental --incremental-parallel option.\n"; - exprMgr = new ExprManager(opts); - pExecutor = new CommandExecutor(*exprMgr, opts); - } else { + useParallelExecutor = false; + } + // proofs? + if(opts[options::checkProofs]) { + if(opts[options::fallbackSequential]) { + Warning() << "Warning: Falling back to sequential mode, as cannot run portfolio in check-proofs mode.\n"; + useParallelExecutor = false; + } + else { + throw OptionException("Cannot run portfolio in check-proofs mode."); + } + } + // pick appropriate one + if(useParallelExecutor) { exprMgr = new ExprManager(threadOpts[0]); pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts); + } else { + exprMgr = new ExprManager(opts); + pExecutor = new CommandExecutor(*exprMgr, opts); } # endif |