Increment Taylor degree for tangent and secant plane inferences for transcendentals...

diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index e8b1b3b930226e8623956539166252bca3367f11..46be960c76cf7bbc181599400c05ccdaf9b4b86c 100644 (file)
--- 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 7bd626ff0573824e5a7eda9d142852007da7f1a8..67cc44a42e9d15afe7e2727487e8ec7ae4fe5ca2 100644 (file)
--- 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 (file)
index 0000000..5bcae30
--- /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)