CNF proofs. Infrastructure for preprocessing proofs. Updates to smt.plf signature. Add regressions.

6 files changed, 517 insertions, 10 deletions

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 22a40ff69..9634cb47b 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -2,7 +2,7 @@
 /*! \file cnf_proof.cpp
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
+ ** Major contributors: Morgan Deters, Andrew Reynolds
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
@@ -71,15 +71,54 @@ void LFSCCnfProof::printAtomMapping(const prop::SatClause* clause, std::ostream&
 }
 
 void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
+  printPreprocess(os, paren);
   printInputClauses(os, paren);
   printTheoryLemmas(os, paren);
 }
 
+void LFSCCnfProof::printPreprocess(std::ostream& os, std::ostream& paren) {
+  os << " ;; Preprocessing \n";
+  __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction >::const_iterator it = ProofManager::currentPM()->begin_deps();
+  __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction >::const_iterator end = ProofManager::currentPM()->end_deps();
+
+  for (; it != end; ++it) {
+    if( !it->second.empty() ){
+      Expr e = it->first.toExpr();
+      os << "(th_let_pf _ ";
+
+      //TODO
+      os << "(trust_f ";
+      LFSCTheoryProof::printTerm(e, os);
+      os << ") ";
+
+      os << "(\\ A" << ProofManager::currentPM()->getAssertionCounter() << std::endl;
+      ProofManager::currentPM()->setAssertion( e );
+      paren << "))";
+    }
+  }
+}
+
+Expr LFSCCnfProof::clauseToExpr( const prop::SatClause& clause,
+                                 std::map< Expr, unsigned >& childIndex,
+                                 std::map< Expr, 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 = Node::fromExpr( getAtom(var) );
+    children.push_back( lit.isNegated() ? atom.negate() : atom );
+    childIndex[atom.toExpr()] = i;
+    childPol[atom.toExpr()] = !lit.isNegated();
+  }
+  return children.size()==1 ? children[0].toExpr() : NodeManager::currentNM()->mkNode( kind::OR, children ).toExpr();
+}
+
 void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
   os << " ;; Clauses\n";
   ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses();
   ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses();
 
+
   for (; it != end; ++it) {
     ClauseId id = it->first;
     const prop::SatClause* clause = it->second;
@@ -87,7 +126,325 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
     os << "(satlem _ _ ";
     std::ostringstream clause_paren;
     printClause(*clause, os, clause_paren);
-    os << "(clausify_false trust)" << clause_paren.str()
+    os << "(clausify_false ";
+
+    Assert( clause->size()>0 );
+
+    Expr base_assertion = ProofManager::currentPM()->getFormulaForClauseId( id );
+    ProofRule pr = ProofManager::currentPM()->getProofRuleForClauseId( id );
+
+    //get the assertion for the clause id
+    std::map< Expr, unsigned > childIndex;
+    std::map< Expr, bool > childPol;
+    Expr assertion = clauseToExpr( *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;
+    bool is_input = ProofManager::currentPM()->isInputAssertion( base_assertion, os_base );
+
+    //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< Expr, 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);
+      base_pol = !childPol[base_assertion];
+    }
+    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);
+      }else{
+        os << ProofManager::getLitName(lit) << " " << 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-- ){
+        Expr 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;
+        }
+        Trace("cnf-pf-debug") << "; child " << j << " " << child_base << " " << child_pol << " " << childPol[child_base] << std::endl;
+        std::map< Expr, 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];
+          if( childPol[child_base] ){
+            os_main << ProofManager::getLitName(lit) << " ";
+          }else{
+            os_main << "(not_not_intro _ " << ProofManager::getLitName(lit) << ") ";
+          }
+          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;
+        Expr 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< Expr, unsigned >::iterator itcic = childIndex.find( child_base );
+        if( itcic!=childIndex.end() ){
+          os << "(contra _ ";
+          prop::SatLiteral lit = (*clause)[itcic->second];
+          if( childPol[child_base] ){
+            os << os_main.str() << " " << ProofManager::getLitName(lit);
+          }else{
+            os << ProofManager::getLitName(lit) << " " << 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;
+      Expr 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;
+      Expr e_base = iatom.getKind()==kind::NOT ? iatom[0] : iatom;
+      bool e_pol = iatom.getKind()!=kind::NOT;
+      std::map< Expr, 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++ ){
+          Expr 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) << " " << os_main.str();
+          }else{
+            os << os_main.str() << " " << ProofManager::getLitName(lit);
+          }
+          os << ")";
+        }
+      }
+    }else if( base_assertion.getKind()==kind::XOR || base_assertion.getKind()==kind::IFF ){
+      //eliminate negation
+      int num_nots_2 = 0;
+      int num_nots_1 = 0;
+      Kind k;
+      if( !base_pol ){
+        if( base_assertion.getKind()==kind::IFF ){
+          num_nots_2 = 1;
+        }
+        k = kind::IFF;
+      }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++ ){
+        Expr 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< Expr, 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::IFF) ){
+              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) << ") ";
+        }else{
+          os_base_n << ProofManager::getLitName(lit1) << " ";
+        }
+        Assert( elimNum!=0 );
+        os_base_n << "(" << ( k==kind::IFF ? "iff" : "xor" ) << "_elim_" << elimNum << " _ _ ";
+        if( !base_pol ){
+          os_base_n << "(not_" << ( base_assertion.getKind()==kind::IFF ? "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) << ")";
+          }else{
+            os << ProofManager::getLitName(lit2);
+          }
+        }else{
+          os << ProofManager::getLitName(lit2) << " " << os_base_n.str();
+        }
+        os << ")";
+      }
+    }else if( base_assertion.getKind()==kind::ITE ){
+      std::map< unsigned, unsigned > appears;
+      std::map< unsigned, Expr > appears_expr;
+      unsigned appears_count = 0;
+      for( unsigned r=0; r<3; r++ ){
+        Expr child_base = base_assertion[r].getKind()==kind::NOT ? base_assertion[r][0] : base_assertion[r];
+        std::map< Expr, 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) << ") ";
+        }else{
+          os_main << ProofManager::getLitName(lit1) << " ";
+        }
+        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) << " " << os_main.str();
+        }else{
+          os << os_main.str() << " " << ProofManager::getLitName(lit2);
+        }
+        os << ")";
+      }
+    }else if( base_assertion.isConst() ){
+      bool pol = base_assertion==NodeManager::currentNM()->mkConst( true ).toExpr();
+      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 << ", proof rule = " << pr << 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) << "\n";
     paren << "))";
   }
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 459815e60..c1d245716 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -2,7 +2,7 @@
 /*! \file cnf_proof.h
  ** \verbatim
  ** Original author: Liana Hadarean
- ** Major contributors: Morgan Deters
+ ** Major contributors: Morgan Deters, Andrew Reynolds
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
@@ -50,11 +50,16 @@ public:
 };/* class CnfProof */
 
 class LFSCCnfProof : public CnfProof {
+  void printPreprocess(std::ostream& os, std::ostream& paren);
   void printInputClauses(std::ostream& os, std::ostream& paren);
   void printTheoryLemmas(std::ostream& os, std::ostream& paren);
   void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren);
   virtual void printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren);
 
