summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/proof_rule.cpp7
-rw-r--r--src/expr/proof_rule.h36
-rw-r--r--src/theory/arith/nl/transcendental/exponential_solver.cpp48
-rw-r--r--src/theory/arith/nl/transcendental/exponential_solver.h6
-rw-r--r--src/theory/arith/nl/transcendental/proof_checker.cpp60
-rw-r--r--src/theory/arith/nl/transcendental/transcendental_solver.cpp2
6 files changed, 149 insertions, 10 deletions
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<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,
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<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());
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)
{
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback