First attempt at incorporating LFSC proof checker into CVC4.

4 files changed, 55 insertions, 0 deletions

diff --git a/src/smt/options b/src/smt/options
index 05a138f60..69b5102de 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -22,6 +22,8 @@ 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"
  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
 option dumpModels --dump-models bool :default false
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0fadca424..1f83bb547 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3358,6 +3358,12 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
       checkModel(/* hard failure iff */ ! r.isUnknown());
     }
   }
+  // Check that UNSAT results generate a proof correctly.
+  if(options::checkProofs()) {
+    if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+      checkProof();
+    }
+  }
 
   return r;
 }/* SmtEngine::checkSat() */
@@ -3428,6 +3434,12 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
       checkModel(/* hard failure iff */ ! r.isUnknown());
     }
   }
+  // Check that UNSAT results generate a proof correctly.
+  if(options::checkProofs()) {
+    if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+      checkProof();
+    }
+  }
 
   return r;
 }/* SmtEngine::query() */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 9655297b3..0781ac1c0 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -249,6 +249,11 @@ class CVC4_PUBLIC SmtEngine {
   smt::SmtEnginePrivate* d_private;
 
   /**
+   * Check that a generated Proof (via getProof()) checks.
+   */
+  void checkProof();
+
+  /**
    * Check that a generated Model (via getModel()) actually satisfies
    * all user assertions.
    */
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
new file mode 100644
index 000000000..e4de1029b
--- /dev/null
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -0,0 +1,36 @@
+/*********************                                                        */
+/*! \file smt_engine_check_proof.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "smt/smt_engine.h"
+#include "check.h"
+
+using namespace CVC4;
+using namespace std;
+
+void SmtEngine::checkProof() {
+
+#ifdef CVC4_PROOF
+
+  //TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
+
+#else /* CVC4_PROOF */
+
+  Unreachable("This version of CVC4 was built without proof support; cannot check proofs.");
+
+#endif /* CVC4_PROOF */
+
+}