diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-10-28 12:50:08 -0500 |
---|---|---|
committer | Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> | 2019-10-28 10:50:08 -0700 |
commit | d6a8803054c0c5731a6c4111d8d00c18e2953032 (patch) | |
tree | 64f0eb21abb95eda0f8366c9106fd8597a0a3167 /src/theory/arith | |
parent | 885ec2cf131450f7f651b68a1cae3920665da31a (diff) |
Fix for non-linear models (#3410)
* Towards fix for non-linear models
* Format
* Fix
* More
* Improve
* Format
* More
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 87 |
1 files changed, 63 insertions, 24 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index f067fda47..4dfda79b7 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -2288,32 +2288,14 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions, void NonlinearExtension::check(Theory::Effort e) { Trace("nl-ext") << std::endl; - Trace("nl-ext") << "NonlinearExtension::check, effort = " << e << std::endl; + Trace("nl-ext") << "NonlinearExtension::check, effort = " << e + << ", built model = " << d_builtModel.get() << std::endl; if (d_builtModel.get()) { - if (e == Theory::EFFORT_FULL) - { - return; - } - // now, record the approximations we used - NodeManager* nm = NodeManager::currentNM(); - for (const std::pair<const Node, std::pair<Node, Node> >& cb : - d_check_model_bounds) - { - Node l = cb.second.first; - Node u = cb.second.second; - if (l != u) - { - Node v = cb.first; - Node pred = - nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); - pred = Rewriter::rewrite(pred); - d_containing.getValuation().getModel()->recordApproximation(v, pred); - } - } - return; + // already built model, nothing to do } - if (e == Theory::EFFORT_FULL) { + else if (e == Theory::EFFORT_FULL) + { d_containing.getExtTheory()->clearCache(); d_needsLastCall = true; if (options::nlExtRewrites()) { @@ -2328,7 +2310,9 @@ void NonlinearExtension::check(Theory::Effort e) { Trace("nl-ext") << "...sent lemmas." << std::endl; } } - } else { + } + else + { // get the assertions std::vector<Node> assertions; getAssertions(assertions); @@ -2508,6 +2492,61 @@ void NonlinearExtension::check(Theory::Effort e) { } while (needsRecheck); } + + // Did we internally determine a model exists? If so, we need to record some + // information in the theory engine's model class. + if (d_builtModel.get()) + { + if (e < Theory::EFFORT_LAST_CALL) + { + // don't need to build the model yet + return; + } + // Record the approximations we used. This code calls the + // recordApproximation method of the model, which overrides the model + // values for variables that we solved for, using techniques specific to + // this class. + NodeManager* nm = NodeManager::currentNM(); + TheoryModel* m = d_containing.getValuation().getModel(); + for (const std::pair<const Node, std::pair<Node, Node> >& cb : + d_check_model_bounds) + { + Node l = cb.second.first; + Node u = cb.second.second; + Node pred; + Node v = cb.first; + if (l != u) + { + pred = nm->mkNode(AND, nm->mkNode(GEQ, v, l), nm->mkNode(GEQ, u, v)); + } + else if (!m->areEqual(v, l)) + { + // only record if value was not equal already + pred = v.eqNode(l); + } + if (!pred.isNull()) + { + pred = Rewriter::rewrite(pred); + m->recordApproximation(v, pred); + } + } + // Also record the exact values we used. An exact value can be seen as a + // special kind approximation of the form (choice x. x = exact_value). + // Notice that the above term gets rewritten such that the choice function + // is eliminated. + for (size_t i = 0, num = d_check_model_vars.size(); i < num; i++) + { + Node v = d_check_model_vars[i]; + Node s = d_check_model_subs[i]; + if (!m->areEqual(v, s)) + { + Node pred = v.eqNode(s); + pred = Rewriter::rewrite(pred); + m->recordApproximation(v, pred); + } + } + return; + } } void NonlinearExtension::presolve() |