From: Guy <katz911@gmail.com>
Date: Wed, 27 Jul 2016 21:27:05 +0000 (-0700)
Subject: Proper handling of IFF lemmas in the unsat core.
X-Git-Tag: cvc5-1.0.0~6040^2~22
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f6372ac24cc635c7639f927b1bac64f015cbec88;p=cvc5.git

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 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