diff options
author | Guy <katz911@gmail.com> | 2016-07-27 09:46:24 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-27 09:46:24 -0700 |
commit | 9dd9a6f7cff50d6877a81675073a322730afad91 (patch) | |
tree | 548d4bb8535b6fd254b513138a2fe75e195724d5 /src/proof/proof_manager.cpp | |
parent | 6743ddb177b7b525d097bb94114a2c4c496ec8ba (diff) |
If we can't find a weaker implicant, fail gracefully and return the original lemma
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 65dbb644d..0e683b084 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -321,9 +321,10 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod // 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)) + continue; + recipe = getCnfProof()->getProofRecipe(lemma); if (recipe.simpleLemma() && recipe.getTheory() == theory) { lemmas.push_back(recipe.getOriginalLemma()); } @@ -368,9 +369,10 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) { // 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 (!getCnfProof()->haveProofRecipe(currentLemma)) + continue; + recipe = getCnfProof()->getProofRecipe(currentLemma); if (recipe.getOriginalLemma() == lemma) { for (lemmaIt = currentLemma.begin(); lemmaIt != currentLemma.end(); ++lemmaIt) { builder << *lemmaIt; @@ -381,12 +383,14 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) { if (lemma[i] == *lemmaIt) found = true; } - AlwaysAssert(found); + + if (!found) + return lemma; } } } - Assert(builder.getNumChildren() != 0); + AlwaysAssert(builder.getNumChildren() != 0); if (builder.getNumChildren() == 1) return builder[0]; |