Proper handling of IFF lemmas in the unsat core.

Don't return duplicates in the unsat core

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index a0b25fab11d0babc25f5bd9075439a3449134747..a869919635262407ad191280c4a9653db6d2c6e3 100644 (file)
--- 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 98eb81755b546e14520718b1534383074f08fa2d..feed010e8d3ba42bb18f4a788214621353930097 100644 (file)
--- 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