Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/rational_cln_imp.h	Lines:	94	104	90.4 %
Date:	2021-08-20	Branches:	44	102	43.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Gereon Kremer, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Multiprecision rational constants; wraps a CLN multiprecision rational.
 */

#include "cvc5_public.h"

#ifndef CVC5__RATIONAL_H
#define CVC5__RATIONAL_H

#include <cln/dfloat.h>
#include <cln/input.h>
#include <cln/io.h>
#include <cln/number_io.h>
#include <cln/output.h>
#include <cln/rational.h>
#include <cln/rational_io.h>
#include <cln/real.h>

#include <optional>
#include <sstream>
#include <string>

#include "base/exception.h"
#include "cvc5_export.h"  // remove when Cvc language support is removed
#include "util/integer.h"

namespace cvc5 {

/**
 * A multi-precision rational constant.
 * This stores the rational as a pair of multi-precision integers,
 * one for the numerator and one for the denominator.
 * The number is always stored so that the gcd of the numerator and denominator
 * is 1.  (This is referred to as referred to as canonical form in GMP's
 * literature.) A consequence is that that the numerator and denominator may be
 * different than the values used to construct the Rational.
 *
 * NOTE: The correct way to create a Rational from an int is to use one of the
 * int numerator/int denominator constructors with the denominator 1.  Trying
 * to construct a Rational with a single int, e.g., Rational(0), will put you
 * in danger of invoking the char* constructor, from whence you will segfault.
 */

class CVC5_EXPORT Rational
{
 public:
  /**
   * Constructs a Rational from a cln::cl_RA object.
   * Does a deep copy.
   */
  Rational(const cln::cl_RA& val) : d_value(val) {}

  /**
   * Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
   *
   * @param dec a string encoding a decimal number in the format
   * <code>[0-9]*\.[0-9]*</code>
   */
  static Rational fromDecimal(const std::string& dec);

  /** Constructs a rational with the value 0/1. */
  Rational() : d_value(0) {}
  /**
   * Constructs a Rational from a C string in a given base (defaults to 10).
   *
   * Throws std::invalid_argument if the string is not a valid rational.
   * For more information about what is a valid rational string,
   * see CLN's documentation for read_rational.
   */
  explicit Rational(const char* s, unsigned base = 10)
  {
    cln::cl_read_flags flags;

    flags.syntax = cln::syntax_rational;
    flags.lsyntax = cln::lsyntax_standard;
    flags.rational_base = base;
    try
    {
      d_value = read_rational(flags, s, NULL, NULL);
    }
    catch (...)
    {
      std::stringstream ss;
      ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
      throw std::invalid_argument(ss.str());
    }
  }
  Rational(const std::string& s, unsigned base = 10)
  {
    cln::cl_read_flags flags;

    flags.syntax = cln::syntax_rational;
    flags.lsyntax = cln::lsyntax_standard;
    flags.rational_base = base;
    try
    {
      d_value = read_rational(flags, s.c_str(), NULL, NULL);
    }
    catch (...)
    {
      std::stringstream ss;
      ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
      throw std::invalid_argument(ss.str());
    }
  }

  /**
   * Creates a Rational from another Rational, q, by performing a deep copy.
   */
  Rational(const Rational& q) : d_value(q.d_value) {}

  /**
   * Constructs a canonical Rational from a numerator.
   */
  Rational(signed int n) : d_value((signed long int)n) {}
  Rational(unsigned int n) : d_value((unsigned long int)n) {}
  Rational(signed long int n) : d_value(n) {}
  Rational(unsigned long int n) : d_value(n) {}

#ifdef CVC5_NEED_INT64_T_OVERLOADS
  Rational(int64_t n) : d_value(static_cast<long>(n)) {}
  Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) {}
#endif /* CVC5_NEED_INT64_T_OVERLOADS */

