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

5 files changed, 102 insertions, 17 deletions

diff --git a/src/smt/options b/src/smt/options
index 69b5102de..b76822caf 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -22,14 +22,16 @@ option expandDefinitions expand-definitions bool :default false
  always expand symbol definitions in output
 common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  support the get-value and get-model commands
-option checkProofs check-proofs --check-proofs bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- after UNSAT/VALID, machine-check the generated proof
-option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
-option dumpModels --dump-models bool :default false
+option dumpModels --dump-models bool :default false :link --produce-models
  output models after every SAT/INVALID/UNKNOWN response
 option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on proof generation
+option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ after UNSAT/VALID, machine-check the generated proof
+option dumpProofs --dump-proofs bool :default false :link --proof
+ output proofs after every UNSAT/VALID response
 # this is just a placeholder for later; it doesn't show up in command-line options listings
 undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on unsat core generation (NOT YET SUPPORTED)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1f83bb547..ec37eaf26 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -46,8 +46,10 @@
 #include "theory/theory_engine.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "proof/proof_manager.h"
+#include "main/options.h"
 #include "util/proof.h"
 #include "proof/proof.h"
+#include "proof/proof_manager.h"
 #include "util/boolean_simplification.h"
 #include "util/node_visitor.h"
 #include "util/configuration.h"
@@ -157,6 +159,8 @@ struct SmtEngineStatistics {
   IntStat d_numAssertionsPost;
   /** time spent in checkModel() */
   TimerStat d_checkModelTime;
+  /** time spent in checkProof() */
+  TimerStat d_checkProofTime;
   /** time spent in PropEngine::checkSat() */
   TimerStat d_solveTime;
   /** time spent in pushing/popping */
@@ -183,11 +187,11 @@ struct SmtEngineStatistics {
     d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
     d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
     d_checkModelTime("smt::SmtEngine::checkModelTime"),
+    d_checkProofTime("smt::SmtEngine::checkProofTime"),
     d_solveTime("smt::SmtEngine::solveTime"),
     d_pushPopTime("smt::SmtEngine::pushPopTime"),
     d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
     d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
-
  {
 
     StatisticsRegistry::registerStat(&d_definitionExpansionTime);
@@ -667,6 +671,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_decisionEngine(NULL),
   d_theoryEngine(NULL),
   d_propEngine(NULL),
+  d_proofManager(NULL),
   d_definedFunctions(NULL),
   d_assertionList(NULL),
   d_assignments(NULL),
@@ -696,6 +701,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_statisticsRegistry = new StatisticsRegistry();
   d_stats = new SmtEngineStatistics();
 
+  PROOF( d_proofManager = new ProofManager(); );
+
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
   d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic));
@@ -763,6 +770,7 @@ void SmtEngine::finishInit() {
   if(options::cumulativeMillisecondLimit() != 0) {
     setTimeLimit(options::cumulativeMillisecondLimit(), true);
   }
+
   PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); 
 }
 
@@ -777,16 +785,11 @@ void SmtEngine::finalOptionsAreSet() {
   }
 
   if(options::checkModels()) {
-    if(! options::produceModels()) {
-      Notice() << "SmtEngine: turning on produce-models to support check-model" << endl;
-      setOption("produce-models", SExpr("true"));
-    }
     if(! options::interactive()) {
-      Notice() << "SmtEngine: turning on interactive-mode to support check-model" << endl;
+      Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl;
       setOption("interactive-mode", SExpr("true"));
     }
   }
-
   if(options::produceAssignments() && !options::produceModels()) {
     Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl;
     setOption("produce-models", SExpr("true"));
@@ -3291,9 +3294,6 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   finalOptionsAreSet();
   doPendingPops();
 
-
-  PROOF( ProofManager::currentPM()->addAssertion(ex); ); 
-
   Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl;
 
   if(d_queryMade && !options::incrementalSolving()) {
@@ -3308,6 +3308,8 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
     e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
     // Ensure expr is type-checked at this point.
     ensureBoolean(e);
+    // Give it to proof manager
+    PROOF( ProofManager::currentPM()->addAssertion(e); ); 
   }
 
   // check to see if a postsolve() is pending
@@ -3361,6 +3363,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   // Check that UNSAT results generate a proof correctly.
   if(options::checkProofs()) {
     if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+      TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
       checkProof();
     }
   }
@@ -3384,9 +3387,10 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
 
   // Substitute out any abstract values in ex
   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
-
   // Ensure that the expression is type-checked at this point, and Boolean
   ensureBoolean(e);
+  // Give it to proof manager
+  PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); ); 
 
   // check to see if a postsolve() is pending
   if(d_needPostsolve) {
@@ -3437,6 +3441,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
   // Check that UNSAT results generate a proof correctly.
   if(options::checkProofs()) {
     if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+      TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
       checkProof();
     }
   }
