diff options
author | Guy <katz911@gmail.com> | 2016-07-27 19:03:13 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-07-27 19:03:13 -0700 |
commit | 4835c73a86d00bf20a88b9fc71964ac13ca08ef0 (patch) | |
tree | 2999778fffe76ff7b940dc88f7b09b8250eba7cf | |
parent | 9242c63ff2564612f7ea719c3bd735be7c68bc00 (diff) |
Proper instrumentation of the preprocessing phase
-rw-r--r-- | src/theory/theory_engine.cpp | 26 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 2 |
2 files changed, 15 insertions, 13 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 123b0bffc..e4b4756bf 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -84,7 +84,7 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, d_engine->d_outputChannelUsed = true; PROOF({ - registerLemmaRecipe(lemma, lemma, d_theory); + registerLemmaRecipe(lemma, lemma, preprocess, d_theory); }); theory::LemmaStatus result = d_engine->lemma(lemma, @@ -96,13 +96,15 @@ theory::LemmaStatus TheoryEngine::EngineOutputChannel::lemma(TNode lemma, return result; } -void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node originalLemma, theory::TheoryId theoryId) { +void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, theory::TheoryId theoryId) { // During CNF conversion, conjunctions will be broken down into // multiple lemmas. In order for the recipes to match, we have to do // the same here. - NodeManager* nm = NodeManager::currentNM(); + if (preprocess) + lemma = d_engine->preprocess(lemma); + bool negated = (lemma.getKind() == kind::NOT); if (negated) lemma = lemma[0]; @@ -112,26 +114,26 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori case kind::AND: Assert(!negated); // TODO for (unsigned i = 0; i < lemma.getNumChildren(); ++i) - registerLemmaRecipe(lemma[i], originalLemma, theoryId); + registerLemmaRecipe(lemma[i], originalLemma, false, 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); + 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); } 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); + 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); } 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); + 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); } 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); + 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); } break; diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ea8628f9c..9316066a5 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -328,7 +328,7 @@ class TheoryEngine { /** * A helper function for registering lemma recipes with the proof engine */ - void registerLemmaRecipe(Node lemma, Node originalLemma, theory::TheoryId theoryId); + void registerLemmaRecipe(Node lemma, Node originalLemma, bool preprocess, theory::TheoryId theoryId); };/* class TheoryEngine::EngineOutputChannel */ /** |