Support for printing a global let map in LFSC proofs.

Added a flag to enable/disbale this feature (enabled by default).

Also, added some infrastructure for proving rewrite rules.

15 files changed, 390 insertions, 171 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index b9907aac9..4864cbf46 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -69,18 +69,18 @@ inline static bool match(TNode n1, TNode n2) {
 void ProofArith::toStream(std::ostream& out) {
   Trace("theory-proof-debug") << "; Print Arith proof..." << std::endl;
   //AJR : carry this further?
-  LetMap map;
+  ProofLetMap map;
   toStreamLFSC(out, ProofManager::getArithProof(), d_proof, map);
 }
 
-void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map) {
+void ProofArith::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) {
   Debug("lfsc-arith") << "Printing arith proof in LFSC : " << std::endl;
   pf->debug_print("lfsc-arith");
   Debug("lfsc-arith") << std::endl;
   toStreamRecLFSC( out, tp, pf, 0, map );
 }
 
-Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map) {
+Node ProofArith::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) {
   Debug("pf::arith") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
   pf->debug_print("pf::arith");
   Debug("pf::arith") << std::endl;
@@ -643,7 +643,7 @@ void ArithProof::registerTerm(Expr term) {
   }
 }
 
-void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCArithProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Debug("pf::arith") << "Arith print term: " << term << ". Kind: " << term.getKind()
                      << ". Type: " << term.getType()
                      << ". Number of children: " << term.getNumChildren() << std::endl;
@@ -810,14 +810,14 @@ void LFSCArithProof::printOwnedSort(Type type, std::ostream& os) {
   }
 }
 
-void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void LFSCArithProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
   os << " ;; Arith Theory Lemma \n;;";
   for (unsigned i = 0; i < lemma.size(); ++i) {
     os << lemma[i] <<" ";
   }
   os <<"\n";
   //os << " (clausify_false trust)";
-  ArithProof::printTheoryLemmaProof( lemma, os, paren );
+  ArithProof::printTheoryLemmaProof(lemma, os, paren, map);
 }
 
 void LFSCArithProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 810d41155..d980654c4 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -29,13 +29,13 @@ namespace CVC4 {
 //proof object outputted by TheoryArith
 class ProofArith : public Proof {
 private:
-  static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map);
+  static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map);
 public:
   ProofArith( theory::eq::EqProof * pf ) : d_proof( pf ) {}
   //it is simply an equality engine proof
   theory::eq::EqProof * d_proof;
   void toStream(std::ostream& out);
-  static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map);
+  static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map);
 };
 
 
@@ -68,9 +68,9 @@ public:
   LFSCArithProof(theory::arith::TheoryArith* arith, TheoryProofEngine* proofEngine)
     : ArithProof(arith, proofEngine)
   {}
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
-  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index aee236677..484bc70c8 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -107,14 +107,17 @@ unsigned ProofArray::getExtMergeTag() const {
 }
 
 void ProofArray::toStream(std::ostream& out) {
+  ProofLetMap map;
+  toStream(out, map);
+}
+
+void ProofArray::toStream(std::ostream& out, const ProofLetMap& map) {
   Trace("pf::array") << "; Print Array proof..." << std::endl;
-  //AJR : carry this further?
-  LetMap map;
   toStreamLFSC(out, ProofManager::getArrayProof(), d_proof, map);
   Debug("pf::array") << "; Print Array proof done!" << std::endl;
 }
 
-void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map) {
+void ProofArray::toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const ProofLetMap& map) {
   Debug("pf::array") << "Printing array proof in LFSC : " << std::endl;
   pf->debug_print("pf::array", 0, &d_proofPrinter);
   Debug("pf::array") << std::endl;
@@ -126,7 +129,7 @@ Node ProofArray::toStreamRecLFSC(std::ostream& out,
                                  TheoryProof* tp,
                                  theory::eq::EqProof* pf,
                                  unsigned tb,
-                                 const LetMap& map) {
+                                 const ProofLetMap& map) {
 
   Debug("pf::array") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
   pf->debug_print("pf::array", 0, &d_proofPrinter);
@@ -1122,7 +1125,7 @@ std::string ArrayProof::skolemToLiteral(Expr skolem) {
   return d_skolemToLiteral[skolem];
 }
 
-void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCArrayProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Assert (theory::Theory::theoryOf(term) == theory::THEORY_ARRAY);
 
   if (theory::Theory::theoryOf(term) != theory::THEORY_ARRAY) {
@@ -1216,14 +1219,14 @@ void LFSCArrayProof::printOwnedSort(Type type, std::ostream& os) {
   }
 }
 
-void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void LFSCArrayProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
   os << " ;; Array Theory Lemma \n;;";
   for (unsigned i = 0; i < lemma.size(); ++i) {
     os << lemma[i] <<" ";
   }
   os <<"\n";
   //os << " (clausify_false trust)";
-  ArrayProof::printTheoryLemmaProof(lemma, os, paren);
+  ArrayProof::printTheoryLemmaProof(lemma, os, paren, map);
 }
 
 void LFSCArrayProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
@@ -1308,7 +1311,7 @@ void LFSCArrayProof::printDeferredDeclarations(std::ostream& os, std::ostream& p
     Node array_one = equality[0][0];
     Node array_two = equality[0][1];
 
-    LetMap map;
+    ProofLetMap map;
     os << "(ext _ _ ";
     printTerm(array_one.toExpr(), os, map);
     os << " ";
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 076ba7381..69e62dbf3 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -59,7 +59,7 @@ private:
   Node toStreamRecLFSC(std::ostream& out, TheoryProof* tp,
                        theory::eq::EqProof* pf,
                        unsigned tb,
-                       const LetMap& map);
+                       const ProofLetMap& map);
 
   /** Merge tag for ROW applications */
   unsigned d_reasonRow;
@@ -74,7 +74,8 @@ public:
   //it is simply an equality engine proof
   theory::eq::EqProof *d_proof;
   void toStream(std::ostream& out);
-  void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const LetMap& map);
+  void toStream(std::ostream& out, const ProofLetMap& map);
+  void toStreamLFSC(std::ostream& out, TheoryProof* tp, theory::eq::EqProof* pf, const ProofLetMap& map);
 
   void registerSkolem(Node equality, Node skolem);
 
