Merged bit-vector and uf proof branch.

7 files changed, 211 insertions, 107 deletions

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 4c431a9b1..f4489c4be 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -25,6 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "base/output.h"
 #include "options/prop_options.h"
 #include "proof/proof_manager.h"
+#include "proof/sat_proof_implementation.h"
 #include "proof/sat_proof.h"
 #include "prop/minisat/core/Solver.h"
 #include "prop/minisat/minisat.h"
@@ -32,6 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/theory_proxy.h"
 #include "smt_util/command.h"
 
+
 using namespace CVC4::prop;
 
 namespace CVC4 {
@@ -40,7 +42,6 @@ namespace Minisat {
 //=================================================================================================
 // Options:
 
-
 static const char* _cat = "CORE";
 
 static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
@@ -55,6 +56,10 @@ static IntOption     opt_restart_first     (_cat, "rfirst",      "The base resta
 static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false));
 static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",  0.20, DoubleRange(0, false, HUGE_VAL, false));
 
+//=================================================================================================
+// Proof declarations
+CRef Solver::TCRef_Undef = CRef_Undef;
+CRef Solver::TCRef_Lazy = CRef_Lazy;
 
 class ScopedBool {
   bool& watch;
@@ -135,8 +140,12 @@ 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, uint64_t(-1)); )
-  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT, uint64_t(-1)); )
+  // FIXME: these should be axioms I believe
+  PROOF
+    (
+     ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
+     ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
+     );
 }
 
 
@@ -217,7 +226,9 @@ CRef Solver::reason(Var x) {
 
     // Get the explanation from the theory
     SatClause explanation_cl;
-    proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl);
+    // FIXME: at some point return a tag with the theory that spawned you
+    proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l),
+                              explanation_cl);
     vec<Lit> explanation;
     MinisatSatSolver::toMinisatClause(explanation_cl, explanation); 
 
@@ -263,7 +274,12 @@ CRef Solver::reason(Var x) {
 
     // Construct the reason
     CRef real_reason = ca.alloc(explLevel, explanation, true);
-    PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA, (uint64_t(RULE_CONFLICT) << 32)); );
+    // FIXME: at some point will need more information about where this explanation
+    // came from (ie. the theory/sharing)
+    PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA);
+           ProofManager::getCnfProof()->registerConvertedClause(id, true);
+           // no need to pop current assertion as this is not converted to cnf
+           );
     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 +287,7 @@ CRef Solver::reason(Var x) {
     return real_reason;
 }
 
-bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
+bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 {
     if (!ok) return false;
 
@@ -289,11 +305,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
       clauseLevel = std::max(clauseLevel, intro_level(var(ps[i])));
       // Tautologies are ignored
       if (ps[i] == ~p) {
+        id = ClauseIdUndef;
         // Clause can be ignored
         return true;
       }
       // Clauses with 0-level true literals are also ignored
       if (value(ps[i]) == l_True && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) {
+        id = ClauseIdUndef;
         return true;
       }
       // Ignore repeated literals
@@ -321,8 +339,19 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
       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);
+      PROOF(
+            // Store the expression being converted to CNF until
+            // the clause is actually created
+            Node assertion = ProofManager::getCnfProof()->getCurrentAssertion();
+            Node def = ProofManager::getCnfProof()->getCurrentDefinition();
+            lemmas_cnf_assertion.push_back(std::make_pair(assertion, def));
+            id = ClauseIdUndef;
+        );
+      // does it have to always be a lemma?
+      // PROOF(id = ProofManager::getSatProof()->registerUnitClause(ps[0], THEORY_LEMMA););
+      // PROOF(id = ProofManager::getSatProof()->registerTheoryLemma(ps););
+      // 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) {
@@ -331,7 +360,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
           // 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_id); )
+            PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); )
             PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); )
             return ok = false;
           }
@@ -353,7 +382,9 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
 	attachClause(cr);
 
         if(PROOF_ON()) {
-          PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT, proof_id); )
+          PROOF(
+                id = ProofManager::getSatProof()->registerClause(cr, INPUT);
+                )
           if(ps.size() == falseLiteralsCount) {
             PROOF( ProofManager::getSatProof()->finalizeProof(cr); )
             return ok = false;
@@ -366,12 +397,16 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
         if(assigns[var(ps[0])] == l_Undef) {
           assert(assigns[var(ps[0])] != l_False);
           uncheckedEnqueue(ps[0], cr);
-          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); } );
+          Debug("cores") << "i'm registering a unit clause, input" << std::endl;
+          PROOF(
+                if(ps.size() == 1) {
+                  id = ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT);
+                }
+                );
           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_id); );
