1 files changed, 71 insertions, 24 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index e03e9058b..43750a504 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -19,6 +19,7 @@
 #include "util/proof.h"
 #include "proof/sat_proof.h"
 #include "proof/cnf_proof.h"
+#include "proof/theory_proof.h"
 #include "util/cvc4_assert.h"
 
 namespace CVC4 {
@@ -29,8 +30,20 @@ ProofManager* ProofManager::proofManager = NULL;
 ProofManager::ProofManager(ProofFormat format):
   d_satProof(NULL),
   d_cnfProof(NULL),
+  d_theoryProof(NULL),
+  d_fullProof(NULL),
   d_format(format)
-{}
+{
+  // FIXME this is until it actually has theory references
+  initTheoryProof(); 
+}
+
+ProofManager::~ProofManager() {
+  delete d_satProof;
+  delete d_cnfProof;
+  delete d_theoryProof;
+  delete d_fullProof; 
+}
 
 ProofManager* ProofManager::currentPM() {
   if (isInitialized) {
@@ -43,8 +56,14 @@ ProofManager* ProofManager::currentPM() {
 }
 
 Proof* ProofManager::getProof() {
-  // for now, this is just the SAT proof
-  return getSatProof();
+  if (currentPM()->d_fullProof != NULL)
+    return currentPM()->d_fullProof;
+  Assert (currentPM()->d_format == LFSC);
+
+  currentPM()->d_fullProof = new LFSCProof((LFSCSatProof*)getSatProof(),
+                                           (LFSCCnfProof*)getCnfProof(),
+                                           (LFSCTheoryProof*)getTheoryProof()); 
+  return currentPM()->d_fullProof;
 }
 
 SatProof* ProofManager::getSatProof() {
@@ -57,37 +76,65 @@ CnfProof* ProofManager::getCnfProof() {
   return currentPM()->d_cnfProof;
 }
 
+TheoryProof* ProofManager::getTheoryProof() {
+  Assert (currentPM()->d_theoryProof);
+  return currentPM()->d_theoryProof;
+}
+
+
 void ProofManager::initSatProof(Minisat::Solver* solver) {
   Assert (currentPM()->d_satProof == NULL);
-  switch(currentPM()->d_format) {
-  case LFSC :
-    currentPM()->d_satProof = new LFSCSatProof(solver);
-    break;
-  case NATIVE :
-    currentPM()->d_satProof = new SatProof(solver);
-    break;
-  default:
-    Assert(false); 
-  }
-  
+  Assert(currentPM()->d_format == LFSC);
+  currentPM()->d_satProof = new LFSCSatProof(solver);
 }
 
 void ProofManager::initCnfProof(prop::CnfStream* cnfStream) {
   Assert (currentPM()->d_cnfProof == NULL);
+  Assert (currentPM()->d_format == LFSC);
+  currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); 
+}
 
-  switch(currentPM()->d_format) {
-  case LFSC :
-    currentPM()->d_cnfProof = new CnfProof(cnfStream); // FIXME
-    break;
-  case NATIVE :
-    currentPM()->d_cnfProof = new CnfProof(cnfStream);
-    break;
-  default:
-    Assert(false); 
-  }
+void ProofManager::initTheoryProof() {
+  Assert (currentPM()->d_theoryProof == NULL);
+  Assert (currentPM()->d_format == LFSC);
+  currentPM()->d_theoryProof = new LFSCTheoryProof();
+}
 
+LFSCProof::LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
+  : d_satProof(sat)
+  , d_cnfProof(cnf)
+  , d_theoryProof(theory)
+{
+  // link the proofs
+  d_satProof->setCnfProof(d_cnfProof);
+  d_cnfProof->setTheoryProof(d_theoryProof);
+  // build the resolution proof out of the traces
+  // this sets up the other proofs with the necessary information
+  d_satProof->constructProof();
 }
 
+void LFSCProof::toStream(std::ostream& out) {
+  std::ostringstream paren;
+  out << "(check \n";
+  d_theoryProof->printDeclarations(out, paren);
+  out << "(: (holds cln) \n";
+  d_cnfProof->printAtomMapping(out, paren);
+  d_cnfProof->printClauses(out, paren);
+  d_satProof->printResolutions(out, paren); 
+  paren <<"))";
+  out << paren.str(); 
+}
+
+// void ProofManager::declareAtom(Expr atom, SatLiteral lit) {
+//   ::Minisat::Lit mlit = toMinisatLit(lit); 
+//   d_satProof->addLiteral(mlit);
+//   d_cnfProof->declareAtom(atom, mlit); 
+// }
+
+// void ProofManager::addInputClause(SatClause clause) {
+//   d_satProof->registerClause(clause, true); 
+//   d_cnfProof->registerClause(clause, true); 
+// }
 
 
 } /* CVC4  namespace */