@@ -117,9 +118,9 @@ public:
     : ArrayProof(arrays, proofEngine)
   {}
 
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
-  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index b2d6fdecf..171085d7f 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -25,6 +25,7 @@
 #include "prop/bvminisat/bvminisat.h"
 #include "theory/bv/bitblaster_template.h"
 #include "theory/bv/theory_bv.h"
+#include "theory/bv/theory_bv_rewrite_rules.h"
 
 using namespace CVC4::theory;
 using namespace CVC4::theory::bv;
@@ -272,7 +273,7 @@ void BitVectorProof::finalizeConflicts(std::vector<Expr>& conflicts) {
   }
 }
 
-void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Debug("pf::bv") << std::endl << "(pf::bv) LFSCBitVectorProof::printOwnedTerm( " << term << " ), theory is: "
                   << Theory::theoryOf(term) << std::endl;
 
@@ -367,7 +368,7 @@ void LFSCBitVectorProof::printOwnedTerm(Expr term, std::ostream& os, const LetMa
   }
 }
 
-void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printBitOf(Expr term, std::ostream& os, const ProofLetMap& map) {
   Assert (term.getKind() == kind::BITVECTOR_BITOF);
   unsigned bit = term.getOperator().getConst<BitVectorBitOf>().bitIndex;
   Expr var = term[0];
@@ -395,7 +396,7 @@ void LFSCBitVectorProof::printConstant(Expr term, std::ostream& os) {
   os << paren.str();
 }
 
-void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map) {
   std::string op = utils::toLFSCKind(term.getKind());
   std::ostringstream paren;
   std::string holes = term.getKind() == kind::BITVECTOR_CONCAT ? "_ _ " : "";
@@ -413,7 +414,7 @@ void LFSCBitVectorProof::printOperatorNary(Expr term, std::ostream& os, const Le
   }
 }
 
-void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map) {
   os <<"(";
   os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" ";
   os << " ";
@@ -421,7 +422,7 @@ void LFSCBitVectorProof::printOperatorUnary(Expr term, std::ostream& os, const L
   os <<")";
 }
 
-void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const ProofLetMap& map) {
   os <<"(";
   os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term[0]) <<" ";
   os << " ";
@@ -431,7 +432,7 @@ void LFSCBitVectorProof::printPredicate(Expr term, std::ostream& os, const LetMa
   os <<")";
 }
 
-void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBitVectorProof::printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map) {
   os <<"(";
   os << utils::toLFSCKind(term.getKind()) << " " << utils::getSize(term) <<" ";
   os <<" ";
@@ -466,7 +467,7 @@ void LFSCBitVectorProof::printOwnedSort(Type type, std::ostream& os) {
   os << "(BitVec "<<width<<")";
 }
 
-void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void LFSCBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
   Debug("pf::bv") << "(pf::bv) LFSCBitVectorProof::printTheoryLemmaProof called" << std::endl;
   Expr conflict = utils::mkSortedExpr(kind::OR, lemma);
   Debug("pf::bv") << "\tconflict = " << conflict << std::endl;
@@ -658,7 +659,7 @@ void LFSCBitVectorProof::printAliasingDeclarations(std::ostream& os, std::ostrea
     os << "(trust_f ";
     os << "(= (BitVec " << utils::getSize(it->first) << ") ";
     os << "(a_var_bv " << utils::getSize(it->first) << " " << it->second << ") ";
-    LetMap emptyMap;
+    ProofLetMap emptyMap;
     d_proofEngine->printBoundTerm(it->first, os, emptyMap);
     os << ")) ";
     os << "(\\ "<< d_aliasToBindDeclaration[it->second] << "\n";
@@ -942,31 +943,28 @@ void LFSCBitVectorProof::printBitblasting(std::ostream& os, std::ostream& paren)
   }
 }
 
-void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
-                                              std::ostream& paren) {
-  // collect the input clauses used
+void LFSCBitVectorProof::calculateAtomsInBitblastingProof() {
+  // Collect the input clauses used
   IdToSatClause used_lemmas;
   IdToSatClause used_inputs;
-  d_resolutionProof->collectClausesUsed(used_inputs,
-                                        used_lemmas);
-  Assert (used_lemmas.empty());
-
-  IdToSatClause::iterator it2;
-  Debug("pf::bv") << std::endl << "BV Used inputs: " << std::endl;
-  for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) {
-    Debug("pf::bv") << "\t input = " << *(it2->second) << std::endl;
-  }
-  Debug("pf::bv") << std::endl;
+  d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas);
+  d_cnfProof->collectAtomsForClauses(used_inputs, d_atomsInBitblastingProof);
+  Assert(used_lemmas.empty());
+}
 
+const std::set<Node>* LFSCBitVectorProof::getAtomsInBitblastingProof() {
+  return &d_atomsInBitblastingProof;
+}
+
+void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
+                                              std::ostream& paren,
+                                              ProofLetMap& letMap) {
   // print mapping between theory atoms and internal SAT variables
   os << std::endl << ";; BB atom mapping\n" << std::endl;
 
-  std::set<Node> atoms;
-  d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
-
   std::set<Node>::iterator atomIt;
   Debug("pf::bv") << std::endl << "BV Dumping atoms from inputs: " << std::endl << std::endl;
-  for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
+  for (atomIt = d_atomsInBitblastingProof.begin(); atomIt != d_atomsInBitblastingProof.end(); ++atomIt) {
     Debug("pf::bv") << "\tAtom: " << *atomIt << std::endl;
   }
   Debug("pf::bv") << std::endl;
@@ -975,7 +973,11 @@ void LFSCBitVectorProof::printResolutionProof(std::ostream& os,
   printBitblasting(os, paren);
 
   // print CNF conversion proof for bit-blasted facts
-  d_cnfProof->printAtomMapping(atoms, os, paren);
+  IdToSatClause used_lemmas;
+  IdToSatClause used_inputs;
+  d_resolutionProof->collectClausesUsed(used_inputs, used_lemmas);
+
+  d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
   os << std::endl << ";; Bit-blasting definitional clauses \n" << std::endl;
   for (IdToSatClause::iterator it = used_inputs.begin();
        it != used_inputs.end(); ++it) {
@@ -1030,4 +1032,13 @@ void LFSCBitVectorProof::printConstantDisequalityProof(std::ostream& os, Expr c1
   os << ")";
 }
 
+void LFSCBitVectorProof::printRewriteProof(std::ostream& os, const Node &n1, const Node &n2) {
+  ProofLetMap emptyMap;
+  os << "(rr_bv_default ";
+  d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap);
+  os << " ";
+  d_proofEngine->printBoundTerm(n1.toExpr(), os, emptyMap);
+  os << ")";
+}
+
 } /* namespace CVC4 */
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 5ea754e08..a52292ec9 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -113,41 +113,48 @@ public:
   virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os) = 0;
 
   virtual void printBitblasting(std::ostream& os, std::ostream& paren) = 0;
-  virtual void printResolutionProof(std::ostream& os, std::ostream& paren) = 0;
-
+  virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap) = 0;
+  virtual const std::set<Node>* getAtomsInBitblastingProof() = 0;
+  virtual void calculateAtomsInBitblastingProof() = 0;
 };
 
 class LFSCBitVectorProof: public BitVectorProof {
 
   void printConstant(Expr term, std::ostream& os);
-  void printOperatorNary(Expr term, std::ostream& os, const LetMap& map);
-  void printOperatorUnary(Expr term, std::ostream& os, const LetMap& map);
-  void printPredicate(Expr term, std::ostream& os, const LetMap& map);
-  void printOperatorParametric(Expr term, std::ostream& os, const LetMap& map);
-  void printBitOf(Expr term, std::ostream& os, const LetMap& map);
+  void printOperatorNary(Expr term, std::ostream& os, const ProofLetMap& map);
+  void printOperatorUnary(Expr term, std::ostream& os, const ProofLetMap& map);
+  void printPredicate(Expr term, std::ostream& os, const ProofLetMap& map);
+  void printOperatorParametric(Expr term, std::ostream& os, const ProofLetMap& map);
+  void printBitOf(Expr term, std::ostream& os, const ProofLetMap& map);
 
   ExprToString d_exprToVariableName;
   ExprToString d_assignedAliases;
   std::map<std::string, std::string> d_aliasToBindDeclaration;
   std::string assignAlias(Expr expr);
   bool hasAlias(Expr expr);
+
+  std::set<Node> d_atomsInBitblastingProof;
+
 public:
   LFSCBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
     :BitVectorProof(bv, proofEngine)
   {}
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
   virtual void printTermBitblasting(Expr term, std::ostream& os);
   virtual void printAtomBitblasting(Expr term, std::ostream& os, bool swap);
   virtual void printAtomBitblastingToFalse(Expr term, std::ostream& os);
-  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printBitblasting(std::ostream& os, std::ostream& paren);
-  virtual void printResolutionProof(std::ostream& os, std::ostream& paren);
+  virtual void printResolutionProof(std::ostream& os, std::ostream& paren, ProofLetMap& letMap);
+  void calculateAtomsInBitblastingProof();
+  const std::set<Node>* getAtomsInBitblastingProof();
   void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+  void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
 };
 
 }/* CVC4 namespace */
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index abe48e3cd..b58ade35e 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -337,6 +337,28 @@ void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
   }
 }
 
+void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
+                                    std::ostream& os,
+                                    std::ostream& paren,
+                                    ProofLetMap &letMap) {
+  std::set<Node>::const_iterator it = atoms.begin();
+  std::set<Node>::const_iterator end = atoms.end();
+
+  for (;it != end; ++it) {
+    os << "(decl_atom ";
+    Node atom = *it;
+    prop::SatVariable var = getLiteral(atom).getSatVariable();
+    //FIXME hideous
+    LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
+    // pe->printLetTerm(atom.toExpr(), os);
+    pe->printBoundTerm(atom.toExpr(), os, letMap);
+
+    os << " (\\ " << ProofManager::getVarName(var, d_name);
+    os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
+    paren << ")))";
+  }
+}
+
 // maps each expr to the position it had in the clause and the polarity it had
 Node LFSCCnfProof::clauseToNode(const prop::SatClause& clause,
                                 std::map<Node, unsigned>& childIndex,
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 62036ced0..788526b80 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -141,6 +141,10 @@ public:
   virtual void printAtomMapping(const std::set<Node>& atoms,
                                 std::ostream& os,
                                 std::ostream& paren) = 0;
+  virtual void printAtomMapping(const std::set<Node>& atoms,
+                           std::ostream& os,
+                           std::ostream& paren,
+                           ProofLetMap &letMap) = 0;
 
   virtual void printClause(const prop::SatClause& clause,
                            std::ostream& os,
@@ -169,6 +173,11 @@ public:
                         std::ostream& os,
                         std::ostream& paren);
 
+  void printAtomMapping(const std::set<Node>& atoms,
+                        std::ostream& os,
+                        std::ostream& paren,
+                        ProofLetMap &letMap);
+
   void printClause(const prop::SatClause& clause,
                    std::ostream& os,
                    std::ostream& paren);
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 5ce8b523f..65a6b1950 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -20,6 +20,7 @@
 #include "base/cvc4_assert.h"
 #include "context/context.h"
 #include "options/bv_options.h"
+#include "options/proof_options.h"
 #include "proof/bitvector_proof.h"
 #include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
@@ -335,6 +336,10 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine,
   , d_smtEngine(smtEngine)
 {}
 
+void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) {
+  Unreachable();
+}
+
 void LFSCProof::toStream(std::ostream& out) {
 
   Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER);
