diff options
| -rw-r--r-- | src/proof/proof_manager.cpp | 4 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 6 |
2 files changed, 9 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()); } } } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 98eb81755..feed010e8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -100,9 +100,15 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori // During CNF conversion, conjunctions will be broken down into // multiple lemmas. In order for the recipes to match, we have to do // the same here. + + NodeManager* nm = NodeManager::currentNM(); + if (lemma.getKind() == kind::AND) { for (unsigned i = 0; i < lemma.getNumChildren(); ++i) registerLemmaRecipe(lemma[i], originalLemma, theoryId); + } else if (lemma.getKind() == kind::IFF) { + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1].negate()), originalLemma, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, theoryId); } // Theory lemmas have one step that proves the empty clause |