From f1c384dff82bffa56b9cf9ba18ec1f35aa529b12 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 23 Feb 2021 05:35:46 +0100 Subject: [PATCH] Add trans secant proofs. (#5957) 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. --- src/expr/proof_rule.cpp | 4 ++ src/expr/proof_rule.h | 30 ++++++++++ .../arith/nl/transcendental/proof_checker.cpp | 59 +++++++++++++++++++ .../transcendental/transcendental_solver.cpp | 12 ++-- .../transcendental/transcendental_state.cpp | 56 +++++++++++++++++- 5 files changed, 154 insertions(+), 7 deletions(-) diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index 110d9467e..85463d2d9 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -167,6 +167,10 @@ const char* toString(PfRule id) 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"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 10801648f..917db4088 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1137,6 +1137,36 @@ enum class PfRule : uint32_t // --------------------- // 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) diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index 6dc2df201..e09c8509a 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -64,7 +64,10 @@ void TranscendentalProofRuleChecker::registerTo(ProofChecker* pc) 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); @@ -133,6 +136,62 @@ Node TranscendentalProofRuleChecker::checkInternal( 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().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().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().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().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()); diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 0548c6a41..e58da1aad 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -323,14 +323,14 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) 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); @@ -374,8 +374,8 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) // 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 { diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp index 35967a39a..76c3d5357 100644 --- a/src/theory/arith/nl/transcendental/transcendental_state.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp @@ -319,7 +319,61 @@ NlLemma TranscendentalState::mkSecantLemma(TNode lower, 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(2 * actual_d), tf[0], lower, upper}); + } + else + { + proof->addStep( + lem, + PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG, + {}, + {nm->mkConst(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(2 * actual_d), + tf[0], + lower, + upper, + lapprox, + uapprox + + }); + } + else + { + proof->addStep(lem, + PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG, + {}, + {nm->mkConst(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& bounds, -- 2.30.2