Unsat core infrastruture and API (SMT-LIB compliance to come).

14 files changed, 123 insertions, 70 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 2121d7366..498b31ce5 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -5,7 +5,7 @@
  ** Major contributors:
  ** Minor contributors (to current version):
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -45,7 +45,7 @@ void BVMinisatSatSolver::setNotify(Notify* notify) {
   d_minisat->setNotify(d_minisatNotify);
 }
 
-void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) {
+void BVMinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) {
   Debug("sat::minisat") << "Add clause " << clause <<"\n";
   BVMinisat::vec<BVMinisat::Lit> minisat_clause;
   toMinisatClause(clause, minisat_clause);
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 0101c5d62..04f21e761 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -5,7 +5,7 @@
  ** Major contributors:
  ** Minor contributors (to current version):
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -76,7 +76,7 @@ public:
 
   void setNotify(Notify* notify);
 
-  void addClause(SatClause& clause, bool removable);
+  void addClause(SatClause& clause, bool removable, uint64_t proof_id);
 
   SatValue propagate();
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index e0697735f..0d133aa13 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -44,7 +44,6 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace prop {
 
-
 CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) :
   d_satSolver(satSolver),
   d_booleanVariables(context),
@@ -52,6 +51,7 @@ CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Contex
   d_literalToNodeMap(context),
   d_fullLitToNodeMap(fullLitToNodeMap),
   d_registrar(registrar),
+  d_assertionTable(context),
   d_removable(false) {
 }
 
@@ -74,7 +74,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
       Dump("clauses") << AssertCommand(Expr(n.toExpr()));
     }
   }
