diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-15 14:08:03 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-15 19:08:03 +0000 |
| commit | 216f3c9fb07a08909942b91a2a4739cd178f5a72 (patch) | |
| tree | 00de2d826d1b4ad6124856536923a2463c4d8641 /src/theory/arith/nl/nonlinear_extension.cpp | |
| parent | 6cbb7824dabd7ab8e85472a22ba30ad2498afebc (diff) | |
Make nonlinear extension account for relevant term set (#6147)
This fixes a subtle issue with non-linear and theory combination.
It currently could use irrelevant terms preregistered to the ExtTheory for its model-based refinement. This means that the non-linear extension could accidentally modify values for terms that are not included in its term set, violating theory combination.
In particular, in the minimized example from #5662, (* a k) was a stale term in ExtTheory, and non-linear extension falsely believed that a was a term whose model value could be modified, since moreover a was not a shared term. In reality, a was not a shared term since it only was registered to UF.
Fixes #5662.
Diffstat (limited to 'src/theory/arith/nl/nonlinear_extension.cpp')
| -rw-r--r-- | src/theory/arith/nl/nonlinear_extension.cpp | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp index 671c3f44a..25aebf6d4 100644 --- a/src/theory/arith/nl/nonlinear_extension.cpp +++ b/src/theory/arith/nl/nonlinear_extension.cpp @@ -301,7 +301,7 @@ void NonlinearExtension::check(Theory::Effort e) } } -bool NonlinearExtension::modelBasedRefinement() +bool NonlinearExtension::modelBasedRefinement(const std::set<Node>& termSet) { ++(d_stats.d_mbrRuns); d_checkCounter++; @@ -317,8 +317,18 @@ bool NonlinearExtension::modelBasedRefinement() Trace("nl-ext") << "# false asserts = " << false_asserts.size() << std::endl; // get the extended terms belonging to this theory + std::vector<Node> xtsAll; + d_extTheory.getTerms(xtsAll); + // only consider those that are currently relevant based on the current + // assertions, i.e. those contained in termSet std::vector<Node> xts; - d_extTheory.getTerms(xts); + for (const Node& x : xtsAll) + { + if (termSet.find(x) != termSet.end()) + { + xts.push_back(x); + } + } if (Trace.isOn("nl-ext-debug")) { @@ -496,7 +506,8 @@ bool NonlinearExtension::modelBasedRefinement() return false; } -void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel) +void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel, + const std::set<Node>& termSet) { if (!needsCheckLastEffort()) { @@ -509,7 +520,7 @@ void NonlinearExtension::interceptModel(std::map<Node, Node>& arithModel) if (!d_builtModel.get()) { Trace("nl-ext") << "interceptModel: do model-based refinement" << std::endl; - modelBasedRefinement(); + modelBasedRefinement(termSet); } if (d_builtModel.get()) { |