merged the proofgen3 branch into trunk:

    - can now output LFSC checkable resolution proofs 
    - added configuration option  --enable-proof
    - added command line argument --proof
To turn proofs on build with proofs enabled and run with --proof. 

22 files changed, 1321 insertions, 26 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 63fcf590d..906a64a65 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -17,7 +17,7 @@ AM_CPPFLAGS = \
 	-I@srcdir@/include -I@srcdir@ -I@builddir@
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-SUBDIRS = lib expr util context theory prop smt printer . parser compat bindings main
+SUBDIRS = lib expr util context theory prop smt printer proof . parser compat bindings main
 
 lib_LTLIBRARIES = libcvc4.la
 if HAVE_CXXTESTGEN
@@ -36,6 +36,7 @@ libcvc4_la_LIBADD = \
 	@builddir@/util/libutil.la \
 	@builddir@/expr/libexpr.la \
 	@builddir@/context/libcontext.la \
+	@builddir@/proof/libproof.la \
 	@builddir@/prop/libprop.la \
 	@builddir@/prop/minisat/libminisat.la \
 	@builddir@/printer/libprinter.la \
@@ -46,6 +47,7 @@ libcvc4_noinst_la_LIBADD = \
 	@builddir@/util/libutil.la \
 	@builddir@/expr/libexpr.la \
 	@builddir@/context/libcontext.la \
+	@builddir@/proof/libproof.la \
 	@builddir@/prop/libprop.la \
 	@builddir@/prop/minisat/libminisat.la \
 	@builddir@/printer/libprinter.la \
diff --git a/src/main/usage.h b/src/main/usage.h
index c11a2b73e..f0c7c7f08 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -54,7 +54,8 @@ CVC4 options:\n\
    --no-interactive       do not run interactively\n\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
-   --lazy-definition-expansion expand define-fun lazily\n";
+   --lazy-definition-expansion expand define-fun lazily\n
+   --proof\n";
 
 }/* CVC4::main namespace */
 }/* CVC4 namespace */
