diff options
Diffstat (limited to 'src/theory/arith/nl/transcendental/exponential_solver.cpp')
| -rw-r--r-- | src/theory/arith/nl/transcendental/exponential_solver.cpp | 26 |
1 files changed, 18 insertions, 8 deletions
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 7d7d0c23c..482e3bc21 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -170,31 +170,41 @@ void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx) d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true); } -void ExponentialSolver::doSecantLemmas( - TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d) +void ExponentialSolver::doSecantLemmas(TNode e, + TNode poly_approx, + TNode center, + TNode cval, + unsigned d, + unsigned actual_d) { - d_data->doSecantLemmas( - getSecantBounds(e, c, d), poly_approx, c, poly_approx_c, e, d, 1); + d_data->doSecantLemmas(getSecantBounds(e, center, d), + poly_approx, + center, + cval, + e, + Convexity::CONVEX, + d, + actual_d); } std::pair<Node, Node> ExponentialSolver::getSecantBounds(TNode e, - TNode c, + TNode center, unsigned d) { - std::pair<Node, Node> bounds = d_data->getClosestSecantPoints(e, c, d); + std::pair<Node, Node> bounds = d_data->getClosestSecantPoints(e, center, d); // Check if we already have neighboring secant points if (bounds.first.isNull()) { // pick c-1 bounds.first = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(Kind::MINUS, c, d_data->d_one)); + NodeManager::currentNM()->mkNode(Kind::MINUS, center, d_data->d_one)); } if (bounds.second.isNull()) { // pick c+1 bounds.second = Rewriter::rewrite( - NodeManager::currentNM()->mkNode(Kind::PLUS, c, d_data->d_one)); + NodeManager::currentNM()->mkNode(Kind::PLUS, center, d_data->d_one)); } return bounds; } |