@@ -3449,7 +3454,9 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
-  PROOF( ProofManager::currentPM()->addAssertion(ex);); 
+
+  PROOF( ProofManager::currentPM()->addAssertion(ex); ); 
+
   Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
 
   // Substitute out any abstract values in ex
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0781ac1c0..8e400468c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -56,6 +56,8 @@ class SmtEngine;
 class DecisionEngine;
 class TheoryEngine;
 
+class ProofManager;
+
 class Model;
 class StatisticsRegistry;
 
@@ -83,6 +85,7 @@ namespace smt {
   class BooleanTermConverter;
 
   void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
+  ProofManager* currentProofManager();
 
   struct CommandCleanup;
   typedef context::CDList<Command*, CommandCleanup> CommandList;
@@ -135,8 +138,11 @@ class CVC4_PUBLIC SmtEngine {
   TheoryEngine* d_theoryEngine;
   /** The propositional engine */
   prop::PropEngine* d_propEngine;
+  /** The proof manager */
+  ProofManager* d_proofManager;
   /** An index of our defined functions */
   DefinedFunctionMap* d_definedFunctions;
+
   /**
    * The assertion list (before any conversion) for supporting
    * getAssertions().  Only maintained if in interactive mode.
@@ -327,6 +333,7 @@ class CVC4_PUBLIC SmtEngine {
   friend class ::CVC4::smt::BooleanTermConverter;
   friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*);
   friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
+  friend ProofManager* ::CVC4::smt::currentProofManager();
   // to access d_modelCommands
   friend class ::CVC4::Model;
   friend class ::CVC4::theory::TheoryModel;
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index e4de1029b..a731ff024 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -16,16 +16,75 @@
  **/
 
 #include "smt/smt_engine.h"
+#include "util/statistics_registry.h"
 #include "check.h"
 
+#include <cstdlib>
+#include <cstring>
+#include <fstream>
+#include <string>
+#include <unistd.h>
+
 using namespace CVC4;
 using namespace std;
 
+namespace CVC4 {
+
+namespace proof {
+  extern const char *const plf_signatures;
+}/* CVC4::proof namespace */
+
+namespace smt {
+
+class UnlinkProofFile {
+  string d_filename;
+public:
+  UnlinkProofFile(const char* filename) : d_filename(filename) {}
+  ~UnlinkProofFile() { unlink(d_filename.c_str()); }
+};/* class UnlinkProofFile */
+
+}/* CVC4::smt namespace */
+
+}/* CVC4 namespace */
+
 void SmtEngine::checkProof() {
 
 #ifdef CVC4_PROOF
 
-  //TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
+  Chat() << "generating proof..." << endl;
+
+  Proof* pf = getProof();
+
+  Chat() << "checking proof..." << endl;
+
+  if(!d_logic.isPure(theory::THEORY_BOOL) &&
+     !d_logic.isPure(theory::THEORY_UF)) {
+    // no checking for these yet
+    Notice() << "Notice: no proof-checking for non-UF proofs yet" << endl;
+    return;
+  }
+
+  char* pfFile = strdup("/tmp/cvc4_proof.XXXXXX");
+  int fd = mkstemp(pfFile);
+
+  // ensure this temp file is removed after
+  smt::UnlinkProofFile unlinker(pfFile);
+
+  ofstream pfStream(pfFile);
+  pfStream << proof::plf_signatures << endl;
+  pf->toStream(pfStream);
+  pfStream.close();
+  args a;
+  a.show_runs = false;
+  a.no_tail_calls = false;
+  a.compile_scc = false;
+  a.compile_scc_debug = false;
+  a.run_scc = false;
+  a.use_nested_app = false;
+  a.compile_lib = false;
+  init();
+  check_file(pfFile, args());
+  close(fd);
 
 #else /* CVC4_PROOF */
 
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 21644d3f4..2389181b5 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -22,10 +22,14 @@
 #include "util/cvc4_assert.h"
 #include "expr/node_manager.h"
 #include "util/output.h"
+#include "proof/proof.h"
 
 #pragma once
 
 namespace CVC4 {
+
+class ProofManager;
+
 namespace smt {
 
 extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
@@ -35,6 +39,12 @@ inline SmtEngine* currentSmtEngine() {
   return s_smtEngine_current;
 }
 
+inline ProofManager* currentProofManager() {
+  Assert(PROOF_ON());
+  Assert(s_smtEngine_current != NULL);
+  return s_smtEngine_current->d_proofManager;
+}
+
 class SmtScope : public NodeManagerScope {
   /** The old NodeManager, to be restored on destruction. */
   SmtEngine* d_oldSmtEngine;