Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/integer_cln_imp.h	Lines:	19	19	100.0 %
Date:	2021-11-07	Branches:	5	6	83.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Aina Niemetz, Tim King, Gereon Kremer
 *
 * 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.
 * ****************************************************************************
 *
 * A multiprecision integer constant; wraps a CLN multiprecision integer.
 */

#include "cvc5_public.h"

#ifndef CVC5__INTEGER_H
#define CVC5__INTEGER_H

#include <cln/integer.h>

#include <iosfwd>
#include <limits>
#include <string>

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

namespace cln
{
  struct cl_read_flags;
}

namespace cvc5 {

class Rational;

class CVC5_EXPORT Integer
{
  friend class cvc5::Rational;

 public:
  /**
   * Constructs an Integer by copying a CLN C++ primitive.
   */
  Integer(const cln::cl_I& val) : d_value(val) {}

  /** Constructs a rational with the value 0. */
  Integer() : d_value(0) {}

  /**
   * Constructs a Integer from a C string.
   * Throws std::invalid_argument if the string is not a valid integer.
   */
  explicit Integer(const char* sp, unsigned base = 10)
  {
    parseInt(std::string(sp), base);
  }

  /**
   * Constructs a Integer from a C++ string.
   * Throws std::invalid_argument if the string is not a valid integer.
   */
  explicit Integer(const std::string& s, unsigned base = 10)
  {
    parseInt(s, base);
  }

  Integer(const Integer& q) : d_value(q.d_value) {}

  Integer(signed int z) : d_value((signed long int)z) {}
  Integer(unsigned int z) : d_value((unsigned long int)z) {}
  Integer(signed long int z) : d_value(z) {}
  Integer(unsigned long int z) : d_value(z) {}

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

  /** Destructor. */
  ~Integer() {}

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

  /** Overload copy assignment operator. */
  Integer& operator=(const Integer& x);

  /** Overload equality comparison operator. */
  bool operator==(const Integer& y) const;
  /** Overload disequality comparison operator. */
  bool operator!=(const Integer& y) const;
  /** Overload less than comparison operator. */
  bool operator<(const Integer& y) const;
  /** Overload less than or equal comparison operator. */
  bool operator<=(const Integer& y) const;
  /** Overload greater than comparison operator. */
  bool operator>(const Integer& y) const;
  /** Overload greater than or equal comparison operator. */
  bool operator>=(const Integer& y) const;

  /** Overload negation operator. */
  Integer operator-() const;
  /** Overload addition operator. */
  Integer operator+(const Integer& y) const;
  /** Overload addition assignment operator. */
  Integer& operator+=(const Integer& y);
  /** Overload subtraction operator. */
  Integer operator-(const Integer& y) const;
  /** Overload subtraction assignment operator. */
  Integer& operator-=(const Integer& y);
  /** Overload multiplication operator. */
  Integer operator*(const Integer& y) const;
  /** Overload multiplication assignment operator. */
  Integer& operator*=(const Integer& y);

  /** Return the bit-wise or of this and the given Integer. */
  Integer bitwiseOr(const Integer& y) const;
  /** Return the bit-wise and of this and the given Integer. */
  Integer bitwiseAnd(const Integer& y) const;
  /** Return the bit-wise exclusive or of this and the given Integer. */
  Integer bitwiseXor(const Integer& y) const;
  /** Return the bit-wise not of this Integer. */
  Integer bitwiseNot() const;

  /** Return this*(2^pow). */
  Integer multiplyByPow2(uint32_t pow) const;

  /** Return true if bit at index 'i' is 1, and false otherwise. */
  bool isBitSet(uint32_t i) const;

  /** Set the ith bit of the current Integer to 'value'.  */
  void setBit(uint32_t i, bool value);

  /**
   * Returns the integer with the binary representation of 'size' bits
   * extended with 'amount' 1's.
   */
  Integer oneExtend(uint32_t size, uint32_t amount) const;

  /** Return a 32 bit unsigned integer representation of this Integer. */
  uint32_t toUnsignedInt() const;

  /**
   * Extract a range of bits from index 'low' to (excluding) 'low + bitCount'.
   * Note: corresponds to the extract operator of theory BV.
   */
  Integer extractBitRange(uint32_t bitCount, uint32_t low) const;

