diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-02-17 18:59:39 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-04 07:56:20 -0500 |
commit | ed87e0c1ccb0cb93cdedf5229c6a2b47af77743c (patch) | |
tree | b7c0efe878b82e6aff545b1d2fd52a02120f5813 /src/theory/theory_engine.cpp | |
parent | 08294c3914e4e87f3c5c1eda60e6ea259b789f55 (diff) |
Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 17 |
1 files changed, 10 insertions, 7 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 63024e5d5..c29177b49 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -475,7 +475,7 @@ void TheoryEngine::combineTheories() { // We need to split on it Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << endl; - lemma(equality.orNode(equality.notNode()), false, false, carePair.theory); + lemma(equality.orNode(equality.notNode()), false, false, false, carePair.theory); } } @@ -779,7 +779,7 @@ Node TheoryEngine::ppTheoryRewrite(TNode term) { Node newTerm; if (theoryOf(term)->ppDontRewriteSubterm(term)) { - newTerm = term; + newTerm = Rewriter::rewrite(term); } else { NodeBuilder<> newNode(term.getKind()); if (term.getMetaKind() == kind::metakind::PARAMETERIZED) { @@ -1320,7 +1320,7 @@ void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::The } } -theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, theory::TheoryId atomsTo) { +theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo) { // Do we need to check atoms if (atomsTo != theory::THEORY_LAST) { @@ -1344,15 +1344,18 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable options::lemmaOutputChannel()->notifyNewLemma(node.toExpr()); } + // Run theory preprocessing, maybe + Node ppNode = preprocess ? this->preprocess(node) : Node(node); + // Remove the ITEs std::vector<Node> additionalLemmas; IteSkolemMap iteSkolemMap; - additionalLemmas.push_back(node); + additionalLemmas.push_back(ppNode); d_iteRemover.run(additionalLemmas, iteSkolemMap); additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]); if(Debug.isOn("lemma-ites")) { - Debug("lemma-ites") << "removed ITEs from lemma: " << node << endl; + Debug("lemma-ites") << "removed ITEs from lemma: " << ppNode << endl; Debug("lemma-ites") << " + now have the following " << additionalLemmas.size() << " lemma(s):" << endl; for(std::vector<Node>::const_iterator i = additionalLemmas.begin(); @@ -1417,11 +1420,11 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) { Node fullConflict = mkExplanation(explanationVector); Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl; Assert(properConflict(fullConflict)); - lemma(fullConflict, true, true, THEORY_LAST); + lemma(fullConflict, true, true, false, THEORY_LAST); } else { // When only one theory, the conflict should need no processing Assert(properConflict(conflict)); - lemma(conflict, true, true, THEORY_LAST); + lemma(conflict, true, true, false, THEORY_LAST); } } |