diff options
author | Guy <katz911@gmail.com> | 2016-07-26 13:09:31 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-26 13:09:31 -0700 |
commit | 319bbda7ad32e6e9ee009c27003f6f1c0a8d7b20 (patch) | |
tree | 9648cdfb58b5f132d9a40a919dac792ad6da3c34 /src/proof/proof_manager.cpp | |
parent | cb835bd526296d97f8ceb001569493723a59f86b (diff) |
Added functionality to retrieve a lemma's "weakest implicant" in the unsat core. Currently, lemmas that are not conjunctions and their own weakest implicants; but for lemmas that *are* conjunctions, we may return only a subset of the conjuncts.
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 94 |
1 files changed, 79 insertions, 15 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 835990613..1b4fbcc47 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -271,7 +271,7 @@ void ProofManager::traceDeps(TNode n) { void ProofManager::traceUnsatCore() { Assert (options::unsatCores()); - d_satProof->constructProof(); + constructSatProof(); IdToSatClause used_lemmas; IdToSatClause used_inputs; d_satProof->collectClausesUsed(used_inputs, @@ -296,11 +296,17 @@ bool ProofManager::unsatCoreAvailable() const { return d_satProof->derivedEmptyClause(); } +void ProofManager::constructSatProof() { + if (!d_satProof->proofConstructed()) { + d_satProof->constructProof(); + } +} + void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas) { Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off"); Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" ); - d_satProof->constructProof(); + constructSatProof(); IdToSatClause used_lemmas; IdToSatClause used_inputs; @@ -309,24 +315,14 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod IdToSatClause::const_iterator it; for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) { - std::set<Node> lemma; - for(unsigned i = 0; i < it->second->size(); ++i) { - prop::SatLiteral lit = (*(it->second))[i]; - Node node = getCnfProof()->getAtom(lit.getSatVariable()); - Expr atom = node.toExpr(); - if (atom.isConst()) { - Assert (atom == utils::mkTrue()); - continue; - } - lemma.insert(lit.isNegated() ? node.notNode() : node); - } + std::set<Node> lemma = satClauseToNodeSet(it->second); // TODO: we should be able to drop the "haveProofRecipe" check. // however, there are some rewrite issues with the arith solver, resulting // in non-registered recipes. For now we assume no one is requesting arith lemmas. LemmaProofRecipe recipe; - if ( getCnfProof()->haveProofRecipe(lemma) ) - recipe = getCnfProof()->getProofRecipe(lemma); + if (getCnfProof()->haveProofRecipe(lemma)) + recipe = getCnfProof()->getProofRecipe(lemma); if (recipe.simpleLemma() && recipe.getTheory() == theory) { lemmas.push_back(recipe.getOriginalLemma()); @@ -334,6 +330,73 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod } } +std::set<Node> ProofManager::satClauseToNodeSet(prop::SatClause* clause) { + std::set<Node> result; + for (unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Node node = getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue()); + continue; + } + result.insert(lit.isNegated() ? node.notNode() : node); + } + + return result; +} + +Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) { + Assert(PROOF_ON(), "Cannot compute unsat core when proofs are off"); + Assert(unsatCoreAvailable(), "Cannot get unsat core at this time. Mabye the input is SAT?" ); + + if (lemma.getKind() != kind::AND) + return lemma; + + constructSatProof(); + + NodeBuilder<> builder(kind::AND); + + IdToSatClause used_lemmas; + IdToSatClause used_inputs; + d_satProof->collectClausesUsed(used_inputs, used_lemmas); + + IdToSatClause::const_iterator it; + std::set<Node>::iterator lemmaIt; + + for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) { + std::set<Node> currentLemma = satClauseToNodeSet(it->second); + + // TODO: we should be able to drop the "haveProofRecipe" check. + // however, there are some rewrite issues with the arith solver, resulting + // in non-registered recipes. For now we assume no one is requesting arith lemmas. + LemmaProofRecipe recipe; + if (getCnfProof()->haveProofRecipe(currentLemma)) + recipe = getCnfProof()->getProofRecipe(currentLemma); + + if (recipe.getOriginalLemma() == lemma) { + for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) { + builder << *lemmaIt; + + // Sanity check: make sure that each conjunct really appears in the original lemma + bool found = false; + for (unsigned i = 0; i < lemma.getNumChildren(); ++i) { + if (lemma[i] == *lemmaIt) + found = true; + } + Assert(found); + } + } + } + + Assert(builder.getNumChildren() != 0); + + if (builder.getNumChildren() == 1) + return builder[0]; + + return builder; +} + void ProofManager::addAssertion(Expr formula) { Debug("proof:pm") << "assert: " << formula << std::endl; d_inputFormulas.insert(formula); @@ -385,6 +448,7 @@ void LFSCProof::toStream(std::ostream& out) { Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); + Assert(!d_satProof->proofConstructed()); d_satProof->constructProof(); // collecting leaf clauses in resolution proof |