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