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                 :            :  * !!! This header is only to be included in floating-point literal headers !!!
      13                 :            :  *
      14                 :            :  * This is a symfpu literal "back-end".  It allows the library to be used as
      15                 :            :  * an arbitrary precision floating-point implementation.  This is effectively
      16                 :            :  * the glue between symfpu's notion of "signed bit-vector" and cvc5's
      17                 :            :  * BitVector.
      18                 :            :  */
      19                 :            : 
      20                 :            : #include "cvc5_private.h"
      21                 :            : 
      22                 :            : #ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
      23                 :            : #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H
      24                 :            : 
      25                 :            : #include <symfpu/core/unpackedFloat.h>
      26                 :            : 
      27                 :            : #include "util/bitvector.h"
      28                 :            : #include "util/floatingpoint_size.h"
      29                 :            : #include "util/roundingmode.h"
      30                 :            : 
      31                 :            : /* -------------------------------------------------------------------------- */
      32                 :            : 
      33                 :            : namespace cvc5::internal {
      34                 :            : namespace symfpuLiteral {
      35                 :            : 
      36                 :            : /**
      37                 :            :  * Forward declaration of wrapper so that traits can be defined early and so
      38                 :            :  * used in the implementation of wrappedBitVector.
      39                 :            :  */
      40                 :            : template <bool T>
      41                 :            : class wrappedBitVector;
      42                 :            : 
      43                 :            : using Cvc5BitWidth = uint32_t;
      44                 :            : using Cvc5Prop = bool;
      45                 :            : using Cvc5RM = cvc5::internal::RoundingMode;
      46                 :            : using Cvc5FPSize = cvc5::internal::FloatingPointSize;
      47                 :            : using Cvc5UnsignedBitVector = wrappedBitVector<false>;
      48                 :            : using Cvc5SignedBitVector = wrappedBitVector<true>;
      49                 :            : 
      50                 :            : /**
      51                 :            :  * This is the template parameter for symfpu's templates.
      52                 :            :  */
      53                 :            : class traits
      54                 :            : {
      55                 :            :  public:
      56                 :            :   /** The six key types that symfpu uses. */
      57                 :            :   using bwt = Cvc5BitWidth;           // bit-width type
      58                 :            :   using prop = Cvc5Prop;              // boolean type
      59                 :            :   using rm = Cvc5RM;                  // rounding-mode type
      60                 :            :   using fpt = Cvc5FPSize;             // floating-point format type
      61                 :            :   using ubv = Cvc5UnsignedBitVector;  // unsigned bit-vector type
      62                 :            :   using sbv = Cvc5SignedBitVector;    // signed bit-vector type
      63                 :            : 
      64                 :            :   /** Give concrete instances of each rounding mode, mainly for comparisons. */
      65                 :            :   static rm RNE(void);
      66                 :            :   static rm RNA(void);
      67                 :            :   static rm RTP(void);
      68                 :            :   static rm RTN(void);
      69                 :            :   static rm RTZ(void);
      70                 :            : 
      71                 :            :   /** The sympfu properties. */
      72                 :            :   static void precondition(const prop& p);
      73                 :            :   static void postcondition(const prop& p);
      74                 :            :   static void invariant(const prop& p);
      75                 :            : };
      76                 :            : 
      77                 :            : /**
      78                 :            :  * Type function for mapping between types.
      79                 :            :  */
      80                 :            : template <bool T>
      81                 :            : struct signedToLiteralType;
      82                 :            : 
      83                 :            : template <>
      84                 :            : struct signedToLiteralType<true>
      85                 :            : {
      86                 :            :   using literalType = int32_t;
      87                 :            : };
      88                 :            : template <>
      89                 :            : struct signedToLiteralType<false>
      90                 :            : {
      91                 :            :   using literalType = uint32_t;
      92                 :            : };
      93                 :            : 
      94                 :            : /**
      95                 :            :  * This extends the interface for cvc5::internal::BitVector for compatibility
      96                 :            :  * with symFPU. The template parameter distinguishes signed and unsigned
      97                 :            :  * bit-vectors, a distinction symfpu uses.
      98                 :            :  */
      99                 :            : template <bool isSigned>
     100                 :            : class wrappedBitVector : public BitVector
     101                 :            : {
     102                 :            :  protected:
     103                 :            :   using literalType = typename signedToLiteralType<isSigned>::literalType;
     104                 :            :   friend wrappedBitVector<!isSigned>;  // To allow conversion between types
     105                 :            : 
     106                 :            :   friend ::symfpu::ite<Cvc5Prop, wrappedBitVector<isSigned> >;  // For ITE
     107                 :            : 
     108                 :            :  public:
     109                 :            :   /** Constructors. */
     110                 :    7487764 :   wrappedBitVector(const Cvc5BitWidth w, const uint32_t v) : BitVector(w, v) {}
     111         [ +  + ]:     128992 :   wrappedBitVector(const Cvc5Prop& p) : BitVector(1, p ? 1U : 0U) {}
     112                 :    9163969 :   wrappedBitVector(const BitVector& old) : BitVector(old) {}
     113                 :            : 
     114                 :            :   /** Get the bit-width of this wrapped bit-vector. */
     115                 :    5113099 :   Cvc5BitWidth getWidth(void) const { return getSize(); }
     116                 :            : 
     117                 :            :   /** Create a zero value of given bit-width 'w'. */
     118                 :            :   static wrappedBitVector<isSigned> one(const Cvc5BitWidth& w);
     119                 :            :   /** Create a one value of given bit-width 'w'. */
     120                 :            :   static wrappedBitVector<isSigned> zero(const Cvc5BitWidth& w);
     121                 :            :   /** Create a ones value (all bits 1) of given bit-width 'w'. */
     122                 :            :   static wrappedBitVector<isSigned> allOnes(const Cvc5BitWidth& w);
     123                 :            :   /** Create a maximum signed/unsigned value of given bit-width 'w'. */
     124                 :            :   static wrappedBitVector<isSigned> maxValue(const Cvc5BitWidth& w);
     125                 :            :   /** Create a minimum signed/unsigned value of given bit-width 'w'. */
     126                 :            :   static wrappedBitVector<isSigned> minValue(const Cvc5BitWidth& w);
     127                 :            : 
     128                 :            :   /** Return true if this a bit-vector representing a ones value. */
     129                 :            :   Cvc5Prop isAllOnes() const;
     130                 :            :   /** Return true if this a bit-vector representing a zero value. */
     131                 :            :   Cvc5Prop isAllZeros() const;
     132                 :            : 
     133                 :            :   /** Left shift. */
     134                 :            :   wrappedBitVector<isSigned> operator<<(
     135                 :            :       const wrappedBitVector<isSigned>& op) const;
     136                 :            :   /** Logical (unsigned) and arithmetic (signed) right shift. */
     137                 :            :   wrappedBitVector<isSigned> operator>>(
     138                 :            :       const wrappedBitVector<isSigned>& op) const;
     139                 :            : 
     140                 :            :   /**
     141                 :            :    * Inherited but ...
     142                 :            :    * *sigh* if we use the inherited version then it will return a
     143                 :            :    * cvc5::internal::BitVector which can be converted back to a
     144                 :            :    * wrappedBitVector<isSigned> but isn't done automatically when working
     145                 :            :    * out types for templates instantiation.  ITE is a particular
     146                 :            :    * problem as expressions and constants no longer derive the
     147                 :            :    * same type.  There aren't any good solutions in C++, we could
     148                 :            :    * use CRTP but Liana wouldn't appreciate that, so the following
     149                 :            :    * pointless wrapping functions are needed.
     150                 :            :    */
     151                 :            : 
     152                 :            :   /** Bit-wise or. */
     153                 :            :   wrappedBitVector<isSigned> operator|(
     154                 :            :       const wrappedBitVector<isSigned>& op) const;
     155                 :            :   /** Bit-wise and. */
     156                 :            :   wrappedBitVector<isSigned> operator&(
     157                 :            :       const wrappedBitVector<isSigned>& op) const;
     158                 :            :   /** Bit-vector addition. */
     159                 :            :   wrappedBitVector<isSigned> operator+(
     160                 :            :       const wrappedBitVector<isSigned>& op) const;
     161                 :            :   /** Bit-vector subtraction. */
     162                 :            :   wrappedBitVector<isSigned> operator-(
     163                 :            :       const wrappedBitVector<isSigned>& op) const;
     164                 :            :   /** Bit-vector multiplication. */
     165                 :            :   wrappedBitVector<isSigned> operator*(
     166                 :            :       const wrappedBitVector<isSigned>& op) const;
     167                 :            :   /** Bit-vector signed/unsigned division. */
     168                 :            :   wrappedBitVector<isSigned> operator/(
     169                 :            :       const wrappedBitVector<isSigned>& op) const;
     170                 :            :   /** Bit-vector signed/unsigned remainder. */
     171                 :            :   wrappedBitVector<isSigned> operator%(
     172                 :            :       const wrappedBitVector<isSigned>& op) const;
     173                 :            :   /** Bit-vector negation. */
     174                 :            :   wrappedBitVector<isSigned> operator-(void) const;
     175                 :            :   /** Bit-wise not. */
     176                 :            :   wrappedBitVector<isSigned> operator~(void) const;
     177                 :            : 
     178                 :            :   /** Bit-vector increment. */
     179                 :            :   wrappedBitVector<isSigned> increment() const;
     180                 :            :   /** Bit-vector decrement. */
     181                 :            :   wrappedBitVector<isSigned> decrement() const;
     182                 :            :   /**
     183                 :            :    * Bit-vector logical/arithmetic right shift where 'op' extended to the
     184                 :            :    * bit-width of this wrapped bit-vector.
     185                 :            :    */
     186                 :            :   wrappedBitVector<isSigned> signExtendRightShift(
     187                 :            :       const wrappedBitVector<isSigned>& op) const;
     188                 :            : 
     189                 :            :   /**
     190                 :            :    * Modular operations.
     191                 :            :    * Note: No overflow checking so these are the same as other operations.
     192                 :            :    */
     193                 :            :   wrappedBitVector<isSigned> modularLeftShift(
     194                 :            :       const wrappedBitVector<isSigned>& op) const;
     195                 :            :   wrappedBitVector<isSigned> modularRightShift(
     196                 :            :       const wrappedBitVector<isSigned>& op) const;
     197                 :            :   wrappedBitVector<isSigned> modularIncrement() const;
     198                 :            :   wrappedBitVector<isSigned> modularDecrement() const;
     199                 :            :   wrappedBitVector<isSigned> modularAdd(
     200                 :            :       const wrappedBitVector<isSigned>& op) const;
     201                 :            :   wrappedBitVector<isSigned> modularSubtract(
     202                 :            :       const wrappedBitVector<isSigned>& op) const;
     203                 :            :   wrappedBitVector<isSigned> modularNegate() const;
     204                 :            : 
     205                 :            :   /** Bit-vector equality. */
     206                 :            :   Cvc5Prop operator==(const wrappedBitVector<isSigned>& op) const;
     207                 :            :   /** Bit-vector signed/unsigned less or equal than. */
     208                 :            :   Cvc5Prop operator<=(const wrappedBitVector<isSigned>& op) const;
     209                 :            :   /** Bit-vector sign/unsigned greater or equal than. */
     210                 :            :   Cvc5Prop operator>=(const wrappedBitVector<isSigned>& op) const;
     211                 :            :   /** Bit-vector signed/unsigned less than. */
     212                 :            :   Cvc5Prop operator<(const wrappedBitVector<isSigned>& op) const;
     213                 :            :   /** Bit-vector sign/unsigned greater or equal than. */
     214                 :            :   Cvc5Prop operator>(const wrappedBitVector<isSigned>& op) const;
     215                 :            : 
     216                 :            :   /** Convert this bit-vector to a signed bit-vector. */
     217                 :            :   wrappedBitVector<true> toSigned(void) const;
     218                 :            :   /** Convert this bit-vector to an unsigned bit-vector. */
     219                 :            :   wrappedBitVector<false> toUnsigned(void) const;
     220                 :            : 
     221                 :            :   /** Bit-vector signed/unsigned (zero) extension. */
     222                 :            :   wrappedBitVector<isSigned> extend(Cvc5BitWidth extension) const;
     223                 :            : 
     224                 :            :   /**
     225                 :            :    * Create a "contracted" bit-vector by cutting off the 'reduction' number of
     226                 :            :    * most significant bits, i.e., by extracting the (bit-width - reduction)
     227                 :            :    * least significant bits.
     228                 :            :    */
     229                 :            :   wrappedBitVector<isSigned> contract(Cvc5BitWidth reduction) const;
     230                 :            : 
     231                 :            :   /**
     232                 :            :    * Create a "resized" bit-vector of given size bei either extending (if new
     233                 :            :    * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
     234                 :            :    */
     235                 :            :   wrappedBitVector<isSigned> resize(Cvc5BitWidth newSize) const;
     236                 :            : 
     237                 :            :   /**
     238                 :            :    * Create an extension of this bit-vector that matches the bit-width of the
     239                 :            :    * given bit-vector.
     240                 :            :    *
     241                 :            :    * Note: The size of the given bit-vector may not be larger than the size of
     242                 :            :    *       this bit-vector.
     243                 :            :    */
     244                 :            :   wrappedBitVector<isSigned> matchWidth(
     245                 :            :       const wrappedBitVector<isSigned>& op) const;
     246                 :            : 
     247                 :            :   /** Bit-vector concatenation. */
     248                 :            :   wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
     249                 :            : 
     250                 :            :   /** Inclusive of end points, thus if the same, extracts just one bit. */
     251                 :            :   wrappedBitVector<isSigned> extract(Cvc5BitWidth upper,
     252                 :            :                                      Cvc5BitWidth lower) const;
     253                 :            : };
     254                 :            : }  // namespace symfpuLiteral
     255                 :            : }  // namespace cvc5::internal
     256                 :            : 
     257                 :            : #endif