From f6372ac24cc635c7639f927b1bac64f015cbec88 Mon Sep 17 00:00:00 2001 From: Guy Date: Wed, 27 Jul 2016 14:27:05 -0700 Subject: Proper handling of IFF lemmas in the unsat core. Don't return duplicates in the unsat core --- src/theory/theory_engine.cpp | 6 ++++++ 1 file changed, 6 insertions(+) (limited to 'src/theory/theory_engine.cpp') 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 -- cgit v1.2.3