  /** Returns the floor(this / y). */
  Integer floorDivideQuotient(const Integer& y) const;

  /** Returns r == this - floor(this/y)*y. */
  Integer floorDivideRemainder(const Integer& y) const;

  /** Computes a floor quoient and remainder for x divided by y.  */
  static void floorQR(Integer& q,
                      Integer& r,
                      const Integer& x,
                      const Integer& y);

  /** Returns the ceil(this / y). */
  Integer ceilingDivideQuotient(const Integer& y) const;

  /** Returns the ceil(this / y). */
  Integer ceilingDivideRemainder(const Integer& y) const;

  /**
   * Computes a quoitent and remainder according to Boute's Euclidean
   * definition. euclidianDivideQuotient, euclidianDivideRemainder.
   *
   * Boute, Raymond T. (April 1992).
   * The Euclidean definition of the functions div and mod.
   * ACM Transactions on Programming Languages and Systems (TOPLAS)
   * ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
   */
  static void euclidianQR(Integer& q,
                          Integer& r,
                          const Integer& x,
                          const Integer& y);

  /**
   * Returns the quoitent according to Boute's Euclidean definition.
   * See the documentation for euclidianQR.
   */
  Integer euclidianDivideQuotient(const Integer& y) const;

  /**
   * Returns the remainfing according to Boute's Euclidean definition.
   * See the documentation for euclidianQR.
   */
  Integer euclidianDivideRemainder(const Integer& y) const;

  /** If y divides *this, then exactQuotient returns (this/y). */
  Integer exactQuotient(const Integer& y) const;

  /** Return y mod 2^exp. */
  Integer modByPow2(uint32_t exp) const;

  /** Returns y / 2^exp. */
  Integer divByPow2(uint32_t exp) const;

  /**
   * Raise this Integer to the power <code>exp</code>.
   *
   * @param exp the exponent
   */
  Integer pow(unsigned long int exp) const;

  /** Return the greatest common divisor of this integer with another.  */
  Integer gcd(const Integer& y) const;

  /** Return the least common multiple of this integer with another.  */
  Integer lcm(const Integer& y) const;

  /** Compute addition of this Integer x + y modulo m.  */
  Integer modAdd(const Integer& y, const Integer& m) const;

  /** Compute multiplication of this Integer x * y modulo m.  */
  Integer modMultiply(const Integer& y, const Integer& m) const;

  /**
   * Compute modular inverse x^-1 of this Integer x modulo m with m > 0.
   * Returns a value x^-1 with 0 <= x^-1 < m such that x * x^-1 = 1 modulo m
   * if such an inverse exists, and -1 otherwise.
   *
   * Such an inverse only exists if
   *   - x is non-zero
   *   - x and m are coprime, i.e., if gcd (x, m) = 1
   *
   * Note that if x and m are coprime, then x^-1 > 0 if m > 1 and x^-1 = 0
   * if m = 1 (the zero ring).
   */
  Integer modInverse(const Integer& m) const;

  /** Return true if *this exactly divides y.  */
  bool divides(const Integer& y) const;

  /** Return the absolute value of this integer.  */
  Integer abs() const;

  /** Return a string representation of this Integer. */
  std::string toString(int base = 10) const;

  /** Return 1 if this is > 0, 0 if it is 0, and -1 if it is < 0. */
  int sgn() const;

  /** Return true if this is > 0. */
  bool strictlyPositive() const;

  /** Return true if this is < 0. */
  bool strictlyNegative() const;

  /** Return true if this is 0. */
  bool isZero() const;

  /** Return true if this is 1. */
  bool isOne() const;

  /** Return true if this is -1. */
  bool isNegativeOne() const;

  /** Return true if this Integer fits into a signed int. */
  bool fitsSignedInt() const;

  /** Return true if this Integer fits into an unsigned int. */
  bool fitsUnsignedInt() const;

  /** Return the signed int representation of this Integer. */
  int getSignedInt() const;

  /** Return the unsigned int representation of this Integer. */
  unsigned int getUnsignedInt() const;

  /** Return true if this Integer fits into a signed long. */
  bool fitsSignedLong() const;

  /** Return true if this Integer fits into an unsigned long. */
  bool fitsUnsignedLong() const;

  /** Return the signed long representation of this Integer. */
  long getLong() const;

  /** Return the unsigned long representation of this Integer. */
  unsigned long getUnsignedLong() const;

