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

5 files changed, 25 insertions, 19 deletions

diff --git a/src/proof/proof.h b/src/proof/proof.h
index 3e5b54cc7..a3270c4c0 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -16,8 +16,8 @@
  ** Proof manager
  **/
 
-#ifndef __CVC4__PROOF_H
-#define __CVC4__PROOF_H
+#ifndef __CVC4__PROOF__PROOF_H
+#define __CVC4__PROOF__PROOF_H
 
 #include "util/options.h"
 
@@ -33,4 +33,4 @@
 
 
 
-#endif /* __CVC4__PROOF_H */
+#endif /* __CVC4__PROOF__PROOF_H */
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 2d7432cbc..4191d1046 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -18,6 +18,7 @@
  **/
 
 #include "proof/proof_manager.h"
+#include "util/proof.h"
 #include "proof/sat_proof.h"
 #include "proof/cnf_proof.h"
 #include "util/Assert.h"
@@ -40,7 +41,12 @@ ProofManager* ProofManager::currentPM() {
     proofManager = new ProofManager();
     isInitialized = true; 
     return proofManager; 
-    }
+  }
+}
+
+Proof* ProofManager::getProof() {
+  // for now, this is just the SAT proof
+  return getSatProof();
 }
 
 SatProof* ProofManager::getSatProof() {
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index c79d26fed..e23fbd600 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -22,7 +22,7 @@
 #define __CVC4__PROOF_MANAGER_H
 
 #include <iostream> 
-#include "proof.h"
+#include "proof/proof.h"
 
 // forward declarations
 namespace Minisat {
@@ -33,6 +33,7 @@ namespace CVC4 {
 namespace prop {
 class CnfStream;
 }
+class Proof;
 class SatProof;
 class CnfProof;
 
@@ -56,6 +57,7 @@ public:
   static void      initSatProof(Minisat::Solver* solver); 
   static void      initCnfProof(CVC4::prop::CnfStream* cnfStream);
 
+  static Proof* getProof();
   static SatProof* getSatProof();
   static CnfProof* getCnfProof();
 
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 57bb96513..37a3a9706 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -524,8 +524,9 @@ ClauseId SatProof::resolveUnit(Lit lit) {
   return unit_id; 
 }
 
-void SatProof::printProof() {
+void SatProof::toStream(std::ostream& out) {
   Debug("proof:sat") << "SatProof::printProof\n";
+  Unimplemented("native proof printing not supported yet");
 }
 
 void SatProof::finalizeProof(CRef conflict_ref) {
@@ -543,7 +544,6 @@ void SatProof::finalizeProof(CRef conflict_ref) {
     res->addStep(lit, res_id, !sign(lit)); 
   }
   registerResolution(d_emptyClauseId, res);
-  printProof(); 
 }
 
 /// CRef manager
@@ -693,8 +693,7 @@ void LFSCSatProof::printVariables() {
 }
 
 
-void LFSCSatProof::flush() {
-  ostringstream out;
+void LFSCSatProof::flush(std::ostream& out) {
   out << "(check \n";
   d_paren <<")"; 
   out << d_varSS.str();
@@ -703,11 +702,10 @@ void LFSCSatProof::flush() {
   out << d_lemmaSS.str(); 
   d_paren << "))";
   out << d_paren.str();
-  out << ";"; //to comment out the solver's answer 
-  std::cout << out.str(); 
+  out << "\n";
 }
 
-void LFSCSatProof::printProof() {
+void LFSCSatProof::toStream(std::ostream& out) {
   Debug("proof:sat") << " LFSCSatProof::printProof \n";
 
   // first collect lemmas to print in reverse order
@@ -722,8 +720,7 @@ void LFSCSatProof::printProof() {
 
   printClauses();
   printVariables();
-  flush();
-  
+  flush(out);
 }
 
 } /* CVC4 namespace */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 4641ea4cc..051266df8 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -32,6 +32,7 @@ typedef uint32_t CRef;
 }
 
 #include "prop/minisat/core/SolverTypes.h"
+#include "util/proof.h"
 
 namespace std {
 using namespace __gnu_cxx;
@@ -99,7 +100,7 @@ public:
   void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
 };
 
-class SatProof {
+class SatProof : public Proof {
 protected:
   ::Minisat::Solver*    d_solver;
   // clauses 
@@ -144,8 +145,8 @@ protected:
   ::Minisat::Lit  getUnit(ClauseId id);
   ClauseId      getUnitId(::Minisat::Lit lit); 
   ::Minisat::Clause& getClause(ClauseId id);
-  virtual void printProof();
-  
+  virtual void toStream(std::ostream& out);
+
   bool checkResolution(ClauseId id);
   /** 
    * Constructs a resolution tree that proves lit
@@ -237,7 +238,7 @@ private:
 
   void printVariables();
   void printClauses();
-  void flush();
+  void flush(std::ostream& out);
   
 public:
   LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false):
@@ -249,7 +250,7 @@ public:
     d_seenLemmas(),
     d_seenInput()
   {} 
-  void printProof();  
+  virtual void toStream(std::ostream& out);  
 };
 
 }