  /**
   * Constructs a canonical Rational from a numerator and denominator.
   */
  Rational(signed int n, signed int d) : d_value((signed long int)n)
  {
    d_value /= cln::cl_I(d);
  }
  Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n)
  {
    d_value /= cln::cl_I(d);
  }
  Rational(signed long int n, signed long int d) : d_value(n)
  {
    d_value /= cln::cl_I(d);
  }
  Rational(unsigned long int n, unsigned long int d) : d_value(n)
  {
    d_value /= cln::cl_I(d);
  }

#ifdef CVC5_NEED_INT64_T_OVERLOADS
  Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n))
  {
    d_value /= cln::cl_I(d);
  }
  Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n))
  {
    d_value /= cln::cl_I(d);
  }
#endif /* CVC5_NEED_INT64_T_OVERLOADS */

  Rational(const Integer& n, const Integer& d) : d_value(n.get_cl_I())
  {
    d_value /= d.get_cl_I();
  }
  Rational(const Integer& n) : d_value(n.get_cl_I()) {}

  ~Rational() {}

  /**
   * Returns a copy of d_value to enable public access of CLN data.
   */
  const cln::cl_RA& getValue() const { return d_value; }

  /**
   * Returns the value of numerator of the Rational.
   * Note that this makes a deep copy of the numerator.
   */
  Integer getNumerator() const { return Integer(cln::numerator(d_value)); }

  /**
   * Returns the value of denominator of the Rational.
   * Note that this makes a deep copy of the denominator.
   */
  Integer getDenominator() const { return Integer(cln::denominator(d_value)); }

  /** Return an exact rational for a double d. */
  static std::optional<Rational> fromDouble(double d);

  /**
   * Get a double representation of this Rational, which is
   * approximate: truncation may occur, overflow may result in
   * infinity, and underflow may result in zero.
   */
  double getDouble() const { return cln::double_approx(d_value); }

  Rational inverse() const { return Rational(cln::recip(d_value)); }

  int cmp(const Rational& x) const
  {
    // Don't use mpq_class's cmp() function.
    // The name ends up conflicting with this function.
    return cln::compare(d_value, x.d_value);
  }

  int sgn() const;

  bool isZero() const { return cln::zerop(d_value); }

  bool isOne() const { return d_value == 1; }

  bool isNegativeOne() const { return d_value == -1; }

  Rational abs() const
  {
    if (sgn() < 0)
    {
      return -(*this);
    }
    else
    {
      return *this;
    }
  }

  bool isIntegral() const { return getDenominator() == 1; }

  Integer floor() const { return Integer(cln::floor1(d_value)); }

  Integer ceiling() const { return Integer(cln::ceiling1(d_value)); }

  Rational floor_frac() const { return (*this) - Rational(floor()); }

  Rational& operator=(const Rational& x)
  {
    if (this == &x) return *this;
    d_value = x.d_value;
    return *this;
  }

  Rational operator-() const { return Rational(-(d_value)); }

  bool operator==(const Rational& y) const { return d_value == y.d_value; }

  bool operator!=(const Rational& y) const { return d_value != y.d_value; }

  bool operator<(const Rational& y) const { return d_value < y.d_value; }

  bool operator<=(const Rational& y) const { return d_value <= y.d_value; }

  bool operator>(const Rational& y) const { return d_value > y.d_value; }

  bool operator>=(const Rational& y) const { return d_value >= y.d_value; }

  Rational operator+(const Rational& y) const
  {
    return Rational(d_value + y.d_value);
  }
  Rational operator-(const Rational& y) const
  {
    return Rational(d_value - y.d_value);
  }

  Rational operator*(const Rational& y) const
  {
    return Rational(d_value * y.d_value);
  }
  Rational operator/(const Rational& y) const
  {
    return Rational(d_value / y.d_value);
  }

  Rational& operator+=(const Rational& y)
  {
    d_value += y.d_value;
    return (*this);
  }

  Rational& operator-=(const Rational& y)
  {
    d_value -= y.d_value;
    return (*this);
  }

  Rational& operator*=(const Rational& y)
  {
    d_value *= y.d_value;
    return (*this);
  }

  Rational& operator/=(const Rational& y)
  {
    d_value /= y.d_value;
    return (*this);
  }

  /** Returns a string representing the rational in the given base. */
  std::string toString(int base = 10) const
  {
    cln::cl_print_flags flags;
    flags.rational_base = base;
    flags.rational_readably = false;
    std::stringstream ss;
    print_rational(ss, flags, d_value);
    return ss.str();
  }

  /**
   * Computes the hash of the rational from hashes of the numerator and the
   * denominator.
   */
  size_t hash() const { return equal_hashcode(d_value); }

  uint32_t complexity() const
  {
    return getNumerator().length() + getDenominator().length();
  }

  /** Equivalent to calling (this->abs()).cmp(b.abs()) */
  int absCmp(const Rational& q) const;

 private:
  /**
   * Stores the value of the rational in a C++ CLN rational class.
   */
  cln::cl_RA d_value;

}; /* class Rational */

