diff options
author | Guy <katz911@gmail.com> | 2016-07-28 11:24:07 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-28 11:24:07 -0700 |
commit | fff97c76bc1ba86594114ea91ba6b23944964f55 (patch) | |
tree | abe9eb6c80bf0ee59257f597ba612a6137d0d4df /src/theory/theory_engine.cpp | |
parent | b539fb0692680c16247e3aa6e150457dd265f834 (diff) |
Bug fix involving negated lemmas
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 29 |
1 files changed, 14 insertions, 15 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index bd0b467f2..94281156f 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -106,19 +106,18 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori lemma = d_engine->preprocess(lemma); bool negated = (lemma.getKind() == kind::NOT); - if (negated) - lemma = lemma[0]; + Node nnLemma = negated ? lemma[0] : lemma; - switch (lemma.getKind()) { + switch (nnLemma.getKind()) { case kind::AND: if (!negated) { - for (unsigned i = 0; i < lemma.getNumChildren(); ++i) - registerLemmaRecipe(lemma[i], originalLemma, false, theoryId); + for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) + registerLemmaRecipe(nnLemma[i], originalLemma, false, theoryId); } else { NodeBuilder<> builder(kind::OR); - for (unsigned i = 0; i < lemma.getNumChildren(); ++i) - builder << lemma[i].negate(); + for (unsigned i = 0; i < nnLemma.getNumChildren(); ++i) + builder << nnLemma[i].negate(); Node disjunction = (builder.getNumChildren() == 1) ? builder[0] : builder; registerLemmaRecipe(disjunction, originalLemma, false, theoryId); @@ -127,21 +126,21 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori case kind::IFF: if (!negated) { - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1].negate()), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId); } else { - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1]), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[1]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId); } break; case kind::ITE: if (!negated) { - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1]), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2]), originalLemma, false, theoryId); } else { - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1].negate()), originalLemma, false, theoryId); - registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[2].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0].negate(), nnLemma[1].negate()), originalLemma, false, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, nnLemma[0], nnLemma[2].negate()), originalLemma, false, theoryId); } break; |