+              PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); );
               PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); )
             } else {
               PROOF( ProofManager::getSatProof()->finalizeProof(confl); );
@@ -604,7 +639,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
         for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
             Lit q = c[j];
 
-            if (!seen[var(q)] && level(var(q)) > 0){
+            if (!seen[var(q)] && level(var(q)) > 0) {
                 varBumpActivity(var(q));
                 seen[var(q)] = 1;
                 if (level(var(q)) >= decisionLevel())
@@ -646,7 +681,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
         uint32_t abstract_level = 0;
         for (i = 1; i < out_learnt.size(); i++)
             abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
-        
+
         for (i = j = 1; i < out_learnt.size(); i++) {
             if (reason(var(out_learnt[i])) == CRef_Undef) {
                 out_learnt[j++] = out_learnt[i];
@@ -901,7 +936,8 @@ void Solver::propagateTheory() {
         proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl);
         vec<Lit> explanation;
         MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
-        addClause(explanation, true, 0);
+        ClauseId id; // FIXME: mark it as explanation here somehow?
+        addClause(explanation, true, id);
       }
     }
   }
@@ -1159,8 +1195,17 @@ lbool Solver::search(int nof_conflicts)
                 attachClause(cr);
                 claBumpActivity(ca[cr]);
                 uncheckedEnqueue(learnt_clause[0], cr);
-
-                PROOF( ProofManager::getSatProof()->endResChain(cr); )
+                PROOF(
+                      ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
+                      PSTATS(
+                      __gnu_cxx::hash_set<int> cl_levels;
+                      for (int i = 0; i < learnt_clause.size(); ++i) {
+                        cl_levels.insert(level(var(learnt_clause[i])));
+                      }
+                      ProofManager::getSatProof()->storeClauseGlue(id, cl_levels.size());
+                            )
+                      ProofManager::getSatProof()->endResChain(id);
+                      );
             }
 
             varDecayActivity();
@@ -1650,14 +1695,14 @@ CRef Solver::updateLemmas() {
   // Last index in the trail
   int backtrack_index = trail.size();
 
+  PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size()););
+  
   // Attach all the clauses and enqueue all the propagations
   for (int i = 0; i < lemmas.size(); ++ i)
   {
     // 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;
@@ -1672,7 +1717,15 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA, proof_id); );
+      PROOF
+        (
+         TNode cnf_assertion = lemmas_cnf_assertion[i].first;
+         TNode cnf_def = lemmas_cnf_assertion[i].second;
+
+         ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA);
+         ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
+         ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
+         );
       if (removable) {
         clauses_removable.push(lemma_ref);
       } else {
@@ -1680,7 +1733,15 @@ CRef Solver::updateLemmas() {
       }
       attachClause(lemma_ref);
     } else {
-      PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA, proof_id); );
+      PROOF
+        (
+         Node cnf_assertion = lemmas_cnf_assertion[i].first;
+         Node cnf_def = lemmas_cnf_assertion[i].second;
+         
+         ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
+         ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
+         ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
+         );
     }
 
     // If the lemma is propagating enqueue its literal (or set the conflict)
@@ -1694,7 +1755,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], LEARNT, proof_id); );
+            PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); );
           }
         } else {
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
@@ -1704,10 +1765,11 @@ CRef Solver::updateLemmas() {
     }
   }
 
+  PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size()););
   // Clear the lemmas
   lemmas.clear();
+  lemmas_cnf_assertion.clear();
   lemmas_removable.clear();
