src/theory/fp/theory_fp_type_rules.h

   1 /*********************                                                        */
   2 /*! \file theory_fp_type_rules.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Martin Brain, Tim King, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
  38                                      bool check) {
  39     TRACE("FloatingPointConstantTypeRule");
  40
  41     const FloatingPoint& f = n.getConst<FloatingPoint>();
  42
  43     if (check)
  44     {
  45       if (!(validExponentSize(f.d_fp_size.exponentWidth())))
  46       {
  47         throw TypeCheckingExceptionPrivate(
  48             n, "constant with invalid exponent size");
  49       }
  50       if (!(validSignificandSize(f.d_fp_size.significandWidth())))
  51       {
  52         throw TypeCheckingExceptionPrivate(
  53             n, "constant with invalid significand size");
  54       }
  55     }
  56     return nodeManager->mkFloatingPointType(f.d_fp_size);
  57   }
  58 };
  59
  60 class RoundingModeConstantTypeRule {
  61  public:
  62   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
  63                                      bool check) {
  64     TRACE("RoundingModeConstantTypeRule");
  65
  66     // Nothing to check!
  67     return nodeManager->roundingModeType();
  68   }
  69 };
  70
  71 class FloatingPointFPTypeRule {
  72  public:
  73   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
  74                                      bool check) {
  75     TRACE("FloatingPointFPTypeRule");
  76
  77     TypeNode signType = n[0].getType(check);
  78     TypeNode exponentType = n[1].getType(check);
  79     TypeNode significandType = n[2].getType(check);
  80
  81     if (!signType.isBitVector() || !exponentType.isBitVector() ||
  82         !significandType.isBitVector()) {
  83       throw TypeCheckingExceptionPrivate(n,
  84                                          "arguments to fp must be bit vectors");
  85     }
  86
  87     unsigned signBits = signType.getBitVectorSize();
  88     unsigned exponentBits = exponentType.getBitVectorSize();
  89     unsigned significandBits = significandType.getBitVectorSize();
  90
  91     if (check) {
  92       if (signBits != 1) {
  93         throw TypeCheckingExceptionPrivate(
  94             n, "sign bit vector in fp must be 1 bit long");
  95       } else if (!(validExponentSize(exponentBits))) {
  96         throw TypeCheckingExceptionPrivate(
  97             n, "exponent bit vector in fp is an invalid size");
  98       } 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     return nodeManager->mkFloatingPointType(exponentBits, significandBits + 1);
 106   }
 107 };
 108
 109 class FloatingPointTestTypeRule {
 110  public:
 111   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 112                                      bool check) {
 113     TRACE("FloatingPointTestTypeRule");
 114
 115     if (check) {
 116       TypeNode firstOperand = n[0].getType(check);
 117
 118       if (!firstOperand.isFloatingPoint()) {
 119         throw TypeCheckingExceptionPrivate(
 120             n, "floating-point test applied to a non floating-point sort");
 121       }
 122
 123       size_t children = n.getNumChildren();
 124       for (size_t i = 1; i < children; ++i) {
 125         if (!(n[i].getType(check) == firstOperand)) {
 126           throw TypeCheckingExceptionPrivate(
 127               n, "floating-point test applied to mixed sorts");
 128         }
 129       }
 130     }
 131
 132     return nodeManager->booleanType();
 133   }
 134 };
 135
 136 class FloatingPointOperationTypeRule {
 137  public:
 138   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 139                                      bool check) {
 140     TRACE("FloatingPointOperationTypeRule");
 141
 142     TypeNode firstOperand = n[0].getType(check);
 143
 144     if (check) {
 145       if (!firstOperand.isFloatingPoint()) {
 146         throw TypeCheckingExceptionPrivate(
 147             n, "floating-point operation applied to a non floating-point sort");
 148       }
 149
 150       size_t children = n.getNumChildren();
 151       for (size_t i = 1; i < children; ++i) {
 152         if (!(n[i].getType(check) == firstOperand)) {
 153           throw TypeCheckingExceptionPrivate(
 154               n, "floating-point test applied to mixed sorts");
 155         }
 156       }
 157     }
 158
 159     return firstOperand;
 160   }
 161 };
 162
 163 class FloatingPointRoundingOperationTypeRule {
 164  public:
 165   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 166                                      bool check) {
 167     TRACE("FloatingPointRoundingOperationTypeRule");
 168
 169     if (check) {
 170       TypeNode roundingModeType = n[0].getType(check);
 171
 172       if (!roundingModeType.isRoundingMode()) {
 173         throw TypeCheckingExceptionPrivate(
 174             n, "first argument must be a rounding mode");
 175       }
 176     }
 177
 178     TypeNode firstOperand = n[1].getType(check);
 179
 180     if (check) {
 181       if (!firstOperand.isFloatingPoint()) {
 182         throw TypeCheckingExceptionPrivate(
 183             n, "floating-point operation applied to a non floating-point sort");
 184       }
 185
 186       size_t children = n.getNumChildren();
 187       for (size_t i = 2; i < children; ++i) {
 188         if (!(n[i].getType(check) == firstOperand)) {
 189           throw TypeCheckingExceptionPrivate(
 190               n, "floating-point operation applied to mixed sorts");
 191         }
 192       }
 193     }
 194
 195     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   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 239                                      bool check) {
 240     TRACE("FloatingPointParametricOpTypeRule");
 241
 242     return nodeManager->builtinOperatorType();
 243   }
 244 };
 245
 246 class FloatingPointToFPIEEEBitVectorTypeRule {
 247  public:
 248   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 249                                      bool check) {
 250     TRACE("FloatingPointToFPIEEEBitVectorTypeRule");
 251     AlwaysAssert(n.getNumChildren() == 1);
 252
 253     FloatingPointToFPIEEEBitVector info =
 254         n.getOperator().getConst<FloatingPointToFPIEEEBitVector>();
 255
 256     if (check) {
 257       TypeNode operandType = n[0].getType(check);
 258
 259       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       else if (!(operandType.getBitVectorSize()
 267                  == info.d_fp_size.exponentWidth()
 268                         + 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     return nodeManager->mkFloatingPointType(info.d_fp_size);
 278   }
 279 };
 280
 281 class FloatingPointToFPFloatingPointTypeRule {
 282  public:
 283   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 284                                      bool check) {
 285     TRACE("FloatingPointToFPFloatingPointTypeRule");
 286     AlwaysAssert(n.getNumChildren() == 2);
 287
 288     FloatingPointToFPFloatingPoint info =
 289         n.getOperator().getConst<FloatingPointToFPFloatingPoint>();
 290
 291     if (check) {
 292       TypeNode roundingModeType = n[0].getType(check);
 293
 294       if (!roundingModeType.isRoundingMode()) {
 295         throw TypeCheckingExceptionPrivate(
 296             n, "first argument must be a rounding mode");
 297       }
 298
 299       TypeNode operandType = n[1].getType(check);
 300
 301       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     return nodeManager->mkFloatingPointType(info.d_fp_size);
 310   }
 311 };
 312
 313 class FloatingPointToFPRealTypeRule {
 314  public:
 315   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 316                                      bool check) {
 317     TRACE("FloatingPointToFPRealTypeRule");
 318     AlwaysAssert(n.getNumChildren() == 2);
 319
 320     FloatingPointToFPReal info =
 321         n.getOperator().getConst<FloatingPointToFPReal>();
 322
 323     if (check) {
 324       TypeNode roundingModeType = n[0].getType(check);
 325
 326       if (!roundingModeType.isRoundingMode()) {
 327         throw TypeCheckingExceptionPrivate(
 328             n, "first argument must be a rounding mode");
 329       }
 330
 331       TypeNode operandType = n[1].getType(check);
 332
 333       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     return nodeManager->mkFloatingPointType(info.d_fp_size);
 342   }
 343 };
 344
 345 class FloatingPointToFPSignedBitVectorTypeRule {
 346  public:
 347   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 348                                      bool check) {
 349     TRACE("FloatingPointToFPSignedBitVectorTypeRule");
 350     AlwaysAssert(n.getNumChildren() == 2);
 351
 352     FloatingPointToFPSignedBitVector info =
 353         n.getOperator().getConst<FloatingPointToFPSignedBitVector>();
 354
 355     if (check) {
 356       TypeNode roundingModeType = n[0].getType(check);
 357
 358       if (!roundingModeType.isRoundingMode()) {
 359         throw TypeCheckingExceptionPrivate(
 360             n, "first argument must be a rounding mode");
 361       }
 362
 363       TypeNode operandType = n[1].getType(check);
 364
 365       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     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   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 412                                      bool check) {
 413     TRACE("FloatingPointToFPGenericTypeRule");
 414
 415     FloatingPointToFPGeneric info =
 416         n.getOperator().getConst<FloatingPointToFPGeneric>();
 417
 418     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       size_t children = n.getNumChildren();
 425       for (size_t i = 0; i < children; ++i) {
 426         n[i].getType(check);
 427       }
 428     }
 429
 430     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   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 581                                      bool check) {
 582     TRACE("FloatingPointToRealTypeRule");
 583     AlwaysAssert(n.getNumChildren() == 1);
 584
 585     if (check) {
 586       TypeNode operandType = n[0].getType(check);
 587
 588       if (!operandType.isFloatingPoint()) {
 589         throw TypeCheckingExceptionPrivate(
 590             n, "floating-point to real applied to a non floating-point sort");
 591       }
 592     }
 593
 594     return nodeManager->realType();
 595   }
 596 };
 597
 598 class FloatingPointToRealTotalTypeRule {
 599  public:
 600   inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
 601                                      bool check) {
 602     TRACE("FloatingPointToRealTotalTypeRule");
 603     AlwaysAssert(n.getNumChildren() == 2);
 604
 605     if (check) {
 606       TypeNode operandType = n[0].getType(check);
 607
 608       if (!operandType.isFloatingPoint()) {
 609         throw TypeCheckingExceptionPrivate(
 610             n, "floating-point to real total applied to a non floating-point sort");
 611       }
 612
 613       TypeNode defaultValueType = n[1].getType(check);
 614
 615       if (!defaultValueType.isReal()) {
 616         throw TypeCheckingExceptionPrivate(
 617             n, "floating-point to real total needs a real second argument");
 618       }
 619
 620     }
 621
 622     return nodeManager->realType();
 623   }
 624 };
 625
 626 class FloatingPointComponentBit
 627 {
 628  public:
 629   inline static TypeNode computeType(NodeManager* nodeManager,
 630                                      TNode n,
 631                                      bool check)
 632   {
 633     TRACE("FloatingPointComponentBit");
 634
 635     if (check)
 636     {
 637       TypeNode operandType = n[0].getType(check);
 638
 639       if (!operandType.isFloatingPoint())
 640       {
 641         throw TypeCheckingExceptionPrivate(n,
 642                                            "floating-point bit component "
 643                                            "applied to a non floating-point "
 644                                            "sort");
 645       }
 646       if (!(Theory::isLeafOf(n[0], THEORY_FP)
 647             || 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     return nodeManager->mkBitVectorType(1);
 657   }
 658 };
 659
 660 class FloatingPointComponentExponent
 661 {
 662  public:
 663   inline static TypeNode computeType(NodeManager* nodeManager,
 664                                      TNode n,
 665                                      bool check)
 666   {
 667     TRACE("FloatingPointComponentExponent");
 668
 669     TypeNode operandType = n[0].getType(check);
 670
 671     if (check)
 672     {
 673       if (!operandType.isFloatingPoint())
 674       {
 675         throw TypeCheckingExceptionPrivate(n,
 676                                            "floating-point exponent component "
 677                                            "applied to a non floating-point "
 678                                            "sort");
 679       }
 680       if (!(Theory::isLeafOf(n[0], THEORY_FP)
 681             || 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     FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
 697     unsigned bw = FloatingPoint::getUnpackedExponentWidth(fps);
 698 #else
 699     unsigned bw = 2;
 700 #endif
 701     return nodeManager->mkBitVectorType(bw);
 702   }
 703 };
 704
 705 class FloatingPointComponentSignificand
 706 {
 707  public:
 708   inline static TypeNode computeType(NodeManager* nodeManager,
 709                                      TNode n,
 710                                      bool check)
 711   {
 712     TRACE("FloatingPointComponentSignificand");
 713
 714     TypeNode operandType = n[0].getType(check);
 715
 716     if (check)
 717     {
 718       if (!operandType.isFloatingPoint())
 719       {
 720         throw TypeCheckingExceptionPrivate(n,
 721                                            "floating-point significand "
 722                                            "component applied to a non "
 723                                            "floating-point sort");
 724       }
 725       if (!(Theory::isLeafOf(n[0], THEORY_FP)
 726             || 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     FloatingPointSize fps = operandType.getConst<FloatingPointSize>();
 738     unsigned bw = FloatingPoint::getUnpackedSignificandWidth(fps);
 739 #else
 740     unsigned bw = 1;
 741 #endif
 742     return nodeManager->mkBitVectorType(bw);
 743   }
 744 };
 745
 746 class RoundingModeBitBlast
 747 {
 748  public:
 749   inline static TypeNode computeType(NodeManager* nodeManager,
 750                                      TNode n,
 751                                      bool check)
 752   {
 753     TRACE("RoundingModeBitBlast");
 754
 755     if (check)
 756     {
 757       TypeNode operandType = n[0].getType(check);
 758
 759       if (!operandType.isRoundingMode())
 760       {
 761         throw TypeCheckingExceptionPrivate(
 762             n, "rounding mode bit-blast applied to a non rounding-mode sort");
 763       }
 764       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     return nodeManager->mkBitVectorType(CVC4_NUM_ROUNDING_MODES);
 772   }
 773 };
 774
 775 class CardinalityComputer {
 776 public:
 777   inline static Cardinality computeCardinality(TypeNode type) {
 778     Assert(type.getKind() == kind::FLOATINGPOINT_TYPE);
 779
 780     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     Integer significandValues = Integer(2).pow(fps.significandWidth());
 794     Integer exponentValues = Integer(2).pow(fps.exponentWidth());
 795     exponentValues -= Integer(1);
 796
 797     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 */