Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/nl/transcendental/proof_checker.cpp	Lines:	215	262	82.1 %
Date:	2021-09-17	Branches:	602	2282	26.4 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer, Aina Niemetz
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of proof checker for transcendentals.
 */

#include "theory/arith/nl/transcendental/proof_checker.h"

#include "expr/sequence.h"
#include "theory/arith/arith_utilities.h"
#include "theory/arith/nl/transcendental/taylor_generator.h"
#include "theory/rewriter.h"

using namespace cvc5::kind;

namespace cvc5 {
namespace theory {
namespace arith {
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_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_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);
  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(
    PfRule id, const std::vector<Node>& children, const std::vector<Node>& args)
{
  NodeManager* nm = NodeManager::currentNM();
  auto zero = nm->mkConst<Rational>(0);
  auto one = nm->mkConst<Rational>(1);
  auto mone = nm->mkConst<Rational>(-1);
  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());
    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_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_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());
    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());
    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);
    const auto& x = args[0];
    const auto& y = args[1];
    const auto& s = args[2];
    return nm->mkAnd(std::vector<Node>{
        nm->mkAnd(std::vector<Node>{
            nm->mkNode(Kind::GEQ, y, nm->mkNode(Kind::MULT, mone, pi)),
            nm->mkNode(Kind::LEQ, y, pi)}),
        nm->mkNode(
            Kind::ITE,
            nm->mkAnd(std::vector<Node>{
                nm->mkNode(Kind::GEQ, x, nm->mkNode(Kind::MULT, mone, pi)),
                nm->mkNode(Kind::LEQ, x, pi),
            }),
            x.eqNode(y),
            x.eqNode(nm->mkNode(
                Kind::PLUS,
                y,
                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();
}

}  // namespace transcendental
}  // namespace nl
}  // namespace arith
}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Gereon Kremer, Aina Niemetz
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of proof checker for transcendentals.
14		*/
15
16		#include "theory/arith/nl/transcendental/proof_checker.h"
17
18		#include "expr/sequence.h"
19		#include "theory/arith/arith_utilities.h"
20		#include "theory/arith/nl/transcendental/taylor_generator.h"
21		#include "theory/rewriter.h"
22
23		using namespace cvc5::kind;
24
25		namespace cvc5 {
26		namespace theory {
27		namespace arith {
28		namespace nl {
29		namespace transcendental {
30
31		namespace {
32
33		/**
34		* Helper method to construct (t >= lb) AND (t <= up)
35		*/
36	24	Node mkBounds(TNode t, TNode lb, TNode ub)
37		{
38	24	NodeManager* nm = NodeManager::currentNM();
39	96	return nm->mkAnd(std::vector<Node>{nm->mkNode(Kind::GEQ, t, lb),
40	96	nm->mkNode(Kind::LEQ, t, ub)});
41		}
42
43		/**
44		* Helper method to construct a secant plane:
45		* ((evall - evalu) / (l - u)) * (t - l) + evall
46		*/
47	22	Node mkSecant(TNode t, TNode l, TNode u, TNode evall, TNode evalu)
48		{
49	22	NodeManager* nm = NodeManager::currentNM();
50		return nm->mkNode(Kind::PLUS,
51	88	nm->mkNode(Kind::MULT,
52	88	nm->mkNode(Kind::DIVISION,
53	44	nm->mkNode(Kind::MINUS, evall, evalu),
54	44	nm->mkNode(Kind::MINUS, l, u)),
55	44	nm->mkNode(Kind::MINUS, t, l)),
56	66	evall);
57		}
58
59		} // namespace
60
61	593	void TranscendentalProofRuleChecker::registerTo(ProofChecker* pc)
62		{
63	593	pc->registerChecker(PfRule::ARITH_TRANS_PI, this);
64	593	pc->registerChecker(PfRule::ARITH_TRANS_EXP_NEG, this);
65	593	pc->registerChecker(PfRule::ARITH_TRANS_EXP_POSITIVITY, this);
66	593	pc->registerChecker(PfRule::ARITH_TRANS_EXP_SUPER_LIN, this);
67	593	pc->registerChecker(PfRule::ARITH_TRANS_EXP_ZERO, this);
68	593	pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS, this);
69	593	pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG, this);
70	593	pc->registerChecker(PfRule::ARITH_TRANS_EXP_APPROX_BELOW, this);
71	593	pc->registerChecker(PfRule::ARITH_TRANS_SINE_BOUNDS, this);
72	593	pc->registerChecker(PfRule::ARITH_TRANS_SINE_SHIFT, this);
73	593	pc->registerChecker(PfRule::ARITH_TRANS_SINE_SYMMETRY, this);
74	593	pc->registerChecker(PfRule::ARITH_TRANS_SINE_TANGENT_ZERO, this);
75	593	pc->registerChecker(PfRule::ARITH_TRANS_SINE_TANGENT_PI, this);
76	593	pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS, this);
77	593	pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG, this);
78	593	pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS, this);
79	593	pc->registerChecker(PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG, this);
80	593	}
81
82	107	Node TranscendentalProofRuleChecker::checkInternal(
83		PfRule id, const std::vector<Node>& children, const std::vector<Node>& args)
84		{
85	107	NodeManager* nm = NodeManager::currentNM();
86	214	auto zero = nm->mkConst<Rational>(0);
87	214	auto one = nm->mkConst<Rational>(1);
88	214	auto mone = nm->mkConst<Rational>(-1);
89	214	auto pi = nm->mkNullaryOperator(nm->realType(), Kind::PI);
90	214	auto mpi = nm->mkNode(Kind::MULT, mone, pi);
91	107	Trace("nl-trans-checker") << "Checking " << id << std::endl;
92	107	Trace("nl-trans-checker") << "Children:" << std::endl;
93	107	for (const auto& c : children)
94		{
95		Trace("nl-trans-checker") << "\t" << c << std::endl;
96		}
97	107	Trace("nl-trans-checker") << "Args:" << std::endl;
98	366	for (const auto& a : args)
99		{
100	259	Trace("nl-trans-checker") << "\t" << a << std::endl;
101		}
102	107	if (id == PfRule::ARITH_TRANS_PI)
103		{
104	14	Assert(children.empty());
105	14	Assert(args.size() == 2);
106	70	return nm->mkAnd(std::vector<Node>{nm->mkNode(Kind::GEQ, pi, args[0]),
107	56	nm->mkNode(Kind::LEQ, pi, args[1])});
108		}
109	93	else if (id == PfRule::ARITH_TRANS_EXP_NEG)
110		{
111	2	Assert(children.empty());
112	2	Assert(args.size() == 1);
113	4	Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
114		return nm->mkNode(
115	2	EQUAL, nm->mkNode(LT, args[0], zero), nm->mkNode(LT, e, one));
116		}
117	91	else if (id == PfRule::ARITH_TRANS_EXP_POSITIVITY)
118		{
119	7	Assert(children.empty());
120	7	Assert(args.size() == 1);
121	14	Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
122	7	return nm->mkNode(GT, e, zero);
123		}
124	84	else if (id == PfRule::ARITH_TRANS_EXP_SUPER_LIN)
125		{
126	3	Assert(children.empty());
127	3	Assert(args.size() == 1);
128	6	Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
129		return nm->mkNode(OR,
130	6	nm->mkNode(LEQ, args[0], zero),
131	9	nm->mkNode(GT, e, nm->mkNode(PLUS, args[0], one)));
132		}
133	81	else if (id == PfRule::ARITH_TRANS_EXP_ZERO)
134		{
135		Assert(children.empty());
136		Assert(args.size() == 1);
137		Node e = nm->mkNode(Kind::EXPONENTIAL, args[0]);
138		return nm->mkNode(EQUAL, args[0].eqNode(zero), e.eqNode(one));
139		}
140	81	else if (id == PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_POS)
141		{
142	14	Assert(children.empty());
143	14	Assert(args.size() == 4);
144	14	Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
145		&& args[0].getConst<Rational>().isIntegral());
146	14	Assert(args[1].getType().isReal());
147	14	Assert(args[2].isConst() && args[2].getKind() == Kind::CONST_RATIONAL);
148	14	Assert(args[3].isConst() && args[3].getKind() == Kind::CONST_RATIONAL);
149		std::uint64_t d =
150	14	args[0].getConst<Rational>().getNumerator().toUnsignedInt();
151	28	Node t = args[1];
152	28	Node l = args[2];
153	28	Node u = args[3];
154	28	TaylorGenerator tg;
155	28	TaylorGenerator::ApproximationBounds bounds;
156	14	tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d / 2, bounds);
157		Node evall = Rewriter::rewrite(
158	28	bounds.d_upperPos.substitute(tg.getTaylorVariable(), l));
159		Node evalu = Rewriter::rewrite(
160	28	bounds.d_upperPos.substitute(tg.getTaylorVariable(), u));
161	28	Node evalsecant = mkSecant(t, l, u, evall, evalu);
162		Node lem = nm->mkNode(
163		Kind::IMPLIES,
164	28	mkBounds(t, l, u),
165	56	nm->mkNode(Kind::LEQ, nm->mkNode(Kind::EXPONENTIAL, t), evalsecant));
166	14	return Rewriter::rewrite(lem);
167		}
168	67	else if (id == PfRule::ARITH_TRANS_EXP_APPROX_ABOVE_NEG)
169		{
170	6	Assert(children.empty());
171	6	Assert(args.size() == 4);
172	6	Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
173		&& args[0].getConst<Rational>().isIntegral());
174	6	Assert(args[1].getType().isReal());
175	6	Assert(args[2].isConst() && args[2].getKind() == Kind::CONST_RATIONAL);
176	6	Assert(args[3].isConst() && args[3].getKind() == Kind::CONST_RATIONAL);
177		std::uint64_t d =
178	6	args[0].getConst<Rational>().getNumerator().toUnsignedInt();
179	12	Node t = args[1];
180	12	Node l = args[2];
181	12	Node u = args[3];
182	12	TaylorGenerator tg;
183	12	TaylorGenerator::ApproximationBounds bounds;
184	6	tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d / 2, bounds);
185		Node evall = Rewriter::rewrite(
186	12	bounds.d_upperNeg.substitute(tg.getTaylorVariable(), l));
187		Node evalu = Rewriter::rewrite(
188	12	bounds.d_upperNeg.substitute(tg.getTaylorVariable(), u));
189	12	Node evalsecant = mkSecant(t, l, u, evall, evalu);
190		Node lem = nm->mkNode(
191		Kind::IMPLIES,
192	12	mkBounds(t, l, u),
193	24	nm->mkNode(Kind::LEQ, nm->mkNode(Kind::EXPONENTIAL, t), evalsecant));
194	6	return Rewriter::rewrite(lem);
195		}
196	61	else if (id == PfRule::ARITH_TRANS_EXP_APPROX_BELOW)
197		{
198	14	Assert(children.empty());
199	14	Assert(args.size() == 2);
200	14	Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
201		&& args[0].getConst<Rational>().isIntegral());
202	14	Assert(args[1].getType().isReal());
203		std::uint64_t d =
204	14	args[0].getConst<Rational>().getNumerator().toUnsignedInt();
205	28	Node t = args[1];
206	28	TaylorGenerator tg;
207	28	TaylorGenerator::ApproximationBounds bounds;
208	14	tg.getPolynomialApproximationBounds(Kind::EXPONENTIAL, d, bounds);
209		Node eval =
210	28	Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), t));
211		return nm->mkNode(
212	14	Kind::GEQ, std::vector<Node>{nm->mkNode(Kind::EXPONENTIAL, t), eval});
213		}
214	47	else if (id == PfRule::ARITH_TRANS_SINE_BOUNDS)
215		{
216	6	Assert(children.empty());
217	6	Assert(args.size() == 1);
218	6	Assert(args[0].getType().isReal());
219	12	Node s = nm->mkNode(Kind::SINE, args[0]);
220	6	return nm->mkNode(AND, nm->mkNode(LEQ, s, one), nm->mkNode(GEQ, s, mone));
221		}
222	41	else if (id == PfRule::ARITH_TRANS_SINE_SHIFT)
223		{
224	23	Assert(children.empty());
225	23	Assert(args.size() == 3);
226	23	const auto& x = args[0];
227	23	const auto& y = args[1];
228	23	const auto& s = args[2];
229	276	return nm->mkAnd(std::vector<Node>{
230	92	nm->mkAnd(std::vector<Node>{
231	46	nm->mkNode(Kind::GEQ, y, nm->mkNode(Kind::MULT, mone, pi)),
232	46	nm->mkNode(Kind::LEQ, y, pi)}),
233		nm->mkNode(
234		Kind::ITE,
235	92	nm->mkAnd(std::vector<Node>{
236	46	nm->mkNode(Kind::GEQ, x, nm->mkNode(Kind::MULT, mone, pi)),
237		nm->mkNode(Kind::LEQ, x, pi),
238	46	}),
239	46	x.eqNode(y),
240	46	x.eqNode(nm->mkNode(
241		Kind::PLUS,
242		y,
243	46	nm->mkNode(Kind::MULT, nm->mkConst<Rational>(2), s, pi)))),
244	138	nm->mkNode(Kind::SINE, y).eqNode(nm->mkNode(Kind::SINE, x))});
245		}
246	18	else if (id == PfRule::ARITH_TRANS_SINE_SYMMETRY)
247		{
248	6	Assert(children.empty());
249	6	Assert(args.size() == 1);
250	6	Assert(args[0].getType().isReal());
251	12	Node s1 = nm->mkNode(Kind::SINE, args[0]);
252		Node s2 = nm->mkNode(
253	12	Kind::SINE, Rewriter::rewrite(nm->mkNode(Kind::MULT, mone, args[0])));
254	6	return nm->mkNode(PLUS, s1, s2).eqNode(zero);
255		}
256	12	else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_ZERO)
257		{
258	6	Assert(children.empty());
259	6	Assert(args.size() == 1);
260	6	Assert(args[0].getType().isReal());
261	12	Node s = nm->mkNode(Kind::SINE, args[0]);
262		return nm->mkNode(
263		AND,
264	24	nm->mkNode(
265	24	IMPLIES, nm->mkNode(GT, args[0], zero), nm->mkNode(LT, s, args[0])),
266	24	nm->mkNode(IMPLIES,
267	12	nm->mkNode(LT, args[0], zero),
268	30	nm->mkNode(GT, s, args[0])));
269		}
270	6	else if (id == PfRule::ARITH_TRANS_SINE_TANGENT_PI)
271		{
272	2	Assert(children.empty());
273	2	Assert(args.size() == 1);
274	2	Assert(args[0].getType().isReal());
275	4	Node s = nm->mkNode(Kind::SINE, args[0]);
276		return nm->mkNode(
277		AND,
278	8	nm->mkNode(IMPLIES,
279	4	nm->mkNode(GT, args[0], mpi),
280	4	nm->mkNode(GT, s, nm->mkNode(MINUS, mpi, args[0]))),
281	8	nm->mkNode(IMPLIES,
282	4	nm->mkNode(LT, args[0], pi),
283	10	nm->mkNode(LT, s, nm->mkNode(MINUS, pi, args[0]))));
284		}
285	4	else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_NEG)
286		{
287		Assert(children.empty());
288		Assert(args.size() == 6);
289		Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
290		&& args[0].getConst<Rational>().isIntegral());
291		Assert(args[1].getType().isReal());
292		Assert(args[2].getType().isReal());
293		Assert(args[3].getType().isReal());
294		Assert(args[4].isConst() && args[4].getKind() == Kind::CONST_RATIONAL);
295		Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL);
296		std::uint64_t d =
297		args[0].getConst<Rational>().getNumerator().toUnsignedInt();
298		Node t = args[1];
299		Node lb = args[2];
300		Node ub = args[3];
301		Node l = args[4];
302		Node u = args[5];
303		TaylorGenerator tg;
304		TaylorGenerator::ApproximationBounds bounds;
305		tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
306		Node evall = Rewriter::rewrite(
307		bounds.d_upperNeg.substitute(tg.getTaylorVariable(), l));
308		Node evalu = Rewriter::rewrite(
309		bounds.d_upperNeg.substitute(tg.getTaylorVariable(), u));
310		Node lem = nm->mkNode(
311		Kind::IMPLIES,
312		mkBounds(t, lb, ub),
313		nm->mkNode(
314		Kind::LEQ, nm->mkNode(Kind::SINE, t), mkSecant(t, lb, ub, l, u)));
315		return Rewriter::rewrite(lem);
316		}
317	4	else if (id == PfRule::ARITH_TRANS_SINE_APPROX_ABOVE_POS)
318		{
319		Assert(children.empty());
320		Assert(args.size() == 5);
321		Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
322		&& args[0].getConst<Rational>().isIntegral());
323		Assert(args[1].getType().isReal());
324		Assert(args[2].getType().isReal());
325		Assert(args[3].getType().isReal());
326		std::uint64_t d =
327		args[0].getConst<Rational>().getNumerator().toUnsignedInt();
328		Node t = args[1];
329		Node c = args[2];
330		Node lb = args[3];
331		Node ub = args[4];
332		TaylorGenerator tg;
333		TaylorGenerator::ApproximationBounds bounds;
334		tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
335		Node eval = Rewriter::rewrite(
336		bounds.d_upperPos.substitute(tg.getTaylorVariable(), c));
337		return Rewriter::rewrite(
338		nm->mkNode(Kind::IMPLIES,
339		mkBounds(t, lb, ub),
340		nm->mkNode(Kind::LEQ, nm->mkNode(Kind::SINE, t), eval)));
341		}
342	4	else if (id == PfRule::ARITH_TRANS_SINE_APPROX_BELOW_POS)
343		{
344	2	Assert(children.empty());
345	2	Assert(args.size() == 6);
346	2	Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
347		&& args[0].getConst<Rational>().isIntegral());
348	2	Assert(args[1].getType().isReal());
349	2	Assert(args[2].getType().isReal());
350	2	Assert(args[3].getType().isReal());
351	2	Assert(args[4].isConst() && args[4].getKind() == Kind::CONST_RATIONAL);
352	2	Assert(args[5].isConst() && args[5].getKind() == Kind::CONST_RATIONAL);
353		std::uint64_t d =
354	2	args[0].getConst<Rational>().getNumerator().toUnsignedInt();
355	4	Node t = args[1];
356	4	Node lb = args[2];
357	4	Node ub = args[3];
358	4	Node l = args[4];
359	4	Node u = args[5];
360	4	TaylorGenerator tg;
361	4	TaylorGenerator::ApproximationBounds bounds;
362	2	tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
363		Node evall =
364	4	Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), l));
365		Node evalu =
366	4	Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), u));
367		Node lem = nm->mkNode(
368		Kind::IMPLIES,
369	4	mkBounds(t, lb, ub),
370	8	nm->mkNode(
371	16	Kind::GEQ, nm->mkNode(Kind::SINE, t), mkSecant(t, lb, ub, l, u)));
372	2	return Rewriter::rewrite(lem);
373		}
374	2	else if (id == PfRule::ARITH_TRANS_SINE_APPROX_BELOW_NEG)
375		{
376	2	Assert(children.empty());
377	2	Assert(args.size() == 5);
378	2	Assert(args[0].isConst() && args[0].getKind() == Kind::CONST_RATIONAL
379		&& args[0].getConst<Rational>().isIntegral());
380	2	Assert(args[1].getType().isReal());
381	2	Assert(args[2].getType().isReal());
382	2	Assert(args[3].getType().isReal());
383		std::uint64_t d =
384	2	args[0].getConst<Rational>().getNumerator().toUnsignedInt();
385	4	Node t = args[1];
386	4	Node c = args[2];
387	4	Node lb = args[3];
388	4	Node ub = args[4];
389	4	TaylorGenerator tg;
390	4	TaylorGenerator::ApproximationBounds bounds;
391	2	tg.getPolynomialApproximationBounds(Kind::SINE, d / 2, bounds);
392		Node eval =
393	4	Rewriter::rewrite(bounds.d_lower.substitute(tg.getTaylorVariable(), c));
394		return Rewriter::rewrite(
395	8	nm->mkNode(Kind::IMPLIES,
396	4	mkBounds(t, lb, ub),
397	6	nm->mkNode(Kind::GEQ, nm->mkNode(Kind::SINE, t), eval)));
398		}
399		return Node::null();
400		}
401
402		} // namespace transcendental
403		} // namespace nl
404		} // namespace arith
405		} // namespace theory
406	29577	} // namespace cvc5