-  lemmas_proof_id.clear();
 
   if (conflict != CRef_Undef) {
     theoryConflict = true;
@@ -1718,6 +1780,28 @@ CRef Solver::updateLemmas() {
   return conflict;
 }
 
+void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy)
+{
+ 
+  // FIXME what is this CRef_lazy
+  if (cr == CRef_Lazy) return;
+  
+  CRef old = cr;  // save the old reference
+  Clause& c = operator[](cr);
+  if (c.reloced()) { cr = c.relocation(); return; }
+  
+  cr = to.alloc(c.level(), c, c.removable());
+  c.relocate(cr);
+  if (proxy) {
+    proxy->updateCRef(old, cr); 
+  }
+  // Copy extra data-fields: 
+  // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
+  to[cr].mark(c.mark());
+  if (to[cr].removable())         to[cr].activity() = c.activity();
+  else if (to[cr].has_extra()) to[cr].calcAbstraction();
+}
+
 inline bool Solver::withinBudget(uint64_t ammount) const {
   Assert (proxy);
   // spendResource sets async_interrupt or throws UnsafeInterruptException
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 3be6b1b22..a239eba72 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -37,13 +37,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 
 namespace CVC4 {
-  class SatProof;
+template <class Solver> class TSatProof;
 
-  namespace prop {
-    class TheoryProxy;
-  }/* CVC4::prop namespace */
+namespace prop {
+  class TheoryProxy;
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
+typedef unsigned ClauseId;
+
 namespace CVC4 {
 namespace Minisat {
 
@@ -54,7 +56,18 @@ class Solver {
 
   /** The only two CVC4 entry points to the private solver data */
   friend class CVC4::prop::TheoryProxy;
-  friend class CVC4::SatProof;
+  friend class CVC4::TSatProof<Minisat::Solver>;
+
+public:
+  static CRef TCRef_Undef;
+  static CRef TCRef_Lazy;
+
+  typedef Var TVar;
+  typedef Lit TLit;
+  typedef Clause TClause; 
+  typedef CRef TCRef;
+  typedef vec<Lit> TLitVec;
+  
 protected:
 
   /** The pointer to the proxy that provides interfaces to the SMT engine */
@@ -85,8 +98,8 @@ protected:
   /** Is the lemma removable */
   vec<bool> lemmas_removable;
 
-  /** Proof IDs for lemmas */
-  vec<uint64_t> lemmas_proof_id;
+  /** Nodes being converted to CNF */
+  std::vector< std::pair<CVC4::Node, CVC4::Node > >lemmas_cnf_assertion;
 
   /** Do a another check if FULL_EFFORT was the last one */
   bool recheck;
@@ -157,14 +170,14 @@ public:
     void          push                     ();
     void          pop                      ();
 
-    // 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, 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
+    // addClause returns the ClauseId corresponding to the clause added in the
+    // reference parameter id.
+    bool    addClause (const vec<Lit>& ps, bool removable, ClauseId& 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, ClauseId& id);               // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, bool removable, ClauseId& id);        // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver.
+    bool    addClause_(      vec<Lit>& ps, bool removable, ClauseId& id);  // Add a clause to the solver without making superflous internal copy. Will
                                                                                  // change the passed vector 'ps'.
 
     // Solving:
@@ -495,15 +508,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, 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::addClause       (const vec<Lit>& ps, bool removable, ClauseId& id)
+                                                                { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }
+inline bool     Solver::addEmptyClause  (bool removable)        { add_tmp.clear(); ClauseId tmp; return addClause_(add_tmp, removable, tmp); }
+inline bool     Solver::addClause       (Lit p, bool removable, ClauseId& id)
+                                                                { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); }
+inline bool     Solver::addClause       (Lit p, Lit q, bool removable, ClauseId& id)
+                                                                { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); }
+inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
+                                                                { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, 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/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index b0d78242c..116a39a49 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -169,20 +169,22 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
 }
 
 
-} /* Minisat */
-}
-
+class Solver;
 
-
-namespace CVC4 {
 class ProofProxyAbstract {
 public:
   virtual ~ProofProxyAbstract() {}
   virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; 
 };
-}
+
+} /* namespace CVC4::Minisat */
+} /* namespace CVC4 */
 
 
+namespace CVC4 {
+template <class Solver> class ProofProxy;
+typedef ProofProxy<CVC4::Minisat::Solver> CoreProofProxy;
+} 
 
 namespace CVC4 {
 namespace Minisat{
@@ -305,27 +307,8 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
     }
 
-  void reloc(CRef& cr, ClauseAllocator& to, CVC4::ProofProxyAbstract* proxy = NULL)
-    {
-
-        // FIXME what is this CRef_lazy
-        if (cr == CRef_Lazy) return;
-
-        CRef old = cr;  // save the old reference
-        Clause& c = operator[](cr);
-        if (c.reloced()) { cr = c.relocation(); return; }
-        
-        cr = to.alloc(c.level(), c, c.removable());
-        c.relocate(cr);
-        if (proxy) {
-          proxy->updateCRef(old, cr); 
-        }
-        // Copy extra data-fields: 
-        // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
-        to[cr].mark(c.mark());
-        if (to[cr].removable())         to[cr].activity() = c.activity();
-        else if (to[cr].has_extra()) to[cr].calcAbstraction();
-    }
+  void reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy = NULL);
+  // Implementation moved to Solver.cc.
 };
 
 
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index ce5c1eb92..739d9087a 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -23,6 +23,7 @@
 #include "options/prop_options.h"
 #include "options/smt_options.h"
 #include "prop/minisat/simp/SimpSolver.h"
+#include "proof/sat_proof.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -94,14 +95,6 @@ void MinisatSatSolver::toMinisatClause(SatClause& clause,
   Assert(clause.size() == (unsigned)minisat_clause.size());
 }
 
