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/theory/theory_engine.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/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
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 |