diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 14 |
1 files 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: |