From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 10 Mar 2015 14:15:26 +0000 (+0100)
Subject: CNF proofs.  Infrastructure for preprocessing proofs.  Updates to smt.plf signature... 
X-Git-Tag: cvc5-1.0.0~6380
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=10df4ba0752eb23c76b9aa847e3ad116673a47b6;p=cvc5.git

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

diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf
index 942e17df0..62cdf3f94 100755
--- a/proofs/signatures/smt.plf
+++ b/proofs/signatures/smt.plf
@@ -135,6 +135,12 @@
   (! u2 (th_holds (or f1 f2))
     (th_holds f1))))))
 
+(declare not_or_elim
+  (! f1 formula
+  (! f2 formula
+  (! u2 (th_holds (not (or f1 f2)))
+    (th_holds (and (not f1) (not f2)))))))
+    
 ;; and elimination
 
 (declare and_elim_1
@@ -149,20 +155,12 @@
   (! u (th_holds (and f1 f2))
     (th_holds f2)))))
 
-;; not impl elimination
-
-(declare not_impl_elim_1
-  (! f1 formula
-  (! f2 formula
-  (! u (th_holds (not (impl f1 f2)))
-    (th_holds f1)))))
-
-(declare not_impl_elim_2
+(declare not_and_elim
   (! f1 formula
   (! f2 formula
-  (! u (th_holds (not (impl f1 f2)))
-    (th_holds (not f2))))))
-
+  (! u2 (th_holds (not (and f1 f2)))
+    (th_holds (or (not f1) (not f2)))))))
+    
 ;; impl elimination
 
 (declare impl_intro (! f1 formula
@@ -174,37 +172,54 @@
 (declare impl_elim
   (! f1 formula
   (! f2 formula
-  (! u1 (th_holds f1)
   (! u2 (th_holds (impl f1 f2))
-    (th_holds f2))))))
+    (th_holds (or (not f1) f2))))))
 
+(declare not_impl_elim
+  (! f1 formula
+  (! f2 formula
+  (! u (th_holds (not (impl f1 f2)))
+    (th_holds (and f1 (not f2)))))))
+    
 ;; iff elimination
 
 (declare iff_elim_1
   (! f1 formula
   (! f2 formula
   (! u1 (th_holds (iff f1 f2))
-    (th_holds (impl f1 f2))))))
+    (th_holds (or (not f1) f2))))))
 
 (declare iff_elim_2
   (! f1 formula
   (! f2 formula
   (! u1 (th_holds (iff f1 f2))
-    (th_holds (impl f2 f1))))))
+    (th_holds (or f1 (not f2)))))))
 
-(declare not_iff_elim_1
+(declare not_iff_elim
   (! f1 formula
   (! f2 formula
-  (! u1 (th_holds (not f1))
   (! u2 (th_holds (not (iff f1 f2)))
-    (th_holds f2))))))
+    (th_holds (iff f1 (not f2)))))))
+
+; xor elimination
 
-(declare not_iff_elim_2
+(declare xor_elim_1
   (! f1 formula
   (! f2 formula
-  (! u1 (th_holds f1)
-  (! u2 (th_holds (not (iff f1 f2)))
-    (th_holds (not f2)))))))
+  (! u1 (th_holds (xor f1 f2))
+    (th_holds (or (not f1) (not f2)))))))
+
+(declare xor_elim_2
+  (! f1 formula
+  (! f2 formula
+  (! u1 (th_holds (xor f1 f2))
+    (th_holds (or f1 f2))))))
+
+(declare not_xor_elim
+  (! f1 formula
+  (! f2 formula
+  (! u2 (th_holds (not (xor f1 f2)))
+    (th_holds (iff f1 f2))))))
 
 ;; ite elimination
 
@@ -212,65 +227,43 @@
   (! a formula
   (! b formula
   (! c formula
-  (! u1 (th_holds a)
   (! u2 (th_holds (ifte a b c))
-    (th_holds b)))))))
+    (th_holds (or (not a) b)))))))
 
 (declare ite_elim_2
   (! a formula
   (! b formula
   (! c formula
-  (! u1 (th_holds (not a))
   (! u2 (th_holds (ifte a b c))
-    (th_holds c)))))))
+    (th_holds (or a c)))))))
 
 (declare ite_elim_3
   (! a formula
   (! b formula
   (! c formula
-  (! u1 (th_holds (not b))
   (! u2 (th_holds (ifte a b c))
-    (th_holds c)))))))
-
-(declare ite_elim_2n
-  (! a formula
-  (! b formula
-  (! c formula
-  (! u1 (th_holds a)
-  (! u2 (th_holds (ifte (not a) b c))
-    (th_holds c)))))))
+    (th_holds (or b c)))))))
 
 (declare not_ite_elim_1
   (! a formula
   (! b formula
   (! c formula
-  (! u1 (th_holds a)
   (! u2 (th_holds (not (ifte a b c)))
-    (th_holds (not b))))))))
+    (th_holds (or (not a) (not b))))))))
 
 (declare not_ite_elim_2
   (! a formula
   (! b formula
   (! c formula
-  (! u1 (th_holds (not a))
   (! u2 (th_holds (not (ifte a b c)))
-    (th_holds (not c))))))))
+    (th_holds (or a (not c))))))))
 
 (declare not_ite_elim_3
   (! a formula
   (! b formula
   (! c formula
-  (! u1 (th_holds b)
   (! u2 (th_holds (not (ifte a b c)))
-    (th_holds (not c))))))))
-
-(declare not_ite_elim_2n
-  (! a formula
-  (! b formula
-  (! c formula
-  (! u1 (th_holds a)
-  (! u2 (th_holds (not (ifte (not a) b c)))
-    (th_holds (not c))))))))
+    (th_holds (or (not b) (not c))))))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;
diff --git a/proofs/signatures/th_base.plf b/proofs/signatures/th_base.plf
index 977409b6a..9dd950b5b 100755
--- a/proofs/signatures/th_base.plf
+++ b/proofs/signatures/th_base.plf
@@ -23,6 +23,7 @@
 ; inference rules :
 
 (declare trust (th_holds false))	; temporary
+(declare trust_f (! f formula (th_holds f)))  ; temporary
 
 (declare refl
   (! s sort
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 );
   }
 }
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index fd30cd997..c8d86c73d 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: Morgan Deters, Dejan Jovanovic
- ** Minor contributors (to current version): Kshitij Bansal, Liana Hadarean, Christopher L. Conway
+ ** Minor contributors (to current version): Kshitij Bansal, Liana Hadarean, Christopher L. Conway, 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
@@ -61,8 +61,8 @@ TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, c
   CnfStream(satSolver, registrar, context, fullLitToNodeMap) {
 }
 
-void CnfStream::assertClause(TNode node, SatClause& c) {
-  Debug("cnf") << "Inserting into stream " << c << endl;
+void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) {
+  Debug("cnf") << "Inserting into stream " << c << " node = " << node << ", proof id = " << proof_id << endl;
   if(Dump.isOn("clauses")) {
     if(c.size() == 1) {
       Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr()));
@@ -76,28 +76,31 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
       Dump("clauses") << AssertCommand(Expr(n.toExpr()));
     }
   }
+  //store map between clause and original formula
+  PROOF(ProofManager::currentPM()->setRegisteringFormula( node, proof_id ); );
   d_satSolver->addClause(c, d_removable, d_proofId);
+  PROOF(ProofManager::currentPM()->setRegisteringFormula( Node::null(), RULE_INVALID ); );
 }
 
-void CnfStream::assertClause(TNode node, SatLiteral a) {
+void CnfStream::assertClause(TNode node, SatLiteral a, ProofRule proof_id) {
   SatClause clause(1);
   clause[0] = a;
-  assertClause(node, clause);
+  assertClause(node, clause, proof_id);
 }
 
-void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) {
+void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id) {
   SatClause clause(2);
   clause[0] = a;
   clause[1] = b;
-  assertClause(node, clause);
+  assertClause(node, clause, proof_id);
 }
 
