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                 :  319807073 :   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                 :   19796403 :   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                 :  394023196 :   Rational(const Rational& q) : d_value(q.d_value) {}
      86                 :            : 
      87                 :            :   /**
      88                 :            :    * Constructs a canonical Rational from a numerator.
      89                 :            :    */
      90                 :  797454778 :   Rational(signed int n) : d_value((signed long int)n) {}
      91                 :    8586392 :   Rational(unsigned int n) : d_value((unsigned long int)n) {}
      92                 :     117741 :   Rational(signed long int n) : d_value(n) {}
      93                 :    2069768 :   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                 :   25367722 :   Rational(signed int n, signed int d) : d_value((signed long int)n)
     104                 :            :   {
     105                 :   25367722 :     d_value /= cln::cl_I(d);
     106                 :   25367722 :   }
     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                 :    3624501 :   Rational(const Integer& n, const Integer& d) : d_value(n.get_cl_I())
     126                 :            :   {
     127                 :    3624501 :     d_value /= d.get_cl_I();
     128                 :    3624501 :   }
     129                 :   37845500 :   Rational(const Integer& n) : d_value(n.get_cl_I()) {}
     130                 :            : 
     131                 : 1609522126 :   ~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                 :  206902029 :   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                 :   39517321 :   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                 :    1253360 :   Rational inverse() const { return Rational(cln::recip(d_value)); }
     161                 :            : 
     162                 :  185476000 :   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                 :  185476000 :     return cln::compare(d_value, x.d_value);
     167                 :            :   }
     168                 :            : 
     169                 :            :   int sgn() const;
     170                 :            : 
     171                 :   78391100 :   bool isZero() const { return cln::zerop(d_value); }
     172                 :            : 
     173                 :   27253300 :   bool isOne() const { return d_value == 1; }
     174                 :            : 
     175                 :      75418 :   bool isNegativeOne() const { return d_value == -1; }
     176                 :            : 
     177                 :     650034 :   Rational abs() const
     178                 :            :   {
     179         [ +  + ]:     650034 :     if (sgn() < 0)
     180                 :            :     {
     181                 :     131613 :       return -(*this);
     182                 :            :     }
     183                 :            :     else
     184                 :            :     {
     185                 :     518421 :       return *this;
     186                 :            :     }
     187                 :            :   }
     188                 :            : 
     189                 :  431950000 :   bool isIntegral() const { return cln::denominator(d_value) == 1; }
     190                 :            : 
     191                 :       7406 :   Integer floor() const { return Integer(cln::floor1(d_value)); }
     192                 :            : 
     193                 :    3507170 :   Integer ceiling() const { return Integer(cln::ceiling1(d_value)); }
     194                 :            : 
     195                 :          0 :   Rational floor_frac() const { return (*this) - Rational(floor()); }
     196                 :            : 
     197                 :  192739003 :   Rational& operator=(const Rational& x)
     198                 :            :   {
     199         [ +  + ]:  192739003 :     if (this == &x) return *this;
     200                 :  192739003 :     d_value = x.d_value;
     201                 :  192739003 :     return *this;
     202                 :            :   }
     203                 :            : 
     204                 :   24072600 :   Rational operator-() const { return Rational(-(d_value)); }
     205                 :            : 
     206                 :  768767249 :   bool operator==(const Rational& y) const { return d_value == y.d_value; }
     207                 :            : 
     208                 :  109729016 :   bool operator!=(const Rational& y) const { return d_value != y.d_value; }
     209                 :            : 
     210                 :    2300460 :   bool operator<(const Rational& y) const { return d_value < y.d_value; }
     211                 :            : 
     212                 :   59231000 :   bool operator<=(const Rational& y) const { return d_value <= y.d_value; }
     213                 :            : 
     214                 :     707416 :   bool operator>(const Rational& y) const { return d_value > y.d_value; }
     215                 :            : 
     216                 :     487256 :   bool operator>=(const Rational& y) const { return d_value >= y.d_value; }
     217                 :            : 
     218                 :   65479509 :   Rational operator+(const Rational& y) const
     219                 :            :   {
     220                 :  130959009 :     return Rational(d_value + y.d_value);
     221                 :            :   }
     222                 :     359582 :   Rational operator-(const Rational& y) const
     223                 :            :   {
     224                 :     719155 :     return Rational(d_value - y.d_value);
     225                 :            :   }
     226                 :            : 
     227                 :  236178009 :   Rational operator*(const Rational& y) const
     228                 :            :   {
     229                 :  472357009 :     return Rational(d_value * y.d_value);
     230                 :            :   }
     231                 :    5126232 :   Rational operator/(const Rational& y) const
     232                 :            :   {
     233                 :   10252412 :     return Rational(d_value / y.d_value);
     234                 :            :   }
     235                 :            : 
     236                 :   93082500 :   Rational& operator+=(const Rational& y)
     237                 :            :   {
     238                 :   93082500 :     d_value += y.d_value;
     239                 :   93082500 :     return (*this);
     240                 :            :   }
     241                 :            : 
     242                 :      34822 :   Rational& operator-=(const Rational& y)
     243                 :            :   {
     244                 :      34822 :     d_value -= y.d_value;
     245                 :      34822 :     return (*this);
     246                 :            :   }
     247                 :            : 
     248                 :    8137840 :   Rational& operator*=(const Rational& y)
     249                 :            :   {
     250                 :    8137840 :     d_value *= y.d_value;
     251                 :    8137840 :     return (*this);
     252                 :            :   }
     253                 :            : 
     254                 :       1959 :   Rational& operator/=(const Rational& y)
     255                 :            :   {
     256                 :       1959 :     d_value /= y.d_value;
     257                 :       1959 :     return (*this);
     258                 :            :   }
     259                 :            : 
     260                 :            :   /** Returns a string representing the rational in the given base. */
     261                 :     770469 :   std::string toString(int base = 10) const
     262                 :            :   {
     263                 :    1540934 :     cln::cl_print_flags flags;
     264                 :     770469 :     flags.rational_base = base;
     265                 :     770469 :     flags.rational_readably = false;
     266                 :    1540934 :     std::stringstream ss;
     267                 :     770469 :     print_rational(ss, flags, d_value);
     268                 :    1540934 :     return ss.str();
     269                 :            :   }
     270                 :            : 
     271                 :            :   /**
     272                 :            :    * Computes the hash of the rational from hashes of the numerator and the
     273                 :            :    * denominator.
     274                 :            :    */
     275                 :  219078000 :   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                 :  219078000 :   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 */