Removes old proof code (#4964)

This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.

It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).

1 files changed, 12 insertions, 851 deletions

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 677bf2f8c..258e2fdb2 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -19,8 +19,6 @@
 
 #include "proof/clause_id.h"
 #include "proof/proof_manager.h"
-#include "proof/proof_utils.h"
-#include "proof/theory_proof.h"
 #include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
 #include "prop/sat_solver_types.h"
@@ -32,11 +30,7 @@ CnfProof::CnfProof(prop::CnfStream* stream,
                    const std::string& name)
   : d_cnfStream(stream)
   , d_clauseToAssertion(ctx)
-  , d_assertionToProofRule(ctx)
   , d_currentAssertionStack()
-  , d_currentDefinitionStack()
-  , d_clauseToDefinition(ctx)
-  , d_definitions()
   , d_cnfDeps()
   , d_name(name)
 {
@@ -46,86 +40,22 @@ CnfProof::CnfProof(prop::CnfStream* stream,
 
 CnfProof::~CnfProof() {}
 
-bool CnfProof::isAssertion(Node node) {
-  return d_assertionToProofRule.find(node) !=
-         d_assertionToProofRule.end();
-}
-
-bool CnfProof::isDefinition(Node node) {
-  return d_definitions.find(node) !=
-         d_definitions.end();
-}
-
-ProofRule CnfProof::getProofRule(Node node) {
-  Assert(isAssertion(node));
-  NodeToProofRule::iterator it = d_assertionToProofRule.find(node);
-  return (*it).second;
-}
-
-ProofRule CnfProof::getProofRule(ClauseId clause) {
-  TNode assertion = getAssertionForClause(clause);
-  return getProofRule(assertion);
-}
-
 Node CnfProof::getAssertionForClause(ClauseId clause) {
   ClauseIdToNode::const_iterator it = d_clauseToAssertion.find(clause);
   Assert(it != d_clauseToAssertion.end() && !(*it).second.isNull());
   return (*it).second;
 }
 
-Node CnfProof::getDefinitionForClause(ClauseId clause) {
-  ClauseIdToNode::const_iterator it = d_clauseToDefinition.find(clause);
-  Assert(it != d_clauseToDefinition.end());
-  return (*it).second;
-}
-
-void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) {
+void CnfProof::registerConvertedClause(ClauseId clause)
+{
   Assert(clause != ClauseIdUndef && clause != ClauseIdError
          && clause != ClauseIdEmpty);
-
-  // Explanations do not need a CNF conversion proof since they are in CNF
-  // (they will only need a theory proof as they are theory valid)
-  if (explanation) {
-    Debug("proof:cnf") << "CnfProof::registerConvertedClause "
-                       << clause << " explanation? " << explanation << std::endl;
-    Assert(d_explanations.find(clause) == d_explanations.end());
-    d_explanations.insert(clause);
-    return;
-  }
-
   Node current_assertion = getCurrentAssertion();
-  Node current_expr = getCurrentDefinition();
 
-  Debug("proof:cnf") << "CnfProof::registerConvertedClause "
-                     << clause << " assertion = " << current_assertion
-                     << clause << " definition = " << current_expr << std::endl;
+  Debug("proof:cnf") << "CnfProof::registerConvertedClause " << clause
+                     << " assertion = " << current_assertion << std::endl;
 
   setClauseAssertion(clause, current_assertion);
-  setClauseDefinition(clause, current_expr);
-}
-
-void CnfProof::registerTrueUnitClause(ClauseId clauseId)
-{
-  Node trueNode = NodeManager::currentNM()->mkConst<bool>(true);
-  pushCurrentAssertion(trueNode);
-  pushCurrentDefinition(trueNode);
-  registerConvertedClause(clauseId);
-  popCurrentAssertion();
-  popCurrentDefinition();
-  d_cnfStream->ensureLiteral(trueNode);
-  d_trueUnitClause = clauseId;
-}
-
-void CnfProof::registerFalseUnitClause(ClauseId clauseId)
-{
-  Node falseNode = NodeManager::currentNM()->mkConst<bool>(false).notNode();
-  pushCurrentAssertion(falseNode);
-  pushCurrentDefinition(falseNode);
-  registerConvertedClause(clauseId);
-  popCurrentAssertion();
-  popCurrentDefinition();
-  d_cnfStream->ensureLiteral(falseNode);
-  d_falseUnitClause = clauseId;
 }
 
 void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
@@ -145,56 +75,15 @@ void CnfProof::setClauseAssertion(ClauseId clause, Node expr) {
     return;
   }
 
-  d_clauseToAssertion.insert (clause, expr);
+  d_clauseToAssertion.insert(clause, expr);
 }
 
-void CnfProof::setClauseDefinition(ClauseId clause, Node definition) {
-  Debug("proof:cnf") << "CnfProof::setClauseDefinition "
-                     << clause << " definition " << definition << std::endl;
-  // We keep the first definition
-  if (d_clauseToDefinition.find(clause) != d_clauseToDefinition.end())
-    return;
-
-  d_clauseToDefinition.insert(clause, definition);
-  d_definitions.insert(definition);
-}
-
-void CnfProof::registerAssertion(Node assertion, ProofRule reason) {
-  Debug("proof:cnf") << "CnfProof::registerAssertion "
-                     << assertion << " reason " << reason << std::endl;
-  // We can obtain the assertion from different reasons (e.g. if the
-  // assertion is a lemma over shared terms both theories can generate
-  // the same lemma) We only need to prove the lemma in one way, so we
-  // keep the first reason.
-  if (isAssertion(assertion)) {
-    return;
-  }
-  d_assertionToProofRule.insert(assertion, reason);
-}
-
-LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) {
-  Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end());
-  return d_lemmaToProofRecipe[lemma];
-}
-
-bool CnfProof::haveProofRecipe(const std::set<Node> &lemma) {
-  return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end();
-}
-
-void CnfProof::setCnfDependence(Node from, Node to) {
-  Debug("proof:cnf") << "CnfProof::setCnfDependence "
-                     << "from " << from  << std::endl
-                     << "     to " << to << std::endl;
-
-  Assert(from != to);
-  d_cnfDeps.insert(std::make_pair(from, to));
-}
-
-void CnfProof::pushCurrentAssertion(Node assertion) {
+void CnfProof::pushCurrentAssertion(Node assertion, bool isInput)
+{
   Debug("proof:cnf") << "CnfProof::pushCurrentAssertion " << assertion
                      << std::endl;
 
-  d_currentAssertionStack.push_back(assertion);
+  d_currentAssertionStack.push_back(std::pair<Node, bool>(assertion, isInput));
 
   Debug("proof:cnf") << "CnfProof::pushCurrentAssertion "
                      << "new stack size = " << d_currentAssertionStack.size()
@@ -205,7 +94,7 @@ void CnfProof::popCurrentAssertion() {
   Assert(d_currentAssertionStack.size());
 
   Debug("proof:cnf") << "CnfProof::popCurrentAssertion "
-                     << d_currentAssertionStack.back() << std::endl;
+                     << d_currentAssertionStack.back().first << std::endl;
 
   d_currentAssertionStack.pop_back();
 
@@ -216,740 +105,12 @@ void CnfProof::popCurrentAssertion() {
 
 Node CnfProof::getCurrentAssertion() {
   Assert(d_currentAssertionStack.size());
-  return d_currentAssertionStack.back();
+  return d_currentAssertionStack.back().first;
 }
 
-void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) {
-  Assert(proofRecipe);
-  Assert(proofRecipe->getNumSteps() > 0);
-  d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe;
-}
-
-void CnfProof::pushCurrentDefinition(Node definition) {
-  Debug("proof:cnf") << "CnfProof::pushCurrentDefinition "
-                     << definition  << std::endl;
-
-  d_currentDefinitionStack.push_back(definition);
-}
-
-void CnfProof::popCurrentDefinition() {
-  Assert(d_currentDefinitionStack.size());
-
-  Debug("proof:cnf") << "CnfProof::popCurrentDefinition "
-                     << d_currentDefinitionStack.back() << std::endl;
-
-  d_currentDefinitionStack.pop_back();
-}
-
-Node CnfProof::getCurrentDefinition() {
-  Assert(d_currentDefinitionStack.size());
-  return d_currentDefinitionStack.back();
-}
-
-Node CnfProof::getAtom(prop::SatVariable var) {
-  prop::SatLiteral lit (var);
-  Node node = d_cnfStream->getNode(lit);
-  return node;
-}
-
-void CnfProof::collectAtoms(const prop::SatClause* clause,
-                            std::set<Node>& atoms) {
-  for (unsigned i = 0; i < clause->size(); ++i) {
-    prop::SatLiteral lit = clause->operator[](i);
-    prop::SatVariable var = lit.getSatVariable();
-    TNode atom = getAtom(var);
-    if (atoms.find(atom) == atoms.end()) {
-      atoms.insert(atom);
-    }
-  }
-}
-
-prop::SatLiteral CnfProof::getLiteral(TNode atom) {
-  return d_cnfStream->getLiteral(atom);
-}
-
-bool CnfProof::hasLiteral(TNode atom) {
-  return d_cnfStream->hasLiteral(atom);
-}
-
-void CnfProof::ensureLiteral(TNode atom, bool noPreregistration) {
-  d_cnfStream->ensureLiteral(atom, noPreregistration);
-}
-
-void CnfProof::collectAtomsForClauses(const IdToSatClause& clauses,
-                                      std::set<Node>& atoms) {
-  IdToSatClause::const_iterator it = clauses.begin();
-  for (; it != clauses.end(); ++it) {
-    const prop::SatClause* clause = it->second;
-    collectAtoms(clause, atoms);
-  }
-}
-
-void CnfProof::collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses,
-                                                std::set<Node>& atoms,
-                                                NodePairSet& rewrites) {
-  IdToSatClause::const_iterator it = lemmaClauses.begin();
-  for (; it != lemmaClauses.end(); ++it) {
-    const prop::SatClause* clause = it->second;
-
-    // TODO: just calculate the map from ID to recipe once,
-    // instead of redoing this over and over again
-    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 = getAtom(lit.getSatVariable());
-      Expr atom = node.toExpr();
-      if (atom.isConst()) {
-        Assert(atom == utils::mkTrue());
-        continue;
-      }
-      clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node);
-    }
-
-    LemmaProofRecipe recipe = getProofRecipe(clause_expr_nodes);
-
-    for (unsigned i = 0; i < recipe.getNumSteps(); ++i) {
-      const LemmaProofRecipe::ProofStep* proofStep = recipe.getStep(i);
-      Node atom = proofStep->getLiteral();
-
-      if (atom == Node()) {
-        // The last proof step always has the empty node as its target...
-        continue;
-      }
-
-      if (atom.getKind() == kind::NOT) {
-        atom = atom[0];
-      }
-
-      atoms.insert(atom);
-    }
-
-    LemmaProofRecipe::RewriteIterator rewriteIt;
-    for (rewriteIt = recipe.rewriteBegin(); rewriteIt != recipe.rewriteEnd(); ++rewriteIt) {
-      rewrites.insert(NodePair(rewriteIt->first, rewriteIt->second));
-
-      // The unrewritten terms also need to have literals, so insert them into atoms
-      Node rewritten = rewriteIt->first;
-      if (rewritten.getKind() == kind::NOT) {
-        rewritten = rewritten[0];
-      }
-      atoms.insert(rewritten);
-    }
-  }
-}
-
-void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
-                                           NodeSet& assertions) {
-  IdToSatClause::const_iterator it = clauses.begin();
-  for (; it != clauses.end(); ++it) {
-    TNode used_assertion =  getAssertionForClause(it->first);
-    assertions.insert(used_assertion);
-    // it can be the case that a definition for a clause is an assertion
-    // but it is not the assertion for the clause
-    // e.g. the assertions [(and a b), a]
-    TNode used_definition = getDefinitionForClause(it->first);
-    if (isAssertion(used_definition)) {
-      assertions.insert(used_definition);
-    }
-  }
-}
-
-// Detects whether a clause has x v ~x for some x
-// If so, returns the positive occurence's idx first, then the negative's
-Maybe<std::pair<size_t, size_t>> CnfProof::detectTrivialTautology(
-    const prop::SatClause& clause)
+bool CnfProof::getCurrentAssertionKind()
 {
-  // a map from a SatVariable to its previous occurence's polarity and location
-  std::map<prop::SatVariable, std::pair<bool, size_t>> varsToPolsAndIndices;
-  for (size_t i = 0; i < clause.size(); ++i)
-  {
-    prop::SatLiteral lit = clause[i];
-    prop::SatVariable var = lit.getSatVariable();
-    bool polarity = !lit.isNegated();
-
-    // Check if this var has already occured w/ opposite polarity
-    auto iter = varsToPolsAndIndices.find(var);
-    if (iter != varsToPolsAndIndices.end() && iter->second.first != polarity)
-    {
-      if (iter->second.first)
-      {
-        return Maybe<std::pair<size_t, size_t>>{
-            std::make_pair(iter->second.second, i)};
-      }
-      else
-      {
-        return Maybe<std::pair<size_t, size_t>>{
-            std::make_pair(i, iter->second.second)};
-      }
-    }
-    varsToPolsAndIndices[var] = std::make_pair(polarity, i);
-  }
-  return Maybe<std::pair<size_t, size_t>>{};
-}
-
-void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
-                                    std::ostream& os,
-                                    std::ostream& paren) {
-  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);
-
-    os << " (\\ " << ProofManager::getVarName(var, d_name);
-    os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
-    paren << ")))";
-  }
-}
-
-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();
-    if (pe->printsAsBool(atom.toExpr())) os << "(p_app ";
-    pe->printBoundTerm(atom.toExpr(), os, letMap);
-    if (pe->printsAsBool(atom.toExpr())) os << ")";
-
-    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,
-                                std::map<Node, bool>& childPol ) {
-  std::vector< Node > children;
-  for (unsigned i = 0; i < clause.size(); ++i) {
-    prop::SatLiteral lit = clause[i];
-    prop::SatVariable var = lit.getSatVariable();
-    Node atom = getAtom(var);
-    children.push_back( lit.isNegated() ? atom.negate() : atom );
-    childIndex[atom] = i;
-    childPol[atom] = !lit.isNegated();
-  }
-  return children.size()==1 ? children[0] :
-         NodeManager::currentNM()->mkNode(kind::OR, children );
-}
-
-void LFSCCnfProof::printCnfProofForClause(ClauseId id,
-                                          const prop::SatClause* clause,
-                                          std::ostream& os,
-                                          std::ostream& paren) {
-  Debug("cnf-pf") << std::endl << std::endl << "LFSCCnfProof::printCnfProofForClause( " << id << " ) starting "
-                  << std::endl;
-
-  os << "(satlem _ _ ";
-  std::ostringstream clause_paren;
-  printClause(*clause, os, clause_paren);
-  os << "(clausify_false ";
-
-  // FIXMEEEEEEEEEEEE
-  // os <<"trust)";
-  // os << clause_paren.str()
-  //    << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
-  // paren << "))";
-
-  // return;
-
-  Assert(clause->size() > 0);
-
-  // If the clause contains x v ~x, it's easy!
-  //
-  // It's important to check for this case, because our other logic for
-  // recording the location of variables in the clause assumes the clause is
-  // not tautological
-  Maybe<std::pair<size_t, size_t>> isTrivialTaut =
-      detectTrivialTautology(*clause);
-  if (isTrivialTaut.just())
-  {
-    size_t posIndexInClause = isTrivialTaut.value().first;
-    size_t negIndexInClause = isTrivialTaut.value().second;
-    Trace("cnf-pf") << "; Indices " << posIndexInClause << " (+) and "
-                    << negIndexInClause << " (-) make this clause a tautology"
-                    << std::endl;
-
-    std::string proofOfPos =
-        ProofManager::getLitName((*clause)[negIndexInClause], d_name);
-    std::string proofOfNeg =
-        ProofManager::getLitName((*clause)[posIndexInClause], d_name);
-    os << "(contra _ " << proofOfPos << " " << proofOfNeg << ")";
-  }
-  else
-  {
-    Node base_assertion = getDefinitionForClause(id);
-
-    // get the assertion for the clause id
-    std::map<Node, unsigned> childIndex;
-    std::map<Node, bool> childPol;
-    Node assertion = clauseToNode(*clause, childIndex, childPol);
-    // if there is no reason, construct assertion directly.   This can happen
-    // for unit clauses.
-    if (base_assertion.isNull())
-    {
-      base_assertion = assertion;
-    }
-    // os_base is proof of base_assertion
-    std::stringstream os_base;
-
-    // checks if tautological definitional clause or top-level clause
-    // and prints the proof of the top-level formula
-    bool is_input = printProofTopLevel(base_assertion, os_base);
-
-    if (is_input)
-    {
-      Debug("cnf-pf") << std::endl
-                      << "; base assertion is input. proof: " << os_base.str()
-                      << std::endl;
-    }
-
-    // get base assertion with polarity
-    bool base_pol = base_assertion.getKind() != kind::NOT;
-    base_assertion = base_assertion.getKind() == kind::NOT ? base_assertion[0]
-                                                           : base_assertion;
-
-    std::map<Node, unsigned>::iterator itci = childIndex.find(base_assertion);
-    bool is_in_clause = itci != childIndex.end();
-    unsigned base_index = is_in_clause ? itci->second : 0;
-    Trace("cnf-pf") << std::endl;
-    Trace("cnf-pf") << "; input = " << is_input
-                    << ", is_in_clause = " << is_in_clause << ", id = " << id
-                    << ", assertion = " << assertion
-                    << ", base assertion = " << base_assertion << std::endl;
-    if (!is_input)
-    {
-      Assert(is_in_clause);
-      prop::SatLiteral blit = (*clause)[base_index];
-      os_base << ProofManager::getLitName(blit, d_name);
-      base_pol = !childPol[base_assertion];  // WHY? if the case is =>
-    }
-    Trace("cnf-pf") << "; polarity of base assertion = " << base_pol
-                    << std::endl;
-    Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl;
-
-    bool success = false;
-    if (is_input && is_in_clause && childPol[base_assertion] == base_pol)
-    {
-      // if both in input and in clause, the proof is trivial.  this is the case
-      // for unit clauses.
-      Trace("cnf-pf") << "; trivial" << std::endl;
-      os << "(contra _ ";
-      success = true;
-      prop::SatLiteral lit = (*clause)[itci->second];
-      if (base_pol)
-      {
-        os << os_base.str() << " " << ProofManager::getLitName(lit, d_name);
-      }
-      else
-      {
-        os << ProofManager::getLitName(lit, d_name) << " " << os_base.str();
-      }
-      os << ")";
-    } else if ((base_assertion.getKind()==kind::AND && !base_pol) ||
-           ((base_assertion.getKind()==kind::OR ||
-             base_assertion.getKind()==kind::IMPLIES) && base_pol)) {
-    Trace("cnf-pf") << "; and/or case 1" << std::endl;
-    success = true;
-    std::stringstream os_main;
-    std::stringstream os_paren;
-    //eliminate each one
-    for (int j = base_assertion.getNumChildren()-2; j >= 0; j--) {
-      Trace("cnf-pf-debug") << "; base_assertion[" << j << "] is: " << base_assertion[j]
-                            << ", and its kind is: " << base_assertion[j].getKind() << std::endl ;
-
-      Node child_base = base_assertion[j].getKind()==kind::NOT ?
-                        base_assertion[j][0] : base_assertion[j];
-      bool child_pol = base_assertion[j].getKind()!=kind::NOT;
-
-      Trace("cnf-pf-debug") << "; child " << j << " "
-                            << ", child base: " << child_base
-                            << ", child pol: " << child_pol
-                            << ", childPol[child_base] "
-                            << childPol[child_base] << ", base pol: " << base_pol << std::endl;
-
-      std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base );
-
-      if( itcic!=childIndex.end() ){
-        //Assert( child_pol==childPol[child_base] );
-        os_main << "(or_elim_1 _ _ ";
-        prop::SatLiteral lit = (*clause)[itcic->second];
-        // Should be if in the original formula it was negated
-        // if( childPol[child_base] && base_pol ){
-
-        // Adding the below to catch a specific case where the first child of an IMPLIES is negative,
-        // in which case we need not_not introduction.
-        if (base_assertion.getKind() == kind::IMPLIES && !child_pol && base_pol) {
-          os_main << "(not_not_intro _ " << ProofManager::getLitName(lit, d_name) << ") ";
-        } else if (childPol[child_base] && base_pol) {
-          os_main << ProofManager::getLitName(lit, d_name) << " ";
-        }else{
-          os_main << "(not_not_intro _ " << ProofManager::getLitName(lit, d_name) << ") ";
-        }
-        if( base_assertion.getKind()==kind::AND ){
-          os_main << "(not_and_elim _ _ ";
-          os_paren << ")";
-        }
-        os_paren << ")";
-      }else{
-        success = false;
-      }
-    }
-
-    if( success ){
-      if( base_assertion.getKind()==kind::IMPLIES ){
-        os_main << "(impl_elim _ _ ";
-      }
-      os_main << os_base.str();
-      if( base_assertion.getKind()==kind::IMPLIES ){
-        os_main << ")";
-      }
-      os_main << os_paren.str();
-      int last_index = base_assertion.getNumChildren()-1;
-      Node child_base = base_assertion[last_index].getKind()==kind::NOT ? base_assertion[last_index][0] : base_assertion[last_index];
-      //bool child_pol = base_assertion[last_index].getKind()!=kind::NOT;
-      std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base );
-      if( itcic!=childIndex.end() ){
-        os << "(contra _ ";
-        prop::SatLiteral lit = (*clause)[itcic->second];
-        if( childPol[child_base] && base_pol){
-          os << os_main.str() << " " << ProofManager::getLitName(lit, d_name);
-        }else{
-          os << ProofManager::getLitName(lit, d_name) << " " << os_main.str();
-        }
-        os << ")";
-      }else{
-        success = false;
-      }
-    }
-  }else if ((base_assertion.getKind()==kind::AND && base_pol) ||
-            ((base_assertion.getKind()==kind::OR ||
-              base_assertion.getKind()==kind::IMPLIES) && !base_pol)) {
-
-    std::stringstream os_main;
-
-    Node iatom;
-    if (is_in_clause) {
-      Assert(assertion.getNumChildren() == 2);
-      iatom = assertion[ base_index==0 ? 1 : 0];
-    } else {
-      Assert(assertion.getNumChildren() == 1);
-      iatom = assertion[0];
-    }
-
-    Trace("cnf-pf") << "; and/or case 2, iatom = " << iatom << std::endl;
-    Node e_base = iatom.getKind()==kind::NOT ? iatom[0] : iatom;
-    bool e_pol = iatom.getKind()!=kind::NOT;
-    std::map< Node, unsigned >::iterator itcic = childIndex.find( e_base );
-    if( itcic!=childIndex.end() ){
-      prop::SatLiteral lit = (*clause)[itcic->second];
-      //eliminate until we find iatom
-      for( unsigned j=0; j<base_assertion.getNumChildren(); j++ ){
-        Node child_base = base_assertion[j].getKind()==kind::NOT ? base_assertion[j][0] : base_assertion[j];
-        bool child_pol = base_assertion[j].getKind()!=kind::NOT;
-        if( j==0 && base_assertion.getKind()==kind::IMPLIES ){
-          child_pol = !child_pol;
-        }
-        if( e_base==child_base && (e_pol==child_pol)==(base_assertion.getKind()==kind::AND) ){
-          success = true;
-          bool elimNn =( ( base_assertion.getKind()==kind::OR || ( base_assertion.getKind()==kind::IMPLIES && j==1 ) ) && e_pol );
-          if( elimNn ){
-            os_main << "(not_not_elim _ ";
-          }
-          std::stringstream os_paren;
-          if( j+1<base_assertion.getNumChildren() ){
-            os_main << "(and_elim_1 _ _ ";
-            if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){
-              os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
-              os_paren << ")";
-            }
-            os_paren << ")";
-          }
-          for( unsigned k=0; k<j; k++ ){
-            os_main << "(and_elim_2 _ _ ";
-            if( base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES ){
-              os_main << "(not_" << ( base_assertion.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
-              os_paren << ")";
-            }
-            os_paren << ")";
-          }
-          os_main << os_base.str() << os_paren.str();
-          if( elimNn ){
-            os_main << ")";
-          }
-          break;
-        }
-      }
-      if( success ){
-        os << "(contra _ ";
-        if( !e_pol ){
-          os << ProofManager::getLitName(lit, d_name) << " " << os_main.str();
-        }else{
-          os << os_main.str() << " " << ProofManager::getLitName(lit, d_name);
-        }
-        os << ")";
-      }
-    }
-  }else if( base_assertion.getKind()==kind::XOR || ( base_assertion.getKind()==kind::EQUAL && base_assertion[0].getType().isBoolean() ) ){
-    //eliminate negation
-    int num_nots_2 = 0;
-    int num_nots_1 = 0;
-    Kind k;
-    if( !base_pol ){
-      if( base_assertion.getKind()==kind::EQUAL ){
-        num_nots_2 = 1;
-      }
-      k = kind::EQUAL;
-    }else{
-      k = base_assertion.getKind();
-    }
-    std::vector< unsigned > indices;
-    std::vector< bool > pols;
-    success = true;
-    int elimNum = 0;
-    for( unsigned i=0; i<2; i++ ){
-      Node child_base = base_assertion[i].getKind()==kind::NOT ? base_assertion[i][0] : base_assertion[i];
-      bool child_pol = base_assertion[i].getKind()!=kind::NOT;
-      std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base );
-      if( itcic!=childIndex.end() ){
-        indices.push_back( itcic->second );
-        pols.push_back( childPol[child_base] );
-        if( i==0 ){
-          //figure out which way to elim
-          elimNum = child_pol==childPol[child_base] ? 2 : 1;
-          if( (elimNum==2)==(k==kind::EQUAL) ){
-            num_nots_2++;
-          }
-          if( elimNum==1 ){
-            num_nots_1++;
-          }
-        }
-      }else{
-        success = false;
-        break;
-      }
-    }
-    Trace("cnf-pf") << std::endl << "; num nots = " << num_nots_2 << std::endl;
-    if( success ){
-      os << "(contra _ ";
-      std::stringstream os_base_n;
-      if( num_nots_2==2 ){
-        os_base_n << "(not_not_elim _ ";
-      }
-      os_base_n << "(or_elim_1 _ _ ";
-      prop::SatLiteral lit1 = (*clause)[indices[0]];
-      if( !pols[0] || num_nots_1==1 ){
-        os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") ";
-      }else{
-        Trace("cnf-pf-debug") << "CALLING getlitname" << std::endl;
-        os_base_n << ProofManager::getLitName(lit1, d_name) << " ";
-      }
-      Assert(elimNum != 0);
-      os_base_n << "(" << ( k==kind::EQUAL ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ ";
-      if( !base_pol ){
-        os_base_n << "(not_" << ( base_assertion.getKind()==kind::EQUAL ? "iff" : "xor" ) << "_elim _ _ " << os_base.str() << ")";
-      }else{
-        os_base_n << os_base.str();
-      }
-      os_base_n << "))";
-      if( num_nots_2==2 ){
-        os_base_n << ")";
-        num_nots_2 = 0;
-      }
-      prop::SatLiteral lit2 = (*clause)[indices[1]];
-      if( pols[1]==(num_nots_2==0) ){
-        os << os_base_n.str() << " ";
-        if( num_nots_2==1 ){
-          os << "(not_not_intro _ " << ProofManager::getLitName(lit2, d_name) << ")";
-        }else{
-          os << ProofManager::getLitName(lit2, d_name);
-        }
-      }else{
-        os << ProofManager::getLitName(lit2, d_name) << " " << os_base_n.str();
-      }
-      os << ")";
-    }
-  }else if( base_assertion.getKind()==kind::ITE ){
-    std::map< unsigned, unsigned > appears;
-    std::map< unsigned, Node > appears_expr;
-    unsigned appears_count = 0;
-    for( unsigned r=0; r<3; r++ ){
-      Node child_base = base_assertion[r].getKind()==kind::NOT ? base_assertion[r][0] : base_assertion[r];
-      std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base );
-      if( itcic!=childIndex.end() ){
-        appears[r] = itcic->second;
-        appears_expr[r] = child_base;
-        appears_count++;
-      }
-    }
-    if( appears_count==2 ){
-      success = true;
-      int elimNum = 1;
-      unsigned index1 = 0;
-      unsigned index2 = 1;
-      if( appears.find( 0 )==appears.end() ){
-        elimNum = 3;
-        index1 = 1;
-        index2 = 2;
-      }else if( appears.find( 1 )==appears.end() ){
-        elimNum = 2;
-        index1 = 0;
-        index2 = 2;
-      }
-      std::stringstream os_main;
-      os_main << "(or_elim_1 _ _ ";
-      prop::SatLiteral lit1 = (*clause)[appears[index1]];
-      if( !childPol[appears_expr[index1]] || elimNum==1 || ( elimNum==3 && !base_pol ) ){
-        os_main << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") ";
-      }else{
-        os_main << ProofManager::getLitName(lit1, d_name) << " ";
-      }
-      os_main << "(" << ( base_pol ? "" : "not_" ) << "ite_elim_" << elimNum << " _ _ _ ";
-      os_main << os_base.str() << "))";
-      os << "(contra _ ";
-      prop::SatLiteral lit2 = (*clause)[appears[index2]];
-      if( !childPol[appears_expr[index2]] || !base_pol ){
-        os << ProofManager::getLitName(lit2, d_name) << " " << os_main.str();
-      }else{
-        os << os_main.str() << " " << ProofManager::getLitName(lit2, d_name);
-      }
-      os << ")";
-    }
-  }else if( base_assertion.isConst() ){
-    bool pol = base_assertion==NodeManager::currentNM()->mkConst( true );
-    if( pol!=base_pol ){
-      success = true;
-      if( pol ){
-        os << "(contra _ truth " << os_base.str() << ")";
-      }else{
-        os << os_base.str();
-      }
-    }
-  }
-
-  if( !success ){
-    Trace("cnf-pf") << std::endl;
-    Trace("cnf-pf") << ";!!!!!!!!! CnfProof : Can't process " << assertion << ", base = " << base_assertion << ", id = " << id << std::endl;
-    Trace("cnf-pf") << ";!!!!!!!!! Clause is : ";
-    for (unsigned i = 0; i < clause->size(); ++i) {
-      Trace("cnf-pf") << (*clause)[i] << " ";
-    }
-    Trace("cnf-pf") << std::endl;
-    os << "trust-bad";
-  }
-  }
-
-  os << ")" << clause_paren.str()
-     << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
-
-  paren << "))";
-}
-
-void LFSCCnfProof::printClause(const prop::SatClause& clause,
-                               std::ostream& os,
-                               std::ostream& paren) {
-  for (unsigned i = 0; i < clause.size(); ++i) {
-    prop::SatLiteral lit = clause[i];
-    prop::SatVariable var = lit.getSatVariable();
-    if (lit.isNegated()) {
-      os << "(ast _ _ _ " << ProofManager::getAtomName(var, d_name) <<" (\\ " << ProofManager::getLitName(lit, d_name) << " ";
-      paren << "))";
-    } else {
-      os << "(asf _ _ _ " << ProofManager::getAtomName(var, d_name) <<" (\\ " << ProofManager::getLitName(lit, d_name) << " ";
-      paren << "))";
-    }
-  }
-}
-
-// print a proof of the top-level formula e, based on the input assertions
-bool LFSCCnfProof::printProofTopLevel(Node e, std::ostream& out) {
-  if (!isAssertion(e)) {
-    // check if deduced by CNF
-    // dependence on top level fact i.e. a depends on (a and b)
-    NodeToNode::const_iterator itd = d_cnfDeps.find(e);
-    if (itd != d_cnfDeps.end()) {
-      TNode parent = itd->second;
-      //check if parent is an input assertion
-      std::stringstream out_parent;
-      if (printProofTopLevel(parent, out_parent)) {
-        if(parent.getKind()==kind::AND ||
-           (parent.getKind()==kind::NOT && (parent[0].getKind()==kind::IMPLIES ||
-                                            parent[0].getKind()==kind::OR))) {
-          Node parent_base = parent.getKind()==kind::NOT ? parent[0] : parent;
-          Node e_base = e.getKind()==kind::NOT ? e[0] : e;
-          bool e_pol = e.getKind()!=kind::NOT;
-          for( unsigned i=0; i<parent_base.getNumChildren(); i++ ){
-            Node child_base = parent_base[i].getKind()==kind::NOT ? parent_base[i][0] : parent_base[i];
-            bool child_pol = parent_base[i].getKind()!=kind::NOT;
-            if( parent_base.getKind()==kind::IMPLIES && i==0 ){
-              child_pol = !child_pol;
-            }
-            if (e_base==child_base &&
-                (e_pol==child_pol)==(parent_base.getKind()==kind::AND)) {
-              bool elimNn = ((parent_base.getKind()==kind::OR ||
-                              (parent_base.getKind()==kind::IMPLIES && i==1)) && e_pol);
-              if (elimNn) {
-                out << "(not_not_elim _ ";
-              }
-              std::stringstream out_paren;
-              if (i+1 < parent_base.getNumChildren()) {
-                out << "(and_elim_1 _ _ ";
-                if( parent_base.getKind()==kind::OR ||
-                    parent_base.getKind()==kind::IMPLIES  ){
-                  out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" )
-                      << "_elim _ _ ";
-                  out_paren << ")";
-                }
-                out_paren << ")";
-              }
-              for( unsigned j=0; j<i; j++ ){
-                out << "(and_elim_2 _ _ ";
-                if( parent_base.getKind()==kind::OR || parent_base.getKind()==kind::IMPLIES ){
-                  out << "(not_" << ( parent_base.getKind()==kind::OR ? "or" : "impl" ) << "_elim _ _ ";
-                  out_paren << ")";
-                }
-                out_paren << ")";
-              }
-              out << out_parent.str();
-              out << out_paren.str();
-              if( elimNn ){
-                out << ")";
-              }
-              return true;
-            }
-          }
-        } else {
-          Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e
-                                << " is not correct type (" << parent << ")" << std::endl;
-        }
-      } else {
-        Trace("cnf-pf-debug") << "; isInputAssertion : parent of " << e
-                              << " is not input" << std::endl;
-      }
-    } else {
-      Trace("cnf-pf-debug") << "; isInputAssertion : " << e
-                            << " has no parent" << std::endl;
-    }
-    return false;
-  } else {
-    out << ProofManager::getPreprocessedAssertionName(e);
-    return true;
-  }
+  return d_currentAssertionStack.back().second;
 }
 
 } /* CVC4 namespace */