diff options
Diffstat (limited to 'src/theory/arith/nl/transcendental/transcendental_state.h')
-rw-r--r-- | src/theory/arith/nl/transcendental/transcendental_state.h | 60 |
1 files changed, 45 insertions, 15 deletions
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h index 0a4e46eca..e1510c3b3 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.h +++ b/src/theory/arith/nl/transcendental/transcendental_state.h @@ -27,6 +27,24 @@ namespace nl { namespace transcendental { /** + * This enum indicates whether some function is convex, concave or unknown at + * some point. + */ +enum class Convexity +{ + CONVEX, + CONCAVE, + UNKNOWN +}; +inline std::ostream& operator<<(std::ostream& os, Convexity c) { + switch (c) { + case Convexity::CONVEX: return os << "CONVEX"; + case Convexity::CONCAVE: return os << "CONCAVE"; + default: return os << "UNKNOWN"; + } +} + +/** * Holds common state and utilities for transcendental solvers. * * This includes common lookups and caches as well as generic utilities for @@ -60,20 +78,24 @@ struct TranscendentalState * Get the two closest secant points from the once stored already. * "closest" is determined according to the current model. * @param e The transcendental term (like (exp t)) - * @param c The point currently under consideration (probably the model of t) + * @param center The point currently under consideration (probably the model + * of t) * @param d The taylor degree. */ - std::pair<Node, Node> getClosestSecantPoints(TNode e, TNode c, unsigned d); + std::pair<Node, Node> getClosestSecantPoints(TNode e, + TNode center, + unsigned d); /** - * Construct a secant plane between b and c + * Construct a secant plane as function in arg between lower and upper * @param arg The argument of the transcendental term - * @param b Left secant point - * @param c Right secant point - * @param approx Approximation for b (not yet substituted) - * @param approx_c Approximation for c (already substituted) + * @param lower Left secant point + * @param upper Right secant point + * @param lval Evaluation at lower + * @param uval Evaluation at upper */ - Node mkSecantPlane(TNode arg, TNode b, TNode c, TNode approx, TNode approx_c); + Node mkSecantPlane( + TNode arg, TNode lower, TNode upper, TNode lval, TNode uval); /** * Construct a secant lemma between lower and upper for tf. @@ -83,26 +105,34 @@ struct TranscendentalState * @param tf Current transcendental term * @param splane Secant plane as computed by mkSecantPlane() */ - NlLemma mkSecantLemma( - TNode lower, TNode upper, int concavity, TNode tf, TNode splane); + NlLemma mkSecantLemma(TNode lower, + TNode upper, + TNode lapprox, + TNode uapprox, + int csign, + Convexity convexity, + TNode tf, + TNode splane, + unsigned actual_d); /** * Construct and send secant lemmas (if appropriate) * @param bounds Secant bounds * @param poly_approx Polynomial approximation - * @param c Current point - * @param approx_c Approximation for c + * @param center Current point + * @param cval Evaluation at c * @param tf Current transcendental term * @param d Current taylor degree * @param concavity Concavity in region of c */ void doSecantLemmas(const std::pair<Node, Node>& bounds, TNode poly_approx, - TNode c, - TNode approx_c, + TNode center, + TNode cval, TNode tf, + Convexity convexity, unsigned d, - int concavity); + unsigned actual_d); Node d_true; Node d_false; |