Merge from proof branch

1 files changed, 464 insertions, 156 deletions

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 088275b3f..eaf21846b 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -25,6 +25,7 @@
 #include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
 #include "proof/proof_manager.h"
+#include "proof/proof_output_channel.h"
 #include "proof/proof_utils.h"
 #include "proof/sat_proof.h"
 #include "proof/uf_proof.h"
@@ -48,74 +49,6 @@ namespace CVC4 {
 unsigned CVC4::LetCount::counter = 0;
 static unsigned LET_COUNT = 1;
 
-//for proof replay
-class ProofOutputChannel : public theory::OutputChannel {
-public:
-  Node d_conflict;
-  Proof* d_proof;
-  Node d_lemma;
-
-  ProofOutputChannel() : d_conflict(), d_proof(NULL) {}
-  virtual ~ProofOutputChannel() throw() {}
-
-  void conflict(TNode n, Proof* pf) throw() {
-    Trace("theory-proof-debug") << "; CONFLICT: " << n << std::endl;
-    Assert(d_conflict.isNull());
-    Assert(!n.isNull());
-    d_conflict = n;
-    Assert(pf != NULL);
-    d_proof = pf;
-  }
-  bool propagate(TNode x) throw() {
-    Trace("theory-proof-debug") << "got a propagation: " << x << std::endl;
-    return true;
-  }
-  theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw() {
-    Trace("theory-proof-debug") << "new lemma: " << n << std::endl;
-    d_lemma = n;
-    return theory::LemmaStatus(TNode::null(), 0);
-  }
-  theory::LemmaStatus splitLemma(TNode, bool) throw() {
-    AlwaysAssert(false);
-    return theory::LemmaStatus(TNode::null(), 0);
-  }
-  void requirePhase(TNode n, bool b) throw() {
-    Debug("theory-proof-debug") << "ProofOutputChannel::requirePhase called" << std::endl;
-    Trace("theory-proof-debug") << "requirePhase " << n << " " << b << std::endl;
-  }
-  bool flipDecision() throw() {
-    Debug("theory-proof-debug") << "ProofOutputChannel::flipDecision called" << std::endl;
-    AlwaysAssert(false);
-    return false;
-  }
-  void setIncomplete() throw() {
-    Debug("theory-proof-debug") << "ProofOutputChannel::setIncomplete called" << std::endl;
-    AlwaysAssert(false);
-  }
-};/* class ProofOutputChannel */
-
-//for proof replay
-class MyPreRegisterVisitor {
-  theory::Theory* d_theory;
-  __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited;
-public:
-  typedef void return_type;
-  MyPreRegisterVisitor(theory::Theory* theory)
-  : d_theory(theory)
-  , d_visited()
-  {}
-  bool alreadyVisited(TNode current, TNode parent) { return d_visited.find(current) != d_visited.end(); }
-  void visit(TNode current, TNode parent) {
-    if(theory::Theory::theoryOf(current) == d_theory->getId()) {
-      //Trace("theory-proof-debug") << "preregister " << current << std::endl;
-      d_theory->preRegisterTerm(current);
-      d_visited.insert(current);
-    }
-  }
-  void start(TNode node) { }
-  void done(TNode node) { }
-}; /* class MyPreRegisterVisitor */
-
 TheoryProofEngine::TheoryProofEngine()
   : d_registrationCache()
   , d_theoryProofTable()
@@ -131,13 +64,12 @@ TheoryProofEngine::~TheoryProofEngine() {
   }
 }
 