-  d_satSolver->addClause(c, d_removable);
+  d_satSolver->addClause(c, d_removable, d_proofId);
 }
 
 void CnfStream::assertClause(TNode node, SatLiteral a) {
@@ -104,9 +104,9 @@ bool CnfStream::hasLiteral(TNode n) const {
 }
 
 void TseitinCnfStream::ensureLiteral(TNode n) {
-
-  // These are not removable
+  // These are not removable and have no proof ID
   d_removable = false;
+  d_proofId = uint64_t(-1);
 
   Debug("cnf") << "ensureLiteral(" << n << ")" << endl;
   if(hasLiteral(n)) {
@@ -188,9 +188,12 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister
 
   // If a theory literal, we pre-register it
   if (preRegister) {
-    bool backup = d_removable;
+    // In case we are re-entered due to lemmas, save our state
+    bool backupRemovable = d_removable;
+    uint64_t backupProofId= d_proofId;
     d_registrar->preRegister(node);
-    d_removable = backup;
+    d_removable = backupRemovable;
+    d_proofId = backupProofId;
   }
 
   // Here, you can have it
@@ -642,9 +645,20 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
 // At the top level we must ensure that all clauses that are asserted are
 // not unit, except for the direct assertions. This allows us to remove the
 // clauses later when they are not needed anymore (lemmas for example).
-void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated) {
+void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from) {
   Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl;
   d_removable = removable;
+  if(options::proof() || options::unsatCores()) {
+    // Encode the assertion ID in the proof_id to store with generated clauses.
+    uint64_t assertionTableIndex = d_assertionTable.size();
+    Assert((uint64_t(proof_id) & 0xffffffff00000000) == 0 && (assertionTableIndex & 0xffffffff00000000) == 0, "proof_id/table_index collision");
+    d_proofId = assertionTableIndex | (uint64_t(proof_id) << 32);
+    d_assertionTable.push_back(from.isNull() ? node : from);
+    Debug("cores") << "cnf ix " << assertionTableIndex << " asst " << node << "  proof_id " << proof_id << " from " << from << endl;
+  } else {
+    // We aren't producing proofs or unsat cores; use an invalid proof id.
+    d_proofId = uint64_t(-1);
+  }
   convertAndAssert(node, negated);
 }
 
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 266362ef5..b76051279 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -28,6 +28,7 @@
 #include "expr/node.h"
 #include "prop/theory_proxy.h"
 #include "prop/registrar.h"
+#include "proof/proof_manager.h"
 #include "context/cdlist.h"
 #include "context/cdinsert_hashmap.h"
 
@@ -36,7 +37,6 @@
 namespace CVC4 {
 namespace prop {
 
-
 class PropEngine;
 
 /**
@@ -77,6 +77,9 @@ protected:
   /** The "registrar" for pre-registration of terms */
   Registrar* d_registrar;
 
+  /** A table of assertions, used for regenerating proofs. */
+  context::CDList<Node> d_assertionTable;
+
   /**
    * How many literals were already mapped at the top-level when we
    * tried to convertAndAssert() something.  This
@@ -104,10 +107,18 @@ protected:
   }
 
   /**
+   * A reference into the assertion table, used to map clauses back to
+   * their "original" input assertion/lemma.  This variable is manipulated
+   * by the top-level convertAndAssert().  This is needed in proofs-enabled
+   * runs, to justify where the SAT solver's clauses came from.
+   */
+  uint64_t d_proofId;
+
+  /**
    * Are we asserting a removable clause (true) or a permanent clause (false).
    * This is set at the beginning of convertAndAssert so that it doesn't
-   * need to be passed on over the stack. Only pure clauses  can be asserted as
-   * removable.
+   * need to be passed on over the stack.  Only pure clauses can be asserted
+   * as removable.
    */
   bool d_removable;
 
@@ -190,7 +201,7 @@ public:
    * @param removable whether the sat solver can choose to remove the clauses
    * @param negated whether we are asserting the node negated
    */
-  virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0;
+  virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0;
 
   /**
    * Get the node that is represented by the given SatLiteral.
@@ -223,6 +234,13 @@ public:
   SatLiteral getLiteral(TNode node);
 
   /**
+   * Get the assertion with a given ID.  (Used for reconstructing proofs.)
+   */
+  TNode getAssertion(uint64_t id) {
+    return d_assertionTable[id];
+  }
+
+  /**
    * Returns the Boolean variables from the input problem.
    */
   void getBooleanVariables(std::vector<TNode>& outputVariables) const;
@@ -258,7 +276,7 @@ public:
    * @param removable is this something that can be erased
    * @param negated true if negated
    */
-  void convertAndAssert(TNode node, bool removable, bool negated);
+  void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null());
 
   /**
    * Constructs the stream to use the given sat solver.
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b0d710d66..5403b992e 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -135,8 +135,8 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context,
   // Assert the constants
   uncheckedEnqueue(mkLit(varTrue, false));
   uncheckedEnqueue(mkLit(varFalse, true));
-  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT); )
-  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT); )
+  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT, uint64_t(-1)); )
+  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT, uint64_t(-1)); )
 }
 
 
@@ -263,7 +263,7 @@ CRef Solver::reason(Var x) {
 
     // Construct the reason
     CRef real_reason = ca.alloc(explLevel, explanation, true);
-    PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); );
+    PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA, (uint64_t(RULE_CONFLICT) << 32)); );
     vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
     clauses_removable.push(real_reason);
     attachClause(real_reason);
@@ -271,7 +271,7 @@ CRef Solver::reason(Var x) {
     return real_reason;
 }
 
-bool Solver::addClause_(vec<Lit>& ps, bool removable)
+bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
 {
     if (!ok) return false;
 
@@ -321,6 +321,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
       lemmas.push();
       ps.copyTo(lemmas.last());
       lemmas_removable.push(removable);
+      Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
+      lemmas_proof_id.push(proof_id);
     } else {
       // If all false, we're in conflict
       if (ps.size() == falseLiteralsCount) {
@@ -329,7 +331,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
           // construct the clause below to give to the proof manager
           // as the final conflict.
           if(falseLiteralsCount == 1) {
-            PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); )
+            PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT, proof_id); )
             PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
             return ok = false;
           }
@@ -351,7 +353,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
 	attachClause(cr);
 
         if(PROOF_ON()) {
-          PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); )
+          PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT, proof_id); )
           if(ps.size() == falseLiteralsCount) {
             PROOF( ProofManager::getSatProof()->finalizeProof(cr); )
             return ok = false;
@@ -364,11 +366,12 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
         if(assigns[var(ps[0])] == l_Undef) {
           assert(assigns[var(ps[0])] != l_False);
           uncheckedEnqueue(ps[0], cr);
-          PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } );
+          Debug("cores") << "i'm registering a unit clause, input, proof id " << proof_id << std::endl;
+          PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT, proof_id); } );
           CRef confl = propagate(CHECK_WITHOUT_THEORY);
           if(! (ok = (confl == CRef_Undef)) ) {
             if(ca[confl].size() == 1) {
-              PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); );
+              PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT, proof_id); );
               PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
             } else {
               PROOF( ProofManager::getSatProof()->finalizeProof(confl); );
@@ -842,7 +845,7 @@ CRef Solver::propagate(TheoryCheckType type)
             propagateTheory();
             // If there are lemmas (or conflicts) update them
             if (lemmas.size() > 0) {
-                confl = updateLemmas();
+              confl = updateLemmas();
             }
         } else {
           // Even though in conflict, we still need to discharge the lemmas
@@ -891,7 +894,7 @@ void Solver::propagateTheory() {
         proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl);
         vec<Lit> explanation;
         MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
-        addClause(explanation, true);
+        addClause(explanation, true, 0);
       }
     }
   }
@@ -1645,6 +1648,8 @@ CRef Solver::updateLemmas() {
     // The current lemma
     vec<Lit>& lemma = lemmas[i];
     bool removable = lemmas_removable[i];
+    uint64_t proof_id = lemmas_proof_id[i];
+    Debug("cores") << "pulled lemma proof id " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
 
     // Attach it if non-unit
     CRef lemma_ref = CRef_Undef;
@@ -1659,7 +1664,7 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); );
+      PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA, proof_id); );
       if (removable) {
         clauses_removable.push(lemma_ref);
       } else {
@@ -1667,7 +1672,7 @@ CRef Solver::updateLemmas() {
       }
       attachClause(lemma_ref);
     } else {
-      PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); );
+      PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA, proof_id); );
     }
 
     // If the lemma is propagating enqueue its literal (or set the conflict)
@@ -1681,7 +1686,7 @@ CRef Solver::updateLemmas() {
           } else {
             Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
             conflict = CRef_Lazy;
-            PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0]); );
+            PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT, proof_id); );
           }
         } else {
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
@@ -1694,6 +1699,7 @@ CRef Solver::updateLemmas() {
   // Clear the lemmas
   lemmas.clear();
   lemmas_removable.clear();
+  lemmas_proof_id.clear();
 
   if (conflict != CRef_Undef) {
     theoryConflict = true;
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 7831f211b..2d70cfeef 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -37,12 +37,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "expr/command.h"
 
 namespace CVC4 {
-class SatProof;
-
-namespace prop {
-  class TheoryProxy;
-}/* CVC4::prop namespace */
+  class SatProof;
 
+  namespace prop {
+    class TheoryProxy;
+  }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 namespace Minisat {
@@ -85,6 +84,9 @@ protected:
   /** Is the lemma removable */
   vec<bool> lemmas_removable;
 
+  /** Proof IDs for lemmas */
+  vec<uint64_t> lemmas_proof_id;
+
   /** Do a another check if FULL_EFFORT was the last one */
   bool recheck;
 
@@ -154,12 +156,14 @@ public:
     void          push                     ();
     void          pop                      ();
 
-    bool    addClause (const vec<Lit>& ps, bool removable);                     // Add a clause to the solver.
+    // CVC4 adds the "proof_id" here to refer to the input assertion/lemma
+    // that produced this clause
+    bool    addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id);  // Add a clause to the solver.
     bool    addEmptyClause(bool removable);                                     // Add the empty clause, making the solver contradictory.
-    bool    addClause (Lit p, bool removable);                                  // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, bool removable);                           // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, bool removable);                    // Add a ternary clause to the solver.
-    bool    addClause_(      vec<Lit>& ps, bool removable);                     // Add a clause to the solver without making superflous internal copy. Will
+    bool    addClause (Lit p, bool removable, uint64_t proof_id);               // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, bool removable, uint64_t proof_id);        // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver.
+    bool    addClause_(      vec<Lit>& ps, bool removable, uint64_t proof_id);  // Add a clause to the solver without making superflous internal copy. Will
                                                                                  // change the passed vector 'ps'.
 
     // Solving:
@@ -489,11 +493,15 @@ inline void Solver::checkGarbage(double gf){
 
 // NOTE: enqueue does not set the ok flag! (only public methods do)
 inline bool     Solver::enqueue         (Lit p, CRef from)      { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
-inline bool     Solver::addClause       (const vec<Lit>& ps, bool removable)    { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
-inline bool     Solver::addEmptyClause  (bool removable)                        { add_tmp.clear(); return addClause_(add_tmp, removable); }
-inline bool     Solver::addClause       (Lit p, bool removable)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
-inline bool     Solver::addClause       (Lit p, Lit q, bool removable)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
-inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
+inline bool     Solver::addClause       (const vec<Lit>& ps, bool removable, uint64_t proof_id)
+                                                                { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); }
+inline bool     Solver::addEmptyClause  (bool removable)        { add_tmp.clear(); return addClause_(add_tmp, removable, uint64_t(-1)); }
+inline bool     Solver::addClause       (Lit p, bool removable, uint64_t proof_id)
+                                                                { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); }
+inline bool     Solver::addClause       (Lit p, Lit q, bool removable, uint64_t proof_id)
+                                                                { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); }
+inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id)
+                                                                { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); }
 inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); }
 inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); flipped.push(false); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } }
 
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 4a192d0d2..b50c1c09f 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -149,10 +149,10 @@ void MinisatSatSolver::setupOptions() {
   d_minisat->restart_inc = options::satRestartInc();
 }
 
