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.cpp115
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 << "))";
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback