Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, SmtEngine::getProof(), a few other things..

2 files changed, 40 insertions, 4 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 96ee5b59b..7ea22ce8f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -34,6 +34,8 @@
 #include "smt/no_such_function_exception.h"
 #include "smt/smt_engine.h"
 #include "theory/theory_engine.h"
+#include "proof/proof_manager.h"
+#include "util/proof.h"
 #include "util/boolean_simplification.h"
 #include "util/configuration.h"
 #include "util/exception.h"
@@ -987,7 +989,7 @@ Expr SmtEngine::getValue(const Expr& e)
      d_status.asSatisfiabilityResult() != Result::SAT ||
      d_problemExtended) {
     const char* msg =
-      "Cannot get value unless immediately proceded by SAT/INVALID response.";
+      "Cannot get value unless immediately preceded by SAT/INVALID response.";
     throw ModalException(msg);
   }
   if(type.isFunction() || type.isPredicate() ||
@@ -1040,6 +1042,7 @@ bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
 
 SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   Trace("smt") << "SMT getAssignment()" << endl;
+  NodeManagerScope nms(d_nodeManager);
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssignmentCommand() << endl;
   }
@@ -1053,7 +1056,8 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
      d_status.asSatisfiabilityResult() != Result::SAT ||
      d_problemExtended) {
     const char* msg =
-      "Cannot get value unless immediately proceded by SAT/INVALID response.";
+      "Cannot get the current assignment unless immediately "
+      "preceded by SAT/INVALID response.";
     throw ModalException(msg);
   }
 
@@ -1061,7 +1065,6 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
     return SExpr();
   }
 
-  NodeManagerScope nms(d_nodeManager);
   vector<SExpr> sexprs;
   TypeNode boolType = d_nodeManager->booleanType();
   for(AssignmentSet::const_iterator i = d_assignments->begin(),
@@ -1093,6 +1096,32 @@ SExpr SmtEngine::getAssignment() throw(ModalException, AssertionException) {
   return SExpr(sexprs);
 }
 
+Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
+  Trace("smt") << "SMT getProof()" << endl;
+  NodeManagerScope nms(d_nodeManager);
+  if(Dump.isOn("benchmark")) {
+    Dump("benchmark") << GetProofCommand() << endl;
+  }
+#ifdef CVC4_PROOF
+  if(!Options::current()->proof) {
+    const char* msg =
+      "Cannot get a proof when produce-proofs option is off.";
+    throw ModalException(msg);
+  }
+  if(d_status.isNull() ||
+     d_status.asSatisfiabilityResult() != Result::UNSAT ||
+     d_problemExtended) {
+    const char* msg =
+      "Cannot get a proof unless immediately preceded by UNSAT/VALID response.";
+    throw ModalException(msg);
+  }
+
+  return ProofManager::getProof();
+#else /* CVC4_PROOF */
+  throw ModalException("This build of CVC4 doesn't have proof support.");
+#endif /* CVC4_PROOF */
+}
+
 vector<Expr> SmtEngine::getAssertions()
   throw(ModalException, AssertionException) {
   if(Dump.isOn("benchmark")) {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 5d8f31d3c..90593569b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -28,6 +28,7 @@
 #include "context/cdset_forward.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
+#include "util/proof.h"
 #include "smt/bad_option_exception.h"
 #include "smt/modal_exception.h"
 #include "smt/no_such_function_exception.h"
@@ -36,7 +37,6 @@
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/stats.h"
-#include "proof/proof_manager.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -319,6 +319,13 @@ public:
   SExpr getAssignment() throw(ModalException, AssertionException);
 
   /**
+   * Get the last proof (only if immediately preceded by an UNSAT
+   * or VALID query).  Only permitted if CVC4 was built with proof
+   * support and produce-proofs is on.
+   */
+  Proof* getProof() throw(ModalException, AssertionException);
+
+  /**
    * Get the current set of assertions.  Only permitted if the
    * SmtEngine is set to operate interactively.
    */