Revert "Merging proof branch"

This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.

1 files changed, 156 insertions, 464 deletions

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index eaf21846b..088275b3f 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -25,7 +25,6 @@
 #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"
@@ -49,6 +48,74 @@ 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()
@@ -64,12 +131,13 @@ 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("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl;
+      Trace("theory-proof-debug") << "; register theory " << id << std::endl;
 
       if (id == theory::THEORY_UF) {
         d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this);
@@ -99,42 +167,19 @@ 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( " << term << " ) = " << theory_id << std::endl;
+  Debug("pf::tp") << "Term's theory: " << theory_id << std::endl;
 
   // don't need to register boolean terms
   if (theory_id == theory::THEORY_BUILTIN ||
@@ -148,38 +193,32 @@ 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(const prop::SatClause* clause) {
+theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) {
   ProofManager* pm = ProofManager::currentPM();
 
-  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;
-    }
+  Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )"
+                     << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
 
-    nodes.insert(lit.isNegated() ? node.notNode() : node);
+  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;
   }
 
-  // Ensure that the lemma is in the database.
-  Assert (pm->getCnfProof()->haveProofRecipe(nodes));
-  return pm->getCnfProof()->getProofRecipe(nodes).getTheory();
+  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();
 }
 
 void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) {
@@ -233,6 +272,8 @@ 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
@@ -274,29 +315,6 @@ 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();
@@ -304,8 +322,6 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() {
   for(; it != end; ++it) {
     registerTerm(*it);
   }
-
-  performExtraRegistrations();
 }
 
 void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) {
@@ -317,43 +333,17 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare
 
   for (; it != end; ++it) {
     Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl;
-    std::ostringstream name;
-    name << "A" << counter++;
-    os << "(% " << name.str() << " (th_holds ";
+    // FIXME: merge this with counter
+    os << "(% A" << counter++ << " (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;
 
@@ -388,148 +378,55 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost
   }
 }
 
-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) {
-    it->second->printAliasingDeclarations(os, paren);
-  }
-}
+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();
 
-void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) {
-  Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl;
+  Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl;
 
-  ProofManager* pm = ProofManager::currentPM();
-  for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
+  for (; it != end; ++it) {
+    Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl;
     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");
+    Debug("pf::tp") << "\tLemma = " << id
+                       << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl;
   }
+  it = lemmas.begin();
 
-  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
+  // 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) {
+  for (; it != end; ++it) {
+    ClauseId id = it->first;
     const prop::SatClause* clause = it->second;
 
+    theory::TheoryId theory_id = getTheoryForLemma(id);
+    if (theory_id != theory::THEORY_BV) continue;
+
     std::vector<Expr> conflict;
-    std::set<Node> conflictNodes;
     for(unsigned i = 0; i < clause->size(); ++i) {
       prop::SatLiteral lit = (*clause)[i];
-      Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable());
-      Expr atom = node.toExpr();
-
-      // The literals (true) and (not false) are omitted from conflicts
+      Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr();
       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);
+  bv->printResolutionProof(os, paren);
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     Assert (lemmas.size() == 1);
@@ -537,247 +434,54 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas,
     return;
   }
 
-  ProofManager* pm = ProofManager::currentPM();
+  it = lemmas.begin();
+
   Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl;
 
-  for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) {
+  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;
     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") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = "
-                    << id << std::endl;
+    Debug("pf::tp") << "CnfProof printing clause..." << std::endl;
+    pm->getCnfProof()->printClause(*clause, os, clause_paren);
+    Debug("pf::tp") << "CnfProof printing clause - Done!" << 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];
-      Node node = pm->getCnfProof()->getAtom(lit.getSatVariable());
-      Expr atom = node.toExpr();
+      Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).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);
     }
 
-    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 << "))";
-    }
+    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 << "))";
   }
 }
 
 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()) {
@@ -893,21 +597,19 @@ 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("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl;
-
-  if (d_theory->getId()==theory::THEORY_UF) {
+  Trace("theory-proof-debug") << ";; 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::");
@@ -1012,10 +714,7 @@ void BooleanProof::registerTerm(Expr term) {
 void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) {
   Assert (term.getType().isBoolean());
   if (term.isVariable()) {
-    if (d_treatBoolsAsFormulas)
-      os << "(p_app " << ProofManager::sanitize(term) <<")";
-    else
-      os << ProofManager::sanitize(term);
+    os << "(p_app " << ProofManager::sanitize(term) <<")";
     return;
   }
 
@@ -1054,10 +753,7 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap&
     return;
 
   case kind::CONST_BOOLEAN:
-    if (d_treatBoolsAsFormulas)
-      os << (term.getConst<bool>() ? "true" : "false");
-    else
-      os << (term.getConst<bool>() ? "t_true" : "t_false");
+    os << (term.getConst<bool>() ? "true" : "false");
     return;
 
   default:
@@ -1090,10 +786,6 @@ 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) {