-void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) {
+void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id) {
   SatClause clause(3);
   clause[0] = a;
   clause[1] = b;
   clause[2] = c;
-  assertClause(node, clause);
+  assertClause(node, clause, proof_id);
 }
 
 bool CnfStream::hasLiteral(TNode n) const {
@@ -260,10 +263,10 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
 
   SatLiteral xorLit = newLiteral(xorNode);
 
-  assertClause(xorNode, a, b, ~xorLit);
-  assertClause(xorNode, ~a, ~b, ~xorLit);
-  assertClause(xorNode, a, ~b, xorLit);
-  assertClause(xorNode, ~a, b, xorLit);
+  assertClause(xorNode.negate(), a, b, ~xorLit, RULE_TSEITIN);
+  assertClause(xorNode.negate(), ~a, ~b, ~xorLit, RULE_TSEITIN);
+  assertClause(xorNode, a, ~b, xorLit, RULE_TSEITIN);
+  assertClause(xorNode, ~a, b, xorLit, RULE_TSEITIN);
 
   return xorLit;
 }
@@ -292,14 +295,14 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
   // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
   // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
   for(unsigned i = 0; i < n_children; ++i) {
-    assertClause(orNode, orLit, ~clause[i]);
+    assertClause(orNode, orLit, ~clause[i], RULE_TSEITIN);
   }
 
   // lit -> (a_1 | a_2 | a_3 | ... | a_n)
   // ~lit | a_1 | a_2 | a_3 | ... | a_n
   clause[n_children] = ~orLit;
   // This needs to go last, as the clause might get modified by the SAT solver
-  assertClause(orNode, clause);
+  assertClause(orNode.negate(), clause, RULE_TSEITIN);
 
   // Return the literal
   return orLit;
@@ -329,7 +332,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
   // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
   // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
   for(unsigned i = 0; i < n_children; ++i) {
-    assertClause(andNode, ~andLit, ~clause[i]);
+    assertClause(andNode.negate(), ~andLit, ~clause[i], RULE_TSEITIN);
   }
 
   // lit <- (a_1 & a_2 & a_3 & ... a_n)
@@ -337,7 +340,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
   // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
   clause[n_children] = andLit;
   // This needs to go last, as the clause might get modified by the SAT solver
-  assertClause(andNode, clause);
+  assertClause(andNode, clause, RULE_TSEITIN);
 
   return andLit;
 }
@@ -356,13 +359,13 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
 
   // lit -> (a->b)
   // ~lit | ~ a | b
-  assertClause(impliesNode, ~impliesLit, ~a, b);
+  assertClause(impliesNode.negate(), ~impliesLit, ~a, b, RULE_TSEITIN);
 
   // (a->b) -> lit
   // ~(~a | b) | lit
   // (a | l) & (~b | l)
-  assertClause(impliesNode, a, impliesLit);
-  assertClause(impliesNode, ~b, impliesLit);
+  assertClause(impliesNode, a, impliesLit, RULE_TSEITIN);
+  assertClause(impliesNode, ~b, impliesLit, RULE_TSEITIN);
 
   return impliesLit;
 }
@@ -385,16 +388,16 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
   // lit -> ((a-> b) & (b->a))
   // ~lit | ((~a | b) & (~b | a))
   // (~a | b | ~lit) & (~b | a | ~lit)
-  assertClause(iffNode, ~a, b, ~iffLit);
-  assertClause(iffNode, a, ~b, ~iffLit);
+  assertClause(iffNode.negate(), ~a, b, ~iffLit, RULE_TSEITIN);
+  assertClause(iffNode.negate(), a, ~b, ~iffLit, RULE_TSEITIN);
 
   // (a<->b) -> lit
   // ~((a & b) | (~a & ~b)) | lit
   // (~(a & b)) & (~(~a & ~b)) | lit
   // ((~a | ~b) & (a | b)) | lit
   // (~a | ~b | lit) & (a | b | lit)
-  assertClause(iffNode, ~a, ~b, iffLit);
-  assertClause(iffNode, a, b, iffLit);
+  assertClause(iffNode, ~a, ~b, iffLit, RULE_TSEITIN);
+  assertClause(iffNode, a, b, iffLit, RULE_TSEITIN);
 
   return iffLit;
 }
