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                 :            :  * Base class for floating-point literal implementations.
      11                 :            :  */
      12                 :            : 
      13                 :            : #ifndef CVC5__UTIL__FLOATINGPOINT_LITERAL_H
      14                 :            : #define CVC5__UTIL__FLOATINGPOINT_LITERAL_H
      15                 :            : 
      16                 :            : #include <memory>
      17                 :            : #include <utility>
      18                 :            : 
      19                 :            : #include "util/bitvector.h"
      20                 :            : #include "util/floatingpoint_size.h"
      21                 :            : #include "util/rational.h"
      22                 :            : #include "util/roundingmode.h"
      23                 :            : 
      24                 :            : /* -------------------------------------------------------------------------- */
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : 
      28                 :            : class FloatingPointLiteral
      29                 :            : {
      30                 :            :  public:
      31                 :            :   /**
      32                 :            :    * The kind of floating-point special constants that can be created via the
      33                 :            :    * corresponding constructor.
      34                 :            :    * These are prefixed with FP because of name clashes with NAN.
      35                 :            :    */
      36                 :            :   enum SpecialConstKind
      37                 :            :   {
      38                 :            :     FPINF,   // +-oo
      39                 :            :     FPNAN,   // NaN
      40                 :            :     FPZERO,  // +-zero
      41                 :            :   };
      42                 :            : 
      43                 :            :   /**
      44                 :            :    * Get the number of exponent bits in the unpacked format corresponding to a
      45                 :            :    * given packed format.  This is the unpacked counter-part of
      46                 :            :    * FloatingPointSize::exponentWidth().
      47                 :            :    */
      48                 :            :   static uint32_t getUnpackedExponentWidth(FloatingPointSize& size);
      49                 :            :   /**
      50                 :            :    * Get the number of exponent bits in the unpacked format corresponding to a
      51                 :            :    * given packed format.  This is the unpacked counter-part of
      52                 :            :    * FloatingPointSize::significandWidth().
      53                 :            :    */
      54                 :            :   static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size);
      55                 :            : 
      56                 :            :   /**
      57                 :            :    * Create a FP literal from its IEEE bit-vector representation.
      58                 :            :    * @param exp_size The exponent size.
      59                 :            :    * @param sig_size The significand size.
      60                 :            :    * @param The bit-vector representation.
      61                 :            :    */
      62                 :            :   static std::unique_ptr<FloatingPointLiteral> create(uint32_t exp_size,
      63                 :            :                                                       uint32_t sig_size,
      64                 :            :                                                       const BitVector& bv);
      65                 :            :   /**
      66                 :            :    * Create a FP literal from its IEEE bit-vector representation.
      67                 :            :    * @param size The floating-point format.
      68                 :            :    * @param The bit-vector representation.
      69                 :            :    */
      70                 :            :   static std::unique_ptr<FloatingPointLiteral> create(
      71                 :            :       const FloatingPointSize& size, const BitVector& bv);
      72                 :            : 
      73                 :            :   /**
      74                 :            :    * Create a FP literal that represents a special constant.
      75                 :            :    * @param size The floating-point format.
      76                 :            :    * @param kind The special constant kind.
      77                 :            :    */
      78                 :            :   static std::unique_ptr<FloatingPointLiteral> create(
      79                 :            :       const FloatingPointSize& size, SpecialConstKind kind);
      80                 :            :   /**
      81                 :            :    * Create a FP literal that represents a special constant.
      82                 :            :    * @param size The floating-point format.
      83                 :            :    * @param kind The special constant kind.
      84                 :            :    */
      85                 :            :   static std::unique_ptr<FloatingPointLiteral> create(
      86                 :            :       const FloatingPointSize& size, SpecialConstKind kind, bool sign);
      87                 :            : 
      88                 :            :   /**
      89                 :            :    * Create a FP literal from a signed or unsigned bit-vector value with
      90                 :            :    * respect to given rounding mode.
      91                 :            :    */
      92                 :            :   static std::unique_ptr<FloatingPointLiteral> create(
      93                 :            :       const FloatingPointSize& size,
      94                 :            :       const RoundingMode& rm,
      95                 :            :       const BitVector& bv,
      96                 :            :       bool signedBV);
      97                 :            : 
      98                 :            :   /**
      99                 :            :    * Create a FP literal from a rational value with respect to given rounding
     100                 :            :    * mode.
     101                 :            :    */
     102                 :            :   static std::unique_ptr<FloatingPointLiteral> createFromRational(
     103                 :            :       const FloatingPointSize& size, const RoundingMode& rm, const Rational& r);
     104                 :            : 
     105                 :            :   /**
     106                 :            :    * Constructor.
     107                 :            :    * @param exp_size The exponent size.
     108                 :            :    * @param sig_size The significand size.
     109                 :            :    */
     110                 :       6074 :   FloatingPointLiteral(uint32_t exp_size, uint32_t sig_size)
     111                 :       6074 :       : d_fp_size(exp_size, sig_size)
     112                 :            :   {
     113                 :       6074 :   }
     114                 :            :   /**
     115                 :            :    * Constructor.
     116                 :            :    * @param size The floating-point format.
     117                 :            :    */
     118                 :      42624 :   FloatingPointLiteral(const FloatingPointSize& size) : d_fp_size(size) {}
     119                 :            : 
     120                 :            :   /** Destructor. */
     121                 :            :   virtual ~FloatingPointLiteral();
     122                 :            : 
     123                 :            :   /** Clone this literal (polymorphic copy). */
     124                 :            :   virtual std::unique_ptr<FloatingPointLiteral> clone() const = 0;
     125                 :            : 
     126                 :            :   /** @return The packed (IEEE-754) representation of this literal. */
     127                 :            :   virtual BitVector pack() const = 0;
     128                 :            : 
     129                 :            :   /** @return The absolute value of this floating-point. */
     130                 :            :   virtual std::unique_ptr<FloatingPointLiteral> absolute() const = 0;
     131                 :            :   /** @return The negation of this floating-point. */
     132                 :            :   virtual std::unique_ptr<FloatingPointLiteral> negate() const = 0;
     133                 :            :   /**
     134                 :            :    * Floating-point addition.
     135                 :            :    * @param rm  The rounding mode.
     136                 :            :    * @param arg The floating-point to add to this.
     137                 :            :    * @return The floating-point addition of this and `arg`.
     138                 :            :    */
     139                 :            :   virtual std::unique_ptr<FloatingPointLiteral> add(
     140                 :            :       const RoundingMode& rm, const FloatingPointLiteral& arg) const = 0;
     141                 :            :   /**
     142                 :            :    * Floating-point subtraction.
     143                 :            :    * @param rm  The rounding mode.
     144                 :            :    * @param arg The floating-point to subtract from this.
     145                 :            :    * @return The floating-point subtraction of this and `arg`.
     146                 :            :    */
     147                 :            :   virtual std::unique_ptr<FloatingPointLiteral> sub(
     148                 :            :       const RoundingMode& rm, const FloatingPointLiteral& arg) const = 0;
     149                 :            :   /**
     150                 :            :    * Floating-point multiplication.
     151                 :            :    * @param rm  The rounding mode.
     152                 :            :    * @param arg The floating-point to multiply with this.
     153                 :            :    * @return The floating-point multiplication of this and `arg`.
     154                 :            :    */
     155                 :            :   virtual std::unique_ptr<FloatingPointLiteral> mult(
     156                 :            :       const RoundingMode& rm, const FloatingPointLiteral& arg) const = 0;
     157                 :            :   /**
     158                 :            :    * Floating-point division.
     159                 :            :    * @param rm  The rounding mode.
     160                 :            :    * @param arg The floating-point to divide this by.
     161                 :            :    * @return The floating-point division of this and `arg`.
     162                 :            :    */
     163                 :            :   virtual std::unique_ptr<FloatingPointLiteral> div(
     164                 :            :       const RoundingMode& rm, const FloatingPointLiteral& arg) const = 0;
     165                 :            :   /**
     166                 :            :    * Floating-point fused multiplication and addition.
     167                 :            :    * @param rm   The rounding mode.
     168                 :            :    * @param arg1 The floating-point to multiply to this.
     169                 :            :    * @param arg2 The floating-point to add to the multiplication.
     170                 :            :    * @return The floating-point fused multiplication and addition result.
     171                 :            :    */
     172                 :            :   virtual std::unique_ptr<FloatingPointLiteral> fma(
     173                 :            :       const RoundingMode& rm,
     174                 :            :       const FloatingPointLiteral& arg1,
     175                 :            :       const FloatingPointLiteral& arg2) const = 0;
     176                 :            :   /**
     177                 :            :    * Floating-point square root.
     178                 :            :    * @param rm The rounding mode.
     179                 :            :    * @return The floating-point sqare root of this.
     180                 :            :    */
     181                 :            :   virtual std::unique_ptr<FloatingPointLiteral> sqrt(
     182                 :            :       const RoundingMode& rm) const = 0;
     183                 :            :   /**
     184                 :            :    * Floating-point round to integral.
     185                 :            :    * @param rm The rounding mode.
     186                 :            :    * @return The floating-point round-to-integral of this.
     187                 :            :    */
     188                 :            :   virtual std::unique_ptr<FloatingPointLiteral> rti(
     189                 :            :       const RoundingMode& rm) const = 0;
     190                 :            :   /**
     191                 :            :    * Floating-point remainder.
     192                 :            :    * @param arg The floating-point to divide this by.
     193                 :            :    * @return The floating-point remainder of this and `arg`.
     194                 :            :    */
     195                 :            :   virtual std::unique_ptr<FloatingPointLiteral> rem(
     196                 :            :       const FloatingPointLiteral& arg) const = 0;
     197                 :            : 
     198                 :            :   /**
     199                 :            :    * Floating-point max (total version).
     200                 :            :    * @param arg      The floating-point to compare this with.
     201                 :            :    * @param zeroCase True to return the left (rather than the right operand) in
     202                 :            :    *                 case of max(-0,+0) or max(+0,-0).
     203                 :            :    * @return The floating-point max of this and `arg`.
     204                 :            :    */
     205                 :            :   virtual std::unique_ptr<FloatingPointLiteral> maxTotal(
     206                 :            :       const FloatingPointLiteral& arg, bool zeroCaseLeft) const = 0;
     207                 :            :   /**
     208                 :            :    * Floating-point min (total version).
     209                 :            :    * @param arg      The floating-point to compare this with.
     210                 :            :    * @param zeroCase True to return the left (rather than the right operand) in
     211                 :            :    *                 case of min(-0,+0) or min(+0,-0).
     212                 :            :    * @return The floating-point min of this and `arg`.
     213                 :            :    */
     214                 :            :   virtual std::unique_ptr<FloatingPointLiteral> minTotal(
     215                 :            :       const FloatingPointLiteral& arg, bool zeroCaseLeft) const = 0;
     216                 :            : 
     217                 :            :   /** Equality (NOT: fp.eq but =) over floating-point values. */
     218                 :            :   virtual bool operator==(const FloatingPointLiteral& fp) const = 0;
     219                 :            :   /** Floating-point less or equal than. */
     220                 :            :   virtual bool operator<=(const FloatingPointLiteral& arg) const = 0;
     221                 :            :   /** Floating-point less than. */
     222                 :            :   virtual bool operator<(const FloatingPointLiteral& arg) const = 0;
     223                 :            : 
     224                 :            :   /**
     225                 :            :    * Get the unpacked representation of the exponent (as used by SymFPU) of this
     226                 :            :    * floating-point value.
     227                 :            :    * @note This is only required for constant-folding of floating-point variable
     228                 :            :    *       components, as required by model generation (see #1915).
     229                 :            :    */
     230                 :            :   virtual BitVector getUnpackedExponent() const = 0;
     231                 :            :   /**
     232                 :            :    * Get the unpacked representation of the significand (as used by SymFPU) of
     233                 :            :    * this floating-point value.
     234                 :            :    * @note This is only required for constant-folding of floating-point variable
     235                 :            :    *       components, as required by model generation (see #1915).
     236                 :            :    */
     237                 :            :   virtual BitVector getUnpackedSignificand() const = 0;
     238                 :            :   /** True if this value is a negative value. */
     239                 :            :   virtual bool getSign() const = 0;
     240                 :            : 
     241                 :            :   /** Return true if this represents a normal value. */
     242                 :            :   virtual bool isNormal() const = 0;
     243                 :            :   /** Return true if this represents a subnormal value. */
     244                 :            :   virtual bool isSubnormal() const = 0;
     245                 :            :   /** Return true if this represents a zero value. */
     246                 :            :   virtual bool isZero() const = 0;
     247                 :            :   /** Return true if this represents an infinite value. */
     248                 :            :   virtual bool isInfinite() const = 0;
     249                 :            :   /** Return true if this represents a NaN value. */
     250                 :            :   virtual bool isNaN() const = 0;
     251                 :            :   /** Return true if this represents a negative value. */
     252                 :            :   virtual bool isNegative() const = 0;
     253                 :            :   /** Return true if this represents a positive value. */
     254                 :            :   virtual bool isPositive() const = 0;
     255                 :            : 
     256                 :            :   /**
     257                 :            :    * Convert this floating-point to a floating-point of given size, with
     258                 :            :    * respect to given rounding mode.
     259                 :            :    */
     260                 :            :   virtual std::unique_ptr<FloatingPointLiteral> convert(
     261                 :            :       const FloatingPointSize& target, const RoundingMode& rm) const = 0;
     262                 :            : 
     263                 :            :   /**
     264                 :            :    * Convert this floating-point to a signed bit-vector of given size,
     265                 :            :    * with respect to given rounding mode (total version).
     266                 :            :    * @param width The size of the target bit-vector.
     267                 :            :    * @param rm    The rounding mode.
     268                 :            :    * @returns The converted result, and `undefinedCase` in the undefined case.
     269                 :            :    */
     270                 :            :   virtual BitVector convertToSBVTotal(BitVectorSize width,
     271                 :            :                                       const RoundingMode& rm,
     272                 :            :                                       BitVector undefinedCase) const = 0;
     273                 :            :   /**
     274                 :            :    * Convert this floating-point to an unsigned bit-vector of given
     275                 :            :    * size, with respect to given rounding mode (total version).
     276                 :            :    * @param width The size of the target bit-vector.
     277                 :            :    * @param rm    The rounding mode.
     278                 :            :    * @returns The converted result, and `undefinedCase` in the undefined case.
     279                 :            :    */
     280                 :            :   virtual BitVector convertToUBVTotal(BitVectorSize width,
     281                 :            :                                       const RoundingMode& rm,
     282                 :            :                                       BitVector undefinedCase) const = 0;
     283                 :            : 
     284                 :            :   /**
     285                 :            :    * Convert this floating-point to a rational.
     286                 :            :    * @returns A pair of Rational and bool. The boolean flag is true if the
     287                 :            :    *          result is defined (i.e., the value is not NaN or infinite), and
     288                 :            :    *          false otherwise.
     289                 :            :    */
     290                 :            :   virtual std::pair<Rational, bool> convertToRational() const = 0;
     291                 :            : 
     292                 :            :   /** Return the size of this floating-point. */
     293                 :     104992 :   const FloatingPointSize& getSize() const { return d_fp_size; };
     294                 :            : 
     295                 :            :  protected:
     296                 :            :   /** The floating-point size of this floating-point literal. */
     297                 :            :   FloatingPointSize d_fp_size;
     298                 :            : };
     299                 :            : 
     300                 :            : /* -------------------------------------------------------------------------- */
     301                 :            : 
     302                 :            : }  // namespace cvc5::internal
     303                 :            : #endif