fixes to the proof system so it works with theory lemmas and explanations

3 files changed, 46 insertions, 8 deletions

diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index df695c2d1..2c0c7d036 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -173,7 +173,9 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
     d_emptyClauseId(-1),
     d_nullId(-2),
     d_temp_clauseId(),
-    d_temp_idClause()
+    d_temp_idClause(),
+    d_unitConflictId(),
+    d_storedUnitConflict(false)
   {
     d_proxy = new ProofProxy(this); 
   }
@@ -353,6 +355,7 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, bool isInput) {
        d_inputClauses.insert(newId); 
      }
    }
+   Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " <<isInput << "\n"; 
    return d_clauseId[clause]; 
 }
 
@@ -367,6 +370,7 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, bool isInput) {
       d_inputClauses.insert(newId); 
     }
   }
+  Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << isInput <<"\n"; 
   return d_unitId[toInt(lit)]; 
 }
 
@@ -527,10 +531,25 @@ void SatProof::toStream(std::ostream& out) {
   Unimplemented("native proof printing not supported yet");
 }
 
+void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit) {
+  Assert (!d_storedUnitConflict); 
+  d_unitConflictId = registerUnitClause(conflict_lit);
+  d_storedUnitConflict = true;
+  Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n"; 
+}
+
 void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
   Assert(d_resStack.size() == 0);
-  //ClauseId conflict_id = getClauseId(conflict_ref); 
-  ClauseId conflict_id = registerClause(conflict_ref); //FIXME
+  Assert (conflict_ref != ::Minisat::CRef_Undef);
+  ClauseId conflict_id; 
+  if (conflict_ref == ::Minisat::CRef_Lazy) {
+    Assert (d_storedUnitConflict); 
+    conflict_id = d_unitConflictId; 
+  } else {
+    Assert (!d_storedUnitConflict); 
+    conflict_id = registerClause(conflict_ref); //FIXME
+  }
+
   Debug("proof:sat") << "proof::finalizeProof Final Conflict ";
   print(conflict_id);
   
@@ -613,6 +632,7 @@ void LFSCSatProof::collectLemmas(ClauseId id) {
     d_seenLemmas.insert(id); 
   }
 
+  Assert (d_resChains.find(id) != d_resChains.end()); 
   ResChain* res = d_resChains[id];
   ClauseId start = res->getStart();
   collectLemmas(start);
@@ -658,6 +678,14 @@ void LFSCSatProof::printResolution(ClauseId id) {
 
 
 void LFSCSatProof::printInputClause(ClauseId id) {
+  if (isUnit(id)) {
+    ::Minisat::Lit lit = getUnit(id); 
+    d_clauseSS << "(% " << clauseName(id) << " (holds (clc ";
+    d_clauseSS << varName(lit) << "cln ))";
+    d_paren << ")";
+    return; 
+  }
+  
   ostringstream os;
   CRef ref = getClauseRef(id);
   Assert (ref != CRef_Undef);
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index d497a4eba..a552b66fd 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -124,7 +124,11 @@ protected:
   
   // temporary map for updating CRefs
   ClauseIdMap         d_temp_clauseId;
-  IdClauseMap         d_temp_idClause; 
+  IdClauseMap         d_temp_idClause;
+
+  // unit conflict
+  ClauseId d_unitConflictId;
+  bool d_storedUnitConflict; 
 public:  
   SatProof(::Minisat::Solver* solver, bool checkRes = false);
 protected:
@@ -197,6 +201,9 @@ public:
   /// clause registration methods 
   ClauseId registerClause(const ::Minisat::CRef clause, bool isInput = false);
   ClauseId registerUnitClause(const ::Minisat::Lit lit, bool isInput = false);
+
+  void storeUnitConflict(::Minisat::Lit lit); 
+  
   /** 
    * Marks the deleted clauses as deleted. Note we may still use them in the final
    * resolution. 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 6196ca357..4cce83fef 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -261,6 +261,7 @@ CRef Solver::reason(Var x) {
 
     // Construct the reason
     CRef real_reason = ca.alloc(explLevel, explanation, true);
+    PROOF (ProofManager::getSatProof()->registerClause(real_reason, true); ); 
     vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
     clauses_removable.push(real_reason);
     attachClause(real_reason);
@@ -298,7 +299,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
         continue;
       }
       // If a literals is false at 0 level (both sat and user level) we also ignore it
-      if (value(ps[i]) == l_False) {
+      if (value(ps[i]) == l_False && !PROOF_ON() )  {
         if (level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) {
           continue;
         } else {
@@ -789,7 +790,8 @@ CRef Solver::propagate(TheoryCheckType type)
       // If there are lemmas (or conflicts) update them
       if (lemmas.size() > 0) {
         recheck = true;
-        return updateLemmas();
+        confl = updateLemmas();
+        return confl; 
       } else {
         recheck = proxy->theoryNeedCheck();
         return confl;
@@ -801,7 +803,6 @@ CRef Solver::propagate(TheoryCheckType type)
     do {
         // Propagate on the clauses
         confl = propagateBool();
-
         // If no conflict, do the theory check
         if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) {
             // Do the theory check
@@ -836,7 +837,6 @@ CRef Solver::propagate(TheoryCheckType type)
           }
         }
     } while (confl == CRef_Undef && qhead < trail.size());
-
     return confl;
 }
 
@@ -1579,6 +1579,7 @@ CRef Solver::updateLemmas() {
       vec<Lit>& lemma = lemmas[i];
       // If it's an empty lemma, we have a conflict at zero level
       if (lemma.size() == 0) {
+        Assert (! PROOF_ON()); 
         conflict = CRef_Lazy;
         backtrackLevel = 0;
         Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
@@ -1628,6 +1629,7 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
+      PROOF (ProofManager::getSatProof()->registerClause(lemma_ref, true); ); 
       if (removable) {
         clauses_removable.push(lemma_ref);
       } else {
@@ -1647,6 +1649,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]);); 
           }
         } else {
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;