summaryrefslogtreecommitdiff
path: root/src/proof/cnf_proof.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/cnf_proof.cpp')
-rw-r--r--src/proof/cnf_proof.cpp108
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback