From 319bbda7ad32e6e9ee009c27003f6f1c0a8d7b20 Mon Sep 17 00:00:00 2001 From: Guy Date: Tue, 26 Jul 2016 13:09:31 -0700 Subject: [PATCH] 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. --- src/proof/proof_manager.cpp | 94 +++++++++++++++++++++++----- src/proof/proof_manager.h | 5 ++ src/proof/sat_proof.h | 4 +- src/proof/sat_proof_implementation.h | 7 +++ 4 files changed, 94 insertions(+), 16 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 &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 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 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 ProofManager::satClauseToNodeSet(prop::SatClause* clause) { + std::set 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::iterator lemmaIt; + + for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) { + std::set 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 diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h index b1cfc54b5..23d7d1972 100644 --- a/src/proof/proof_manager.h +++ b/src/proof/proof_manager.h @@ -248,6 +248,7 @@ public: bool unsatCoreAvailable() const; void getLemmasInUnsatCore(theory::TheoryId theory, std::vector &lemmas); + Node getWeakestImplicantInUnsatCore(Node lemma); int nextId() { return d_nextId++; } @@ -271,6 +272,10 @@ public: ProofLetMap& letMap, std::ostream& out, std::ostringstream& paren); + +private: + void constructSatProof(); + std::set satClauseToNodeSet(prop::SatClause* clause); };/* class ProofManager */ class LFSCProof : public Proof { diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h index c571a7b06..52e059e95 100644 --- a/src/proof/sat_proof.h +++ b/src/proof/sat_proof.h @@ -198,6 +198,7 @@ class TSatProof { */ void constructProof(ClauseId id); void constructProof() { constructProof(d_emptyClauseId); } + bool proofConstructed() const; void collectClauses(ClauseId id); bool derivedEmptyClause() const; prop::SatClause* buildClause(ClauseId id); @@ -355,7 +356,7 @@ class TSatProof { IdToSatClause d_seenInputs; IdToSatClause d_seenLemmas; - private: + private: __gnu_cxx::hash_map d_glueMap; struct Statistics { IntStat d_numLearnedClauses; @@ -370,6 +371,7 @@ class TSatProof { ~Statistics(); }; + bool d_satProofConstructed; Statistics d_statistics; }; /* class TSatProof */ diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index cd2473937..fc2bae19b 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -224,6 +224,7 @@ TSatProof::TSatProof(Solver* solver, const std::string& name, d_seenLearnt(), d_seenInputs(), d_seenLemmas(), + d_satProofConstructed(false), d_statistics(name) { d_proxy = new ProofProxy(this); } @@ -957,9 +958,15 @@ void TSatProof::markDeleted(typename Solver::TCRef clause) { template void TSatProof::constructProof(ClauseId conflict) { + d_satProofConstructed = true; collectClauses(conflict); } +template +bool TSatProof::proofConstructed() const { + return d_satProofConstructed; +} + template std::string TSatProof::clauseName(ClauseId id) { std::ostringstream os; -- 2.30.2