diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-14 16:32:25 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-03-14 16:32:25 -0500 |
commit | fef57367d28a62251cac47010cc6e80cd416832e (patch) | |
tree | ab4617644ca96b4d73f0e60d956314b8b19fbb2d /src | |
parent | d4046f5e2e32d07c34b65fbcdfffae6a24d8c399 (diff) |
Use zero slope tangent planes for transcendental functions (#2803)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/arith/nonlinear_extension.cpp | 34 |
1 files changed, 13 insertions, 21 deletions
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp index 929c7808d..c43b9458b 100644 --- a/src/theory/arith/nonlinear_extension.cpp +++ b/src/theory/arith/nonlinear_extension.cpp @@ -2621,8 +2621,10 @@ void NonlinearExtension::mkPi(){ d_pi_neg = Rewriter::rewrite(NodeManager::currentNM()->mkNode( MULT, d_pi, NodeManager::currentNM()->mkConst(Rational(-1)))); //initialize bounds - d_pi_bound[0] = NodeManager::currentNM()->mkConst( Rational(333)/Rational(106) ); - d_pi_bound[1] = NodeManager::currentNM()->mkConst( Rational(355)/Rational(113) ); + d_pi_bound[0] = + NodeManager::currentNM()->mkConst(Rational(103993) / Rational(33102)); + d_pi_bound[1] = + NodeManager::currentNM()->mkConst(Rational(104348) / Rational(33215)); } } @@ -4358,31 +4360,21 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf, { // compute tangent plane // Figure 3: T( x ) - Node tplane; - Node poly_approx_deriv = getDerivative(poly_approx, d_taylor_real_fv); - Assert(!poly_approx_deriv.isNull()); - poly_approx_deriv = Rewriter::rewrite(poly_approx_deriv); - Trace("nl-ext-tftp-debug2") << "...derivative of " << poly_approx << " is " - << poly_approx_deriv << std::endl; - std::vector<Node> taylor_subs; - taylor_subs.push_back(c); - Assert(taylor_vars.size() == taylor_subs.size()); - Node poly_approx_c_deriv = poly_approx_deriv.substitute(taylor_vars.begin(), - taylor_vars.end(), - taylor_subs.begin(), - taylor_subs.end()); - tplane = nm->mkNode( - PLUS, - poly_approx_c, - nm->mkNode(MULT, poly_approx_c_deriv, nm->mkNode(MINUS, tf[0], c))); + // We use zero slope tangent planes, since the concavity of the Taylor + // approximation cannot be easily established. + Node tplane = poly_approx_c; Node lem = nm->mkNode(concavity == 1 ? GEQ : LEQ, tf, tplane); std::vector<Node> antec; + int mdir = regionToMonotonicityDir(k, region); for (unsigned i = 0; i < 2; i++) { - if (!bounds[i].isNull()) + // Tangent plane is valid in the interval [c,u) if the slope of the + // function matches its concavity, and is valid in (l, c] otherwise. + Node use_bound = (mdir == concavity) == (i == 0) ? c : bounds[i]; + if (!use_bound.isNull()) { - Node ant = nm->mkNode(i == 0 ? GEQ : LEQ, tf[0], bounds[i]); + Node ant = nm->mkNode(i == 0 ? GEQ : LEQ, tf[0], use_bound); antec.push_back(ant); } } |