-void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
-                                       SatClause& sat_clause) {
-  for (int i = 0; i < clause.size(); ++i) {
-    sat_clause.push_back(toSatLiteral(clause[i]));
-  }
-  Assert((unsigned)clause.size() == sat_clause.size());
-}
-
 void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
                                        SatClause& sat_clause) {
   for (int i = 0; i < clause.size(); ++i) {
@@ -149,10 +142,18 @@ void MinisatSatSolver::setupOptions() {
   d_minisat->restart_inc = options::satRestartInc();
 }
 
-void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) {
+ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
   Minisat::vec<Minisat::Lit> minisat_clause;
   toMinisatClause(clause, minisat_clause);
-  d_minisat->addClause(minisat_clause, removable, proof_id);
+  ClauseId clause_id = ClauseIdError;
+  // FIXME: This relies on the invariant that when ok() is false
+  // the SAT solver does not add the clause (which is what Minisat currently does)
+  if (!ok()) {
+    return ClauseIdUndef; 
+  }
+  d_minisat->addClause(minisat_clause, removable, clause_id);
+  PROOF( Assert (clause_id != ClauseIdError););
+  return clause_id;
 }
 
 SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
@@ -182,6 +183,9 @@ SatValue MinisatSatSolver::solve() {
   return toSatLiteralValue(d_minisat->solve());
 }
 
+bool MinisatSatSolver::ok() const {
+  return d_minisat->okay(); 
+}
 
 void MinisatSatSolver::interrupt() {
   d_minisat->interrupt();
@@ -280,3 +284,20 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
 
 } /* namespace CVC4::prop */
 } /* namespace CVC4 */
+
+
+namespace CVC4 {
+template<>
+prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) {
+  return prop::MinisatSatSolver::toSatLiteral(lit);
+} 
+
+template<>
+void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl,
+                                      prop::SatClause& sat_cl) {
+  prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
+}
+
+} /* namespace CVC4 */
+
+
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index f279b3a5b..535ce1a47 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -40,11 +40,10 @@ public:
   //(Commented because not in use) static bool            tobool(SatValue val);
 
   static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
-  static void  toSatClause    (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause);
   static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
   void initialize(context::Context* context, TheoryProxy* theoryProxy);
 
-  void addClause(SatClause& clause, bool removable, uint64_t proof_id);
+  ClauseId addClause(SatClause& clause, bool removable);
 
   SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
   SatVariable trueVar() { return d_minisat->trueVar(); }
@@ -53,6 +52,8 @@ public:
   SatValue solve();
   SatValue solve(long unsigned int&);
 
+  bool ok() const;
+  
   void interrupt();
 
   SatValue value(SatLiteral l);
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 235c97e8f..5bdaea950 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -160,7 +160,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 
 
 
-bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
+bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 {
 #ifndef NDEBUG
     if (use_simplification) {
@@ -174,7 +174,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
     if (use_rcheck && implied(ps))
         return true;
 
-    if (!Solver::addClause_(ps, removable, proof_id))
+    if (!Solver::addClause_(ps, removable, id))
         return false;
 
     if (use_simplification && clauses_persistent.size() == nclauses + 1){
@@ -541,12 +541,14 @@ bool SimpSolver::eliminateVar(Var v)
     for (int i = 0; i < cls.size(); i++)
         removeClause(cls[i]); 
 
+    ClauseId id = ClauseIdUndef; 
     // Produce clauses in cross product:
     vec<Lit>& resolvent = add_tmp;
     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, uint64_t(-1))) {
+            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) &&
+                !addClause_(resolvent, removable, id)) {
                 return false;
             }
         }
@@ -585,8 +587,8 @@ bool SimpSolver::substitute(Var v, Lit x)
         }
 
         removeClause(cls[i]);
-
-        if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) {
+        ClauseId id = ClauseIdUndef;
+        if (!addClause_(subst_clause, c.removable(), id)) {
             return ok = false;
         }
     }
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 0c5062726..a19bec1ef 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -48,12 +48,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, 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    addClause (const vec<Lit>& ps, bool removable, ClauseId& id);
+    bool    addEmptyClause(bool removable); // Add the empty clause to the solver.
+    bool    addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver.
+    bool    addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
     bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
@@ -183,15 +183,15 @@ inline void SimpSolver::updateElimHeap(Var v) {
         elim_heap.update(v); }
 
 
-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 bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id)
+{ ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addEmptyClause(bool removable)    { add_tmp.clear(); ClauseId id=-1; return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addClause    (Lit p, bool removable, ClauseId& id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable, ClauseId& id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); }
 inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
 
 // the solver can always return unknown due to resource limiting