From 02f4f0500849bc719cb45bbc771bea90eb6e96f8 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Sat, 29 Oct 2011 05:21:49 +0000
Subject: Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command,
 SmtEngine::getProof(), a few other things..

---
 src/expr/command.cpp | 17 +++++++++++++++++
 src/expr/command.h   | 11 +++++++++++
 2 files changed, 28 insertions(+)

(limited to 'src/expr')

diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 61702561a..345d7f956 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -423,6 +423,23 @@ void GetAssignmentCommand::printResult(std::ostream& out) const {
   out << d_result << endl;
 }
 
+/* class GetProofCommand */
+
+GetProofCommand::GetProofCommand() {
+}
+
+void GetProofCommand::invoke(SmtEngine* smtEngine) {
+  d_result = smtEngine->getProof();
+}
+
+Proof* GetProofCommand::getResult() const {
+  return d_result;
+}
+
+void GetProofCommand::printResult(std::ostream& out) const {
+  d_result->toStream(out);
+}
+
 /* class GetAssertionsCommand */
 
 GetAssertionsCommand::GetAssertionsCommand() {
diff --git a/src/expr/command.h b/src/expr/command.h
index 5cf4f6fa0..b686025fe 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -35,6 +35,7 @@
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/datatype.h"
+#include "util/proof.h"
 
 namespace CVC4 {
 
@@ -232,6 +233,16 @@ public:
   void printResult(std::ostream& out) const;
 };/* class GetAssignmentCommand */
 
+class CVC4_PUBLIC GetProofCommand : public Command {
+protected:
+  Proof* d_result;
+public:
+  GetProofCommand();
+  void invoke(SmtEngine* smtEngine);
+  Proof* getResult() const;
+  void printResult(std::ostream& out) const;
+};/* class GetProofCommand */
+
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
 protected:
   std::string d_result;
-- 
cgit v1.2.3