GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/fp/theory_fp_type_rules.h Lines: 165 281 58.7 %
Date: 2021-03-23 Branches: 346 1452 23.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_fp_type_rules.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Martin Brain, Tim King, Aina Niemetz
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level source
10
 ** directory for licensing information.\endverbatim
11
 **
12
 ** \brief [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "cvc4_private.h"
19
20
// This is only needed for checking that components are only applied to leaves.
21
#include "theory/theory.h"
22
#include "util/roundingmode.h"
23
24
#ifndef CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
25
#define CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H
26
27
namespace CVC4 {
28
namespace theory {
29
namespace fp {
30
31
#define TRACE(FUNCTION)                                                \
32
  Trace("fp-type") << FUNCTION "::computeType(" << check << "): " << n \
33
                   << std::endl
34
35
class FloatingPointConstantTypeRule {
36
 public:
37
480
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
38
                                     bool check) {
39
480
    TRACE("FloatingPointConstantTypeRule");
40
41
480
    const FloatingPoint& f = n.getConst<FloatingPoint>();
42
43
480
    if (check)
44
    {
45
311
      if (!(validExponentSize(f.d_fp_size.exponentWidth())))
46
      {
47
        throw TypeCheckingExceptionPrivate(
48
            n, "constant with invalid exponent size");
49
      }
50
311
      if (!(validSignificandSize(f.d_fp_size.significandWidth())))
51
      {
52
        throw TypeCheckingExceptionPrivate(
53
            n, "constant with invalid significand size");
54
      }
55
    }
56
480
    return nodeManager->mkFloatingPointType(f.d_fp_size);
57
  }
58
};
59
60
class RoundingModeConstantTypeRule {
61
 public:
62
6634
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
63
                                     bool check) {
64
6634
    TRACE("RoundingModeConstantTypeRule");
65
66
    // Nothing to check!
67
6634
    return nodeManager->roundingModeType();
68
  }
69
};
70
71
class FloatingPointFPTypeRule {
72
 public:
73
22
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
74
                                     bool check) {
75
22
    TRACE("FloatingPointFPTypeRule");
76
77
44
    TypeNode signType = n[0].getType(check);
78
44
    TypeNode exponentType = n[1].getType(check);
79
44
    TypeNode significandType = n[2].getType(check);
80
81
44
    if (!signType.isBitVector() || !exponentType.isBitVector() ||
82
22
        !significandType.isBitVector()) {
83
      throw TypeCheckingExceptionPrivate(n,
84
                                         "arguments to fp must be bit vectors");
85
    }
86
87
22
    unsigned signBits = signType.getBitVectorSize();
88
22
    unsigned exponentBits = exponentType.getBitVectorSize();
89
22
    unsigned significandBits = significandType.getBitVectorSize();
90
91
22
    if (check) {
92
22
      if (signBits != 1) {
93
        throw TypeCheckingExceptionPrivate(
94
            n, "sign bit vector in fp must be 1 bit long");
95
22
      } else if (!(validExponentSize(exponentBits))) {
96
        throw TypeCheckingExceptionPrivate(
97
            n, "exponent bit vector in fp is an invalid size");
98
22
      } else if (!(validSignificandSize(significandBits))) {
99
        throw TypeCheckingExceptionPrivate(
100
            n, "significand bit vector in fp is an invalid size");
101
      }
102
    }
103
104
    // The +1 is for the implicit hidden bit
105
44
    return nodeManager->mkFloatingPointType(exponentBits, significandBits + 1);
106
  }
107
};
108
109
class FloatingPointTestTypeRule {
110
 public:
111
951
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
112
                                     bool check) {
113
951
    TRACE("FloatingPointTestTypeRule");
114
115
951
    if (check) {
116
1902
      TypeNode firstOperand = n[0].getType(check);
117
118
951
      if (!firstOperand.isFloatingPoint()) {
119
        throw TypeCheckingExceptionPrivate(
120
            n, "floating-point test applied to a non floating-point sort");
121
      }
122
123
951
      size_t children = n.getNumChildren();
124
1250
      for (size_t i = 1; i < children; ++i) {
125
299
        if (!(n[i].getType(check) == firstOperand)) {
126
          throw TypeCheckingExceptionPrivate(
127
              n, "floating-point test applied to mixed sorts");
128
        }
129
      }
130
    }
131
132
951
    return nodeManager->booleanType();
133
  }
134
};
135
136
class FloatingPointOperationTypeRule {
137
 public:
138
827
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
139
                                     bool check) {
140
827
    TRACE("FloatingPointOperationTypeRule");
141
142
827
    TypeNode firstOperand = n[0].getType(check);
143
144
827
    if (check) {
145
827
      if (!firstOperand.isFloatingPoint()) {
146
        throw TypeCheckingExceptionPrivate(
147
            n, "floating-point operation applied to a non floating-point sort");
148
      }
149
150
827
      size_t children = n.getNumChildren();
151
1309
      for (size_t i = 1; i < children; ++i) {
152
482
        if (!(n[i].getType(check) == firstOperand)) {
153
          throw TypeCheckingExceptionPrivate(
154
              n, "floating-point test applied to mixed sorts");
155
        }
156
      }
157
    }
158
159
827
    return firstOperand;
160
  }
