diff options
author | Guy <katz911@gmail.com> | 2016-07-27 14:27:05 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-27 14:27:05 -0700 |
commit | f6372ac24cc635c7639f927b1bac64f015cbec88 (patch) | |
tree | f22fad4a894374f0927c110d7688e52f423687da /src/proof/proof_manager.cpp | |
parent | 6e5f92fe7c71fdbd11f28a11071bd3d37e429c82 (diff) |
Proper handling of IFF lemmas in the unsat core.
Don't return duplicates in the unsat core
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index a0b25fab1..a86991963 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -313,6 +313,7 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod d_satProof->collectClausesUsed(used_inputs, used_lemmas); IdToSatClause::const_iterator it; + std::set<Node> seen; for (it = used_lemmas.begin(); it != used_lemmas.end(); ++it) { std::set<Node> lemma = satClauseToNodeSet(it->second); @@ -325,8 +326,9 @@ void ProofManager::getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Nod continue; recipe = getCnfProof()->getProofRecipe(lemma); - if (recipe.simpleLemma() && recipe.getTheory() == theory) { + if (recipe.simpleLemma() && recipe.getTheory() == theory && seen.find(recipe.getOriginalLemma()) == seen.end()) { lemmas.push_back(recipe.getOriginalLemma()); + seen.insert(recipe.getOriginalLemma()); } } } |