diff --git a/src/proof/Makefile b/src/proof/Makefile
new file mode 100644
index 000000000..b0985ba84
--- /dev/null
+++ b/src/proof/Makefile
@@ -0,0 +1,4 @@
+topdir = ../..
+srcdir = src/proof
+
+include $(topdir)/Makefile.subdir
diff --git a/src/proof/Makefile.am b/src/proof/Makefile.am
new file mode 100644
index 000000000..d657dfa80
--- /dev/null
+++ b/src/proof/Makefile.am
@@ -0,0 +1,18 @@
+AM_CPPFLAGS = \
+	-D__BUILDING_CVC4LIB \
+	-D __STDC_LIMIT_MACROS \
+	-D __STDC_FORMAT_MACROS \
+	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -I@srcdir@/../prop/minisat
+AM_CXXFLAGS = -Wall -Wno-parentheses -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libproof.la
+
+libproof_la_SOURCES = \
+	proof.h \
+	sat_proof.h \
+	sat_proof.cpp \
+	cnf_proof.h \
+	cnf_proof.cpp \
+	proof_manager.h \
+	proof_manager.cpp
+
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
new file mode 100644
index 000000000..2bf146661
--- /dev/null
+++ b/src/proof/cnf_proof.cpp
@@ -0,0 +1,9 @@
+#include "cnf_proof.h"
+using namespace CVC4::prop;
+
+namespace CVC4 {
+CnfProof::CnfProof(CnfStream* stream) :
+  d_cnfStream(stream) {}
+
+
+} /* CVC4 namespace */
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
new file mode 100644
index 000000000..c43c9fc62
--- /dev/null
+++ b/src/proof/cnf_proof.h
@@ -0,0 +1,35 @@
+/*********************                                                        */
+/*! \file cnf_proof.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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
+ ** information.\endverbatim
+ **
+ ** \brief A manager for CnfProofs.
+ **
+ ** A manager for CnfProofs.
+ **
+ ** 
+ **/
+
+#ifndef __CVC4__CNF_PROOF_H
+#define __CVC4__CNF_PROOF_H
+
+#include <iostream> 
+namespace CVC4 {
+namespace prop {
+class CnfStream;
+}
+class CnfProof {
+  CVC4::prop::CnfStream* d_cnfStream;
+public:
+  CnfProof(CVC4::prop::CnfStream* cnfStream);
+};
+
+} /* CVC4 namespace*/ 
+#endif /* __CVC4__CNF_PROOF_H */
diff --git a/src/proof/proof.h b/src/proof/proof.h
new file mode 100644
index 000000000..f163a4ffd
--- /dev/null
+++ b/src/proof/proof.h
@@ -0,0 +1,37 @@
+/*********************                                                        */
+/*! \file sat_proof.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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
+ ** information.\endverbatim
+ **
+ ** \brief Proof manager
+ **
+ ** Proof manager
+ **/
+
+#ifndef __CVC4__PROOF_H
+#define __CVC4__PROOF_H
+
+#include "util/options.h"
+//#define CVC4_PROOFS
+
+#ifdef CVC4_PROOF
+#  define PROOF(x) if(Options::current()->proof) { x; }
+#  define NULLPROOF(x) (Options::current()->proof)? x : NULL
+#  define PROOF_ON() Options::current()->proof
+#else /* CVC4_PROOF */
+#  define PROOF(x)
+#  define NULLPROOF(x) NULL
+#  define PROOF_ON() false
+#endif /* CVC4_PROOF */
+
+
+
+#endif /* __CVC4__PROOF_H */
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
new file mode 100644
index 000000000..d6dd7b73d
--- /dev/null
+++ b/src/proof/proof_manager.cpp
@@ -0,0 +1,70 @@
+#include "proof/proof_manager.h"
+#include "proof/sat_proof.h"
+#include "proof/cnf_proof.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+bool          ProofManager::isInitialized = false;
+ProofManager* ProofManager::proofManager = NULL;
+
+ProofManager::ProofManager(ProofFormat format = LFSC):
+  d_satProof(NULL),
+  d_cnfProof(NULL),
+  d_format(format)
+{}
+
+ProofManager* ProofManager::currentPM() {
+  if (isInitialized) {
+    return proofManager; 
+  } else {
+    proofManager = new ProofManager();
+    isInitialized = true; 
+    return proofManager; 
+    }
+}
+
+SatProof* ProofManager::getSatProof() {
+  Assert (currentPM()->d_satProof);
+  return currentPM()->d_satProof; 
+}
+
+CnfProof* ProofManager::getCnfProof() {
+  Assert (currentPM()->d_cnfProof);
+  return currentPM()->d_cnfProof;
+}
+
+void ProofManager::initSatProof(Minisat::Solver* solver) {
+  Assert (currentPM()->d_satProof == NULL);
+  switch(currentPM()->d_format) {
+  case LFSC :
+    currentPM()->d_satProof = new LFSCSatProof(solver);
+    break;
+  case NATIVE :
+    currentPM()->d_satProof = new SatProof(solver);
+    break;
+  default:
+    Assert(false); 
+  }
+  
+}
+
+void ProofManager::initCnfProof(prop::CnfStream* cnfStream) {
+  Assert (currentPM()->d_cnfProof == NULL);
+
+  switch(currentPM()->d_format) {
+  case LFSC :
+    currentPM()->d_cnfProof = new CnfProof(cnfStream); // FIXME
+    break;
+  case NATIVE :
+    currentPM()->d_cnfProof = new CnfProof(cnfStream);
+    break;
+  default:
+    Assert(false); 
+  }
+
+}
+
+
+
+} /* CVC4  namespace */ 
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
new file mode 100644
index 000000000..5d8b9d271
--- /dev/null
+++ b/src/proof/proof_manager.h
@@ -0,0 +1,64 @@
+/*********************                                                        */
+/*! \file proof_manager.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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
+ ** information.\endverbatim
+ **
+ ** \brief A manager for Proofs.
+ **
+ ** A manager for Proofs.
+ **
+ ** 
+ **/
+
+#ifndef __CVC4__PROOF_MANAGER_H
+#define __CVC4__PROOF_MANAGER_H
+
+#include <iostream> 
+#include "proof.h"
+
+// forward declarations
+namespace Minisat {
+class Solver;
+}
+
+namespace CVC4 {
+namespace prop {
+class CnfStream;
+}
+class SatProof;
+class CnfProof;
+
+// different proof modes
+enum ProofFormat {
+  LFSC,
+  NATIVE
+};
+
+class ProofManager {
+  SatProof*   d_satProof;
+  CnfProof*   d_cnfProof;
+  ProofFormat d_format;
+  
+  static ProofManager* proofManager; 
+  static bool isInitialized; 
+  ProofManager(ProofFormat format);
+public:
+  static ProofManager* currentPM();
+
+  static void      initSatProof(Minisat::Solver* solver); 
+  static void      initCnfProof(CVC4::prop::CnfStream* cnfStream);
+
+  static SatProof* getSatProof();
+  static CnfProof* getCnfProof();
+
+};
+
+} /* CVC4 namespace*/ 
+#endif /* __CVC4__PROOF_MANAGER_H */
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
new file mode 100644
index 000000000..095251da8
--- /dev/null
+++ b/src/proof/sat_proof.cpp
@@ -0,0 +1,711 @@
+#include "proof/sat_proof.h"
+#include "prop/minisat/core/Solver.h"
+
+using namespace std;
+using namespace Minisat;
+
+namespace CVC4 {
+
+/// some helper functions 
+
+void printLit (Minisat::Lit l) {
+  Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1;
+}
+
+void printClause (Minisat::Clause& c) {
+  for (int i = 0; i < c.size(); i++) {
+    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; 
+  }
+}
+
+void printLitSet(const LitSet& s) {
+  for(LitSet::iterator it = s.begin(); it != s.end(); ++it) {
+    printLit(*it);
+    Debug("proof:sat") << " "; 
+  }
+  Debug("proof:sat") << endl; 
+}
+
+// purely debugging functions
+void printDebug (Minisat::Lit l) {
+  Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << endl;
+}
+
+void printDebug (Minisat::Clause& c) {
+  for (int i = 0; i < c.size(); i++) {
+    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; 
+  }
+  Debug("proof:sat") << endl;
+}
+
+
+int SatProof::d_idCounter = 0; 
+
+/** 
+ * Converts the clause associated to id to a set of literals
+ * 
+ * @param id the clause id
+ * @param set the clause converted to a set of literals 
+ */
+void SatProof::createLitSet(ClauseId id, LitSet& set) {
+  Assert (set.empty());
+  if(isUnit(id)) {
+    set.insert(getUnit(id));
+    return;
+  }
+  if ( id == d_emptyClauseId) {
+    return; 
+  }
+  CRef ref = getClauseRef(id);
+  Assert (ref != CRef_Undef); 
+  Clause& c = d_solver->ca[ref];
+  for (int i = 0; i < c.size(); i++) {
+    set.insert(c[i]); 
+  }
+}
+
+
+/** 
+ * Resolves clause1 and clause2 on variable var and stores the
+ * result in clause1
+ * @param var 
+ * @param clause1 
+ * @param clause2 
+ */
+bool resolve(const Lit v, LitSet& clause1, LitSet& clause2, bool s) {
+  Assert(!clause1.empty());
+  Assert(!clause2.empty()); 
+  Lit var = sign(v) ? ~v : v; 
+  if (s) {
+    // literal appears positive in the first clause
+    if( !clause2.count(~var)) {
+      Debug("proof:sat") << "proof:resolve: Missing literal ";
+      printLit(var);
+      Debug("proof:sat") << endl; 
+      return false; 
+    }
+    clause1.erase(var);
+    clause2.erase(~var);
+    for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) {
+      clause1.insert(*it); 
+    }
+  } else {
+    // literal appears negative in the first clause
+    if( !clause1.count(~var) || !clause2.count(var)) {
+      Debug("proof:sat") << "proof:resolve: Mising literal ";
+      printLit(var);
+      Debug("proof:sat") << endl; 
+      return false; 
+    }
+    clause1.erase(~var);
+    clause2.erase(var);
+    for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) {
+      clause1.insert(*it); 
+    }
+  }
+  return true; 
+}
+
+/// ResChain
+
+ResChain::ResChain(ClauseId start) :
+    d_start(start),
+    d_steps(),
+    d_redundantLits(NULL)
+  {}
+
+void ResChain::addStep(Lit lit, ClauseId id, bool sign) {
+  ResStep step(lit, id, sign);
+  d_steps.push_back(step); 
+}
+
+
+void ResChain::addRedundantLit(Lit lit) {
+  if (d_redundantLits) {
+    d_redundantLits->insert(lit); 
+  } else {
+    d_redundantLits = new LitSet();
+    d_redundantLits->insert(lit); 
+  }
+}
+
+
+/// ProxyProof
+
+ProofProxy::ProofProxy(SatProof* proof):
+  d_proof(proof)
+{}
+
+void ProofProxy::updateCRef(CRef oldref, CRef newref) {
+  d_proof->updateCRef(oldref, newref); 
+}
+
+
+/// SatProof
+
+SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
+    d_solver(solver),
+    d_idClause(),
+    d_clauseId(),
+    d_idUnit(),
+    d_deleted(),
+    d_inputClauses(), 
+    d_resChains(),
+    d_resStack(),
+    d_checkRes(checkRes),
+    d_emptyClauseId(-1),
+    d_nullId(-2),
+    d_temp_clauseId(),
+    d_temp_idClause()
+  {
+    d_proxy = new ProofProxy(this); 
+  }
+
+
+/** 
+ * Returns true if the resolution chain corresponding to id
+ * does resolve to the clause associated to id
+ * @param id 
+ * 
+ * @return 
+ */
+bool SatProof::checkResolution(ClauseId id) {
+  if(d_checkRes) {
+    bool validRes = true; 
+    Assert (d_resChains.find(id) != d_resChains.end());
+    ResChain* res = d_resChains[id];
+    LitSet clause1;
+    createLitSet(res->getStart(), clause1);
+    ResSteps& steps = res->getSteps(); 
+    for (unsigned i = 0; i < steps.size(); i++) {
+      Lit    var = steps[i].lit;
+      LitSet clause2; 
+      createLitSet (steps[i].id, clause2);
+      bool res = resolve (var, clause1, clause2, steps[i].sign);
+      if(res == false) {
+        validRes = false;
+        break;
+      }
+    }
+    // compare clause we claimed to prove with the resolution result
+    if (isUnit(id)) {
+      // special case if it was a unit clause
+      Lit unit = getUnit(id);
+      validRes = clause1.size() == clause1.count(unit) && !clause1.empty(); 
+      return validRes; 
+    }
+    if (id == d_emptyClauseId) {
+      return clause1.empty(); 
+    }
+    CRef ref = getClauseRef(id);
+    Assert (ref != CRef_Undef);
+    Clause& c = d_solver->ca[ref];
+    for (int i = 0; i < c.size(); ++i) {
+      int count = clause1.erase(c[i]);
+      if (count == 0) {
+        Debug("proof:sat") << "proof:checkResolution::literal not in computed result ";
+        printLit(c[i]);
+        Debug("proof:sat") << "\n";
+        validRes = false; 
+      }
+    }
+    validRes = clause1.empty();
+    if (! validRes) {
+      Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n";
+      printLitSet(clause1);
+      Debug("proof:sat") << "proof:checkResolution:: result should be: \n";
+      printClause(c); 
+    }
+    return validRes; 
+    
+  } else {
+    return true; 
+  }
+}
+
+
+
+
+/// helper methods
+
+ClauseId SatProof::getClauseId(CRef ref) {
+  if(d_clauseId.find(ref) == d_clauseId.end()) {
+    Debug("proof:sat") << "Missing clause \n"; 
+  }
+  Assert(d_clauseId.find(ref) != d_clauseId.end());
+  return d_clauseId[ref]; 
+}
+
+
+ClauseId SatProof::getClauseId(Lit lit) {
+  Assert(d_unitId.find(toInt(lit)) != d_unitId.end());
+  return d_unitId[toInt(lit)]; 
+}
+
+CRef SatProof::getClauseRef(ClauseId id) {
+  if (d_idClause.find(id) == d_idClause.end()) {
+    Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" "
+                       << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "")
+                       << (isUnit(id)? "Unit" : "") << endl;
+  }
+  Assert(d_idClause.find(id) != d_idClause.end());
+  return d_idClause[id]; 
+}
+
+Clause& SatProof::getClause(ClauseId id) {
+  return d_solver->ca[id]; 
+}
+Lit SatProof::getUnit(ClauseId id) {
+  Assert (d_idUnit.find(id) != d_idUnit.end());
+  return d_idUnit[id]; 
+}
+
+bool SatProof::isUnit(ClauseId id) {
+  return d_idUnit.find(id) != d_idUnit.end(); 
+}
+
+bool SatProof::isUnit(Lit lit) {
+  return d_unitId.find(toInt(lit)) != d_unitId.end(); 
+}
+
+ClauseId SatProof::getUnitId(Lit lit) {
+  Assert(isUnit(lit)); 
+  return d_unitId[toInt(lit)]; 
+}
+
+bool SatProof::hasResolution(ClauseId id) {
+  return d_resChains.find(id) != d_resChains.end(); 
+}
+
+bool SatProof::isInputClause(ClauseId id) {
+  return (d_inputClauses.find(id) != d_inputClauses.end()); 
+}
+
+
+void SatProof::print(ClauseId id) {
+  if (d_deleted.find(id) != d_deleted.end()) {
+    Debug("proof:sat") << "del"<<id; 
+  } else if (isUnit(id)) {
+    printLit(getUnit(id)); 
+  } else if (id == d_emptyClauseId) {
+    Debug("proof:sat") << "empty "<< endl; 
+  }
+  else {
+    CRef ref  = getClauseRef(id);
+    Assert (ref != CRef_Undef);
+    printClause(d_solver->ca[ref]);
+  }
+}
+
+void SatProof::printRes(ClauseId id) {
+  Assert(hasResolution(id));
+  Debug("proof:sat") << "id "<< id <<": ";
+  printRes(d_resChains[id]); 
+}
+
+void SatProof::printRes(ResChain* res) {
+  ClauseId start_id = res->getStart();
+
+  Debug("proof:sat") << "(";
+  print(start_id); 
+
+  ResSteps& steps = res->getSteps();
+  for(unsigned i = 0; i < steps.size(); i++ ) {
+    Lit v = steps[i].lit;
+    ClauseId id = steps[i].id;
+
+    Debug("proof:sat") << "[";
+    printLit(v);
+    Debug("proof:sat") << "] ";
+    print(id); 
+  }
+  Debug("proof:sat") << ") \n";
+}
+
+/// registration methods
+
+ClauseId SatProof::registerClause(CRef clause, bool isInput) {
+  Assert(clause != CRef_Undef); 
+  ClauseIdMap::iterator it = d_clauseId.find(clause);
+   if (it == d_clauseId.end()) {
+     ClauseId newId = d_idCounter++; 
+     d_clauseId[clause]= newId;
+     d_idClause[newId] =clause;
+     if (isInput) {
+       Assert (d_inputClauses.find(newId) == d_inputClauses.end()); 
+       d_inputClauses.insert(newId); 
+     }
+   }
+   return d_clauseId[clause]; 
+}
+
+ClauseId SatProof::registerUnitClause(Lit lit, bool isInput) {
+  UnitIdMap::iterator it = d_unitId.find(toInt(lit));
+  if (it == d_unitId.end()) {
+    ClauseId newId = d_idCounter++;
+    d_unitId[toInt(lit)] = newId;
+    d_idUnit[newId] = lit; 
+    if (isInput) {
+      Assert (d_inputClauses.find(newId) == d_inputClauses.end());
+      d_inputClauses.insert(newId); 
+    }
+  }
+  return d_unitId[toInt(lit)]; 
+}
+
+void SatProof::removedDfs(Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen){
+  // if we already added the literal return
+  if (seen.count(lit)) {
+    return; 
+  }
+
+  CRef reason_ref = d_solver->reason(var(lit));
+  if (reason_ref == CRef_Undef) {
+    seen.insert(lit);
+    removeStack.push_back(lit); 
+    return; 
+  }
+
+  Assert (reason_ref != CRef_Undef); 
+  int size = d_solver->ca[reason_ref].size();
+  for (int i = 1; i < size; i++ ) {
+    Lit v = d_solver->ca[reason_ref][i];
+    if(inClause.count(v) == 0 && seen.count(v) == 0) {
+      removedDfs(v, removedSet, removeStack, inClause, seen);
+    }
+  }
+  if(seen.count(lit) == 0) {
+    seen.insert(lit); 
+    removeStack.push_back(lit);
+  }
+}
+
+
+void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) {
+  LitSet* removed = res->getRedundant();
+  if (removed == NULL) {
+    return;
+  }
+
+  LitSet inClause;
+  createLitSet(id, inClause); 
+  
+  LitVector removeStack;
+  LitSet seen; 
+  for (LitSet::iterator it = removed->begin(); it != removed->end(); ++it) {
+    removedDfs(*it, removed, removeStack, inClause, seen); 
+  }
+  
+  for (int i = removeStack.size()-1; i >= 0; --i) {
+    Lit lit = removeStack[i];
+    CRef reason_ref = d_solver->reason(var(lit));
+    ClauseId reason_id; 
+
+    if (reason_ref == CRef_Undef) {
+      Assert(isUnit(~lit));
+      reason_id = getUnitId(~lit); 
+    } else {
+      reason_id = registerClause(reason_ref);
+    }
+    res->addStep(lit, reason_id, !sign(lit));
+  }
+  removed->clear(); 
+}
+
+void SatProof::registerResolution(ClauseId id, ResChain* res) {
+  Assert(res != NULL);
+
+  removeRedundantFromRes(res, id);
+  Assert(res->redundantRemoved()); 
+
+  d_resChains[id] = res;
+  printRes(id); 
+  if (d_checkRes) {
+    Assert(checkResolution(id));
+  }
+}
+
+
+/// recording resolutions
+
+void SatProof::startResChain(CRef start) {
+  ClauseId id = getClauseId(start); 
+  ResChain* res = new ResChain(id);
+  d_resStack.push_back(res); 
+}
+
+void SatProof::addResolutionStep(Lit lit, CRef clause, bool sign) {
+  ClauseId id = registerClause(clause);
+  ResChain* res = d_resStack.back();
+  res->addStep(lit, id, sign); 
+}
+
+void SatProof::endResChain(CRef clause) {
+  Assert(d_resStack.size() > 0);
+  ClauseId  id = registerClause(clause); 
+  ResChain* res = d_resStack.back();
+  registerResolution(id, res);
+  d_resStack.pop_back(); 
+}
+
+
+void SatProof::endResChain(Lit lit) {
+  Assert(d_resStack.size() > 0);
+  ClauseId  id = registerUnitClause(lit); 
+  ResChain* res = d_resStack.back();
+  
+
+  registerResolution(id, res);
+  d_resStack.pop_back(); 
+}
+
+void SatProof::storeLitRedundant(Lit lit) {
+  Assert(d_resStack.size() > 0);
+  ResChain* res = d_resStack.back();
+  res->addRedundantLit(lit);  
+}
+
+/// constructing resolutions 
+
+void SatProof::resolveOutUnit(Lit lit) {
+  ClauseId id = resolveUnit(~lit);
+  ResChain* res = d_resStack.back();
+  res->addStep(lit, id, !sign(lit)); 
+}
+
+void SatProof::storeUnitResolution(Lit lit) {
+  resolveUnit(lit);
+}
+
+ClauseId SatProof::resolveUnit(Lit lit) {
+  // first check if we already have a resolution for lit
+  if(isUnit(lit)) {
+    ClauseId id = getClauseId(lit);
+    if(hasResolution(id) || isInputClause(id)) {
+      return id; 
+    }
+    Assert (false); 
+  }
+  CRef reason_ref = d_solver->reason(var(lit));
+  Assert (reason_ref != CRef_Undef);
+  
+  ClauseId reason_id = registerClause(reason_ref); 
+
+  ResChain* res = new ResChain(reason_id); 
+  Clause& reason  = d_solver->ca[reason_ref];
+  for (int i = 0; i < reason.size(); i++) {
+    Lit l = reason[i];
+    if(lit != l) { 
+      ClauseId res_id = resolveUnit(~l);
+      res->addStep(l, res_id, !sign(l));
+    }
+  }
+  ClauseId unit_id = registerUnitClause(lit); 
+  registerResolution(unit_id, res);
+  return unit_id; 
+}
+
+void SatProof::printProof() {
+  Debug("proof:sat") << "SatProof::printProof\n";
+}
+
+void SatProof::finalizeProof(CRef conflict_ref) {
+  Assert(d_resStack.size() == 0);
+  //ClauseId conflict_id = getClauseId(conflict_ref); 
+  ClauseId conflict_id = registerClause(conflict_ref); //FIXME
+  Debug("proof:sat") << "proof::finalizeProof Final Conflict ";
+  print(conflict_id);
+  
+  ResChain* res = new ResChain(conflict_id);
+  Clause& conflict = d_solver->ca[conflict_ref] ;
+  for (int i = 0; i < conflict.size(); ++i) {
+    Lit lit = conflict[i];
+    ClauseId res_id = resolveUnit(~lit);
+    res->addStep(lit, res_id, !sign(lit)); 
+  }
+  registerResolution(d_emptyClauseId, res);
+  printProof(); 
+}
+
+/// CRef manager
+
+void SatProof::updateCRef(CRef oldref, CRef newref) {
+  if (d_clauseId.find(oldref) == d_clauseId.end()) {
+    return; 
+  }
+  ClauseId id = getClauseId(oldref);
+  Assert (d_temp_clauseId.find(newref) == d_temp_clauseId.end());
+  Assert (d_temp_idClause.find(id) == d_temp_idClause.end()); 
+  d_temp_clauseId[newref] = id;
+  d_temp_idClause[id] = newref;
+}
+
+void SatProof::finishUpdateCRef() {
+  d_clauseId.swap(d_temp_clauseId);
+  d_temp_clauseId.clear();
+
+  d_idClause.swap(d_temp_idClause);
+  d_temp_idClause.clear(); 
+}
+
+void SatProof::markDeleted(CRef clause) {
+  if (d_clauseId.find(clause) != d_clauseId.end()) {
+    ClauseId id = getClauseId(clause);
+    Assert (d_deleted.find(id) == d_deleted.end()); 
+    d_deleted.insert(id); 
+  }
+}
+
+/// LFSCSatProof class
+
+string LFSCSatProof::varName(Lit lit) {
+  ostringstream os;
+  if (sign(lit)) {
+    os << "(neg v"<<var(lit) << ")" ; 
+  }
+  else {
+    os << "(pos v"<<var(lit) << ")"; 
+  }
+  return os.str(); 
+}
+
+
+string LFSCSatProof::clauseName(ClauseId id) {
+  ostringstream os;
+  if (isInputClause(id)) {
+    os << "p"<<id;
+    return os.str(); 
+  } else {
+    os << "l"<<id;
+    return os.str(); 
+  }
+}
+
+void LFSCSatProof::collectLemmas(ClauseId id) {
+  if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
+    return; 
+  }
+  if (d_seenInput.find(id) != d_seenInput.end()) {
+    return; 
+  }
+
+  if (isInputClause(id)) {
+    d_seenInput.insert(id);
+    return; 
+  } else {
+    d_seenLemmas.insert(id); 
+  }
+
+  ResChain* res = d_resChains[id];
+  ClauseId start = res->getStart();
+  collectLemmas(start);
+
+  ResSteps steps = res->getSteps(); 
+  for(unsigned i = 0; i < steps.size(); i++) {
+    collectLemmas(steps[i].id); 
+  }
+}
+
+
+
+void LFSCSatProof::printResolution(ClauseId id) {
+  d_lemmaSS << "(satlem _ _ _ ";
+
+  ResChain* res = d_resChains[id];  
+  ResSteps& steps = res->getSteps();
+  
+  for (int i = steps.size()-1; i >= 0; i--) {
+    d_lemmaSS << "(";
+    d_lemmaSS << (steps[i].sign? "R" : "Q") << " _ _ ";
+              
+  }
+  
+  ClauseId start_id = res->getStart();
+  if(isInputClause(start_id)) {
+    d_seenInput.insert(start_id); 
+  }
+  d_lemmaSS << clauseName(start_id) << " ";
+  
+  for(unsigned i = 0; i < steps.size(); i++) {
+    d_lemmaSS << clauseName(steps[i].id) << " v" << var(steps[i].lit) <<")"; 
+  }
+  
+  if (id == d_emptyClauseId) {
+    d_lemmaSS <<"(\\empty empty)";
+    return; 
+  }
+
+  d_lemmaSS << "(\\" << clauseName(id) << "\n";   // bind to lemma name
+  d_paren << "))";                                // closing parethesis for lemma binding and satlem
+}
+
+
+void LFSCSatProof::printInputClause(ClauseId id){
+  ostringstream os;
+  CRef ref = getClauseRef(id);
+  Assert (ref != CRef_Undef);
+  Clause& c = getClause(ref);
+
+  d_clauseSS << "(% " << clauseName(id) << " (holds ";
+  os << ")"; // closing paren for holds
+  d_paren << ")"; // closing paren for (%
+
+  for(int i = 0; i < c.size(); i++) {
+    d_clauseSS << " (clc " << varName(c[i]) <<" ";
+    os <<")";
+    d_seenVars.insert(var(c[i])); 
+  }
+  d_clauseSS << "cln";
+  d_clauseSS << os.str() << "\n";  
+} 
+
+
+void LFSCSatProof::printClauses() {
+  for (IdHashSet::iterator it = d_seenInput.begin(); it!= d_seenInput.end(); ++it) {
+    printInputClause(*it);
+  }
+}
+
+void LFSCSatProof::printVariables() {
+  for (VarSet::iterator it = d_seenVars.begin(); it != d_seenVars.end(); ++it) {
+    d_varSS << "(% v" << *it <<" var \n";
+    d_paren << ")"; 
+  }
+}
+
+
+void LFSCSatProof::flush() {
+  ostringstream out;
+  out << "(check \n";
+  d_paren <<")"; 
+  out << d_varSS.str();
+  out << d_clauseSS.str();
+  out << "(: (holds cln) \n"; 
+  out << d_lemmaSS.str(); 
+  d_paren << "))";
+  out << d_paren.str();
+  out << ";"; //to comment out the solver's answer 
+  std::cout << out.str(); 
+}
+
+void LFSCSatProof::printProof() {
+  Debug("proof:sat") << " LFSCSatProof::printProof \n";
+
+  // first collect lemmas to print in reverse order
+  collectLemmas(d_emptyClauseId); 
+  for(IdSet::iterator it = d_seenLemmas.begin(); it!= d_seenLemmas.end(); ++it) {
+    if(*it != d_emptyClauseId) {
+      printResolution(*it);
+    }
+  }
+  // last resolution to be printed is the empty clause
+  printResolution(d_emptyClauseId);
+
+  printClauses();
+  printVariables();
+  flush();
+  
+}
+
+} /* CVC4 namespace */
+
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
new file mode 100644
index 000000000..4f9ba8e4a
--- /dev/null
+++ b/src/proof/sat_proof.h
@@ -0,0 +1,256 @@
+/*********************                                                        */
+/*! \file sat_proof.h
+ ** \verbatim
+ ** Original author: lianah
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  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
+ ** information.\endverbatim
+ **
+ ** \brief Resolution proof 
+ **
+ ** Resolution proof
+ **/
+
+#ifndef __CVC4__SAT__PROOF_H
+#define __CVC4__SAT__PROOF_H
+
+#include <iostream>
+#include <stdint.h>
+#include <vector>
+#include <set>
+#include <ext/hash_map>
+#include <ext/hash_set>
+#include <sstream>
+namespace Minisat {
+class Solver;
+typedef uint32_t CRef;
+}
+
+#include "prop/minisat/core/SolverTypes.h"
+
+namespace std {
+using namespace __gnu_cxx;
+}
+
+namespace CVC4 {
+/** 
+ * Helper debugging functions
+ * 
+ */
+void printDebug(::Minisat::Lit l);
+void printDebug(::Minisat::Clause& c); 
+
+typedef int ClauseId;
+struct ResStep {
+  ::Minisat::Lit lit;
+  ClauseId id;
+  bool sign;
+  ResStep(::Minisat::Lit l, ClauseId i, bool s) :
+    lit(l),
+    id(i),
+    sign(s)
+  {}
+};
+
+typedef std::vector< ResStep > ResSteps; 
+typedef std::set < ::Minisat::Lit> LitSet; 
+
+class ResChain {
+private:
+  ClauseId       d_start;
+  ResSteps       d_steps;
+  LitSet*        d_redundantLits;
+public:
+  ResChain(ClauseId start);
+  void addStep(::Minisat::Lit, ClauseId, bool);
+  bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); }
+  void addRedundantLit(::Minisat::Lit lit); 
+  ~ResChain();
+  // accessor methods
+  ClauseId  getStart()     { return d_start; }
+  ResSteps& getSteps()     { return d_steps; }
+  LitSet*   getRedundant() { return d_redundantLits; }
+};
+
+
+typedef std::hash_map < ClauseId, ::Minisat::CRef > IdClauseMap;
+typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap;
+typedef std::hash_map < ClauseId, ::Minisat::Lit>   IdUnitMap;
+typedef std::hash_map < int, ClauseId>            UnitIdMap; //FIXME 
+typedef std::hash_map < ClauseId, ResChain*>      IdResMap; 
+typedef std::hash_set < ClauseId >                IdHashSet;
+typedef std::vector   < ResChain* >               ResStack; 
+
+typedef std::hash_set < int >                     VarSet; 
+typedef std::set < ClauseId >                     IdSet; 
+typedef std::vector < ::Minisat::Lit >              LitVector; 
+class SatProof; 
+
+class ProofProxy : public ProofProxyAbstract {
+private:
+  SatProof* d_proof;
+public:
+  ProofProxy(SatProof* pf);
+  void updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref);
+};
+
+class SatProof {
+protected:
+  ::Minisat::Solver*    d_solver;
+  // clauses 
+  IdClauseMap         d_idClause;
+  ClauseIdMap         d_clauseId;
+  IdUnitMap           d_idUnit;
+  UnitIdMap           d_unitId;
+  IdHashSet           d_deleted;
+  IdHashSet           d_inputClauses; 
+  
+  // resolutions 
+  IdResMap            d_resChains;
+  ResStack            d_resStack; 
+  bool                d_checkRes;
+  
+  static ClauseId     d_idCounter; 
+  const ClauseId      d_emptyClauseId;
+  const ClauseId      d_nullId;
+  // proxy class to break circular dependencies 
+  ProofProxy*         d_proxy;
+  
+  // temporary map for updating CRefs
+  ClauseIdMap         d_temp_clauseId;
+  IdClauseMap         d_temp_idClause; 
+public:  
+  SatProof(::Minisat::Solver* solver, bool checkRes = false);
+protected:
+  void print(ClauseId id); 
+  void printRes(ClauseId id);
+  void printRes(ResChain* res); 
+  
+  bool isInputClause(ClauseId id); 
+  bool isUnit(ClauseId id);
+  bool isUnit(::Minisat::Lit lit); 
+  bool hasResolution(ClauseId id); 
+  void createLitSet(ClauseId id, LitSet& set); 
+  void registerResolution(ClauseId id, ResChain* res);
+  
+  ClauseId      getClauseId(::Minisat::CRef clause);
+  ClauseId      getClauseId(::Minisat::Lit lit); 
+  ::Minisat::CRef getClauseRef(ClauseId id);
+  ::Minisat::Lit  getUnit(ClauseId id);
+  ClauseId      getUnitId(::Minisat::Lit lit); 
+  ::Minisat::Clause& getClause(ClauseId id);
+  virtual void printProof();
+  
+  bool checkResolution(ClauseId id);
+  /** 
+   * Constructs a resolution tree that proves lit
+   * and returns the ClauseId for the unit clause lit
+   * @param lit the literal we are proving
+   * 
+   * @return 
+   */
+  ClauseId resolveUnit(::Minisat::Lit lit);
+  /** 
+   * Does a depth first search on removed literals and adds the literals
+   * to be removed in the proper order to the stack. 
+   * 
+   * @param lit the literal we are recusing on
+   * @param removedSet the previously computed set of redundantant literals
+   * @param removeStack the stack of literals in reverse order of resolution
+   */
+  void removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen);
+  void removeRedundantFromRes(ResChain* res, ClauseId id);
+public:
+  void startResChain(::Minisat::CRef start);
+  void addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign);
+  /** 
+   * Pops the current resolution of the stack and stores it
+   * in the resolution map. Also registers the @param clause. 
+   * @param clause the clause the resolution is proving 
+   */
+  void endResChain(::Minisat::CRef clause);
+  void endResChain(::Minisat::Lit lit);
+  /** 
+   * Stores in the current derivation the redundant literals that were 
+   * eliminated from the conflict clause during conflict clause minimization. 
+   * @param lit the eliminated literal 
+   */
+  void storeLitRedundant(::Minisat::Lit lit);
+
+  /// update the CRef Id maps when Minisat does memory reallocation x
+  void updateCRef(::Minisat::CRef old_ref, ::Minisat::CRef new_ref);
+  void finishUpdateCRef();
+  
+  /** 
+   * Constructs the empty clause resolution from the final conflict
+   * 
+   * @param conflict 
+   */void finalizeProof(::Minisat::CRef conflict);
+
+  /// clause registration methods 
+  ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false);
+  ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false);
+  /** 
+   * Marks the deleted clauses as deleted. Note we may still use them in the final
+   * resolution. 
+   * @param clause 
+   */
+  void markDeleted(::Minisat::CRef clause);
+  /** 
+   * Constructs the resolution of ~q and resolves it with the current
+   * resolution thus eliminating q from the current clause
+   * @param q the literal to be resolved out
+   */
+  void     resolveOutUnit(::Minisat::Lit q);
+  /** 
+   * Constructs the resolution of the literal lit. Called when a clause
+   * containing lit becomes satisfied and is removed. 
+   * @param lit 
+   */
+  void     storeUnitResolution(::Minisat::Lit lit); 
+  
+  ProofProxy* getProxy() {return d_proxy; } 
+};
+
+class LFSCSatProof: public SatProof {
+private:
+  VarSet             d_seenVars; 
+  std::ostringstream d_varSS;
+  std::ostringstream d_lemmaSS;
+  std::ostringstream d_clauseSS;
+  std::ostringstream d_paren; 
+  IdSet              d_seenLemmas;
+  IdHashSet          d_seenInput; 
+
+  inline std::string varName(::Minisat::Lit lit);
+  inline std::string clauseName(ClauseId id); 
+
+  void collectLemmas(ClauseId id);
+  void printResolution(ClauseId id);
+  void printInputClause(ClauseId id);
+
+  void printVariables();
+  void printClauses();
+  void flush();
+  
+public:
+  LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false):
+    SatProof(solver, checkRes),
+    d_seenVars(),
+    d_varSS(),
+    d_lemmaSS(),
+    d_paren(),
+    d_seenLemmas(),
+    d_seenInput()
+  {} 
+  void printProof();  
+};
+
+}
+
+#endif
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 1c327c5a8..961ef85c5 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -28,6 +28,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/sat.h"
 #include "util/output.h"
 #include "expr/command.h"
