Branch data     Line data    Source code

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