161
};
162
163
class FloatingPointRoundingOperationTypeRule {
164
 public:
165
1729
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
166
                                     bool check) {
167
1729
    TRACE("FloatingPointRoundingOperationTypeRule");
168
169
1729
    if (check) {
170
3458
      TypeNode roundingModeType = n[0].getType(check);
171
172
1729
      if (!roundingModeType.isRoundingMode()) {
173
        throw TypeCheckingExceptionPrivate(
174
            n, "first argument must be a rounding mode");
175
      }
176
    }
177
178
1729
    TypeNode firstOperand = n[1].getType(check);
179
180
1729
    if (check) {
181
1729
      if (!firstOperand.isFloatingPoint()) {
182
        throw TypeCheckingExceptionPrivate(
183
            n, "floating-point operation applied to a non floating-point sort");
184
      }
185
186
1729
      size_t children = n.getNumChildren();
187
3285
      for (size_t i = 2; i < children; ++i) {
188
1556
        if (!(n[i].getType(check) == firstOperand)) {
189
          throw TypeCheckingExceptionPrivate(
190
              n, "floating-point operation applied to mixed sorts");
191
        }
192
      }
193
    }
194
195
1729
    return firstOperand;
196
  }
197
};
198
199
class FloatingPointPartialOperationTypeRule {
200
 public:
201
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
202
                                     bool check) {
203
    TRACE("FloatingPointOperationTypeRule");
204
    AlwaysAssert(n.getNumChildren() > 0);
205
206
    TypeNode firstOperand = n[0].getType(check);
207
208
    if (check) {
209
      if (!firstOperand.isFloatingPoint()) {
210
        throw TypeCheckingExceptionPrivate(
211
            n, "floating-point operation applied to a non floating-point sort");
212
      }
213
214
      const size_t children = n.getNumChildren();
215
      for (size_t i = 1; i < children - 1; ++i) {
216
        if (n[i].getType(check) != firstOperand) {
217
          throw TypeCheckingExceptionPrivate(
218
              n, "floating-point partial operation applied to mixed sorts");
219
        }
220
      }
221
222
      TypeNode UFValueType = n[children - 1].getType(check);
223
224
      if (!(UFValueType.isBitVector()) ||
225
	  !(UFValueType.getBitVectorSize() == 1)) {
226
	throw TypeCheckingExceptionPrivate(
227
	    n, "floating-point partial operation final argument must be a bit-vector of length 1");
228
      }
229
    }
230
231
    return firstOperand;
232
  }
