From: Guy Date: Thu, 28 Jul 2016 20:40:36 +0000 (-0700) Subject: The "aggressive" optimizer for lemma L now returns the conjunction of all lemmas... X-Git-Tag: cvc5-1.0.0~6040^2~16 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2bd04431e38dbbaad843a8f92ba730a6a7a86e53;p=cvc5.git 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 --- 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::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)) - continue; + if (!options::aggressiveCoreMin()) { + 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)) + 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 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);