diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-22 17:19:20 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-22 17:19:20 -0600 |
| commit | 13819c4ae33a103b1075e816772a305b16db9157 (patch) | |
| tree | f8598d57ac30065091fd2115af2f25cef1673acd /src/theory/quantifiers/fmf | |
| parent | 4479383c2fd8a3b81ab63d66f843b09b5c9d0cd3 (diff) | |
Eliminate raw use of output channel and valuation in quantifiers (#5933)
This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.
Diffstat (limited to 'src/theory/quantifiers/fmf')
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index e8b9f5dea..b9a3e1f34 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -498,7 +498,7 @@ void BoundedIntegers::checkOwnership(Node f) new IntRangeDecisionHeuristic(r, d_qstate.getSatContext(), d_qstate.getUserContext(), - d_quantEngine->getValuation(), + d_qstate.getValuation(), isProxy)); d_quantEngine->getTheoryEngine() ->getDecisionManager() @@ -726,7 +726,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); + d_qim.lemma(lem, InferenceId::UNKNOWN); } return false; }else{ |