@@ -469,6 +474,16 @@ void LFSCProof::toStream(std::ostream& out) {
   out << " ;; Printing deferred declarations \n\n";
   d_theoryProof->printDeferredDeclarations(out, paren);
 
+  d_theoryProof->finalizeBvConflicts(used_lemmas, out);
+  ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
+
+  out << "\n ;; Printing the global let map \n";
+
+  ProofLetMap globalLetMap;
+  if (options::lfscLetification()) {
+    ProofManager::currentPM()->printGlobalLetMap(atoms, globalLetMap, out, paren);
+  }
+
   out << " ;; Printing aliasing declarations \n\n";
   d_theoryProof->printAliasingDeclarations(out, paren);
 
@@ -476,11 +491,11 @@ void LFSCProof::toStream(std::ostream& out) {
   d_theoryProof->printLemmaRewrites(rewrites, out, paren);
 
   // print trust that input assertions are their preprocessed form
-  printPreprocessedAssertions(used_assertions, out, paren);
+  printPreprocessedAssertions(used_assertions, out, paren, globalLetMap);
 
   // print mapping between theory atoms and internal SAT variables
   out << ";; Printing mapping from preprocessed assertions into atoms \n";
-  d_cnfProof->printAtomMapping(atoms, out, paren);
+  d_cnfProof->printAtomMapping(atoms, out, paren, globalLetMap);
 
   Debug("pf::pm") << std::endl << "Printing cnf proof for clauses" << std::endl;
 
@@ -493,7 +508,7 @@ void LFSCProof::toStream(std::ostream& out) {
   Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl;
 
   Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
-  d_theoryProof->printTheoryLemmas(used_lemmas, out, paren);
+  d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap);
   Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
@@ -515,7 +530,8 @@ void LFSCProof::toStream(std::ostream& out) {
 
 void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
                                             std::ostream& os,
-                                            std::ostream& paren) {
+                                            std::ostream& paren,
+                                            ProofLetMap& globalLetMap) {
   os << "\n ;; In the preprocessor we trust \n";
   NodeSet::const_iterator it = assertions.begin();
   NodeSet::const_iterator end = assertions.end();
@@ -527,7 +543,7 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
 
     //TODO
     os << "(trust_f ";
-    ProofManager::currentPM()->getTheoryProofEngine()->printLetTerm((*it).toExpr(), os);
+    ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap);
     os << ") ";
 
     os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
@@ -640,5 +656,75 @@ std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) {
   return out;
 }
 
+void ProofManager::registerRewrite(unsigned ruleId, Node original, Node result){
+  Assert (currentPM()->d_theoryProof != NULL);
+  currentPM()->d_rewriteLog.push_back(RewriteLogEntry(ruleId, original, result));
+}
+
+void ProofManager::clearRewriteLog() {
+  Assert (currentPM()->d_theoryProof != NULL);
+  currentPM()->d_rewriteLog.clear();
+}
+
+std::vector<RewriteLogEntry> ProofManager::getRewriteLog() {
+  return currentPM()->d_rewriteLog;
+}
+
+void ProofManager::dumpRewriteLog() const {
+  Debug("pf::rr") << "Dumpign rewrite log:" << std::endl;
+
+  for (unsigned i = 0; i < d_rewriteLog.size(); ++i) {
+    Debug("pf::rr") << "\tRule " << d_rewriteLog[i].getRuleId()
+                    << ": "
+                    << d_rewriteLog[i].getOriginal()
+                    << " --> "
+                    << d_rewriteLog[i].getResult() << std::endl;
+  }
+}
+
+void bind(Expr term, ProofLetMap& map, Bindings& letOrder) {
+  ProofLetMap::iterator it = map.find(term);
+  if (it != map.end())
+    return;
+
+  for (unsigned i = 0; i < term.getNumChildren(); ++i)
+    bind(term[i], map, letOrder);
+
+  unsigned newId = ProofLetCount::newId();
+  ProofLetCount letCount(newId);
+  map[term] = letCount;
+  letOrder.push_back(LetOrderElement(term, newId));
+}
+
+void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
+                                     ProofLetMap& letMap,
+                                     std::ostream& out,
+                                     std::ostringstream& paren) {
+  Bindings letOrder;
+  std::set<Node>::const_iterator atom;
+  for (atom = atoms.begin(); atom != atoms.end(); ++atom) {
+    bind(atom->toExpr(), letMap, letOrder);
+  }
+
+  // TODO: give each theory a chance to add atoms. For now, just query BV directly...
+  const std::set<Node>* additionalAtoms = ProofManager::getBitVectorProof()->getAtomsInBitblastingProof();
+  for (atom = additionalAtoms->begin(); atom != additionalAtoms->end(); ++atom) {
+    Debug("gk::temp") << "Binding additional atom: " << *atom << std::endl;
+    bind(atom->toExpr(), letMap, letOrder);
+  }
+
+  for (unsigned i = 0; i < letOrder.size(); ++i) {
+    Expr currentExpr = letOrder[i].expr;
+    unsigned letId = letOrder[i].id;
+    ProofLetMap::iterator it = letMap.find(currentExpr);
+    Assert(it != letMap.end());
+    out << "\n(@ let" << letId << " ";
+    d_theoryProof->printBoundTerm(currentExpr, out, letMap);
+    paren << ")";
+    it->second.increment();
+  }
+
+  out << std::endl << std::endl;
+}
 
 } /* CVC4  namespace */
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index c6454b652..14793f380 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -22,6 +22,7 @@
 #include <iosfwd>
 #include <map>
 #include "proof/proof.h"
+#include "proof/proof_utils.h"
 #include "proof/skolemization_manager.h"
 #include "util/proof.h"
 #include "expr/node.h"
@@ -115,6 +116,30 @@ enum ProofRule {
   RULE_ARRAYS_ROW,  /* arrays, read-over-write */
 };/* enum ProofRules */
 
+class RewriteLogEntry {
+public:
+  RewriteLogEntry(unsigned ruleId, Node original, Node result)
+    : d_ruleId(ruleId), d_original(original), d_result(result) {
+  }
+
+  unsigned getRuleId() const {
+    return d_ruleId;
+  }
+
+  Node getOriginal() const {
+    return d_original;
+  }
+
+  Node getResult() const {
+    return d_result;
+  }
+
+private:
+  unsigned d_ruleId;
+  Node d_original;
+  Node d_result;
+};
+
 class ProofManager {
   CoreSatProof*  d_satProof;
   CnfProof*      d_cnfProof;
@@ -140,6 +165,8 @@ class ProofManager {
 
   std::map<std::string, std::string> d_rewriteFilters;
 
+  std::vector<RewriteLogEntry> d_rewriteLog;
+
 protected:
   LogicInfo d_logic;
 
@@ -231,6 +258,16 @@ public:
   void addRewriteFilter(const std::string &original, const std::string &substitute);
   void clearRewriteFilters();
 
+  static void registerRewrite(unsigned ruleId, Node original, Node result);
+  static void clearRewriteLog();
+
+  std::vector<RewriteLogEntry> getRewriteLog();
+  void dumpRewriteLog() const;
+
+  void printGlobalLetMap(std::set<Node>& atoms,
+                         ProofLetMap& letMap,
+                         std::ostream& out,
+                         std::ostringstream& paren);
 };/* class ProofManager */
 
 class LFSCProof : public Proof {
@@ -242,13 +279,15 @@ class LFSCProof : public Proof {
   // FIXME: hack until we get preprocessing
   void printPreprocessedAssertions(const NodeSet& assertions,
                                    std::ostream& os,
-                                   std::ostream& paren);
+                                   std::ostream& paren,
+                                   ProofLetMap& globalLetMap);
 public:
   LFSCProof(SmtEngine* smtEngine,
             LFSCCoreSatProof* sat,
             LFSCCnfProof* cnf,
             LFSCTheoryProofEngine* theory);
   virtual void toStream(std::ostream& out);
+  virtual void toStream(std::ostream& out, const ProofLetMap& map);
   virtual ~LFSCProof() {}
 };/* class LFSCProof */
 
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index 8c734c892..546d419fc 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -32,6 +32,58 @@ typedef __gnu_cxx::hash_set<Node, NodeHashFunction> NodeSet;
 typedef std::pair<Node, Node> NodePair;
 typedef std::set<NodePair> NodePairSet;
 
+
+struct ProofLetCount {
+  static unsigned counter;
+  static void resetCounter() { counter = 0; }
+  static unsigned newId() { return ++counter; }
+
+  unsigned count;
+  unsigned id;
+  ProofLetCount()
+    : count(0)
+    , id(-1)
+  {}
+
+  void increment() { ++count; }
+  ProofLetCount(unsigned i)
+    : count(1)
+    , id(i)
+  {}
+
+  ProofLetCount(const ProofLetCount& other)
+    : count(other.count)
+    , id (other.id)
+  {}
+
+  bool operator==(const ProofLetCount &other) const {
+    return other.id == id && other.count == count;
+  }
+
+  ProofLetCount& operator=(const ProofLetCount &rhs) {
+    if (&rhs == this) return *this;
+    id = rhs.id;
+    count = rhs.count;
+    return *this;
+  }
+};
+
+struct LetOrderElement {
+  Expr expr;
+  unsigned id;
+  LetOrderElement(Expr e, unsigned i)
+    : expr(e)
+    , id(i)
+  {}
+
+  LetOrderElement()
+    : expr()
+    , id(-1)
+  {}
+};
+
+typedef std::vector<LetOrderElement> Bindings;
+
 namespace utils {
 
 std::string toLFSCKind(Kind kind);
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index fe67ec94d..7fa11cc5f 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -46,7 +46,7 @@
 
 namespace CVC4 {
 
-unsigned CVC4::LetCount::counter = 0;
+unsigned CVC4::ProofLetCount::counter = 0;
 static unsigned LET_COUNT = 1;
 
 TheoryProofEngine::TheoryProofEngine()
@@ -180,30 +180,30 @@ theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* cla
   return pm->getCnfProof()->getProofRecipe(nodes).getTheory();
 }
 
-void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) {
-  LetMap::iterator it = map.find(term);
+void LFSCTheoryProofEngine::bind(Expr term, ProofLetMap& map, Bindings& let_order) {
+  ProofLetMap::iterator it = map.find(term);
   if (it != map.end()) {
-    LetCount& count = it->second;
+    ProofLetCount& count = it->second;
     count.increment();
     return;
   }
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
     bind(term[i], map, let_order);
   }
-  unsigned new_id = LetCount::newId();
-  map[term] = LetCount(new_id);
+  unsigned new_id = ProofLetCount::newId();
+  map[term] = ProofLetCount(new_id);
   let_order.push_back(LetOrderElement(term, new_id));
 }
 
 void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) {
-  LetMap map;
+  ProofLetMap map;
   Bindings let_order;
   bind(term, map, let_order);
   std::ostringstream paren;
   for (unsigned i = 0; i < let_order.size(); ++i) {
     Expr current_expr = let_order[i].expr;
     unsigned let_id = let_order[i].id;
-    LetMap::const_iterator it = map.find(current_expr);
+    ProofLetMap::const_iterator it = map.find(current_expr);
     Assert (it != map.end());
     unsigned let_count = it->second.count;
     Assert(let_count);
@@ -212,7 +212,7 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) {
       continue;
     }
 
-    os << "(@ let"<<let_id << " ";
+    os << "(@ let" <<let_id << " ";
     printTheoryTerm(current_expr, os, map);
     paren <<")";
   }
