This PR adds proofs for lemmas concerned with the exponential function. If also adds the necessary proof rules and corresponding proof checker.
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";
// 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)
{
// 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)
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);
}
}
}
}
}
-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
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<Rational>(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,
*/
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,
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);
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());
return nm->mkAnd(std::vector<Node>{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<Rational>().isIntegral());
+ Assert(args[1].getType().isReal());
+ std::uint64_t d =
+ args[0].getConst<Rational>().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<Node>{nm->mkNode(Kind::EXPONENTIAL, t), eval});
+ }
else if (id == PfRule::ARITH_TRANS_SINE_BOUNDS)
{
Assert(children.empty());
{
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)
{
projects / cvc5.git / commitdiff