Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Aina Niemetz, Martin Brain, Mathias Preiner
       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                 :            :  * The class representing a floating-point format.
      14                 :            :  */
      15                 :            : #include "cvc5_public.h"
      16                 :            : 
      17                 :            : #ifndef CVC5__FLOATINGPOINT_SIZE_H
      18                 :            : #define CVC5__FLOATINGPOINT_SIZE_H
      19                 :            : 
      20                 :            : namespace cvc5::internal {
      21                 :            : 
      22                 :            : // Inline these!
      23                 :     365955 : inline bool validExponentSize(uint32_t e) { return e >= 2; }
      24                 :     365955 : inline bool validSignificandSize(uint32_t s) { return s >= 2; }
      25                 :            : 
      26                 :            : /**
      27                 :            :  * Floating point sorts are parameterised by two constants > 1 giving the
      28                 :            :  * width (in bits) of the exponent and significand (including the hidden bit).
      29                 :            :  * So, IEEE-754 single precision, a.k.a. float, is described as 8 24.
      30                 :            :  */
      31                 :            : class FloatingPointSize
      32                 :            : {
      33                 :            :  public:
      34                 :            :   /** Constructors. */
      35                 :            :   FloatingPointSize(uint32_t exp_size, uint32_t sig_size);
      36                 :            :   FloatingPointSize(const FloatingPointSize& old);
      37                 :            : 
      38                 :            :   /** Operator overload for equality comparison. */
      39                 :     267211 :   bool operator==(const FloatingPointSize& fps) const
      40                 :            :   {
      41 [ +  - ][ +  - ]:     267211 :     return (d_exp_size == fps.d_exp_size) && (d_sig_size == fps.d_sig_size);
      42                 :            :   }
      43                 :            : 
      44                 :            :   /** Implement the interface that symfpu uses for floating-point formats. */
      45                 :            : 
      46                 :            :   /** Get the exponent bit-width of this floating-point format. */
      47                 :   14783400 :   inline uint32_t exponentWidth(void) const { return d_exp_size; }
      48                 :            :   /** Get the significand bit-width of this floating-point format. */
      49                 :   23189200 :   inline uint32_t significandWidth(void) const { return d_sig_size; }
      50                 :            :   /**
      51                 :            :    * Get the bit-width of the packed representation of this floating-point
      52                 :            :    * format (= exponent + significand bit-width, convenience wrapper).
      53                 :            :    */
      54                 :     139905 :   inline uint32_t packedWidth(void) const
      55                 :            :   {
      56                 :     139905 :     return exponentWidth() + significandWidth();
      57                 :            :   }
      58                 :            :   /**
      59                 :            :    * Get the exponent bit-width of the packed representation of this
      60                 :            :    * floating-point format (= exponent bit-width).
      61                 :            :    */
      62                 :     139937 :   inline uint32_t packedExponentWidth(void) const { return exponentWidth(); }
      63                 :            :   /**
      64                 :            :    * Get the significand bit-width of the packed representation of this
      65                 :            :    * floating-point format (= significand bit-width - 1).
      66                 :            :    */
      67                 :     140245 :   inline uint32_t packedSignificandWidth(void) const
      68                 :            :   {
      69                 :     140245 :     return significandWidth() - 1;
      70                 :            :   }
      71                 :            : 
      72                 :            :  private:
      73                 :            :   /** Exponent bit-width. */
      74                 :            :   uint32_t d_exp_size;
      75                 :            :   /** Significand bit-width. */
      76                 :            :   uint32_t d_sig_size;
      77                 :            : 
      78                 :            : }; /* class FloatingPointSize */
      79                 :            : 
      80                 :            : /**
      81                 :            :  * Hash function for floating point formats.
      82                 :            :  */
      83                 :            : struct FloatingPointSizeHashFunction
      84                 :            : {
      85                 :     361257 :   static inline size_t ROLL(size_t X, size_t N)
      86                 :            :   {
      87                 :     361257 :     return (((X) << (N)) | ((X) >> (8 * sizeof((X)) - (N))));
      88                 :            :   }
      89                 :            : 
      90                 :     361257 :   inline size_t operator()(const FloatingPointSize& t) const
      91                 :            :   {
      92                 :     361257 :     return size_t(ROLL(t.exponentWidth(), 4 * sizeof(uint32_t))
      93                 :     361257 :                   | t.significandWidth());
      94                 :            :   }
      95                 :            : }; /* struct FloatingPointSizeHashFunction */
      96                 :            : }  // namespace cvc5::internal
      97                 :            : 
      98                 :            : #endif