@@ -223,13 +223,12 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) {
     printTheoryTerm(last, os, map);
   }
   else {
-    os << " let"<< last_let_id;
+    os << " let" << last_let_id;
   }
   os << paren.str();
 }
 
-
-void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   theory::TheoryId theory_id = theory::Theory::theoryOf(term);
 
   // boolean terms and ITEs are special because they
@@ -318,7 +317,11 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare
     std::ostringstream name;
     name << "A" << counter++;
     os << "(% " << name.str() << " (th_holds ";
-    printLetTerm(*it,  os);
+
+    // Assertions appear before the global let map, so we use a dummpMap to avoid letification here.
+    ProofLetMap dummyMap;
+    printBoundTerm(*it, os, dummyMap);
+
     os << ")\n";
     paren << ")";
   }
@@ -326,7 +329,9 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare
   Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl << std::endl;
 }
 
-void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren) {
+void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites,
+                                               std::ostream& os,
+                                               std::ostream& paren) {
   Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites called" << std::endl << std::endl;
 
   NodePairSet::const_iterator it;
@@ -334,15 +339,16 @@ void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, std::ostre
   for (it = rewrites.begin(); it != rewrites.end(); ++it) {
     Debug("pf::tp") << "printLemmaRewrites: " << it->first << " --> " << it->second << std::endl;
 
+    Node n1 = it->first;
+    Node n2 = it->second;
+    Assert(theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2));
+
     std::ostringstream rewriteRule;
     rewriteRule << ".lrr" << d_assertionToRewrite.size();
 
-    LetMap emptyMap;
-    os << "(th_let_pf _ (trust_f (iff ";
-    printBoundTerm(it->second.toExpr(), os, emptyMap);
-    os << " ";
-    printBoundTerm(it->first.toExpr(), os, emptyMap);
-    os << ")) (\\ " << rewriteRule.str() << "\n";
+    os << "(th_let_pf _ ";
+    getTheoryProof(theory::Theory::theoryOf(n1))->printRewriteProof(os, n1, n2);
+    os << "(\\ " << rewriteRule.str() << "\n";
 
     d_assertionToRewrite[it->first] = rewriteRule.str();
     Debug("pf::tp") << "d_assertionToRewrite[" << it->first << "] = " << rewriteRule.str() << std::endl;
@@ -423,7 +429,7 @@ void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) {
 }
 
 // TODO: this function should be moved into the BV prover.
-void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren) {
+void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os) {
   // BitVector theory is special case: must know all conflicts needed
   // ahead of time for resolution proof lemmas
   std::vector<Expr> bv_lemmas;
@@ -514,12 +520,13 @@ void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std
 
   BitVectorProof* bv = ProofManager::getBitVectorProof();
   bv->finalizeConflicts(bv_lemmas);
-  bv->printResolutionProof(os, paren);
+  //  bv->printResolutionProof(os, paren, letMap);
 }
 
 void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
                                               std::ostream& os,
-                                              std::ostream& paren) {
+                                              std::ostream& paren,
+                                              ProofLetMap& map) {
   os << " ;; Theory Lemmas \n";
   Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl;
 
@@ -527,7 +534,8 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
     dumpTheoryLemmas(lemmas);
   }
 
-  finalizeBvConflicts(lemmas, os, paren);
+  //  finalizeBvConflicts(lemmas, os, paren, map);
+  ProofManager::getBitVectorProof()->printResolutionProof(os, paren, map);
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     Assert (lemmas.size() == 1);
@@ -627,7 +635,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
       // Query the appropriate theory for a proof of this clause
       theory::TheoryId theory_id = getTheoryForLemma(clause);
       Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
-      getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren);
+      getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren, map);
 
       // Turn rewrite filter OFF
       pm->clearRewriteFilters();
@@ -734,7 +742,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
           pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
         }
 
-        getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren);
+        getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren, map);
 
         // Turn rewrite filter OFF
         pm->clearRewriteFilters();
@@ -774,15 +782,15 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
   }
 }
 
-void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
 
-  LetMap::const_iterator it = map.find(term);
+  ProofLetMap::const_iterator it = map.find(term);
   if (it != map.end()) {
     unsigned id = it->second.id;
     unsigned count = it->second.count;
     if (count > LET_COUNT) {
-      os <<"let"<<id;
+      os << "let" << id;
       return;
     }
   }