+#include "proof/proof_manager.h"
+#include "proof/sat_proof.h"
 
 using namespace Minisat;
 using namespace CVC4;
@@ -121,7 +123,9 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo
   , conflict_budget    (-1)
   , propagation_budget (-1)
   , asynch_interrupt   (false)
-{}
+{
+  PROOF(ProofManager::initSatProof(this);)
+}
 
 
 Solver::~Solver()
@@ -233,6 +237,9 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
       } else if (ps.size() == 1) {
         if(assigns[var(ps[0])] == l_Undef) {
           uncheckedEnqueue(ps[0]);
+          
+          PROOF( ProofManager::getSatProof()->registerUnitClause(ps[0], true); )
+
           if(assertionLevel > 0) {
             // remember to unset it on user pop
             Debug("minisat") << "got new unit " << ps[0] << " at assertion level " << assertionLevel << std::endl;
@@ -244,6 +251,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
         CRef cr = ca.alloc(assertionLevel, ps, false);
         clauses_persistent.push(cr);
 	attachClause(cr);
+        
+        PROOF( ProofManager::getSatProof()->registerClause(cr, true); )
       }
     }
 
@@ -263,6 +272,8 @@ void Solver::attachClause(CRef cr) {
 
 
 void Solver::detachClause(CRef cr, bool strict) {
+    PROOF( ProofManager::getSatProof()->markDeleted(cr); ) 
+
     const Clause& c = ca[cr];
     Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
     assert(c.size() > 1);
@@ -401,10 +412,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 
     int max_level = 0; // Maximal level of the resolved clauses
 
+    PROOF( ProofManager::getSatProof()->startResChain(confl); )
     do{
         assert(confl != CRef_Undef); // (otherwise should be UIP)
         Clause& c = ca[confl];
-
         if (c.level() > max_level) {
           max_level = c.level();
         }
@@ -422,6 +433,11 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
                     pathC++;
                 else
                     out_learnt.push(q);
+            } else {
+              // FIXME: can we do it lazily if we actually need the proof?
+              if (level(var(q)) == 0) {
+                PROOF( ProofManager::getSatProof()->resolveOutUnit(q); )
+              }
             }
         }
         
@@ -431,6 +447,10 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
         confl = reason(var(p));
         seen[var(p)] = 0;
         pathC--;
+        
+        if ( pathC > 0 && confl != CRef_Undef ) {
+          PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); )
+        }
 
     }while (pathC > 0);
     out_learnt[0] = ~p;