  /**
   * Computes the hash of the node from the first word of the
   * numerator, the denominator.
   */
  size_t hash() const;

  /**
   * Returns true iff bit n is set.
   *
   * @param n the bit to test (0 == least significant bit)
   * @return true if bit n is set in this integer; false otherwise
   */
  bool testBit(unsigned n) const;

  /**
   * Returns k if the integer is equal to 2^(k-1)
   * @return k if the integer is equal to 2^(k-1) and 0 otherwise
   */
  unsigned isPow2() const;

  /**
   * If x != 0, returns the unique n s.t. 2^{n-1} <= abs(x) < 2^{n}.
   * If x == 0, returns 1.
   */
  size_t length() const;

  /*   cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */
  /* This function ("extended gcd") returns the greatest common divisor g of a
   * and b and at the same time the representation of g as an integral linear
   * combination of a and b: u and v with u*a+v*b = g, g >= 0. u and v will be
   * normalized to be of smallest possible absolute value, in the following
   * sense: If a and b are non-zero, and abs(a) != abs(b), u and v will satisfy
   * the inequalities abs(u) <= abs(b)/(2*g), abs(v) <= abs(a)/(2*g). */
  static void extendedGcd(
      Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b);

  /** Returns a reference to the minimum of two integers. */
  static const Integer& min(const Integer& a, const Integer& b);

  /** Returns a reference to the maximum of two integers. */
  static const Integer& max(const Integer& a, const Integer& b);

 private:
  /**
   * Gets a reference to the cln data that backs up the integer.
   * Only accessible to friend classes.
   */
  const cln::cl_I& get_cl_I() const { return d_value; }

  /**
   * Helper for parseInt.
   * Throws a std::invalid_argument on invalid input `s` for the given base.
   */
  void readInt(const cln::cl_read_flags& flags,
               const std::string& s,
               unsigned base);

  /**
   * Parse string representation of integer into this Integer.
   * Throws a std::invalid_argument on invalid inputs.
   */
  void parseInt(const std::string& s, unsigned base);

  /**
   * The following constants are to help with CLN conversion in 32 bit.
   * See http://www.ginac.de/CLN/cln.html#Conversions.
   */

  /**  2^29 - 1 */
  static signed int s_fastSignedIntMax;
  /** -2^29 */
  static signed int s_fastSignedIntMin;
  /** 2^29 - 1 */
  static unsigned int s_fastUnsignedIntMax;
  /** std::numeric_limits<signed int>::max() */
  static signed long s_slowSignedIntMax;
  /** std::numeric_limits<signed int>::min() */
  static signed long s_slowSignedIntMin;
  /** std::numeric_limits<unsigned int>::max() */
  static unsigned long s_slowUnsignedIntMax;
  /** std::numeric_limits<signed long>::min() */
  static unsigned long s_signedLongMin;
  /** std::numeric_limits<signed long>::max() */
  static unsigned long s_signedLongMax;
  /** std::numeric_limits<unsigned long>::max() */
  static unsigned long s_unsignedLongMax;

  /** Value of the rational is stored in a C++ CLN integer class. */
  cln::cl_I d_value;
}; /* class Integer */

struct IntegerHashFunction
{
  size_t operator()(const cvc5::Integer& i) const { return i.hash(); }
}; /* struct IntegerHashFunction */

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

}  // namespace cvc5

