diff options
author | Guy <katz911@gmail.com> | 2016-07-28 13:40:36 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-28 13:40:36 -0700 |
commit | 2bd04431e38dbbaad843a8f92ba730a6a7a86e53 (patch) | |
tree | fdc06e1c6d2006ea9919d77b47d5393134ace90a /src/proof | |
parent | 0ec7ff2ab463ea23c9c461d2544182744f688db6 (diff) |
The "aggressive" optimizer for lemma L now returns the conjunction of all lemmas L' that originated from L and were used in the unsat core
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/proof_manager.cpp | 54 |
1 files changed, 38 insertions, 16 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 3249ed19d..42319153f 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -380,24 +380,23 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) { 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)) - continue; + if (!options::aggressiveCoreMin()) { + 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)) + continue; - recipe = getCnfProof()->getProofRecipe(currentLemma); - if (recipe.getOriginalLemma() == lemma) { - for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) { - builder << *lemmaIt; + recipe = getCnfProof()->getProofRecipe(currentLemma); + if (recipe.getOriginalLemma() == lemma) { + for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) { + builder << *lemmaIt; - // Unless in aggressive mode, check that each conjunct appears in the original - // lemma. - if (!options::aggressiveCoreMin()) { + // Check that each conjunct appears in the original lemma. bool found = false; for (unsigned i = 0; i < lemma.getNumChildren(); ++i) { if (lemma[i] == *lemmaIt) @@ -409,6 +408,29 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) { } } } + } else { + // Aggressive mode + 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)) + continue; + + recipe = getCnfProof()->getProofRecipe(currentLemma); + if (recipe.getOriginalLemma() == lemma) { + NodeBuilder<> disjunction(kind::OR); + for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) { + disjunction << *lemmaIt; + } + + Node conjunct = (disjunction.getNumChildren() == 1) ? disjunction[0] : disjunction; + builder << conjunct; + } + } } AlwaysAssert(builder.getNumChildren() != 0); |