GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/fp/theory_fp_rewriter.cpp Lines: 527 721 73.1 %
Date: 2021-03-22 Branches: 867 3655 23.7 %

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