From b539fb0692680c16247e3aa6e150457dd265f834 Mon Sep 17 00:00:00 2001 From: Guy Date: Thu, 28 Jul 2016 09:01:52 -0700 Subject: [PATCH] Add the negative conjunction case --- src/theory/theory_engine.cpp | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index e4b4756bf..bd0b467f2 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -112,9 +112,17 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori switch (lemma.getKind()) { case kind::AND: - Assert(!negated); // TODO - for (unsigned i = 0; i < lemma.getNumChildren(); ++i) - registerLemmaRecipe(lemma[i], originalLemma, false, theoryId); + if (!negated) { + for (unsigned i = 0; i < lemma.getNumChildren(); ++i) + registerLemmaRecipe(lemma[i], originalLemma, false, theoryId); + } else { + NodeBuilder<> builder(kind::OR); + for (unsigned i = 0; i < lemma.getNumChildren(); ++i) + builder << lemma[i].negate(); + + Node disjunction = (builder.getNumChildren() == 1) ? builder[0] : builder; + registerLemmaRecipe(disjunction, originalLemma, false, theoryId); + } break; case kind::IFF: -- 2.30.2