This PR adds proofs for secant lemmas in the transcendental lemmas for both exponential and sine functions.
It also adds proof rules and corresponding proof checkers.
return "ARITH_TRANS_EXP_POSITIVITY";
case PfRule::ARITH_TRANS_EXP_SUPER_LIN: return "ARITH_TRANS_EXP_SUPER_LIN";
case PfRule::ARITH_TRANS_EXP_ZERO: return "ARITH_TRANS_EXP_ZERO";
+ case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG:
+ return "ARITH_TRANS_EXP_APPROX_ABOVE_NEG";
+ case PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS:
+ return "ARITH_TRANS_EXP_APPROX_ABOVE_POS";
case PfRule::ARITH_TRANS_EXP_APPROX_BELOW:
return "ARITH_TRANS_EXP_APPROX_BELOW";
case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS";
// ---------------------
// Conclusion: (= (= t 0) (= (exp t) 1))
ARITH_TRANS_EXP_ZERO,
+ //======== Exp is approximated from above for negative values
+ // Children: none
+ // Arguments: (d, t, l, u)
+ // ---------------------
+ // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant exp l u t))
+ // Where d is an even positive number, t an arithmetic term and l (u) a lower
+ // (upper) bound on t. Let p be the d'th taylor polynomial at zero (also
+ // called the Maclaurin series) of the exponential function. (secant exp l u
+ // t) denotes the secant of p from (l, exp(l)) to (u, exp(u)) evaluated at t,
+ // calculated as follows:
+ // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
+ // The lemma states that if t is between l and u, then (exp t) is below the
+ // secant of p from l to u.
+ ARITH_TRANS_EXP_APPROX_ABOVE_NEG,
+ //======== Exp is approximated from above for positive values
+ // Children: none
+ // Arguments: (d, t, l, u)
+ // ---------------------
+ // Conclusion: (=> (and (>= t l) (<= t u)) (<= (exp t) (secant-pos exp l u t))
+ // Where d is an even positive number, t an arithmetic term and l (u) a lower
+ // (upper) bound on t. Let p* be a modification of the d'th taylor polynomial
+ // at zero (also called the Maclaurin series) of the exponential function as
+ // follows where p(d-1) is the regular Maclaurin series of degree d-1:
+ // p* = p(d-1) * (1 + t^n / n!)
+ // (secant-pos exp l u t) denotes the secant of p from (l, exp(l)) to (u,
+ // exp(u)) evaluated at t, calculated as follows:
+ // (p(l) - p(u)) / (l - u) * (t - l) + p(l)
+ // The lemma states that if t is between l and u, then (exp t) is below the
+ // secant of p from l to u.
+ ARITH_TRANS_EXP_APPROX_ABOVE_POS,
//======== Exp is approximated from below
// Children: none
// Arguments: (d, t)
pc->registerChecker(PfRule::ARITH_TRANS_EXP_POSITIVITY, this);
pc->registerChecker(PfRule::ARITH_TRANS_EXP_SUPER_LIN, this);
pc->registerChecker(PfRule::ARITH_TRANS_EXP_ZERO, this);
+ pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS, this);
+ pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG, this);
pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_BELOW, this);
+ pc->registerChecker(PfRule::ARITH_TRANS_SINE_BOUNDS, this);
pc->registerChecker(PfRule::ARITH_TRANS_SINE_SHIFT, this);
pc->registerChecker(PfRule::ARITH_TRANS_SINE_SYMMETRY, this);
pc->registerChecker(PfRule::ARITH_TRANS_SINE_TANGENT_ZERO, this);
Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
return nm->mkNode(EQUAL, args[0].eqNode(zero), e.eqNode(one));
}
+ else if (id == PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 4);
+ Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+ && args[0].getConst<Rational>().isIntegral());
+ Assert(args[1].getType().isReal());
+ Assert(args[2].isConst() && args[2].getKind() == Kind::CONST_RATIONAL);
+ Assert(args[3].isConst() && args[3].getKind() == Kind::CONST_RATIONAL);
+ std::uint64_t d =
+ args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+ Node t = args[1];
+ Node l = args[2];
+ Node u = args[3];
+ TaylorGenerator tg;
+ TaylorGenerator::ApproximationBounds bounds;
+ tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d / 2, bounds);
+ Node evall = Rewriter::rewrite(
+ bounds.d_upperPos.substitute(tg.getTaylorVariable(), l));
+ Node evalu = Rewriter::rewrite(
+ bounds.d_upperPos.substitute(tg.getTaylorVariable(), u));
+ Node evalsecant = mkSecant(t, l, u, evall, evalu);
+ Node lem = nm->mkNode(
+ Kind::IMPLIES,
+ mkBounds(t, l, u),
+ nm->mkNode(Kind::LEQ, nm->mkNode(Kind::EXPONENTIAL, t), evalsecant));
+ return Rewriter::rewrite(lem);
+ }
+ else if (id == PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 4);
+ Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+ && args[0].getConst<Rational>().isIntegral());
+ Assert(args[1].getType().isReal());
+ Assert(args[2].isConst() && args[2].getKind() == Kind::CONST_RATIONAL);
+ Assert(args[3].isConst() && args[3].getKind() == Kind::CONST_RATIONAL);
+ std::uint64_t d =
+ args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+ Node t = args[1];
+ Node l = args[2];
+ Node u = args[3];
+ TaylorGenerator tg;
+ TaylorGenerator::ApproximationBounds bounds;
+ tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d / 2, bounds);
+ Node evall = Rewriter::rewrite(
+ bounds.d_upperNeg.substitute(tg.getTaylorVariable(), l));
+ Node evalu = Rewriter::rewrite(
+ bounds.d_upperNeg.substitute(tg.getTaylorVariable(), u));
+ Node evalsecant = mkSecant(t, l, u, evall, evalu);
+ Node lem = nm->mkNode(
+ Kind::IMPLIES,
+ mkBounds(t, l, u),
+ nm->mkNode(Kind::LEQ, nm->mkNode(Kind::EXPONENTIAL, t), evalsecant));
+ return Rewriter::rewrite(lem);
+ }
else if (id == PfRule::ARITH_TRANS_EXP_APPROX_BELOW)
{
Assert(children.empty());
Node v_pab = r == 0 ? mvb.first : mvb.second;
if (!v_pab.isNull())
{
- Trace("nl-ext-tftp-debug2")
- << "...model value of " << pab << " is " << v_pab << std::endl;
+ Trace("nl-trans") << "...model value of " << pab << " is " << v_pab
+ << std::endl;
Assert(v_pab.isConst());
Node comp = nm->mkNode(r == 0 ? LT : GT, v, v_pab);
- Trace("nl-ext-tftp-debug2") << "...compare : " << comp << std::endl;
+ Trace("nl-trans") << "...compare : " << comp << std::endl;
Node compr = Rewriter::rewrite(comp);
- Trace("nl-ext-tftp-debug2") << "...got : " << compr << std::endl;
+ Trace("nl-trans") << "...got : " << compr << std::endl;
if (compr == d_tstate.d_true)
{
poly_approx_c = Rewriter::rewrite(v_pab);
// Figure 3: P( c )
if (is_tangent || is_secant)
{
- Trace("nl-ext-tftp-debug2")
- << "...poly approximation at c is " << poly_approx_c << std::endl;
+ Trace("nl-trans") << "...poly approximation at c is " << poly_approx_c
+ << std::endl;
}
else
{
lem = Rewriter::rewrite(lem);
Trace("nl-trans-lemma") << "*** Secant plane lemma : " << lem << std::endl;
Assert(d_model.computeAbstractModelValue(lem) == d_false);
- return NlLemma(InferenceId::ARITH_NL_T_SECANT, lem);
+ CDProof* proof = nullptr;
+ if (isProofEnabled())
+ {
+ proof = getProof();
+ if (tf.getKind() == Kind::EXPONENTIAL)
+ {
+ if (csign == 1)
+ {
+ proof->addStep(
+ lem,
+ PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS,
+ {},
+ {nm->mkConst<Rational>(2 * actual_d), tf[0], lower, upper});
+ }
+ else
+ {
+ proof->addStep(
+ lem,
+ PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG,
+ {},
+ {nm->mkConst<Rational>(2 * actual_d), tf[0], lower, upper});
+ }
+ }
+ else if (tf.getKind() == Kind::SINE)
+ {
+ if (convexity == Convexity::CONCAVE)
+ {
+ proof->addStep(lem,
+ PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS,
+ {},
+ {nm->mkConst<Rational>(2 * actual_d),
+ tf[0],
+ lower,
+ upper,
+ lapprox,
+ uapprox
+
+ });
+ }
+ else
+ {
+ proof->addStep(lem,
+ PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG,
+ {},
+ {nm->mkConst<Rational>(2 * actual_d),
+ tf[0],
+ lower,
+ upper,
+ lapprox,
+ uapprox});
+ }
+ }
+ }
+ return NlLemma(
+ InferenceId::ARITH_NL_T_SECANT, lem, LemmaProperty::NONE, proof);
}
void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds,
projects / cvc5.git / commitdiff