diff options
author | lianah <lianahady@gmail.com> | 2013-10-09 13:48:26 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-10-09 13:48:26 -0400 |
commit | 08c8433e4ab849024930a8c4dbe8756e13d08099 (patch) | |
tree | 2515d746c9b190e8770c5c690046410449900d7a /src/proof/sat_proof.cpp | |
parent | 000f574406c29df4c60947169ef527ee5316beb7 (diff) |
fixed uf proof bug: now storing deleted theory lemmas
Diffstat (limited to 'src/proof/sat_proof.cpp')
-rw-r--r-- | src/proof/sat_proof.cpp | 89 |
1 files changed, 15 insertions, 74 deletions
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp index e8c63bb74..e1534a635 100644 --- a/src/proof/sat_proof.cpp +++ b/src/proof/sat_proof.cpp @@ -621,32 +621,20 @@ 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); + d_deleted.insert(id); + if (isLemmaClause(id)) { + const Clause& minisat_cl = getClause(clause); + SatClause* sat_cl = new SatClause(); + MinisatSatSolver::toSatClause(minisat_cl, *sat_cl); + d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); + } } } void SatProof::constructProof() { - // if (isLemmaClause(d_conflictId)) { - // addClauseToCnfProof(d_emptyClauseId, THEORY_LEMMA); - // } - // if (isInputClause(d_emptyClauseId)) { - // addClauseToCnfProof(d_emptyClauseId, INPUT); - // } 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(); -// } - - std::string SatProof::clauseName(ClauseId id) { ostringstream os; if (isInputClause(id)) { @@ -671,6 +659,14 @@ void SatProof::addClauseToCnfProof(ClauseId id, ClauseKind kind) { getCnfProof()->addClause(id, clause, kind); return; } + + if (isDeleted(id)) { + Assert (kind == THEORY_LEMMA); + SatClause* clause = d_deletedTheoryLemmas.find(id)->second; + getCnfProof()->addClause(id, clause, kind); + return; + } + CRef ref = getClauseRef(id); const Clause& minisat_cl = getClause(ref); SatClause* clause = new SatClause(); @@ -748,54 +744,6 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& 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; -// } - -// 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) { @@ -805,13 +753,6 @@ void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) { printResolution(d_emptyClauseId, out, paren); } -// 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 */ |