struct RationalHashFunction
{
  inline size_t operator()(const cvc5::Rational& r) const { return r.hash(); }
}; /* struct RationalHashFunction */

std::ostream& operator<<(std::ostream& os, const Rational& n) CVC5_EXPORT;

}  // namespace cvc5

#endif /* CVC5__RATIONAL_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Gereon Kremer, Morgan Deters
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 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 "cvc5_export.h" // remove when Cvc language support is removed
36		#include "util/integer.h"
37
38		namespace cvc5 {
39
40		/**
41		* A multi-precision rational constant.
42		* This stores the rational as a pair of multi-precision integers,
43		* one for the numerator and one for the denominator.
44		* The number is always stored so that the gcd of the numerator and denominator
45		* is 1. (This is referred to as referred to as canonical form in GMP's
46		* literature.) A consequence is that that the numerator and denominator may be
47		* different than the values used to construct the Rational.
48		*
49		* NOTE: The correct way to create a Rational from an int is to use one of the
50		* int numerator/int denominator constructors with the denominator 1. Trying
51		* to construct a Rational with a single int, e.g., Rational(0), will put you
52		* in danger of invoking the char* constructor, from whence you will segfault.
53		*/
54
55		class CVC5_EXPORT Rational
56		{
57		public:
58		/**
59		* Constructs a Rational from a cln::cl_RA object.
60		* Does a deep copy.
61		*/
62	131356188	Rational(const cln::cl_RA& val) : d_value(val) {}
63
64		/**
65		* Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
66		*
67		* @param dec a string encoding a decimal number in the format
68		* <code>[0-9]\.[0-9]</code>
69		*/
70		static Rational fromDecimal(const std::string& dec);
71
72		/** Constructs a rational with the value 0/1. */
73	2515596	Rational() : d_value(0) {}
74		/**
75		* Constructs a Rational from a C string in a given base (defaults to 10).
76		*
77		* Throws std::invalid_argument if the string is not a valid rational.
78		* For more information about what is a valid rational string,
79		* see CLN's documentation for read_rational.
80		*/
81	52	explicit Rational(const char* s, unsigned base = 10)
82	52	{
83		cln::cl_read_flags flags;
84
85	52	flags.syntax = cln::syntax_rational;
86	52	flags.lsyntax = cln::lsyntax_standard;
87	52	flags.rational_base = base;
88		try
89		{
90	52	d_value = read_rational(flags, s, NULL, NULL);
91		}
92		catch (...)
93		{
94		std::stringstream ss;
95		ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
96		throw std::invalid_argument(ss.str());
97		}
98	52	}
99	364090	Rational(const std::string& s, unsigned base = 10)
100	364180	{
101		cln::cl_read_flags flags;
102
103	364090	flags.syntax = cln::syntax_rational;
104	364090	flags.lsyntax = cln::lsyntax_standard;
105	364090	flags.rational_base = base;
106		try
107		{
108	364090	d_value = read_rational(flags, s.c_str(), NULL, NULL);
109		}
110	180	catch (...)
111		{
112	180	std::stringstream ss;
113	90	ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
114	90	throw std::invalid_argument(ss.str());
115		}
116	364000	}
117
118		/**
119		* Creates a Rational from another Rational, q, by performing a deep copy.
120		*/
121	123005695	Rational(const Rational& q) : d_value(q.d_value) {}
122
123		/**
124		* Constructs a canonical Rational from a numerator.
125		*/
126	540825975	Rational(signed int n) : d_value((signed long int)n) {}
127	3345245	Rational(unsigned int n) : d_value((unsigned long int)n) {}
128	37830	Rational(signed long int n) : d_value(n) {}
129	49928	Rational(unsigned long int n) : d_value(n) {}
130
131		#ifdef CVC5_NEED_INT64_T_OVERLOADS
132		Rational(int64_t n) : d_value(static_cast<long>(n)) {}
133		Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) {}
134		#endif /* CVC5_NEED_INT64_T_OVERLOADS */
135
136		/**
137		* Constructs a canonical Rational from a numerator and denominator.
138		*/
139	15251107	Rational(signed int n, signed int d) : d_value((signed long int)n)
140		{
141	15251107	d_value /= cln::cl_I(d);
142	15251107	}
143	10	Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n)
144		{
145	10	d_value /= cln::cl_I(d);
146	10	}
147	20	Rational(signed long int n, signed long int d) : d_value(n)
148		{
149	20	d_value /= cln::cl_I(d);
150	20	}
151	2	Rational(unsigned long int n, unsigned long int d) : d_value(n)
152		{
153	2	d_value /= cln::cl_I(d);
154	2	}
155
156		#ifdef CVC5_NEED_INT64_T_OVERLOADS
157		Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n))
158		{
159		d_value /= cln::cl_I(d);
160		}
161		Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n))
162		{
163		d_value /= cln::cl_I(d);
164		}
165		#endif /* CVC5_NEED_INT64_T_OVERLOADS */
166
167	1231883	Rational(const Integer& n, const Integer& d) : d_value(n.get_cl_I())
168		{
169	1231883	d_value /= d.get_cl_I();
170	1231883	}
171	3085566	Rational(const Integer& n) : d_value(n.get_cl_I()) {}
172
173	821069097	~Rational() {}
174
175		/**
176		* Returns a copy of d_value to enable public access of CLN data.
177		*/
178		const cln::cl_RA& getValue() const { return d_value; }
179
180		/**
181		* Returns the value of numerator of the Rational.
182		* Note that this makes a deep copy of the numerator.
183		*/
184	17133202	Integer getNumerator() const { return Integer(cln::numerator(d_value)); }
185
186		/**
187		* Returns the value of denominator of the Rational.
188		* Note that this makes a deep copy of the denominator.
189		*/
190	217490236	Integer getDenominator() const { return Integer(cln::denominator(d_value)); }
191
192		/** Return an exact rational for a double d. */
193		static std::optional<Rational> fromDouble(double d);
194
195		/**
196		* Get a double representation of this Rational, which is
197		* approximate: truncation may occur, overflow may result in
198		* infinity, and underflow may result in zero.
199		*/
200		double getDouble() const { return cln::double_approx(d_value); }
201
202	570652	Rational inverse() const { return Rational(cln::recip(d_value)); }
203
204	75111307	int cmp(const Rational& x) const
205		{
206		// Don't use mpq_class's cmp() function.
207		// The name ends up conflicting with this function.
208	75111307	return cln::compare(d_value, x.d_value);
209		}
210
211		int sgn() const;
212
213	204404073	bool isZero() const { return cln::zerop(d_value); }
214
215	10586202	bool isOne() const { return d_value == 1; }
216
217	33178	bool isNegativeOne() const { return d_value == -1; }
218
219	293740	Rational abs() const
220		{
221	293740	if (sgn() < 0)
222		{
223	54811	return -(*this);
224		}
225		else
226		{
227	238929	return *this;
228		}
229		}
230
231	202513469	bool isIntegral() const { return getDenominator() == 1; }
232
233	2599	Integer floor() const { return Integer(cln::floor1(d_value)); }
234
235	200860	Integer ceiling() const { return Integer(cln::ceiling1(d_value)); }
236
237		Rational floor_frac() const { return (*this) - Rational(floor()); }
238
239	68603573	Rational& operator=(const Rational& x)
240		{
241	68603573	if (this == &x) return *this;
242	68603573	d_value = x.d_value;
243	68603573	return *this;
244		}
245
246	3717121	Rational operator-() const { return Rational(-(d_value)); }
247
248	513706321	bool operator==(const Rational& y) const { return d_value == y.d_value; }
249
250	53868566	bool operator!=(const Rational& y) const { return d_value != y.d_value; }
251
252	369097	bool operator<(const Rational& y) const { return d_value < y.d_value; }
253
254	24983994	bool operator<=(const Rational& y) const { return d_value <= y.d_value; }
255
256	178606	bool operator>(const Rational& y) const { return d_value > y.d_value; }
257
258	250454	bool operator>=(const Rational& y) const { return d_value >= y.d_value; }
259
260	26110096	Rational operator+(const Rational& y) const
261		{
262	26110096	return Rational(d_value + y.d_value);
263		}
264	112586	Rational operator-(const Rational& y) const
265		{
266	112586	return Rational(d_value - y.d_value);
267		}
268
269	99459165	Rational operator*(const Rational& y) const
270		{
271	99459165	return Rational(d_value * y.d_value);
272		}
273	1386568	Rational operator/(const Rational& y) const
274		{
275	1386568	return Rational(d_value / y.d_value);
276		}
277
278	45880862	Rational& operator+=(const Rational& y)
279		{
280	45880862	d_value += y.d_value;
281	45880862	return (*this);
282		}
283
284		Rational& operator-=(const Rational& y)
285		{
286		d_value -= y.d_value;
287		return (*this);
288		}
289
290	4878544	Rational& operator*=(const Rational& y)
291		{
292	4878544	d_value *= y.d_value;
293	4878544	return (*this);
294		}
295
296	1176	Rational& operator/=(const Rational& y)
297		{
298	1176	d_value /= y.d_value;
299	1176	return (*this);
300		}
301
302		/** Returns a string representing the rational in the given base. */
303	220203	std::string toString(int base = 10) const
304		{
305	440406	cln::cl_print_flags flags;
306	220203	flags.rational_base = base;
307	220203	flags.rational_readably = false;
308	440406	std::stringstream ss;
309	220203	print_rational(ss, flags, d_value);
310	440406	return ss.str();
311		}
312
313		/**
314		* Computes the hash of the rational from hashes of the numerator and the
315		* denominator.
316		*/
317	158619803	size_t hash() const { return equal_hashcode(d_value); }
318
319		uint32_t complexity() const
320		{
321		return getNumerator().length() + getDenominator().length();
322		}
323
324		/** Equivalent to calling (this->abs()).cmp(b.abs()) */
325		int absCmp(const Rational& q) const;
326
327		private:
328		/**
329		* Stores the value of the rational in a C++ CLN rational class.
330		*/
331		cln::cl_RA d_value;
332
333		}; /* class Rational */
334
335		struct RationalHashFunction
336		{
337	158619803	inline size_t operator()(const cvc5::Rational& r) const { return r.hash(); }
338		}; /* struct RationalHashFunction */
339
340		std::ostream& operator<<(std::ostream& os, const Rational& n) CVC5_EXPORT;
341
342		} // namespace cvc5
343
344		#endif /* CVC5__RATIONAL_H */