diff options
| -rw-r--r-- | src/main/driver_unified.cpp | 26 | ||||
| -rwxr-xr-x | test/regress/run_regression | 2 |
2 files changed, 21 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 diff --git a/test/regress/run_regression b/test/regress/run_regression index b6fb735fe..9204fe33c 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -239,6 +239,7 @@ if [ "$proof" = yes ]; then ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null && ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null && ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null && + ! expr "$BINARY" : '.*pcvc4' &>/dev/null && ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then # later on, we'll run another test with --check-proofs on check_proofs=true @@ -248,6 +249,7 @@ if [ "$proof" = yes ]; then ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null && ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null && ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null && + ! expr "$BINARY" : '.*pcvc4' &>/dev/null && ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then # later on, we'll run another test with --check-unsat-cores on check_unsat_cores=true |