1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Martin Brain, Andres Noetzli, Aina Niemetz |
4 |
|
* Copyright (c) 2013 University of Oxford |
5 |
|
* |
6 |
|
* This file is part of the cvc5 project. |
7 |
|
* |
8 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
9 |
|
* in the top-level source directory and their institutional affiliations. |
10 |
|
* All rights reserved. See the file COPYING in the top-level source |
11 |
|
* directory for licensing information. |
12 |
|
* **************************************************************************** |
13 |
|
* |
14 |
|
* Rewrite rules for floating point theories. |
15 |
|
* |
16 |
|
* \todo - Single argument constant propagate / simplify |
17 |
|
* - Push negations through arithmetic operators (include max and min? |
18 |
|
* maybe not due to +0/-0) |
19 |
|
* - classifications to normal tests (maybe) |
20 |
|
* - (= x (fp.neg x)) --> (isNaN x) |
21 |
|
* - (fp.eq x (fp.neg x)) --> (isZero x) (previous and reorganise |
22 |
|
* should be sufficient) |
23 |
|
* - (fp.eq x const) --> various = depending on const |
24 |
|
* - (fp.isPositive (fp.neg x)) --> (fp.isNegative x) |
25 |
|
* - (fp.isNegative (fp.neg x)) --> (fp.isPositive x) |
26 |
|
* - (fp.isPositive (fp.abs x)) --> (not (isNaN x)) |
27 |
|
* - (fp.isNegative (fp.abs x)) --> false |
28 |
|
* - A -> castA --> A |
29 |
|
* - A -> castB -> castC --> A -> castC if A <= B <= C |
30 |
|
* - A -> castB -> castA --> A if A <= B |
31 |
|
* - promotion converts can ignore rounding mode |
32 |
|
* - Samuel Figuer results |
33 |
|
*/ |
34 |
|
|
35 |
|
#include "theory/fp/theory_fp_rewriter.h" |
36 |
|
|
37 |
|
#include <algorithm> |
38 |
|
|
39 |
|
#include "base/check.h" |
40 |
|
#include "theory/bv/theory_bv_utils.h" |
41 |
|
#include "theory/fp/fp_converter.h" |
42 |
|
|
43 |
|
namespace cvc5 { |
44 |
|
namespace theory { |
45 |
|
namespace fp { |
46 |
|
|
47 |
|
namespace rewrite { |
48 |
|
/** Rewrite rules **/ |
49 |
|
template <RewriteFunction first, RewriteFunction second> |
50 |
232 |
RewriteResponse then (TNode node, bool isPreRewrite) { |
51 |
464 |
RewriteResponse result(first(node, isPreRewrite)); |
52 |
|
|
53 |
232 |
if (result.d_status == REWRITE_DONE) |
54 |
|
{ |
55 |
232 |
return second(result.d_node, isPreRewrite); |
56 |
|
} |
57 |
|
else |
58 |
|
{ |
59 |
|
return result; |
60 |
|
} |
61 |
|
} |
62 |
|
|
63 |
|
RewriteResponse notFP(TNode node, bool isPreRewrite) |
64 |
|
{ |
65 |
|
Unreachable() << "non floating-point kind (" << node.getKind() |
66 |
|
<< ") in floating point rewrite?"; |
67 |
|
} |
68 |
|
|
69 |
10828 |
RewriteResponse identity(TNode node, bool isPreRewrite) |
70 |
|
{ |
71 |
10828 |
return RewriteResponse(REWRITE_DONE, node); |
72 |
|
} |
73 |
|
|
74 |
|
RewriteResponse type(TNode node, bool isPreRewrite) |
75 |
|
{ |
76 |
|
Unreachable() << "sort kind (" << node.getKind() |
77 |
|
<< ") found in expression?"; |
78 |
|
} |
79 |
|
|
80 |
58 |
RewriteResponse removeToFPGeneric(TNode node, bool isPreRewrite) |
81 |
|
{ |
82 |
58 |
Assert(!isPreRewrite); |
83 |
58 |
Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_GENERIC); |
84 |
|
|
85 |
|
FloatingPointToFPGeneric info = |
86 |
58 |
node.getOperator().getConst<FloatingPointToFPGeneric>(); |
87 |
|
|
88 |
58 |
uint32_t children = node.getNumChildren(); |
89 |
|
|
90 |
116 |
Node op; |
91 |
58 |
NodeManager* nm = NodeManager::currentNM(); |
92 |
|
|
93 |
58 |
if (children == 1) |
94 |
|
{ |
95 |
18 |
op = nm->mkConst(FloatingPointToFPIEEEBitVector(info)); |
96 |
18 |
return RewriteResponse(REWRITE_AGAIN, nm->mkNode(op, node[0])); |
97 |
|
} |
98 |
40 |
Assert(children == 2); |
99 |
40 |
Assert(node[0].getType().isRoundingMode()); |
100 |
|
|
101 |
80 |
TypeNode t = node[1].getType(); |
102 |
|
|
103 |
40 |
if (t.isFloatingPoint()) |
104 |
|
{ |
105 |
8 |
op = nm->mkConst(FloatingPointToFPFloatingPoint(info)); |
106 |
|
} |
107 |
32 |
else if (t.isReal()) |
108 |
|
{ |
109 |
16 |
op = nm->mkConst(FloatingPointToFPReal(info)); |
110 |
|
} |
111 |
|
else |
112 |
|
{ |
113 |
16 |
Assert(t.isBitVector()); |
114 |
16 |
op = nm->mkConst(FloatingPointToFPSignedBitVector(info)); |
115 |
|
} |
116 |
|
|
117 |
40 |
return RewriteResponse(REWRITE_AGAIN, nm->mkNode(op, node[0], node[1])); |
118 |
|
} |
119 |
|
|
120 |
423 |
RewriteResponse removeDoubleNegation(TNode node, bool isPreRewrite) |
121 |
|
{ |
122 |
423 |
Assert(node.getKind() == kind::FLOATINGPOINT_NEG); |
123 |
423 |
if (node[0].getKind() == kind::FLOATINGPOINT_NEG) { |
124 |
4 |
return RewriteResponse(REWRITE_AGAIN, node[0][0]); |
125 |
|
} |
126 |
|
|
127 |
419 |
return RewriteResponse(REWRITE_DONE, node); |
128 |
|
} |
129 |
|
|
130 |
78 |
RewriteResponse compactAbs(TNode node, bool isPreRewrite) |
131 |
|
{ |
132 |
78 |
Assert(node.getKind() == kind::FLOATINGPOINT_ABS); |
133 |
234 |
if (node[0].getKind() == kind::FLOATINGPOINT_NEG |
134 |
234 |
|| node[0].getKind() == kind::FLOATINGPOINT_ABS) |
135 |
|
{ |
136 |
|
Node ret = |
137 |
16 |
NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_ABS, node[0][0]); |
138 |
8 |
return RewriteResponse(REWRITE_AGAIN, ret); |
139 |
|
} |
140 |
|
|
141 |
70 |
return RewriteResponse(REWRITE_DONE, node); |
142 |
|
} |
143 |
|
|
144 |
31 |
RewriteResponse convertSubtractionToAddition(TNode node, bool isPreRewrite) |
145 |
|
{ |
146 |
31 |
Assert(node.getKind() == kind::FLOATINGPOINT_SUB); |
147 |
62 |
Node negation = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_NEG,node[2]); |
148 |
62 |
Node addition = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_PLUS,node[0],node[1],negation); |
149 |
62 |
return RewriteResponse(REWRITE_DONE, addition); |
150 |
|
} |
151 |
|
|
152 |
232 |
RewriteResponse breakChain (TNode node, bool isPreRewrite) { |
153 |
232 |
Assert(isPreRewrite); // Should be run first |
154 |
|
|
155 |
232 |
Kind k = node.getKind(); |
156 |
232 |
Assert(k == kind::FLOATINGPOINT_EQ || k == kind::FLOATINGPOINT_GEQ |
157 |
|
|| k == kind::FLOATINGPOINT_LEQ || k == kind::FLOATINGPOINT_GT |
158 |
|
|| k == kind::FLOATINGPOINT_LT); |
159 |
|
|
160 |
232 |
size_t children = node.getNumChildren(); |
161 |
232 |
if (children > 2) { |
162 |
|
NodeBuilder conjunction(kind::AND); |
163 |
|
|
164 |
|
for (size_t i = 0; i < children - 1; ++i) { |
165 |
|
for (size_t j = i + 1; j < children; ++j) { |
166 |
|
conjunction << NodeManager::currentNM()->mkNode(k, node[i], node[j]); |
167 |
|
} |
168 |
|
} |
169 |
|
return RewriteResponse(REWRITE_AGAIN_FULL, conjunction); |
170 |
|
|
171 |
|
} else { |
172 |
232 |
return RewriteResponse(REWRITE_DONE, node); |
173 |
|
} |
174 |
|
} |
175 |
|
|
176 |
|
|
177 |
|
/* Implies (fp.eq x x) --> (not (isNaN x)) |
178 |
|
*/ |
179 |
|
|
180 |
12 |
RewriteResponse ieeeEqToEq(TNode node, bool isPreRewrite) |
181 |
|
{ |
182 |
12 |
Assert(node.getKind() == kind::FLOATINGPOINT_EQ); |
183 |
12 |
NodeManager *nm = NodeManager::currentNM(); |
184 |
|
|
185 |
|
return RewriteResponse(REWRITE_DONE, |
186 |
48 |
nm->mkNode(kind::AND, |
187 |
48 |
nm->mkNode(kind::AND, |
188 |
24 |
nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0])), |
189 |
24 |
nm->mkNode(kind::NOT, nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[1]))), |
190 |
48 |
nm->mkNode(kind::OR, |
191 |
24 |
nm->mkNode(kind::EQUAL, node[0], node[1]), |
192 |
48 |
nm->mkNode(kind::AND, |
193 |
24 |
nm->mkNode(kind::FLOATINGPOINT_ISZ, node[0]), |
194 |
36 |
nm->mkNode(kind::FLOATINGPOINT_ISZ, node[1]))))); |
195 |
|
} |
196 |
|
|
197 |
21 |
RewriteResponse geqToleq(TNode node, bool isPreRewrite) |
198 |
|
{ |
199 |
21 |
Assert(node.getKind() == kind::FLOATINGPOINT_GEQ); |
200 |
21 |
return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LEQ,node[1],node[0])); |
201 |
|
} |
202 |
|
|
203 |
4 |
RewriteResponse gtTolt(TNode node, bool isPreRewrite) |
204 |
|
{ |
205 |
4 |
Assert(node.getKind() == kind::FLOATINGPOINT_GT); |
206 |
4 |
return RewriteResponse(REWRITE_DONE,NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_LT,node[1],node[0])); |
207 |
|
} |
208 |
|
|
209 |
|
RewriteResponse removed(TNode node, bool isPreRewrite) |
210 |
|
{ |
211 |
|
Unreachable() << "kind (" << node.getKind() |
212 |
|
<< ") should have been removed?"; |
213 |
|
} |
214 |
|
|
215 |
|
RewriteResponse variable(TNode node, bool isPreRewrite) |
216 |
|
{ |
217 |
|
// We should only get floating point and rounding mode variables to rewrite. |
218 |
|
TypeNode tn = node.getType(true); |
219 |
|
Assert(tn.isFloatingPoint() || tn.isRoundingMode()); |
220 |
|
|
221 |
|
// Not that we do anything with them... |
222 |
|
return RewriteResponse(REWRITE_DONE, node); |
223 |
|
} |
224 |
|
|
225 |
2316 |
RewriteResponse equal (TNode node, bool isPreRewrite) { |
226 |
2316 |
Assert(node.getKind() == kind::EQUAL); |
227 |
|
|
228 |
|
// We should only get equalities of floating point or rounding mode types. |
229 |
4632 |
TypeNode tn = node[0].getType(true); |
230 |
|
|
231 |
2316 |
Assert(tn.isFloatingPoint() || tn.isRoundingMode()); |
232 |
2316 |
Assert(tn |
233 |
|
== node[1].getType(true)); // Should be ensured by the typing rules |
234 |
|
|
235 |
2316 |
if (node[0] == node[1]) { |
236 |
65 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true)); |
237 |
2251 |
} else if (!isPreRewrite && (node[0] > node[1])) { |
238 |
|
Node normal = |
239 |
406 |
NodeManager::currentNM()->mkNode(kind::EQUAL, node[1], node[0]); |
240 |
203 |
return RewriteResponse(REWRITE_DONE, normal); |
241 |
|
} else { |
242 |
2048 |
return RewriteResponse(REWRITE_DONE, node); |
243 |
|
} |
244 |
|
} |
245 |
|
|
246 |
|
|
247 |
|
// Note these cannot be assumed to be symmetric for +0/-0, thus no symmetry reorder |
248 |
360 |
RewriteResponse compactMinMax (TNode node, bool isPreRewrite) { |
249 |
|
#ifdef CVC5_ASSERTIONS |
250 |
360 |
Kind k = node.getKind(); |
251 |
360 |
Assert((k == kind::FLOATINGPOINT_MIN) || (k == kind::FLOATINGPOINT_MAX) |
252 |
|
|| (k == kind::FLOATINGPOINT_MIN_TOTAL) |
253 |
|
|| (k == kind::FLOATINGPOINT_MAX_TOTAL)); |
254 |
|
#endif |
255 |
360 |
if (node[0] == node[1]) { |
256 |
23 |
return RewriteResponse(REWRITE_AGAIN, node[0]); |
257 |
|
} else { |
258 |
337 |
return RewriteResponse(REWRITE_DONE, node); |
259 |
|
} |
260 |
|
} |
261 |
|
|
262 |
|
|
263 |
|
RewriteResponse reorderFPEquality (TNode node, bool isPreRewrite) { |
264 |
|
Assert(node.getKind() == kind::FLOATINGPOINT_EQ); |
265 |
|
Assert(!isPreRewrite); // Likely redundant in pre-rewrite |
266 |
|
|
267 |
|
if (node[0] > node[1]) { |
268 |
|
Node normal = NodeManager::currentNM()->mkNode(kind::FLOATINGPOINT_EQ,node[1],node[0]); |
269 |
|
return RewriteResponse(REWRITE_DONE, normal); |
270 |
|
} else { |
271 |
|
return RewriteResponse(REWRITE_DONE, node); |
272 |
|
} |
273 |
|
} |
274 |
|
|
275 |
1114 |
RewriteResponse reorderBinaryOperation (TNode node, bool isPreRewrite) { |
276 |
1114 |
Kind k = node.getKind(); |
277 |
1114 |
Assert((k == kind::FLOATINGPOINT_PLUS) || (k == kind::FLOATINGPOINT_MULT)); |
278 |
1114 |
Assert(!isPreRewrite); // Likely redundant in pre-rewrite |
279 |
|
|
280 |
1114 |
if (node[1] > node[2]) { |
281 |
488 |
Node normal = NodeManager::currentNM()->mkNode(k,node[0],node[2],node[1]); |
282 |
244 |
return RewriteResponse(REWRITE_DONE, normal); |
283 |
|
} else { |
284 |
870 |
return RewriteResponse(REWRITE_DONE, node); |
285 |
|
} |
286 |
|
} |
287 |
|
|
288 |
|
RewriteResponse reorderFMA (TNode node, bool isPreRewrite) { |
289 |
|
Assert(node.getKind() == kind::FLOATINGPOINT_FMA); |
290 |
|
Assert(!isPreRewrite); // Likely redundant in pre-rewrite |
291 |
|
|
292 |
|
if (node[1] > node[2]) { |
293 |
|
Node normal = NodeManager::currentNM()->mkNode( |
294 |
|
kind::FLOATINGPOINT_FMA, {node[0], node[2], node[1], node[3]}); |
295 |
|
return RewriteResponse(REWRITE_DONE, normal); |
296 |
|
} else { |
297 |
|
return RewriteResponse(REWRITE_DONE, node); |
298 |
|
} |
299 |
|
} |
300 |
|
|
301 |
487 |
RewriteResponse removeSignOperations (TNode node, bool isPreRewrite) { |
302 |
487 |
Assert(node.getKind() == kind::FLOATINGPOINT_ISN |
303 |
|
|| node.getKind() == kind::FLOATINGPOINT_ISSN |
304 |
|
|| node.getKind() == kind::FLOATINGPOINT_ISZ |
305 |
|
|| node.getKind() == kind::FLOATINGPOINT_ISINF |
306 |
|
|| node.getKind() == kind::FLOATINGPOINT_ISNAN); |
307 |
487 |
Assert(node.getNumChildren() == 1); |
308 |
|
|
309 |
487 |
Kind childKind(node[0].getKind()); |
310 |
|
|
311 |
487 |
if ((childKind == kind::FLOATINGPOINT_NEG) || |
312 |
|
(childKind == kind::FLOATINGPOINT_ABS)) { |
313 |
|
|
314 |
|
Node rewritten = NodeManager::currentNM()->mkNode(node.getKind(),node[0][0]); |
315 |
|
return RewriteResponse(REWRITE_AGAIN_FULL, rewritten); |
316 |
|
} else { |
317 |
487 |
return RewriteResponse(REWRITE_DONE, node); |
318 |
|
} |
319 |
|
} |
320 |
|
|
321 |
179 |
RewriteResponse compactRemainder (TNode node, bool isPreRewrite) { |
322 |
179 |
Assert(node.getKind() == kind::FLOATINGPOINT_REM); |
323 |
179 |
Assert(!isPreRewrite); // status assumes parts have been rewritten |
324 |
|
|
325 |
358 |
Node working = node; |
326 |
|
|
327 |
|
// (fp.rem (fp.rem X Y) Y) == (fp.rem X Y) |
328 |
358 |
if (working[0].getKind() == kind::FLOATINGPOINT_REM && // short-cut matters! |
329 |
179 |
working[0][1] == working[1]) { |
330 |
|
working = working[0]; |
331 |
|
} |
332 |
|
|
333 |
|
// Sign of the RHS does not matter |
334 |
716 |
if (working[1].getKind() == kind::FLOATINGPOINT_NEG || |
335 |
537 |
working[1].getKind() == kind::FLOATINGPOINT_ABS) { |
336 |
|
working[1] = working[1][0]; |
337 |
|
} |
338 |
|
|
339 |
|
// Lift negation out of the LHS so it can be cancelled out |
340 |
179 |
if (working[0].getKind() == kind::FLOATINGPOINT_NEG) { |
341 |
|
NodeManager * nm = NodeManager::currentNM(); |
342 |
|
working = nm->mkNode( |
343 |
|
kind::FLOATINGPOINT_NEG, |
344 |
|
nm->mkNode(kind::FLOATINGPOINT_REM, working[0][0], working[1])); |
345 |
|
// in contrast to other rewrites here, this requires rewrite again full |
346 |
|
return RewriteResponse(REWRITE_AGAIN_FULL, working); |
347 |
|
} |
348 |
|
|
349 |
179 |
return RewriteResponse(REWRITE_DONE, working); |
350 |
|
} |
351 |
|
|
352 |
446 |
RewriteResponse leqId(TNode node, bool isPreRewrite) |
353 |
|
{ |
354 |
446 |
Assert(node.getKind() == kind::FLOATINGPOINT_LEQ); |
355 |
|
|
356 |
446 |
if (node[0] == node[1]) |
357 |
|
{ |
358 |
|
NodeManager *nm = NodeManager::currentNM(); |
359 |
|
return RewriteResponse( |
360 |
|
isPreRewrite ? REWRITE_DONE : REWRITE_AGAIN_FULL, |
361 |
|
nm->mkNode(kind::NOT, |
362 |
|
nm->mkNode(kind::FLOATINGPOINT_ISNAN, node[0]))); |
363 |
|
} |
364 |
446 |
return RewriteResponse(REWRITE_DONE, node); |
365 |
|
} |
366 |
|
|
367 |
135 |
RewriteResponse ltId(TNode node, bool isPreRewrite) |
368 |
|
{ |
369 |
135 |
Assert(node.getKind() == kind::FLOATINGPOINT_LT); |
370 |
|
|
371 |
135 |
if (node[0] == node[1]) |
372 |
|
{ |
373 |
|
return RewriteResponse(REWRITE_DONE, |
374 |
|
NodeManager::currentNM()->mkConst(false)); |
375 |
|
} |
376 |
135 |
return RewriteResponse(REWRITE_DONE, node); |
377 |
|
} |
378 |
|
|
379 |
32 |
RewriteResponse toFPSignedBV(TNode node, bool isPreRewrite) |
380 |
|
{ |
381 |
32 |
Assert(!isPreRewrite); |
382 |
32 |
Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR); |
383 |
|
|
384 |
|
/* symFPU does not allow conversions from signed bit-vector of size 1 */ |
385 |
32 |
if (node[1].getType().getBitVectorSize() == 1) |
386 |
|
{ |
387 |
24 |
NodeManager* nm = NodeManager::currentNM(); |
388 |
48 |
Node op = nm->mkConst(FloatingPointToFPUnsignedBitVector( |
389 |
96 |
node.getOperator().getConst<FloatingPointToFPSignedBitVector>())); |
390 |
48 |
Node fromubv = nm->mkNode(op, node[0], node[1]); |
391 |
|
return RewriteResponse( |
392 |
|
REWRITE_AGAIN_FULL, |
393 |
144 |
nm->mkNode(kind::ITE, |
394 |
48 |
node[1].eqNode(bv::utils::mkOne(1)), |
395 |
48 |
nm->mkNode(kind::FLOATINGPOINT_NEG, fromubv), |
396 |
24 |
fromubv)); |
397 |
|
} |
398 |
8 |
return RewriteResponse(REWRITE_DONE, node); |
399 |
|
} |
400 |
|
|
401 |
|
}; // namespace rewrite |
402 |
|
|
403 |
|
namespace constantFold { |
404 |
|
|
405 |
26 |
RewriteResponse fpLiteral(TNode node, bool isPreRewrite) |
406 |
|
{ |
407 |
26 |
Assert(node.getKind() == kind::FLOATINGPOINT_FP); |
408 |
|
|
409 |
52 |
BitVector bv(node[0].getConst<BitVector>()); |
410 |
26 |
bv = bv.concat(node[1].getConst<BitVector>()); |
411 |
26 |
bv = bv.concat(node[2].getConst<BitVector>()); |
412 |
|
|
413 |
|
// +1 to support the hidden bit |
414 |
|
Node lit = NodeManager::currentNM()->mkConst( |
415 |
52 |
FloatingPoint(node[1].getConst<BitVector>().getSize(), |
416 |
52 |
node[2].getConst<BitVector>().getSize() + 1, |
417 |
78 |
bv)); |
418 |
|
|
419 |
52 |
return RewriteResponse(REWRITE_DONE, lit); |
420 |
|
} |
421 |
|
|
422 |
9 |
RewriteResponse abs(TNode node, bool isPreRewrite) |
423 |
|
{ |
424 |
9 |
Assert(node.getKind() == kind::FLOATINGPOINT_ABS); |
425 |
9 |
Assert(node.getNumChildren() == 1); |
426 |
|
|
427 |
|
return RewriteResponse(REWRITE_DONE, |
428 |
27 |
NodeManager::currentNM()->mkConst( |
429 |
27 |
node[0].getConst<FloatingPoint>().absolute())); |
430 |
|
} |
431 |
|
|
432 |
127 |
RewriteResponse neg(TNode node, bool isPreRewrite) |
433 |
|
{ |
434 |
127 |
Assert(node.getKind() == kind::FLOATINGPOINT_NEG); |
435 |
127 |
Assert(node.getNumChildren() == 1); |
436 |
|
|
437 |
|
return RewriteResponse(REWRITE_DONE, |
438 |
381 |
NodeManager::currentNM()->mkConst( |
439 |
381 |
node[0].getConst<FloatingPoint>().negate())); |
440 |
|
} |
441 |
|
|
442 |
451 |
RewriteResponse plus(TNode node, bool isPreRewrite) |
443 |
|
{ |
444 |
451 |
Assert(node.getKind() == kind::FLOATINGPOINT_PLUS); |
445 |
451 |
Assert(node.getNumChildren() == 3); |
446 |
|
|
447 |
451 |
RoundingMode rm(node[0].getConst<RoundingMode>()); |
448 |
902 |
FloatingPoint arg1(node[1].getConst<FloatingPoint>()); |
449 |
902 |
FloatingPoint arg2(node[2].getConst<FloatingPoint>()); |
450 |
|
|
451 |
451 |
Assert(arg1.getSize() == arg2.getSize()); |
452 |
|
|
453 |
|
return RewriteResponse( |
454 |
902 |
REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.plus(rm, arg2))); |
455 |
|
} |
456 |
|
|
457 |
132 |
RewriteResponse mult(TNode node, bool isPreRewrite) |
458 |
|
{ |
459 |
132 |
Assert(node.getKind() == kind::FLOATINGPOINT_MULT); |
460 |
132 |
Assert(node.getNumChildren() == 3); |
461 |
|
|
462 |
132 |
RoundingMode rm(node[0].getConst<RoundingMode>()); |
463 |
264 |
FloatingPoint arg1(node[1].getConst<FloatingPoint>()); |
464 |
264 |
FloatingPoint arg2(node[2].getConst<FloatingPoint>()); |
465 |
|
|
466 |
132 |
Assert(arg1.getSize() == arg2.getSize()); |
467 |
|
|
468 |
|
return RewriteResponse( |
469 |
264 |
REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1.mult(rm, arg2))); |
470 |
|
} |
471 |
|
|
472 |
|
RewriteResponse fma(TNode node, bool isPreRewrite) |
473 |
|
{ |
474 |
|
Assert(node.getKind() == kind::FLOATINGPOINT_FMA); |
475 |
|
Assert(node.getNumChildren() == 4); |
476 |
|
|
477 |
|
RoundingMode rm(node[0].getConst<RoundingMode>()); |
478 |
|
FloatingPoint arg1(node[1].getConst<FloatingPoint>()); |
479 |
|
FloatingPoint arg2(node[2].getConst<FloatingPoint>()); |
480 |
|
FloatingPoint arg3(node[3].getConst<FloatingPoint>()); |
481 |
|
|
482 |
|
Assert(arg1.getSize() == arg2.getSize()); |
483 |
|
Assert(arg1.getSize() == arg3.getSize()); |
484 |
|
|
485 |
|
return RewriteResponse( |
486 |
|
REWRITE_DONE, |
487 |
|
NodeManager::currentNM()->mkConst(arg1.fma(rm, arg2, arg3))); |
488 |
|
} |
489 |
|
|
490 |
189 |
RewriteResponse div(TNode node, bool isPreRewrite) |
491 |
|
{ |
492 |
189 |
Assert(node.getKind() == kind::FLOATINGPOINT_DIV); |
493 |
189 |
Assert(node.getNumChildren() == 3); |
494 |
|
|
495 |
189 |
RoundingMode rm(node[0].getConst<RoundingMode>()); |
496 |
378 |
FloatingPoint arg1(node[1].getConst<FloatingPoint>()); |
497 |
378 |
FloatingPoint arg2(node[2].getConst<FloatingPoint>()); |
498 |
|
|
499 |
189 |
Assert(arg1.getSize() == arg2.getSize()); |
500 |
|
|
501 |
|
return RewriteResponse(REWRITE_DONE, |
502 |
378 |
NodeManager::currentNM()->mkConst(arg1.div(rm, arg2))); |
503 |
|
} |
504 |
|
|
505 |
27 |
RewriteResponse sqrt(TNode node, bool isPreRewrite) |
506 |
|
{ |
507 |
27 |
Assert(node.getKind() == kind::FLOATINGPOINT_SQRT); |
508 |
27 |
Assert(node.getNumChildren() == 2); |
509 |
|
|
510 |
27 |
RoundingMode rm(node[0].getConst<RoundingMode>()); |
511 |
54 |
FloatingPoint arg(node[1].getConst<FloatingPoint>()); |
512 |
|
|
513 |
|
return RewriteResponse(REWRITE_DONE, |
514 |
54 |
NodeManager::currentNM()->mkConst(arg.sqrt(rm))); |
515 |
|
} |
516 |
|
|
517 |
140 |
RewriteResponse rti(TNode node, bool isPreRewrite) |
518 |
|
{ |
519 |
140 |
Assert(node.getKind() == kind::FLOATINGPOINT_RTI); |
520 |
140 |
Assert(node.getNumChildren() == 2); |
521 |
|
|
522 |
140 |
RoundingMode rm(node[0].getConst<RoundingMode>()); |
523 |
280 |
FloatingPoint arg(node[1].getConst<FloatingPoint>()); |
524 |
|
|
525 |
|
return RewriteResponse(REWRITE_DONE, |
526 |
280 |
NodeManager::currentNM()->mkConst(arg.rti(rm))); |
527 |
|
} |
528 |
|
|
529 |
99 |
RewriteResponse rem(TNode node, bool isPreRewrite) |
530 |
|
{ |
531 |
99 |
Assert(node.getKind() == kind::FLOATINGPOINT_REM); |
532 |
99 |
Assert(node.getNumChildren() == 2); |
533 |
|
|
534 |
198 |
FloatingPoint arg1(node[0].getConst<FloatingPoint>()); |
535 |
198 |
FloatingPoint arg2(node[1].getConst<FloatingPoint>()); |
536 |
|
|
537 |
99 |
Assert(arg1.getSize() == arg2.getSize()); |
538 |
|
|
539 |
|
return RewriteResponse(REWRITE_DONE, |
540 |
198 |
NodeManager::currentNM()->mkConst(arg1.rem(arg2))); |
541 |
|
} |
542 |
|
|
543 |
|
RewriteResponse min(TNode node, bool isPreRewrite) |
544 |
|
{ |
545 |
|
Assert(node.getKind() == kind::FLOATINGPOINT_MIN); |
546 |
|
Assert(node.getNumChildren() == 2); |
547 |
|
|
548 |
|
FloatingPoint arg1(node[0].getConst<FloatingPoint>()); |
549 |
|
FloatingPoint arg2(node[1].getConst<FloatingPoint>()); |
550 |
|
|
551 |
|
Assert(arg1.getSize() == arg2.getSize()); |
552 |
|
|
553 |
|
FloatingPoint::PartialFloatingPoint res(arg1.min(arg2)); |
554 |
|
|
555 |
|
if (res.second) |
556 |
|
{ |
557 |
|
Node lit = NodeManager::currentNM()->mkConst(res.first); |
558 |
|
return RewriteResponse(REWRITE_DONE, lit); |
559 |
|
} |
560 |
|
else |
561 |
|
{ |
562 |
|
// Can't constant fold the underspecified case |
563 |
|
return RewriteResponse(REWRITE_DONE, node); |
564 |
|
} |
565 |
|
} |
566 |
|
|
567 |
4 |
RewriteResponse max(TNode node, bool isPreRewrite) |
568 |
|
{ |
569 |
4 |
Assert(node.getKind() == kind::FLOATINGPOINT_MAX); |
570 |
4 |
Assert(node.getNumChildren() == 2); |
571 |
|
|
572 |
8 |
FloatingPoint arg1(node[0].getConst<FloatingPoint>()); |
573 |
8 |
FloatingPoint arg2(node[1].getConst<FloatingPoint>()); |
574 |
|
|
575 |
4 |
Assert(arg1.getSize() == arg2.getSize()); |
576 |
|
|
577 |
8 |
FloatingPoint::PartialFloatingPoint res(arg1.max(arg2)); |
578 |
|
|
579 |
4 |
if (res.second) |
580 |
|
{ |
581 |
8 |
Node lit = NodeManager::currentNM()->mkConst(res.first); |
582 |
4 |
return RewriteResponse(REWRITE_DONE, lit); |
583 |
|
} |
584 |
|
else |
585 |
|
{ |
586 |
|
// Can't constant fold the underspecified case |
587 |
|
return RewriteResponse(REWRITE_DONE, node); |
588 |
|
} |
589 |
|
} |
590 |
|
|
591 |
|
RewriteResponse minTotal(TNode node, bool isPreRewrite) |
592 |
|
{ |
593 |
|
Assert(node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL); |
594 |
|
Assert(node.getNumChildren() == 3); |
595 |
|
|
596 |
|
FloatingPoint arg1(node[0].getConst<FloatingPoint>()); |
597 |
|
FloatingPoint arg2(node[1].getConst<FloatingPoint>()); |
598 |
|
|
599 |
|
Assert(arg1.getSize() == arg2.getSize()); |
600 |
|
|
601 |
|
// Can be called with the third argument non-constant |
602 |
|
if (node[2].getMetaKind() == kind::metakind::CONSTANT) |
603 |
|
{ |
604 |
|
BitVector arg3(node[2].getConst<BitVector>()); |
605 |
|
|
606 |
|
FloatingPoint folded(arg1.minTotal(arg2, arg3.isBitSet(0))); |
607 |
|
Node lit = NodeManager::currentNM()->mkConst(folded); |
608 |
|
return RewriteResponse(REWRITE_DONE, lit); |
609 |
|
} |
610 |
|
else |
611 |
|
{ |
612 |
|
FloatingPoint::PartialFloatingPoint res(arg1.min(arg2)); |
613 |
|
|
614 |
|
if (res.second) |
615 |
|
{ |
616 |
|
Node lit = NodeManager::currentNM()->mkConst(res.first); |
617 |
|
return RewriteResponse(REWRITE_DONE, lit); |
618 |
|
} |
619 |
|
else |
620 |
|
{ |
621 |
|
// Can't constant fold the underspecified case |
622 |
|
return RewriteResponse(REWRITE_DONE, node); |
623 |
|
} |
624 |
|
} |
625 |
|
} |
626 |
|
|
627 |
104 |
RewriteResponse maxTotal(TNode node, bool isPreRewrite) |
628 |
|
{ |
629 |
104 |
Assert(node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL); |
630 |
104 |
Assert(node.getNumChildren() == 3); |
631 |
|
|
632 |
208 |
FloatingPoint arg1(node[0].getConst<FloatingPoint>()); |
633 |
208 |
FloatingPoint arg2(node[1].getConst<FloatingPoint>()); |
634 |
|
|
635 |
104 |
Assert(arg1.getSize() == arg2.getSize()); |
636 |
|
|
637 |
|
// Can be called with the third argument non-constant |
638 |
104 |
if (node[2].getMetaKind() == kind::metakind::CONSTANT) |
639 |
|
{ |
640 |
|
BitVector arg3(node[2].getConst<BitVector>()); |
641 |
|
|
642 |
|
FloatingPoint folded(arg1.maxTotal(arg2, arg3.isBitSet(0))); |
643 |
|
Node lit = NodeManager::currentNM()->mkConst(folded); |
644 |
|
return RewriteResponse(REWRITE_DONE, lit); |
645 |
|
} |
646 |
|
else |
647 |
|
{ |
648 |
208 |
FloatingPoint::PartialFloatingPoint res(arg1.max(arg2)); |
649 |
|
|
650 |
104 |
if (res.second) |
651 |
|
{ |
652 |
208 |
Node lit = NodeManager::currentNM()->mkConst(res.first); |
653 |
104 |
return RewriteResponse(REWRITE_DONE, lit); |
654 |
|
} |
655 |
|
else |
656 |
|
{ |
657 |
|
// Can't constant fold the underspecified case |
658 |
|
return RewriteResponse(REWRITE_DONE, node); |
659 |
|
} |
660 |
|
} |
661 |
|
} |
662 |
|
|
663 |
28 |
RewriteResponse equal (TNode node, bool isPreRewrite) { |
664 |
28 |
Assert(node.getKind() == kind::EQUAL); |
665 |
|
|
666 |
|
// We should only get equalities of floating point or rounding mode types. |
667 |
56 |
TypeNode tn = node[0].getType(true); |
668 |
|
|
669 |
28 |
if (tn.isFloatingPoint()) { |
670 |
36 |
FloatingPoint arg1(node[0].getConst<FloatingPoint>()); |
671 |
36 |
FloatingPoint arg2(node[1].getConst<FloatingPoint>()); |
672 |
|
|
673 |
18 |
Assert(arg1.getSize() == arg2.getSize()); |
674 |
|
|
675 |
18 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 == arg2)); |
676 |
|
|
677 |
10 |
} else if (tn.isRoundingMode()) { |
678 |
10 |
RoundingMode arg1(node[0].getConst<RoundingMode>()); |
679 |
10 |
RoundingMode arg2(node[1].getConst<RoundingMode>()); |
680 |
|
|
681 |
10 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 == arg2)); |
682 |
|
|
683 |
|
} |
684 |
|
Unreachable() << "Equality of unknown type"; |
685 |
|
} |
686 |
|
|
687 |
26 |
RewriteResponse leq(TNode node, bool isPreRewrite) |
688 |
|
{ |
689 |
26 |
Assert(node.getKind() == kind::FLOATINGPOINT_LEQ); |
690 |
26 |
Assert(node.getNumChildren() == 2); |
691 |
|
|
692 |
52 |
FloatingPoint arg1(node[0].getConst<FloatingPoint>()); |
693 |
52 |
FloatingPoint arg2(node[1].getConst<FloatingPoint>()); |
694 |
|
|
695 |
26 |
Assert(arg1.getSize() == arg2.getSize()); |
696 |
|
|
697 |
52 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 <= arg2)); |
698 |
|
} |
699 |
|
|
700 |
2 |
RewriteResponse lt(TNode node, bool isPreRewrite) |
701 |
|
{ |
702 |
2 |
Assert(node.getKind() == kind::FLOATINGPOINT_LT); |
703 |
2 |
Assert(node.getNumChildren() == 2); |
704 |
|
|
705 |
4 |
FloatingPoint arg1(node[0].getConst<FloatingPoint>()); |
706 |
4 |
FloatingPoint arg2(node[1].getConst<FloatingPoint>()); |
707 |
|
|
708 |
2 |
Assert(arg1.getSize() == arg2.getSize()); |
709 |
|
|
710 |
4 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(arg1 < arg2)); |
711 |
|
} |
712 |
|
|
713 |
7 |
RewriteResponse isNormal(TNode node, bool isPreRewrite) |
714 |
|
{ |
715 |
7 |
Assert(node.getKind() == kind::FLOATINGPOINT_ISN); |
716 |
7 |
Assert(node.getNumChildren() == 1); |
717 |
|
|
718 |
7 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isNormal())); |
719 |
|
} |
720 |
|
|
721 |
9 |
RewriteResponse isSubnormal(TNode node, bool isPreRewrite) |
722 |
|
{ |
723 |
9 |
Assert(node.getKind() == kind::FLOATINGPOINT_ISSN); |
724 |
9 |
Assert(node.getNumChildren() == 1); |
725 |
|
|
726 |
9 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isSubnormal())); |
727 |
|
} |
728 |
|
|
729 |
138 |
RewriteResponse isZero(TNode node, bool isPreRewrite) |
730 |
|
{ |
731 |
138 |
Assert(node.getKind() == kind::FLOATINGPOINT_ISZ); |
732 |
138 |
Assert(node.getNumChildren() == 1); |
733 |
|
|
734 |
138 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isZero())); |
735 |
|
} |
736 |
|
|
737 |
5 |
RewriteResponse isInfinite(TNode node, bool isPreRewrite) |
738 |
|
{ |
739 |
5 |
Assert(node.getKind() == kind::FLOATINGPOINT_ISINF); |
740 |
5 |
Assert(node.getNumChildren() == 1); |
741 |
|
|
742 |
5 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isInfinite())); |
743 |
|
} |
744 |
|
|
745 |
22 |
RewriteResponse isNaN(TNode node, bool isPreRewrite) |
746 |
|
{ |
747 |
22 |
Assert(node.getKind() == kind::FLOATINGPOINT_ISNAN); |
748 |
22 |
Assert(node.getNumChildren() == 1); |
749 |
|
|
750 |
22 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isNaN())); |
751 |
|
} |
752 |
|
|
753 |
10 |
RewriteResponse isNegative(TNode node, bool isPreRewrite) |
754 |
|
{ |
755 |
10 |
Assert(node.getKind() == kind::FLOATINGPOINT_ISNEG); |
756 |
10 |
Assert(node.getNumChildren() == 1); |
757 |
|
|
758 |
10 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isNegative())); |
759 |
|
} |
760 |
|
|
761 |
7 |
RewriteResponse isPositive(TNode node, bool isPreRewrite) |
762 |
|
{ |
763 |
7 |
Assert(node.getKind() == kind::FLOATINGPOINT_ISPOS); |
764 |
7 |
Assert(node.getNumChildren() == 1); |
765 |
|
|
766 |
7 |
return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(node[0].getConst<FloatingPoint>().isPositive())); |
767 |
|
} |
768 |
|
|
769 |
203 |
RewriteResponse convertFromIEEEBitVectorLiteral(TNode node, bool isPreRewrite) |
770 |
|
{ |
771 |
203 |
Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR); |
772 |
|
|
773 |
406 |
TNode op = node.getOperator(); |
774 |
203 |
const FloatingPointToFPIEEEBitVector ¶m = op.getConst<FloatingPointToFPIEEEBitVector>(); |
775 |
203 |
const BitVector &bv = node[0].getConst<BitVector>(); |
776 |
|
|
777 |
|
Node lit = NodeManager::currentNM()->mkConst( |
778 |
406 |
FloatingPoint(param.getSize().exponentWidth(), |
779 |
406 |
param.getSize().significandWidth(), |
780 |
609 |
bv)); |
781 |
|
|
782 |
406 |
return RewriteResponse(REWRITE_DONE, lit); |
783 |
|
} |
784 |
|
|
785 |
19 |
RewriteResponse constantConvert(TNode node, bool isPreRewrite) |
786 |
|
{ |
787 |
19 |
Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT); |
788 |
19 |
Assert(node.getNumChildren() == 2); |
789 |
|
|
790 |
19 |
RoundingMode rm(node[0].getConst<RoundingMode>()); |
791 |
38 |
FloatingPoint arg1(node[1].getConst<FloatingPoint>()); |
792 |
19 |
FloatingPointToFPFloatingPoint info = node.getOperator().getConst<FloatingPointToFPFloatingPoint>(); |
793 |
|
|
794 |
|
return RewriteResponse( |
795 |
|
REWRITE_DONE, |
796 |
38 |
NodeManager::currentNM()->mkConst(arg1.convert(info.getSize(), rm))); |
797 |
|
} |
798 |
|
|
799 |
46 |
RewriteResponse convertFromRealLiteral(TNode node, bool isPreRewrite) |
800 |
|
{ |
801 |
46 |
Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_REAL); |
802 |
|
|
803 |
92 |
TNode op = node.getOperator(); |
804 |
|
const FloatingPointSize& size = |
805 |
46 |
op.getConst<FloatingPointToFPReal>().getSize(); |
806 |
|
|
807 |
46 |
RoundingMode rm(node[0].getConst<RoundingMode>()); |
808 |
92 |
Rational arg(node[1].getConst<Rational>()); |
809 |
|
|
810 |
92 |
FloatingPoint res(size, rm, arg); |
811 |
|
|
812 |
92 |
Node lit = NodeManager::currentNM()->mkConst(res); |
813 |
|
|
814 |
92 |
return RewriteResponse(REWRITE_DONE, lit); |
815 |
|
} |
816 |
|
|
817 |
8 |
RewriteResponse convertFromSBV(TNode node, bool isPreRewrite) |
818 |
|
{ |
819 |
8 |
Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR); |
820 |
|
|
821 |
16 |
TNode op = node.getOperator(); |
822 |
|
const FloatingPointSize& size = |
823 |
8 |
op.getConst<FloatingPointToFPSignedBitVector>().getSize(); |
824 |
|
|
825 |
8 |
RoundingMode rm(node[0].getConst<RoundingMode>()); |
826 |
16 |
BitVector sbv(node[1].getConst<BitVector>()); |
827 |
|
|
828 |
8 |
NodeManager* nm = NodeManager::currentNM(); |
829 |
|
|
830 |
|
/* symFPU does not allow conversions from signed bit-vector of size 1 */ |
831 |
8 |
if (sbv.getSize() == 1) |
832 |
|
{ |
833 |
|
FloatingPoint fromubv(size, rm, sbv, false); |
834 |
|
if (sbv.isBitSet(0)) |
835 |
|
{ |
836 |
|
return RewriteResponse(REWRITE_DONE, nm->mkConst(fromubv.negate())); |
837 |
|
} |
838 |
|
return RewriteResponse(REWRITE_DONE, nm->mkConst(fromubv)); |
839 |
|
} |
840 |
|
|
841 |
|
return RewriteResponse(REWRITE_DONE, |
842 |
8 |
nm->mkConst(FloatingPoint(size, rm, sbv, true))); |
843 |
|
} |
844 |
|
|
845 |
60 |
RewriteResponse convertFromUBV(TNode node, bool isPreRewrite) |
846 |
|
{ |
847 |
60 |
Assert(node.getKind() == kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR); |
848 |
|
|
849 |
120 |
TNode op = node.getOperator(); |
850 |
|
const FloatingPointSize& size = |
851 |
60 |
op.getConst<FloatingPointToFPUnsignedBitVector>().getSize(); |
852 |
|
|
853 |
60 |
RoundingMode rm(node[0].getConst<RoundingMode>()); |
854 |
120 |
BitVector arg(node[1].getConst<BitVector>()); |
855 |
|
|
856 |
120 |
FloatingPoint res(size, rm, arg, false); |
857 |
|
|
858 |
120 |
Node lit = NodeManager::currentNM()->mkConst(res); |
859 |
|
|
860 |
120 |
return RewriteResponse(REWRITE_DONE, lit); |
861 |
|
} |
862 |
|
|
863 |
|
RewriteResponse convertToUBV(TNode node, bool isPreRewrite) |
864 |
|
{ |
865 |
|
Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV); |
866 |
|
|
867 |
|
TNode op = node.getOperator(); |
868 |
|
const BitVectorSize& size = op.getConst<FloatingPointToUBV>().d_bv_size; |
869 |
|
|
870 |
|
RoundingMode rm(node[0].getConst<RoundingMode>()); |
871 |
|
FloatingPoint arg(node[1].getConst<FloatingPoint>()); |
872 |
|
|
873 |
|
FloatingPoint::PartialBitVector res(arg.convertToBV(size, rm, false)); |
874 |
|
|
875 |
|
if (res.second) { |
876 |
|
Node lit = NodeManager::currentNM()->mkConst(res.first); |
877 |
|
return RewriteResponse(REWRITE_DONE, lit); |
878 |
|
} else { |
879 |
|
// Can't constant fold the underspecified case |
880 |
|
return RewriteResponse(REWRITE_DONE, node); |
881 |
|
} |
882 |
|
} |
883 |
|
|
884 |
|
RewriteResponse convertToSBV(TNode node, bool isPreRewrite) |
885 |
|
{ |
886 |
|
Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV); |
887 |
|
|
888 |
|
TNode op = node.getOperator(); |
889 |
|
const BitVectorSize& size = op.getConst<FloatingPointToSBV>().d_bv_size; |
890 |
|
|
891 |
|
RoundingMode rm(node[0].getConst<RoundingMode>()); |
892 |
|
FloatingPoint arg(node[1].getConst<FloatingPoint>()); |
893 |
|
|
894 |
|
FloatingPoint::PartialBitVector res(arg.convertToBV(size, rm, true)); |
895 |
|
|
896 |
|
if (res.second) { |
897 |
|
Node lit = NodeManager::currentNM()->mkConst(res.first); |
898 |
|
return RewriteResponse(REWRITE_DONE, lit); |
899 |
|
} else { |
900 |
|
// Can't constant fold the underspecified case |
901 |
|
return RewriteResponse(REWRITE_DONE, node); |
902 |
|
} |
903 |
|
} |
904 |
|
|
905 |
2 |
RewriteResponse convertToReal(TNode node, bool isPreRewrite) |
906 |
|
{ |
907 |
2 |
Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL); |
908 |
|
|
909 |
4 |
FloatingPoint arg(node[0].getConst<FloatingPoint>()); |
910 |
|
|
911 |
4 |
FloatingPoint::PartialRational res(arg.convertToRational()); |
912 |
|
|
913 |
2 |
if (res.second) { |
914 |
4 |
Node lit = NodeManager::currentNM()->mkConst(res.first); |
915 |
2 |
return RewriteResponse(REWRITE_DONE, lit); |
916 |
|
} else { |
917 |
|
// Can't constant fold the underspecified case |
918 |
|
return RewriteResponse(REWRITE_DONE, node); |
919 |
|
} |
920 |
|
} |
921 |
|
|
922 |
|
RewriteResponse convertToUBVTotal(TNode node, bool isPreRewrite) |
923 |
|
{ |
924 |
|
Assert(node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL); |
925 |
|
|
926 |
|
TNode op = node.getOperator(); |
927 |
|
const BitVectorSize& size = |
928 |
|
op.getConst<FloatingPointToUBVTotal>().d_bv_size; |
929 |
|
|
930 |
|
RoundingMode rm(node[0].getConst<RoundingMode>()); |
931 |
|
FloatingPoint arg(node[1].getConst<FloatingPoint>()); |
932 |
|
|
933 |
|
// Can be called with the third argument non-constant |
934 |
|
if (node[2].getMetaKind() == kind::metakind::CONSTANT) { |
935 |
|
BitVector partialValue(node[2].getConst<BitVector>()); |
936 |
|
|
937 |
|
BitVector folded(arg.convertToBVTotal(size, rm, false, partialValue)); |
938 |
|
Node lit = NodeManager::currentNM()->mkConst(folded); |
939 |
|
return RewriteResponse(REWRITE_DONE, lit); |
940 |
|
|
941 |
|
} else { |
942 |
|
FloatingPoint::PartialBitVector res(arg.convertToBV(size, rm, false)); |
943 |
|
|
944 |
|
if (res.second) { |
945 |
|
Node lit = NodeManager::currentNM()->mkConst(res.first); |
946 |
|
return RewriteResponse(REWRITE_DONE, lit); |
947 |
|
} else { |
948 |
|
// Can't constant fold the underspecified case |
949 |
|
return RewriteResponse(REWRITE_DONE, node); |
950 |
|
} |
951 |
|
} |
952 |
|
} |
953 |
|
|
954 |
|
RewriteResponse convertToSBVTotal(TNode node, bool isPreRewrite) |
955 |
|
{ |
956 |
|
Assert(node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL); |
957 |
|
|
958 |
|
TNode op = node.getOperator(); |
959 |
|
const BitVectorSize& size = |
960 |
|
op.getConst<FloatingPointToSBVTotal>().d_bv_size; |
961 |
|
|
962 |
|
RoundingMode rm(node[0].getConst<RoundingMode>()); |
963 |
|
FloatingPoint arg(node[1].getConst<FloatingPoint>()); |
964 |
|
|
965 |
|
// Can be called with the third argument non-constant |
966 |
|
if (node[2].getMetaKind() == kind::metakind::CONSTANT) { |
967 |
|
BitVector partialValue(node[2].getConst<BitVector>()); |
968 |
|
|
969 |
|
BitVector folded(arg.convertToBVTotal(size, rm, true, partialValue)); |
970 |
|
Node lit = NodeManager::currentNM()->mkConst(folded); |
971 |
|
return RewriteResponse(REWRITE_DONE, lit); |
972 |
|
|
973 |
|
} else { |
974 |
|
FloatingPoint::PartialBitVector res(arg.convertToBV(size, rm, true)); |
975 |
|
|
976 |
|
if (res.second) { |
977 |
|
Node lit = NodeManager::currentNM()->mkConst(res.first); |
978 |
|
return RewriteResponse(REWRITE_DONE, lit); |
979 |
|
} else { |
980 |
|
// Can't constant fold the underspecified case |
981 |
|
return RewriteResponse(REWRITE_DONE, node); |
982 |
|
} |
983 |
|
} |
984 |
|
} |
985 |
|
|
986 |
8 |
RewriteResponse convertToRealTotal(TNode node, bool isPreRewrite) |
987 |
|
{ |
988 |
8 |
Assert(node.getKind() == kind::FLOATINGPOINT_TO_REAL_TOTAL); |
989 |
|
|
990 |
16 |
FloatingPoint arg(node[0].getConst<FloatingPoint>()); |
991 |
|
|
992 |
|
// Can be called with the third argument non-constant |
993 |
8 |
if (node[1].getMetaKind() == kind::metakind::CONSTANT) { |
994 |
16 |
Rational partialValue(node[1].getConst<Rational>()); |
995 |
|
|
996 |
16 |
Rational folded(arg.convertToRationalTotal(partialValue)); |
997 |
16 |
Node lit = NodeManager::currentNM()->mkConst(folded); |
998 |
8 |
return RewriteResponse(REWRITE_DONE, lit); |
999 |
|
|
1000 |
|
} else { |
1001 |
|
FloatingPoint::PartialRational res(arg.convertToRational()); |
1002 |
|
|
1003 |
|
if (res.second) { |
1004 |
|
Node lit = NodeManager::currentNM()->mkConst(res.first); |
1005 |
|
return RewriteResponse(REWRITE_DONE, lit); |
1006 |
|
} else { |
1007 |
|
// Can't constant fold the underspecified case |
1008 |
|
return RewriteResponse(REWRITE_DONE, node); |
1009 |
|
} |
1010 |
|
} |
1011 |
|
} |
1012 |
|
|
1013 |
20 |
RewriteResponse componentFlag(TNode node, bool isPreRewrite) |
1014 |
|
{ |
1015 |
20 |
Kind k = node.getKind(); |
1016 |
|
|
1017 |
20 |
Assert((k == kind::FLOATINGPOINT_COMPONENT_NAN) |
1018 |
|
|| (k == kind::FLOATINGPOINT_COMPONENT_INF) |
1019 |
|
|| (k == kind::FLOATINGPOINT_COMPONENT_ZERO) |
1020 |
|
|| (k == kind::FLOATINGPOINT_COMPONENT_SIGN)); |
1021 |
|
|
1022 |
40 |
FloatingPoint arg0(node[0].getConst<FloatingPoint>()); |
1023 |
|
|
1024 |
|
bool result; |
1025 |
20 |
switch (k) |
1026 |
|
{ |
1027 |
|
#ifdef CVC5_USE_SYMFPU |
1028 |
5 |
case kind::FLOATINGPOINT_COMPONENT_NAN: result = arg0.isNaN(); break; |
1029 |
5 |
case kind::FLOATINGPOINT_COMPONENT_INF: result = arg0.isInfinite(); break; |
1030 |
5 |
case kind::FLOATINGPOINT_COMPONENT_ZERO: result = arg0.isZero(); break; |
1031 |
5 |
case kind::FLOATINGPOINT_COMPONENT_SIGN: result = arg0.getSign(); break; |
1032 |
|
#endif |
1033 |
|
default: Unreachable() << "Unknown kind used in componentFlag"; break; |
1034 |
|
} |
1035 |
|
|
1036 |
40 |
BitVector res(1U, (result) ? 1U : 0U); |
1037 |
|
|
1038 |
|
return RewriteResponse(REWRITE_DONE, |
1039 |
40 |
NodeManager::currentNM()->mkConst(res)); |
1040 |
|
} |
1041 |
|
|
1042 |
5 |
RewriteResponse componentExponent(TNode node, bool isPreRewrite) |
1043 |
|
{ |
1044 |
5 |
Assert(node.getKind() == kind::FLOATINGPOINT_COMPONENT_EXPONENT); |
1045 |
|
|
1046 |
10 |
FloatingPoint arg0(node[0].getConst<FloatingPoint>()); |
1047 |
|
|
1048 |
|
// \todo Add a proper interface for this sort of thing to FloatingPoint #1915 |
1049 |
|
return RewriteResponse( |
1050 |
|
REWRITE_DONE, |
1051 |
|
#ifdef CVC5_USE_SYMFPU |
1052 |
10 |
NodeManager::currentNM()->mkConst((BitVector)arg0.getExponent()) |
1053 |
|
#else |
1054 |
|
node |
1055 |
|
#endif |
1056 |
10 |
); |
1057 |
|
} |
1058 |
|
|
1059 |
5 |
RewriteResponse componentSignificand(TNode node, bool isPreRewrite) |
1060 |
|
{ |
1061 |
5 |
Assert(node.getKind() == kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND); |
1062 |
|
|
1063 |
10 |
FloatingPoint arg0(node[0].getConst<FloatingPoint>()); |
1064 |
|
|
1065 |
|
return RewriteResponse( |
1066 |
|
REWRITE_DONE, |
1067 |
|
#ifdef CVC5_USE_SYMFPU |
1068 |
10 |
NodeManager::currentNM()->mkConst((BitVector)arg0.getSignificand()) |
1069 |
|
#else |
1070 |
|
node |
1071 |
|
#endif |
1072 |
10 |
); |
1073 |
|
} |
1074 |
|
|
1075 |
1 |
RewriteResponse roundingModeBitBlast(TNode node, bool isPreRewrite) |
1076 |
|
{ |
1077 |
1 |
Assert(node.getKind() == kind::ROUNDINGMODE_BITBLAST); |
1078 |
|
|
1079 |
2 |
BitVector value; |
1080 |
|
|
1081 |
|
#ifdef CVC5_USE_SYMFPU |
1082 |
|
/* \todo fix the numbering of rounding modes so this doesn't need |
1083 |
|
* to call symfpu at all and remove the dependency on fp_converter.h #1915 */ |
1084 |
1 |
RoundingMode arg0(node[0].getConst<RoundingMode>()); |
1085 |
1 |
switch (arg0) |
1086 |
|
{ |
1087 |
|
case ROUND_NEAREST_TIES_TO_EVEN: |
1088 |
|
value = symfpuSymbolic::traits::RNE().getConst<BitVector>(); |
1089 |
|
break; |
1090 |
|
|
1091 |
|
case ROUND_NEAREST_TIES_TO_AWAY: |
1092 |
|
value = symfpuSymbolic::traits::RNA().getConst<BitVector>(); |
1093 |
|
break; |
1094 |
|
|
1095 |
|
case ROUND_TOWARD_POSITIVE: |
1096 |
|
value = symfpuSymbolic::traits::RTP().getConst<BitVector>(); |
1097 |
|
break; |
1098 |
|
|
1099 |
1 |
case ROUND_TOWARD_NEGATIVE: |
1100 |
1 |
value = symfpuSymbolic::traits::RTN().getConst<BitVector>(); |
1101 |
1 |
break; |
1102 |
|
|
1103 |
|
case ROUND_TOWARD_ZERO: |
1104 |
|
value = symfpuSymbolic::traits::RTZ().getConst<BitVector>(); |
1105 |
|
break; |
1106 |
|
|
1107 |
|
default: |
1108 |
|
Unreachable() << "Unknown rounding mode in roundingModeBitBlast"; |
1109 |
|
break; |
1110 |
|
} |
1111 |
|
#else |
1112 |
|
value = BitVector(5U, 0U); |
1113 |
|
#endif |
1114 |
|
return RewriteResponse(REWRITE_DONE, |
1115 |
2 |
NodeManager::currentNM()->mkConst(value)); |
1116 |
|
} |
1117 |
|
|
1118 |
|
}; // namespace constantFold |
1119 |
|
|
1120 |
|
/** |
1121 |
|
* Initialize the rewriter. |
1122 |
|
*/ |
1123 |
9460 |
TheoryFpRewriter::TheoryFpRewriter(context::UserContext* u) : d_fpExpDef(u) |
1124 |
|
{ |
1125 |
|
/* Set up the pre-rewrite dispatch table */ |
1126 |
3074500 |
for (uint32_t i = 0; i < kind::LAST_KIND; ++i) |
1127 |
|
{ |
1128 |
3065040 |
d_preRewriteTable[i] = rewrite::notFP; |
1129 |
|
} |
1130 |
|
|
1131 |
|
/******** Constants ********/ |
1132 |
|
/* No rewriting possible for constants */ |
1133 |
9460 |
d_preRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity; |
1134 |
9460 |
d_preRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity; |
1135 |
|
|
1136 |
|
/******** Sorts(?) ********/ |
1137 |
|
/* These kinds should only appear in types */ |
1138 |
|
// d_preRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type; |
1139 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type; |
1140 |
|
|
1141 |
|
/******** Operations ********/ |
1142 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity; |
1143 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs; |
1144 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation; |
1145 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_PLUS] = rewrite::identity; |
1146 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_SUB] = |
1147 |
|
rewrite::convertSubtractionToAddition; |
1148 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_MULT] = rewrite::identity; |
1149 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity; |
1150 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::identity; |
1151 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity; |
1152 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::identity; |
1153 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity; |
1154 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax; |
1155 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax; |
1156 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax; |
1157 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax; |
1158 |
|
|
1159 |
|
/******** Comparisons ********/ |
1160 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_EQ] = |
1161 |
|
rewrite::then<rewrite::breakChain, rewrite::ieeeEqToEq>; |
1162 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_LEQ] = |
1163 |
|
rewrite::then<rewrite::breakChain, rewrite::leqId>; |
1164 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_LT] = |
1165 |
|
rewrite::then<rewrite::breakChain, rewrite::ltId>; |
1166 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_GEQ] = |
1167 |
|
rewrite::then<rewrite::breakChain, rewrite::geqToleq>; |
1168 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_GT] = |
1169 |
|
rewrite::then<rewrite::breakChain, rewrite::gtTolt>; |
1170 |
|
|
1171 |
|
/******** Classifications ********/ |
1172 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::identity; |
1173 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::identity; |
1174 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::identity; |
1175 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::identity; |
1176 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::identity; |
1177 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity; |
1178 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity; |
1179 |
|
|
1180 |
|
/******** Conversions ********/ |
1181 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = |
1182 |
|
rewrite::identity; |
1183 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = |
1184 |
|
rewrite::identity; |
1185 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity; |
1186 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = |
1187 |
|
rewrite::identity; |
1188 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = |
1189 |
|
rewrite::identity; |
1190 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = rewrite::identity; |
1191 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity; |
1192 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity; |
1193 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity; |
1194 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity; |
1195 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity; |
1196 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity; |
1197 |
|
|
1198 |
|
/******** Variables ********/ |
1199 |
9460 |
d_preRewriteTable[kind::VARIABLE] = rewrite::variable; |
1200 |
9460 |
d_preRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable; |
1201 |
9460 |
d_preRewriteTable[kind::SKOLEM] = rewrite::variable; |
1202 |
9460 |
d_preRewriteTable[kind::INST_CONSTANT] = rewrite::variable; |
1203 |
|
|
1204 |
9460 |
d_preRewriteTable[kind::EQUAL] = rewrite::equal; |
1205 |
|
|
1206 |
|
/******** Components for bit-blasting ********/ |
1207 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity; |
1208 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity; |
1209 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity; |
1210 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity; |
1211 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = rewrite::identity; |
1212 |
9460 |
d_preRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] = |
1213 |
|
rewrite::identity; |
1214 |
9460 |
d_preRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity; |
1215 |
|
|
1216 |
|
/* Set up the post-rewrite dispatch table */ |
1217 |
3074500 |
for (uint32_t i = 0; i < kind::LAST_KIND; ++i) |
1218 |
|
{ |
1219 |
3065040 |
d_postRewriteTable[i] = rewrite::notFP; |
1220 |
|
} |
1221 |
|
|
1222 |
|
/******** Constants ********/ |
1223 |
|
/* No rewriting possible for constants */ |
1224 |
9460 |
d_postRewriteTable[kind::CONST_FLOATINGPOINT] = rewrite::identity; |
1225 |
9460 |
d_postRewriteTable[kind::CONST_ROUNDINGMODE] = rewrite::identity; |
1226 |
|
|
1227 |
|
/******** Sorts(?) ********/ |
1228 |
|
/* These kinds should only appear in types */ |
1229 |
|
// d_postRewriteTable[kind::ROUNDINGMODE_TYPE] = rewrite::type; |
1230 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TYPE] = rewrite::type; |
1231 |
|
|
1232 |
|
/******** Operations ********/ |
1233 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_FP] = rewrite::identity; |
1234 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_ABS] = rewrite::compactAbs; |
1235 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_NEG] = rewrite::removeDoubleNegation; |
1236 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_PLUS] = |
1237 |
|
rewrite::reorderBinaryOperation; |
1238 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_SUB] = rewrite::identity; |
1239 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_MULT] = |
1240 |
|
rewrite::reorderBinaryOperation; |
1241 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_DIV] = rewrite::identity; |
1242 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_FMA] = rewrite::reorderFMA; |
1243 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_SQRT] = rewrite::identity; |
1244 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_REM] = rewrite::compactRemainder; |
1245 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_RTI] = rewrite::identity; |
1246 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_MIN] = rewrite::compactMinMax; |
1247 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_MAX] = rewrite::compactMinMax; |
1248 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_MIN_TOTAL] = rewrite::compactMinMax; |
1249 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_MAX_TOTAL] = rewrite::compactMinMax; |
1250 |
|
|
1251 |
|
/******** Comparisons ********/ |
1252 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_EQ] = rewrite::identity; |
1253 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_LEQ] = rewrite::leqId; |
1254 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_LT] = rewrite::ltId; |
1255 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_GEQ] = rewrite::identity; |
1256 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_GT] = rewrite::identity; |
1257 |
|
|
1258 |
|
/******** Classifications ********/ |
1259 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_ISN] = rewrite::removeSignOperations; |
1260 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_ISSN] = rewrite::removeSignOperations; |
1261 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_ISZ] = rewrite::removeSignOperations; |
1262 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_ISINF] = rewrite::removeSignOperations; |
1263 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_ISNAN] = rewrite::removeSignOperations; |
1264 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_ISNEG] = rewrite::identity; |
1265 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_ISPOS] = rewrite::identity; |
1266 |
|
|
1267 |
|
/******** Conversions ********/ |
1268 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = |
1269 |
|
rewrite::identity; |
1270 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = |
1271 |
|
rewrite::identity; |
1272 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_REAL] = rewrite::identity; |
1273 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = |
1274 |
|
rewrite::toFPSignedBV; |
1275 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = |
1276 |
|
rewrite::identity; |
1277 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_FP_GENERIC] = |
1278 |
|
rewrite::removeToFPGeneric; |
1279 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV] = rewrite::identity; |
1280 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV] = rewrite::identity; |
1281 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL] = rewrite::identity; |
1282 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = rewrite::identity; |
1283 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = rewrite::identity; |
1284 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = rewrite::identity; |
1285 |
|
|
1286 |
|
/******** Variables ********/ |
1287 |
9460 |
d_postRewriteTable[kind::VARIABLE] = rewrite::variable; |
1288 |
9460 |
d_postRewriteTable[kind::BOUND_VARIABLE] = rewrite::variable; |
1289 |
9460 |
d_postRewriteTable[kind::SKOLEM] = rewrite::variable; |
1290 |
9460 |
d_postRewriteTable[kind::INST_CONSTANT] = rewrite::variable; |
1291 |
|
|
1292 |
9460 |
d_postRewriteTable[kind::EQUAL] = rewrite::equal; |
1293 |
|
|
1294 |
|
/******** Components for bit-blasting ********/ |
1295 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_NAN] = rewrite::identity; |
1296 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_INF] = rewrite::identity; |
1297 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = rewrite::identity; |
1298 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = rewrite::identity; |
1299 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = |
1300 |
|
rewrite::identity; |
1301 |
9460 |
d_postRewriteTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] = |
1302 |
|
rewrite::identity; |
1303 |
9460 |
d_postRewriteTable[kind::ROUNDINGMODE_BITBLAST] = rewrite::identity; |
1304 |
|
|
1305 |
|
/* Set up the post-rewrite constant fold table */ |
1306 |
3074500 |
for (uint32_t i = 0; i < kind::LAST_KIND; ++i) |
1307 |
|
{ |
1308 |
|
// Note that this is identity, not notFP |
1309 |
|
// Constant folding is called after post-rewrite |
1310 |
|
// So may have to deal with cases of things being |
1311 |
|
// re-written to non-floating-point sorts (i.e. true). |
1312 |
3065040 |
d_constantFoldTable[i] = rewrite::identity; |
1313 |
|
} |
1314 |
|
|
1315 |
|
/******** Constants ********/ |
1316 |
|
/* Already folded! */ |
1317 |
9460 |
d_constantFoldTable[kind::CONST_FLOATINGPOINT] = rewrite::identity; |
1318 |
9460 |
d_constantFoldTable[kind::CONST_ROUNDINGMODE] = rewrite::identity; |
1319 |
|
|
1320 |
|
/******** Sorts(?) ********/ |
1321 |
|
/* These kinds should only appear in types */ |
1322 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TYPE] = rewrite::type; |
1323 |
|
|
1324 |
|
/******** Operations ********/ |
1325 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_FP] = constantFold::fpLiteral; |
1326 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_ABS] = constantFold::abs; |
1327 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_NEG] = constantFold::neg; |
1328 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_PLUS] = constantFold::plus; |
1329 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_MULT] = constantFold::mult; |
1330 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_DIV] = constantFold::div; |
1331 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_FMA] = constantFold::fma; |
1332 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_SQRT] = constantFold::sqrt; |
1333 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_REM] = constantFold::rem; |
1334 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_RTI] = constantFold::rti; |
1335 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_MIN] = constantFold::min; |
1336 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_MAX] = constantFold::max; |
1337 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_MIN_TOTAL] = constantFold::minTotal; |
1338 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_MAX_TOTAL] = constantFold::maxTotal; |
1339 |
|
|
1340 |
|
/******** Comparisons ********/ |
1341 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_LEQ] = constantFold::leq; |
1342 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_LT] = constantFold::lt; |
1343 |
|
|
1344 |
|
/******** Classifications ********/ |
1345 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_ISN] = constantFold::isNormal; |
1346 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_ISSN] = constantFold::isSubnormal; |
1347 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_ISZ] = constantFold::isZero; |
1348 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_ISINF] = constantFold::isInfinite; |
1349 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_ISNAN] = constantFold::isNaN; |
1350 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_ISNEG] = constantFold::isNegative; |
1351 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_ISPOS] = constantFold::isPositive; |
1352 |
|
|
1353 |
|
/******** Conversions ********/ |
1354 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR] = |
1355 |
|
constantFold::convertFromIEEEBitVectorLiteral; |
1356 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT] = |
1357 |
|
constantFold::constantConvert; |
1358 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_REAL] = |
1359 |
|
constantFold::convertFromRealLiteral; |
1360 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR] = |
1361 |
|
constantFold::convertFromSBV; |
1362 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR] = |
1363 |
|
constantFold::convertFromUBV; |
1364 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV] = constantFold::convertToUBV; |
1365 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV] = constantFold::convertToSBV; |
1366 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL] = |
1367 |
|
constantFold::convertToReal; |
1368 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_UBV_TOTAL] = |
1369 |
|
constantFold::convertToUBVTotal; |
1370 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_SBV_TOTAL] = |
1371 |
|
constantFold::convertToSBVTotal; |
1372 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_TO_REAL_TOTAL] = |
1373 |
|
constantFold::convertToRealTotal; |
1374 |
|
|
1375 |
|
/******** Variables ********/ |
1376 |
9460 |
d_constantFoldTable[kind::VARIABLE] = rewrite::variable; |
1377 |
9460 |
d_constantFoldTable[kind::BOUND_VARIABLE] = rewrite::variable; |
1378 |
|
|
1379 |
9460 |
d_constantFoldTable[kind::EQUAL] = constantFold::equal; |
1380 |
|
|
1381 |
|
/******** Components for bit-blasting ********/ |
1382 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_NAN] = |
1383 |
|
constantFold::componentFlag; |
1384 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_INF] = |
1385 |
|
constantFold::componentFlag; |
1386 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_ZERO] = |
1387 |
|
constantFold::componentFlag; |
1388 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGN] = |
1389 |
|
constantFold::componentFlag; |
1390 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_EXPONENT] = |
1391 |
|
constantFold::componentExponent; |
1392 |
9460 |
d_constantFoldTable[kind::FLOATINGPOINT_COMPONENT_SIGNIFICAND] = |
1393 |
|
constantFold::componentSignificand; |
1394 |
9460 |
d_constantFoldTable[kind::ROUNDINGMODE_BITBLAST] = |
1395 |
|
constantFold::roundingModeBitBlast; |
1396 |
9460 |
} |
1397 |
|
|
1398 |
|
/** |
1399 |
|
* Rewrite a node into the normal form for the theory of fp |
1400 |
|
* in pre-order (really topological order)---meaning that the |
1401 |
|
* children may not be in the normal form. This is an optimization |
1402 |
|
* for theories with cancelling terms (e.g., 0 * (big-nasty-expression) |
1403 |
|
* in arithmetic rewrites to 0 without the need to look at the big |
1404 |
|
* nasty expression). Since it's only an optimization, the |
1405 |
|
* implementation here can do nothing. |
1406 |
|
*/ |
1407 |
|
|
1408 |
5000 |
RewriteResponse TheoryFpRewriter::preRewrite(TNode node) { |
1409 |
5000 |
Trace("fp-rewrite") << "TheoryFpRewriter::preRewrite(): " << node << std::endl; |
1410 |
5000 |
RewriteResponse res = d_preRewriteTable[node.getKind()](node, true); |
1411 |
5000 |
if (res.d_node != node) |
1412 |
|
{ |
1413 |
132 |
Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): before " << node << std::endl; |
1414 |
264 |
Debug("fp-rewrite") << "TheoryFpRewriter::preRewrite(): after " |
1415 |
132 |
<< res.d_node << std::endl; |
1416 |
|
} |
1417 |
5000 |
return res; |
1418 |
|
} |
1419 |
|
|
1420 |
|
|
1421 |
|
/** |
1422 |
|
* Rewrite a node into the normal form for the theory of fp. |
1423 |
|
* Called in post-order (really reverse-topological order) when |
1424 |
|
* traversing the expression DAG during rewriting. This is the |
1425 |
|
* main function of the rewriter, and because of the ordering, |
1426 |
|
* it can assume its children are all rewritten already. |
1427 |
|
* |
1428 |
|
* This function can return one of three rewrite response codes |
1429 |
|
* along with the rewritten node: |
1430 |
|
* |
1431 |
|
* REWRITE_DONE indicates that no more rewriting is needed. |
1432 |
|
* REWRITE_AGAIN means that the top-level expression should be |
1433 |
|
* rewritten again, but that its children are in final form. |
1434 |
|
* REWRITE_AGAIN_FULL means that the entire returned expression |
1435 |
|
* should be rewritten again (top-down with preRewrite(), then |
1436 |
|
* bottom-up with postRewrite()). |
1437 |
|
* |
1438 |
|
* Even if this function returns REWRITE_DONE, if the returned |
1439 |
|
* expression belongs to a different theory, it will be fully |
1440 |
|
* rewritten by that theory's rewriter. |
1441 |
|
*/ |
1442 |
|
|
1443 |
8980 |
RewriteResponse TheoryFpRewriter::postRewrite(TNode node) { |
1444 |
8980 |
Trace("fp-rewrite") << "TheoryFpRewriter::postRewrite(): " << node << std::endl; |
1445 |
17960 |
RewriteResponse res = d_postRewriteTable[node.getKind()](node, false); |
1446 |
8980 |
if (res.d_node != node) |
1447 |
|
{ |
1448 |
565 |
Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): before " << node << std::endl; |
1449 |
1130 |
Debug("fp-rewrite") << "TheoryFpRewriter::postRewrite(): after " |
1450 |
565 |
<< res.d_node << std::endl; |
1451 |
|
} |
1452 |
|
|
1453 |
8980 |
if (res.d_status == REWRITE_DONE) |
1454 |
|
{ |
1455 |
8882 |
bool allChildrenConst = true; |
1456 |
8882 |
bool apartFromRoundingMode = false; |
1457 |
8882 |
bool apartFromPartiallyDefinedArgument = false; |
1458 |
14924 |
for (Node::const_iterator i = res.d_node.begin(); i != res.d_node.end(); |
1459 |
|
++i) |
1460 |
|
{ |
1461 |
10202 |
if ((*i).getMetaKind() != kind::metakind::CONSTANT) { |
1462 |
4787 |
if ((*i).getType().isRoundingMode() && !apartFromRoundingMode) { |
1463 |
523 |
apartFromRoundingMode = true; |
1464 |
|
} |
1465 |
8528 |
else if ((res.d_node.getKind() == kind::FLOATINGPOINT_MIN_TOTAL |
1466 |
4264 |
|| res.d_node.getKind() == kind::FLOATINGPOINT_MAX_TOTAL |
1467 |
4090 |
|| res.d_node.getKind() == kind::FLOATINGPOINT_TO_UBV_TOTAL |
1468 |
4090 |
|| res.d_node.getKind() == kind::FLOATINGPOINT_TO_SBV_TOTAL |
1469 |
4090 |
|| res.d_node.getKind() |
1470 |
|
== kind::FLOATINGPOINT_TO_REAL_TOTAL) |
1471 |
4446 |
&& ((*i).getType().isBitVector() || (*i).getType().isReal()) |
1472 |
8632 |
&& !apartFromPartiallyDefinedArgument) |
1473 |
|
{ |
1474 |
104 |
apartFromPartiallyDefinedArgument = true; |
1475 |
|
} |
1476 |
|
else |
1477 |
|
{ |
1478 |
4160 |
allChildrenConst = false; |
1479 |
4160 |
break; |
1480 |
|
} |
1481 |
|
} |
1482 |
|
} |
1483 |
|
|
1484 |
8882 |
if (allChildrenConst) |
1485 |
|
{ |
1486 |
4722 |
RewriteStatus rs = REWRITE_DONE; // This is a bit messy because |
1487 |
9444 |
Node rn = res.d_node; // RewriteResponse is too functional.. |
1488 |
|
|
1489 |
4722 |
if (apartFromRoundingMode) |
1490 |
|
{ |
1491 |
478 |
if (!(res.d_node.getKind() == kind::EQUAL) |
1492 |
376 |
&& // Avoid infinite recursion... |
1493 |
137 |
!(res.d_node.getKind() == kind::ROUNDINGMODE_BITBLAST)) |
1494 |
|
{ |
1495 |
|
// Don't eliminate the bit-blast |
1496 |
|
// We are close to being able to constant fold this |
1497 |
|
// and in many cases the rounding mode really doesn't matter. |
1498 |
|
// So we can try brute forcing our way through them. |
1499 |
|
|
1500 |
125 |
NodeManager* nm = NodeManager::currentNM(); |
1501 |
|
|
1502 |
250 |
Node rne(nm->mkConst(ROUND_NEAREST_TIES_TO_EVEN)); |
1503 |
250 |
Node rna(nm->mkConst(ROUND_NEAREST_TIES_TO_AWAY)); |
1504 |
250 |
Node rtz(nm->mkConst(ROUND_TOWARD_POSITIVE)); |
1505 |
250 |
Node rtn(nm->mkConst(ROUND_TOWARD_NEGATIVE)); |
1506 |
250 |
Node rtp(nm->mkConst(ROUND_TOWARD_ZERO)); |
1507 |
|
|
1508 |
250 |
TNode rm(res.d_node[0]); |
1509 |
|
|
1510 |
250 |
Node w_rne(res.d_node.substitute(rm, TNode(rne))); |
1511 |
250 |
Node w_rna(res.d_node.substitute(rm, TNode(rna))); |
1512 |
250 |
Node w_rtz(res.d_node.substitute(rm, TNode(rtz))); |
1513 |
250 |
Node w_rtn(res.d_node.substitute(rm, TNode(rtn))); |
1514 |
250 |
Node w_rtp(res.d_node.substitute(rm, TNode(rtp))); |
1515 |
|
|
1516 |
125 |
rs = REWRITE_AGAIN_FULL; |
1517 |
375 |
rn = nm->mkNode( |
1518 |
|
kind::ITE, |
1519 |
250 |
nm->mkNode(kind::EQUAL, rm, rne), |
1520 |
|
w_rne, |
1521 |
500 |
nm->mkNode( |
1522 |
|
kind::ITE, |
1523 |
250 |
nm->mkNode(kind::EQUAL, rm, rna), |
1524 |
|
w_rna, |
1525 |
500 |
nm->mkNode(kind::ITE, |
1526 |
250 |
nm->mkNode(kind::EQUAL, rm, rtz), |
1527 |
|
w_rtz, |
1528 |
500 |
nm->mkNode(kind::ITE, |
1529 |
250 |
nm->mkNode(kind::EQUAL, rm, rtn), |
1530 |
|
w_rtn, |
1531 |
|
w_rtp)))); |
1532 |
|
} |
1533 |
|
} |
1534 |
|
else |
1535 |
|
{ |
1536 |
|
RewriteResponse tmp = |
1537 |
8966 |
d_constantFoldTable[res.d_node.getKind()](res.d_node, false); |
1538 |
4483 |
rs = tmp.d_status; |
1539 |
4483 |
rn = tmp.d_node; |
1540 |
|
} |
1541 |
|
|
1542 |
9444 |
RewriteResponse constRes(rs, rn); |
1543 |
|
|
1544 |
4722 |
if (constRes.d_node != res.d_node) |
1545 |
|
{ |
1546 |
4128 |
Debug("fp-rewrite") |
1547 |
2064 |
<< "TheoryFpRewriter::postRewrite(): before constant fold " |
1548 |
2064 |
<< res.d_node << std::endl; |
1549 |
4128 |
Debug("fp-rewrite") |
1550 |
2064 |
<< "TheoryFpRewriter::postRewrite(): after constant fold " |
1551 |
2064 |
<< constRes.d_node << std::endl; |
1552 |
|
} |
1553 |
|
|
1554 |
4722 |
return constRes; |
1555 |
|
} |
1556 |
|
} |
1557 |
|
|
1558 |
4258 |
return res; |
1559 |
|
} |
1560 |
2593 |
TrustNode TheoryFpRewriter::expandDefinition(Node node) |
1561 |
|
{ |
1562 |
2593 |
return d_fpExpDef.expandDefinition(node); |
1563 |
|
} |
1564 |
|
|
1565 |
|
} // namespace fp |
1566 |
|
} // namespace theory |
1567 |
28194 |
} // namespace cvc5 |