-
 void TheoryProofEngine::registerTheory(theory::Theory* th) {
-  if( th ){
+  if (th) {
     theory::TheoryId id = th->getId();
     if(d_theoryProofTable.find(id) == d_theoryProofTable.end()) {
 
-      Trace("theory-proof-debug") << "; register theory " << id << std::endl;
+      Trace("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl;
 
       if (id == theory::THEORY_UF) {
         d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this);
@@ -167,19 +99,42 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
 }
 
 TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) {
+  // The UF theory handles queries for the Builtin theory.
+  if (id == theory::THEORY_BUILTIN) {
+    Debug("pf::tp") << "TheoryProofEngine::getTheoryProof: BUILTIN --> UF" << std::endl;
+    id = theory::THEORY_UF;
+  }
+
   Assert (d_theoryProofTable.find(id) != d_theoryProofTable.end());
   return d_theoryProofTable[id];
 }
 
+void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryId id) {
+  d_exprToTheoryIds[term].insert(id);
+}
+
+void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) {
+  LetMap emptyMap;
+
+  os << "(trust_f (not (= _ ";
+  printBoundTerm(c1, os, emptyMap);
+  os << " ";
+  printBoundTerm(c2, os, emptyMap);
+  os << ")))";
+}
+
 void TheoryProofEngine::registerTerm(Expr term) {
+  Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl;
+
   if (d_registrationCache.count(term)) {
     return;
   }
-  Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering new term: " << term << std::endl;
+
+  Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl;
 
   theory::TheoryId theory_id = theory::Theory::theoryOf(term);
 
-  Debug("pf::tp") << "Term's theory: " << theory_id << std::endl;
+  Debug("pf::tp") << "Term's theory( " << term << " ) = " << theory_id << std::endl;
 
   // don't need to register boolean terms
   if (theory_id == theory::THEORY_BUILTIN ||
@@ -193,32 +148,38 @@ void TheoryProofEngine::registerTerm(Expr term) {
 
   if (!supportedTheory(theory_id)) return;
 
+  // Register the term with its owner theory
   getTheoryProof(theory_id)->registerTerm(term);
+
+  // A special case: the array theory needs to know of every skolem, even if
+  // it belongs to another theory (e.g., a BV skolem)
+  if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) {
+    Debug("pf::tp") << "TheoryProofEngine::registerTerm: Special case: registering a non-array skolem: " << term << std::endl;
+    getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term);
+  }
+
   d_registrationCache.insert(term);
 }
 
-theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) {
+theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* clause) {
   ProofManager* pm = ProofManager::currentPM();
 
-  Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )"
-                     << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
+  std::set<Node> nodes;
+  for(unsigned i = 0; i < clause->size(); ++i) {
+    prop::SatLiteral lit = (*clause)[i];
+    Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+    Expr atom = node.toExpr();
+    if (atom.isConst()) {
+      Assert (atom == utils::mkTrue());
+      continue;
+    }
 
-  if ((pm->getLogic() == "QF_UFLIA") || (pm->getLogic() == "QF_UFLRA")) {
-    Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma: special hack for Arithmetic-with-holes support. "
-                       << "Returning THEORY_ARITH" << std::endl;
-    return theory::THEORY_ARITH;
+    nodes.insert(lit.isNegated() ? node.notNode() : node);
   }
 
-  return pm->getCnfProof()->getOwnerTheory(id);
-
-  // if (pm->getLogic() == "QF_UF") return theory::THEORY_UF;
-  // if (pm->getLogic() == "QF_BV") return theory::THEORY_BV;
-  // if (pm->getLogic() == "QF_AX") return theory::THEORY_ARRAY;
-  // if (pm->getLogic() == "ALL_SUPPORTED") return theory::THEORY_BV;
-
-  // Debug("pf::tp") << "Unsupported logic (" << pm->getLogic() << ")" << std::endl;
-
-  // Unreachable();
+  // Ensure that the lemma is in the database.
+  Assert (pm->getCnfProof()->haveProofRecipe(nodes));
+  return pm->getCnfProof()->getProofRecipe(nodes).getTheory();
 }
 
 void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) {
@@ -272,8 +233,6 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) {
 
 void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) {
   theory::TheoryId theory_id = theory::Theory::theoryOf(term);
-  Debug("pf::tp") << std::endl << "LFSCTheoryProofEngine::printTheoryTerm: term = " << term
-                     << ", theory_id = " << theory_id << std::endl;
 
   // boolean terms and ITEs are special because they
   // are common to all theories
@@ -315,6 +274,29 @@ void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) {
   Unreachable();
 }
 
