This PR adds proofs for the lemmas related to the sine function in the transcendental solver.
It introduces several new proof rules with corresponding proof checkers and produces proofs in the sine solver.
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_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";
+ case PfRule::ARITH_TRANS_SINE_TANGENT_ZERO:
+ return "ARITH_TRANS_SINE_TANGENT_ZERO";
+ case PfRule::ARITH_TRANS_SINE_TANGENT_PI:
+ return "ARITH_TRANS_SINE_TANGENT_PI";
+ case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG:
+ return "ARITH_TRANS_SINE_APPROX_ABOVE_NEG";
+ case PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS:
+ return "ARITH_TRANS_SINE_APPROX_ABOVE_POS";
+ case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG:
+ return "ARITH_TRANS_SINE_APPROX_BELOW_NEG";
+ case PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS:
+ return "ARITH_TRANS_SINE_APPROX_BELOW_POS";
//================================================= Unknown rule
case PfRule::UNKNOWN: return "UNKNOWN";
default: return "?";
// Conclusion: (and (>= real.pi l) (<= real.pi u))
// Where l (u) is a valid lower (upper) bound on pi.
ARITH_TRANS_PI,
+
+ //======== Sine is always between -1 and 1
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (and (<= (sin t) 1) (>= (sin t) (- 1)))
+ ARITH_TRANS_SINE_BOUNDS,
//======== Sine arg shifted to -pi..pi
// Children: none
// Arguments: (x, y, s)
// into -pi..pi and s is a new integer skolem that is the number of phases y
// is shifted.
ARITH_TRANS_SINE_SHIFT,
+ //======== Sine is symmetric with respect to negation of the argument
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (= (- (sin t) (sin (- t))) 0)
+ ARITH_TRANS_SINE_SYMMETRY,
+ //======== Sine is bounded by the tangent at zero
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (and
+ // (=> (> t 0) (< (sin t) t))
+ // (=> (< t 0) (> (sin t) t))
+ // )
+ ARITH_TRANS_SINE_TANGENT_ZERO,
+ //======== Sine is bounded by the tangents at -pi and pi
+ // Children: none
+ // Arguments: (t)
+ // ---------------------
+ // Conclusion: (and
+ // (=> (> t -pi) (> (sin t) (- -pi t)))
+ // (=> (< t pi) (< (sin t) (- pi t)))
+ // )
+ ARITH_TRANS_SINE_TANGENT_PI,
+ //======== Sine is approximated from above for negative values
+ // Children: none
+ // Arguments: (d, t, lb, ub, l, u)
+ // ---------------------
+ // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (secant sin l u t))
+ // Where d is an even positive number, t an arithmetic term, lb (ub) a
+ // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
+ // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
+ // zero (also called the Maclaurin series) of the sine function. (secant sin l
+ // u t) denotes the secant of p from (l, sin(l)) to (u, sin(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 (sin t) is below the
+ // secant of p from l to u.
+ ARITH_TRANS_SINE_APPROX_ABOVE_NEG,
+ //======== Sine is approximated from above for positive values
+ // Children: none
+ // Arguments: (d, t, c, lb, ub)
+ // ---------------------
+ // Conclusion: (=> (and (>= t lb) (<= t ub)) (<= (sin t) (upper sin c))
+ // Where d is an even positive number, t an arithmetic term, c an arithmetic
+ // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
+ // containing pi). Let p be the d'th taylor polynomial at zero (also called
+ // the Maclaurin series) of the sine function. (upper sin c) denotes the upper
+ // bound on sin(c) given by p and lb,ub are such that sin(t) is the maximum of
+ // the sine function on (lb,ub).
+ ARITH_TRANS_SINE_APPROX_ABOVE_POS,
+ //======== Sine is approximated from below for negative values
+ // Children: none
+ // Arguments: (d, t, c, lb, ub)
+ // ---------------------
+ // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (lower sin c))
+ // Where d is an even positive number, t an arithmetic term, c an arithmetic
+ // constant, and lb (ub) a symbolic lower (upper) bound on t (possibly
+ // containing pi). Let p be the d'th taylor polynomial at zero (also called
+ // the Maclaurin series) of the sine function. (lower sin c) denotes the lower
+ // bound on sin(c) given by p and lb,ub are such that sin(t) is the minimum of
+ // the sine function on (lb,ub).
+ ARITH_TRANS_SINE_APPROX_BELOW_NEG,
+ //======== Sine is approximated from below for positive values
+ // Children: none
+ // Arguments: (d, t, lb, ub, l, u)
+ // ---------------------
+ // Conclusion: (=> (and (>= t lb) (<= t ub)) (>= (sin t) (secant sin l u t))
+ // Where d is an even positive number, t an arithmetic term, lb (ub) a
+ // symbolic lower (upper) bound on t (possibly containing pi) and l (u) the
+ // evaluated lower (upper) bound on t. Let p be the d'th taylor polynomial at
+ // zero (also called the Maclaurin series) of the sine function. (secant sin l
+ // u t) denotes the secant of p from (l, sin(l)) to (u, sin(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 (sin t) is above the
+ // secant of p from l to u.
+ ARITH_TRANS_SINE_APPROX_BELOW_POS,
//================================================= Unknown rule
UNKNOWN,
namespace nl {
namespace transcendental {
+namespace {
+
+/**
+ * Helper method to construct (t >= lb) AND (t <= up)
+ */
+Node mkBounds(TNode t, TNode lb, TNode ub)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ return nm->mkAnd(std::vector<Node>{nm->mkNode(Kind::GEQ, t, lb),
+ nm->mkNode(Kind::LEQ, t, ub)});
+}
+
+/**
+ * Helper method to construct a secant plane:
+ * ((evall - evalu) / (l - u)) * (t - l) + evall
+ */
+Node mkSecant(TNode t, TNode l, TNode u, TNode evall, TNode evalu)
+{
+ NodeManager* nm = NodeManager::currentNM();
+ return nm->mkNode(Kind::PLUS,
+ nm->mkNode(Kind::MULT,
+ nm->mkNode(Kind::DIVISION,
+ nm->mkNode(Kind::MINUS, evall, evalu),
+ nm->mkNode(Kind::MINUS, l, u)),
+ nm->mkNode(Kind::MINUS, t, l)),
+ evall);
+}
+
+} // namespace
+
void TranscendentalProofRuleChecker::registerTo(ProofChecker* pc)
{
pc->registerChecker(PfRule::ARITH_TRANS_PI, 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);
+ pc->registerChecker(PfRule::ARITH_TRANS_SINE_TANGENT_PI, this);
+ pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS, this);
+ pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG, this);
+ pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS, this);
+ pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG, this);
}
Node TranscendentalProofRuleChecker::checkInternal(
Assert(args.size() == 2);
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_SINE_SHIFT)
+ }
+ else if (id == PfRule::ARITH_TRANS_SINE_BOUNDS)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ Assert(args[0].getType().isReal());
+ Node s = nm->mkNode(Kind::SINE, args[0]);
+ return nm->mkNode(AND, nm->mkNode(LEQ, s, one), nm->mkNode(GEQ, s, mone));
+ }
+ else if (id == PfRule::ARITH_TRANS_SINE_SHIFT)
{
Assert(children.empty());
Assert(args.size() == 3);
nm->mkNode(Kind::MULT, nm->mkConst<Rational>(2), s, pi)))),
nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))});
}
+ else if (id == PfRule::ARITH_TRANS_SINE_SYMMETRY)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ Assert(args[0].getType().isReal());
+ Node s1 = nm->mkNode(Kind::SINE, args[0]);
+ Node s2 = nm->mkNode(
+ Kind::SINE, Rewriter::rewrite(nm->mkNode(Kind::MULT, mone, args[0])));
+ return nm->mkNode(PLUS, s1, s2).eqNode(zero);
+ }
+ else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_ZERO)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ Assert(args[0].getType().isReal());
+ Node s = nm->mkNode(Kind::SINE, args[0]);
+ return nm->mkNode(
+ AND,
+ nm->mkNode(
+ IMPLIES, nm->mkNode(GT, args[0], zero), nm->mkNode(LT, s, args[0])),
+ nm->mkNode(IMPLIES,
+ nm->mkNode(LT, args[0], zero),
+ nm->mkNode(GT, s, args[0])));
+ }
+ else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_PI)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 1);
+ Assert(args[0].getType().isReal());
+ Node s = nm->mkNode(Kind::SINE, args[0]);
+ return nm->mkNode(
+ AND,
+ nm->mkNode(IMPLIES,
+ nm->mkNode(GT, args[0], mpi),
+ nm->mkNode(GT, s, nm->mkNode(MINUS, mpi, args[0]))),
+ nm->mkNode(IMPLIES,
+ nm->mkNode(LT, args[0], pi),
+ nm->mkNode(LT, s, nm->mkNode(MINUS, pi, args[0]))));
+ }
+ else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 6);
+ Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+ && args[0].getConst<Rational>().isIntegral());
+ Assert(args[1].getType().isReal());
+ Assert(args[2].getType().isReal());
+ Assert(args[3].getType().isReal());
+ Assert(args[4].isConst() && args[4].getKind() == Kind::CONST_RATIONAL);
+ Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL);
+ std::uint64_t d =
+ args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+ Node t = args[1];
+ Node lb = args[2];
+ Node ub = args[3];
+ Node l = args[4];
+ Node u = args[5];
+ TaylorGenerator tg;
+ TaylorGenerator::ApproximationBounds bounds;
+ tg.getPolynomialApproximationBounds(Kind::SINE, 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 lem = nm->mkNode(
+ Kind::IMPLIES,
+ mkBounds(t, lb, ub),
+ nm->mkNode(
+ Kind::LEQ, nm->mkNode(Kind::SINE, t), mkSecant(t, lb, ub, l, u)));
+ return Rewriter::rewrite(lem);
+ }
+ else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 5);
+ Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+ && args[0].getConst<Rational>().isIntegral());
+ Assert(args[1].getType().isReal());
+ Assert(args[2].getType().isReal());
+ Assert(args[3].getType().isReal());
+ std::uint64_t d =
+ args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+ Node t = args[1];
+ Node c = args[2];
+ Node lb = args[3];
+ Node ub = args[4];
+ TaylorGenerator tg;
+ TaylorGenerator::ApproximationBounds bounds;
+ tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
+ Node eval = Rewriter::rewrite(
+ bounds.d_upperPos.substitute(tg.getTaylorVariable(), c));
+ return Rewriter::rewrite(
+ nm->mkNode(Kind::IMPLIES,
+ mkBounds(t, lb, ub),
+ nm->mkNode(Kind::LEQ, nm->mkNode(Kind::SINE, t), eval)));
+ }
+ else if (id == PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 6);
+ Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+ && args[0].getConst<Rational>().isIntegral());
+ Assert(args[1].getType().isReal());
+ Assert(args[2].getType().isReal());
+ Assert(args[3].getType().isReal());
+ Assert(args[4].isConst() && args[4].getKind() == Kind::CONST_RATIONAL);
+ Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL);
+ std::uint64_t d =
+ args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+ Node t = args[1];
+ Node lb = args[2];
+ Node ub = args[3];
+ Node l = args[4];
+ Node u = args[5];
+ TaylorGenerator tg;
+ TaylorGenerator::ApproximationBounds bounds;
+ tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
+ Node evall =
+ Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), l));
+ Node evalu =
+ Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), u));
+ Node lem = nm->mkNode(
+ Kind::IMPLIES,
+ mkBounds(t, lb, ub),
+ nm->mkNode(
+ Kind::GEQ, nm->mkNode(Kind::SINE, t), mkSecant(t, lb, ub, l, u)));
+ return Rewriter::rewrite(lem);
+ }
+ else if (id == PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG)
+ {
+ Assert(children.empty());
+ Assert(args.size() == 5);
+ Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
+ && args[0].getConst<Rational>().isIntegral());
+ Assert(args[1].getType().isReal());
+ Assert(args[2].getType().isReal());
+ Assert(args[3].getType().isReal());
+ std::uint64_t d =
+ args[0].getConst<Rational>().getNumerator().toUnsignedInt();
+ Node t = args[1];
+ Node c = args[2];
+ Node lb = args[3];
+ Node ub = args[4];
+ TaylorGenerator tg;
+ TaylorGenerator::ApproximationBounds bounds;
+ tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
+ Node eval =
+ Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), c));
+ return Rewriter::rewrite(
+ nm->mkNode(Kind::IMPLIES,
+ mkBounds(t, lb, ub),
+ nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SINE, t), eval)));
+ }
return Node::null();
}
Node lem = nm->mkNode(Kind::AND,
nm->mkNode(Kind::LEQ, t, d_data->d_one),
nm->mkNode(Kind::GEQ, t, d_data->d_neg_one));
- d_data->d_im.addPendingLemma(lem,
- InferenceId::ARITH_NL_T_INIT_REFINE);
+ CDProof* proof = nullptr;
+ if (d_data->isProofEnabled())
+ {
+ proof = d_data->getProof();
+ proof->addStep(lem, PfRule::ARITH_TRANS_SINE_BOUNDS, {}, {t[0]});
+ }
+ d_data->d_im.addPendingLemma(
+ lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);
}
{
// sine symmetry: sin(t) - sin(-t) = 0
Node lem = nm->mkNode(Kind::PLUS, t, symn).eqNode(d_data->d_zero);
- d_data->d_im.addPendingLemma(lem,
- InferenceId::ARITH_NL_T_INIT_REFINE);
+ CDProof* proof = nullptr;
+ if (d_data->isProofEnabled())
+ {
+ proof = d_data->getProof();
+ proof->addStep(lem, PfRule::ARITH_TRANS_SINE_SYMMETRY, {}, {t[0]});
+ }
+ d_data->d_im.addPendingLemma(
+ lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);
}
{
// sine zero tangent:
nm->mkNode(Kind::IMPLIES,
nm->mkNode(Kind::LT, t[0], d_data->d_zero),
nm->mkNode(Kind::GT, t, t[0])));
- d_data->d_im.addPendingLemma(lem,
- InferenceId::ARITH_NL_T_INIT_REFINE);
+ CDProof* proof = nullptr;
+ if (d_data->isProofEnabled())
+ {
+ proof = d_data->getProof();
+ proof->addStep(
+ lem, PfRule::ARITH_TRANS_SINE_TANGENT_ZERO, {}, {t[0]});
+ }
+ d_data->d_im.addPendingLemma(
+ lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);
}
{
// sine pi tangent:
nm->mkNode(Kind::LT,
t,
nm->mkNode(Kind::MINUS, d_data->d_pi, t[0]))));
- d_data->d_im.addPendingLemma(lem,
- InferenceId::ARITH_NL_T_INIT_REFINE);
+ CDProof* proof = nullptr;
+ if (d_data->isProofEnabled())
+ {
+ proof = d_data->getProof();
+ proof->addStep(
+ lem, PfRule::ARITH_TRANS_SINE_TANGENT_PI, {}, {t[0]});
+ }
+ d_data->d_im.addPendingLemma(
+ lem, InferenceId::ARITH_NL_T_INIT_REFINE, proof);
}
{
Node lem =
}
}
-void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region)
+void SineSolver::doTangentLemma(
+ TNode e, TNode c, TNode poly_approx, int region, std::uint64_t d)
{
NodeManager* nm = NodeManager::currentNM();
nm->mkNode(
Kind::AND,
nm->mkNode(
- Kind::GEQ, e[0], usec ? Node(c) : regionToLowerBound(region)),
+ Kind::GEQ, e[0], usec ? regionToLowerBound(region) : Node(c)),
nm->mkNode(
Kind::LEQ, e[0], usec ? Node(c) : regionToUpperBound(region))),
nm->mkNode(convexity == Convexity::CONVEX ? Kind::GEQ : Kind::LEQ,
Trace("nl-ext-sine") << "*** 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();
+ if (convexity == Convexity::CONVEX)
+ {
+ if (usec)
+ {
+ proof->addStep(lem,
+ PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG,
+ {},
+ {nm->mkConst<Rational>(2 * d),
+ e[0],
+ c,
+ regionToLowerBound(region),
+ c});
+ }
+ else
+ {
+ proof->addStep(lem,
+ PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG,
+ {},
+ {nm->mkConst<Rational>(2 * d),
+ e[0],
+ c,
+ c,
+ regionToUpperBound(region)});
+ }
+ }
+ else
+ {
+ if (usec)
+ {
+ proof->addStep(lem,
+ PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS,
+ {},
+ {nm->mkConst<Rational>(2 * d),
+ e[0],
+ c,
+ regionToLowerBound(region),
+ c});
+ }
+ else
+ {
+ proof->addStep(lem,
+ PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS,
+ {},
+ {nm->mkConst<Rational>(2 * d),
+ e[0],
+ c,
+ c,
+ regionToUpperBound(region)});
+ }
+ }
+ }
d_data->d_im.addPendingLemma(
- lem, InferenceId::ARITH_NL_T_TANGENT, nullptr, true);
+ lem, InferenceId::ARITH_NL_T_TANGENT, proof, true);
}
void SineSolver::doSecantLemmas(TNode e,
void checkMonotonic();
/** Sent tangent lemma around c for e */
- void doTangentLemma(TNode e, TNode c, TNode poly_approx, int region);
+ void doTangentLemma(
+ TNode e, TNode c, TNode poly_approx, int region, std::uint64_t d);
/** Sent secant lemmas around c for e */
void doSecantLemmas(TNode e,
}
else if (k == Kind::SINE)
{
- d_sineSlv.doTangentLemma(tf, c, poly_approx_c, region);
+ d_sineSlv.doTangentLemma(tf, c, poly_approx_c, region, d);
}
}
else if (is_secant)
projects / cvc5.git / commitdiff