-void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
+void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) {
   Minisat::vec<Minisat::Lit> minisat_clause;
   toMinisatClause(clause, minisat_clause);
-  d_minisat->addClause(minisat_clause, removable);
+  d_minisat->addClause(minisat_clause, removable, proof_id);
 }
 
 SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
@@ -228,7 +228,7 @@ void MinisatSatSolver::push() {
   d_minisat->push();
 }
 
-void MinisatSatSolver::pop(){
+void MinisatSatSolver::pop() {
   d_minisat->pop();
 }
 
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index b37371d98..3992f1adb 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -53,7 +53,7 @@ public:
   static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
   void initialize(context::Context* context, TheoryProxy* theoryProxy);
 
-  void addClause(SatClause& clause, bool removable);
+  void addClause(SatClause& clause, bool removable, uint64_t proof_id);
 
   SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
   SatVariable trueVar() { return d_minisat->trueVar(); }
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 6dcdb76c7..71e747f72 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -159,7 +159,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 
 
 
-bool SimpSolver::addClause_(vec<Lit>& ps, bool removable)
+bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
 {
 #ifndef NDEBUG
     if (use_simplification) {
@@ -173,7 +173,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable)
     if (use_rcheck && implied(ps))
         return true;
 
-    if (!Solver::addClause_(ps, removable))
+    if (!Solver::addClause_(ps, removable, proof_id))
         return false;
 
     if (use_simplification && clauses_persistent.size() == nclauses + 1){
@@ -545,7 +545,7 @@ bool SimpSolver::eliminateVar(Var v)
     for (int i = 0; i < pos.size(); i++)
         for (int j = 0; j < neg.size(); j++) {
             bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable();
-            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable)) {
+            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) {
                 return false;
             }
         }
@@ -585,7 +585,7 @@ bool SimpSolver::substitute(Var v, Lit x)
 
         removeClause(cls[i]);
 
-        if (!addClause_(subst_clause, c.removable())) {
+        if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) {
             return ok = false;
         }
     }
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 878d799a5..041309546 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -47,12 +47,12 @@ class SimpSolver : public Solver {
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
-    bool    addClause (const vec<Lit>& ps, bool removable);
-    bool    addEmptyClause(bool removable);                  // Add the empty clause to the solver.
-    bool    addClause (Lit p, bool removable);               // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, bool removable);        // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver.
-    bool    addClause_(vec<Lit>& ps, bool removable);
+    bool    addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id);
+    bool    addEmptyClause(bool removable, uint64_t proof_id); // Add the empty clause to the solver.
+    bool    addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver.
+    bool    addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id);
     bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