+void LFSCTheoryProofEngine::performExtraRegistrations() {
+  ExprToTheoryIds::const_iterator it;
+  for (it = d_exprToTheoryIds.begin(); it != d_exprToTheoryIds.end(); ++it) {
+    if (d_registrationCache.count(it->first)) { // Only register if the term appeared
+      TheoryIdSet::const_iterator theoryIt;
+      for (theoryIt = it->second.begin(); theoryIt != it->second.end(); ++theoryIt) {
+        Debug("pf::tp") << "\tExtra registration of term " << it->first
+                        << " with theory: " << *theoryIt << std::endl;
+        Assert(supportedTheory(*theoryIt));
+        getTheoryProof(*theoryIt)->registerTerm(it->first);
+      }
+    }
+  }
+}
+
+void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) {
+  TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
+  TheoryProofTable::const_iterator end = d_theoryProofTable.end();
+  for (; it != end; ++it) {
+    it->second->treatBoolsAsFormulas(value);
+  }
+}
+
 void LFSCTheoryProofEngine::registerTermsFromAssertions() {
   ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
   ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
@@ -322,6 +304,8 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() {
   for(; it != end; ++it) {
     registerTerm(*it);
   }
+
+  performExtraRegistrations();
 }
 
 void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) {
@@ -333,17 +317,43 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare
 
   for (; it != end; ++it) {
     Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl;
-    // FIXME: merge this with counter
-    os << "(% A" << counter++ << " (th_holds ";
+    std::ostringstream name;
+    name << "A" << counter++;
+    os << "(% " << name.str() << " (th_holds ";
     printLetTerm(*it,  os);
     os << ")\n";
     paren << ")";
   }
-  //store map between assertion and counter
-  // ProofManager::currentPM()->setAssertion( *it );
+
   Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl << std::endl;
 }
 
+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;
+
+  for (it = rewrites.begin(); it != rewrites.end(); ++it) {
+    Debug("pf::tp") << "printLemmaRewrites: " << it->first << " --> " << it->second << std::endl;
+
+    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";
+
+    d_assertionToRewrite[it->first] = rewriteRule.str();
+    Debug("pf::tp") << "d_assertionToRewrite[" << it->first << "] = " << rewriteRule.str() << std::endl;
+    paren << "))";
+  }
+
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites done" << std::endl << std::endl;
+}
+
 void LFSCTheoryProofEngine::printSortDeclarations(std::ostream& os, std::ostream& paren) {
   Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations called" << std::endl << std::endl;
 
@@ -378,55 +388,148 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost
   }
 }
 
-void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
-                                              std::ostream& os,
-                                              std::ostream& paren) {
-  os << " ;; Theory Lemmas \n";
-  ProofManager* pm = ProofManager::currentPM();
-  IdToSatClause::const_iterator it = lemmas.begin();
-  IdToSatClause::const_iterator end = lemmas.end();
-
-  Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl;
+void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printAliasingDeclarations called" << std::endl;
 
+  TheoryProofTable::const_iterator it = d_theoryProofTable.begin();
+  TheoryProofTable::const_iterator end = d_theoryProofTable.end();
   for (; it != end; ++it) {
-    Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl;
-    ClauseId id = it->first;
-    Debug("pf::tp") << "\tLemma = " << id
-                       << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
+    it->second->printAliasingDeclarations(os, paren);
   }
-  it = lemmas.begin();
+}
 
-  // BitVector theory is special case: must know all
-  // conflicts needed ahead of time for resolution
-  // proof lemmas
-  std::vector<Expr> bv_lemmas;
-  for (; it != end; ++it) {
+void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) {
+  Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl;
+
+  ProofManager* pm = ProofManager::currentPM();
+  for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
     ClauseId id = it->first;
+    Debug("pf::dumpLemmas") << "**** \tLemma ID = " << id << std::endl;
     const prop::SatClause* clause = it->second;
+    std::set<Node> nodes;
+    for(unsigned i = 0; i < clause->size(); ++i) {
+      prop::SatLiteral lit = (*clause)[i];
+      Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+      if (node.isConst()) {
+        Assert (node.toExpr() == utils::mkTrue());
+        continue;
+      }
+      nodes.insert(lit.isNegated() ? node.notNode() : node);
+    }
+
+    LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes);
+    recipe.dump("pf::dumpLemmas");
+  }
 