@@ -442,7 +462,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];
@@ -453,6 +473,8 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
                 // Literal is not redundant
                 out_learnt[j++] = out_learnt[i];
               } else {
+                //
+                PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); )
                 // Literal is redundant, mark the level of the redundancy derivation
                 if (max_level < red_level) {
                   max_level = red_level;
@@ -809,8 +831,13 @@ void Solver::removeSatisfied(vec<CRef>& cs)
     int i, j;
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
-        if (satisfied(c))
+        if (satisfied(c)) {
+          if (locked(c)) {
+            // store a resolution of the literal c propagated
+            PROOF( ProofManager::getSatProof()->storeUnitResolution(c[0]); )
+          }
             removeClause(cs[i]);
+        }
         else
             cs[j++] = cs[i];
     }
@@ -908,7 +935,10 @@ lbool Solver::search(int nof_conflicts)
 
           conflicts++; conflictC++;
 
-          if (decisionLevel() == 0) return l_False;
+          if (decisionLevel() == 0) {
+            PROOF( ProofManager::getSatProof()->finalizeProof(confl); )
+            return l_False;
+          }
 
             // Analyze the conflict
             learnt_clause.clear();
@@ -918,12 +948,17 @@ lbool Solver::search(int nof_conflicts)
             // Assert the conflict clause and the asserting literal
             if (learnt_clause.size() == 1) {
                 uncheckedEnqueue(learnt_clause[0]);
-            } else {
+
+                PROOF( ProofManager::getSatProof()->endResChain(learnt_clause[0]); )
+
+             } else {
                 CRef cr = ca.alloc(max_level, learnt_clause, true);
                 clauses_removable.push(cr);
                 attachClause(cr);
                 claBumpActivity(ca[cr]);
                 uncheckedEnqueue(learnt_clause[0], cr);
+
+                PROOF( ProofManager::getSatProof()->endResChain(cr); )
             }
 
             varDecayActivity();
