diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-19 01:23:43 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-18 23:23:43 -0800 |
commit | 8fe04676488e7ff4fbe149f98b1ad62f2bdfee1d (patch) | |
tree | 7c428ce1f93a8647378997eeed69044234daaf94 /src/theory | |
parent | 0398c53a582a3242ef89dceae59d00137f17df79 (diff) |
Fix approximate bounds for transcendental functions whose model values rewrite (#3747)
* Fix bounds for negative sine apps
* Format
* Comment
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 29 |
1 files changed, 27 insertions, 2 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 1c8b9611f..6c04268db 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -793,15 +793,40 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions, bool success = true; // tf is Figure 3 : tf( x ) Node atf = d_model.computeConcreteModelValue(tf); + Trace("nl-ext-cm-debug") + << "Value for is " << tf << " is " << atf << std::endl; + Node bl; + Node bu; if (k == PI) { - success = d_model.addCheckModelBound(atf, d_pi_bound[0], d_pi_bound[1]); + bl = d_pi_bound[0]; + bu = d_pi_bound[1]; } else if (d_model.isRefineableTfFun(tf)) { d_model.setUsedApproximate(); std::pair<Node, Node> bounds = getTfModelBounds(tf, d_taylor_degree); - success = d_model.addCheckModelBound(atf, bounds.first, bounds.second); + bl = bounds.first; + bu = bounds.second; + } + if (!bl.isNull() && !bu.isNull()) + { + // We have rewritten an application of a transcendental function + // based on the current model values.It could be that the model value + // rewrites sin(x) ---> sin(-c) ---> -sin(c), thus we need + // to negate the bounds in this case. + if (atf.getKind() != tf.getKind()) + { + if (atf.getKind() == MULT && atf.getNumChildren() == 2 + && atf[0] == d_neg_one) + { + atf = atf[1]; + Node btmp = bl; + bl = ArithMSum::negate(bu); + bu = ArithMSum::negate(btmp); + } + } + success = d_model.addCheckModelBound(atf, bl, bu); } if (!success) { |