fixed uf proof with holes bugs

1 files changed, 44 insertions, 31 deletions

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index caafa6b83..d73202147 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -41,33 +41,46 @@ void CnfProof::setTheoryProof(TheoryProof* theory_proof) {
   d_theoryProof = theory_proof; 
 }
 
-void CnfProof::addInputClause(ClauseId id, const ::Minisat::Clause& clause) {
-  d_inputClauses.insert(std::make_pair(id, clause)); 
-}
-
-void CnfProof::addTheoryLemma(ClauseId id, const ::Minisat::Clause& clause) {
-  d_theoryLemmas.insert(std::make_pair(id, clause)); 
+void CnfProof::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) {
+  for (unsigned i = 0; i < clause->size(); ++i) {
+    SatLiteral lit = clause->operator[](i); 
+    addVariable(lit.getSatVariable()); 
+  }
+  if (kind == INPUT) {
+    d_inputClauses.insert(std::make_pair(id, clause));
+    return;
+  }
+  Assert (kind == THEORY_LEMMA);
+  d_theoryLemmas.insert(std::make_pair(id, clause));
 }
 
-void CnfProof::addVariable(unsigned var) {
+void CnfProof::addVariable(prop::SatVariable var) {
   d_propVars.insert(var); 
-  Expr atom = getAtom(var);
+  Expr atom = getAtom(var); 
   getTheoryProof()->addAtom(atom); 
 }
 
-Expr CnfProof::getAtom(unsigned var) {
-  Minisat::Lit m_lit = Minisat::mkLit(var); 
-  prop::SatLiteral sat_lit = prop::MinisatSatSolver::toSatLiteral(m_lit); 
-  Expr atom = d_cnfStream->getNode(sat_lit).toExpr();
+Expr CnfProof::getAtom(prop::SatVariable var) {
+  prop::SatLiteral lit (var); 
+  Expr atom = d_cnfStream->getNode(lit).toExpr();
   return atom; 
 }
 
+CnfProof::~CnfProof() {
+  for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
+    delete it->second; 
+  }
+  for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) {
+    delete it->second; 
+  }
+}
+
 void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
   for (VarSet::iterator it = d_propVars.begin();it != d_propVars.end();  ++it) {
     Expr atom = getAtom(*it);
     os << "(decl_atom ";
     getTheoryProof()->printFormula(atom, os);
-    os << " (\\ " << ProofManager::getVarPrefix() <<*it << " (\\ " << ProofManager::getAtomPrefix() <<*it << "\n";
+    os << " (\\ " << ProofManager::printVarName(*it) << " (\\ " << ProofManager::printAtomName(*it) << "\n";
     paren << ")))"; 
   }
 }
@@ -78,44 +91,44 @@ void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
 }
 
 void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
+  os << " ;; Input Clauses \n";  
   for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
     ClauseId id = it->first;
-    const Minisat::Clause& clause = it->second;
-    os << " ;; input clause \n";  
+    const prop::SatClause* clause = it->second;
     os << "(satlem _ _ ";
     std::ostringstream clause_paren; 
-    printClause(clause, os, clause_paren);
+    printClause(*clause, os, clause_paren);
     os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getInputClausePrefix() << id <<"\n"; 
+    os << "( \\ " << ProofManager::printInputClauseName(id) << "\n"; 
     paren << "))"; 
   }
 }
 
 
 void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
-  for (IdToClause::const_iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
+  os << " ;; Theory Lemmas \n";  
+  for (IdToClause::const_iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) {
     ClauseId id = it->first;
-    const Minisat::Clause& clause = it->second;
-    os << " ;; theory lemma \n";  
+    const prop::SatClause* clause = it->second;
     os << "(satlem _ _ ";
     std::ostringstream clause_paren; 
-    printClause(clause, os, clause_paren);
+    printClause(*clause, os, clause_paren);
     os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getLemmaClausePrefix() << id <<"\n"; 
+    os << "( \\ " << ProofManager::printLemmaClauseName(id) <<"\n"; 
     paren << "))"; 
   }
 }
 
-void LFSCCnfProof::printClause(const Minisat::Clause& clause, std::ostream& os, std::ostream& paren) {
-  for (int i = 0; i < clause.size(); ++i) {
-    Minisat::Lit lit = clause[i];
-    unsigned var = Minisat::var(lit);
-    if (sign(lit)) {
-      os << "(asf _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " ";
-      paren << ")"; 
+void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) {
+  for (unsigned i = 0; i < clause.size(); ++i) {
+    prop::SatLiteral lit = clause[i];
+    prop::SatVariable var = lit.getSatVariable(); 
+    if (lit.isNegated()) {
+      os << "(ast _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " ";
+      paren << "))"; 
     } else {
-      os << "(ast _ _ _ " << ProofManager::getAtomPrefix()<< var <<" (\\ " << ProofManager::getLitPrefix() << Minisat::toInt(lit) << " ";
-      paren << ")"; 
+      os << "(asf _ _ _ " << ProofManager::printAtomName(var) <<" (\\ " << ProofManager::printLitName(lit) << " ";
+      paren << "))"; 
     }
   }
 }