diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-01 14:55:19 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-01 14:55:19 -0600 |
| commit | c48548ea68b6241bee2cb9393ef2710c5803fb06 (patch) | |
| tree | 044b335f3ea83baef89207c49c0cd5da227ecaa8 /src/theory/quantifiers_engine.cpp | |
| parent | eac7249ef4e35ad8c37f36098c228965f71a319b (diff) | |
Eliminate PREPROCESS lemma property (#5827)
This is now possible since we always preprocess lemmas.
Note that the LemmaProperty on inferences may be redundant throughout the non-linear solver now.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 2cc904ed1..6338c30b3 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -781,8 +781,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } - getOutputChannel().trustedLemma( - lem, LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY); + getOutputChannel().trustedLemma(lem, LemmaProperty::NEEDS_JUSTIFY); } return; } @@ -947,8 +946,7 @@ void QuantifiersEngine::flushLemmas(){ const Node& lemw = d_lemmas_waiting[i]; Trace("qe-lemma") << "Lemma : " << lemw << std::endl; itp = d_lemmasWaitingPg.find(lemw); - LemmaProperty p = - LemmaProperty::PREPROCESS | LemmaProperty::NEEDS_JUSTIFY; + LemmaProperty p = LemmaProperty::NEEDS_JUSTIFY; if (itp != d_lemmasWaitingPg.end()) { TrustNode tlemw = TrustNode::mkTrustLemma(lemw, itp->second); |