233
};
234
235
236
class FloatingPointParametricOpTypeRule {
237
 public:
238
33
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
239
                                     bool check) {
240
33
    TRACE("FloatingPointParametricOpTypeRule");
241
242
33
    return nodeManager->builtinOperatorType();
243
  }
244
};
245
246
class FloatingPointToFPIEEEBitVectorTypeRule {
247
 public:
248
445
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
249
                                     bool check) {
250
445
    TRACE("FloatingPointToFPIEEEBitVectorTypeRule");
251
445
    AlwaysAssert(n.getNumChildren() == 1);
252
253
    FloatingPointToFPIEEEBitVector info =
254
445
        n.getOperator().getConst<FloatingPointToFPIEEEBitVector>();
255
256
445
    if (check) {
257
890
      TypeNode operandType = n[0].getType(check);
258
259
445
      if (!(operandType.isBitVector()))
260
      {
261
        throw TypeCheckingExceptionPrivate(n,
262
                                           "conversion to floating-point from "
263
                                           "bit vector used with sort other "
264
                                           "than bit vector");
265
      }
266
890
      else if (!(operandType.getBitVectorSize()
267
445
                 == info.d_fp_size.exponentWidth()
268
445
                        + info.d_fp_size.significandWidth()))
269
      {
270
        throw TypeCheckingExceptionPrivate(
271
            n,
272
            "conversion to floating-point from bit vector used with bit vector "
273
            "length that does not match floating point parameters");
274
      }
275
    }
276
277
445
    return nodeManager->mkFloatingPointType(info.d_fp_size);
278
  }
279
};
280
281
class FloatingPointToFPFloatingPointTypeRule {
282
 public:
283
6
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
284
                                     bool check) {
285
6
    TRACE("FloatingPointToFPFloatingPointTypeRule");
286
6
    AlwaysAssert(n.getNumChildren() == 2);
287
288
    FloatingPointToFPFloatingPoint info =
289
6
        n.getOperator().getConst<FloatingPointToFPFloatingPoint>();
290
291
6
    if (check) {
292
12
      TypeNode roundingModeType = n[0].getType(check);
293
294
6
      if (!roundingModeType.isRoundingMode()) {
295
        throw TypeCheckingExceptionPrivate(
296
            n, "first argument must be a rounding mode");
297
      }
298
299
12
      TypeNode operandType = n[1].getType(check);
300
301
6
      if (!(operandType.isFloatingPoint())) {
302
        throw TypeCheckingExceptionPrivate(n,
303
                                           "conversion to floating-point from "
304
                                           "floating-point used with sort "
305
                                           "other than floating-point");
306
      }
307
    }
308
309
6
    return nodeManager->mkFloatingPointType(info.d_fp_size);
310
  }
311
};
312
313
class FloatingPointToFPRealTypeRule {
314
 public:
315
17
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
316
                                     bool check) {
317
17
    TRACE("FloatingPointToFPRealTypeRule");
318
17
    AlwaysAssert(n.getNumChildren() == 2);
319
320
    FloatingPointToFPReal info =
321
17
        n.getOperator().getConst<FloatingPointToFPReal>();
322
323
17
    if (check) {
324
34
      TypeNode roundingModeType = n[0].getType(check);
325
326
17
      if (!roundingModeType.isRoundingMode()) {
327
        throw TypeCheckingExceptionPrivate(
328
            n, "first argument must be a rounding mode");
329
      }
330
331
34
      TypeNode operandType = n[1].getType(check);
332
333
17
      if (!(operandType.isReal())) {
334
        throw TypeCheckingExceptionPrivate(n,
335
                                           "conversion to floating-point from "
336
                                           "real used with sort other than "
337
                                           "real");
338
      }
339
    }
340
341
17
    return nodeManager->mkFloatingPointType(info.d_fp_size);
342
  }
