diff options
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r-- | src/proof/cnf_proof.cpp | 108 |
1 files changed, 67 insertions, 41 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 884a67856..19e9cbac9 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -1,13 +1,13 @@ /********************* */ /*! \file cnf_proof.cpp ** \verbatim - ** Original author: Liana Hadarean - ** Major contributors: Morgan Deters, Andrew Reynolds - ** Minor contributors (to current version): none + ** Top contributors (to current version): + ** Liana Hadarean, Guy Katz, Andrew Reynolds ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2014 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim + ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim ** ** \brief [[ Add one-line brief description here ]] ** @@ -16,22 +16,23 @@ **/ #include "proof/cnf_proof.h" -#include "proof/theory_proof.h" + +#include "proof/clause_id.h" #include "proof/proof_manager.h" -#include "prop/sat_solver_types.h" -#include "prop/minisat/minisat.h" +#include "proof/theory_proof.h" #include "prop/cnf_stream.h" - -using namespace CVC4::prop; +#include "prop/minisat/minisat.h" +#include "prop/sat_solver_types.h" namespace CVC4 { -CnfProof::CnfProof(CnfStream* stream, +CnfProof::CnfProof(prop::CnfStream* stream, context::Context* ctx, const std::string& name) : d_cnfStream(stream) , d_clauseToAssertion(ctx) , d_assertionToProofRule(ctx) + , d_clauseIdToOwnerTheory(ctx) , d_currentAssertionStack() , d_currentDefinitionStack() , d_clauseToDefinition(ctx) @@ -54,12 +55,13 @@ bool CnfProof::isDefinition(Node node) { return d_definitions.find(node) != d_definitions.end(); } - + ProofRule CnfProof::getProofRule(Node node) { Assert (isAssertion(node)); NodeToProofRule::iterator it = d_assertionToProofRule.find(node); return (*it).second; } + ProofRule CnfProof::getProofRule(ClauseId clause) { TNode assertion = getAssertionForClause(clause); return getProofRule(assertion); @@ -94,13 +96,14 @@ void CnfProof::registerConvertedClause(ClauseId clause, bool explanation) { Node current_assertion = getCurrentAssertion(); Node current_expr = getCurrentDefinition(); - + Debug("proof:cnf") << "CnfProof::registerConvertedClause " << clause << " assertion = " << current_assertion << clause << " definition = " << current_expr << std::endl; setClauseAssertion(clause, current_assertion); setClauseDefinition(clause, current_expr); + registerExplanationLemma(clause); } void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { @@ -112,7 +115,7 @@ void CnfProof::setClauseAssertion(ClauseId clause, Node expr) { // that since b is top level, it is not cached by the CnfStream) if (d_clauseToAssertion.find(clause) != d_clauseToAssertion.end()) return; - + d_clauseToAssertion.insert (clause, expr); } @@ -126,7 +129,7 @@ void CnfProof::setClauseDefinition(ClauseId clause, Node definition) { d_clauseToDefinition.insert(clause, definition); d_definitions.insert(definition); } - + void CnfProof::registerAssertion(Node assertion, ProofRule reason) { Debug("proof:cnf") << "CnfProof::registerAssertion " << assertion << " reason " << reason << std::endl; @@ -140,6 +143,16 @@ void CnfProof::registerAssertion(Node assertion, ProofRule reason) { d_assertionToProofRule.insert(assertion, reason); } +void CnfProof::registerExplanationLemma(ClauseId clauseId) { + d_clauseIdToOwnerTheory.insert(clauseId, getExplainerTheory()); +} + +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 @@ -158,10 +171,10 @@ void CnfProof::pushCurrentAssertion(Node assertion) { void CnfProof::popCurrentAssertion() { Assert (d_currentAssertionStack.size()); - + Debug("proof:cnf") << "CnfProof::popCurrentAssertion " << d_currentAssertionStack.back() << std::endl; - + d_currentAssertionStack.pop_back(); } @@ -170,6 +183,14 @@ 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::pushCurrentDefinition(Node definition) { Debug("proof:cnf") << "CnfProof::pushCurrentDefinition " << definition << std::endl; @@ -179,10 +200,10 @@ void CnfProof::pushCurrentDefinition(Node definition) { void CnfProof::popCurrentDefinition() { Assert (d_currentDefinitionStack.size()); - + Debug("proof:cnf") << "CnfProof::popCurrentDefinition " << d_currentDefinitionStack.back() << std::endl; - + d_currentDefinitionStack.pop_back(); } @@ -202,8 +223,8 @@ Node CnfProof::getAtom(prop::SatVariable var) { void CnfProof::collectAtoms(const prop::SatClause* clause, NodeSet& atoms) { for (unsigned i = 0; i < clause->size(); ++i) { - SatLiteral lit = clause->operator[](i); - SatVariable var = lit.getSatVariable(); + 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()); @@ -245,8 +266,8 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses, void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, std::ostream& os, std::ostream& paren) { - NodeSet::const_iterator it = atoms.begin(); - NodeSet::const_iterator end = atoms.end(); + NodeSet::const_iterator it = atoms.begin(); + NodeSet::const_iterator end = atoms.end(); for (;it != end; ++it) { os << "(decl_atom "; @@ -255,7 +276,7 @@ void LFSCCnfProof::printAtomMapping(const NodeSet& atoms, //FIXME hideous LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); pe->printLetTerm(atom.toExpr(), os); - + os << " (\\ " << ProofManager::getVarName(var, d_name) << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; paren << ")))"; @@ -295,9 +316,9 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, // paren << "))"; // return; - + Assert( clause->size()>0 ); - + Node base_assertion = getDefinitionForClause(id); //get the assertion for the clause id @@ -357,19 +378,19 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, std::stringstream os_paren; //eliminate each one for (int j = base_assertion.getNumChildren()-2; j >= 0; j--) { + Trace("cnf-pf-debug") << "; base_assertion[" << j << "] is: " << base_assertion[j] + << ", and its kind is: " << base_assertion[j].getKind() << std::endl ; + Node child_base = base_assertion[j].getKind()==kind::NOT ? base_assertion[j][0] : base_assertion[j]; bool child_pol = base_assertion[j].getKind()!=kind::NOT; - - if( j==0 && base_assertion.getKind()==kind::IMPLIES ){ - child_pol = !child_pol; - } - + Trace("cnf-pf-debug") << "; child " << j << " " - << child_base << " " - << child_pol << " " - << childPol[child_base] << std::endl; - + << ", child base: " << child_base + << ", child pol: " << child_pol + << ", childPol[child_base] " + << childPol[child_base] << ", base pol: " << base_pol << std::endl; + std::map< Node, unsigned >::iterator itcic = childIndex.find( child_base ); if( itcic!=childIndex.end() ){ @@ -377,7 +398,13 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, os_main << "(or_elim_1 _ _ "; prop::SatLiteral lit = (*clause)[itcic->second]; // Should be if in the original formula it was negated - if( childPol[child_base] && base_pol ){ + // if( childPol[child_base] && base_pol ){ + + // Adding the below to catch a specific case where the first child of an IMPLIES is negative, + // in which case we need not_not introduction. + if (base_assertion.getKind() == kind::IMPLIES && !child_pol && base_pol) { + os_main << "(not_not_intro _ " << ProofManager::getLitName(lit, d_name) << ") "; + } else if (childPol[child_base] && base_pol) { os_main << ProofManager::getLitName(lit, d_name) << " "; }else{ os_main << "(not_not_intro _ " << ProofManager::getLitName(lit, d_name) << ") "; @@ -391,6 +418,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, success = false; } } + if( success ){ if( base_assertion.getKind()==kind::IMPLIES ){ os_main << "(impl_elim _ _ "; @@ -420,7 +448,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, }else if ((base_assertion.getKind()==kind::AND && base_pol) || ((base_assertion.getKind()==kind::OR || base_assertion.getKind()==kind::IMPLIES) && !base_pol)) { - + std::stringstream os_main; Node iatom; @@ -431,7 +459,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id, Assert( assertion.getNumChildren()==1 ); iatom = assertion[0]; } - + Trace("cnf-pf") << "; and/or case 2, iatom = " << iatom << std::endl; Node e_base = iatom.getKind()==kind::NOT ? iatom[0] : iatom; bool e_pol = iatom.getKind()!=kind::NOT; @@ -729,6 +757,4 @@ bool LFSCCnfProof::printProofTopLevel(Node e, std::ostream& out) { } } - - } /* CVC4 namespace */ |