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-2025 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                 :    3231410 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::one(
      25                 :            :     const Cvc5BitWidth& w)
      26                 :            : {
      27                 :    3231410 :   return wrappedBitVector<isSigned>(w, 1);
      28                 :            : }
      29                 :            : 
      30                 :            : template <bool isSigned>
      31                 :    1769191 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::zero(
      32                 :            :     const Cvc5BitWidth& w)
      33                 :            : {
      34                 :    1769191 :   return wrappedBitVector<isSigned>(w, 0);
      35                 :            : }
      36                 :            : 
      37                 :            : template <bool isSigned>
      38                 :     214617 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(
      39                 :            :     const Cvc5BitWidth& w)
      40                 :            : {
      41                 :     214617 :   return ~wrappedBitVector<isSigned>::zero(w);
      42                 :            : }
      43                 :            : 
      44                 :            : template <bool isSigned>
      45                 :     111860 : Cvc5Prop wrappedBitVector<isSigned>::isAllOnes() const
      46                 :            : {
      47                 :     111860 :   return (*this == wrappedBitVector<isSigned>::allOnes(getWidth()));
      48                 :            : }
      49                 :            : template <bool isSigned>
      50                 :     570591 : Cvc5Prop wrappedBitVector<isSigned>::isAllZeros() const
      51                 :            : {
      52                 :     570591 :   return (*this == wrappedBitVector<isSigned>::zero(getWidth()));
      53                 :            : }
      54                 :            : 
      55                 :            : template <bool isSigned>
      56                 :        498 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::maxValue(
      57                 :            :     const Cvc5BitWidth& w)
      58                 :            : {
      59                 :            :   if (isSigned)
      60                 :            :   {
      61                 :        498 :     BitVector base(w - 1, 0U);
      62                 :        498 :     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                 :        950 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::minValue(
      72                 :            :     const Cvc5BitWidth& w)
      73                 :            : {
      74                 :            :   if (isSigned)
      75                 :            :   {
      76                 :       1900 :     BitVector base(w, 1U);
      77                 :       1900 :     BitVector shiftAmount(w, w - 1);
      78                 :       1900 :     BitVector result(base.leftShift(shiftAmount));
      79                 :        950 :     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                 :    2459428 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<(
      90                 :            :     const wrappedBitVector<isSigned>& op) const
      91                 :            : {
      92                 :    2459428 :   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                 :      58958 : wrappedBitVector<false> wrappedBitVector<false>::operator>>(
     104                 :            :     const wrappedBitVector<false>& op) const
     105                 :            : {
     106                 :     117916 :   return BitVector::logicalRightShift(op);
     107                 :            : }
     108                 :            : 
     109                 :            : template <bool isSigned>
     110                 :      74120 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
     111                 :            :     const wrappedBitVector<isSigned>& op) const
     112                 :            : {
     113                 :            :   return static_cast<const BitVector&>(*this)
     114                 :      74120 :          | static_cast<const BitVector&>(op);
     115                 :            : }
     116                 :            : 
     117                 :            : template <bool isSigned>
     118                 :     514056 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
     119                 :            :     const wrappedBitVector<isSigned>& op) const
     120                 :            : {
     121                 :            :   return static_cast<const BitVector&>(*this)
     122                 :     514056 :          & static_cast<const BitVector&>(op);
     123                 :            : }
     124                 :            : 
     125                 :            : template <bool isSigned>
     126                 :     104863 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
     127                 :            :     const wrappedBitVector<isSigned>& op) const
     128                 :            : {
     129                 :            :   return static_cast<const BitVector&>(*this)
     130                 :     104863 :          + static_cast<const BitVector&>(op);
     131                 :            : }
     132                 :            : 
     133                 :            : template <bool isSigned>
     134                 :    3053533 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
     135                 :            :     const wrappedBitVector<isSigned>& op) const
     136                 :            : {
     137                 :            :   return static_cast<const BitVector&>(*this)
     138                 :    3053533 :          - static_cast<const BitVector&>(op);
     139                 :            : }
     140                 :            : 
     141                 :            : template <bool isSigned>
     142                 :      17886 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
     143                 :            :     const wrappedBitVector<isSigned>& op) const
     144                 :            : {
     145                 :            :   return static_cast<const BitVector&>(*this)
     146                 :      17886 :          * static_cast<const BitVector&>(op);
     147                 :            : }
     148                 :            : 
     149                 :            : template <>
     150                 :       2890 : wrappedBitVector<false> wrappedBitVector<false>::operator/(
     151                 :            :     const wrappedBitVector<false>& op) const
     152                 :            : {
     153                 :       5780 :   return BitVector::unsignedDivTotal(op);
     154                 :            : }
     155                 :            : 
     156                 :            : template <>
     157                 :       2890 : wrappedBitVector<false> wrappedBitVector<false>::operator%(
     158                 :            :     const wrappedBitVector<false>& op) const
     159                 :            : {
     160                 :       5780 :   return BitVector::unsignedRemTotal(op);
     161                 :            : }
     162                 :            : 
     163                 :            : template <bool isSigned>
     164                 :    1228523 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
     165                 :            : {
     166                 :    1228523 :   return -(static_cast<const BitVector&>(*this));
     167                 :            : }
     168                 :            : 
     169                 :            : template <bool isSigned>
     170                 :     257804 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void) const
     171                 :            : {
     172                 :     257804 :   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                 :     246845 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
     183                 :            : {
     184                 :     246845 :   return *this - wrappedBitVector<isSigned>::one(getWidth());
     185                 :            : }
     186                 :            : 
     187                 :            : template <bool isSigned>
     188                 :      19385 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
     189                 :            :     const wrappedBitVector<isSigned>& op) const
     190                 :            : {
     191                 :      19385 :   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                 :     296230 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularLeftShift(
     198                 :            :     const wrappedBitVector<isSigned>& op) const
     199                 :            : {
     200                 :     296230 :   return *this << op;
     201                 :            : }
     202                 :            : 
     203                 :            : template <bool isSigned>
     204                 :       5669 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift(
     205                 :            :     const wrappedBitVector<isSigned>& op) const
     206                 :            : {
     207                 :       5669 :   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                 :     221763 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
     218                 :            : {
     219                 :     221763 :   return decrement();
     220                 :            : }
     221                 :            : 
     222                 :            : template <bool isSigned>
     223                 :      30499 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd(
     224                 :            :     const wrappedBitVector<isSigned>& op) const
     225                 :            : {
     226                 :      30499 :   return *this + op;
     227                 :            : }
     228                 :            : 
     229                 :            : template <bool isSigned>
     230                 :      27973 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
     231                 :            : {
     232                 :      27973 :   return -(*this);
     233                 :            : }
     234                 :            : 
     235                 :            : /*** Comparisons ***/
     236                 :            : 
     237                 :            : template <bool isSigned>
     238                 :    1180476 : Cvc5Prop wrappedBitVector<isSigned>::operator==(
     239                 :            :     const wrappedBitVector<isSigned>& op) const
     240                 :            : {
     241                 :            :   return static_cast<const BitVector&>(*this)
     242                 :    1180476 :          == static_cast<const BitVector&>(op);
     243                 :            : }
     244                 :            : 
     245                 :            : template <>
     246                 :    1766120 : Cvc5Prop wrappedBitVector<true>::operator<=(
     247                 :            :     const wrappedBitVector<true>& op) const
     248                 :            : {
     249                 :    1766120 :   return signedLessThanEq(op);
     250                 :            : }
     251                 :            : 
     252                 :            : template <>
     253                 :      12658 : Cvc5Prop wrappedBitVector<true>::operator>=(
     254                 :            :     const wrappedBitVector<true>& op) const
     255                 :            : {
     256                 :      12658 :   return !(signedLessThan(op));
     257                 :            : }
     258                 :            : 
     259                 :            : template <>
     260                 :      63161 : Cvc5Prop wrappedBitVector<true>::operator<(
     261                 :            :     const wrappedBitVector<true>& op) const
     262                 :            : {
     263                 :      63161 :   return signedLessThan(op);
     264                 :            : }
     265                 :            : 
     266                 :            : template <>
     267                 :      34780 : Cvc5Prop wrappedBitVector<true>::operator>(
     268                 :            :     const wrappedBitVector<true>& op) const
     269                 :            : {
     270                 :      34780 :   return !(signedLessThanEq(op));
     271                 :            : }
     272                 :            : 
     273                 :            : template <>
     274                 :      14247 : Cvc5Prop wrappedBitVector<false>::operator<=(
     275                 :            :     const wrappedBitVector<false>& op) const
     276                 :            : {
     277                 :      14247 :   return unsignedLessThanEq(op);
     278                 :            : }
     279                 :            : 
     280                 :            : template <>
     281                 :      29028 : Cvc5Prop wrappedBitVector<false>::operator>=(
     282                 :            :     const wrappedBitVector<false>& op) const
     283                 :            : {
     284                 :      29028 :   return !(unsignedLessThan(op));
     285                 :            : }
     286                 :            : 
     287                 :            : template <>
     288                 :      12746 : Cvc5Prop wrappedBitVector<false>::operator<(
     289                 :            :     const wrappedBitVector<false>& op) const
     290                 :            : {
     291                 :      12746 :   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                 :      18789 : wrappedBitVector<true> wrappedBitVector<isSigned>::toSigned(void) const
     306                 :            : {
     307                 :      18789 :   return wrappedBitVector<true>(*this);
     308                 :            : }
     309                 :            : 
     310                 :            : template <bool isSigned>
     311                 :     308950 : wrappedBitVector<false> wrappedBitVector<isSigned>::toUnsigned(void) const
     312                 :            : {
     313                 :     308950 :   return wrappedBitVector<false>(*this);
     314                 :            : }
     315                 :            : 
     316                 :            : /*** Bit hacks ***/
     317                 :            : 
     318                 :            : template <bool isSigned>
     319                 :     818720 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
     320                 :            :     Cvc5BitWidth extension) const
     321                 :            : {
     322                 :            :   if (isSigned)
     323                 :            :   {
     324                 :     196259 :     return BitVector::signExtend(extension);
     325                 :            :   }
     326                 :            :   else
     327                 :            :   {
     328                 :     622461 :     return BitVector::zeroExtend(extension);
     329                 :            :   }
     330                 :            : }
     331                 :            : 
     332                 :            : template <bool isSigned>
     333                 :      18117 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
     334                 :            :     Cvc5BitWidth reduction) const
     335                 :            : {
     336 [ -  + ][ -  + ]:      18117 :   Assert(getWidth() > reduction);
                 [ -  - ]
     337                 :            : 
     338                 :      18117 :   return extract((getWidth() - 1) - reduction, 0);
     339                 :            : }
     340                 :            : 
     341                 :            : template <bool isSigned>
     342                 :     240023 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize(
     343                 :            :     Cvc5BitWidth newSize) const
     344                 :            : {
     345                 :     240023 :   Cvc5BitWidth width = getWidth();
     346                 :            : 
     347         [ +  + ]:     240023 :   if (newSize > width)
     348                 :            :   {
     349                 :     240011 :     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                 :     331666 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
     363                 :            :     const wrappedBitVector<isSigned>& op) const
     364                 :            : {
     365 [ -  + ][ -  + ]:     331666 :   Assert(getWidth() <= op.getWidth());
                 [ -  - ]
     366                 :     331666 :   return extend(op.getWidth() - getWidth());
     367                 :            : }
     368                 :            : 
     369                 :            : template <bool isSigned>
     370                 :     204763 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
     371                 :            :     const wrappedBitVector<isSigned>& op) const
     372                 :            : {
     373                 :     204763 :   return BitVector::concat(op);
     374                 :            : }
     375                 :            : 
     376                 :            : // Inclusive of end points, thus if the same, extracts just one bit
     377                 :            : template <bool isSigned>
     378                 :     574693 : wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(
     379                 :            :     Cvc5BitWidth upper, Cvc5BitWidth lower) const
     380                 :            : {
     381 [ -  + ][ -  + ]:     574693 :   Assert(upper >= lower);
                 [ -  - ]
     382                 :     574693 :   return BitVector::extract(upper, lower);
     383                 :            : }
     384                 :            : 
     385                 :            : // Explicit instantiation
     386                 :            : template class wrappedBitVector<true>;
     387                 :            : template class wrappedBitVector<false>;
     388                 :            : 
     389                 :      38618 : traits::rm traits::RNE(void)
     390                 :            : {
     391                 :      38618 :   return RoundingMode::ROUND_NEAREST_TIES_TO_EVEN;
     392                 :            : };
     393                 :      31474 : traits::rm traits::RNA(void)
     394                 :            : {
     395                 :      31474 :   return RoundingMode::ROUND_NEAREST_TIES_TO_AWAY;
     396                 :            : };
     397                 :      25896 : traits::rm traits::RTP(void) { return RoundingMode::ROUND_TOWARD_POSITIVE; };
     398                 :      34818 : traits::rm traits::RTN(void) { return RoundingMode::ROUND_TOWARD_NEGATIVE; };
     399                 :      20048 : 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                 :     568182 : void traits::precondition(const traits::prop& p)
     404                 :            : {
     405 [ -  + ][ -  + ]:     568182 :   Assert(p);
                 [ -  - ]
     406                 :     568182 :   return;
     407                 :            : }
     408                 :     142439 : void traits::postcondition(const traits::prop& p)
     409                 :            : {
     410 [ -  + ][ -  + ]:     142439 :   Assert(p);
                 [ -  - ]
     411                 :     142439 :   return;
     412                 :            : }
     413                 :     640611 : void traits::invariant(const traits::prop& p)
     414                 :            : {
     415 [ -  + ][ -  + ]:     640611 :   Assert(p);
                 [ -  - ]
     416                 :     640611 :   return;
     417                 :            : }
     418                 :            : }  // namespace symfpuLiteral
     419                 :            : }  // namespace cvc5::internal