From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 8 Oct 2013 02:49:45 +0000 (-0400)
Subject: first draft implementation of uf proofs with holes
X-Git-Tag: cvc5-1.0.0~7285
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=867e79e0823c689889224078dfaebec03aee9730;p=cvc5.git

first draft implementation of uf proofs with holes
---

diff --git a/src/proof/Makefile.am b/src/proof/Makefile.am
index 75588ceb8..e996ddb60 100644
--- a/src/proof/Makefile.am
+++ b/src/proof/Makefile.am
@@ -13,6 +13,8 @@ libproof_la_SOURCES = \
 	sat_proof.cpp \
 	cnf_proof.h \
 	cnf_proof.cpp \
+	theory_proof.h \
+	theory_proof.cpp \
 	proof_manager.h \
 	proof_manager.cpp
 
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 5f03ef5cf..caafa6b83 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -16,11 +16,110 @@
  **/
 
 #include "proof/cnf_proof.h"
+#include "proof/theory_proof.h"
+#include "proof/proof_manager.h"
+#include "prop/sat_solver_types.h"
+#include "prop/minisat/minisat.h"
+#include "prop/cnf_stream.h"
+
 using namespace CVC4::prop;
 
 namespace CVC4 {
 
-CnfProof::CnfProof(CnfStream* stream) :
-  d_cnfStream(stream) {}
+CnfProof::CnfProof(CnfStream* stream)
+  : d_cnfStream(stream)
+  , d_theoryProof(NULL)
+{}
+
+TheoryProof* CnfProof::getTheoryProof() {
+  Assert (d_theoryProof);
+  return d_theoryProof; 
+}
+
+void CnfProof::setTheoryProof(TheoryProof* theory_proof) {
+  Assert (d_theoryProof == NULL);
+  d_theoryProof = theory_proof; 
+}
+
+void CnfProof::addInputClause(ClauseId id, const ::Minisat::Clause& clause) {
+  d_inputClauses.insert(std::make_pair(id, clause)); 
+}
+
+void CnfProof::addTheoryLemma(ClauseId id, const ::Minisat::Clause& clause) {
+  d_theoryLemmas.insert(std::make_pair(id, clause)); 
+}
+
+void CnfProof::addVariable(unsigned var) {
+  d_propVars.insert(var); 
+  Expr atom = getAtom(var);
+  getTheoryProof()->addAtom(atom); 
+}
+
+Expr CnfProof::getAtom(unsigned var) {
+  Minisat::Lit m_lit = Minisat::mkLit(var); 
+  prop::SatLiteral sat_lit = prop::MinisatSatSolver::toSatLiteral(m_lit); 
+  Expr atom = d_cnfStream->getNode(sat_lit).toExpr();
+  return atom; 
+}
+
+void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
+  for (VarSet::iterator it = d_propVars.begin();it != d_propVars.end();  ++it) {
+    Expr atom = getAtom(*it);
+    os << "(decl_atom ";
+    getTheoryProof()->printFormula(atom, os);
+    os << " (\\ " << ProofManager::getVarPrefix() <<*it << " (\\ " << ProofManager::getAtomPrefix() <<*it << "\n";
+    paren << ")))"; 
+  }
+}
+
+void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
+  printInputClauses(os, paren); 
+  printTheoryLemmas(os, paren);
+}
+
+void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
+  for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
+    ClauseId id = it->first;
+    const Minisat::Clause& clause = it->second;
+    os << " ;; input clause \n";  
+    os << "(satlem _ _ ";
+    std::ostringstream clause_paren; 
+    printClause(clause, os, clause_paren);
+    os << " (clausify_false trust)" << clause_paren.str();
+    os << "( \\ " << ProofManager::getInputClausePrefix() << id <<"\n"; 
+    paren << "))"; 
+  }
+}
+
+
+void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
+  for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
+    ClauseId id = it->first;
+    const Minisat::Clause& clause = it->second;
+    os << " ;; theory lemma \n";  
+    os << "(satlem _ _ ";
+    std::ostringstream clause_paren; 
+    printClause(clause, os, clause_paren);
+    os << " (clausify_false trust)" << clause_paren.str();
+    os << "( \\ " << ProofManager::getLemmaClausePrefix() << id <<"\n"; 
+    paren << "))"; 
+  }
+}
+
+void LFSCCnfProof::printClause(const Minisat::Clause& clause, std::ostream& os, std::ostream& paren) {
+  for (int i = 0; i < clause.size(); ++i) {
+    Minisat::Lit lit = clause[i];
+    unsigned var = Minisat::var(lit);
+    if (sign(lit)) {
+      os << "(asf _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " ";
+      paren << ")"; 
+    } else {
+      os << "(ast _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " ";
+      paren << ")"; 
+    }
+  }
+}
+
 
 } /* CVC4 namespace */
