src/util/floatingpoint.cpp

   1 /*********************                                                        */
   2 /*! \file floatingpoint.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Martin Brain, Martin Brain, Tim King
   6  ** Copyright (c) 2013  University of Oxford
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2019 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 [[ Implementations of the utility functions for working with floating point theories. ]]
  14  **
  15  **/
  16
  17 #include "util/floatingpoint.h"
  18 #include "base/cvc4_assert.h"
  19 #include "util/integer.h"
  20
  21 #include <math.h>
  22
  23 #ifdef CVC4_USE_SYMFPU
  24 #include "symfpu/core/add.h"
  25 #include "symfpu/core/classify.h"
  26 #include "symfpu/core/compare.h"
  27 #include "symfpu/core/convert.h"
  28 #include "symfpu/core/divide.h"
  29 #include "symfpu/core/fma.h"
  30 #include "symfpu/core/ite.h"
  31 #include "symfpu/core/multiply.h"
  32 #include "symfpu/core/packing.h"
  33 #include "symfpu/core/remainder.h"
  34 #include "symfpu/core/sign.h"
  35 #include "symfpu/core/sqrt.h"
  36 #include "symfpu/utils/numberOfRoundingModes.h"
  37 #include "symfpu/utils/properties.h"
  38 #endif
  39
  40 #ifdef CVC4_USE_SYMFPU
  41 namespace symfpu {
  42
  43 #define CVC4_LIT_ITE_DFN(T)                                        \
  44   template <>                                                      \
  45   struct ite<::CVC4::symfpuLiteral::prop, T>                       \
  46   {                                                                \
  47     static const T &iteOp(const ::CVC4::symfpuLiteral::prop &cond, \
  48                           const T &l,                              \
  49                           const T &r)                              \
  50     {                                                              \
  51       return cond ? l : r;                                         \
  52     }                                                              \
  53   }
  54
  55 CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm);
  56 CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop);
  57 CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv);
  58 CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv);
  59
  60 #undef CVC4_LIT_ITE_DFN
  61 }
  62 #endif
  63
  64 #ifndef CVC4_USE_SYMFPU
  65 #define PRECONDITION(X) Assert((X))
  66 #endif
  67
  68 namespace CVC4 {
  69
  70 FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s)
  71 {
  72   PrettyCheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e);
  73   PrettyCheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s);
  74 }
  75
  76 FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s)
  77 {
  78   PrettyCheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e);
  79   PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s);
  80 }
  81
  82 namespace symfpuLiteral {
  83
  84 // To simplify the property macros
  85 typedef traits t;
  86
  87 template <bool isSigned>
  88 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(const bwt &w)
  89 {
  90   return wrappedBitVector<isSigned>(w, 1);
  91 }
  92
  93 template <bool isSigned>
  94 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(const bwt &w)
  95 {
  96   return wrappedBitVector<isSigned>(w, 0);
  97 }
  98
  99 template <bool isSigned>
 100 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(const bwt &w)
 101 {
 102   return ~wrappedBitVector<isSigned>::zero(w);
 103 }
 104
 105 template <bool isSigned>
 106 prop wrappedBitVector<isSigned>::isAllOnes() const
 107 {
 108   return (*this == wrappedBitVector<isSigned>::allOnes(this->getWidth()));
 109 }
 110 template <bool isSigned>
 111 prop wrappedBitVector<isSigned>::isAllZeros() const
 112 {
 113   return (*this == wrappedBitVector<isSigned>::zero(this->getWidth()));
 114 }
 115
 116 template <bool isSigned>
 117 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(const bwt &w)
 118 {
 119   if (isSigned)
 120   {
 121     BitVector base(w - 1, 0U);
 122     return wrappedBitVector<true>((~base).zeroExtend(1));
 123   }
 124   else
 125   {
 126     return wrappedBitVector<false>::allOnes(w);
 127   }
 128 }
 129
 130 template <bool isSigned>
 131 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(const bwt &w)
 132 {
 133   if (isSigned)
 134   {
 135     BitVector base(w, 1U);
 136     BitVector shiftAmount(w, w - 1);
 137     BitVector result(base.leftShift(shiftAmount));
 138     return wrappedBitVector<true>(result);
 139   }
 140   else
 141   {
 142     return wrappedBitVector<false>::zero(w);
 143   }
 144 }
 145
 146 /*** Operators ***/
 147 template <bool isSigned>
 148 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<(
 149     const wrappedBitVector<isSigned> &op) const
 150 {
 151   return this->BitVector::leftShift(op);
 152 }
 153
 154 template <>
 155 wrappedBitVector<true> wrappedBitVector<true>::operator>>(
 156     const wrappedBitVector<true> &op) const
 157 {
 158   return this->BitVector::arithRightShift(op);
 159 }
 160
 161 template <>
 162 wrappedBitVector<false> wrappedBitVector<false>::operator>>(
 163     const wrappedBitVector<false> &op) const
 164 {
 165   return this->BitVector::logicalRightShift(op);
 166 }
 167
 168 template <bool isSigned>
 169 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
 170     const wrappedBitVector<isSigned> &op) const
 171 {
 172   return this->BitVector::operator|(op);
 173 }
 174
 175 template <bool isSigned>
 176 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
 177     const wrappedBitVector<isSigned> &op) const
 178 {
 179   return this->BitVector::operator&(op);
 180 }
 181
 182 template <bool isSigned>
 183 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
 184     const wrappedBitVector<isSigned> &op) const
 185 {
 186   return this->BitVector::operator+(op);
 187 }
 188
 189 template <bool isSigned>
 190 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
 191     const wrappedBitVector<isSigned> &op) const
 192 {
 193   return this->BitVector::operator-(op);
 194 }
 195
 196 template <bool isSigned>
 197 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
 198     const wrappedBitVector<isSigned> &op) const
 199 {
 200   return this->BitVector::operator*(op);
 201 }
 202
 203 template <>
 204 wrappedBitVector<false> wrappedBitVector<false>::operator/(
 205     const wrappedBitVector<false> &op) const
 206 {
 207   return this->BitVector::unsignedDivTotal(op);
 208 }
 209
 210 template <>
 211 wrappedBitVector<false> wrappedBitVector<false>::operator%(
 212     const wrappedBitVector<false> &op) const
 213 {
 214   return this->BitVector::unsignedRemTotal(op);
 215 }
 216
 217 template <bool isSigned>
 218 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
 219 {
 220   return this->BitVector::operator-();
 221 }
 222
 223 template <bool isSigned>
 224 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void)const
 225 {
 226   return this->BitVector::operator~();
 227 }
 228
 229 template <bool isSigned>
 230 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
 231 {
 232   return *this + wrappedBitVector<isSigned>::one(this->getWidth());
 233 }
 234
 235 template <bool isSigned>
 236 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
 237 {
 238   return *this - wrappedBitVector<isSigned>::one(this->getWidth());
 239 }
 240
 241 template <bool isSigned>
 242 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
 243     const wrappedBitVector<isSigned> &op) const
 244 {
 245   return this->BitVector::arithRightShift(BitVector(this->getWidth(), op));
 246 }
 247
 248 /*** Modular opertaions ***/
 249 // No overflow checking so these are the same as other operations
 250 template <bool isSigned>
 251 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift(
 252     const wrappedBitVector<isSigned> &op) const
 253 {
 254   return *this << op;
 255 }
 256
 257 template <bool isSigned>
 258 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift(
 259     const wrappedBitVector<isSigned> &op) const
 260 {
 261   return *this >> op;
 262 }
 263
 264 template <bool isSigned>
 265 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const
 266 {
 267   return this->increment();
 268 }
 269
 270 template <bool isSigned>
 271 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
 272 {
 273   return this->decrement();
 274 }
 275
 276 template <bool isSigned>
 277 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd(
 278     const wrappedBitVector<isSigned> &op) const
 279 {
 280   return *this + op;
 281 }
 282
 283 template <bool isSigned>
 284 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
 285 {
 286   return -(*this);
 287 }
 288
 289 /*** Comparisons ***/
 290
 291 template <bool isSigned>
 292 prop wrappedBitVector<isSigned>::operator==(
 293     const wrappedBitVector<isSigned> &op) const
 294 {
 295   return this->BitVector::operator==(op);
 296 }
 297
 298 template <>
 299 prop wrappedBitVector<true>::operator<=(const wrappedBitVector<true> &op) const
 300 {
 301   return this->signedLessThanEq(op);
 302 }
 303
 304 template <>
 305 prop wrappedBitVector<true>::operator>=(const wrappedBitVector<true> &op) const
 306 {
 307   return !(this->signedLessThan(op));
 308 }
 309
 310 template <>
 311 prop wrappedBitVector<true>::operator<(const wrappedBitVector<true> &op) const
 312 {
 313   return this->signedLessThan(op);
 314 }
 315
 316 template <>
 317 prop wrappedBitVector<true>::operator>(const wrappedBitVector<true> &op) const
 318 {
 319   return !(this->signedLessThanEq(op));
 320 }
 321
 322 template <>
 323 prop wrappedBitVector<false>::operator<=(
 324     const wrappedBitVector<false> &op) const
 325 {
 326   return this->unsignedLessThanEq(op);
 327 }
 328
 329 template <>
 330 prop wrappedBitVector<false>::operator>=(
 331     const wrappedBitVector<false> &op) const
 332 {
 333   return !(this->unsignedLessThan(op));
 334 }
 335
 336 template <>
 337 prop wrappedBitVector<false>::operator<(const wrappedBitVector<false> &op) const
 338 {
 339   return this->unsignedLessThan(op);
 340 }
 341
 342 template <>
 343 prop wrappedBitVector<false>::operator>(const wrappedBitVector<false> &op) const
 344 {
 345   return !(this->unsignedLessThanEq(op));
 346 }
 347
 348 /*** Type conversion ***/
 349 // CVC4 nodes make no distinction between signed and unsigned, thus ...
 350 template <bool isSigned>
 351 wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const
 352 {
 353   return wrappedBitVector<true>(*this);
 354 }
 355
 356 template <bool isSigned>
 357 wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const
 358 {
 359   return wrappedBitVector<false>(*this);
 360 }
 361
 362 /*** Bit hacks ***/
 363
 364 template <bool isSigned>
 365 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
 366     bwt extension) const
 367 {
 368   if (isSigned)
 369   {
 370     return this->BitVector::signExtend(extension);
 371   }
 372   else
 373   {
 374     return this->BitVector::zeroExtend(extension);
 375   }
 376 }
 377
 378 template <bool isSigned>
 379 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
 380     bwt reduction) const
 381 {
 382   PRECONDITION(this->getWidth() > reduction);
 383
 384   return this->extract((this->getWidth() - 1) - reduction, 0);
 385 }
 386
 387 template <bool isSigned>
 388 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize(bwt newSize) const
 389 {
 390   bwt width = this->getWidth();
 391
 392   if (newSize > width)
 393   {
 394     return this->extend(newSize - width);
 395   }
 396   else if (newSize < width)
 397   {
 398     return this->contract(width - newSize);
 399   }
 400   else
 401   {
 402     return *this;
 403   }
 404 }
 405
 406 template <bool isSigned>
 407 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
 408     const wrappedBitVector<isSigned> &op) const
 409 {
 410   PRECONDITION(this->getWidth() <= op.getWidth());
 411   return this->extend(op.getWidth() - this->getWidth());
 412 }
 413
 414 template <bool isSigned>
 415 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
 416     const wrappedBitVector<isSigned> &op) const
 417 {
 418   return this->BitVector::concat(op);
 419 }
 420
 421 // Inclusive of end points, thus if the same, extracts just one bit
 422 template <bool isSigned>
 423 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(bwt upper,
 424                                                                bwt lower) const
 425 {
 426   PRECONDITION(upper >= lower);
 427   return this->BitVector::extract(upper, lower);
 428 }
 429
 430 // Explicit instantiation
 431 template class wrappedBitVector<true>;
 432 template class wrappedBitVector<false>;
 433
 434 rm traits::RNE(void) { return ::CVC4::roundNearestTiesToEven; };
 435 rm traits::RNA(void) { return ::CVC4::roundNearestTiesToAway; };
 436 rm traits::RTP(void) { return ::CVC4::roundTowardPositive; };
 437 rm traits::RTN(void) { return ::CVC4::roundTowardNegative; };
 438 rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
 439 // This is a literal back-end so props are actually bools
 440 // so these can be handled in the same way as the internal assertions above
 441
 442 void traits::precondition(const prop &p)
 443 {
 444   AlwaysAssert(p);
 445   return;
 446 }
 447 void traits::postcondition(const prop &p)
 448 {
 449   AlwaysAssert(p);
 450   return;
 451 }
 452 void traits::invariant(const prop &p)
 453 {
 454   AlwaysAssert(p);
 455   return;
 456 }
 457 }
 458
 459 #ifndef CVC4_USE_SYMFPU
 460 void FloatingPointLiteral::unfinished(void) const
 461 {
 462   Unimplemented("Floating-point literals not yet implemented.");
 463 }
 464 #endif
 465
 466 FloatingPoint::FloatingPoint(unsigned e, unsigned s, const BitVector &bv)
 467     :
 468 #ifdef CVC4_USE_SYMFPU
 469       fpl(symfpu::unpack<symfpuLiteral::traits>(symfpuLiteral::fpt(e, s), bv)),
 470 #else
 471       fpl(e, s, 0.0),
 472 #endif
 473       t(e, s)
 474 {
 475 }
 476
 477 static FloatingPointLiteral constructorHelperBitVector(
 478     const FloatingPointSize &ct,
 479     const RoundingMode &rm,
 480     const BitVector &bv,
 481     bool signedBV)
 482 {
 483 #ifdef CVC4_USE_SYMFPU
 484   if (signedBV)
 485   {
 486     return FloatingPointLiteral(
 487         symfpu::convertSBVToFloat<symfpuLiteral::traits>(
 488             symfpuLiteral::fpt(ct),
 489             symfpuLiteral::rm(rm),
 490             symfpuLiteral::sbv(bv)));
 491   }
 492   else
 493   {
 494     return FloatingPointLiteral(
 495         symfpu::convertUBVToFloat<symfpuLiteral::traits>(
 496             symfpuLiteral::fpt(ct),
 497             symfpuLiteral::rm(rm),
 498             symfpuLiteral::ubv(bv)));
 499   }
 500 #else
 501   return FloatingPointLiteral(2, 2, 0.0);
 502 #endif
 503   Unreachable("Constructor helper broken");
 504   }
 505
 506   FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const BitVector &bv, bool signedBV) :
 507     fpl(constructorHelperBitVector(ct, rm, bv, signedBV)),
 508     t(ct) {}
 509
 510
 511   static FloatingPointLiteral constructorHelperRational (const FloatingPointSize &ct, const RoundingMode &rm, const Rational &ri) {
 512     Rational r(ri);
 513     Rational two(2,1);
 514
 515     if (r.isZero()) {
 516 #ifdef CVC4_USE_SYMFPU
 517       return FloatingPointLiteral::makeZero(
 518           ct, false);  // In keeping with the SMT-LIB standard
 519 #else
 520       return FloatingPointLiteral(2,2,0.0);
 521 #endif
 522     } else {
 523 #ifdef CVC4_USE_SYMFPU
 524       int negative = (r.sgn() < 0) ? 1 : 0;
 525 #endif
 526       r = r.abs();
 527
 528       // Compute the exponent
 529       Integer exp(0U);
 530       Integer inc(1U);
 531       Rational working(1,1);
 532
 533       if (r == working) {
 534
 535       } else if ( r < working ) {
 536         while (r < working) {
 537           exp -= inc;
 538           working /= two;
 539         }
 540       } else {
 541         while (r >= working) {
 542           exp += inc;
 543           working *= two;
 544         }
 545         exp -= inc;
 546         working /= two;
 547       }
 548
 549       Assert(working <= r);
 550       Assert(r < working * two);
 551
 552       // Work out the number of bits required to represent the exponent for a normal number
 553       unsigned expBits = 2; // No point starting with an invalid amount
 554
 555       Integer doubleInt(2);
 556       if (exp.strictlyPositive()) {
 557         Integer representable(4);     // 1 more than exactly representable with expBits
 558         while (representable <= exp) {// hence <=
 559           representable *= doubleInt;
 560           ++expBits;
 561         }
 562       } else if (exp.strictlyNegative()) {
 563         Integer representable(-4);    // Exactly representable with expBits + sign
 564                                       // but -2^n and -(2^n - 1) are both subnormal
 565         while ((representable + doubleInt) > exp) {
 566           representable *= doubleInt;
 567           ++expBits;
 568         }
 569       }
 570       ++expBits; // To allow for sign
 571
 572       BitVector exactExp(expBits, exp);
 573
 574
 575
 576       // Compute the significand.
 577       unsigned sigBits = ct.significandWidth() + 2;  // guard and sticky bits
 578       BitVector sig(sigBits, 0U);
 579       BitVector one(sigBits, 1U);
 580       Rational workingSig(0,1);
 581       for (unsigned i = 0; i < sigBits - 1; ++i) {
 582         Rational mid(workingSig + working);
 583
 584         if (mid <= r) {
 585           sig = sig | one;
 586           workingSig = mid;
 587         }
 588
 589         sig = sig.leftShift(one);
 590         working /= two;
 591       }
 592
 593       // Compute the sticky bit
 594       Rational remainder(r - workingSig);
 595       Assert(Rational(0,1) <= remainder);
 596
 597       if (!remainder.isZero()) {
 598         sig = sig | one;
 599       }
 600
 601       // Build an exact float
 602       FloatingPointSize exactFormat(expBits, sigBits);
 603
 604       // A small subtlety... if the format has expBits the unpacked format
 605       // may have more to allow subnormals to be normalised.
 606       // Thus...
 607 #ifdef CVC4_USE_SYMFPU
 608       unsigned extension =
 609           FloatingPointLiteral::exponentWidth(exactFormat) - expBits;
 610
 611       FloatingPointLiteral exactFloat(
 612           negative, exactExp.signExtend(extension), sig);
 613
 614       // Then cast...
 615       FloatingPointLiteral rounded(
 616           symfpu::convertFloatToFloat(exactFormat, ct, rm, exactFloat));
 617       return rounded;
 618 #else
 619       Unreachable("no concrete implementation of FloatingPointLiteral");
 620 #endif
 621     }
 622     Unreachable("Constructor helper broken");
 623   }
 624
 625   FloatingPoint::FloatingPoint (const FloatingPointSize &ct, const RoundingMode &rm, const Rational &r) :
 626     fpl(constructorHelperRational(ct, rm, r)),
 627     t(ct) {}
 628
 629
 630   FloatingPoint FloatingPoint::makeNaN (const FloatingPointSize &t) {
 631 #ifdef CVC4_USE_SYMFPU
 632     return FloatingPoint(
 633         t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeNaN(t));
 634 #else
 635     return FloatingPoint(2, 2, BitVector(4U,0U));
 636 #endif
 637   }
 638
 639   FloatingPoint FloatingPoint::makeInf (const FloatingPointSize &t, bool sign) {
 640 #ifdef CVC4_USE_SYMFPU
 641     return FloatingPoint(
 642         t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeInf(t, sign));
 643 #else
 644     return FloatingPoint(2, 2, BitVector(4U,0U));
 645 #endif
 646   }
 647
 648   FloatingPoint FloatingPoint::makeZero (const FloatingPointSize &t, bool sign) {
 649 #ifdef CVC4_USE_SYMFPU
 650     return FloatingPoint(
 651         t, symfpu::unpackedFloat<symfpuLiteral::traits>::makeZero(t, sign));
 652 #else
 653     return FloatingPoint(2, 2, BitVector(4U,0U));
 654 #endif
 655   }
 656
 657
 658   /* Operations implemented using symfpu */
 659   FloatingPoint FloatingPoint::absolute (void) const {
 660 #ifdef CVC4_USE_SYMFPU
 661     return FloatingPoint(t, symfpu::absolute<symfpuLiteral::traits>(t, fpl));
 662 #else
 663     return *this;
 664 #endif
 665   }
 666
 667   FloatingPoint FloatingPoint::negate (void) const {
 668 #ifdef CVC4_USE_SYMFPU
 669     return FloatingPoint(t, symfpu::negate<symfpuLiteral::traits>(t, fpl));
 670 #else
 671     return *this;
 672 #endif
 673   }
 674
 675   FloatingPoint FloatingPoint::plus (const RoundingMode &rm, const FloatingPoint &arg) const {
 676 #ifdef CVC4_USE_SYMFPU
 677     Assert(this->t == arg.t);
 678     return FloatingPoint(
 679         t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, true));
 680 #else
 681     return *this;
 682 #endif
 683   }
 684
 685   FloatingPoint FloatingPoint::sub (const RoundingMode &rm, const FloatingPoint &arg) const {
 686 #ifdef CVC4_USE_SYMFPU
 687     Assert(this->t == arg.t);
 688     return FloatingPoint(
 689         t, symfpu::add<symfpuLiteral::traits>(t, rm, fpl, arg.fpl, false));
 690 #else
 691     return *this;
 692 #endif
 693   }
 694
 695   FloatingPoint FloatingPoint::mult (const RoundingMode &rm, const FloatingPoint &arg) const {
 696 #ifdef CVC4_USE_SYMFPU
 697     Assert(this->t == arg.t);
 698     return FloatingPoint(
 699         t, symfpu::multiply<symfpuLiteral::traits>(t, rm, fpl, arg.fpl));
 700 #else
 701     return *this;
 702 #endif
 703   }
 704
 705   FloatingPoint FloatingPoint::fma (const RoundingMode &rm, const FloatingPoint &arg1, const FloatingPoint &arg2) const {
 706 #ifdef CVC4_USE_SYMFPU
 707     Assert(this->t == arg1.t);
 708     Assert(this->t == arg2.t);
 709     return FloatingPoint(
 710         t, symfpu::fma<symfpuLiteral::traits>(t, rm, fpl, arg1.fpl, arg2.fpl));
 711 #else
 712     return *this;
 713 #endif
 714   }
 715
 716   FloatingPoint FloatingPoint::div (const RoundingMode &rm, const FloatingPoint &arg) const {
 717 #ifdef CVC4_USE_SYMFPU
 718     Assert(this->t == arg.t);
 719     return FloatingPoint(
 720         t, symfpu::divide<symfpuLiteral::traits>(t, rm, fpl, arg.fpl));
 721 #else
 722     return *this;
 723 #endif
 724   }
 725
 726   FloatingPoint FloatingPoint::sqrt (const RoundingMode &rm) const {
 727 #ifdef CVC4_USE_SYMFPU
 728     return FloatingPoint(t, symfpu::sqrt<symfpuLiteral::traits>(t, rm, fpl));
 729 #else
 730     return *this;
 731 #endif
 732   }
 733
 734   FloatingPoint FloatingPoint::rti (const RoundingMode &rm) const {
 735 #ifdef CVC4_USE_SYMFPU
 736     return FloatingPoint(
 737         t, symfpu::roundToIntegral<symfpuLiteral::traits>(t, rm, fpl));
 738 #else
 739     return *this;
 740 #endif
 741   }
 742
 743   FloatingPoint FloatingPoint::rem (const FloatingPoint &arg) const {
 744 #ifdef CVC4_USE_SYMFPU
 745     Assert(this->t == arg.t);
 746     return FloatingPoint(
 747         t, symfpu::remainder<symfpuLiteral::traits>(t, fpl, arg.fpl));
 748 #else
 749     return *this;
 750 #endif
 751   }
 752
 753   FloatingPoint FloatingPoint::maxTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
 754 #ifdef CVC4_USE_SYMFPU
 755     Assert(this->t == arg.t);
 756     return FloatingPoint(
 757         t, symfpu::max<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft));
 758 #else
 759     return *this;
 760 #endif
 761   }
 762
 763   FloatingPoint FloatingPoint::minTotal (const FloatingPoint &arg, bool zeroCaseLeft) const {
 764 #ifdef CVC4_USE_SYMFPU
 765     Assert(this->t == arg.t);
 766     return FloatingPoint(
 767         t, symfpu::min<symfpuLiteral::traits>(t, fpl, arg.fpl, zeroCaseLeft));
 768 #else
 769     return *this;
 770 #endif
 771   }
 772
 773   FloatingPoint::PartialFloatingPoint FloatingPoint::max (const FloatingPoint &arg) const {
 774     FloatingPoint tmp(maxTotal(arg, true));
 775     return PartialFloatingPoint(tmp, tmp == maxTotal(arg, false));
 776   }
 777
 778   FloatingPoint::PartialFloatingPoint FloatingPoint::min (const FloatingPoint &arg) const {
 779     FloatingPoint tmp(minTotal(arg, true));
 780     return PartialFloatingPoint(tmp, tmp == minTotal(arg, false));
 781   }
 782
 783   bool FloatingPoint::operator ==(const FloatingPoint& fp) const {
 784 #ifdef CVC4_USE_SYMFPU
 785     return ((t == fp.t)
 786             && symfpu::smtlibEqual<symfpuLiteral::traits>(t, fpl, fp.fpl));
 787 #else
 788     return ( (t == fp.t) );
 789 #endif
 790   }
 791
 792   bool FloatingPoint::operator <= (const FloatingPoint &arg) const {
 793 #ifdef CVC4_USE_SYMFPU
 794     Assert(this->t == arg.t);
 795     return symfpu::lessThanOrEqual<symfpuLiteral::traits>(t, fpl, arg.fpl);
 796 #else
 797     return false;
 798 #endif
 799   }
 800
 801   bool FloatingPoint::operator < (const FloatingPoint &arg) const {
 802 #ifdef CVC4_USE_SYMFPU
 803     Assert(this->t == arg.t);
 804     return symfpu::lessThan<symfpuLiteral::traits>(t, fpl, arg.fpl);
 805 #else
 806     return false;
 807 #endif
 808   }
 809
 810   bool FloatingPoint::isNormal (void) const {
 811 #ifdef CVC4_USE_SYMFPU
 812     return symfpu::isNormal<symfpuLiteral::traits>(t, fpl);
 813 #else
 814     return false;
 815 #endif
 816   }
 817
 818   bool FloatingPoint::isSubnormal (void) const {
 819 #ifdef CVC4_USE_SYMFPU
 820     return symfpu::isSubnormal<symfpuLiteral::traits>(t, fpl);
 821 #else
 822     return false;
 823 #endif
 824   }
 825
 826   bool FloatingPoint::isZero (void) const {
 827 #ifdef CVC4_USE_SYMFPU
 828     return symfpu::isZero<symfpuLiteral::traits>(t, fpl);
 829 #else
 830     return false;
 831 #endif
 832   }
 833
 834   bool FloatingPoint::isInfinite (void) const {
 835 #ifdef CVC4_USE_SYMFPU
 836     return symfpu::isInfinite<symfpuLiteral::traits>(t, fpl);
 837 #else
 838     return false;
 839 #endif
 840   }
 841
 842   bool FloatingPoint::isNaN (void) const {
 843 #ifdef CVC4_USE_SYMFPU
 844     return symfpu::isNaN<symfpuLiteral::traits>(t, fpl);
 845 #else
 846     return false;
 847 #endif
 848   }
 849
 850   bool FloatingPoint::isNegative (void) const {
 851 #ifdef CVC4_USE_SYMFPU
 852     return symfpu::isNegative<symfpuLiteral::traits>(t, fpl);
 853 #else
 854     return false;
 855 #endif
 856   }
 857
 858   bool FloatingPoint::isPositive (void) const {
 859 #ifdef CVC4_USE_SYMFPU
 860     return symfpu::isPositive<symfpuLiteral::traits>(t, fpl);
 861 #else
 862     return false;
 863 #endif
 864   }
 865
 866   FloatingPoint FloatingPoint::convert (const FloatingPointSize &target, const RoundingMode &rm) const {
 867 #ifdef CVC4_USE_SYMFPU
 868     return FloatingPoint(
 869         target,
 870         symfpu::convertFloatToFloat<symfpuLiteral::traits>(t, target, rm, fpl));
 871 #else
 872     return *this;
 873 #endif
 874   }
 875
 876   BitVector FloatingPoint::convertToBVTotal (BitVectorSize width, const RoundingMode &rm, bool signedBV, BitVector undefinedCase) const {
 877 #ifdef CVC4_USE_SYMFPU
 878     if (signedBV)
 879       return symfpu::convertFloatToSBV<symfpuLiteral::traits>(
 880           t, rm, fpl, width, undefinedCase);
 881     else
 882       return symfpu::convertFloatToUBV<symfpuLiteral::traits>(
 883           t, rm, fpl, width, undefinedCase);
 884 #else
 885     return undefinedCase;
 886 #endif
 887   }
 888
 889   Rational FloatingPoint::convertToRationalTotal (Rational undefinedCase) const {
 890     PartialRational p(convertToRational());
 891
 892     return p.second ? p.first : undefinedCase;
 893   }
 894
 895   FloatingPoint::PartialBitVector FloatingPoint::convertToBV (BitVectorSize width, const RoundingMode &rm, bool signedBV) const {
 896     BitVector tmp(convertToBVTotal (width, rm, signedBV, BitVector(width, 0U)));
 897     BitVector confirm(convertToBVTotal (width, rm, signedBV, BitVector(width, 1U)));
 898
 899     return PartialBitVector(tmp, tmp == confirm);
 900   }
 901
 902   FloatingPoint::PartialRational FloatingPoint::convertToRational (void) const {
 903     if (this->isNaN() || this->isInfinite()) {
 904       return PartialRational(Rational(0U, 1U), false);
 905     }
 906     if (this->isZero()) {
 907       return PartialRational(Rational(0U, 1U), true);
 908
 909     } else {
 910 #ifdef CVC4_USE_SYMFPU
 911       Integer sign((this->fpl.getSign()) ? -1 : 1);
 912       Integer exp(
 913           this->fpl.getExponent().toSignedInteger()
 914           - (Integer(t.significand()
 915                      - 1)));  // -1 as forcibly normalised into the [1,2) range
 916       Integer significand(this->fpl.getSignificand().toInteger());
 917 #else
 918       Integer sign(0);
 919       Integer exp(0);
 920       Integer significand(0);
 921 #endif
 922       Integer signedSignificand(sign * significand);
 923
 924       // Only have pow(uint32_t) so we should check this.
 925       Assert(this->t.significand() <= 32);
 926
 927       if (!(exp.strictlyNegative())) {
 928         Integer r(signedSignificand.multiplyByPow2(exp.toUnsignedInt()));
 929         return PartialRational(Rational(r), true);
 930       } else {
 931         Integer one(1U);
 932         Integer q(one.multiplyByPow2((-exp).toUnsignedInt()));
 933         Rational r(signedSignificand, q);
 934         return PartialRational(r, true);
 935       }
 936     }
 937
 938     Unreachable("Convert float literal to real broken.");
 939   }
 940
 941   BitVector FloatingPoint::pack (void) const {
 942 #ifdef CVC4_USE_SYMFPU
 943     BitVector bv(symfpu::pack<symfpuLiteral::traits>(this->t, this->fpl));
 944 #else
 945     BitVector bv(4u,0u);
 946 #endif
 947     return bv;
 948   }
 949
 950
 951
 952 }/* CVC4 namespace */