diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-28 11:03:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-28 11:03:33 -0500 |
| commit | c38f35164adc5ab255803765a568ef820fa8f3b2 (patch) | |
| tree | 6cbd4b21e8e9ff364b5b2f14467cd986ea69acf2 /src/theory/quantifiers_engine.cpp | |
| parent | b90cfb462bde3e75c07bb14e2393ee8e4b4f4d42 (diff) | |
Use lemma property enum for OutputChannel::lemma (#4755)
There are 3 Boolean flags for OutputChannel::lemma, and plans to add another for relevance.
This makes them into a enum.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 6dcf1a980..bb5950c5e 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -970,7 +970,7 @@ void QuantifiersEngine::assertQuantifier( Node f, bool pol ){ Trace("quantifiers-sk-debug") << "Skolemize lemma : " << slem << std::endl; } - getOutputChannel().lemma(lem, false, true); + getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); } return; } @@ -1021,7 +1021,6 @@ bool QuantifiersEngine::addLemma( Node lem, bool doCache, bool doRewrite ){ Trace("inst-add-debug") << "Adding lemma : " << lem << std::endl; BoolMap::const_iterator itp = d_lemmas_produced_c.find( lem ); if( itp==d_lemmas_produced_c.end() || !(*itp).second ){ - //d_curr_out->lemma( lem, false, true ); d_lemmas_produced_c[ lem ] = true; d_lemmas_waiting.push_back( lem ); Trace("inst-add-debug") << "Added lemma" << std::endl; @@ -1122,7 +1121,7 @@ void QuantifiersEngine::flushLemmas(){ d_hasAddedLemma = true; for( unsigned i=0; i<d_lemmas_waiting.size(); i++ ){ Trace("qe-lemma") << "Lemma : " << d_lemmas_waiting[i] << std::endl; - getOutputChannel().lemma( d_lemmas_waiting[i], false, true ); + getOutputChannel().lemma(d_lemmas_waiting[i], LemmaProperty::PREPROCESS); } d_lemmas_waiting.clear(); } |