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. 

4 files changed, 83 insertions, 22 deletions

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(); 
 }