From: Gereon Kremer Date: Mon, 22 Feb 2021 21:27:30 +0000 (+0100) Subject: (proof-new) Add proofs for exponential functions (#5956) X-Git-Tag: cvc5-1.0.0~2245 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=580f3e93c2cc4564e6fa87d07426dc1ff87224e4;p=cvc5.git (proof-new) Add proofs for exponential functions (#5956) This PR adds proofs for lemmas concerned with the exponential function. If also adds the necessary proof rules and corresponding proof checker. --- diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp index a5dde78ab..110d9467e 100644 --- a/src/expr/proof_rule.cpp +++ b/src/expr/proof_rule.cpp @@ -162,6 +162,13 @@ const char* toString(PfRule id) case PfRule::ARITH_MULT_TANGENT: return "ARITH_MULT_TANGENT"; case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM"; case PfRule::ARITH_TRANS_PI: return "ARITH_TRANS_PI"; + case PfRule::ARITH_TRANS_EXP_NEG: return "ARITH_TRANS_EXP_NEG"; + case PfRule::ARITH_TRANS_EXP_POSITIVITY: + 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_BELOW: + return "ARITH_TRANS_EXP_APPROX_BELOW"; case PfRule::ARITH_TRANS_SINE_BOUNDS: return "ARITH_TRANS_SINE_BOUNDS"; case PfRule::ARITH_TRANS_SINE_SHIFT: return "ARITH_TRANS_SINE_SHIFT"; case PfRule::ARITH_TRANS_SINE_SYMMETRY: return "ARITH_TRANS_SINE_SYMMETRY"; diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h index 28ea24533..10801648f 100644 --- a/src/expr/proof_rule.h +++ b/src/expr/proof_rule.h @@ -1113,6 +1113,42 @@ enum class PfRule : uint32_t // Where l (u) is a valid lower (upper) bound on pi. ARITH_TRANS_PI, + //======== Exp at negative values + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= (< t 0) (< (exp t) 1)) + ARITH_TRANS_EXP_NEG, + //======== Exp is always positive + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (> (exp t) 0) + ARITH_TRANS_EXP_POSITIVITY, + //======== Exp grows super-linearly for positive values + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (or (<= t 0) (> exp(t) (+ t 1))) + ARITH_TRANS_EXP_SUPER_LIN, + //======== Exp at zero + // Children: none + // Arguments: (t) + // --------------------- + // Conclusion: (= (= t 0) (= (exp t) 1)) + ARITH_TRANS_EXP_ZERO, + //======== Exp is approximated from below + // Children: none + // Arguments: (d, t) + // --------------------- + // Conclusion: (>= (exp t) (maclaurin exp d t)) + // Where d is an odd positive number and (maclaurin exp d t) is the d'th + // taylor polynomial at zero (also called the Maclaurin series) of the + // exponential function evaluated at t. The Maclaurin series for the + // exponential function is the following: + // e^x = \sum_{n=0}^{\infty} x^n / n! + ARITH_TRANS_EXP_APPROX_BELOW, + //======== Sine is always between -1 and 1 // Children: none // Arguments: (t) diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp index 7f9d98fe1..86b17376c 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.cpp +++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp @@ -70,24 +70,42 @@ void ExponentialSolver::checkInitialRefine() { // exp is always positive: exp(t) > 0 Node lem = nm->mkNode(Kind::GT, t, d_data->d_zero); + CDProof* proof = nullptr; + if (d_data->isProofEnabled()) + { + proof = d_data->getProof(); + proof->addStep(lem, PfRule::ARITH_TRANS_EXP_POSITIVITY, {}, {t[0]}); + } d_data->d_im.addPendingLemma( - lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr); + lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof); } { // exp at zero: (t = 0) <=> (exp(t) = 1) Node lem = nm->mkNode(Kind::EQUAL, t[0].eqNode(d_data->d_zero), t.eqNode(d_data->d_one)); + CDProof* proof = nullptr; + if (d_data->isProofEnabled()) + { + proof = d_data->getProof(); + proof->addStep(lem, PfRule::ARITH_TRANS_EXP_ZERO, {}, {t[0]}); + } d_data->d_im.addPendingLemma( - lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr); + lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof); } { // exp on negative values: (t < 0) <=> (exp(t) < 1) Node lem = nm->mkNode(Kind::EQUAL, nm->mkNode(Kind::LT, t[0], d_data->d_zero), nm->mkNode(Kind::LT, t, d_data->d_one)); + CDProof* proof = nullptr; + if (d_data->isProofEnabled()) + { + proof = d_data->getProof(); + proof->addStep(lem, PfRule::ARITH_TRANS_EXP_NEG, {}, {t[0]}); + } d_data->d_im.addPendingLemma( - lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr); + lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof); } { // exp on positive values: (t <= 0) or (exp(t) > t+1) @@ -96,8 +114,14 @@ void ExponentialSolver::checkInitialRefine() nm->mkNode(Kind::LEQ, t[0], d_data->d_zero), nm->mkNode( Kind::GT, t, nm->mkNode(Kind::PLUS, t[0], d_data->d_one))); + CDProof* proof = nullptr; + if (d_data->isProofEnabled()) + { + proof = d_data->getProof(); + proof->addStep(lem, PfRule::ARITH_TRANS_EXP_SUPER_LIN, {}, {t[0]}); + } d_data->d_im.addPendingLemma( - lem, InferenceId::ARITH_NL_T_INIT_REFINE, nullptr); + lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof); } } } @@ -172,7 +196,10 @@ void ExponentialSolver::checkMonotonic() } } -void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx) +void ExponentialSolver::doTangentLemma(TNode e, + TNode c, + TNode poly_approx, + std::uint64_t d) { NodeManager* nm = NodeManager::currentNM(); // compute tangent plane @@ -189,8 +216,17 @@ void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx) Trace("nl-ext-exp") << "*** Tangent plane lemma : " << lem << std::endl; Assert(d_data->d_model.computeAbstractModelValue(lem) == d_data->d_false); // Figure 3 : line 9 + CDProof* proof = nullptr; + if (d_data->isProofEnabled()) + { + proof = d_data->getProof(); + proof->addStep(lem, + PfRule::ARITH_TRANS_EXP_APPROX_BELOW, + {}, + {nm->mkConst(d), e[0]}); + } d_data->d_im.addPendingLemma( - lem, InferenceId::ARITH_NL_T_TANGENT, nullptr, true); + lem, InferenceId::ARITH_NL_T_TANGENT, proof, true); } void ExponentialSolver::doSecantLemmas(TNode e, diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h index 1fad896e4..b874e1a4b 100644 --- a/src/theory/arith/nl/transcendental/exponential_solver.h +++ b/src/theory/arith/nl/transcendental/exponential_solver.h @@ -85,10 +85,10 @@ class ExponentialSolver */ void checkMonotonic(); - /** Sent tangent lemma around c for e */ - void doTangentLemma(TNode e, TNode c, TNode poly_approx); + /** Send tangent lemma around c for e */ + void doTangentLemma(TNode e, TNode c, TNode poly_approx, std::uint64_t d); - /** Sent secant lemmas around c for e */ + /** Send secant lemmas around c for e */ void doSecantLemmas(TNode e, TNode poly_approx, TNode center, diff --git a/src/theory/arith/nl/transcendental/proof_checker.cpp b/src/theory/arith/nl/transcendental/proof_checker.cpp index bec2bd9b8..6dc2df201 100644 --- a/src/theory/arith/nl/transcendental/proof_checker.cpp +++ b/src/theory/arith/nl/transcendental/proof_checker.cpp @@ -60,6 +60,11 @@ Node mkSecant(TNode t, TNode l, TNode u, TNode evall, TNode evalu) void TranscendentalProofRuleChecker::registerTo(ProofChecker* pc) { pc->registerChecker(PfRule::ARITH_TRANS_PI, this); + pc->registerChecker(PfRule::ARITH_TRANS_EXP_NEG, this); + 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_BELOW, 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); @@ -80,10 +85,16 @@ Node TranscendentalProofRuleChecker::checkInternal( auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI); auto mpi = nm->mkNode(Kind::MULT, mone, pi); Trace("nl-trans-checker") << "Checking " << id << std::endl; + Trace("nl-trans-checker") << "Children:" << std::endl; for (const auto& c : children) { Trace("nl-trans-checker") << "\t" << c << std::endl; } + Trace("nl-trans-checker") << "Args:" << std::endl; + for (const auto& a : args) + { + Trace("nl-trans-checker") << "\t" << a << std::endl; + } if (id == PfRule::ARITH_TRANS_PI) { Assert(children.empty()); @@ -91,6 +102,55 @@ Node TranscendentalProofRuleChecker::checkInternal( return nm->mkAnd(std::vector{nm->mkNode(Kind::GEQ, pi, args[0]), nm->mkNode(Kind::LEQ, pi, args[1])}); } + else if (id == PfRule::ARITH_TRANS_EXP_NEG) + { + Assert(children.empty()); + Assert(args.size() == 1); + Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]); + return nm->mkNode( + EQUAL, nm->mkNode(LT, args[0], zero), nm->mkNode(LT, e, one)); + } + else if (id == PfRule::ARITH_TRANS_EXP_POSITIVITY) + { + Assert(children.empty()); + Assert(args.size() == 1); + Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]); + return nm->mkNode(GT, e, zero); + } + else if (id == PfRule::ARITH_TRANS_EXP_SUPER_LIN) + { + Assert(children.empty()); + Assert(args.size() == 1); + Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]); + return nm->mkNode(OR, + nm->mkNode(LEQ, args[0], zero), + nm->mkNode(GT, e, nm->mkNode(PLUS, args[0], one))); + } + else if (id == PfRule::ARITH_TRANS_EXP_ZERO) + { + Assert(children.empty()); + Assert(args.size() == 1); + 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_BELOW) + { + Assert(children.empty()); + Assert(args.size() == 2); + Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL + && args[0].getConst().isIntegral()); + Assert(args[1].getType().isReal()); + std::uint64_t d = + args[0].getConst().getNumerator().toUnsignedInt(); + Node t = args[1]; + TaylorGenerator tg; + TaylorGenerator::ApproximationBounds bounds; + tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d, bounds); + Node eval = + Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), t)); + return nm->mkNode( + Kind::GEQ, std::vector{nm->mkNode(Kind::EXPONENTIAL, t), eval}); + } else if (id == PfRule::ARITH_TRANS_SINE_BOUNDS) { Assert(children.empty()); diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp index 7b87adab1..0548c6a41 100644 --- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp +++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp @@ -387,7 +387,7 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d) { if (k == Kind::EXPONENTIAL) { - d_expSlv.doTangentLemma(tf, c, poly_approx_c); + d_expSlv.doTangentLemma(tf, c, poly_approx_c, d); } else if (k == Kind::SINE) {