diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-10-07 22:49:45 -0400 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2013-10-07 22:54:01 -0400 |
commit | 867e79e0823c689889224078dfaebec03aee9730 (patch) | |
tree | b4c8281beda8f5263e32145e22dc58c7b1b8209a /src/proof/sat_proof.cpp | |
parent | 1a56238b7ed75c6127293cb7c52d5b6b85245c64 (diff) |
first draft implementation of uf proofs with holes
Diffstat (limited to 'src/proof/sat_proof.cpp')
-rw-r--r-- | src/proof/sat_proof.cpp | 270 |
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 */ |