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 | |
| 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')
| -rw-r--r-- | src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 8a8678749..cb31e80d3 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -374,7 +374,7 @@ void InstStrategyCegqi::registerCounterexampleLemma(Node q, Node lem) ce_vars.push_back(tutil->getInstantiationConstant(q, i)); } // send the lemma - d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); + d_quantEngine->getOutputChannel().lemma(lem); // get the preprocessed form of the lemma we just sent std::vector<Node> skolems; std::vector<Node> skAsserts; diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 0f17bb04a..9144bca2a 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -725,7 +725,7 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] ); Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma(lem, LemmaProperty::PREPROCESS); + d_quantEngine->getOutputChannel().lemma(lem); } return false; }else{ |