diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/proof/cnf_proof.cpp | |
parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r-- | src/proof/cnf_proof.cpp | 115 |
1 files changed, 26 insertions, 89 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index abe48e3cd..19e9cbac9 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -19,7 +19,6 @@ #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" @@ -33,6 +32,7 @@ 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,6 +103,7 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { setClauseAssertion(clause, current_assertion); setClauseDefinition(clause, current_expr); + registerExplanationLemma(clause); } void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { @@ -142,15 +143,16 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) { d_assertionToProofRule.insert(assertion, reason); } -LemmaProofRecipe CnfProof::getProofRecipe(const std::set<Node> &lemma) { - Assert(d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end()); - return d_lemmaToProofRecipe[lemma]; +void CnfProof::registerExplanationLemma(ClauseId clauseId) { + d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory()); } -bool CnfProof::haveProofRecipe(const std::set<Node> &lemma) { - return d_lemmaToProofRecipe.find(lemma) != d_lemmaToProofRecipe.end(); +theory::TheoryId CnfProof::getOwnerTheory(ClauseId clause) { + Assert(d_clauseIdToOwnerTheory.find(clause) != d_clauseIdToOwnerTheory.end()); + return d_clauseIdToOwnerTheory[clause]; } + void CnfProof::setCnfDependence(Node from, Node to) { Debug("proof:cnf") << "CnfProof::setCnfDependence " << "from " << from << std::endl @@ -181,10 +183,12 @@ Node CnfProof::getCurrentAssertion() { return d_currentAssertionStack.back(); } -void CnfProof::setProofRecipe(LemmaProofRecipe* proofRecipe) { - Assert(proofRecipe); - Assert(proofRecipe->getNumSteps() > 0); - d_lemmaToProofRecipe[proofRecipe->getBaseAssertions()] = *proofRecipe; +void CnfProof::setExplainerTheory(theory::TheoryId theory) { + d_explainerTheory = theory; +} + +theory::TheoryId CnfProof::getExplainerTheory() { + return d_explainerTheory; } void CnfProof::pushCurrentDefinition(Node definition) { @@ -208,19 +212,22 @@ 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, - std::set<Node>& atoms) { + NodeSet& 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); } } @@ -230,75 +237,14 @@ 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, - std::set<Node>& atoms) { + NodeSet& atom_map) { IdToSatClause::const_iterator it = clauses.begin(); for (; it != clauses.end(); ++it) { const prop::SatClause* clause = it->second; - collectAtoms(clause, atoms); + collectAtoms(clause, atom_map); } -} - -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, @@ -317,13 +263,13 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, } } -void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms, +void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren) { - std::set<Node>::const_iterator it = atoms.begin(); - std::set<Node>::const_iterator end = atoms.end(); + NodeSet::const_iterator it = atoms.begin(); + NodeSet::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(); @@ -331,8 +277,8 @@ void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms, LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); pe->printLetTerm(atom.toExpr(), os); - os << " (\\ " << ProofManager::getVarName(var, d_name); - os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; + os << " (\\ " << ProofManager::getVarName(var, d_name) + << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; paren << ")))"; } } @@ -358,9 +304,6 @@ 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); @@ -393,10 +336,6 @@ 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; @@ -625,7 +564,6 @@ 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 ); @@ -724,7 +662,6 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, os << ")" << clause_paren.str() << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n"; - paren << "))"; } |