@@ -1211,7 +1246,7 @@ void Solver::relocAll(ClauseAllocator& to)
             // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
             vec<Watcher>& ws = watches[p];
             for (int j = 0; j < ws.size(); j++)
-                ca.reloc(ws[j].cref, to);
+              ca.reloc(ws[j].cref, to,   NULLPROOF( ProofManager::getSatProof()->getProxy() ));
         }
 
     // All reasons:
@@ -1220,18 +1255,19 @@ void Solver::relocAll(ClauseAllocator& to)
         Var v = var(trail[i]);
 
         if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
-            ca.reloc(vardata[v].reason, to);
+          ca.reloc(vardata[v].reason, to, NULLPROOF( ProofManager::getSatProof()->getProxy() ));
     }
-
     // All learnt:
     //
     for (int i = 0; i < clauses_removable.size(); i++)
-        ca.reloc(clauses_removable[i], to);
+      ca.reloc(clauses_removable[i], to,  NULLPROOF( ProofManager::getSatProof()->getProxy() ));
 
     // All original:
     //
     for (int i = 0; i < clauses_persistent.size(); i++)
-        ca.reloc(clauses_persistent[i], to);
+      ca.reloc(clauses_persistent[i], to,  NULLPROOF( ProofManager::getSatProof()->getProxy() ));
+
+      PROOF( ProofManager::getSatProof()->finishUpdateCRef(); )
 }
 
 
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index c5220997b..a3d449a36 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -37,9 +37,12 @@ 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 SatSolver;
 }/* CVC4::prop namespace */
