Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.

* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line

3 files changed, 39 insertions, 12 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 467b150d3..485a478d8 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -76,14 +76,20 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   if(q != NULL) {
     d_result = res = q->getResult();
   }
-  // dump the model if option is set
-  if( status &&
-      d_options[options::produceModels] &&
-      d_options[options::dumpModels] &&
-      ( res.asSatisfiabilityResult() == Result::SAT ||
-        (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
-    Command* gm = new GetModelCommand();
-    status = doCommandSingleton(gm);
+  // dump the model/proof if option is set
+  if(status) {
+    if( d_options[options::produceModels] &&
+        d_options[options::dumpModels] &&
+        ( res.asSatisfiabilityResult() == Result::SAT ||
+          (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
+      Command* gm = new GetModelCommand();
+      status = doCommandSingleton(gm);
+    } else if( d_options[options::proof] &&
+               d_options[options::dumpProofs] &&
+               res.asSatisfiabilityResult() == Result::UNSAT ) {
+      Command* gp = new GetProofCommand();
+      status = doCommandSingleton(gp);
+    }
   }
   return status;
 }
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 971aa2131..24469c668 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -213,7 +213,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     if(d_lastWinner != 0) delete cmdExported;
     return ret;
   } else if(mode == 1) {               // portfolio
-
     d_seq->addCommand(cmd->clone());
 
     // We currently don't support changing number of threads for each
@@ -327,7 +326,26 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     lemmaSharingCleanup();
 
     delete[] fns;
-    return portfolioReturn.second;
+
+    bool status = portfolioReturn.second;
+
+    // dump the model/proof if option is set
+    if(status) {
+      if( d_options[options::produceModels] &&
+          d_options[options::dumpModels] &&
+          ( d_result.asSatisfiabilityResult() == Result::SAT ||
+            (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) {
+        Command* gm = new GetModelCommand();
+        status = doCommandSingleton(gm);
+      } else if( d_options[options::proof] &&
+                 d_options[options::dumpProofs] &&
+                 d_result.asSatisfiabilityResult() == Result::UNSAT ) {
+        Command* gp = new GetProofCommand();
+        status = doCommandSingleton(gp);
+      }
+    }
+
+    return status;
   } else if(mode == 2) {
     Command* cmdExported = 
       d_lastWinner == 0 ?
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index d1baaa2e9..bf66629dd 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -108,6 +108,10 @@ 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();
@@ -201,8 +205,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
              << "Notice: ...the experimental --incremental-parallel option.\n";
     exprMgr = new ExprManager(opts);
     pExecutor = new CommandExecutor(*exprMgr, opts);
-  }
-  else {
+  } else {
     exprMgr = new ExprManager(threadOpts[0]);
     pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
   }