343
};
344
345
class FloatingPointToFPSignedBitVectorTypeRule {
346
 public:
347
3
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
348
                                     bool check) {
349
3
    TRACE("FloatingPointToFPSignedBitVectorTypeRule");
350
3
    AlwaysAssert(n.getNumChildren() == 2);
351
352
    FloatingPointToFPSignedBitVector info =
353
3
        n.getOperator().getConst<FloatingPointToFPSignedBitVector>();
354
355
3
    if (check) {
356
6
      TypeNode roundingModeType = n[0].getType(check);
357
358
3
      if (!roundingModeType.isRoundingMode()) {
359
        throw TypeCheckingExceptionPrivate(
360
            n, "first argument must be a rounding mode");
361
      }
362
363
6
      TypeNode operandType = n[1].getType(check);
364
365
3
      if (!(operandType.isBitVector())) {
366
        throw TypeCheckingExceptionPrivate(n,
367
                                           "conversion to floating-point from "
368
                                           "signed bit vector used with sort "
369
                                           "other than bit vector");
370
      }
371
    }
372
373
3
    return nodeManager->mkFloatingPointType(info.d_fp_size);
374
  }
375
};
376
377
class FloatingPointToFPUnsignedBitVectorTypeRule {
378
 public:
379
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
380
                                     bool check) {
381
    TRACE("FloatingPointToFPUnsignedBitVectorTypeRule");
382
    AlwaysAssert(n.getNumChildren() == 2);
383
384
    FloatingPointToFPUnsignedBitVector info =
385
        n.getOperator().getConst<FloatingPointToFPUnsignedBitVector>();
386
387
    if (check) {
388
      TypeNode roundingModeType = n[0].getType(check);
389
390
      if (!roundingModeType.isRoundingMode()) {
391
        throw TypeCheckingExceptionPrivate(
392
            n, "first argument must be a rounding mode");
393
      }
394
395
      TypeNode operandType = n[1].getType(check);
396
397
      if (!(operandType.isBitVector())) {
398
        throw TypeCheckingExceptionPrivate(n,
399
                                           "conversion to floating-point from "
400
                                           "unsigned bit vector used with sort "
401
                                           "other than bit vector");
402
      }
403
    }
404
405
    return nodeManager->mkFloatingPointType(info.d_fp_size);
406
  }
407
};
408
409
class FloatingPointToFPGenericTypeRule {
410
 public:
411
46
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
412
                                     bool check) {
413
46
    TRACE("FloatingPointToFPGenericTypeRule");
414
415
    FloatingPointToFPGeneric info =
416
46
        n.getOperator().getConst<FloatingPointToFPGeneric>();
417
418
46
    if (check) {
419
      /* As this is a generic kind intended only for parsing,
420
       * the checking here is light.  For better checking, use
421
       * expandDefinitions first.
422
       */
423
424
46
      size_t children = n.getNumChildren();
425
116
      for (size_t i = 0; i < children; ++i) {
426
70
        n[i].getType(check);
427
      }
428
    }
429
430
46
    return nodeManager->mkFloatingPointType(info.d_fp_size);
431
  }
432
};
433
434
class FloatingPointToUBVTypeRule {
435
 public:
436
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
437
                                     bool check) {
438
    TRACE("FloatingPointToUBVTypeRule");
439
    AlwaysAssert(n.getNumChildren() == 2);
440
441
    FloatingPointToUBV info = n.getOperator().getConst<FloatingPointToUBV>();
442
443
    if (check) {
444
      TypeNode roundingModeType = n[0].getType(check);
445
446
      if (!roundingModeType.isRoundingMode()) {
447
        throw TypeCheckingExceptionPrivate(
448
            n, "first argument must be a rounding mode");
449
      }
450
451
      TypeNode operandType = n[1].getType(check);
452
453
      if (!(operandType.isFloatingPoint())) {
454
        throw TypeCheckingExceptionPrivate(n,
455
                                           "conversion to unsigned bit vector "
456
                                           "used with a sort other than "
457
                                           "floating-point");
458
      }
459
    }
460
461
    return nodeManager->mkBitVectorType(info.d_bv_size);
462
  }