+
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 984dc76c6..8acb7a50f 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -16,20 +16,58 @@
  ** 
  **/
 
-#include "cvc4_private.h"
-#include "util/proof.h"
 #ifndef __CVC4__CNF_PROOF_H
 #define __CVC4__CNF_PROOF_H
 
+#include "cvc4_private.h"
+#include "util/proof.h"
+#include "proof/sat_proof.h"
+
+#include <ext/hash_set>
+#include <ext/hash_map>
 #include <iostream> 
+
 namespace CVC4 {
 namespace prop {
 class CnfStream;
 }
+
+typedef __gnu_cxx::hash_map < ClauseId, ::Minisat::Clause > IdToClause; 
+typedef __gnu_cxx::hash_set<unsigned > VarSet;
+
+class TheoryProof; 
+  
 class CnfProof {
+protected:
   CVC4::prop::CnfStream* d_cnfStream;
+  IdToClause d_inputClauses;
+  IdToClause d_theoryLemmas;
+  VarSet     d_propVars;
+  TheoryProof* d_theoryProof;
+  TheoryProof* getTheoryProof();
+
+  Expr getAtom(unsigned var);
 public:
   CnfProof(CVC4::prop::CnfStream* cnfStream);
+  void addInputClause(ClauseId id, const ::Minisat::Clause& clause);
+  void addTheoryLemma(ClauseId id, const ::Minisat::Clause& clause);
+  void addVariable(unsigned var); 
+  void setTheoryProof(TheoryProof* theory_proof);
+  virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0;
+  virtual void printClauses(std::ostream& os, std::ostream& paren) = 0;
+
+};
+
+class LFSCCnfProof: public CnfProof {
+  void printInputClauses(std::ostream& os, std::ostream& paren);
+  void printTheoryLemmas(std::ostream& os, std::ostream& paren);
+  void printClause(const Minisat::Clause& clause, std::ostream& os, std::ostream& paren);
+public:
+  LFSCCnfProof(CVC4::prop::CnfStream* cnfStream)
+    : CnfProof(cnfStream)
+  {}
+  virtual void printAtomMapping(std::ostream& os, std::ostream& paren);
+  virtual void printClauses(std::ostream& os, std::ostream& paren);
 };
 
 } /* CVC4 namespace */
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 */ 
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index efd39a118..4ae8a6dae 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -23,6 +23,7 @@
 
 #include <iostream> 
 #include "proof/proof.h"