@@ -182,11 +182,15 @@ inline void SimpSolver::updateElimHeap(Var v) {
         elim_heap.update(v); }
 
 
-inline bool SimpSolver::addClause    (const vec<Lit>& ps, bool removable)    { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addEmptyClause(bool removable)                       { add_tmp.clear(); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addClause    (Lit p, bool removable)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause    (const vec<Lit>& ps, bool removable, uint64_t proof_id)
+                                                                             { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); }
+inline bool SimpSolver::addEmptyClause(bool removable, uint64_t proof_id)    { add_tmp.clear(); return addClause_(add_tmp, removable, proof_id); }
+inline bool SimpSolver::addClause    (Lit p, bool removable, uint64_t proof_id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable, uint64_t proof_id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); }
 inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
 
 inline bool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 82c0bae1a..a02e40e32 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -25,6 +25,7 @@
 #include "decision/options.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
+#include "proof/proof_manager.h"
 #include "util/cvc4_assert.h"
 #include "options/options.h"
 #include "smt/options.h"
@@ -109,15 +110,15 @@ void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as non-removable
-  d_cnfStream->convertAndAssert(node, false, false);
+  d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN);
 }
 
-void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
+void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
-  // Assert as removable
-  d_cnfStream->convertAndAssert(node, removable, negated);
+  // Assert as (possibly) removable
+  d_cnfStream->convertAndAssert(node, removable, negated, rule, from);
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a5132e3da..ed022a64f 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -25,6 +25,7 @@
 #include "options/options.h"
 #include "util/result.h"
 #include "smt/modal_exception.h"
+#include "proof/proof_manager.h"
 #include <sys/time.h>
 
 namespace CVC4 {
@@ -199,7 +200,7 @@ public:
    * @param removable whether this lemma can be quietly removed based
    * on an activity heuristic (or not)
    */
-  void assertLemma(TNode node, bool negated, bool removable);
+  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null());
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 8e7e53474..e3b0f3449 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -24,6 +24,7 @@
 #include "util/statistics_registry.h"
 #include "context/cdlist.h"
 #include "prop/sat_solver_types.h"
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace prop {
@@ -38,7 +39,7 @@ public:
   virtual ~SatSolver() { }
 
   /** Assert a clause in the solver. */
-  virtual void addClause(SatClause& clause, bool removable) = 0;
+  virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0;
 
   /**
    * Create a new boolean variable in the solver.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 67325cb18..2bcd48099 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -122,7 +122,7 @@ void TheoryProxy::notifyRestart() {
           if(lemmaCount % 1 == 0) {
             Debug("shared") << "=) " << asNode << std::endl;
           }
-          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true);
+          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID);
         } else {
           Debug("shared") << "=(" << asNode << std::endl;
         }