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                 :            :  * Multiprecision rational constants; wraps a CLN multiprecision rational.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "cvc5_public.h"
      14                 :            : 
      15                 :            : #ifndef CVC5__RATIONAL_H
      16                 :            : #define CVC5__RATIONAL_H
      17                 :            : 
      18                 :            : #include <cln/dfloat.h>
      19                 :            : #include <cln/input.h>
      20                 :            : #include <cln/io.h>
      21                 :            : #include <cln/number_io.h>
      22                 :            : #include <cln/output.h>
      23                 :            : #include <cln/rational.h>
      24                 :            : #include <cln/rational_io.h>
      25                 :            : #include <cln/real.h>
      26                 :            : 
      27                 :            : #include <optional>
      28                 :            : #include <sstream>
      29                 :            : #include <string>
      30                 :            : 
      31                 :            : #include "base/exception.h"
      32                 :            : #include "util/integer.h"
      33                 :            : 
      34                 :            : namespace cvc5::internal {
      35                 :            : 
      36                 :            : /**
      37                 :            :  * A multi-precision rational constant.
      38                 :            :  * This stores the rational as a pair of multi-precision integers,
      39                 :            :  * one for the numerator and one for the denominator.
      40                 :            :  * The number is always stored so that the gcd of the numerator and denominator
      41                 :            :  * is 1.  (This is referred to as referred to as canonical form in GMP's
      42                 :            :  * literature.) A consequence is that that the numerator and denominator may be
      43                 :            :  * different than the values used to construct the Rational.
      44                 :            :  *
      45                 :            :  * NOTE: The correct way to create a Rational from an int is to use one of the
      46                 :            :  * int numerator/int denominator constructors with the denominator 1.  Trying
      47                 :            :  * to construct a Rational with a single int, e.g., Rational(0), will put you
      48                 :            :  * in danger of invoking the char* constructor, from whence you will segfault.
      49                 :            :  */
      50                 :            : 
      51                 :            : class Rational
      52                 :            : {
      53                 :            :  public:
      54                 :            :   /**
      55                 :            :    * Constructs a Rational from a cln::cl_RA object.
      56                 :            :    * Does a deep copy.
      57                 :            :    */
      58                 :  223845563 :   Rational(const cln::cl_RA& val) : d_value(val) {}
      59                 :            : 
      60                 :            :   /**
      61                 :            :    * Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
      62                 :            :    *
      63                 :            :    * @param dec a string encoding a decimal number in the format
      64                 :            :    * <code>[0-9]*\.[0-9]*</code>
      65                 :            :    */
      66                 :            :   static Rational fromDecimal(const std::string& dec);
      67                 :            : 
      68                 :            :   /** Constructs a rational with the value 0/1. */
      69                 :   26930378 :   Rational() : d_value(0) {}
      70                 :            :   /**
      71                 :            :    * Constructs a Rational from a C string in a given base (defaults to 10).
      72                 :            :    *
      73                 :            :    * Throws std::invalid_argument if the string is not a valid rational, i.e.,
      74                 :            :    * if it does not match sign{digit}+/sign{digit}+.
      75                 :            :    */
      76                 :            :   explicit Rational(const char* s, uint32_t base = 10);
      77                 :            :   Rational(const std::string& s, uint32_t base = 10);
      78                 :            : 
      79                 :            :   /**
      80                 :            :    * Creates a Rational from another Rational, q, by performing a deep copy.
      81                 :            :    */
      82                 :  323366422 :   Rational(const Rational& q) : d_value(q.d_value) {}
      83                 :            : 
      84                 :            :   /**
      85                 :            :    * Constructs a canonical Rational from a numerator.
      86                 :            :    */
      87                 :  651820225 :   Rational(signed int n) : d_value((signed long int)n) {}
      88                 :   14203575 :   Rational(unsigned int n) : d_value((unsigned long int)n) {}
      89                 :      68061 :   Rational(signed long int n) : d_value(n) {}
      90                 :    2210755 :   Rational(unsigned long int n) : d_value(n) {}
      91                 :            : 
      92                 :            : #ifdef CVC5_NEED_INT64_T_OVERLOADS
      93                 :            :   Rational(int64_t n) : d_value(n) {}
      94                 :            :   Rational(uint64_t n) : d_value(n) {}
      95                 :            : #endif /* CVC5_NEED_INT64_T_OVERLOADS */
      96                 :            : 
      97                 :            :   /**
      98                 :            :    * Constructs a canonical Rational from a numerator and denominator.
      99                 :            :    */
     100                 :   23122329 :   Rational(signed int n, signed int d) : d_value((signed long int)n)
     101                 :            :   {
     102                 :   23122329 :     d_value /= cln::cl_I(d);
     103                 :   23122329 :   }
     104                 :         15 :   Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n)
     105                 :            :   {
     106                 :         15 :     d_value /= cln::cl_I(d);
     107                 :         15 :   }
     108                 :        486 :   Rational(signed long int n, signed long int d) : d_value(n)
     109                 :            :   {
     110                 :        486 :     d_value /= cln::cl_I(d);
     111                 :        486 :   }
     112                 :          1 :   Rational(unsigned long int n, unsigned long int d) : d_value(n)
     113                 :            :   {
     114                 :          1 :     d_value /= cln::cl_I(d);
     115                 :          1 :   }
     116                 :            : 
     117                 :            : #ifdef CVC5_NEED_INT64_T_OVERLOADS
     118                 :            :   Rational(int64_t n, int64_t d) : d_value(n) { d_value /= cln::cl_I(d); }
     119                 :            :   Rational(uint64_t n, uint64_t d) : d_value(n) { d_value /= cln::cl_I(d); }
     120                 :            : #endif /* CVC5_NEED_INT64_T_OVERLOADS */
     121                 :            : 
     122                 :    3547504 :   Rational(const Integer& n, const Integer& d) : d_value(n.get_cl_I())
     123                 :            :   {
     124                 :    3547504 :     d_value /= d.get_cl_I();
     125                 :    3547504 :   }
     126                 :   31219139 :   Rational(const Integer& n) : d_value(n.get_cl_I()) {}
     127                 :            : 
     128                 : 1301197409 :   ~Rational() {}
     129                 :            : 
     130                 :            :   /**
     131                 :            :    * Returns a copy of d_value to enable public access of CLN data.
     132                 :            :    */
     133                 :            :   const cln::cl_RA& getValue() const { return d_value; }
     134                 :            : 
     135                 :            :   /**
     136                 :            :    * Returns the value of numerator of the Rational.
     137                 :            :    * Note that this makes a deep copy of the numerator.
     138                 :            :    */
     139                 :  216873801 :   Integer getNumerator() const { return Integer(cln::numerator(d_value)); }
     140                 :            : 
     141                 :            :   /**
     142                 :            :    * Returns the value of denominator of the Rational.
     143                 :            :    * Note that this makes a deep copy of the denominator.
     144                 :            :    */
     145                 :   39591533 :   Integer getDenominator() const { return Integer(cln::denominator(d_value)); }
     146                 :            : 
     147                 :            :   /** Return an exact rational for a double d. */
     148                 :            :   static std::optional<Rational> fromDouble(double d);
     149                 :            : 
     150                 :            :   /**
     151                 :            :    * Get a double representation of this Rational, which is
     152                 :            :    * approximate: truncation may occur, overflow may result in
     153                 :            :    * infinity, and underflow may result in zero.
     154                 :            :    */
     155                 :         92 :   double getDouble() const { return cln::double_approx(d_value); }
     156                 :            : 
     157                 :     804304 :   Rational inverse() const { return Rational(cln::recip(d_value)); }
     158                 :            : 
     159                 :  189964855 :   int cmp(const Rational& x) const
     160                 :            :   {
     161                 :            :     // Don't use mpq_class's cmp() function.
     162                 :            :     // The name ends up conflicting with this function.
     163                 :  189964855 :     return cln::compare(d_value, x.d_value);
     164                 :            :   }
     165                 :            : 
     166                 :            :   int sgn() const;
     167                 :            : 
     168                 :   68803510 :   bool isZero() const { return cln::zerop(d_value); }
     169                 :            : 
     170                 :   25457627 :   bool isOne() const { return d_value == 1; }
     171                 :            : 
     172                 :      70671 :   bool isNegativeOne() const { return d_value == -1; }
     173                 :            : 
     174                 :     731282 :   Rational abs() const
     175                 :            :   {
     176         [ +  + ]:     731282 :     if (sgn() < 0)
     177                 :            :     {
     178                 :     187143 :       return -(*this);
     179                 :            :     }
     180                 :            :     else
     181                 :            :     {
     182                 :     544139 :       return *this;
     183                 :            :     }
     184                 :            :   }
     185                 :            : 
     186                 :  438367374 :   bool isIntegral() const { return cln::denominator(d_value) == 1; }
     187                 :            : 
     188                 :       9732 :   Integer floor() const { return Integer(cln::floor1(d_value)); }
     189                 :            : 
     190                 :    3014700 :   Integer ceiling() const { return Integer(cln::ceiling1(d_value)); }
     191                 :            : 
     192                 :          0 :   Rational floor_frac() const { return (*this) - Rational(floor()); }
     193                 :            : 
     194                 :  151679538 :   Rational& operator=(const Rational& x)
     195                 :            :   {
     196         [ +  + ]:  151679538 :     if (this == &x) return *this;
     197                 :  151679536 :     d_value = x.d_value;
     198                 :  151679536 :     return *this;
     199                 :            :   }
     200                 :            : 
     201                 :   21220028 :   Rational operator-() const { return Rational(-(d_value)); }
     202                 :            : 
     203                 :  646535256 :   bool operator==(const Rational& y) const { return d_value == y.d_value; }
     204                 :            : 
     205                 :   75039475 :   bool operator!=(const Rational& y) const { return d_value != y.d_value; }
     206                 :            : 
     207                 :    2313785 :   bool operator<(const Rational& y) const { return d_value < y.d_value; }
     208                 :            : 
     209                 :   67375357 :   bool operator<=(const Rational& y) const { return d_value <= y.d_value; }
     210                 :            : 
     211                 :     689222 :   bool operator>(const Rational& y) const { return d_value > y.d_value; }
     212                 :            : 
     213                 :    1154540 :   bool operator>=(const Rational& y) const { return d_value >= y.d_value; }
     214                 :            : 
     215                 :   44647473 :   Rational operator+(const Rational& y) const
     216                 :            :   {
     217                 :   89294937 :     return Rational(d_value + y.d_value);
     218                 :            :   }
     219                 :     342893 :   Rational operator-(const Rational& y) const
     220                 :            :   {
     221                 :     685777 :     return Rational(d_value - y.d_value);
     222                 :            :   }
     223                 :            : 
     224                 :  164200417 :   Rational operator*(const Rational& y) const
     225                 :            :   {
     226                 :  328400825 :     return Rational(d_value * y.d_value);
     227                 :            :   }
     228                 :    3642614 :   Rational operator/(const Rational& y) const
     229                 :            :   {
     230                 :    7285216 :     return Rational(d_value / y.d_value);
     231                 :            :   }
     232                 :            : 
     233                 :   69042423 :   Rational& operator+=(const Rational& y)
     234                 :            :   {
     235                 :   69042423 :     d_value += y.d_value;
     236                 :   69042423 :     return (*this);
     237                 :            :   }
     238                 :            : 
     239                 :      43391 :   Rational& operator-=(const Rational& y)
     240                 :            :   {
     241                 :      43391 :     d_value -= y.d_value;
     242                 :      43391 :     return (*this);
     243                 :            :   }
     244                 :            : 
     245                 :    6965923 :   Rational& operator*=(const Rational& y)
     246                 :            :   {
     247                 :    6965923 :     d_value *= y.d_value;
     248                 :    6965923 :     return (*this);
     249                 :            :   }
     250                 :            : 
     251                 :       2167 :   Rational& operator/=(const Rational& y)
     252                 :            :   {
     253                 :       2167 :     d_value /= y.d_value;
     254                 :       2167 :     return (*this);
     255                 :            :   }
     256                 :            : 
     257                 :            :   /** Returns a string representing the rational in the given base. */
     258                 :    2125543 :   std::string toString(int base = 10) const
     259                 :            :   {
     260                 :    2125543 :     cln::cl_print_flags flags;
     261                 :    2125543 :     flags.rational_base = base;
     262                 :    2125543 :     flags.rational_readably = false;
     263                 :    2125543 :     std::stringstream ss;
     264                 :    2125543 :     print_rational(ss, flags, d_value);
     265                 :    4251086 :     return ss.str();
     266                 :    2125543 :   }
     267                 :            : 
     268                 :            :   /**
     269                 :            :    * Computes the hash of the rational from hashes of the numerator and the
     270                 :            :    * denominator.
     271                 :            :    */
     272                 :  223620994 :   size_t hash() const { return equal_hashcode(d_value); }
     273                 :            : 
     274                 :          0 :   uint32_t complexity() const
     275                 :            :   {
     276                 :          0 :     return getNumerator().length() + getDenominator().length();
     277                 :            :   }
     278                 :            : 
     279                 :            :   /** Equivalent to calling (this->abs()).cmp(b.abs()) */
     280                 :            :   int absCmp(const Rational& q) const;
     281                 :            : 
     282                 :            :  private:
     283                 :            :   /**
     284                 :            :    * Stores the value of the rational in a C++ CLN rational class.
     285                 :            :    */
     286                 :            :   cln::cl_RA d_value;
     287                 :            : 
     288                 :            : }; /* class Rational */
     289                 :            : 
     290                 :            : struct RationalHashFunction
     291                 :            : {
     292                 :  223620994 :   inline size_t operator()(const cvc5::internal::Rational& r) const
     293                 :            :   {
     294                 :  223620994 :     return r.hash();
     295                 :            :   }
     296                 :            : }; /* struct RationalHashFunction */
     297                 :            : 
     298                 :            : std::ostream& operator<<(std::ostream& os, const Rational& n);
     299                 :            : 
     300                 :            : }  // namespace cvc5::internal
     301                 :            : 
     302                 :            : #endif /* CVC5__RATIONAL_H */