+#include "util/proof.h"
 
 // forward declarations
 namespace Minisat {
@@ -38,7 +39,12 @@ namespace prop {
 class Proof;
 class SatProof;
 class CnfProof;
+class TheoryProof;
 
+class LFSCSatProof;
+class LFSCCnfProof;
+class LFSCTheoryProof;
+  
 // different proof modes
 enum ProofFormat {
   LFSC,
@@ -48,23 +54,44 @@ enum ProofFormat {
 class ProofManager {
   SatProof*   d_satProof;
   CnfProof*   d_cnfProof;
+  TheoryProof* d_theoryProof; 
+
+  Proof* d_fullProof; 
   ProofFormat d_format;
   
   static ProofManager* proofManager; 
   static bool isInitialized; 
   ProofManager(ProofFormat format = LFSC);
+  ~ProofManager(); 
 public:
   static ProofManager* currentPM();
-
   static void      initSatProof(Minisat::Solver* solver); 
   static void      initCnfProof(CVC4::prop::CnfStream* cnfStream);
-
-  static Proof* getProof();
+  static void      initTheoryProof();
+  static Proof*    getProof();
   static SatProof* getSatProof();
   static CnfProof* getCnfProof();
+  static TheoryProof* getTheoryProof();
 
+  // variable prefixes
+  static std::string getInputClausePrefix() { return "pb"; }
+  static std::string getLemmaClausePrefix() { return "lem"; }
+  static std::string getLearntClausePrefix() { return "cl"; }
+  static std::string getVarPrefix() { return "v"; }
+  static std::string getAtomPrefix() { return "a"; }
+  static std::string getLitPrefix() {return "l"; }
 };/* class ProofManager */
 
+class LFSCProof : public Proof {
+  LFSCSatProof* d_satProof;
+  LFSCCnfProof* d_cnfProof;
+  LFSCTheoryProof* d_theoryProof; 
+public:
+  LFSCProof(LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); 
+  virtual void toStream(std::ostream& out);
+  virtual ~LFSCProof() {}
+};
+  
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROOF_MANAGER_H */
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index d9b57f87e..624aac237 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -16,6 +16,8 @@
  **/
 
 #include "proof/sat_proof.h"
+#include "proof/cnf_proof.h"
+#include "proof/proof_manager.h"
 #include "prop/minisat/core/Solver.h"
 
 using namespace std;
@@ -166,7 +168,8 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
     d_clauseId(),
     d_idUnit(),
     d_deleted(),
-    d_inputClauses(), 
+    d_inputClauses(),
+    d_lemmaClauses(),
     d_resChains(),
     d_resStack(),
     d_checkRes(checkRes),
@@ -176,11 +179,23 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
     d_temp_idClause(),
     d_unitConflictId(),
     d_storedUnitConflict(false),
-    d_atomToVar()
+    d_seenLearnt(),
+    d_seenInput(),
+    d_seenLemmas(),
+    d_cnfProof(NULL)
   {
     d_proxy = new ProofProxy(this); 
   }
 
+CnfProof* SatProof::getCnfProof() {
+  Assert (d_cnfProof);
+  return d_cnfProof; 
+}
+
+void SatProof::setCnfProof(CnfProof* cnfProof) {
+  Assert (d_cnfProof == NULL);
+  d_cnfProof = cnfProof; 
+}
 
 /** 
  * Returns true if the resolution chain corresponding to id
@@ -272,8 +287,8 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
   return d_idClause[id]; 
 }
 
-Clause& SatProof::getClause(ClauseId id) {
-  return d_solver->ca[id]; 
+Clause& SatProof::getClause(CRef ref) {
+  return d_solver->ca[ref]; 
 }
 ::Minisat::Lit SatProof::getUnit(ClauseId id) {
   Assert (d_idUnit.find(id) != d_idUnit.end());
@@ -301,6 +316,10 @@ bool SatProof::isInputClause(ClauseId id) {
   return (d_inputClauses.find(id) != d_inputClauses.end()); 
 }
 
+bool SatProof::isLemmaClause(ClauseId id) {
+  return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); 
+}
+
 
 void SatProof::print(ClauseId id) {
   if (d_deleted.find(id) != d_deleted.end()) {
@@ -344,34 +363,43 @@ void SatProof::printRes(ResChain* res) {
 
 /// registration methods
 
-ClauseId SatProof::registerClause(::Minisat::CRef clause, bool isInput) {
+ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) {
   Assert(clause != CRef_Undef); 
   ClauseIdMap::iterator it = d_clauseId.find(clause);
    if (it == d_clauseId.end()) {
      ClauseId newId = d_idCounter++; 
      d_clauseId[clause]= newId;
      d_idClause[newId] =clause;
-     if (isInput) {
+     if (kind == INPUT) {
        Assert (d_inputClauses.find(newId) == d_inputClauses.end()); 
        d_inputClauses.insert(newId); 
      }
+     if (kind == THEORY_LEMMA) {
+       Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end());
+       d_lemmaClauses.insert(newId); 
+     }
    }
-   Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " <<isInput << "\n"; 
+   Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " << kind << "\n"; 
    return d_clauseId[clause]; 
 }
 
-ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, bool isInput) {
+ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) {
   UnitIdMap::iterator it = d_unitId.find(toInt(lit));
   if (it == d_unitId.end()) {
     ClauseId newId = d_idCounter++;
     d_unitId[toInt(lit)] = newId;
     d_idUnit[newId] = lit; 
-    if (isInput) {
+    if (kind == INPUT) {
       Assert (d_inputClauses.find(newId) == d_inputClauses.end());
       d_inputClauses.insert(newId); 
     }
+    if (kind == THEORY_LEMMA) {
+      Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end());
+      d_lemmaClauses.insert(newId); 
+    }
+
   }
-  Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << isInput <<"\n"; 
+  Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n"; 
   return d_unitId[toInt(lit)]; 
 }
 
@@ -593,179 +621,173 @@ void SatProof::markDeleted(CRef clause) {
   }
 }
 
-/// store mapping from theory atoms to new variables
-void SatProof::storeAtom(::Minisat::Lit literal, Expr atom) {
-  Assert(d_atomToVar.find(atom) == d_atomToVar.end());
-  d_atomToVar[atom] = literal; 
+void SatProof::constructProof() {
+  collectClauses(d_emptyClauseId); 
 }
 
+// std::string SatProof::varName(::Minisat::Lit lit) {
+//   ostringstream os;
+//   if (sign(lit)) {
+//     os << "(neg "<< ProofManager::getVarPrefix() <<var(lit) << ")" ; 
+//   }
+//   else {
+//     os << "(pos "<< ProofManager::getVarPrefix() <<var(lit) << ")"; 
+//   }
+//   return os.str(); 
+// }
 
 
-/// LFSCSatProof class
-
-std::string LFSCSatProof::varName(::Minisat::Lit lit) {
-  ostringstream os;
-  if (sign(lit)) {
-    os << "(neg v"<<var(lit) << ")" ; 
-  }
-  else {
-    os << "(pos v"<<var(lit) << ")"; 
-  }
-  return os.str(); 
-}
-
-
-std::string LFSCSatProof::clauseName(ClauseId id) {
+std::string SatProof::clauseName(ClauseId id) {
   ostringstream os;
   if (isInputClause(id)) {
-    os << "p"<<id;
+    os << ProofManager::getInputClausePrefix()<<id;
     return os.str(); 
-  } else {
-    os << "l"<<id;
+  } else 
+  if (isLemmaClause(id)) {
+    os << ProofManager::getLemmaClausePrefix()<<id;
+    return os.str(); 
+  }else {
+    os << ProofManager::getLearntClausePrefix()<<id;
     return os.str(); 
   }
 }
 
-void LFSCSatProof::collectLemmas(ClauseId id) {
-  if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
+void SatProof::collectClauses(ClauseId id) {
+  if (d_seenLearnt.find(id) != d_seenLearnt.end()) {
     return; 
   }
   if (d_seenInput.find(id) != d_seenInput.end()) {
     return; 
   }
+  if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
+    return; 
+  }
 
   if (isInputClause(id)) {
+    CRef input_ref = getClauseRef(id);
+    const Clause& cl = getClause(input_ref);
+    getCnfProof()->addInputClause(id, cl); 
     d_seenInput.insert(id);
     return; 
-  } else {
+  }
+  else if (isLemmaClause(id)) {
+    CRef lemma_ref = getClauseRef(id);
+    const Clause& cl = getClause(lemma_ref);
+    getCnfProof()->addTheoryLemma(id, cl); 
     d_seenLemmas.insert(id); 
+  } 
+  else {
+    d_seenLearnt.insert(id); 
   }
 
   Assert (d_resChains.find(id) != d_resChains.end()); 
   ResChain* res = d_resChains[id];
   ClauseId start = res->getStart();
-  collectLemmas(start);
+  collectClauses(start);
 
   ResSteps steps = res->getSteps(); 
   for(unsigned i = 0; i < steps.size(); i++) {
-    collectLemmas(steps[i].id); 
+    collectClauses(steps[i].id); 
   }
 }
 
+/// LFSCSatProof class
 
-
-void LFSCSatProof::printResolution(ClauseId id) {
-  d_lemmaSS << "(satlem _ _ _ ";
+void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) {
+  out << "(satlem_simplify _ _ _ ";
 
   ResChain* res = d_resChains[id];  
   ResSteps& steps = res->getSteps();
   
   for (int i = steps.size()-1; i >= 0; i--) {
-    d_lemmaSS << "(";
-    d_lemmaSS << (steps[i].sign? "R" : "Q") << " _ _ ";
+    out << "(";
+    out << (steps[i].sign? "R" : "Q") << " _ _ ";
               
   }
   
   ClauseId start_id = res->getStart();
-  if(isInputClause(start_id)) {
-    d_seenInput.insert(start_id); 
-  }
-  d_lemmaSS << clauseName(start_id) << " ";
+  // WHY DID WE NEED THIS?
+  // if(isInputClause(start_id)) {
+  //   d_seenInput.insert(start_id); 
+  // }
+  out << clauseName(start_id) << " ";
   
   for(unsigned i = 0; i < steps.size(); i++) {
-    d_lemmaSS << clauseName(steps[i].id) << " v" << var(steps[i].lit) <<")"; 
+    out << clauseName(steps[i].id) << " "<<ProofManager::getVarPrefix() << var(steps[i].lit) <<")"; 
   }
   
   if (id == d_emptyClauseId) {
-    d_lemmaSS <<"(\\empty empty)";
+    out <<"(\\empty empty)";
     return; 
   }
 
-  d_lemmaSS << "(\\" << clauseName(id) << "\n";   // bind to lemma name
-  d_paren << "))";                                // closing parethesis for lemma binding and satlem
+  out << "(\\" << clauseName(id) << "\n";   // bind to lemma name
+  paren << "))";                            // closing parethesis for lemma binding and satlem
 }
 
 
-void LFSCSatProof::printInputClause(ClauseId id) {
-  if (isUnit(id)) {
-    ::Minisat::Lit lit = getUnit(id); 
-    d_clauseSS << "(% " << clauseName(id) << " (holds (clc ";
-    d_clauseSS << varName(lit) << "cln ))";
-    d_paren << ")";
-    return; 
-  }
+// void LFSCSatProof::printInputClause(ClauseId id) {
+//   if (isUnit(id)) {
+//     ::Minisat::Lit lit = getUnit(id); 
+//     d_clauseSS << "(% " << clauseName(id) << " (holds (clc ";
+//     d_clauseSS << varName(lit) << "cln ))";
+//     d_paren << ")";
+//     return; 
+//   }
   
-  ostringstream os;
-  CRef ref = getClauseRef(id);
-  Assert (ref != CRef_Undef);
-  Clause& c = getClause(ref);
-
-  d_clauseSS << "(% " << clauseName(id) << " (holds ";
-  os << ")"; // closing paren for holds
-  d_paren << ")"; // closing paren for (%
-
-  for(int i = 0; i < c.size(); i++) {
-    d_clauseSS << " (clc " << varName(c[i]) <<" ";
-    os <<")";
-    d_seenVars.insert(var(c[i])); 
-  }
-  d_clauseSS << "cln";
-  d_clauseSS << os.str() << "\n";  
-} 
-
-
-void LFSCSatProof::printClauses() {
-  for (IdHashSet::iterator it = d_seenInput.begin(); it!= d_seenInput.end(); ++it) {
-    printInputClause(*it);
-  }
-}
-
-void LFSCSatProof::printVariables() {
-  for (VarSet::iterator it = d_seenVars.begin(); it != d_seenVars.end(); ++it) {
-    d_varSS << "(% v" << *it <<" var \n";
-    d_paren << ")"; 
-  }
-}
-
-
-void LFSCSatProof::flush(std::ostream& out) {
-  out << d_atomsSS.str(); 
-  out << "(check \n";
-  d_paren <<")"; 
-  out << d_varSS.str();
-  out << d_clauseSS.str();
-  out << "(: (holds cln) \n"; 
-  out << d_lemmaSS.str(); 
-  d_paren << "))";
-  out << d_paren.str();
-  out << "\n";
-}
-
-void LFSCSatProof::toStream(std::ostream& out) {
-  Debug("proof:sat") << " LFSCSatProof::printProof \n";
-  
-  // first collect lemmas to print in reverse order
-  collectLemmas(d_emptyClauseId); 
-  for(IdSet::iterator it = d_seenLemmas.begin(); it!= d_seenLemmas.end(); ++it) {
+//   ostringstream os;
+//   CRef ref = getClauseRef(id);
+//   Assert (ref != CRef_Undef);
+//   Clause& c = getClause(ref);
+
+//   d_clauseSS << "(% " << clauseName(id) << " (holds ";
+//   os << ")"; // closing paren for holds
+//   d_paren << ")"; // closing paren for (%
+
+//   for(int i = 0; i < c.size(); i++) {
+//     d_clauseSS << " (clc " << varName(c[i]) <<" ";
+//     os <<")";
+//     d_seenVars.insert(var(c[i])); 
+//   }
+//   d_clauseSS << "cln";
+//   d_clauseSS << os.str() << "\n";  
+// } 
+
+
+// void LFSCSatProof::printInputClauses() {
+//   for (IdHashSet::iterator it = d_seenInput.begin(); it!= d_seenInput.end(); ++it) {
+//     printInputClause(*it);
+//   }
+// }
+
+
+// void LFSCSatProof::flush(std::ostream& out) {
+//   out << "(check \n";
+//   d_paren <<")"; 
+//   out << d_varSS.str();
+//   out << d_clauseSS.str();
+//   out << "(: (holds cln) \n"; 
+//   out << d_learntSS.str(); 
+//   d_paren << "))";
+//   out << d_paren.str();
+//   out << "\n";
+// }
+
+void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) {
+  for(IdSet::iterator it = d_seenLearnt.begin(); it!= d_seenLearnt.end(); ++it) {
     if(*it != d_emptyClauseId) {
-      printResolution(*it);
+      printResolution(*it, out, paren);
     }
   }
-  printAtoms(); 
-  // last resolution to be printed is the empty clause
-  printResolution(d_emptyClauseId);
-  
-  printClauses();
-  printVariables();
-  flush(out);
+  printResolution(d_emptyClauseId, out, paren);
 }
 
-void LFSCSatProof::printAtoms() {
-  d_atomsSS << "; Mapping between boolean variables and theory atoms \n"; 
-  for (AtomToVar::iterator it = d_atomToVar.begin(); it != d_atomToVar.end(); ++it) {
-    d_atomsSS << "; " << it->first << " => v" << var(it->second) << "\n"; 
-  }
-}
+// void LFSCSatProof::printVariables(std::ostream& out, std::ostream& paren) {
+//   for (VarSet::iterator it = d_seenVars.begin(); it != d_seenVars.end(); ++it) {
+//     out << "(% " << ProofManager::getVarPrefix() << *it <<" var \n";
+//     paren << ")"; 
+//   }
+// }
 
 
 } /* CVC4 namespace */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index fb8966400..0ab86b554 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -89,10 +89,10 @@ typedef std::hash_map < ClauseId, ResChain*>      IdResMap;
 typedef std::hash_set < ClauseId >                IdHashSet;
 typedef std::vector   < ResChain* >               ResStack; 
 
-typedef std::hash_set < int >                     VarSet; 
+typedef std::hash_set < unsigned >                     VarSet; 
 typedef std::set < ClauseId >                     IdSet; 
 typedef std::vector < ::Minisat::Lit >              LitVector; 
-typedef __gnu_cxx::hash_map<Expr, ::Minisat::Lit, ExprHashFunction >  AtomToVar; 
+typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause;
 
 class SatProof; 
 
@@ -104,7 +104,16 @@ public:
   void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
 };/* class ProofProxy */
 
-class SatProof : public Proof {
+
+enum ClauseKind {
+  INPUT,
+  THEORY_LEMMA,
+  LEARNT
+};
+
+class CnfProof; 
+
+class SatProof {
 protected:
   ::Minisat::Solver*    d_solver;
   // clauses 
@@ -114,7 +123,7 @@ protected:
   UnitIdMap           d_unitId;
   IdHashSet           d_deleted;
   IdHashSet           d_inputClauses; 
-  
+  IdHashSet           d_lemmaClauses; 
   // resolutions 
   IdResMap            d_resChains;
   ResStack            d_resStack; 
@@ -133,9 +142,6 @@ protected:
   // unit conflict
   ClauseId d_unitConflictId;
   bool d_storedUnitConflict;
-
-  // atom mapping
-  AtomToVar d_atomToVar;
 public:  
   SatProof(::Minisat::Solver* solver, bool checkRes = false);
 protected:
@@ -143,7 +149,8 @@ protected:
   void printRes(ClauseId id);
   void printRes(ResChain* res); 
   
-  bool isInputClause(ClauseId id); 
+  bool isInputClause(ClauseId id);
+  bool isLemmaClause(ClauseId id);
   bool isUnit(ClauseId id);
   bool isUnit(::Minisat::Lit lit); 
   bool hasResolution(ClauseId id); 
@@ -155,7 +162,7 @@ protected:
   ::Minisat::CRef getClauseRef(ClauseId id);
   ::Minisat::Lit  getUnit(ClauseId id);
   ClauseId      getUnitId(::Minisat::Lit lit); 
-  ::Minisat::Clause& getClause(ClauseId id);
+  ::Minisat::Clause& getClause(::Minisat::CRef ref);
   virtual void toStream(std::ostream& out);
 
   bool checkResolution(ClauseId id);
@@ -206,8 +213,8 @@ public:
   void finalizeProof(::Minisat::CRef conflict);
 
   /// clause registration methods 
-  ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false);
-  ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false);
+  ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT);
+  ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT);
 
   void storeUnitConflict(::Minisat::Lit lit); 
   
@@ -231,49 +238,36 @@ public:
   void     storeUnitResolution(::Minisat::Lit lit); 
   
   ProofProxy* getProxy() {return d_proxy; }
-  /** 
-   * At mapping between literal and theory-atom it represents
-   * 
-   * @param literal 
-   * @param atom 
-   */
-  void storeAtom(::Minisat::Lit literal, Expr atom);
-};/* class SatProof */
-
-class LFSCSatProof: public SatProof {
-private:
-  VarSet             d_seenVars;
-  std::ostringstream d_atomsSS;
-  std::ostringstream d_varSS;
-  std::ostringstream d_lemmaSS;
-  std::ostringstream d_clauseSS;
-  std::ostringstream d_paren; 
-  IdSet              d_seenLemmas;
-  IdHashSet          d_seenInput; 
 
+  /**
+     Constructs the SAT proof identifying the needed lemmas 
+   */
+  void constructProof();
+  
+protected:
+  IdSet              d_seenLearnt;
+  IdHashSet          d_seenInput;
+  IdHashSet          d_seenLemmas; 
+  
   inline std::string varName(::Minisat::Lit lit);
   inline std::string clauseName(ClauseId id); 
 
-  void collectLemmas(ClauseId id);
-  void printResolution(ClauseId id);
-  void printInputClause(ClauseId id);
+  void collectClauses(ClauseId id);
+  CnfProof* d_cnfProof; 
+  CnfProof* getCnfProof();
+public:
+  void setCnfProof(CnfProof* cnfProof);
+  virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0;
+};/* class SatProof */
 
