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

1 files changed, 11 insertions, 0 deletions

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;