463
};
464
465
class FloatingPointToSBVTypeRule {
466
 public:
467
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
468
                                     bool check) {
469
    TRACE("FloatingPointToSBVTypeRule");
470
    AlwaysAssert(n.getNumChildren() == 2);
471
472
    FloatingPointToSBV info = n.getOperator().getConst<FloatingPointToSBV>();
473
474
    if (check) {
475
      TypeNode roundingModeType = n[0].getType(check);
476
477
      if (!roundingModeType.isRoundingMode()) {
478
        throw TypeCheckingExceptionPrivate(
479
            n, "first argument must be a rounding mode");
480
      }
481
482
      TypeNode operandType = n[1].getType(check);
483
484
      if (!(operandType.isFloatingPoint())) {
485
        throw TypeCheckingExceptionPrivate(n,
486
                                           "conversion to signed bit vector "
487
                                           "used with a sort other than "
488
                                           "floating-point");
489
      }
490
    }
491
492
    return nodeManager->mkBitVectorType(info.d_bv_size);
493
  }
494
};
495
496
class FloatingPointToUBVTotalTypeRule {
497
 public:
498
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
499
                                     bool check) {
500
    TRACE("FloatingPointToUBVTotalTypeRule");
501
    AlwaysAssert(n.getNumChildren() == 3);
502
503
    FloatingPointToUBVTotal info = n.getOperator().getConst<FloatingPointToUBVTotal>();
504
505
    if (check) {
506
      TypeNode roundingModeType = n[0].getType(check);
507
508
      if (!roundingModeType.isRoundingMode()) {
509
        throw TypeCheckingExceptionPrivate(
510
            n, "first argument must be a rounding mode");
511
      }
512
513
      TypeNode operandType = n[1].getType(check);
514
515
      if (!(operandType.isFloatingPoint())) {
516
        throw TypeCheckingExceptionPrivate(n,
517
                                           "conversion to unsigned bit vector total"
518
                                           "used with a sort other than "
519
                                           "floating-point");
520
      }
521
522
      TypeNode defaultValueType = n[2].getType(check);
523
524
      if (!(defaultValueType.isBitVector()) ||
525
	  !(defaultValueType.getBitVectorSize() == info)) {
526
	throw TypeCheckingExceptionPrivate(n,
527
					   "conversion to unsigned bit vector total"
528
					   "needs a bit vector of the same length"
529
					   "as last argument");
530
      }
531
    }
532
533
    return nodeManager->mkBitVectorType(info.d_bv_size);
534
  }
535
};
536
537
class FloatingPointToSBVTotalTypeRule {
538
 public:
539
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
540
                                     bool check) {
541
    TRACE("FloatingPointToSBVTotalTypeRule");
542
    AlwaysAssert(n.getNumChildren() == 3);
543
544
    FloatingPointToSBVTotal info = n.getOperator().getConst<FloatingPointToSBVTotal>();
545
546
    if (check) {
547
      TypeNode roundingModeType = n[0].getType(check);
548
549
      if (!roundingModeType.isRoundingMode()) {
550
        throw TypeCheckingExceptionPrivate(
551
            n, "first argument must be a rounding mode");
552
      }
553
554
      TypeNode operandType = n[1].getType(check);
555
556
      if (!(operandType.isFloatingPoint())) {
557
        throw TypeCheckingExceptionPrivate(n,
558
                                           "conversion to signed bit vector "
559
                                           "used with a sort other than "
560
                                           "floating-point");
561
      }
562
563
      TypeNode defaultValueType = n[2].getType(check);
564
565
      if (!(defaultValueType.isBitVector()) ||
566
	  !(defaultValueType.getBitVectorSize() == info)) {
567
	throw TypeCheckingExceptionPrivate(n,
568
					   "conversion to signed bit vector total"
569
					   "needs a bit vector of the same length"
570
					   "as last argument");
571
      }
572
    }
573
574
    return nodeManager->mkBitVectorType(info.d_bv_size);
575
  }
