Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/integer_cln_imp.h	Lines:	19	19	100.0 %
Date:	2021-09-19	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/input.h>
#include <cln/integer.h>
#include <cln/integer_io.h>
#include <cln/modinteger.h>

#include <iostream>
#include <limits>
#include <sstream>
#include <string>

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

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