@@ -790,7 +798,7 @@ void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const Le
   printTheoryTerm(term, os, map);
 }
 
-void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   if (term.isVariable()) {
     os << ProofManager::sanitize(term);
     return;
@@ -890,7 +898,10 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Let
 
 }
 
-void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
+                                        std::ostream& os,
+                                        std::ostream& paren,
+                                        const ProofLetMap& map) {
   // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
   Assert(d_theory!=NULL);
 
@@ -975,7 +986,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream&
     th->check(theory::Theory::EFFORT_FULL);
   }
   Debug("pf::tp") << "Calling   oc.d_proof->toStream(os)" << std::endl;
-  oc.d_proof->toStream(os);
+  oc.d_proof->toStream(os, map);
   Debug("pf::tp") << "Calling   oc.d_proof->toStream(os) -- DONE!" << std::endl;
 
   Debug("pf::tp") << "About to delete the theory solver used for proving the lemma... " << std::endl;
@@ -1007,7 +1018,7 @@ void BooleanProof::registerTerm(Expr term) {
   }
 }
 
-void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Assert (term.getType().isBoolean());
   if (term.isVariable()) {
     if (d_treatBoolsAsFormulas)
@@ -1101,7 +1112,7 @@ void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
 void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
   // By default, we just print a trust statement. Specific theories can implement
   // better proofs.
-  LetMap emptyMap;
+  ProofLetMap emptyMap;
 
   os << "(trust_f (not (= _ ";
   d_proofEngine->printBoundTerm(c1, os, emptyMap);
@@ -1110,4 +1121,14 @@ void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr
   os << ")))";
 }
 
+void TheoryProof::printRewriteProof(std::ostream& os, const Node &n1, const Node &n2) {
+  // This is the default for a rewrite proof: just a trust statement.
+  ProofLetMap emptyMap;
+  os << "(trust_f (iff ";
+  d_proofEngine->printBoundTerm(n1.toExpr(), os, emptyMap);
+  os << " ";
+  d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap);
+  os << "))";
+}
+
 } /* namespace CVC4 */
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 352cc1b53..f6f00fa11 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -35,57 +35,8 @@ namespace theory {
 class Theory;
 } /* namespace CVC4::theory */
 
-struct LetCount {
-  static unsigned counter;
-  static void resetCounter() { counter = 0; }
-  static unsigned newId() { return ++counter; }
-
-  unsigned count;
-  unsigned id;
-  LetCount()
-    : count(0)
-    , id(-1)
-  {}
-
-  void increment() { ++count; }
-  LetCount(unsigned i)
-    : count(1)
-    , id(i)
-  {}
-  LetCount(const LetCount& other)
-    : count(other.count)
-    , id (other.id)
-  {}
-  bool operator==(const LetCount &other) const {
-    return other.id == id && other.count == count;
-  }
-  LetCount& operator=(const LetCount &rhs) {
-    if (&rhs == this) return *this;
-    id = rhs.id;
-    count = rhs.count;
-    return *this;
-  }
-};
-
-struct LetOrderElement {
-  Expr expr;
-  unsigned id;
-  LetOrderElement(Expr e, unsigned i)
-    : expr(e)
-    , id(i)
-  {}
-
-  LetOrderElement()
-    : expr()
-    , id(-1)
-  {}
-};
-
 typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
 
-typedef __gnu_cxx::hash_map<Expr, LetCount, ExprHashFunction> LetMap;
-typedef std::vector<LetOrderElement> Bindings;
-
 class TheoryProof;
 
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
@@ -118,7 +69,7 @@ public:
    */
   virtual void printLetTerm(Expr term, std::ostream& os) = 0;
   virtual void printBoundTerm(Expr term, std::ostream& os,
-                              const LetMap& map) = 0;
+                              const ProofLetMap& map) = 0;
 
   /**
    * Print the proof representation of the given sort.
@@ -168,7 +119,7 @@ public:
    * @param paren
    */
   virtual void printTheoryLemmas(const IdToSatClause& lemmas, std::ostream& os,
-                                 std::ostream& paren) = 0;
+                                 std::ostream& paren, ProofLetMap& map) = 0;
 
   /**
    * Register theory atom (ensures all terms and atoms are declared).
@@ -192,40 +143,43 @@ public:
   void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
 
   virtual void treatBoolsAsFormulas(bool value) {};
+
+  virtual void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
 };
 
 class LFSCTheoryProofEngine : public TheoryProofEngine {
-  LetMap d_letMap;
-  void printTheoryTerm(Expr term, std::ostream& os, const LetMap& map);
-  void bind(Expr term, LetMap& map, Bindings& let_order);
+  void bind(Expr term, ProofLetMap& map, Bindings& let_order);
 public:
   LFSCTheoryProofEngine()
     : TheoryProofEngine() {}
 
+  void printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map);
+
   void registerTermsFromAssertions();
   void printSortDeclarations(std::ostream& os, std::ostream& paren);
   void printTermDeclarations(std::ostream& os, std::ostream& paren);
-  virtual void printCoreTerm(Expr term, std::ostream& os, const LetMap& map);
+  virtual void printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printLetTerm(Expr term, std::ostream& os);
-  virtual void printBoundTerm(Expr term, std::ostream& os, const LetMap& map);
+  virtual void printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printAssertions(std::ostream& os, std::ostream& paren);
   virtual void printLemmaRewrites(NodePairSet& rewrites, std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printAliasingDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTheoryLemmas(const IdToSatClause& lemmas,
                                  std::ostream& os,
-                                 std::ostream& paren);
+                                 std::ostream& paren,
+                                 ProofLetMap& map);
   virtual void printSort(Type type, std::ostream& os);
 
   void performExtraRegistrations();
 
   void treatBoolsAsFormulas(bool value);
+  void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os);
 
 private:
   static void dumpTheoryLemmas(const IdToSatClause& lemmas);
 
   // TODO: this function should be moved into the BV prover.
-  void finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren);
 
   std::map<Node, std::string> d_assertionToRewrite;
 };
@@ -247,7 +201,7 @@ public:
    * @param term expresion representing term
    * @param os output stream
    */
