diff options
author | Guy <katz911@gmail.com> | 2016-07-28 09:01:52 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-28 09:01:52 -0700 |
commit | b539fb0692680c16247e3aa6e150457dd265f834 (patch) | |
tree | 599c47048a537b2d4ac72764564ee7ab71836654 /src | |
parent | 4835c73a86d00bf20a88b9fc71964ac13ca08ef0 (diff) |
Add the negative conjunction case
Diffstat (limited to 'src')
-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: |