1 /********************* */ 2 /*! \file rational_cln_imp.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Tim King, Morgan Deters, Christopher L. Conway 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 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.\endverbatim 11 ** 12 ** \brief Multiprecision rational constants; wraps a CLN multiprecision 13 ** rational. 14 ** 15 ** Multiprecision rational constants; wraps a CLN multiprecision rational. 16 **/ 17 18 #include "cvc4_public.h" 19 20 #ifndef __CVC4__RATIONAL_H 21 #define __CVC4__RATIONAL_H 22 23 #include <gmp.h> 24 #include <string> 25 #include <sstream> 26 #include <cassert> 27 #include <cln/rational.h> 28 #include <cln/input.h> 29 #include <cln/io.h> 30 #include <cln/output.h> 31 #include <cln/rational_io.h> 32 #include <cln/number_io.h> 33 #include <cln/dfloat.h> 34 #include <cln/real.h> 35 36 #include "base/exception.h" 37 #include "util/integer.h" 38 #include "util/maybe.h" 39 40 namespace CVC4 { 41 42 /** 43 ** A multi-precision rational constant. 44 ** This stores the rational as a pair of multi-precision integers, 45 ** one for the numerator and one for the denominator. 46 ** The number is always stored so that the gcd of the numerator and denominator 47 ** is 1. (This is referred to as referred to as canonical form in GMP's 48 ** literature.) A consequence is that that the numerator and denominator may be 49 ** different than the values used to construct the Rational. 50 ** 51 ** NOTE: The correct way to create a Rational from an int is to use one of the 52 ** int numerator/int denominator constructors with the denominator 1. Trying 53 ** to construct a Rational with a single int, e.g., Rational(0), will put you 54 ** in danger of invoking the char* constructor, from whence you will segfault. 55 **/ 56 57 class CVC4_PUBLIC Rational { 58 private: 59 /** 60 * Stores the value of the rational is stored in a C++ GMP rational class. 61 * Using this instead of mpq_t allows for easier destruction. 62 */ 63 cln::cl_RA d_value; 64 65 /** 66 * Constructs a Rational from a mpq_class object. 67 * Does a deep copy. 68 * Assumes that the value is in canonical form, and thus does not 69 * have to call canonicalize() on the value. 70 */ 71 //Rational(const mpq_class& val) : d_value(val) { } Rational(const cln::cl_RA & val)72 Rational(const cln::cl_RA& val) : d_value(val) { } 73 74 public: 75 76 /** 77 * Creates a rational from a decimal string (e.g., <code>"1.5"</code>). 78 * 79 * @param dec a string encoding a decimal number in the format 80 * <code>[0-9]*\.[0-9]*</code> 81 */ 82 static Rational fromDecimal(const std::string& dec); 83 84 /** Constructs a rational with the value 0/1. */ Rational()85 Rational() : d_value(0){ 86 } 87 /** 88 * Constructs a Rational from a C string in a given base (defaults to 10). 89 * 90 * Throws std::invalid_argument if the string is not a valid rational. 91 * For more information about what is a valid rational string, 92 * see GMP's documentation for mpq_set_str(). 93 */ 94 explicit Rational(const char* s, unsigned base = 10) 95 { 96 cln::cl_read_flags flags; 97 98 flags.syntax = cln::syntax_rational; 99 flags.lsyntax = cln::lsyntax_standard; 100 flags.rational_base = base; 101 try{ 102 d_value = read_rational(flags, s, NULL, NULL); catch(...)103 }catch(...){ 104 std::stringstream ss; 105 ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base; 106 throw std::invalid_argument(ss.str()); 107 } 108 } 109 Rational(const std::string& s, unsigned base = 10) 110 { 111 cln::cl_read_flags flags; 112 113 flags.syntax = cln::syntax_rational; 114 flags.lsyntax = cln::lsyntax_standard; 115 flags.rational_base = base; 116 try{ 117 d_value = read_rational(flags, s.c_str(), NULL, NULL); catch(...)118 }catch(...){ 119 std::stringstream ss; 120 ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base; 121 throw std::invalid_argument(ss.str()); 122 } 123 } 124 125 /** 126 * Creates a Rational from another Rational, q, by performing a deep copy. 127 */ Rational(const Rational & q)128 Rational(const Rational& q) : d_value(q.d_value) { } 129 130 /** 131 * Constructs a canonical Rational from a numerator. 132 */ Rational(signed int n)133 Rational(signed int n) : d_value((signed long int)n) { } Rational(unsigned int n)134 Rational(unsigned int n) : d_value((unsigned long int)n) { } Rational(signed long int n)135 Rational(signed long int n) : d_value(n) { } Rational(unsigned long int n)136 Rational(unsigned long int n) : d_value(n) { } 137 138 #ifdef CVC4_NEED_INT64_T_OVERLOADS Rational(int64_t n)139 Rational(int64_t n) : d_value(static_cast<long>(n)) { } Rational(uint64_t n)140 Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) { } 141 #endif /* CVC4_NEED_INT64_T_OVERLOADS */ 142 143 /** 144 * Constructs a canonical Rational from a numerator and denominator. 145 */ Rational(signed int n,signed int d)146 Rational(signed int n, signed int d) : d_value((signed long int)n) { 147 d_value /= cln::cl_I(d); 148 } Rational(unsigned int n,unsigned int d)149 Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n) { 150 d_value /= cln::cl_I(d); 151 } Rational(signed long int n,signed long int d)152 Rational(signed long int n, signed long int d) : d_value(n) { 153 d_value /= cln::cl_I(d); 154 } Rational(unsigned long int n,unsigned long int d)155 Rational(unsigned long int n, unsigned long int d) : d_value(n) { 156 d_value /= cln::cl_I(d); 157 } 158 159 #ifdef CVC4_NEED_INT64_T_OVERLOADS Rational(int64_t n,int64_t d)160 Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) { 161 d_value /= cln::cl_I(d); 162 } Rational(uint64_t n,uint64_t d)163 Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) { 164 d_value /= cln::cl_I(d); 165 } 166 #endif /* CVC4_NEED_INT64_T_OVERLOADS */ 167 Rational(const Integer & n,const Integer & d)168 Rational(const Integer& n, const Integer& d) : 169 d_value(n.get_cl_I()) 170 { 171 d_value /= d.get_cl_I(); 172 } Rational(const Integer & n)173 Rational(const Integer& n) : d_value(n.get_cl_I()){ } 174 ~Rational()175 ~Rational() {} 176 177 /** 178 * Returns a copy of d_value to enable public access of CLN data. 179 */ getValue()180 cln::cl_RA getValue() const 181 { 182 return d_value; 183 } 184 185 /** 186 * Returns the value of numerator of the Rational. 187 * Note that this makes a deep copy of the numerator. 188 */ getNumerator()189 Integer getNumerator() const { 190 return Integer(cln::numerator(d_value)); 191 } 192 193 /** 194 * Returns the value of denominator of the Rational. 195 * Note that this makes a deep copy of the denominator. 196 */ getDenominator()197 Integer getDenominator() const { 198 return Integer(cln::denominator(d_value)); 199 } 200 201 /** Return an exact rational for a double d. */ 202 static Maybe<Rational> fromDouble(double d); 203 204 /** 205 * Get a double representation of this Rational, which is 206 * approximate: truncation may occur, overflow may result in 207 * infinity, and underflow may result in zero. 208 */ getDouble()209 double getDouble() const { 210 return cln::double_approx(d_value); 211 } 212 inverse()213 Rational inverse() const { 214 return Rational(cln::recip(d_value)); 215 } 216 cmp(const Rational & x)217 int cmp(const Rational& x) const { 218 //Don't use mpq_class's cmp() function. 219 //The name ends up conflicting with this function. 220 return cln::compare(d_value, x.d_value); 221 } 222 223 sgn()224 int sgn() const { 225 if(cln::zerop(d_value)){ 226 return 0; 227 }else if(cln::minusp(d_value)){ 228 return -1; 229 }else{ 230 assert(cln::plusp(d_value)); 231 return 1; 232 } 233 } 234 isZero()235 bool isZero() const { 236 return cln::zerop(d_value); 237 } 238 isOne()239 bool isOne() const { 240 return d_value == 1; 241 } 242 isNegativeOne()243 bool isNegativeOne() const { 244 return d_value == -1; 245 } 246 abs()247 Rational abs() const { 248 if(sgn() < 0){ 249 return -(*this); 250 }else{ 251 return *this; 252 } 253 } 254 isIntegral()255 bool isIntegral() const{ 256 return getDenominator() == 1; 257 } 258 floor()259 Integer floor() const { 260 return Integer(cln::floor1(d_value)); 261 } 262 ceiling()263 Integer ceiling() const { 264 return Integer(cln::ceiling1(d_value)); 265 } 266 floor_frac()267 Rational floor_frac() const { 268 return (*this) - Rational(floor()); 269 } 270 271 Rational& operator=(const Rational& x){ 272 if(this == &x) return *this; 273 d_value = x.d_value; 274 return *this; 275 } 276 277 Rational operator-() const{ 278 return Rational(-(d_value)); 279 } 280 281 bool operator==(const Rational& y) const { 282 return d_value == y.d_value; 283 } 284 285 bool operator!=(const Rational& y) const { 286 return d_value != y.d_value; 287 } 288 289 bool operator< (const Rational& y) const { 290 return d_value < y.d_value; 291 } 292 293 bool operator<=(const Rational& y) const { 294 return d_value <= y.d_value; 295 } 296 297 bool operator> (const Rational& y) const { 298 return d_value > y.d_value; 299 } 300 301 bool operator>=(const Rational& y) const { 302 return d_value >= y.d_value; 303 } 304 305 Rational operator+(const Rational& y) const{ 306 return Rational( d_value + y.d_value ); 307 } 308 Rational operator-(const Rational& y) const { 309 return Rational( d_value - y.d_value ); 310 } 311 312 Rational operator*(const Rational& y) const { 313 return Rational( d_value * y.d_value ); 314 } 315 Rational operator/(const Rational& y) const { 316 return Rational( d_value / y.d_value ); 317 } 318 319 Rational& operator+=(const Rational& y){ 320 d_value += y.d_value; 321 return (*this); 322 } 323 324 Rational& operator-=(const Rational& y){ 325 d_value -= y.d_value; 326 return (*this); 327 } 328 329 Rational& operator*=(const Rational& y){ 330 d_value *= y.d_value; 331 return (*this); 332 } 333 334 Rational& operator/=(const Rational& y){ 335 d_value /= y.d_value; 336 return (*this); 337 } 338 339 /** Returns a string representing the rational in the given base. */ 340 std::string toString(int base = 10) const { 341 cln::cl_print_flags flags; 342 flags.rational_base = base; 343 flags.rational_readably = false; 344 std::stringstream ss; 345 print_rational(ss, flags, d_value); 346 return ss.str(); 347 } 348 349 /** 350 * Computes the hash of the rational from hashes of the numerator and the 351 * denominator. 352 */ hash()353 size_t hash() const { 354 return equal_hashcode(d_value); 355 } 356 complexity()357 uint32_t complexity() const { 358 return getNumerator().length() + getDenominator().length(); 359 } 360 361 /** Equivalent to calling (this->abs()).cmp(b.abs()) */ 362 int absCmp(const Rational& q) const; 363 364 };/* class Rational */ 365 366 struct RationalHashFunction { operatorRationalHashFunction367 inline size_t operator()(const CVC4::Rational& r) const { 368 return r.hash(); 369 } 370 };/* struct RationalHashFunction */ 371 372 CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n); 373 374 }/* CVC4 namespace */ 375 376 #endif /* __CVC4__RATIONAL_H */ 377