From 8fe04676488e7ff4fbe149f98b1ad62f2bdfee1d Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 19 Feb 2020 01:23:43 -0600 Subject: [PATCH] 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> --- src/theory/arith/nonlinear_extension.cpp | 29 ++++++++++++++++++++++-- 1 file 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& 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 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) { -- 2.30.2