Branch data     Line data    Source code

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