-  void printVariables();
-  void printClauses();
-  void flush(std::ostream& out);
-  void printAtoms(); 
+class LFSCSatProof: public SatProof {
+private:
+  void printResolution(ClauseId id, std::ostream& out, std::ostream& paren);
 public:
-  LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false):
-    SatProof(solver, checkRes),
-    d_seenVars(),
-    d_atomsSS(), 
-    d_varSS(),
-    d_lemmaSS(),
-    d_paren(),
-    d_seenLemmas(),
-    d_seenInput()
-  {} 
-  virtual void toStream(std::ostream& out);  
+  LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false)
+    : SatProof(solver, checkRes)
+  {}
+  virtual void printResolutions(std::ostream& out, std::ostream& paren);
 };/* class LFSCSatProof */
 
 }/* CVC4 namespace */
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
new file mode 100644
index 000000000..224c74e2c
--- /dev/null
+++ b/src/proof/theory_proof.cpp
@@ -0,0 +1,97 @@
+/*********************                                                        */
+/*! \file theory_proof.cpp
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "proof/theory_proof.h"
+
+using namespace CVC4;
+
+TheoryProof::TheoryProof()
+  : d_atomSet()
+{}
+void TheoryProof::addAtom(Expr atom) {
+  d_atomSet.insert(atom); 
+  Assert (atom.getKind() == kind::EQUAL);
+  addDeclaration(atom[0]);
+  addDeclaration(atom[1]); 
+}
+
+void TheoryProof::addDeclaration(Expr term) {
+  Type type = term.getType();
+  if (type.isSort())
+    d_sortDeclarations.insert(type);
+  if (term.getKind() == kind::APPLY_UF) {
+    Expr function = term.getOperator();
+    d_termDeclarations.insert(function); 
+  } else {
+    Assert (term.isVariable()); 
+    Assert (type.isSort()); 
+    d_termDeclarations.insert(term);
+  }
+}
+
+void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
+  if (term.isVariable()) {
+    os << term; 
+    return;
+  }
+  Assert (term.getKind() == kind::APPLY_UF);
+  Expr func = term.getOperator();
+  // only support unary functions so far
+  Assert (func.getNumChildren() == 1); 
+  os << "(apply _ _ " << func << " ";
+  printTerm(term[0], os);
+  os <<")"; 
+}
+
+void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) {
+  // should make this more general 
+  Assert (atom.getKind() == kind::EQUAL);
+  os << "(= ";
+  printTerm(atom[0], os);
+  os << " ";
+  printTerm(atom[1], os);
+  os << ")"; 
+}
+
+void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) {
+  // declaring the sorts
+  for (SortSet::const_iterator it = d_sortDeclarations.begin(); it != d_sortDeclarations.end(); ++it) {
+    os << "(% " << *it << "sort \n";
+    paren << ")"; 
+  }
+
+  // declaring the terms
+  for (TermSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) {
+    Expr term = *it;
+    
+    os << "(% " << term << "(term "; 
+    paren <<")"; 
+
+    Type type = term.getType();
+    if (type.isFunction()) {
+      FunctionType ftype = (FunctionType)type; 
+      Assert (ftype.getArity() == 2);
+      Type arg_type = ftype.getArgTypes()[0];
+      Type result_type = ftype.getRangeType();
+      os << "(arrow " << arg_type << " " << result_type << "))\n"; 
+    } else {
+      Assert (term.isVariable());
+      Assert (type.isSort());
+      os << type << ")\n";
+    }
+  }
+} 
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
new file mode 100644
index 000000000..ac8f9f7b8
--- /dev/null
+++ b/src/proof/theory_proof.h
@@ -0,0 +1,55 @@
+/*********************                                                        */
+/*! \file theory_proof.h
+ ** \verbatim
+ ** Original author: Liana Hadarean
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A manager for UfProofs.
+ **
+ ** A manager for UfProofs.
+ **
+ ** 
+ **/
+
+
+#ifndef __CVC4__THEORY_PROOF_H
+#define __CVC4__THEORY_PROOF_H
+
+#include "cvc4_private.h"
+#include "util/proof.h"
+#include "expr/expr.h"
+#include <ext/hash_set>
+#include <iostream> 
+
+namespace CVC4 {
+
+  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > AtomSet;
+  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > TermSet; 
+  typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; 
+  
+  class TheoryProof {
+  protected:
+    AtomSet d_atomSet;
+    TermSet d_termDeclarations;
+    SortSet d_sortDeclarations; 
+    void addDeclaration(Expr atom); 
+  public:
+    TheoryProof();
+    void addAtom(Expr atom); 
+    virtual void printFormula(Expr atom, std::ostream& os) = 0;
+    virtual void printDeclarations(std::ostream& os, std::ostream& paren) = 0; 
+  };
+
+  class LFSCTheoryProof: public TheoryProof {
+    void printTerm(Expr term, std::ostream& os); 
+  public:
+    virtual void printFormula(Expr atom, std::ostream& os);
+    virtual void printDeclarations(std::ostream& os, std::ostream& paren); 
+  }; 
+} /* CVC4 namespace */
+#endif /* __CVC4__THEORY_PROOF_H */
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 8ebb461e5..47d352949 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -238,7 +238,6 @@ SatLiteral CnfStream::convertAtom(TNode node) {
 
   // Make a new literal (variables are not considered theory literals)
   SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate);