-    theory::TheoryId theory_id = getTheoryForLemma(id);
-    if (theory_id != theory::THEORY_BV) continue;
+  Debug("pf::dumpLemmas") << "Theory lemma printing DONE" << std::endl << std::endl;
+}
+
+// TODO: this function should be moved into the BV prover.
+void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os, std::ostream& paren) {
+  // BitVector theory is special case: must know all conflicts needed
+  // ahead of time for resolution proof lemmas
+  std::vector<Expr> bv_lemmas;
+
+  for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
+    const prop::SatClause* clause = it->second;
 
     std::vector<Expr> conflict;
+    std::set<Node> conflictNodes;
     for(unsigned i = 0; i < clause->size(); ++i) {
       prop::SatLiteral lit = (*clause)[i];
-      Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr();
+      Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable());
+      Expr atom = node.toExpr();
+
+      // The literals (true) and (not false) are omitted from conflicts
       if (atom.isConst()) {
         Assert (atom == utils::mkTrue() ||
                 (atom == utils::mkFalse() && lit.isNegated()));
         continue;
       }
+
       Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
       conflict.push_back(expr_lit);
+      conflictNodes.insert(lit.isNegated() ? node.notNode() : node);
+    }
+
+    LemmaProofRecipe recipe = ProofManager::currentPM()->getCnfProof()->getProofRecipe(conflictNodes);
+
+    unsigned numberOfSteps = recipe.getNumSteps();
+
+    prop::SatClause currentClause = *clause;
+    std::vector<Expr> currentClauseExpr = conflict;
+
+    for (unsigned i = 0; i < numberOfSteps; ++i) {
+      const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i);
+
+      if (currentStep->getTheory() != theory::THEORY_BV) {
+        continue;
+      }
+
+      // If any rewrites took place, we need to update the conflict clause accordingly
+      std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i);
+      std::map<Node, Node> explanationToMissingAssertion;
+      std::set<Node>::iterator assertionIt;
+      for (assertionIt = missingAssertions.begin();
+           assertionIt != missingAssertions.end();
+           ++assertionIt) {
+        Node negated = (*assertionIt).negate();
+        explanationToMissingAssertion[recipe.getExplanation(negated)] = negated;
+      }
+
+      currentClause = *clause;
+      currentClauseExpr = conflict;
+
+      for (unsigned j = 0; j < i; ++j) {
+        // Literals already used in previous steps need to be negated
+        Node previousLiteralNode = recipe.getStep(j)->getLiteral();
+
+        // If this literal is the result of a rewrite, we need to translate it
+        if (explanationToMissingAssertion.find(previousLiteralNode) !=
+            explanationToMissingAssertion.end()) {
+          previousLiteralNode = explanationToMissingAssertion[previousLiteralNode];
+        }
+
+        Node previousLiteralNodeNegated = previousLiteralNode.negate();
+        prop::SatLiteral previousLiteralNegated =
+          ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated);
+
+        currentClause.push_back(previousLiteralNegated);
+        currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr());
+      }
+
+      // If we're in the final step, the last literal is Null and should not be added.
+      // Otherwise, the current literal does NOT need to be negated
+      Node currentLiteralNode = currentStep->getLiteral();
+
+      if (currentLiteralNode != Node()) {
+        prop::SatLiteral currentLiteral =
+          ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode);
+
+        currentClause.push_back(currentLiteral);
+        currentClauseExpr.push_back(currentLiteralNode.toExpr());
+      }
+
+      bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, currentClauseExpr));
     }
-    bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, conflict));
   }
-  // FIXME: ugly, move into bit-vector proof by adding lemma
-  // queue inside each theory_proof
+
   BitVectorProof* bv = ProofManager::getBitVectorProof();
   bv->finalizeConflicts(bv_lemmas);
