diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:46:24 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:46:24 -0700 |
commit | 4dac1ec234ee0d0885f058b4b35a7eeba2ca5007 (patch) | |
tree | aae1792c05c0a67c521160226deb451ca861822c /src/proof/cnf_proof.cpp | |
parent | de0dd1dc966b05467f1a5443ff33094262f5076a (diff) |
Merge from proof branch
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r-- | src/proof/cnf_proof.cpp | 115 |
1 files changed, 89 insertions, 26 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 19e9cbac9..abe48e3cd 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -19,6 +19,7 @@ #include "proof/clause_id.h" #include "proof/proof_manager.h" +#include "proof/proof_utils.h" #include "proof/theory_proof.h" #include "prop/cnf_stream.h" #include "prop/minisat/minisat.h" @@ -32,7 +33,6 @@ CnfProof::CnfProof(prop::CnfStream* stream, : d_cnfStream(stream) , d_clauseToAssertion(ctx) , d_assertionToProofRule(ctx) - , d_clauseIdToOwnerTheory(ctx) , d_currentAssertionStack() , d_currentDefinitionStack() , d_clauseToDefinition(ctx) @@ -103,7 +103,6 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { setClauseAssertion(clause, current_assertion); setClauseDefinition(clause, current_expr); - registerExplanationLemma(clause); } void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { @@ -143,16 +142,15 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) { d_assertionToProofRule.insert(assertion, reason); } -void CnfProof::registerExplanationLemma(ClauseId clauseId) { - d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory()); +LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) { + Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end()); + return d_lemmaToProofRecipe[lemma]; } -theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) { - Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end()); - return d_clauseIdToOwnerTheory[clause]; +bool CnfProof::haveProofRecipe(const std::set<Node> &lemma) { + return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end(); } - void CnfProof::setCnfDependence(Node from, Node to) { Debug("proof:cnf") << "CnfProof::setCnfDependence " << "from " << from << std::endl @@ -183,12 +181,10 @@ Node CnfProof::getCurrentAssertion() { return d_currentAssertionStack.back(); } -void CnfProof::setExplainerTheory(theory::TheoryId theory) { - d_explainerTheory = theory; -} - -theory::TheoryId CnfProof::getExplainerTheory() { - return d_explainerTheory; +void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) { + Assert(proofRecipe); + Assert(proofRecipe->getNumSteps() > 0); + d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe; } void CnfProof::pushCurrentDefinition(Node definition) { @@ -212,22 +208,19 @@ Node CnfProof::getCurrentDefinition() { return d_currentDefinitionStack.back(); } - Node CnfProof::getAtom(prop::SatVariable var) { prop::SatLiteral lit (var); Node node = d_cnfStream->getNode(lit); return node; } - void CnfProof::collectAtoms(const prop::SatClause* clause, - NodeSet& atoms) { + std::set<Node>& atoms) { for (unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = clause->operator[](i); prop::SatVariable var = lit.getSatVariable(); TNode atom = getAtom(var); if (atoms.find(atom) == atoms.end()) { - Assert (atoms.find(atom) == atoms.end()); atoms.insert(atom); } } @@ -237,14 +230,75 @@ prop::SatLiteral CnfProof::getLiteral(TNode atom) { return d_cnfStream->getLiteral(atom); } +bool CnfProof::hasLiteral(TNode atom) { + return d_cnfStream->hasLiteral(atom); +} + +void CnfProof::ensureLiteral(TNode atom, bool noPreregistration) { + d_cnfStream->ensureLiteral(atom, noPreregistration); +} + void CnfProof::collectAtomsForClauses(const IdToSatClause& clauses, - NodeSet& atom_map) { + std::set<Node>& atoms) { IdToSatClause::const_iterator it = clauses.begin(); for (; it != clauses.end(); ++it) { const prop::SatClause* clause = it->second; - collectAtoms(clause, atom_map); + collectAtoms(clause, atoms); } +} + +void CnfProof::collectAtomsAndRewritesForLemmas(const IdToSatClause& lemmaClauses, + std::set<Node>& atoms, + NodePairSet& rewrites) { + IdToSatClause::const_iterator it = lemmaClauses.begin(); + for (; it != lemmaClauses.end(); ++it) { + const prop::SatClause* clause = it->second; + + // TODO: just calculate the map from ID to recipe once, + // instead of redoing this over and over again + std::vector<Expr> clause_expr; + std::set<Node> clause_expr_nodes; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Node node = getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue()); + continue; + } + clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node); + } + + LemmaProofRecipe recipe = getProofRecipe(clause_expr_nodes); + for (unsigned i = 0; i < recipe.getNumSteps(); ++i) { + const LemmaProofRecipe::ProofStep* proofStep = recipe.getStep(i); + Node atom = proofStep->getLiteral(); + + if (atom == Node()) { + // The last proof step always has the empty node as its target... + continue; + } + + if (atom.getKind() == kind::NOT) { + atom = atom[0]; + } + + atoms.insert(atom); + } + + LemmaProofRecipe::RewriteIterator rewriteIt; + for (rewriteIt = recipe.rewriteBegin(); rewriteIt != recipe.rewriteEnd(); ++rewriteIt) { + rewrites.insert(NodePair(rewriteIt->first, rewriteIt->second)); + + // The unrewritten terms also need to have literals, so insert them into atoms + Node rewritten = rewriteIt->first; + if (rewritten.getKind() == kind::NOT) { + rewritten = rewritten[0]; + } + atoms.insert(rewritten); + } + } } void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, @@ -263,13 +317,13 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, } } -void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, +void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms, std::ostream& os, std::ostream& paren) { - NodeSet::const_iterator it = atoms.begin(); - NodeSet::const_iterator end = atoms.end(); + std::set<Node>::const_iterator it = atoms.begin(); + std::set<Node>::const_iterator end = atoms.end(); - for (;it != end; ++it) { + for (;it != end; ++it) { os << "(decl_atom "; Node atom = *it; prop::SatVariable var = getLiteral(atom).getSatVariable(); @@ -277,8 +331,8 @@ void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); pe->printLetTerm(atom.toExpr(), os); - os << " (\\ " << ProofManager::getVarName(var, d_name) - << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; + os << " (\\ " << ProofManager::getVarName(var, d_name); + os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; paren << ")))"; } } @@ -304,6 +358,9 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, const prop::SatClause* clause, std::ostream& os, std::ostream& paren) { + Debug("cnf-pf") << std::endl << std::endl << "LFSCCnfProof::printCnfProofForClause( " << id << " ) starting " + << std::endl; + os << "(satlem _ _ "; std::ostringstream clause_paren; printClause(*clause, os, clause_paren); @@ -336,6 +393,10 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, // and prints the proof of the top-level formula bool is_input = printProofTopLevel(base_assertion, os_base); + if (is_input) { + Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl; + } + //get base assertion with polarity bool base_pol = base_assertion.getKind()!=kind::NOT; base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion; @@ -564,6 +625,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, if( !pols[0] || num_nots_1==1 ){ os_base_n << "(not_not_intro _ " << ProofManager::getLitName(lit1, d_name) << ") "; }else{ + Trace("cnf-pf-debug") << "CALLING getlitname" << std::endl; os_base_n << ProofManager::getLitName(lit1, d_name) << " "; } Assert( elimNum!=0 ); @@ -662,6 +724,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, os << ")" << clause_paren.str() << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n"; + paren << "))"; } |