+  Expr clauseToExpr( const prop::SatClause& clause,
+                     std::map< Expr, unsigned >& childIndex,
+                     std::map< Expr, bool >& childPol );
+ 
 public:
   LFSCCnfProof(CVC4::prop::CnfStream* cnfStream)
     : CnfProof(cnfStream)
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 87eded8e6..4bff66b92 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -47,7 +47,8 @@ ProofManager::ProofManager(ProofFormat format):
   d_theoryProof(NULL),
   d_fullProof(NULL),
   d_format(format),
-  d_deps()
+  d_deps(),
+  d_assertion_counter(1)
 {
 }
 
@@ -155,7 +156,9 @@ void ProofManager::traceDeps(TNode n) {
     std::vector<Node> deps = (*d_deps.find(n)).second;
     for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
       Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
-      traceDeps(*i);
+      if( !(*i).isNull() ){
+        traceDeps(*i);
+      }
     }
   }
 }
@@ -203,7 +206,7 @@ void ProofManager::addAssertion(Expr formula, bool inUnsatCore) {
 void ProofManager::addDependence(TNode n, TNode dep) {
   if(dep != n) {
     Debug("cores") << "dep: " << n << " : " << dep << std::endl;
-    if(d_deps.find(dep) == d_deps.end()) {
+    if( !dep.isNull() && d_deps.find(dep) == d_deps.end()) {
       Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl;
     }
     //Assert(d_deps.find(dep) != d_deps.end());
@@ -219,6 +222,116 @@ void ProofManager::printProof(std::ostream& os, TNode n) {
   // no proofs here yet
 }
 
+void ProofManager::setCnfDep( Expr child, Expr parent ) {
+  Debug("cores") << "CNF dep : " << child << " : " << parent << std::endl;
+  d_cnf_dep[child] = parent;
+}
+
+Expr ProofManager::getFormulaForClauseId( ClauseId id ) {
+  std::map< ClauseId, Expr >::const_iterator it = d_clause_id_to_assertion.find( id );
+  if( it!=d_clause_id_to_assertion.end() ){
+    return it->second;
+  }else{
+    Node ret;
+    return ret.toExpr();
+  }
+}
+
+ProofRule ProofManager::getProofRuleForClauseId( ClauseId id ) {
+  std::map< ClauseId, ProofRule >::const_iterator it = d_clause_id_to_rule.find( id );
+  if( it!=d_clause_id_to_rule.end() ){
+    return it->second;
+  }else{
+    return RULE_INVALID;
+  }
+}
+
+void ProofManager::setAssertion( Expr e ) {
+  d_assertion_to_id[e] = d_assertion_counter;
+  d_assertion_counter++;
+}
+
+// if this function returns true, writes to out a proof of e based on input assertions
+bool ProofManager::isInputAssertion( Expr e, std::ostream& out ) {
+  std::map< Expr, unsigned >::iterator itp = d_assertion_to_id.find( e );
+  if( itp==d_assertion_to_id.end() ){
+    //check if deduced by CNF
+    std::map< Expr, Expr >::iterator itd = d_cnf_dep.find( e );
+    if( itd!=d_cnf_dep.end() ){
+      Expr parent = itd->second;
+      //check if parent is an input assertion
+      std::stringstream out_parent;
+      if( isInputAssertion( parent, out_parent ) ){
+        if( parent.getKind()==kind::AND || ( parent.getKind()==kind::NOT && ( parent[0].getKind()==kind::IMPLIES || parent[0].getKind()==kind::OR ) ) ){
+          Expr parent_base = parent.getKind()==kind::NOT ? parent[0] : parent;
+          Expr 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++ ){
+            Expr 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 << "A" << itp->second;
+    return true;
+  }
+}
+
+void ProofManager::setRegisteringFormula( Node n, ProofRule proof_id ) {
+  d_registering_assertion = n;
+  d_registering_rule = proof_id;
+}
+
+void ProofManager::setRegisteredClauseId( ClauseId id ) {
+  Trace("cnf-pf-debug") << "set register clause id " << id << " " << d_registering_assertion << std::endl;
+  if( !d_registering_assertion.isNull() ){
+     d_clause_id_to_assertion[id] = d_registering_assertion.toExpr();
+     d_clause_id_to_rule[id] = d_registering_rule;
+     setRegisteringFormula( Node::null(), RULE_INVALID );
+  }
+}
+
 LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
   : d_satProof(sat)
   , d_cnfProof(cnf)
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index d60a3f6e3..43d6723fa 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Liana Hadarean
  ** Major contributors: Morgan Deters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2014  New York University and The University of Iowa
  ** See the file COPYING in the top-level source directory for licensing
@@ -85,12 +85,14 @@ enum ProofRule {
   RULE_TRUST,       /* trust without evidence (escape hatch until proofs are fully supported) */
   RULE_INVALID,     /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */
   RULE_CONFLICT,    /* re-construct as a conflict */
+  RULE_TSEITIN,     /* Tseitin CNF transformation */
 
   RULE_ARRAYS_EXT,  /* arrays, extensional */
   RULE_ARRAYS_ROW,  /* arrays, read-over-write */
 };/* enum ProofRules */
 
 class ProofManager {
+
   SatProof*    d_satProof;
   CnfProof*    d_cnfProof;
   TheoryProof* d_theoryProof;
@@ -114,6 +116,14 @@ class ProofManager {
   // trace dependences back to unsat core
   void traceDeps(TNode n);
 
+  Node d_registering_assertion;
+  ProofRule d_registering_rule;
+  std::map< ClauseId, Expr > d_clause_id_to_assertion;
+  std::map< ClauseId, ProofRule > d_clause_id_to_rule;
+  std::map< Expr, Expr > d_cnf_dep;
+  //LFSC number for assertions
+  unsigned d_assertion_counter;
+  std::map< Expr, unsigned > d_assertion_to_id;
 protected:
   LogicInfo d_logic;
 
@@ -139,6 +149,10 @@ public:
   typedef ExprSet::const_iterator assertions_iterator;
   typedef VarSet::const_iterator var_iterator;
 
+
+  __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction >::const_iterator begin_deps() const { return d_deps.begin(); }
+  __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction >::const_iterator end_deps() const { return d_deps.end(); }
+
   clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); }
   clause_iterator end_input_clauses() const { return d_inputClauses.end(); }
   size_t num_input_clauses() const { return d_inputClauses.size(); }
@@ -179,6 +193,21 @@ public:
   void setLogic(const LogicInfo& logic);
   const std::string getLogic() const { return d_logic.getLogicString(); }
 
+  
+  void setCnfDep( Expr child, Expr parent );
+  Expr getFormulaForClauseId( ClauseId id );
+  ProofRule getProofRuleForClauseId( ClauseId id );
+  unsigned getAssertionCounter() { return d_assertion_counter; }
+  void setAssertion( Expr e );
+  bool isInputAssertion( Expr e, std::ostream& out );
+
+public:  // AJR : FIXME this is hacky
+  //currently, to map between ClauseId and Expr, requires:
+  // (1) CnfStream::assertClause(...) to call setRegisteringFormula,
+  // (2) SatProof::registerClause(...)/registerUnitClause(...) to call setRegisteredClauseId.
+  //this is under the assumption that the first call at (2) is invoked for the clause corresponding to the Expr at (1).
+  void setRegisteringFormula( Node n, ProofRule proof_id );
+  void setRegisteredClauseId( ClauseId id );
 };/* class ProofManager */
 
 class LFSCProof : public Proof {
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index f7b9c4889..2c86d45a4 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -377,6 +377,7 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint6
     }
   }
   Debug("proof:sat:detailed") << "registerClause CRef:" << clause << " id:" << d_clauseId[clause] << " " << kind << " " << int32_t((proof_id >> 32) & 0xffffffff) << "\n";
+  ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] );
   return d_clauseId[clause];
 }
 
@@ -397,6 +398,7 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint6
     }
   }
   Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n";
+  ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] );
   return d_unitId[toInt(lit)];
 }
 
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 52989d722..6982509b1 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -188,7 +188,6 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
 }
 
 void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) {
-  unsigned counter = 0;
   ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
   ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
 
@@ -200,10 +199,12 @@ void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) {
 
   it = ProofManager::currentPM()->begin_assertions();
   for (; it != end; ++it) {
-    os << "(% A" << counter++ << " (th_holds ";
+    os << "(% A" << ProofManager::currentPM()->getAssertionCounter() << " (th_holds ";
     printTerm(*it,  os);
     os << ")\n";
     paren << ")";
+    //store map between assertion and counter
+    ProofManager::currentPM()->setAssertion( *it );
   }
 }