-  PROOF (ProofManager::getSatProof()->storeAtom(MinisatSatSolver::toMinisatLit(lit), node.toExpr()); ); 
   // Return the resulting literal
   return lit;
 }
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 36e196821..45127a182 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -135,8 +135,8 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context,
   // Assert the constants
   uncheckedEnqueue(mkLit(varTrue, false));
   uncheckedEnqueue(mkLit(varFalse, true));
-  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), true); )
-  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), true); )
+  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT); )
+  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT); )
 }
 
 
@@ -263,7 +263,7 @@ CRef Solver::reason(Var x) {
 
     // Construct the reason
     CRef real_reason = ca.alloc(explLevel, explanation, true);
-    PROOF (ProofManager::getSatProof()->registerClause(real_reason, true); ); 
+    PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ); 
     vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
     clauses_removable.push(real_reason);
     attachClause(real_reason);
@@ -339,7 +339,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
         clauses_persistent.push(cr);
 	attachClause(cr);
 
-        PROOF( ProofManager::getSatProof()->registerClause(cr, true); )
+        PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); )
       }
 
       // Check if it propagates
@@ -347,7 +347,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
         if(assigns[var(ps[0])] == l_Undef) {
           assert(assigns[var(ps[0])] != l_False);
           uncheckedEnqueue(ps[0], cr);
-          PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], true); } )
+          PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } )
           return ok = (propagate(CHECK_WITHOUT_THEORY) == CRef_Undef);
         } else return ok;
       }
@@ -1631,7 +1631,7 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, true); ); 
+      PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ); 
       if (removable) {
         clauses_removable.push(lemma_ref);
       } else {