From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 18 Dec 2019 14:44:06 +0000 (-0600)
Subject: Increment Taylor degree for tangent and secant plane inferences for transcendentals... 
X-Git-Tag: cvc5-1.0.0~3752
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b0ef3a7e604d8b5a01c7fff2b149987c91d08baf;p=cvc5.git

Increment Taylor degree for tangent and secant plane inferences for transcendentals (#3577)
---

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index e8b1b3b93..46be960c7 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -3042,21 +3042,22 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf,
 
   NodeManager* nm = NodeManager::currentNM();
   Kind k = tf.getKind();
+
+  // Figure 3 : c
+  Node c = d_model.computeAbstractModelValue(tf[0]);
+  int csign = c.getConst<Rational>().sgn();
+  Assert(csign == 1 || csign == -1);
+
   // Figure 3: P_l, P_u
   // mapped to for signs of c
   std::map<int, Node> poly_approx_bounds[2];
   std::vector<Node> pbounds;
-  getPolynomialApproximationBounds(k, d, pbounds);
+  getPolynomialApproximationBoundForArg(k, c, d, pbounds);
   poly_approx_bounds[0][1] = pbounds[0];
   poly_approx_bounds[0][-1] = pbounds[1];
   poly_approx_bounds[1][1] = pbounds[2];
   poly_approx_bounds[1][-1] = pbounds[3];
 
-  // Figure 3 : c
-  Node c = d_model.computeAbstractModelValue(tf[0]);
-  int csign = c.getConst<Rational>().sgn();
-  Assert(csign == 1 || csign == -1);
-
   // Figure 3 : v
   Node v = d_model.computeAbstractModelValue(tf);
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7bd626ff0..67cc44a42 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1268,6 +1268,7 @@ set(regress_1_tests
   regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
   regress1/nl/exp-4.5-lt.smt2
   regress1/nl/exp-approx.smt2
+  regress1/nl/exp-soundness-bound.smt2
   regress1/nl/exp1-lb.smt2
   regress1/nl/exp_monotone.smt2
   regress1/nl/factor_agg_s.smt2
diff --git a/test/regress/regress1/nl/exp-soundness-bound.smt2 b/test/regress/regress1/nl/exp-soundness-bound.smt2
new file mode 100644
index 000000000..5bcae30b0
--- /dev/null
+++ b/test/regress/regress1/nl/exp-soundness-bound.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: --nl-ext --decision=internal --no-check-models
+; EXPECT: sat
+(set-logic ALL)
+(assert (or (< 60.3 (exp 4.1) 60.4) (< (exp 5.1) 164.1)))
+(check-sat)