576
};
577
578
class FloatingPointToRealTypeRule {
579
 public:
580
6
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
581
                                     bool check) {
582
6
    TRACE("FloatingPointToRealTypeRule");
583
6
    AlwaysAssert(n.getNumChildren() == 1);
584
585
6
    if (check) {
586
12
      TypeNode operandType = n[0].getType(check);
587
588
6
      if (!operandType.isFloatingPoint()) {
589
        throw TypeCheckingExceptionPrivate(
590
            n, "floating-point to real applied to a non floating-point sort");
591
      }
592
    }
593
594
6
    return nodeManager->realType();
595
  }
596
};
597
598
class FloatingPointToRealTotalTypeRule {
599
 public:
600
12
  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
601
                                     bool check) {
602
12
    TRACE("FloatingPointToRealTotalTypeRule");
603
12
    AlwaysAssert(n.getNumChildren() == 2);
604
605
12
    if (check) {
606
24
      TypeNode operandType = n[0].getType(check);
607
608
12
      if (!operandType.isFloatingPoint()) {
609
        throw TypeCheckingExceptionPrivate(
610
            n, "floating-point to real total applied to a non floating-point sort");
611
      }
612
613
24
      TypeNode defaultValueType = n[1].getType(check);
614
615
12
      if (!defaultValueType.isReal()) {
616
        throw TypeCheckingExceptionPrivate(
617
            n, "floating-point to real total needs a real second argument");
618
      }
619
620
    }
621
622
12
    return nodeManager->realType();
623
  }
