From 9242c63ff2564612f7ea719c3bd735be7c68bc00 Mon Sep 17 00:00:00 2001 From: Guy Date: Wed, 27 Jul 2016 18:17:41 -0700 Subject: [PATCH] proper handling of ITEs --- src/theory/theory_engine.cpp | 36 ++++++++++++++++++++++++++++++++---- 1 file changed, 32 insertions(+), 4 deletions(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index feed010e8..123b0bffc 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -103,12 +103,40 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori NodeManager* nm = NodeManager::currentNM(); - if (lemma.getKind() == kind::AND) { + bool negated = (lemma.getKind() == kind::NOT); + if (negated) + lemma = lemma[0]; + + switch (lemma.getKind()) { + + case kind::AND: + Assert(!negated); // TODO 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); + break; + + case kind::IFF: + if (!negated) { + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1].negate()), originalLemma, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, theoryId); + } else { + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1]), originalLemma, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, theoryId); + } + break; + + case kind::ITE: + if (!negated) { + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2]), originalLemma, theoryId); + } else { + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2].negate()), originalLemma, theoryId); + } + break; + + default: + break; } // Theory lemmas have one step that proves the empty clause -- 2.30.2