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.h | |
parent | 08294c3914e4e87f3c5c1eda60e6ea259b789f55 (diff) |
Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index d5de8e3b2..db31ef9b7 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -292,18 +292,18 @@ class TheoryEngine { return d_engine->propagate(literal, d_theory); } - theory::LemmaStatus lemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { + theory::LemmaStatus lemma(TNode lemma, bool removable = false, bool preprocess = false) throw(TypeCheckingExceptionPrivate, AssertionException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable, theory::THEORY_LAST); + return d_engine->lemma(lemma, false, removable, preprocess, theory::THEORY_LAST); } theory::LemmaStatus splitLemma(TNode lemma, bool removable = false) throw(TypeCheckingExceptionPrivate, AssertionException) { Trace("theory::lemma") << "EngineOutputChannel<" << d_theory << ">::lemma(" << lemma << ")" << std::endl; ++ d_statistics.lemmas; d_engine->d_outputChannelUsed = true; - return d_engine->lemma(lemma, false, removable, d_theory); + return d_engine->lemma(lemma, false, removable, false, d_theory); } void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) { @@ -451,7 +451,7 @@ class TheoryEngine { * @param removable can the lemma be remove (restrictions apply) * @param needAtoms if not THEORY_LAST, then */ - theory::LemmaStatus lemma(TNode node, bool negated, bool removable, theory::TheoryId atomsTo); + theory::LemmaStatus lemma(TNode node, bool negated, bool removable, bool preprocess, theory::TheoryId atomsTo); /** Enusre that the given atoms are send to the given theory */ void ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId theory); |