Branch data     Line data    Source code

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