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