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