#endif /* CVC5__INTEGER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Aina Niemetz, Tim King, Gereon Kremer
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		* A multiprecision integer constant; wraps a CLN multiprecision integer.
14		*/
15
16		#include "cvc5_public.h"
17
18		#ifndef CVC5__INTEGER_H
19		#define CVC5__INTEGER_H
20
21		#include <cln/integer.h>
22
23		#include <iosfwd>
24		#include <limits>
25		#include <string>
26
27		#include "base/exception.h"
28		#include "cvc5_export.h" // remove when Cvc language support is removed
29
30		namespace cln
31		{
32		struct cl_read_flags;
33		}
34
35		namespace cvc5 {
36
37		class Rational;
38
39		class CVC5_EXPORT Integer
40		{
41		friend class cvc5::Rational;
42
43		public:
44		/**
45		* Constructs an Integer by copying a CLN C++ primitive.
46		*/
47	415416098	Integer(const cln::cl_I& val) : d_value(val) {}
48
49		/** Constructs a rational with the value 0. */
50	211868	Integer() : d_value(0) {}
51
52		/**
53		* Constructs a Integer from a C string.
54		* Throws std::invalid_argument if the string is not a valid integer.
55		*/
56	10461	explicit Integer(const char* sp, unsigned base = 10)
57	10477	{
58	10477	parseInt(std::string(sp), base);
59	10445	}
60
61		/**
62		* Constructs a Integer from a C++ string.
63		* Throws std::invalid_argument if the string is not a valid integer.
64		*/
65	237329	explicit Integer(const std::string& s, unsigned base = 10)
66	237410	{
67	237329	parseInt(s, base);
68	237248	}
69
70	15255895	Integer(const Integer& q) : d_value(q.d_value) {}
71
72	357191424	Integer(signed int z) : d_value((signed long int)z) {}
73	6138961	Integer(unsigned int z) : d_value((unsigned long int)z) {}
74	42035	Integer(signed long int z) : d_value(z) {}
75	8932	Integer(unsigned long int z) : d_value(z) {}
76
77		#ifdef CVC5_NEED_INT64_T_OVERLOADS
78		Integer(int64_t z) : d_value(static_cast<long>(z)) {}
79		Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
80		#endif /* CVC5_NEED_INT64_T_OVERLOADS */
81
82		/** Destructor. */
83	794511400	~Integer() {}
84
85		/** Returns a copy of d_value to enable public access of CLN data. */
86	22268	const cln::cl_I& getValue() const { return d_value; }
87
88		/** Overload copy assignment operator. */
89		Integer& operator=(const Integer& x);
90
91		/** Overload equality comparison operator. */
92		bool operator==(const Integer& y) const;
93		/** Overload disequality comparison operator. */
94		bool operator!=(const Integer& y) const;
95		/** Overload less than comparison operator. */
96		bool operator<(const Integer& y) const;
97		/** Overload less than or equal comparison operator. */
98		bool operator<=(const Integer& y) const;
99		/** Overload greater than comparison operator. */
100		bool operator>(const Integer& y) const;
101		/** Overload greater than or equal comparison operator. */
102		bool operator>=(const Integer& y) const;
103
104		/** Overload negation operator. */
105		Integer operator-() const;
106		/** Overload addition operator. */
107		Integer operator+(const Integer& y) const;
108		/** Overload addition assignment operator. */
109		Integer& operator+=(const Integer& y);
110		/** Overload subtraction operator. */
111		Integer operator-(const Integer& y) const;
112		/** Overload subtraction assignment operator. */
113		Integer& operator-=(const Integer& y);
114		/** Overload multiplication operator. */
115		Integer operator*(const Integer& y) const;
116		/** Overload multiplication assignment operator. */
117		Integer& operator*=(const Integer& y);
118
119		/** Return the bit-wise or of this and the given Integer. */
120		Integer bitwiseOr(const Integer& y) const;
121		/** Return the bit-wise and of this and the given Integer. */
122		Integer bitwiseAnd(const Integer& y) const;
123		/** Return the bit-wise exclusive or of this and the given Integer. */
124		Integer bitwiseXor(const Integer& y) const;
125		/** Return the bit-wise not of this Integer. */
126		Integer bitwiseNot() const;
127
128		/** Return this(2^pow). /
129		Integer multiplyByPow2(uint32_t pow) const;
130
131		/** Return true if bit at index 'i' is 1, and false otherwise. */
132		bool isBitSet(uint32_t i) const;
133
134		/** Set the ith bit of the current Integer to 'value'. */
135		void setBit(uint32_t i, bool value);
136
137		/**
138		* Returns the integer with the binary representation of 'size' bits
139		* extended with 'amount' 1's.
140		*/
141		Integer oneExtend(uint32_t size, uint32_t amount) const;
142
143		/** Return a 32 bit unsigned integer representation of this Integer. */
144		uint32_t toUnsignedInt() const;
145
146		/**
147		* Extract a range of bits from index 'low' to (excluding) 'low + bitCount'.
148		* Note: corresponds to the extract operator of theory BV.
149		*/
150		Integer extractBitRange(uint32_t bitCount, uint32_t low) const;
151
152		/** Returns the floor(this / y). */
153		Integer floorDivideQuotient(const Integer& y) const;
154
155		/** Returns r == this - floor(this/y)y. /
156		Integer floorDivideRemainder(const Integer& y) const;
157
158		/** Computes a floor quoient and remainder for x divided by y. */
159		static void floorQR(Integer& q,
160		Integer& r,
161		const Integer& x,
162		const Integer& y);
163
164		/** Returns the ceil(this / y). */
165		Integer ceilingDivideQuotient(const Integer& y) const;
166
167		/** Returns the ceil(this / y). */
168		Integer ceilingDivideRemainder(const Integer& y) const;
169
170		/**
171		* Computes a quoitent and remainder according to Boute's Euclidean
172		* definition. euclidianDivideQuotient, euclidianDivideRemainder.
173		*
174		* Boute, Raymond T. (April 1992).
175		* The Euclidean definition of the functions div and mod.
176		* ACM Transactions on Programming Languages and Systems (TOPLAS)
177		* ACM Press. 14 (2): 127 - 144. doi:10.1145/128861.128862.
178		*/
179		static void euclidianQR(Integer& q,
180		Integer& r,
181		const Integer& x,
182		const Integer& y);
183
184		/**
185		* Returns the quoitent according to Boute's Euclidean definition.
186		* See the documentation for euclidianQR.
187		*/
188		Integer euclidianDivideQuotient(const Integer& y) const;
189
190		/**
191		* Returns the remainfing according to Boute's Euclidean definition.
192		* See the documentation for euclidianQR.
193		*/
194		Integer euclidianDivideRemainder(const Integer& y) const;
195
196		/** If y divides this, then exactQuotient returns (this/y). /
197		Integer exactQuotient(const Integer& y) const;
198
199		/** Return y mod 2^exp. */
200		Integer modByPow2(uint32_t exp) const;
201
202		/** Returns y / 2^exp. */
203		Integer divByPow2(uint32_t exp) const;
204
205		/**
206		* Raise this Integer to the power <code>exp</code>.
207		*
208		* @param exp the exponent
209		*/
210		Integer pow(unsigned long int exp) const;
211
212		/** Return the greatest common divisor of this integer with another. */
213		Integer gcd(const Integer& y) const;
214
215		/** Return the least common multiple of this integer with another. */
216		Integer lcm(const Integer& y) const;
217
218		/** Compute addition of this Integer x + y modulo m. */
219		Integer modAdd(const Integer& y, const Integer& m) const;
220
221		/** Compute multiplication of this Integer x * y modulo m. */
222		Integer modMultiply(const Integer& y, const Integer& m) const;
223
224		/**
225		* Compute modular inverse x^-1 of this Integer x modulo m with m > 0.
226		* Returns a value x^-1 with 0 <= x^-1 < m such that x * x^-1 = 1 modulo m
227		* if such an inverse exists, and -1 otherwise.
228		*
229		* Such an inverse only exists if
230		* - x is non-zero
231		* - x and m are coprime, i.e., if gcd (x, m) = 1
232		*
233		* Note that if x and m are coprime, then x^-1 > 0 if m > 1 and x^-1 = 0
234		* if m = 1 (the zero ring).
235		*/
236		Integer modInverse(const Integer& m) const;
237
238		/** Return true if this exactly divides y. /
239		bool divides(const Integer& y) const;
240
241		/** Return the absolute value of this integer. */
242		Integer abs() const;
243
244		/** Return a string representation of this Integer. */
245		std::string toString(int base = 10) const;
246
247		/** Return 1 if this is > 0, 0 if it is 0, and -1 if it is < 0. */
248		int sgn() const;
249
250		/** Return true if this is > 0. */
251		bool strictlyPositive() const;
252
253		/** Return true if this is < 0. */
254		bool strictlyNegative() const;
255
256		/** Return true if this is 0. */
257		bool isZero() const;
258
259		/** Return true if this is 1. */
260		bool isOne() const;
261
262		/** Return true if this is -1. */
263		bool isNegativeOne() const;
264
265		/** Return true if this Integer fits into a signed int. */
266		bool fitsSignedInt() const;
267
268		/** Return true if this Integer fits into an unsigned int. */
269		bool fitsUnsignedInt() const;
270
271		/** Return the signed int representation of this Integer. */
272		int getSignedInt() const;
273
274		/** Return the unsigned int representation of this Integer. */
275		unsigned int getUnsignedInt() const;
276
277		/** Return true if this Integer fits into a signed long. */
278		bool fitsSignedLong() const;
279
280		/** Return true if this Integer fits into an unsigned long. */
281		bool fitsUnsignedLong() const;
282
283		/** Return the signed long representation of this Integer. */
284		long getLong() const;
285
286		/** Return the unsigned long representation of this Integer. */
287		unsigned long getUnsignedLong() const;
288
289		/**
290		* Computes the hash of the node from the first word of the
291		* numerator, the denominator.
292		*/
293		size_t hash() const;
294
295		/**
296		* Returns true iff bit n is set.
297		*
298		* @param n the bit to test (0 == least significant bit)
299		* @return true if bit n is set in this integer; false otherwise
300		*/
301		bool testBit(unsigned n) const;
302
303		/**
304		* Returns k if the integer is equal to 2^(k-1)
305		* @return k if the integer is equal to 2^(k-1) and 0 otherwise
306		*/
307		unsigned isPow2() const;
308
309		/**
310		* If x != 0, returns the unique n s.t. 2^{n-1} <= abs(x) < 2^{n}.
311		* If x == 0, returns 1.
312		*/
313		size_t length() const;
314
315		/* cl_I xgcd (const cl_I& a, const cl_I& b, cl_I* u, cl_I* v) */
316		/* This function ("extended gcd") returns the greatest common divisor g of a
317		* and b and at the same time the representation of g as an integral linear
318		* combination of a and b: u and v with ua+vb = g, g >= 0. u and v will be
319		* normalized to be of smallest possible absolute value, in the following
320		* sense: If a and b are non-zero, and abs(a) != abs(b), u and v will satisfy
321		* the inequalities abs(u) <= abs(b)/(2g), abs(v) <= abs(a)/(2g). */
322		static void extendedGcd(
323		Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b);
324
325		/** Returns a reference to the minimum of two integers. */
326		static const Integer& min(const Integer& a, const Integer& b);
327
328		/** Returns a reference to the maximum of two integers. */
329		static const Integer& max(const Integer& a, const Integer& b);
330
331		private:
332		/**
333		* Gets a reference to the cln data that backs up the integer.
334		* Only accessible to friend classes.
335		*/
336	6762081	const cln::cl_I& get_cl_I() const { return d_value; }
337
338		/**
339		* Helper for parseInt.
340		* Throws a std::invalid_argument on invalid input `s` for the given base.
341		*/
342		void readInt(const cln::cl_read_flags& flags,
343		const std::string& s,
344		unsigned base);
345
346		/**
347		* Parse string representation of integer into this Integer.
348		* Throws a std::invalid_argument on invalid inputs.
349		*/
350		void parseInt(const std::string& s, unsigned base);
351
352		/**
353		* The following constants are to help with CLN conversion in 32 bit.
354		* See http://www.ginac.de/CLN/cln.html#Conversions.
355		*/
356
357		/** 2^29 - 1 */
358		static signed int s_fastSignedIntMax;
359		/** -2^29 */
360		static signed int s_fastSignedIntMin;
361		/** 2^29 - 1 */
362		static unsigned int s_fastUnsignedIntMax;
363		/** std::numeric_limits<signed int>::max() */
364		static signed long s_slowSignedIntMax;
365		/** std::numeric_limits<signed int>::min() */
366		static signed long s_slowSignedIntMin;
367		/** std::numeric_limits<unsigned int>::max() */
368		static unsigned long s_slowUnsignedIntMax;
369		/** std::numeric_limits<signed long>::min() */
370		static unsigned long s_signedLongMin;
371		/** std::numeric_limits<signed long>::max() */
372		static unsigned long s_signedLongMax;
373		/** std::numeric_limits<unsigned long>::max() */
374		static unsigned long s_unsignedLongMax;
375
376		/** Value of the rational is stored in a C++ CLN integer class. */
377		cln::cl_I d_value;
378		}; /* class Integer */
379
380		struct IntegerHashFunction
381		{
382	75683	size_t operator()(const cvc5::Integer& i) const { return i.hash(); }
383		}; /* struct IntegerHashFunction */
384
385		std::ostream& operator<<(std::ostream& os, const Integer& n);
386
387		} // namespace cvc5
388
389		#endif /* CVC5__INTEGER_H */