}
std::pair<Node, Node> TranscendentalState::getClosestSecantPoints(TNode e,
- TNode c,
+ TNode center,
unsigned d)
{
// bounds are the minimum and maximum previous secant points
// should not repeat secant points: secant lemmas should suffice to
// rule out previous assignment
- Assert(
- std::find(d_secant_points[e][d].begin(), d_secant_points[e][d].end(), c)
- == d_secant_points[e][d].end());
+ Assert(std::find(
+ d_secant_points[e][d].begin(), d_secant_points[e][d].end(), center)
+ == d_secant_points[e][d].end());
// Insert into the (temporary) vector. We do not update this vector
// until we are sure this secant plane lemma has been processed. We do
// this by mapping the lemma to a side effect below.
std::vector<Node> spoints = d_secant_points[e][d];
- spoints.push_back(c);
+ spoints.push_back(center);
// sort
sortByNlModel(spoints.begin(), spoints.end(), &d_model);
// get the resulting index of c
unsigned index =
- std::find(spoints.begin(), spoints.end(), c) - spoints.begin();
+ std::find(spoints.begin(), spoints.end(), center) - spoints.begin();
// bounds are the next closest upper/lower bound values
return {index > 0 ? spoints[index - 1] : Node(),
}
Node TranscendentalState::mkSecantPlane(
- TNode arg, TNode b, TNode c, TNode approx_b, TNode approx_c)
+ TNode arg, TNode lower, TNode upper, TNode lval, TNode uval)
{
NodeManager* nm = NodeManager::currentNM();
// Figure 3: S_l( x ), S_u( x ) for s = 0,1
- Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, b, c));
+ Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, lower, upper));
Assert(rcoeff_n.isConst());
Rational rcoeff = rcoeff_n.getConst<Rational>();
Assert(rcoeff.sgn() != 0);
- return nm->mkNode(Kind::PLUS,
- approx_b,
- nm->mkNode(Kind::MULT,
- nm->mkNode(Kind::MINUS, approx_b, approx_c),
- nm->mkConst(rcoeff.inverse()),
- nm->mkNode(Kind::MINUS, arg, b)));
+ Node res =
+ nm->mkNode(Kind::PLUS,
+ lval,
+ nm->mkNode(Kind::MULT,
+ nm->mkNode(Kind::DIVISION,
+ nm->mkNode(Kind::MINUS, lval, uval),
+ nm->mkNode(Kind::MINUS, lower, upper)),
+ nm->mkNode(Kind::MINUS, arg, lower)));
+ Trace("nl-trans") << "Creating secant plane for transcendental function of "
+ << arg << std::endl;
+ Trace("nl-trans") << "\tfrom ( " << lower << " ; " << lval << " ) to ( "
+ << upper << " ; " << uval << " )" << std::endl;
+ Trace("nl-trans") << "\t" << res << std::endl;
+ Trace("nl-trans") << "\trewritten: " << Rewriter::rewrite(res) << std::endl;
+ return res;
}
-NlLemma TranscendentalState::mkSecantLemma(
- TNode lower, TNode upper, int concavity, TNode tf, TNode splane)
+NlLemma TranscendentalState::mkSecantLemma(TNode lower,
+ TNode upper,
+ TNode lapprox,
+ TNode uapprox,
+ int csign,
+ Convexity convexity,
+ TNode tf,
+ TNode splane,
+ unsigned actual_d)
{
NodeManager* nm = NodeManager::currentNM();
// With respect to Figure 3, this is slightly different.
Node antec_n = nm->mkNode(Kind::AND,
nm->mkNode(Kind::GEQ, tf[0], lower),
nm->mkNode(Kind::LEQ, tf[0], upper));
+ Trace("nl-trans") << "Bound for secant plane: " << lower << " <= " << tf[0]
+ << " <= " << upper << std::endl;
+ Trace("nl-trans") << "\t" << antec_n << std::endl;
+ // Convex: actual value is below the secant
+ // Concave: actual value is above the secant
Node lem = nm->mkNode(
Kind::IMPLIES,
antec_n,
- nm->mkNode(concavity == 1 ? Kind::LEQ : Kind::GEQ, tf, splane));
- Trace("nl-ext-tftp-debug2")
- << "*** Secant plane lemma (pre-rewrite) : " << lem << std::endl;
+ nm->mkNode(
+ convexity == Convexity::CONVEX ? Kind::LEQ : Kind::GEQ, tf, splane));
+ Trace("nl-trans-lemma") << "*** Secant plane lemma (pre-rewrite) : " << lem
+ << std::endl;
lem = Rewriter::rewrite(lem);
- Trace("nl-ext-tftp-lemma") << "*** Secant plane lemma : " << lem << std::endl;
+ Trace("nl-trans-lemma") << "*** Secant plane lemma : " << lem << std::endl;
Assert(d_model.computeAbstractModelValue(lem) == d_false);
return NlLemma(lem, LemmaProperty::NONE, nullptr, InferenceId::NL_T_SECANT);
}
void TranscendentalState::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)
{
- Trace("nl-ext-tftp-debug2") << "...secant bounds are : " << bounds.first
- << " ... " << bounds.second << std::endl;
- // take the model value of l or u (since may contain PI)
- // Make secant from bounds.first to c
- Node lval = d_model.computeAbstractModelValue(bounds.first);
- Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.first
- << " is " << lval << std::endl;
- if (lval != c)
+ int csign = center.getConst<Rational>().sgn();
+ Trace("nl-trans") << "...do secant lemma with center " << center << " val "
+ << cval << " sign " << csign << std::endl;
+ Trace("nl-trans") << "...secant bounds are : " << bounds.first << " ... "
+ << bounds.second << std::endl;
+ // take the model value of lower (since may contain PI)
+ // Make secant from bounds.first to center
+ Node lower = d_model.computeAbstractModelValue(bounds.first);
+ Trace("nl-trans") << "...model value of bound " << bounds.first << " is "
+ << lower << std::endl;
+ if (lower != center)
{
// Figure 3 : P(l), P(u), for s = 0
- Node approx_l = Rewriter::rewrite(
- poly_approx.substitute(d_taylor.getTaylorVariable(), lval));
- Node splane = mkSecantPlane(tf[0], lval, c, approx_l, approx_c);
- NlLemma nlem = mkSecantLemma(lval, c, concavity, tf, splane);
+ Node lval = Rewriter::rewrite(
+ poly_approx.substitute(d_taylor.getTaylorVariable(), lower));
+ Node splane = mkSecantPlane(tf[0], lower, center, lval, cval);
+ NlLemma nlem = mkSecantLemma(
+ lower, center, lval, cval, csign, convexity, tf, splane, actual_d);
// The side effect says that if lem is added, then we should add the
// secant point c for (tf,d).
- nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c));
+ nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center));
d_im.addPendingArithLemma(nlem, true);
}
- // Make secant from c to bounds.second
- Node uval = d_model.computeAbstractModelValue(bounds.second);
- Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.second
- << " is " << uval << std::endl;
- if (c != uval)
+ // take the model value of upper (since may contain PI)
+ // Make secant from center to bounds.second
+ Node upper = d_model.computeAbstractModelValue(bounds.second);
+ Trace("nl-trans") << "...model value of bound " << bounds.second << " is "
+ << upper << std::endl;
+ if (center != upper)
{
// Figure 3 : P(l), P(u), for s = 1
- Node approx_u = Rewriter::rewrite(
- poly_approx.substitute(d_taylor.getTaylorVariable(), uval));
- Node splane = mkSecantPlane(tf[0], c, uval, approx_c, approx_u);
- NlLemma nlem = mkSecantLemma(c, uval, concavity, tf, splane);
+ Node uval = Rewriter::rewrite(
+ poly_approx.substitute(d_taylor.getTaylorVariable(), upper));
+ Node splane = mkSecantPlane(tf[0], center, upper, cval, uval);
+ NlLemma nlem = mkSecantLemma(
+ center, upper, cval, uval, csign, convexity, tf, splane, actual_d);
// The side effect says that if lem is added, then we should add the
// secant point c for (tf,d).
- nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c));
+ nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center));
d_im.addPendingArithLemma(nlem, true);
}
}
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.
*
* 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.
* @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;
projects / cvc5.git / commitdiff