diff options
author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-23 05:35:46 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-02-22 22:35:46 -0600 |
commit | f1c384dff82bffa56b9cf9ba18ec1f35aa529b12 (patch) | |
tree | 5049b8dda3ad679e6b164c50daa458649d0515af /src/theory | |
parent | 4711be9f5f65d5ea61321bc80d31e030536de81b (diff) |
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.
Diffstat (limited to 'src/theory')
3 files changed, 120 insertions, 7 deletions
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<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()); 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<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, |