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