@@ -429,9 +432,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   // lit -> (t | e) & (b -> t) & (!b -> e)
   // lit -> (t | e) & (!b | t) & (b | e)
   // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
-  assertClause(iteNode, ~iteLit, thenLit, elseLit);
-  assertClause(iteNode, ~iteLit, ~condLit, thenLit);
-  assertClause(iteNode, ~iteLit, condLit, elseLit);
+  assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit, RULE_TSEITIN);
+  assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit, RULE_TSEITIN);
+  assertClause(iteNode.negate(), ~iteLit, condLit, elseLit, RULE_TSEITIN);
 
   // If ITE is false then one of the branches is false and the condition
   // implies which one
@@ -439,9 +442,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
   // !lit -> (!t | !e) & (!b | !t) & (b | !e)
   // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
-  assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
-  assertClause(iteNode, iteLit, ~condLit, ~thenLit);
-  assertClause(iteNode, iteLit, condLit, ~elseLit);
+  assertClause(iteNode, iteLit, ~thenLit, ~elseLit, RULE_TSEITIN);
+  assertClause(iteNode, iteLit, ~condLit, ~thenLit, RULE_TSEITIN);
+  assertClause(iteNode, iteLit, condLit, ~elseLit, RULE_TSEITIN);
 
   return iteLit;
 }
@@ -506,13 +509,14 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
   else return ~nodeLit;
 }
 
-void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id) {
   Assert(node.getKind() == AND);
   if (!negated) {
     // If the node is a conjunction, we handle each conjunct separately
     for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
         conjunct != node_end; ++conjunct ) {
-      convertAndAssert(*conjunct, false);
+      PROOF(ProofManager::currentPM()->setCnfDep( (*conjunct).toExpr(), node.toExpr() ) );
+      convertAndAssert(*conjunct, false, proof_id);
     }
   } else {
     // If the node is a disjunction, we construct a clause and assert it
@@ -524,11 +528,11 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
       clause[i] = toCNF(*disjunct, true);
     }
     Assert(disjunct == node.end());
-    assertClause(node, clause);
+    assertClause(node.negate(), clause, proof_id);
   }
 }
 
-void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated, ProofRule proof_id) {
   Assert(node.getKind() == OR);
   if (!negated) {
     // If the node is a disjunction, we construct a clause and assert it
@@ -540,17 +544,18 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
       clause[i] = toCNF(*disjunct, false);
     }
     Assert(disjunct == node.end());
-    assertClause(node, clause);
+    assertClause(node, clause, proof_id);
   } else {
     // If the node is a conjunction, we handle each conjunct separately
     for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
         conjunct != node_end; ++conjunct ) {
-      convertAndAssert(*conjunct, true);
+      PROOF(ProofManager::currentPM()->setCnfDep( (*conjunct).negate().toExpr(), node.negate().toExpr() ) );
+      convertAndAssert(*conjunct, true, proof_id);
     }
   }
 }
 
-void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated, ProofRule proof_id) {
   if (!negated) {
     // p XOR q
     SatLiteral p = toCNF(node[0], false);
@@ -559,11 +564,11 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
     SatClause clause1(2);
     clause1[0] = ~p;
     clause1[1] = ~q;
-    assertClause(node, clause1);
+    assertClause(node, clause1, proof_id);
     SatClause clause2(2);
     clause2[0] = p;
     clause2[1] = q;
-    assertClause(node, clause2);
+    assertClause(node, clause2, proof_id);
   } else {
     // !(p XOR q) is the same as p <=> q
     SatLiteral p = toCNF(node[0], false);
@@ -572,15 +577,15 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
     SatClause clause1(2);
     clause1[0] = ~p;
     clause1[1] = q;
-    assertClause(node, clause1);
+    assertClause(node.negate(), clause1, proof_id);
     SatClause clause2(2);
     clause2[0] = p;
     clause2[1] = ~q;
-    assertClause(node, clause2);
+    assertClause(node.negate(), clause2, proof_id);
   }
 }
 