-
   bv->printResolutionProof(os, paren);
+}
+
+void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
+                                              std::ostream& os,
+                                              std::ostream& paren) {
+  os << " ;; Theory Lemmas \n";
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl;
+
+  if (Debug.isOn("pf::dumpLemmas")) {
+    dumpTheoryLemmas(lemmas);
+  }
+
+  finalizeBvConflicts(lemmas, os, paren);
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     Assert (lemmas.size() == 1);
@@ -434,54 +537,247 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
     return;
   }
 
-  it = lemmas.begin();
-
+  ProofManager* pm = ProofManager::currentPM();
   Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl;
 
-  for (; it != end; ++it) {
-    Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing a new lemma!" << std::endl;
-
-    // Debug("pf::tp") << "\tLemma = " << it->first << ", " << *(it->second) << std::endl;
+  for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
     ClauseId id = it->first;
-    Debug("pf::tp") << "Owner theory:" << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
     const prop::SatClause* clause = it->second;
-    // printing clause as it appears in resolution proof
-    os << "(satlem _ _ ";
-    std::ostringstream clause_paren;
 
-    Debug("pf::tp") << "CnfProof printing clause..." << std::endl;
-    pm->getCnfProof()->printClause(*clause, os, clause_paren);
-    Debug("pf::tp") << "CnfProof printing clause - Done!" << std::endl;
+    Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = "
+                    << id << std::endl;
 
     std::vector<Expr> clause_expr;
+    std::set<Node> clause_expr_nodes;
     for(unsigned i = 0; i < clause->size(); ++i) {
       prop::SatLiteral lit = (*clause)[i];
-      Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr();
+      Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
+      Expr atom = node.toExpr();
       if (atom.isConst()) {
         Assert (atom == utils::mkTrue());
         continue;
       }
       Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom;
       clause_expr.push_back(expr_lit);
+      clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node);
     }
 
-    Debug("pf::tp") << "Expression printing done!" << std::endl;
-
-    // query appropriate theory for proof of clause
-    theory::TheoryId theory_id = getTheoryForLemma(id);
-    Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
-    Debug("theory-proof-debug") << ";; Get theory lemma from " << theory_id << "..." << std::endl;
-    getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren);
-    Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
-    // os << " (clausify_false trust)";
-    os << clause_paren.str();
-    os << "( \\ " << pm->getLemmaClauseName(id) <<"\n";
-    paren << "))";
+    LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(clause_expr_nodes);
+
+    if (recipe.simpleLemma()) {
+      // In a simple lemma, there will be no propositional resolution in the end
+
+      Debug("pf::tp") << "Simple lemma" << std::endl;
+      // Printing the clause as it appears in resolution proof
+      os << "(satlem _ _ ";
+      std::ostringstream clause_paren;
+      pm->getCnfProof()->printClause(*clause, os, clause_paren);
+
+      // Find and handle missing assertions, due to rewrites
+      std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(0);
+      if (!missingAssertions.empty()) {
+        Debug("pf::tp") << "Have missing assertions for this simple lemma!" << std::endl;
+      }
+
+      std::set<Node>::const_iterator missingAssertion;
+      for (missingAssertion = missingAssertions.begin();
+           missingAssertion != missingAssertions.end();
+           ++missingAssertion) {
+
+        Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl;
+        Assert(recipe.wasRewritten(missingAssertion->negate()));
+        Node explanation = recipe.getExplanation(missingAssertion->negate()).negate();
+        Debug("pf::tp") << "Found explanation: " << explanation << std::endl;
+
+        // We have a missing assertion.
+        //     rewriteIt->first is the assertion after the rewrite (the explanation),
+        //     rewriteIt->second is the original assertion that needs to be fed into the theory.
+
+        bool found = false;
+        unsigned k;
+        for (k = 0; k < clause_expr.size(); ++k) {
+          if (clause_expr[k] == explanation.toExpr()) {
+            found = true;
+            break;
+          }
+        }
+
+        Assert(found);
+        Debug("pf::tp") << "Replacing theory assertion "
+                        << clause_expr[k]
+                        << " with "
+                        << *missingAssertion
+                        << std::endl;
+
+        clause_expr[k] = missingAssertion->toExpr();
+
+        std::ostringstream rewritten;
+        rewritten << "(or_elim_1 _ _ ";
+        rewritten << "(not_not_intro _ ";
+        rewritten << pm->getLitName(explanation);
+        rewritten << ") (iff_elim_1 _ _ ";
+        rewritten << d_assertionToRewrite[missingAssertion->negate()];
+        rewritten << "))";
+
+        Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
+                        << pm->getLitName(*missingAssertion) << " --> " << rewritten.str()
+                        << std::endl << std::endl;
+
+        pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
+      }
+
+      // 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);
+
+      // Turn rewrite filter OFF
+      pm->clearRewriteFilters();
+
+      Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
+      os << clause_paren.str();
+      os << "( \\ " << pm->getLemmaClauseName(id) <<"\n";
+      paren << "))";
+    } else { // This is a composite lemma
+
+      unsigned numberOfSteps = recipe.getNumSteps();
+      prop::SatClause currentClause = *clause;
+      std::vector<Expr> currentClauseExpr = clause_expr;
+
+      for (unsigned i = 0; i < numberOfSteps; ++i) {
+        const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i);
+
+        currentClause = *clause;
+        currentClauseExpr = clause_expr;
+
+        for (unsigned j = 0; j < i; ++j) {
+          // Literals already used in previous steps need to be negated
+          Node previousLiteralNode = recipe.getStep(j)->getLiteral();
+          Node previousLiteralNodeNegated = previousLiteralNode.negate();
+          prop::SatLiteral previousLiteralNegated =
+            ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated);
+          currentClause.push_back(previousLiteralNegated);
+          currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr());
+        }
+
+        // If the current literal is NULL, can ignore (final step)
+        // Otherwise, the current literal does NOT need to be negated
+        Node currentLiteralNode = currentStep->getLiteral();
+        if (currentLiteralNode != Node()) {
+          prop::SatLiteral currentLiteral =
+            ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode);
+
+          currentClause.push_back(currentLiteral);
+          currentClauseExpr.push_back(currentLiteralNode.toExpr());
+        }
+
+        os << "(satlem _ _ ";
+        std::ostringstream clause_paren;
+
+        pm->getCnfProof()->printClause(currentClause, os, clause_paren);
+
+        // query appropriate theory for proof of clause
+        theory::TheoryId theory_id = currentStep->getTheory();
+        Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl;
+
+        std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i);
+        if (!missingAssertions.empty()) {
+          Debug("pf::tp") << "Have missing assertions for this step!" << std::endl;
+        }
+
+        // Turn rewrite filter ON
+        std::set<Node>::const_iterator missingAssertion;
+        for (missingAssertion = missingAssertions.begin();
+             missingAssertion != missingAssertions.end();
+             ++missingAssertion) {
+
+          Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl;
+
+          Assert(recipe.wasRewritten(missingAssertion->negate()));
+          Node explanation = recipe.getExplanation(missingAssertion->negate()).negate();
+
+          Debug("pf::tp") << "Found explanation: " << explanation << std::endl;
+
+          // We have a missing assertion.
+          //     rewriteIt->first is the assertion after the rewrite (the explanation),
+          //     rewriteIt->second is the original assertion that needs to be fed into the theory.
+
+          bool found = false;
+          unsigned k;
+          for (k = 0; k < currentClauseExpr.size(); ++k) {
+            if (currentClauseExpr[k] == explanation.toExpr()) {
+              found = true;
+              break;
+            }
+          }
+
+          Assert(found);
+
+          Debug("pf::tp") << "Replacing theory assertion "
+                          << currentClauseExpr[k]
+                          << " with "
+                          << *missingAssertion
+                          << std::endl;
+
+          currentClauseExpr[k] = missingAssertion->toExpr();
+
+          std::ostringstream rewritten;
+          rewritten << "(or_elim_1 _ _ ";
+          rewritten << "(not_not_intro _ ";
+          rewritten << pm->getLitName(explanation);
+          rewritten << ") (iff_elim_1 _ _ ";
+          rewritten << d_assertionToRewrite[missingAssertion->negate()];
+          rewritten << "))";
+
+          Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl
+                          << pm->getLitName(*missingAssertion) << " --> " << rewritten.str()
+                          << std::endl << std::endl;
+
+          pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str());
+        }
+
+        getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren);
+
+        // Turn rewrite filter OFF
+        pm->clearRewriteFilters();
+
+        Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl;
+        os << clause_paren.str();
+        os << "( \\ " << pm->getLemmaClauseName(id) << "s" << i <<"\n";
+        paren << "))";
+      }
+
+      Assert(numberOfSteps >= 2);
+
+      os << "(satlem_simplify _ _ _ ";
+      for (unsigned i = 0; i < numberOfSteps - 1; ++i) {
+        // Resolve step i with step i + 1
+        if (recipe.getStep(i)->getLiteral().getKind() == kind::NOT) {
+          os << "(Q _ _ ";
+        } else {
+          os << "(R _ _ ";
+        }
+
+        os << pm->getLemmaClauseName(id) << "s" << i;
+        os << " ";
+      }
+
+      os << pm->getLemmaClauseName(id) << "s" << numberOfSteps - 1 << " ";
+
+      prop::SatLiteral v;
+      for (int i = numberOfSteps - 2; i >= 0; --i) {
+        v = ProofManager::currentPM()->getCnfProof()->getLiteral(recipe.getStep(i)->getLiteral());
+        os << ProofManager::getVarName(v.getSatVariable(), "") << ") ";
+      }
+
+      os << "( \\ " << pm->getLemmaClauseName(id) << "\n";
+      paren << "))";
+    }
   }
 }
 
 void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) {
-  // Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl;
 
   LetMap::const_iterator it = map.find(term);
   if (it != map.end()) {
@@ -597,19 +893,21 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Let
 }
 
 void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) {
-  //default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
-  Assert( d_theory!=NULL );
+  // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory
+  Assert(d_theory!=NULL);
+
   context::UserContext fakeContext;
   ProofOutputChannel oc;
   theory::Valuation v(NULL);
   //make new copy of theory
   theory::Theory* th;
-  Trace("theory-proof-debug") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
-  if(d_theory->getId()==theory::THEORY_UF) {
+  Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
+
+  if (d_theory->getId()==theory::THEORY_UF) {
     th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v,
                                   ProofManager::currentPM()->getLogicInfo(),
                                   "replay::");
-  } else if(d_theory->getId()==theory::THEORY_ARRAY) {
+  } else if (d_theory->getId()==theory::THEORY_ARRAY) {
     th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v,
                                           ProofManager::currentPM()->getLogicInfo(),
                                           "replay::");
@@ -714,7 +1012,10 @@ void BooleanProof::registerTerm(Expr term) {
 void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
   Assert (term.getType().isBoolean());
   if (term.isVariable()) {
-    os << "(p_app " << ProofManager::sanitize(term) <<")";
+    if (d_treatBoolsAsFormulas)
+      os << "(p_app " << ProofManager::sanitize(term) <<")";
+    else
+      os << ProofManager::sanitize(term);
     return;
   }
 
@@ -753,7 +1054,10 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap&
     return;
 
   case kind::CONST_BOOLEAN:
-    os << (term.getConst<bool>() ? "true" : "false");
+    if (d_treatBoolsAsFormulas)
+      os << (term.getConst<bool>() ? "true" : "false");
+    else
+      os << (term.getConst<bool>() ? "t_true" : "t_false");
     return;
 
   default:
@@ -786,6 +1090,10 @@ void LFSCBooleanProof::printDeferredDeclarations(std::ostream& os, std::ostream&
   // Nothing to do here at this point.
 }
 
+void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) {
+  // Nothing to do here at this point.
+}
+
 void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
                                              std::ostream& os,
                                              std::ostream& paren) {