-  void printTerm(Expr term, std::ostream& os, const LetMap& map) {
+  void printTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
     d_proofEngine->printBoundTerm(term, os, map);
   }
   /**
@@ -256,7 +210,7 @@ public:
    * @param term expresion representing term
    * @param os output stream
    */
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
+  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
   /**
    * Print the proof representation of the given type that belongs to some theory.
    *
@@ -279,7 +233,10 @@ public:
    *
    * @param os output stream
    */
-  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma,
+                                     std::ostream& os,
+                                     std::ostream& paren,
+                                     const ProofLetMap& map);
   /**
    * Print the sorts declarations for this theory.
    *
@@ -321,6 +278,12 @@ public:
    * @param term
    */
   virtual void printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2);
+  /**
+   * Print a proof for the equivalence of n1 and n2.
+   *
+   * @param term
+   */
+  virtual void printRewriteProof(std::ostream& os, const Node &n1, const Node &n2);
 
   virtual void treatBoolsAsFormulas(bool value) {}
 };
@@ -333,7 +296,7 @@ public:
 
   virtual void registerTerm(Expr term);
 
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) = 0;
+  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) = 0;
 
   virtual void printOwnedSort(Type type, std::ostream& os) = 0;
   virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) = 0;
@@ -348,7 +311,7 @@ public:
   LFSCBooleanProof(TheoryProofEngine* proofEngine)
     : BooleanProof(proofEngine), d_treatBoolsAsFormulas(true)
   {}
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
   virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index bc409901c..139ce5ed2 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -67,13 +67,17 @@ inline static bool match(TNode n1, TNode n2) {
 
 
 void ProofUF::toStream(std::ostream& out) {
+  ProofLetMap map;
+  toStream(out, map);
+}
+
+void ProofUF::toStream(std::ostream& out, const ProofLetMap& map) {
   Trace("theory-proof-debug") << "; Print UF proof..." << std::endl;
   //AJR : carry this further?
-  LetMap map;
   toStreamLFSC(out, ProofManager::getUfProof(), d_proof, map);
 }
 
-void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map) {
+void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map) {
   Debug("pf::uf") << "ProofUF::toStreamLFSC starting" << std::endl;
   Debug("lfsc-uf") << "Printing uf proof in LFSC : " << std::endl;
   pf->debug_print("lfsc-uf");
@@ -81,7 +85,7 @@ void ProofUF::toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqPr
   toStreamRecLFSC( out, tp, pf, 0, map );
 }
 
-Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map) {
+Node ProofUF::toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map) {
   Debug("pf::uf") << std::endl << std::endl << "toStreamRecLFSC called. tb = " << tb << " . proof:" << std::endl;
   pf->debug_print("pf::uf");
   Debug("pf::uf") << std::endl;
@@ -693,7 +697,7 @@ void UFProof::registerTerm(Expr term) {
   }
 }
 
-void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
+void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) {
   Debug("pf::uf") << std::endl << "(pf::uf) LFSCUfProof::printOwnedTerm: term = " << term << std::endl;
 
   Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF);
@@ -732,14 +736,14 @@ void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
   os << type <<" ";
 }
 
-void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
+void LFSCUFProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map) {
   os << " ;; UF Theory Lemma \n;;";
   for (unsigned i = 0; i < lemma.size(); ++i) {
     os << lemma[i] <<" ";
   }
   os <<"\n";
   //os << " (clausify_false trust)";
-  UFProof::printTheoryLemmaProof( lemma, os, paren );
+  UFProof::printTheoryLemmaProof(lemma, os, paren, map);
 }
 
 void LFSCUFProof::printSortDeclarations(std::ostream& os, std::ostream& paren) {
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index 0a23267d8..444b602dc 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -28,13 +28,14 @@ namespace CVC4 {
 //proof object outputted by TheoryUF
 class ProofUF : public Proof {
 private:
-  static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const LetMap& map);
+  static Node toStreamRecLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, unsigned tb, const ProofLetMap& map);
 public:
   ProofUF( theory::eq::EqProof * pf ) : d_proof( pf ) {}
   //it is simply an equality engine proof
   theory::eq::EqProof * d_proof;
   void toStream(std::ostream& out);
-  static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const LetMap& map);
+  void toStream(std::ostream& out, const ProofLetMap& map);
+  static void toStreamLFSC(std::ostream& out, TheoryProof * tp, theory::eq::EqProof * pf, const ProofLetMap& map);
 };
 
 
@@ -63,9 +64,9 @@ public:
   LFSCUFProof(theory::uf::TheoryUF* uf, TheoryProofEngine* proofEngine)
     : UFProof(uf, proofEngine)
   {}
-  virtual void printOwnedTerm(Expr term, std::ostream& os, const LetMap& map);
+  virtual void printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map);
   virtual void printOwnedSort(Type type, std::ostream& os);
-  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren);
+  virtual void printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren, const ProofLetMap& map);
   virtual void printSortDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printTermDeclarations(std::ostream& os, std::ostream& paren);
   virtual void printDeferredDeclarations(std::ostream& os, std::ostream& paren);