From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Sun, 11 Oct 2015 23:20:16 +0000 (-0400)
Subject: fix regression tests, support fallback mode for proofs
X-Git-Tag: cvc5-1.0.0~6210^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c79677bdfc6342d4f669b7343a35511334503fdb;p=cvc5.git

fix regression tests, support fallback mode for proofs
---

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