-void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated, ProofRule proof_id) {
   if (!negated) {
     // p <=> q
     SatLiteral p = toCNF(node[0], false);
@@ -589,11 +594,11 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
     SatClause clause1(2);
     clause1[0] = ~p;
     clause1[1] = q;
-    assertClause(node, clause1);
+    assertClause(node, clause1, proof_id);
     SatClause clause2(2);
     clause2[0] = p;
     clause2[1] = ~q;
-    assertClause(node, clause2);
+    assertClause(node, clause2, proof_id);
   } else {
     // !(p <=> q) is the same as p XOR q
     SatLiteral p = toCNF(node[0], false);
@@ -602,15 +607,15 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
     SatClause clause1(2);
     clause1[0] = ~p;
     clause1[1] = ~q;
-    assertClause(node, clause1);
+    assertClause(node.negate(), clause1, proof_id);
     SatClause clause2(2);
     clause2[0] = p;
     clause2[1] = q;
-    assertClause(node, clause2);
+    assertClause(node.negate(), clause2, proof_id);
   }
 }
 
-void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id) {
   if (!negated) {
     // p => q
     SatLiteral p = toCNF(node[0], false);
@@ -619,29 +624,35 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
     SatClause clause(2);
     clause[0] = ~p;
     clause[1] = q;
-    assertClause(node, clause);
+    assertClause(node, clause, proof_id);
   } else {// Construct the
+    PROOF(ProofManager::currentPM()->setCnfDep( node[0].toExpr(), node.negate().toExpr() ) );
+    PROOF(ProofManager::currentPM()->setCnfDep( node[1].negate().toExpr(), node.negate().toExpr() ) );
     // !(p => q) is the same as (p && ~q)
-    convertAndAssert(node[0], false);
-    convertAndAssert(node[1], true);
+    convertAndAssert(node[0], false, proof_id);
+    convertAndAssert(node[1], true, proof_id);
   }
 }
 
-void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated, ProofRule proof_id) {
   // ITE(p, q, r)
   SatLiteral p = toCNF(node[0], false);
   SatLiteral q = toCNF(node[1], negated);
   SatLiteral r = toCNF(node[2], negated);
   // Construct the clauses:
   // (p => q) and (!p => r)
+  Node nnode = node;
+  if( negated ){
+    nnode = node.negate();
+  }
   SatClause clause1(2);
   clause1[0] = ~p;
   clause1[1] = q;
-  assertClause(node, clause1);
+  assertClause(nnode, clause1, proof_id);
   SatClause clause2(2);
   clause2[0] = p;
   clause2[1] = r;
-  assertClause(node, clause2);
+  assertClause(nnode, clause2, proof_id);
 }
 
 // At the top level we must ensure that all clauses that are asserted are
@@ -661,10 +672,10 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated
     // We aren't producing proofs or unsat cores; use an invalid proof id.
     d_proofId = uint64_t(-1);
   }
-  convertAndAssert(node, negated);
+  convertAndAssert(node, negated, proof_id);
 }
 
-void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
+void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proof_id) {
   Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
   if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
@@ -675,29 +686,35 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
 
   switch(node.getKind()) {
   case AND:
-    convertAndAssertAnd(node, negated);
+    convertAndAssertAnd(node, negated, proof_id);
     break;
   case OR:
-    convertAndAssertOr(node, negated);
+    convertAndAssertOr(node, negated, proof_id);
     break;
   case IFF:
-    convertAndAssertIff(node, negated);
+    convertAndAssertIff(node, negated, proof_id);
     break;
   case XOR:
-    convertAndAssertXor(node, negated);
+    convertAndAssertXor(node, negated, proof_id);
     break;
   case IMPLIES:
-    convertAndAssertImplies(node, negated);
+    convertAndAssertImplies(node, negated, proof_id);
     break;
   case ITE:
-    convertAndAssertIte(node, negated);
+    convertAndAssertIte(node, negated, proof_id);
     break;
   case NOT:
-    convertAndAssert(node[0], !negated);
+    convertAndAssert(node[0], !negated, proof_id);
     break;
   default:
+  {
+    Node nnode = node;
+    if( negated ){
+      nnode = node.negate();
+    }
     // Atoms
-    assertClause(node, toCNF(node, negated));
+    assertClause(nnode, toCNF(node, negated), proof_id);
+  }
     break;
   }
 }
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index b22290ae4..d5d01d126 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: Tim King
  ** Major contributors: Morgan Deters, Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway
+ ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway, 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
@@ -133,14 +133,14 @@ protected:
    * @param node the node giving rise to this clause
    * @param clause the clause to assert
    */
-  void assertClause(TNode node, SatClause& clause);
+  void assertClause(TNode node, SatClause& clause, ProofRule proof_id);
 
   /**
    * Asserts the unit clause to the sat solver.
    * @param node the node giving rise to this clause
    * @param a the unit literal of the clause
    */
-  void assertClause(TNode node, SatLiteral a);
+  void assertClause(TNode node, SatLiteral a, ProofRule proof_id);
 
   /**
    * Asserts the binary clause to the sat solver.
@@ -148,7 +148,7 @@ protected:
    * @param a the first literal in the clause
    * @param b the second literal in the clause
    */
-  void assertClause(TNode node, SatLiteral a, SatLiteral b);
+  void assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id);
 
   /**
    * Asserts the ternary clause to the sat solver.
@@ -157,7 +157,7 @@ protected:
    * @param b the second literal in the clause
    * @param c the thirs literal in the clause
    */
-  void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
+  void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id);
 
   /**
    * Acquires a new variable from the SAT solver to represent the node
@@ -298,7 +298,7 @@ private:
   /**
    * Same as above, except that removable is remembered.
    */
-  void convertAndAssert(TNode node, bool negated);
+  void convertAndAssert(TNode node, bool negated, ProofRule proof_id);
 
   // Each of these formulas handles takes care of a Node of each Kind.
   //
@@ -318,12 +318,12 @@ private:
   SatLiteral handleAnd(TNode node);
   SatLiteral handleOr(TNode node);
 
