Merge pull request #76 from CVC4/proofs

Proofs

3 files changed, 25 insertions, 11 deletions

diff --git a/configure.ac b/configure.ac
index 8f17768f3..ac68a8edd 100644
--- a/configure.ac
+++ b/configure.ac
@@ -443,7 +443,7 @@ case "$with_build" in
     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
     if test -z "${enable_replay+set}"       ; then enable_replay=no                 ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=no             ; fi
-    if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
+    if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=no                ; fi
     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
@@ -459,7 +459,7 @@ case "$with_build" in
     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
-    if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
+    if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
@@ -476,7 +476,7 @@ case "$with_build" in
     if test -z "${enable_statistics+set}"   ; then enable_statistics=yes            ; fi
     if test -z "${enable_replay+set}"       ; then enable_replay=yes                ; fi
     if test -z "${enable_assertions+set}"   ; then enable_assertions=yes            ; fi
-    if test -z "${enable_proof+set}"        ; then enable_proof=no                  ; fi
+    if test -z "${enable_proof+set}"        ; then enable_proof=yes                 ; fi
     if test -z "${enable_tracing+set}"      ; then enable_tracing=yes               ; fi
     if test -z "${enable_dumping+set}"      ; then enable_dumping=yes               ; fi
     if test -z "${enable_muzzle+set}"       ; then enable_muzzle=no                 ; fi
@@ -542,7 +542,7 @@ AC_ARG_ENABLE([proof],
   [AS_HELP_STRING([--enable-proof],
      [support proof generation])])
 if test -z "${enable_proof+set}"; then
-  enable_proof=no
+  enable_proof=yes
 fi
 AC_MSG_RESULT([$enable_proof])
 
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