first draft implementation of uf proofs with holes

1 files changed, 146 insertions, 124 deletions

diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index d9b57f87e..624aac237 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -16,6 +16,8 @@
  **/
 
 #include "proof/sat_proof.h"
+#include "proof/cnf_proof.h"
+#include "proof/proof_manager.h"
 #include "prop/minisat/core/Solver.h"
 
 using namespace std;
@@ -166,7 +168,8 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
     d_clauseId(),
     d_idUnit(),
     d_deleted(),
-    d_inputClauses(), 
+    d_inputClauses(),
+    d_lemmaClauses(),
     d_resChains(),
     d_resStack(),
     d_checkRes(checkRes),
@@ -176,11 +179,23 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
     d_temp_idClause(),
     d_unitConflictId(),
     d_storedUnitConflict(false),
-    d_atomToVar()
+    d_seenLearnt(),
+    d_seenInput(),
+    d_seenLemmas(),
+    d_cnfProof(NULL)
   {
     d_proxy = new ProofProxy(this); 
   }
 
+CnfProof* SatProof::getCnfProof() {
+  Assert (d_cnfProof);
+  return d_cnfProof; 
+}
+
+void SatProof::setCnfProof(CnfProof* cnfProof) {
+  Assert (d_cnfProof == NULL);
+  d_cnfProof = cnfProof; 
+}
 
 /** 
  * Returns true if the resolution chain corresponding to id
@@ -272,8 +287,8 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
   return d_idClause[id]; 
 }
 
-Clause& SatProof::getClause(ClauseId id) {
-  return d_solver->ca[id]; 
+Clause& SatProof::getClause(CRef ref) {
+  return d_solver->ca[ref]; 
 }
 ::Minisat::Lit SatProof::getUnit(ClauseId id) {
   Assert (d_idUnit.find(id) != d_idUnit.end());
@@ -301,6 +316,10 @@ bool SatProof::isInputClause(ClauseId id) {
   return (d_inputClauses.find(id) != d_inputClauses.end()); 
 }
 
+bool SatProof::isLemmaClause(ClauseId id) {
+  return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); 
+}
+
 
 void SatProof::print(ClauseId id) {
   if (d_deleted.find(id) != d_deleted.end()) {
@@ -344,34 +363,43 @@ void SatProof::printRes(ResChain* res) {
 
 /// registration methods
 
-ClauseId SatProof::registerClause(::Minisat::CRef clause, bool isInput) {
+ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) {
   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) {
+     if (kind == INPUT) {
        Assert (d_inputClauses.find(newId) == d_inputClauses.end()); 
        d_inputClauses.insert(newId); 
      }
+     if (kind == THEORY_LEMMA) {
+       Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end());
+       d_lemmaClauses.insert(newId); 
+     }
    }
-   Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " <<isInput << "\n"; 
+   Debug("proof:sat:detailed") <<"registerClause " << d_clauseId[clause] << " " << kind << "\n"; 
    return d_clauseId[clause]; 
 }
 
-ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, bool isInput) {
+ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) {
   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) {
+    if (kind == INPUT) {
       Assert (d_inputClauses.find(newId) == d_inputClauses.end());
       d_inputClauses.insert(newId); 
     }
+    if (kind == THEORY_LEMMA) {
+      Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end());
+      d_lemmaClauses.insert(newId); 
+    }
+
   }
-  Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << isInput <<"\n"; 
+  Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n"; 
   return d_unitId[toInt(lit)]; 
 }
 
@@ -593,179 +621,173 @@ void SatProof::markDeleted(CRef clause) {
   }
 }
 
-/// store mapping from theory atoms to new variables
-void SatProof::storeAtom(::Minisat::Lit literal, Expr atom) {
-  Assert(d_atomToVar.find(atom) == d_atomToVar.end());
-  d_atomToVar[atom] = literal; 
+void SatProof::constructProof() {
+  collectClauses(d_emptyClauseId); 
 }
 
+// std::string SatProof::varName(::Minisat::Lit lit) {
+//   ostringstream os;
+//   if (sign(lit)) {
+//     os << "(neg "<< ProofManager::getVarPrefix() <<var(lit) << ")" ; 
+//   }
+//   else {
+//     os << "(pos "<< ProofManager::getVarPrefix() <<var(lit) << ")"; 
+//   }
+//   return os.str(); 
+// }
 
 
-/// LFSCSatProof class
-
-std::string LFSCSatProof::varName(::Minisat::Lit lit) {
-  ostringstream os;
-  if (sign(lit)) {
-    os << "(neg v"<<var(lit) << ")" ; 
-  }
-  else {
-    os << "(pos v"<<var(lit) << ")"; 
-  }
-  return os.str(); 
-}
-
-
-std::string LFSCSatProof::clauseName(ClauseId id) {
+std::string SatProof::clauseName(ClauseId id) {
   ostringstream os;
   if (isInputClause(id)) {
-    os << "p"<<id;
+    os << ProofManager::getInputClausePrefix()<<id;
     return os.str(); 
-  } else {
-    os << "l"<<id;
+  } else 
+  if (isLemmaClause(id)) {
+    os << ProofManager::getLemmaClausePrefix()<<id;
+    return os.str(); 
+  }else {
+    os << ProofManager::getLearntClausePrefix()<<id;
     return os.str(); 
   }
 }
 
-void LFSCSatProof::collectLemmas(ClauseId id) {
-  if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
+void SatProof::collectClauses(ClauseId id) {
+  if (d_seenLearnt.find(id) != d_seenLearnt.end()) {
     return; 
   }
   if (d_seenInput.find(id) != d_seenInput.end()) {
     return; 
   }
+  if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
+    return; 
+  }
 
   if (isInputClause(id)) {
+    CRef input_ref = getClauseRef(id);
+    const Clause& cl = getClause(input_ref);
+    getCnfProof()->addInputClause(id, cl); 
     d_seenInput.insert(id);
     return; 
-  } else {
+  }
+  else if (isLemmaClause(id)) {
+    CRef lemma_ref = getClauseRef(id);
+    const Clause& cl = getClause(lemma_ref);
+    getCnfProof()->addTheoryLemma(id, cl); 
     d_seenLemmas.insert(id); 
+  } 
+  else {
+    d_seenLearnt.insert(id); 
   }
 
   Assert (d_resChains.find(id) != d_resChains.end()); 
   ResChain* res = d_resChains[id];
   ClauseId start = res->getStart();
-  collectLemmas(start);
+  collectClauses(start);
 
   ResSteps steps = res->getSteps(); 
   for(unsigned i = 0; i < steps.size(); i++) {
-    collectLemmas(steps[i].id); 
+    collectClauses(steps[i].id); 
   }
 }
 
+/// LFSCSatProof class
 
-
-void LFSCSatProof::printResolution(ClauseId id) {
-  d_lemmaSS << "(satlem _ _ _ ";
+void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) {
+  out << "(satlem_simplify _ _ _ ";
 
   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") << " _ _ ";
+    out << "(";
+    out << (steps[i].sign? "R" : "Q") << " _ _ ";
               
   }
   
   ClauseId start_id = res->getStart();
-  if(isInputClause(start_id)) {
-    d_seenInput.insert(start_id); 
-  }
-  d_lemmaSS << clauseName(start_id) << " ";
+  // WHY DID WE NEED THIS?
+  // if(isInputClause(start_id)) {
+  //   d_seenInput.insert(start_id); 
+  // }
+  out << clauseName(start_id) << " ";
   
   for(unsigned i = 0; i < steps.size(); i++) {
-    d_lemmaSS << clauseName(steps[i].id) << " v" << var(steps[i].lit) <<")"; 
+    out << clauseName(steps[i].id) << " "<<ProofManager::getVarPrefix() << var(steps[i].lit) <<")"; 
   }
   
   if (id == d_emptyClauseId) {
-    d_lemmaSS <<"(\\empty empty)";
+    out <<"(\\empty empty)";
     return; 
   }
 
-  d_lemmaSS << "(\\" << clauseName(id) << "\n";   // bind to lemma name
-  d_paren << "))";                                // closing parethesis for lemma binding and satlem
+  out << "(\\" << clauseName(id) << "\n";   // bind to lemma name
+  paren << "))";                            // closing parethesis for lemma binding and satlem
 }
 
 
-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; 
-  }
+// 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);
-  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(std::ostream& out) {
-  out << d_atomsSS.str(); 
-  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 << "\n";
-}
-
-void LFSCSatProof::toStream(std::ostream& out) {
-  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) {
+//   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::printInputClauses() {
+//   for (IdHashSet::iterator it = d_seenInput.begin(); it!= d_seenInput.end(); ++it) {
+//     printInputClause(*it);
+//   }
+// }
+
+
+// void LFSCSatProof::flush(std::ostream& out) {
+//   out << "(check \n";
+//   d_paren <<")"; 
+//   out << d_varSS.str();
+//   out << d_clauseSS.str();
+//   out << "(: (holds cln) \n"; 
+//   out << d_learntSS.str(); 
+//   d_paren << "))";
+//   out << d_paren.str();
+//   out << "\n";
+// }
+
+void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) {
+  for(IdSet::iterator it = d_seenLearnt.begin(); it!= d_seenLearnt.end(); ++it) {
     if(*it != d_emptyClauseId) {
-      printResolution(*it);
+      printResolution(*it, out, paren);
     }
   }
-  printAtoms(); 
-  // last resolution to be printed is the empty clause
-  printResolution(d_emptyClauseId);
-  
-  printClauses();
-  printVariables();
-  flush(out);
+  printResolution(d_emptyClauseId, out, paren);
 }
 
-void LFSCSatProof::printAtoms() {
-  d_atomsSS << "; Mapping between boolean variables and theory atoms \n"; 
-  for (AtomToVar::iterator it = d_atomToVar.begin(); it != d_atomToVar.end(); ++it) {
-    d_atomsSS << "; " << it->first << " => v" << var(it->second) << "\n"; 
-  }
-}
+// void LFSCSatProof::printVariables(std::ostream& out, std::ostream& paren) {
+//   for (VarSet::iterator it = d_seenVars.begin(); it != d_seenVars.end(); ++it) {
+//     out << "(% " << ProofManager::getVarPrefix() << *it <<" var \n";
+//     paren << ")"; 
+//   }
+// }
 
 
 } /* CVC4 namespace */