src/util/floatingpoint_literal_symfpu_traits.cpp

   1 /*********************                                                        */
   2 /*! \file floatingpoint_literal_symfpu_traits.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   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 SymFPU glue code for floating-point values.
  13  **/
  14
  15 #if CVC4_USE_SYMFPU
  16
  17 #include "util/floatingpoint_literal_symfpu_traits.h"
  18
  19 #include "base/check.h"
  20
  21 namespace cvc5 {
  22 namespace symfpuLiteral {
  23
  24 template <bool isSigned>
  25 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(
  26     const Cvc5BitWidth& w)
  27 {
  28   return wrappedBitVector<isSigned>(w, 1);
  29 }
  30
  31 template <bool isSigned>
  32 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(
  33     const Cvc5BitWidth& w)
  34 {
  35   return wrappedBitVector<isSigned>(w, 0);
  36 }
  37
  38 template <bool isSigned>
  39 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(
  40     const Cvc5BitWidth& w)
  41 {
  42   return ~wrappedBitVector<isSigned>::zero(w);
  43 }
  44
  45 template <bool isSigned>
  46 Cvc5Prop wrappedBitVector<isSigned>::isAllOnes() const
  47 {
  48   return (*this == wrappedBitVector<isSigned>::allOnes(getWidth()));
  49 }
  50 template <bool isSigned>
  51 Cvc5Prop wrappedBitVector<isSigned>::isAllZeros() const
  52 {
  53   return (*this == wrappedBitVector<isSigned>::zero(getWidth()));
  54 }
  55
  56 template <bool isSigned>
  57 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(
  58     const Cvc5BitWidth& w)
  59 {
  60   if (isSigned)
  61   {
  62     BitVector base(w - 1, 0U);
  63     return wrappedBitVector<true>((~base).zeroExtend(1));
  64   }
  65   else
  66   {
  67     return wrappedBitVector<false>::allOnes(w);
  68   }
  69 }
  70
  71 template <bool isSigned>
  72 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(
  73     const Cvc5BitWidth& w)
  74 {
  75   if (isSigned)
  76   {
  77     BitVector base(w, 1U);
  78     BitVector shiftAmount(w, w - 1);
  79     BitVector result(base.leftShift(shiftAmount));
  80     return wrappedBitVector<true>(result);
  81   }
  82   else
  83   {
  84     return wrappedBitVector<false>::zero(w);
  85   }
  86 }
  87
  88 /*** Operators ***/
  89 template <bool isSigned>
  90 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<(
  91     const wrappedBitVector<isSigned>& op) const
  92 {
  93   return BitVector::leftShift(op);
  94 }
  95
  96 template <>
  97 wrappedBitVector<true> wrappedBitVector<true>::operator>>(
  98     const wrappedBitVector<true>& op) const
  99 {
 100   return BitVector::arithRightShift(op);
 101 }
 102
 103 template <>
 104 wrappedBitVector<false> wrappedBitVector<false>::operator>>(
 105     const wrappedBitVector<false>& op) const
 106 {
 107   return BitVector::logicalRightShift(op);
 108 }
 109
 110 template <bool isSigned>
 111 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
 112     const wrappedBitVector<isSigned>& op) const
 113 {
 114   return BitVector::operator|(op);
 115 }
 116
 117 template <bool isSigned>
 118 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
 119     const wrappedBitVector<isSigned>& op) const
 120 {
 121   return BitVector::operator&(op);
 122 }
 123
 124 template <bool isSigned>
 125 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
 126     const wrappedBitVector<isSigned>& op) const
 127 {
 128   return BitVector::operator+(op);
 129 }
 130
 131 template <bool isSigned>
 132 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
 133     const wrappedBitVector<isSigned>& op) const
 134 {
 135   return BitVector::operator-(op);
 136 }
 137
 138 template <bool isSigned>
 139 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
 140     const wrappedBitVector<isSigned>& op) const
 141 {
 142   return BitVector::operator*(op);
 143 }
 144
 145 template <>
 146 wrappedBitVector<false> wrappedBitVector<false>::operator/(
 147     const wrappedBitVector<false>& op) const
 148 {
 149   return BitVector::unsignedDivTotal(op);
 150 }
 151
 152 template <>
 153 wrappedBitVector<false> wrappedBitVector<false>::operator%(
 154     const wrappedBitVector<false>& op) const
 155 {
 156   return BitVector::unsignedRemTotal(op);
 157 }
 158
 159 template <bool isSigned>
 160 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
 161 {
 162   return BitVector::operator-();
 163 }
 164
 165 template <bool isSigned>
 166 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void) const
 167 {
 168   return BitVector::operator~();
 169 }
 170
 171 template <bool isSigned>
 172 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
 173 {
 174   return *this + wrappedBitVector<isSigned>::one(getWidth());
 175 }
 176
 177 template <bool isSigned>
 178 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
 179 {
 180   return *this - wrappedBitVector<isSigned>::one(getWidth());
 181 }
 182
 183 template <bool isSigned>
 184 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
 185     const wrappedBitVector<isSigned>& op) const
 186 {
 187   return BitVector::arithRightShift(BitVector(getWidth(), op));
 188 }
 189
 190 /*** Modular opertaions ***/
 191 // No overflow checking so these are the same as other operations
 192 template <bool isSigned>
 193 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift(
 194     const wrappedBitVector<isSigned>& op) const
 195 {
 196   return *this << op;
 197 }
 198
 199 template <bool isSigned>
 200 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift(
 201     const wrappedBitVector<isSigned>& op) const
 202 {
 203   return *this >> op;
 204 }
 205
 206 template <bool isSigned>
 207 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const
 208 {
 209   return increment();
 210 }
 211
 212 template <bool isSigned>
 213 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
 214 {
 215   return decrement();
 216 }
 217
 218 template <bool isSigned>
 219 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd(
 220     const wrappedBitVector<isSigned>& op) const
 221 {
 222   return *this + op;
 223 }
 224
 225 template <bool isSigned>
 226 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
 227 {
 228   return -(*this);
 229 }
 230
 231 /*** Comparisons ***/
 232
 233 template <bool isSigned>
 234 Cvc5Prop wrappedBitVector<isSigned>::operator==(
 235     const wrappedBitVector<isSigned>& op) const
 236 {
 237   return BitVector::operator==(op);
 238 }
 239
 240 template <>
 241 Cvc5Prop wrappedBitVector<true>::operator<=(
 242     const wrappedBitVector<true>& op) const
 243 {
 244   return signedLessThanEq(op);
 245 }
 246
 247 template <>
 248 Cvc5Prop wrappedBitVector<true>::operator>=(
 249     const wrappedBitVector<true>& op) const
 250 {
 251   return !(signedLessThan(op));
 252 }
 253
 254 template <>
 255 Cvc5Prop wrappedBitVector<true>::operator<(
 256     const wrappedBitVector<true>& op) const
 257 {
 258   return signedLessThan(op);
 259 }
 260
 261 template <>
 262 Cvc5Prop wrappedBitVector<true>::operator>(
 263     const wrappedBitVector<true>& op) const
 264 {
 265   return !(signedLessThanEq(op));
 266 }
 267
 268 template <>
 269 Cvc5Prop wrappedBitVector<false>::operator<=(
 270     const wrappedBitVector<false>& op) const
 271 {
 272   return unsignedLessThanEq(op);
 273 }
 274
 275 template <>
 276 Cvc5Prop wrappedBitVector<false>::operator>=(
 277     const wrappedBitVector<false>& op) const
 278 {
 279   return !(unsignedLessThan(op));
 280 }
 281
 282 template <>
 283 Cvc5Prop wrappedBitVector<false>::operator<(
 284     const wrappedBitVector<false>& op) const
 285 {
 286   return unsignedLessThan(op);
 287 }
 288
 289 template <>
 290 Cvc5Prop wrappedBitVector<false>::operator>(
 291     const wrappedBitVector<false>& op) const
 292 {
 293   return !(unsignedLessThanEq(op));
 294 }
 295
 296 /*** Type conversion ***/
 297
 298 // Node makes no distinction between signed and unsigned, thus ...
 299 template <bool isSigned>
 300 wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const
 301 {
 302   return wrappedBitVector<true>(*this);
 303 }
 304
 305 template <bool isSigned>
 306 wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const
 307 {
 308   return wrappedBitVector<false>(*this);
 309 }
 310
 311 /*** Bit hacks ***/
 312
 313 template <bool isSigned>
 314 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
 315     Cvc5BitWidth extension) const
 316 {
 317   if (isSigned)
 318   {
 319     return BitVector::signExtend(extension);
 320   }
 321   else
 322   {
 323     return BitVector::zeroExtend(extension);
 324   }
 325 }
 326
 327 template <bool isSigned>
 328 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
 329     Cvc5BitWidth reduction) const
 330 {
 331   Assert(getWidth() > reduction);
 332
 333   return extract((getWidth() - 1) - reduction, 0);
 334 }
 335
 336 template <bool isSigned>
 337 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize(
 338     Cvc5BitWidth newSize) const
 339 {
 340   Cvc5BitWidth width = getWidth();
 341
 342   if (newSize > width)
 343   {
 344     return extend(newSize - width);
 345   }
 346   else if (newSize < width)
 347   {
 348     return contract(width - newSize);
 349   }
 350   else
 351   {
 352     return *this;
 353   }
 354 }
 355
 356 template <bool isSigned>
 357 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
 358     const wrappedBitVector<isSigned>& op) const
 359 {
 360   Assert(getWidth() <= op.getWidth());
 361   return extend(op.getWidth() - getWidth());
 362 }
 363
 364 template <bool isSigned>
 365 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
 366     const wrappedBitVector<isSigned>& op) const
 367 {
 368   return BitVector::concat(op);
 369 }
 370
 371 // Inclusive of end points, thus if the same, extracts just one bit
 372 template <bool isSigned>
 373 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(
 374     Cvc5BitWidth upper, Cvc5BitWidth lower) const
 375 {
 376   Assert(upper >= lower);
 377   return BitVector::extract(upper, lower);
 378 }
 379
 380 // Explicit instantiation
 381 template class wrappedBitVector<true>;
 382 template class wrappedBitVector<false>;
 383
 384 traits::rm traits::RNE(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_EVEN; };
 385 traits::rm traits::RNA(void) { return ::cvc5::ROUND_NEAREST_TIES_TO_AWAY; };
 386 traits::rm traits::RTP(void) { return ::cvc5::ROUND_TOWARD_POSITIVE; };
 387 traits::rm traits::RTN(void) { return ::cvc5::ROUND_TOWARD_NEGATIVE; };
 388 traits::rm traits::RTZ(void) { return ::cvc5::ROUND_TOWARD_ZERO; };
 389 // This is a literal back-end so props are actually bools
 390 // so these can be handled in the same way as the internal assertions above
 391
 392 void traits::precondition(const traits::prop& p)
 393 {
 394   Assert(p);
 395   return;
 396 }
 397 void traits::postcondition(const traits::prop& p)
 398 {
 399   Assert(p);
 400   return;
 401 }
 402 void traits::invariant(const traits::prop& p)
 403 {
 404   Assert(p);
 405   return;
 406 }
 407 }  // namespace symfpuLiteral
 408 }  // namespace cvc5
 409 #endif