+
 }/* CVC4 namespace */
 
 namespace Minisat {
@@ -49,9 +52,9 @@ namespace Minisat {
 
 class Solver {
 
-  /** The only CVC4 entry point to the private solver data */
+  /** The only two CVC4 entry points to the private solver data */
   friend class CVC4::prop::SatSolver;
-
+  friend class CVC4::SatProof; 
 protected:
 
   /** The pointer to the proxy that provides interfaces to the SMT engine */
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 1aff5094d..57ca95a41 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -24,7 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #define Minisat_SolverTypes_h
 
 #include <assert.h>
-
+#include "util/output.h"
 #include "mtl/IntTypes.h"
 #include "mtl/Alg.h"
 #include "mtl/Vec.h"
@@ -44,6 +44,7 @@ typedef int Var;
 #define var_Undef (-1)
 
 
+
 struct Lit {
     int     x;
 
@@ -115,11 +116,26 @@ public:
 inline int   toInt  (lbool l) { return l.value; }
 inline lbool toLbool(int   v) { return lbool((uint8_t)v);  }
 
-//=================================================================================================
-// Clause -- a simple class for representing a clause:
 
 class Clause;
 typedef RegionAllocator<uint32_t>::Ref CRef;
+} /* Minisat */
+
+
+
+namespace CVC4 {
+class ProofProxyAbstract {
+public:
+  virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; 
+};
+}
+
+
+
+namespace Minisat{
+
+//=================================================================================================
+// Clause -- a simple class for representing a clause:
 
 class Clause {
     struct {
@@ -236,17 +252,21 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
     }
 
-    void reloc(CRef& cr, ClauseAllocator& to)
+  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());
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 8c31dd377..6045fc881 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -21,7 +21,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "mtl/Sort.h"
 #include "simp/SimpSolver.h"
 #include "utils/System.h"
-
+#include "proof/proof.h"
 using namespace Minisat;
 using namespace CVC4;
 
@@ -57,7 +57,7 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con
   , asymm_lits         (0)
   , eliminated_vars    (0)
   , elimorder          (1)
-  , use_simplification (!enableIncremental)
+  , use_simplification (!enableIncremental && !PROOF_ON()) // TODO: turn off simplifications if proofs are on initially
   , occurs             (ClauseDeleted(ca))
   , elim_heap          (ElimLt(n_occ))
   , bwdsub_assigns     (0)
@@ -702,10 +702,11 @@ void SimpSolver::relocAll(ClauseAllocator& to)
     //
     for (int i = 0; i < subsumption_queue.size(); i++)
         ca.reloc(subsumption_queue[i], to);
-
+        // TODO reloc now takes the proof form the core solver 
     // Temporary clause:
     //
     ca.reloc(bwdsub_tmpunit, to);
+    // TODO reloc now takes the proof form the core solver 
 }
 
 
@@ -723,4 +724,5 @@ void SimpSolver::garbageCollect()
         printf("|  Garbage collection:   %12d bytes => %12d bytes             |\n", 
                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
     to.moveTo(ca);
+    // TODO: proof.finalizeUpdateId(); 
 }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ecd61c0b4..96ee5b59b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -244,6 +244,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   if(Options::current()->cumulativeMillisecondLimit != 0) {
     setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
   }
+
 }
 
 void SmtEngine::shutdown() {
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f898ee76a..5d8f31d3c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -36,6 +36,7 @@
 #include "util/result.h"
 #include "util/sexpr.h"
 #include "util/stats.h"
+#include "proof/proof_manager.h"
 
 // In terms of abstraction, this is below (and provides services to)
 // ValidityChecker and above (and requires the services of)
@@ -43,6 +44,7 @@
 
 namespace CVC4 {
 
+
 template <bool ref_count> class NodeTemplate;
 typedef NodeTemplate<true> Node;
 typedef NodeTemplate<false> TNode;
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 3164b75a5..211a1127b 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -69,6 +69,10 @@ bool Configuration::isAssertionBuild() {
   return IS_ASSERTIONS_BUILD;
 }
 
+bool Configuration::isProofBuild() {
+  return IS_PROOFS_BUILD;
+}
+
 bool Configuration::isCoverageBuild() {
   return IS_COVERAGE_BUILD;
 }
diff --git a/src/util/configuration.h b/src/util/configuration.h
index c3040f3fb..1a57af62b 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -59,6 +59,8 @@ public:
 
   static bool isAssertionBuild();
 
+  static bool isProofBuild(); 
+  
   static bool isCoverageBuild();
 
   static bool isProfilingBuild();
diff --git a/src/util/configuration_private.h b/src/util/configuration_private.h
index abff15b3b..53b69ebfc 100644
--- a/src/util/configuration_private.h
+++ b/src/util/configuration_private.h
@@ -67,6 +67,12 @@ namespace CVC4 {
 #  define IS_ASSERTIONS_BUILD false
 #endif /* CVC4_ASSERTIONS */
 
+#ifdef CVC4_PROOF
+#  define IS_PROOFS_BUILD true
+#else  /* CVC4_PROOF */
+#  define IS_PROOFS_BUILD false
+#endif /* CVC4_PROOF */
+
 #ifdef CVC4_COVERAGE
 #  define IS_COVERAGE_BUILD true
 #else /* CVC4_COVERAGE */
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 64f1fe4d5..c69db62a3 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -80,6 +80,7 @@ Options::Options() :
   cumulativeMillisecondLimit(0),
   segvNoSpin(false),
   produceModels(false),
+  proof(false),
   produceAssignments(false),
   typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
   earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
@@ -129,6 +130,7 @@ static const string optionsDescription = "\
    --no-interactive       do not run interactively\n\
    --produce-models | -m  support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
+   --proof                turn proof generation on\n\
    --lazy-definition-expansion expand define-fun lazily\n\
    --simplification=MODE  choose simplification mode, see --simplification=help\n\
    --no-static-learning   turn off static learning (e.g. diamond-breaking)\n\
@@ -292,6 +294,7 @@ enum OptionValue {
   INTERACTIVE,
   NO_INTERACTIVE,
   PRODUCE_ASSIGNMENTS,
+  PROOF,
   NO_TYPE_CHECKING,
   LAZY_TYPE_CHECKING,
   EAGER_TYPE_CHECKING,
@@ -369,6 +372,7 @@ static struct option cmdlineOptions[] = {
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { "produce-models", no_argument   , NULL, 'm' },
   { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
+  { "proof", no_argument, NULL, PROOF },
   { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING },
   { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
   { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
@@ -628,11 +632,15 @@ throw(OptionException) {
     case 'm':
       produceModels = true;
       break;
-
+      
     case PRODUCE_ASSIGNMENTS:
       produceAssignments = true;
       break;
-
+      
+    case PROOF:
+      proof = true;
+      break;
+      
     case NO_TYPE_CHECKING:
       typeChecking = false;
       earlyTypeChecking = false;
@@ -828,6 +836,7 @@ throw(OptionException) {
       printf("dumping    : %s\n", Configuration::isDumpingBuild() ? "yes" : "no");
       printf("muzzled    : %s\n", Configuration::isMuzzledBuild() ? "yes" : "no");
       printf("assertions : %s\n", Configuration::isAssertionBuild() ? "yes" : "no");
+      printf("proof      : %s\n", Configuration::isProofBuild() ? "yes" : "no");
       printf("coverage   : %s\n", Configuration::isCoverageBuild() ? "yes" : "no");
       printf("profiling  : %s\n", Configuration::isProfilingBuild() ? "yes" : "no");
       printf("competition: %s\n", Configuration::isCompetitionBuild() ? "yes" : "no");
diff --git a/src/util/options.h b/src/util/options.h
index f9dc042d1..699895c47 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -145,6 +145,9 @@ struct CVC4_PUBLIC Options {
   /** Whether we support SmtEngine::getValue() for this run. */
   bool produceModels;
 
+  /** Whether we produce proofs. */
+  bool proof;
+  
   /** Whether we support SmtEngine::getAssignment() for this run. */
   bool produceAssignments;