-  void convertAndAssertAnd(TNode node, bool negated);
-  void convertAndAssertOr(TNode node, bool negated);
-  void convertAndAssertXor(TNode node, bool negated);
-  void convertAndAssertIff(TNode node, bool negated);
-  void convertAndAssertImplies(TNode node, bool negated);
-  void convertAndAssertIte(TNode node, bool negated);
+  void convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id);
+  void convertAndAssertOr(TNode node, bool negated, ProofRule proof_id);
+  void convertAndAssertXor(TNode node, bool negated, ProofRule proof_id);
+  void convertAndAssertIff(TNode node, bool negated, ProofRule proof_id);
+  void convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id);
+  void convertAndAssertIte(TNode node, bool negated, ProofRule proof_id);
 
   /**
    * Transforms the node into CNF recursively.
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index eca8c9d17..eb7792d2c 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -162,7 +162,6 @@ public:
     PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); );
     d_nodes[i] = n;
   }
-
 };/* class AssertionPipeline */
 
 struct SmtEngineStatistics {
@@ -572,8 +571,9 @@ public:
    * formula might be pushed out to the propositional layer
    * immediately, or it might be simplified and kept, or it might not
    * even be simplified.
+   * the 2nd and 3rd arguments added for bookkeeping for proofs
    */
-  void addFormula(TNode n)
+  void addFormula(TNode n, bool inUnsatCore, bool inInput = true)
     throw(TypeCheckingException, LogicException);
 
   /**
@@ -1930,7 +1930,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     Node falseNode = NodeManager::currentNM()->mkConst<bool>(false);
     Assert(!options::unsatCores());
     d_assertions.clear();
-    d_assertions.push_back(falseNode);
+    addFormula(falseNode, false, false);
     d_propagatorNeedsFinish = true;
     return false;
   }
@@ -1969,7 +1969,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
                           << d_nonClausalLearnedLiterals[i] << endl;
         Assert(!options::unsatCores());
         d_assertions.clear();
-        d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+        addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
         d_propagatorNeedsFinish = true;
         return false;
       }
@@ -2005,7 +2005,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
                           << learnedLiteral << endl;
         Assert(!options::unsatCores());
         d_assertions.clear();
-        d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+        addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
         d_propagatorNeedsFinish = true;
         return false;
       default:
@@ -2031,7 +2031,7 @@ bool SmtEnginePrivate::nonClausalSimplify() {
           // if (!equations.empty()) {
           //   Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
           //   d_assertions.clear();
-          //   d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+          //   addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false);
           //   return;
           // }
           // d_topLevelSubstitutions.simplifyRHS(constantPropagations);
@@ -2642,7 +2642,7 @@ void SmtEnginePrivate::doMiplibTrick() {
               Node newVar = nm->mkSkolem(ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME);
               Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero));
               Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
-              d_assertions.push_back(Rewriter::rewrite(geq.andNode(leq)));
+              addFormula(Rewriter::rewrite(geq.andNode(leq)), false, false);
               SubstitutionMap nullMap(&d_fakeContext);
               Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
               status = d_smt.d_theoryEngine->solve(geq, nullMap);
@@ -2693,7 +2693,7 @@ void SmtEnginePrivate::doMiplibTrick() {
           }
           newAssertion = Rewriter::rewrite(newAssertion);
           Debug("miplib") << "  " << newAssertion << endl;
-          d_assertions.push_back(newAssertion);
+          addFormula(newAssertion, false, false);
           Debug("miplib") << "  assertions to remove: " << endl;
           for(vector<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) {
             Debug("miplib") << "    " << *k << endl;
@@ -3417,7 +3417,7 @@ void SmtEnginePrivate::processAssertions() {
   d_iteSkolemMap.clear();
 }
 
-void SmtEnginePrivate::addFormula(TNode n)
+void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)
   throw(TypeCheckingException, LogicException) {
 
   if (n == d_true) {
@@ -3425,7 +3425,17 @@ void SmtEnginePrivate::addFormula(TNode n)
     return;
   }
 
-  Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl;
+  Trace("smt") << "SmtEnginePrivate::addFormula(" << n << "), inUnsatCore = " << inUnsatCore << ", inInput = " << inInput << endl;
+  // Give it to proof manager
+  PROOF( 
+    if( inInput ){
+      // n is an input assertion
+      ProofManager::currentPM()->addAssertion(n.toExpr(), inUnsatCore); 
+    }else{
+      // n is the result of an unknown preprocessing step, add it to dependency map to null
+      ProofManager::currentPM()->addDependence(n, Node::null());
+    }
+  );
 
   // Add the normalized formula to the queue
   d_assertions.push_back(n);
@@ -3465,8 +3475,6 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
       e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
       // Ensure expr is type-checked at this point.
       ensureBoolean(e);
-      // Give it to proof manager
-      PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); );
     }
 
     // check to see if a postsolve() is pending
@@ -3487,7 +3495,7 @@ Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingE
       if(d_assertionList != NULL) {
         d_assertionList->push_back(e);
       }
-      d_private->addFormula(e.getNode());
+      d_private->addFormula(e.getNode(), inUnsatCore);
     }
 
     Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
@@ -3553,8 +3561,6 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce
   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
   // Ensure that the expression is type-checked at this point, and Boolean
   ensureBoolean(e);
-  // Give it to proof manager
-  PROOF( ProofManager::currentPM()->addAssertion(e.notExpr(), inUnsatCore); );
 
   // check to see if a postsolve() is pending
   if(d_needPostsolve) {
@@ -3573,7 +3579,7 @@ Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingExce
   if(d_assertionList != NULL) {
     d_assertionList->push_back(e.notExpr());
   }
-  d_private->addFormula(e.getNode().notNode());
+  d_private->addFormula(e.getNode().notNode(), inUnsatCore);
 
   // Run the check
   Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
@@ -3625,9 +3631,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
-
-  PROOF( ProofManager::currentPM()->addAssertion(ex, inUnsatCore); );
-
+  
   Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
 
   // Substitute out any abstract values in ex
@@ -3637,7 +3641,7 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec
   if(d_assertionList != NULL) {
     d_assertionList->push_back(e);
   }
-  d_private->addFormula(e.getNode());
+  d_private->addFormula(e.getNode(), inUnsatCore);
   return quickCheck().asValidityResult();
 }/* SmtEngine::assertFormula() */
 
diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am
index da992286e..a8e7b6a8e 100644
--- a/test/regress/regress0/uf/Makefile.am
+++ b/test/regress/regress0/uf/Makefile.am
@@ -45,7 +45,10 @@ TESTS =	\
 	simple.02.cvc \
 	simple.03.cvc \
 	simple.04.cvc \
-	proof00.smt2
+	proof00.smt2 \
+	cnf-iff.smt2 \
+	cnf-iff-base.smt2 \
+	cnf-ite.smt2
 
 EXTRA_DIST = $(TESTS) \
 	mkpidgeon
diff --git a/test/regress/regress0/uf/cnf-iff-base.smt2 b/test/regress/regress0/uf/cnf-iff-base.smt2
new file mode 100644
index 000000000..9c538de6c
--- /dev/null
+++ b/test/regress/regress0/uf/cnf-iff-base.smt2
@@ -0,0 +1,16 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort U 0)
+
+(declare-fun f (U) U)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+
+(assert (= (not (= (f a) d)) (not (= d (f b)))))
+
+(assert (or (not (= (f a) d)) (not (= d (f b)))))
+(assert (or (= (f a) d) (= d (f b))))
+
+(check-sat)
diff --git a/test/regress/regress0/uf/cnf-iff.smt2 b/test/regress/regress0/uf/cnf-iff.smt2
new file mode 100644
index 000000000..03377005c
--- /dev/null
+++ b/test/regress/regress0/uf/cnf-iff.smt2
@@ -0,0 +1,38 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort U 0)
+
+(declare-fun f (U) U)
+(declare-fun g (U) U)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(declare-fun e () U)
+(declare-fun h () U)
+(declare-fun i () U)
+
+(assert (or 
+(= a c)
+(= h c)
+(not (= h d))
+(not (= h e))
+(= h i)
+(= (= (f a) d) (= d (f b)))
+(= (not (= (f a) d)) (not (= d (f b))))
+(not (= (not (= d (f b))) (= (f a) d)))
+(not (= (= d (f b)) (not (= (f a) d))))
+(xor (= (f a) d) (not (= d (f b))))
+(xor (not (= (f a) d)) (= d (f b)))
+(not (xor (= (f a) d) (= d (f b))))
+(not (xor (not (= (f a) d)) (not (= d (f b)))))
+))
+(assert (not (= h i)))
+(assert (or (not (= (f a) d)) (not (= d (f b)))))
+(assert (or (= (f a) d) (= d (f b))))
+(assert (and (not (= b e)) (not (= c a))))
+(assert (and (= h e) (not (= b e))))
+
+(assert (not (or (= b h) (= c h))))
+(assert (not (or (= b h) (not (= d h)))))
+(check-sat)
diff --git a/test/regress/regress0/uf/cnf-ite.smt2 b/test/regress/regress0/uf/cnf-ite.smt2
new file mode 100644
index 000000000..851eb45aa
--- /dev/null
+++ b/test/regress/regress0/uf/cnf-ite.smt2
@@ -0,0 +1,35 @@
+; COMMAND-LINE: --simplification=none
+; EXPECT: unsat
+
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort U 0)
+
+(declare-fun f (U) U)
+(declare-fun g (U) U)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(declare-fun e () U)
+(declare-fun h () U)
+(declare-fun i () U)
+
+(assert (or 
+(ite (= (f a) d) (not (= d (f b))) (= a c))
+(ite (not (= (f a) d)) (= d e) (not (= d (f b))))
+(not (ite (not (= (f a) d)) (= d e) (= d (f b))))
+(not (ite (= (f a) d) (= d (f b)) (= a c)))
+(ite (not (= (f a) e)) (= e (f b)) (= a c))
+(ite (= (f a) e) (= e e) (= e (f b)))
+(not (ite (= (f a) e) (= e e) (not (= e (f b)))))
+(not (ite (not (= (f a) e)) (not (= e (f b))) (= a c)))
+(= a b)
+))
+
+(assert (and (= (f a) d) (= d (f b))))
+(assert (and (not (= (f a) e)) (not (= e (f b)))))
+
+(assert (not (= a b)))
+
+(check-sat)