624
};
625
626
class FloatingPointComponentBit
627
{
628
 public:
629
420
  inline static TypeNode computeType(NodeManager* nodeManager,
630
                                     TNode n,
631
                                     bool check)
632
  {
633
420
    TRACE("FloatingPointComponentBit");
634
635
420
    if (check)
636
    {
637
840
      TypeNode operandType = n[0].getType(check);
638
639
420
      if (!operandType.isFloatingPoint())
640
      {
641
        throw TypeCheckingExceptionPrivate(n,
642
                                           "floating-point bit component "
643
                                           "applied to a non floating-point "
644
                                           "sort");
645
      }
646
840
      if (!(Theory::isLeafOf(n[0], THEORY_FP)
647
420
            || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
648
      {
649
        throw TypeCheckingExceptionPrivate(n,
650
                                           "floating-point bit component "
651
                                           "applied to a non leaf / to_fp leaf "
652
                                           "node");
653
      }
654
    }
655
656
420
    return nodeManager->mkBitVectorType(1);
657
  }
658
};
659
660
class FloatingPointComponentExponent
661
{
662
 public:
663
105
  inline static TypeNode computeType(NodeManager* nodeManager,
664
                                     TNode n,
665
                                     bool check)
666
  {
667
105
    TRACE("FloatingPointComponentExponent");
668
669
210
    TypeNode operandType = n[0].getType(check);
670
671
105
    if (check)
672
    {
673
105
      if (!operandType.isFloatingPoint())
674
      {
675
        throw TypeCheckingExceptionPrivate(n,
676
                                           "floating-point exponent component "
677
                                           "applied to a non floating-point "
678
                                           "sort");
679
      }
680
210
      if (!(Theory::isLeafOf(n[0], THEORY_FP)
681
105
            || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
682
      {
683
        throw TypeCheckingExceptionPrivate(n,
684
                                           "floating-point exponent component "
685
                                           "applied to a non leaf / to_fp "
686
                                           "node");
687
      }
688
    }
689
690
#ifdef CVC4_USE_SYMFPU
691
    /* Need to create some symfpu objects as the size of bit-vector
692
     * that is needed for this component is dependent on the encoding
693
     * used (i.e. whether subnormals are forcibly normalised or not).
694
     * Here we use types from floatingpoint.h which are the literal
695
     * back-end but it should't make a difference. */
696
105
    FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
697
105
    unsigned bw = FloatingPoint::getUnpackedExponentWidth(fps);
698
#else
699
    unsigned bw = 2;
700
#endif
701
210
    return nodeManager->mkBitVectorType(bw);
702
  }
703
};
704
705
class FloatingPointComponentSignificand
706
{
707
 public:
708
105
  inline static TypeNode computeType(NodeManager* nodeManager,
709
                                     TNode n,
710
                                     bool check)
711
  {
712
105
    TRACE("FloatingPointComponentSignificand");
713
714
210
    TypeNode operandType = n[0].getType(check);
715
716
105
    if (check)
717
    {
718
105
      if (!operandType.isFloatingPoint())
719
      {
720
        throw TypeCheckingExceptionPrivate(n,
721
                                           "floating-point significand "
722
                                           "component applied to a non "
723
                                           "floating-point sort");
724
      }
725
210
      if (!(Theory::isLeafOf(n[0], THEORY_FP)
726
105
            || n[0].getKind() == kind::FLOATINGPOINT_TO_FP_REAL))
727
      {
728
        throw TypeCheckingExceptionPrivate(n,
729
                                           "floating-point significand "
730
                                           "component applied to a non leaf / "
731
                                           "to_fp node");
732
      }
733
    }
734
735
#ifdef CVC4_USE_SYMFPU
736
    /* As before we need to use some of sympfu. */
737
105
    FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
738
105
    unsigned bw = FloatingPoint::getUnpackedSignificandWidth(fps);
739
#else
740
    unsigned bw = 1;
741
#endif
742
210
    return nodeManager->mkBitVectorType(bw);
743
  }
744
};
745
746
class RoundingModeBitBlast
747
{
748
 public:
749
1
  inline static TypeNode computeType(NodeManager* nodeManager,
750
                                     TNode n,
751
                                     bool check)
752
  {
753
1
    TRACE("RoundingModeBitBlast");
754
755
1
    if (check)
756
    {
757
2
      TypeNode operandType = n[0].getType(check);
758
759
1
      if (!operandType.isRoundingMode())
760
      {
761
        throw TypeCheckingExceptionPrivate(
762
            n, "rounding mode bit-blast applied to a non rounding-mode sort");
763
      }
764
1
      if (!Theory::isLeafOf(n[0], THEORY_FP))
765
      {
766
        throw TypeCheckingExceptionPrivate(
767
            n, "rounding mode bit-blast applied to a non leaf node");
768
      }
769
    }
770
771
1
    return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES);
772
  }
773
};
774
775
class CardinalityComputer {
776
public:
777
12
  inline static Cardinality computeCardinality(TypeNode type) {
778
12
    Assert(type.getKind() == kind::FLOATINGPOINT_TYPE);
779
780
12
    FloatingPointSize fps = type.getConst<FloatingPointSize>();
781
782
    /*
783
     * 1                    NaN
784
     * 2*1                  Infinities
785
     * 2*1                  Zeros
786
     * 2*2^(s-1)            Subnormal
787
     * 2*((2^e)-2)*2^(s-1)  Normal
788
     *
789
     *  = 1 + 2*2 + 2*((2^e)-1)*2^(s-1)
790
     *  =       5 + ((2^e)-1)*2^s
791
     */
792
793
24
    Integer significandValues = Integer(2).pow(fps.significandWidth());
794
24
    Integer exponentValues = Integer(2).pow(fps.exponentWidth());
795
12
    exponentValues -= Integer(1);
796
797
24
    return Integer(5) + exponentValues * significandValues;
798
  }
799
};/* class CardinalityComputer */
800
801
802
803
804
}/* CVC4::theory::fp namespace */
805
}/* CVC4::theory namespace */
806
}/* CVC4 namespace */
807
808
#endif /* CVC4__THEORY__FP__THEORY_FP_TYPE_RULES_H */