#include <cln/integer.h>
#include <cln/integer_io.h>
#include <cln/modinteger.h>
+
#include <iostream>
#include <limits>
#include <sstream>
class Rational;
-class CVC4_PUBLIC Integer {
-private:
- /**
- * Stores the value of the rational is stored in a C++ CLN integer class.
- */
- cln::cl_I d_value;
-
- /**
- * 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; }
+class CVC4_PUBLIC Integer
+{
+ friend class CVC4::Rational;
+ public:
/**
* Constructs an Integer by copying a CLN C++ primitive.
*/
Integer(const cln::cl_I& val) : d_value(val) {}
- // 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);
-
- // Throws a std::invalid_argument on invalid inputs.
- void parseInt(const std::string& s, unsigned base);
-
- // These constants are to help with CLN conversion in 32 bit.
- // See http://www.ginac.de/CLN/cln.html#Conversions
- static signed int s_fastSignedIntMax; /* 2^29 - 1 */
- static signed int s_fastSignedIntMin; /* -2^29 */
- static unsigned int s_fastUnsignedIntMax; /* 2^29 - 1 */
-
- static signed long s_slowSignedIntMax; /* std::numeric_limits<signed int>::max() */
- static signed long s_slowSignedIntMin; /* std::numeric_limits<signed int>::min() */
- static unsigned long s_slowUnsignedIntMax; /* std::numeric_limits<unsigned int>::max() */
- static unsigned long s_signedLongMin;
- static unsigned long s_signedLongMax;
- static unsigned long s_unsignedLongMax;
-public:
/** Constructs a rational with the value 0. */
- Integer() : d_value(0){}
+ Integer() : d_value(0) {}
/**
* Constructs a Integer from a C string.
- * Throws std::invalid_argument if the string is not a valid rational.
- * For more information about what is a valid rational string,
- * see GMP's documentation for mpq_set_str().
+ * Throws std::invalid_argument if the string is not a valid integer.
*/
explicit Integer(const char* sp, unsigned base = 10)
{
Integer(const Integer& q) : d_value(q.d_value) {}
- Integer( signed int z) : d_value((signed long int)z) {}
+ 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(signed long int z) : d_value(z) {}
Integer(unsigned long int z) : d_value(z) {}
#ifdef CVC4_NEED_INT64_T_OVERLOADS
- Integer( int64_t z) : d_value(static_cast<long>(z)) {}
+ Integer(int64_t z) : d_value(static_cast<long>(z)) {}
Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
/**
* Returns a copy of d_value to enable public access of CLN data.
*/
- cln::cl_I getValue() const
- {
- return d_value;
- }
+ const cln::cl_I& getValue() const { return d_value; }
- Integer& operator=(const Integer& x){
- if(this == &x) return *this;
+ Integer& operator=(const Integer& x)
+ {
+ if (this == &x) return *this;
d_value = x.d_value;
return *this;
}
- bool operator==(const Integer& y) const {
- return d_value == y.d_value;
- }
-
- Integer operator-() const{
- return Integer(-(d_value));
- }
+ bool operator==(const Integer& y) const { return d_value == y.d_value; }
+ Integer operator-() const { return Integer(-(d_value)); }
- bool operator!=(const Integer& y) const {
- return d_value != y.d_value;
- }
+ bool operator!=(const Integer& y) const { return d_value != y.d_value; }
- bool operator< (const Integer& y) const {
- return d_value < y.d_value;
- }
+ bool operator<(const Integer& y) const { return d_value < y.d_value; }
- bool operator<=(const Integer& y) const {
- return d_value <= y.d_value;
- }
+ bool operator<=(const Integer& y) const { return d_value <= y.d_value; }
- bool operator> (const Integer& y) const {
- return d_value > y.d_value;
- }
+ bool operator>(const Integer& y) const { return d_value > y.d_value; }
- bool operator>=(const Integer& y) const {
- return d_value >= y.d_value;
- }
+ bool operator>=(const Integer& y) const { return d_value >= y.d_value; }
-
- Integer operator+(const Integer& y) const {
- return Integer( d_value + y.d_value );
+ Integer operator+(const Integer& y) const
+ {
+ return Integer(d_value + y.d_value);
}
- Integer& operator+=(const Integer& y) {
+ Integer& operator+=(const Integer& y)
+ {
d_value += y.d_value;
return *this;
}
- Integer operator-(const Integer& y) const {
- return Integer( d_value - y.d_value );
+ Integer operator-(const Integer& y) const
+ {
+ return Integer(d_value - y.d_value);
}
- Integer& operator-=(const Integer& y) {
+ Integer& operator-=(const Integer& y)
+ {
d_value -= y.d_value;
return *this;
}
- Integer operator*(const Integer& y) const {
- return Integer( d_value * y.d_value );
+ Integer operator*(const Integer& y) const
+ {
+ return Integer(d_value * y.d_value);
}
- Integer& operator*=(const Integer& y) {
+ Integer& operator*=(const Integer& y)
+ {
d_value *= y.d_value;
return *this;
}
-
- Integer bitwiseOr(const Integer& y) const {
+ Integer bitwiseOr(const Integer& y) const
+ {
return Integer(cln::logior(d_value, y.d_value));
}
- Integer bitwiseAnd(const Integer& y) const {
+ Integer bitwiseAnd(const Integer& y) const
+ {
return Integer(cln::logand(d_value, y.d_value));
}
- Integer bitwiseXor(const Integer& y) const {
+ Integer bitwiseXor(const Integer& y) const
+ {
return Integer(cln::logxor(d_value, y.d_value));
}
- Integer bitwiseNot() const {
- return Integer(cln::lognot(d_value));
- }
-
+ Integer bitwiseNot() const { return Integer(cln::lognot(d_value)); }
/**
* Return this*(2^pow).
*/
- Integer multiplyByPow2(uint32_t pow) const {
+ Integer multiplyByPow2(uint32_t pow) const
+ {
cln::cl_I ipow(pow);
- return Integer( d_value << ipow);
+ return Integer(d_value << ipow);
}
- bool isBitSet(uint32_t i) const {
- return !extractBitRange(1, i).isZero();
- }
+ bool isBitSet(uint32_t i) const { return !extractBitRange(1, i).isZero(); }
- Integer setBit(uint32_t i) const {
+ Integer setBit(uint32_t i) const
+ {
cln::cl_I mask(1);
mask = mask << i;
return Integer(cln::logior(d_value, mask));
Integer oneExtend(uint32_t size, uint32_t amount) const;
- uint32_t toUnsignedInt() const {
- return cln::cl_I_to_uint(d_value);
- }
-
+ uint32_t toUnsignedInt() const { return cln::cl_I_to_uint(d_value); }
/** See CLN Documentation. */
- Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
+ Integer extractBitRange(uint32_t bitCount, uint32_t low) const
+ {
cln::cl_byte range(bitCount, low);
return Integer(cln::ldb(d_value, range));
}
/**
* Returns the floor(this / y)
*/
- Integer floorDivideQuotient(const Integer& y) const {
- return Integer( cln::floor1(d_value, y.d_value) );
+ Integer floorDivideQuotient(const Integer& y) const
+ {
+ return Integer(cln::floor1(d_value, y.d_value));
}
/**
* Returns r == this - floor(this/y)*y
*/
- Integer floorDivideRemainder(const Integer& y) const {
- return Integer( cln::floor2(d_value, y.d_value).remainder );
+ Integer floorDivideRemainder(const Integer& y) const
+ {
+ return Integer(cln::floor2(d_value, y.d_value).remainder);
}
- /**
+ /**
* Computes a floor quoient and remainder for x divided by y.
*/
- static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
+ static void floorQR(Integer& q,
+ Integer& r,
+ const Integer& x,
+ const Integer& y)
+ {
cln::cl_I_div_t res = cln::floor2(x.d_value, y.d_value);
q.d_value = res.quotient;
r.d_value = res.remainder;
/**
* Returns the ceil(this / y)
*/
- Integer ceilingDivideQuotient(const Integer& y) const {
- return Integer( cln::ceiling1(d_value, y.d_value) );
+ Integer ceilingDivideQuotient(const Integer& y) const
+ {
+ return Integer(cln::ceiling1(d_value, y.d_value));
}
/**
* Returns the ceil(this / y)
*/
- Integer ceilingDivideRemainder(const Integer& y) const {
- return Integer( cln::ceiling2(d_value, y.d_value).remainder );
+ Integer ceilingDivideRemainder(const Integer& y) const
+ {
+ return Integer(cln::ceiling2(d_value, y.d_value).remainder);
}
/**
- * Computes a quoitent and remainder according to Boute's Euclidean definition.
- * euclidianDivideQuotient, euclidianDivideRemainder.
+ * 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) {
+ static void euclidianQR(Integer& q,
+ Integer& r,
+ const Integer& x,
+ const Integer& y)
+ {
// compute the floor and then fix the value up if needed.
- floorQR(q,r,x,y);
+ floorQR(q, r, x, y);
- if(r.strictlyNegative()){
+ if (r.strictlyNegative())
+ {
// if r < 0
// abs(r) < abs(y)
// - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
// n = y * q + r
// n = y * q - abs(y) + r + abs(y)
- if(r.sgn() >= 0){
+ if (r.sgn() >= 0)
+ {
// y = abs(y)
// n = y * q - y + r + y
// n = y * (q-1) + (r+y)
q -= 1;
r += y;
- }else{
+ }
+ else
+ {
// y = -abs(y)
// n = y * q + y + r - y
// n = y * (q+1) + (r-y)
* Returns the quoitent according to Boute's Euclidean definition.
* See the documentation for euclidianQR.
*/
- Integer euclidianDivideQuotient(const Integer& y) const {
- Integer q,r;
- euclidianQR(q,r, *this, y);
+ Integer euclidianDivideQuotient(const Integer& y) const
+ {
+ Integer q, r;
+ euclidianQR(q, r, *this, y);
return q;
}
* Returns the remainfing according to Boute's Euclidean definition.
* See the documentation for euclidianQR.
*/
- Integer euclidianDivideRemainder(const Integer& y) const {
- Integer q,r;
- euclidianQR(q,r, *this, y);
+ Integer euclidianDivideRemainder(const Integer& y) const
+ {
+ Integer q, r;
+ euclidianQR(q, r, *this, y);
return r;
}
*/
Integer exactQuotient(const Integer& y) const;
- Integer modByPow2(uint32_t exp) const {
+ Integer modByPow2(uint32_t exp) const
+ {
cln::cl_byte range(exp, 0);
return Integer(cln::ldb(d_value, range));
}
- Integer divByPow2(uint32_t exp) const {
- return d_value >> exp;
- }
+ Integer divByPow2(uint32_t exp) const { return d_value >> exp; }
/**
* Raise this Integer to the power <code>exp</code>.
/**
* Return the greatest common divisor of this integer with another.
*/
- Integer gcd(const Integer& y) const {
+ Integer gcd(const Integer& y) const
+ {
cln::cl_I result = cln::gcd(d_value, y.d_value);
return Integer(result);
}
/**
* Return the least common multiple of this integer with another.
*/
- Integer lcm(const Integer& y) const {
+ Integer lcm(const Integer& y) const
+ {
cln::cl_I result = cln::lcm(d_value, y.d_value);
return Integer(result);
}
/**
* Return true if *this exactly divides y.
*/
- bool divides(const Integer& y) const {
+ bool divides(const Integer& y) const
+ {
cln::cl_I result = cln::rem(y.d_value, d_value);
return cln::zerop(result);
}
/**
* Return the absolute value of this integer.
*/
- Integer abs() const {
- return d_value >= 0 ? *this : -*this;
- }
+ Integer abs() const { return d_value >= 0 ? *this : -*this; }
- std::string toString(int base = 10) const{
+ std::string toString(int base = 10) const
+ {
std::stringstream ss;
- switch(base){
- case 2:
- fprintbinary(ss,d_value);
- break;
- case 8:
- fprintoctal(ss,d_value);
- break;
- case 10:
- fprintdecimal(ss,d_value);
- break;
- case 16:
- fprinthexadecimal(ss,d_value);
- break;
- default:
- throw Exception("Unhandled base in Integer::toString()");
+ switch (base)
+ {
+ case 2: fprintbinary(ss, d_value); break;
+ case 8: fprintoctal(ss, d_value); break;
+ case 10: fprintdecimal(ss, d_value); break;
+ case 16: fprinthexadecimal(ss, d_value); break;
+ default: throw Exception("Unhandled base in Integer::toString()");
}
std::string output = ss.str();
- for( unsigned i = 0; i <= output.length(); ++i){
- if(isalpha(output[i])){
+ for (unsigned i = 0; i <= output.length(); ++i)
+ {
+ if (isalpha(output[i]))
+ {
output.replace(i, 1, 1, tolower(output[i]));
}
}
return output;
}
- int sgn() const {
+ int sgn() const
+ {
cln::cl_I sgn = cln::signum(d_value);
return cln::cl_I_to_int(sgn);
}
+ inline bool strictlyPositive() const { return sgn() > 0; }
- inline bool strictlyPositive() const {
- return sgn() > 0;
- }
-
- inline bool strictlyNegative() const {
- return sgn() < 0;
- }
+ inline bool strictlyNegative() const { return sgn() < 0; }
- inline bool isZero() const {
- return sgn() == 0;
- }
+ inline bool isZero() const { return sgn() == 0; }
- inline bool isOne() const {
- return d_value == 1;
- }
+ inline bool isOne() const { return d_value == 1; }
- inline bool isNegativeOne() const {
- return d_value == -1;
- }
+ inline bool isNegativeOne() const { return d_value == -1; }
/** fits the C "signed int" primitive */
bool fitsSignedInt() const;
bool fitsUnsignedLong() const;
- long getLong() const {
+ long getLong() const
+ {
// ensure there isn't overflow
- CheckArgument(d_value <= std::numeric_limits<long>::max(), this,
+ CheckArgument(d_value <= std::numeric_limits<long>::max(),
+ this,
"Overflow detected in Integer::getLong()");
- CheckArgument(d_value >= std::numeric_limits<long>::min(), this,
+ CheckArgument(d_value >= std::numeric_limits<long>::min(),
+ this,
"Overflow detected in Integer::getLong()");
return cln::cl_I_to_long(d_value);
}
- unsigned long getUnsignedLong() const {
+ unsigned long getUnsignedLong() const
+ {
// ensure there isn't overflow
- CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(), this,
+ CheckArgument(d_value <= std::numeric_limits<unsigned long>::max(),
+ this,
"Overflow detected in Integer::getUnsignedLong()");
- CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(), this,
+ CheckArgument(d_value >= std::numeric_limits<unsigned long>::min(),
+ this,
"Overflow detected in Integer::getUnsignedLong()");
return cln::cl_I_to_ulong(d_value);
}
* Computes the hash of the node from the first word of the
* numerator, the denominator.
*/
- size_t hash() const {
- return equal_hashcode(d_value);
- }
+ size_t hash() const { return equal_hashcode(d_value); }
/**
* 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 {
- return cln::logbitp(n, d_value);
- }
+ bool testBit(unsigned n) const { return cln::logbitp(n, d_value); }
/**
* 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 {
+ unsigned isPow2() const
+ {
if (d_value <= 0) return 0;
// power2p returns n such that d_value = 2^(n-1)
return cln::power2p(d_value);
* 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 {
+ size_t length() const
+ {
int s = sgn();
- if(s == 0){
+ if (s == 0)
+ {
return 1;
- }else if(s < 0){
+ }
+ else if (s < 0)
+ {
size_t len = cln::integer_length(d_value);
- /*If this is -2^n, return len+1 not len to stay consistent with the definition above!
- * From CLN's documentation of integer_length:
- * This is the smallest n >= 0 such that -2^n <= x < 2^n.
- * If x > 0, this is the unique n > 0 such that 2^(n-1) <= x < 2^n.
+ /*If this is -2^n, return len+1 not len to stay consistent with the
+ * definition above! From CLN's documentation of integer_length: This is
+ * the smallest n >= 0 such that -2^n <= x < 2^n. If x > 0, this is the
+ * unique n > 0 such that 2^(n-1) <= x < 2^n.
*/
size_t ord2 = cln::ord2(d_value);
return (len == ord2) ? (len + 1) : len;
- }else{
+ }
+ else
+ {
return cln::integer_length(d_value);
}
}
-/* 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){
+ /* 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)
+ {
g.d_value = cln::xgcd(a.d_value, b.d_value, &s.d_value, &t.d_value);
}
/** Returns a reference to the minimum of two integers. */
- static const Integer& min(const Integer& a, const Integer& b){
- return (a <=b ) ? a : b;
+ static const Integer& min(const Integer& a, const Integer& b)
+ {
+ return (a <= b) ? a : b;
}
/** Returns a reference to the maximum of two integers. */
- static const Integer& max(const Integer& a, const Integer& b){
- return (a >= b ) ? a : b;
+ static const Integer& max(const Integer& a, const Integer& b)
+ {
+ return (a >= b) ? a : b;
}
- friend class CVC4::Rational;
-};/* class Integer */
+ 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; }
+ // 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);
-struct IntegerHashFunction {
- inline size_t operator()(const CVC4::Integer& i) const {
- return i.hash();
- }
-};/* struct IntegerHashFunction */
+ // Throws a std::invalid_argument on invalid inputs.
+ void parseInt(const std::string& s, unsigned base);
+
+ // These constants are to help with CLN conversion in 32 bit.
+ // See http://www.ginac.de/CLN/cln.html#Conversions
+ static signed int s_fastSignedIntMax; /* 2^29 - 1 */
+ static signed int s_fastSignedIntMin; /* -2^29 */
+ static unsigned int s_fastUnsignedIntMax; /* 2^29 - 1 */
+
+ static signed long
+ s_slowSignedIntMax; /* std::numeric_limits<signed int>::max() */
+ static signed long
+ s_slowSignedIntMin; /* std::numeric_limits<signed int>::min() */
+ static unsigned long
+ s_slowUnsignedIntMax; /* std::numeric_limits<unsigned int>::max() */
+ static unsigned long s_signedLongMin;
+ static unsigned long s_signedLongMax;
+ static unsigned long s_unsignedLongMax;
+
+ /**
+ * Stores the value of the rational is stored in a C++ CLN integer class.
+ */
+ cln::cl_I d_value;
+}; /* class Integer */
+
+struct IntegerHashFunction
+{
+ inline size_t operator()(const CVC4::Integer& i) const { return i.hash(); }
+}; /* struct IntegerHashFunction */
-inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
+inline std::ostream& operator<<(std::ostream& os, const Integer& n)
+{
return os << n.toString();
}
-}/* CVC4 namespace */
+} // namespace CVC4
#endif /* CVC4__INTEGER_H */
#ifndef CVC4__INTEGER_H
#define CVC4__INTEGER_H
-#include <string>
#include <iosfwd>
#include <limits>
+#include <string>
#include "base/exception.h"
#include "util/gmp_util.h"
class Rational;
-class CVC4_PUBLIC Integer {
-private:
- /**
- * Stores the value of the rational is stored in a C++ GMP integer class.
- * Using this instead of mpz_t allows for easier destruction.
- */
- mpz_class d_value;
-
- /**
- * Gets a reference to the gmp data that backs up the integer.
- * Only accessible to friend classes.
- */
- const mpz_class& get_mpz() const { return d_value; }
+class CVC4_PUBLIC Integer
+{
+ friend class CVC4::Rational;
+ public:
/**
* Constructs an Integer by copying a GMP C++ primitive.
*/
Integer(const mpz_class& val) : d_value(val) {}
-public:
-
/** Constructs a rational with the value 0. */
- Integer() : d_value(0){}
+ Integer() : d_value(0) {}
/**
* Constructs a Integer from a C string.
Integer(const Integer& q) : d_value(q.d_value) {}
- Integer( signed int z) : d_value(z) {}
+ Integer(signed int z) : d_value(z) {}
Integer(unsigned int z) : d_value(z) {}
- Integer( signed long int z) : d_value(z) {}
+ Integer(signed long int z) : d_value(z) {}
Integer(unsigned long int z) : d_value(z) {}
#ifdef CVC4_NEED_INT64_T_OVERLOADS
- Integer( int64_t z) : d_value(static_cast<long>(z)) {}
+ Integer(int64_t z) : d_value(static_cast<long>(z)) {}
Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
/**
* Returns a copy of d_value to enable public access of GMP data.
*/
- mpz_class getValue() const
- {
- return d_value;
- }
+ const mpz_class& getValue() const { return d_value; }
- Integer& operator=(const Integer& x){
- if(this == &x) return *this;
+ Integer& operator=(const Integer& x)
+ {
+ if (this == &x) return *this;
d_value = x.d_value;
return *this;
}
- bool operator==(const Integer& y) const {
- return d_value == y.d_value;
- }
-
- Integer operator-() const {
- return Integer(-(d_value));
- }
+ bool operator==(const Integer& y) const { return d_value == y.d_value; }
+ Integer operator-() const { return Integer(-(d_value)); }
- bool operator!=(const Integer& y) const {
- return d_value != y.d_value;
- }
-
- bool operator< (const Integer& y) const {
- return d_value < y.d_value;
- }
+ bool operator!=(const Integer& y) const { return d_value != y.d_value; }
- bool operator<=(const Integer& y) const {
- return d_value <= y.d_value;
- }
+ bool operator<(const Integer& y) const { return d_value < y.d_value; }
- bool operator> (const Integer& y) const {
- return d_value > y.d_value;
- }
+ bool operator<=(const Integer& y) const { return d_value <= y.d_value; }
- bool operator>=(const Integer& y) const {
- return d_value >= y.d_value;
- }
+ bool operator>(const Integer& y) const { return d_value > y.d_value; }
+ bool operator>=(const Integer& y) const { return d_value >= y.d_value; }
- Integer operator+(const Integer& y) const {
- return Integer( d_value + y.d_value );
+ Integer operator+(const Integer& y) const
+ {
+ return Integer(d_value + y.d_value);
}
- Integer& operator+=(const Integer& y) {
+ Integer& operator+=(const Integer& y)
+ {
d_value += y.d_value;
return *this;
}
- Integer operator-(const Integer& y) const {
- return Integer( d_value - y.d_value );
+ Integer operator-(const Integer& y) const
+ {
+ return Integer(d_value - y.d_value);
}
- Integer& operator-=(const Integer& y) {
+ Integer& operator-=(const Integer& y)
+ {
d_value -= y.d_value;
return *this;
}
- Integer operator*(const Integer& y) const {
- return Integer( d_value * y.d_value );
+ Integer operator*(const Integer& y) const
+ {
+ return Integer(d_value * y.d_value);
}
- Integer& operator*=(const Integer& y) {
+ Integer& operator*=(const Integer& y)
+ {
d_value *= y.d_value;
return *this;
}
-
- Integer bitwiseOr(const Integer& y) const {
+ Integer bitwiseOr(const Integer& y) const
+ {
mpz_class result;
mpz_ior(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
return Integer(result);
}
- Integer bitwiseAnd(const Integer& y) const {
+ Integer bitwiseAnd(const Integer& y) const
+ {
mpz_class result;
mpz_and(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
return Integer(result);
}
- Integer bitwiseXor(const Integer& y) const {
+ Integer bitwiseXor(const Integer& y) const
+ {
mpz_class result;
mpz_xor(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
return Integer(result);
}
- Integer bitwiseNot() const {
+ Integer bitwiseNot() const
+ {
mpz_class result;
mpz_com(result.get_mpz_t(), d_value.get_mpz_t());
return Integer(result);
/**
* Return this*(2^pow).
*/
- Integer multiplyByPow2(uint32_t pow) const{
+ Integer multiplyByPow2(uint32_t pow) const
+ {
mpz_class result;
mpz_mul_2exp(result.get_mpz_t(), d_value.get_mpz_t(), pow);
- return Integer( result );
+ return Integer(result);
}
/**
* Returns the Integer obtained by setting the ith bit of the
* current Integer to 1.
*/
- Integer setBit(uint32_t i) const {
+ Integer setBit(uint32_t i) const
+ {
mpz_class res = d_value;
mpz_setbit(res.get_mpz_t(), i);
return Integer(res);
}
- bool isBitSet(uint32_t i) const {
- return !extractBitRange(1, i).isZero();
- }
+ bool isBitSet(uint32_t i) const { return !extractBitRange(1, i).isZero(); }
/**
* Returns the integer with the binary representation of size bits
*/
Integer oneExtend(uint32_t size, uint32_t amount) const;
- uint32_t toUnsignedInt() const {
- return mpz_get_ui(d_value.get_mpz_t());
- }
+ uint32_t toUnsignedInt() const { return mpz_get_ui(d_value.get_mpz_t()); }
/** See GMP Documentation. */
- Integer extractBitRange(uint32_t bitCount, uint32_t low) const {
+ Integer extractBitRange(uint32_t bitCount, uint32_t low) const
+ {
// bitCount = high-low+1
- uint32_t high = low + bitCount-1;
+ uint32_t high = low + bitCount - 1;
//— Function: void mpz_fdiv_r_2exp (mpz_t r, mpz_t n, mp_bitcnt_t b)
mpz_class rem, div;
- mpz_fdiv_r_2exp(rem.get_mpz_t(), d_value.get_mpz_t(), high+1);
+ mpz_fdiv_r_2exp(rem.get_mpz_t(), d_value.get_mpz_t(), high + 1);
mpz_fdiv_q_2exp(div.get_mpz_t(), rem.get_mpz_t(), low);
return Integer(div);
/**
* Returns the floor(this / y)
*/
- Integer floorDivideQuotient(const Integer& y) const {
+ Integer floorDivideQuotient(const Integer& y) const
+ {
mpz_class q;
mpz_fdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
- return Integer( q );
+ return Integer(q);
}
/**
* Returns r == this - floor(this/y)*y
*/
- Integer floorDivideRemainder(const Integer& y) const {
+ Integer floorDivideRemainder(const Integer& y) const
+ {
mpz_class r;
mpz_fdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
- return Integer( r );
+ return Integer(r);
}
/**
* Computes a floor quotient and remainder for x divided by y.
*/
- static void floorQR(Integer& q, Integer& r, const Integer& x, const Integer& y) {
- mpz_fdiv_qr(q.d_value.get_mpz_t(), r.d_value.get_mpz_t(), x.d_value.get_mpz_t(), y.d_value.get_mpz_t());
+ static void floorQR(Integer& q,
+ Integer& r,
+ const Integer& x,
+ const Integer& y)
+ {
+ mpz_fdiv_qr(q.d_value.get_mpz_t(),
+ r.d_value.get_mpz_t(),
+ x.d_value.get_mpz_t(),
+ y.d_value.get_mpz_t());
}
/**
* Returns the ceil(this / y)
*/
- Integer ceilingDivideQuotient(const Integer& y) const {
+ Integer ceilingDivideQuotient(const Integer& y) const
+ {
mpz_class q;
mpz_cdiv_q(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
- return Integer( q );
+ return Integer(q);
}
/**
* Returns the ceil(this / y)
*/
- Integer ceilingDivideRemainder(const Integer& y) const {
+ Integer ceilingDivideRemainder(const Integer& y) const
+ {
mpz_class r;
mpz_cdiv_r(r.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
- return Integer( r );
+ return Integer(r);
}
/**
- * Computes a quotient and remainder according to Boute's Euclidean definition.
- * euclidianDivideQuotient, euclidianDivideRemainder.
+ * Computes a quotient 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) {
+ static void euclidianQR(Integer& q,
+ Integer& r,
+ const Integer& x,
+ const Integer& y)
+ {
// compute the floor and then fix the value up if needed.
- floorQR(q,r,x,y);
+ floorQR(q, r, x, y);
- if(r.strictlyNegative()){
+ if (r.strictlyNegative())
+ {
// if r < 0
// abs(r) < abs(y)
// - abs(y) < r < 0, then 0 < r + abs(y) < abs(y)
// n = y * q + r
// n = y * q - abs(y) + r + abs(y)
- if(r.sgn() >= 0){
+ if (r.sgn() >= 0)
+ {
// y = abs(y)
// n = y * q - y + r + y
// n = y * (q-1) + (r+y)
q -= 1;
r += y;
- }else{
+ }
+ else
+ {
// y = -abs(y)
// n = y * q + y + r - y
// n = y * (q+1) + (r-y)
* Returns the quotient according to Boute's Euclidean definition.
* See the documentation for euclidianQR.
*/
- Integer euclidianDivideQuotient(const Integer& y) const {
- Integer q,r;
- euclidianQR(q,r, *this, y);
+ Integer euclidianDivideQuotient(const Integer& y) const
+ {
+ Integer q, r;
+ euclidianQR(q, r, *this, y);
return q;
}
* Returns the remainder according to Boute's Euclidean definition.
* See the documentation for euclidianQR.
*/
- Integer euclidianDivideRemainder(const Integer& y) const {
- Integer q,r;
- euclidianQR(q,r, *this, y);
+ Integer euclidianDivideRemainder(const Integer& y) const
+ {
+ Integer q, r;
+ euclidianQR(q, r, *this, y);
return r;
}
-
/**
* If y divides *this, then exactQuotient returns (this/y)
*/
/**
* Returns y mod 2^exp
*/
- Integer modByPow2(uint32_t exp) const {
+ Integer modByPow2(uint32_t exp) const
+ {
mpz_class res;
mpz_fdiv_r_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
return Integer(res);
/**
* Returns y / 2^exp
*/
- Integer divByPow2(uint32_t exp) const {
+ Integer divByPow2(uint32_t exp) const
+ {
mpz_class res;
mpz_fdiv_q_2exp(res.get_mpz_t(), d_value.get_mpz_t(), exp);
return Integer(res);
}
+ int sgn() const { return mpz_sgn(d_value.get_mpz_t()); }
- int sgn() const {
- return mpz_sgn(d_value.get_mpz_t());
- }
+ inline bool strictlyPositive() const { return sgn() > 0; }
- inline bool strictlyPositive() const {
- return sgn() > 0;
- }
+ inline bool strictlyNegative() const { return sgn() < 0; }
- inline bool strictlyNegative() const {
- return sgn() < 0;
- }
-
- inline bool isZero() const {
- return sgn() == 0;
- }
+ inline bool isZero() const { return sgn() == 0; }
- bool isOne() const {
- return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0;
- }
+ bool isOne() const { return mpz_cmp_si(d_value.get_mpz_t(), 1) == 0; }
- bool isNegativeOne() const {
+ bool isNegativeOne() const
+ {
return mpz_cmp_si(d_value.get_mpz_t(), -1) == 0;
}
*
* @param exp the exponent
*/
- Integer pow(unsigned long int exp) const {
+ Integer pow(unsigned long int exp) const
+ {
mpz_class result;
mpz_pow_ui(result.get_mpz_t(), d_value.get_mpz_t(), exp);
return Integer(result);
/**
* Return the greatest common divisor of this integer with another.
*/
- Integer gcd(const Integer& y) const {
+ Integer gcd(const Integer& y) const
+ {
mpz_class result;
mpz_gcd(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
return Integer(result);
/**
* Return the least common multiple of this integer with another.
*/
- Integer lcm(const Integer& y) const {
+ Integer lcm(const Integer& y) const
+ {
mpz_class result;
mpz_lcm(result.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
return Integer(result);
* All non-zero integers z, z.divide(0)
* ! zero.divides(zero)
*/
- bool divides(const Integer& y) const {
+ bool divides(const Integer& y) const
+ {
int res = mpz_divisible_p(y.d_value.get_mpz_t(), d_value.get_mpz_t());
return res != 0;
}
/**
* Return the absolute value of this integer.
*/
- Integer abs() const {
- return d_value >= 0 ? *this : -*this;
- }
+ Integer abs() const { return d_value >= 0 ? *this : -*this; }
- std::string toString(int base = 10) const{
- return d_value.get_str(base);
- }
+ std::string toString(int base = 10) const { return d_value.get_str(base); }
bool fitsSignedInt() const;
bool fitsUnsignedLong() const;
- long getLong() const {
+ long getLong() const
+ {
long si = d_value.get_si();
// ensure there wasn't overflow
- CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this,
- "Overflow detected in Integer::getLong().");
+ CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0,
+ this,
+ "Overflow detected in Integer::getLong().");
return si;
}
- unsigned long getUnsignedLong() const {
+ unsigned long getUnsignedLong() const
+ {
unsigned long ui = d_value.get_ui();
// ensure there wasn't overflow
- CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this,
+ CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0,
+ this,
"Overflow detected in Integer::getUnsignedLong().");
return ui;
}
* Computes the hash of the node from the first word of the
* numerator, the denominator.
*/
- size_t hash() const {
- return gmpz_hash(d_value.get_mpz_t());
- }
+ size_t hash() const { return gmpz_hash(d_value.get_mpz_t()); }
/**
* 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 {
- return mpz_tstbit(d_value.get_mpz_t(), n);
- }
+ bool testBit(unsigned n) const { return mpz_tstbit(d_value.get_mpz_t(), n); }
/**
* 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 {
+ unsigned isPow2() const
+ {
if (d_value <= 0) return 0;
// check that the number of ones in the binary representation is 1
- if (mpz_popcount(d_value.get_mpz_t()) == 1) {
+ if (mpz_popcount(d_value.get_mpz_t()) == 1)
+ {
// return the index of the first one plus 1
return mpz_scan1(d_value.get_mpz_t(), 0) + 1;
}
- return 0;
+ return 0;
}
-
/**
* If x != 0, returns the smallest n s.t. 2^{n-1} <= abs(x) < 2^{n}.
* If x == 0, returns 1.
*/
- size_t length() const {
- if(sgn() == 0){
+ size_t length() const
+ {
+ if (sgn() == 0)
+ {
return 1;
- }else{
- return mpz_sizeinbase(d_value.get_mpz_t(),2);
+ }
+ else
+ {
+ return mpz_sizeinbase(d_value.get_mpz_t(), 2);
}
}
- static void extendedGcd(Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b){
- //see the documentation for:
- //mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b);
- mpz_gcdext (g.d_value.get_mpz_t(), s.d_value.get_mpz_t(), t.d_value.get_mpz_t(), a.d_value.get_mpz_t(), b.d_value.get_mpz_t());
+ static void extendedGcd(
+ Integer& g, Integer& s, Integer& t, const Integer& a, const Integer& b)
+ {
+ // see the documentation for:
+ // mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b);
+ mpz_gcdext(g.d_value.get_mpz_t(),
+ s.d_value.get_mpz_t(),
+ t.d_value.get_mpz_t(),
+ a.d_value.get_mpz_t(),
+ b.d_value.get_mpz_t());
}
/** Returns a reference to the minimum of two integers. */
- static const Integer& min(const Integer& a, const Integer& b){
- return (a <=b ) ? a : b;
+ static const Integer& min(const Integer& a, const Integer& b)
+ {
+ return (a <= b) ? a : b;
}
/** Returns a reference to the maximum of two integers. */
- static const Integer& max(const Integer& a, const Integer& b){
- return (a >= b ) ? a : b;
+ static const Integer& max(const Integer& a, const Integer& b)
+ {
+ return (a >= b) ? a : b;
}
- friend class CVC4::Rational;
-};/* class Integer */
+ private:
+ /**
+ * Gets a reference to the gmp data that backs up the integer.
+ * Only accessible to friend classes.
+ */
+ const mpz_class& get_mpz() const { return d_value; }
-struct IntegerHashFunction {
- inline size_t operator()(const CVC4::Integer& i) const {
- return i.hash();
- }
-};/* struct IntegerHashFunction */
+ /**
+ * Stores the value of the rational is stored in a C++ GMP integer class.
+ * Using this instead of mpz_t allows for easier destruction.
+ */
+ mpz_class d_value;
+}; /* class Integer */
+
+struct IntegerHashFunction
+{
+ inline size_t operator()(const CVC4::Integer& i) const { return i.hash(); }
+}; /* struct IntegerHashFunction */
-inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
+inline std::ostream& operator<<(std::ostream& os, const Integer& n)
+{
return os << n.toString();
}
-}/* CVC4 namespace */
+} // namespace CVC4
#endif /* CVC4__INTEGER_H */
#ifndef CVC4__RATIONAL_H
#define CVC4__RATIONAL_H
-#include <gmp.h>
-#include <string>
-#include <sstream>
-#include <cassert>
-#include <cln/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/number_io.h>
-#include <cln/dfloat.h>
#include <cln/real.h>
+#include <cassert>
+#include <sstream>
+#include <string>
+
#include "base/exception.h"
#include "util/integer.h"
#include "util/maybe.h"
** in danger of invoking the char* constructor, from whence you will segfault.
**/
-class CVC4_PUBLIC Rational {
-private:
+class CVC4_PUBLIC Rational
+{
+ public:
/**
- * Stores the value of the rational is stored in a C++ GMP rational class.
- * Using this instead of mpq_t allows for easier destruction.
- */
- cln::cl_RA d_value;
-
- /**
- * Constructs a Rational from a mpq_class object.
+ * Constructs a Rational from a cln::cl_RA object.
* Does a deep copy.
- * Assumes that the value is in canonical form, and thus does not
- * have to call canonicalize() on the value.
*/
- //Rational(const mpq_class& val) : d_value(val) { }
- Rational(const cln::cl_RA& val) : d_value(val) { }
-
-public:
+ Rational(const cln::cl_RA& val) : d_value(val) {}
/**
* Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
static Rational fromDecimal(const std::string& dec);
/** Constructs a rational with the value 0/1. */
- Rational() : d_value(0){
- }
+ 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 GMP's documentation for mpq_set_str().
+ * see CLN's documentation for read_rational.
*/
explicit Rational(const char* s, unsigned base = 10)
{
flags.syntax = cln::syntax_rational;
flags.lsyntax = cln::lsyntax_standard;
flags.rational_base = base;
- try{
+ try
+ {
d_value = read_rational(flags, s, NULL, NULL);
- }catch(...){
+ }
+ catch (...)
+ {
std::stringstream ss;
- ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
+ ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
throw std::invalid_argument(ss.str());
}
}
flags.syntax = cln::syntax_rational;
flags.lsyntax = cln::lsyntax_standard;
flags.rational_base = base;
- try{
+ try
+ {
d_value = read_rational(flags, s.c_str(), NULL, NULL);
- }catch(...){
+ }
+ catch (...)
+ {
std::stringstream ss;
- ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
+ 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) { }
+ 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) { }
+ 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 CVC4_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)) { }
+ Rational(int64_t n) : d_value(static_cast<long>(n)) {}
+ Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) {}
#endif /* CVC4_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) {
+ 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) {
+ 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) {
+ 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) {
+ Rational(unsigned long int n, unsigned long int d) : d_value(n)
+ {
d_value /= cln::cl_I(d);
}
#ifdef CVC4_NEED_INT64_T_OVERLOADS
- Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) {
+ 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)) {
+ Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n))
+ {
d_value /= cln::cl_I(d);
}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
- Rational(const Integer& n, const Integer& d) :
- d_value(n.get_cl_I())
+ 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(const Integer& n) : d_value(n.get_cl_I()) {}
~Rational() {}
/**
* Returns a copy of d_value to enable public access of CLN data.
*/
- cln::cl_RA getValue() const
- {
- return d_value;
- }
+ 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));
- }
+ 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));
- }
+ Integer getDenominator() const { return Integer(cln::denominator(d_value)); }
/** Return an exact rational for a double d. */
static Maybe<Rational> fromDouble(double d);
* approximate: truncation may occur, overflow may result in
* infinity, and underflow may result in zero.
*/
- double getDouble() const {
- return cln::double_approx(d_value);
- }
+ double getDouble() const { return cln::double_approx(d_value); }
- Rational inverse() const {
- return Rational(cln::recip(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.
+ 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 {
- if(cln::zerop(d_value)){
- return 0;
- }else if(cln::minusp(d_value)){
- return -1;
- }else{
+ int sgn() const
+ {
+ if (cln::zerop(d_value))
+ {
+ return 0;
+ }
+ else if (cln::minusp(d_value))
+ {
+ return -1;
+ }
+ else
+ {
assert(cln::plusp(d_value));
return 1;
}
}
- bool isZero() const {
- return cln::zerop(d_value);
- }
+ bool isZero() const { return cln::zerop(d_value); }
- bool isOne() const {
- return d_value == 1;
- }
+ bool isOne() const { return d_value == 1; }
- bool isNegativeOne() const {
- return d_value == -1;
- }
+ bool isNegativeOne() const { return d_value == -1; }
- Rational abs() const {
- if(sgn() < 0){
+ Rational abs() const
+ {
+ if (sgn() < 0)
+ {
return -(*this);
- }else{
+ }
+ else
+ {
return *this;
}
}
- bool isIntegral() const{
- return getDenominator() == 1;
- }
+ bool isIntegral() const { return getDenominator() == 1; }
- Integer floor() const {
- return Integer(cln::floor1(d_value));
- }
+ Integer floor() const { return Integer(cln::floor1(d_value)); }
- Integer ceiling() const {
- return Integer(cln::ceiling1(d_value));
- }
+ Integer ceiling() const { return Integer(cln::ceiling1(d_value)); }
- Rational floor_frac() const {
- return (*this) - Rational(floor());
- }
+ Rational floor_frac() const { return (*this) - Rational(floor()); }
- Rational& operator=(const Rational& x){
- if(this == &x) return *this;
+ Rational& operator=(const Rational& x)
+ {
+ if (this == &x) return *this;
d_value = x.d_value;
return *this;
}
- Rational operator-() const{
- return Rational(-(d_value));
- }
+ 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; }
- 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) 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){
+ Rational& operator+=(const Rational& y)
+ {
d_value += y.d_value;
return (*this);
}
- Rational& operator-=(const Rational& y){
+ Rational& operator-=(const Rational& y)
+ {
d_value -= y.d_value;
return (*this);
}
- Rational& operator*=(const Rational& y){
+ Rational& operator*=(const Rational& y)
+ {
d_value *= y.d_value;
return (*this);
}
- Rational& operator/=(const Rational& y){
+ 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 {
+ std::string toString(int base = 10) const
+ {
cln::cl_print_flags flags;
flags.rational_base = base;
flags.rational_readably = false;
* Computes the hash of the rational from hashes of the numerator and the
* denominator.
*/
- size_t hash() const {
- return equal_hashcode(d_value);
- }
+ size_t hash() const { return equal_hashcode(d_value); }
- uint32_t complexity() const {
+ uint32_t complexity() const
+ {
return getNumerator().length() + getDenominator().length();
}
/** Equivalent to calling (this->abs()).cmp(b.abs()) */
int absCmp(const Rational& q) const;
-};/* class Rational */
+ 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 CVC4::Rational& r) const {
- return r.hash();
- }
-};/* struct RationalHashFunction */
+struct RationalHashFunction
+{
+ inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); }
+}; /* struct RationalHashFunction */
CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
-}/* CVC4 namespace */
+} // namespace CVC4
#endif /* CVC4__RATIONAL_H */
* cause errors: https://gcc.gnu.org/gcc-4.9/porting_to.html
* Including <cstddef> is a workaround for this issue.
*/
-#include <cstddef>
-
#include <gmp.h>
+
+#include <cstddef>
#include <string>
#include "base/exception.h"
** in danger of invoking the char* constructor, from whence you will segfault.
**/
-class CVC4_PUBLIC Rational {
-private:
- /**
- * Stores the value of the rational is stored in a C++ GMP rational class.
- * Using this instead of mpq_t allows for easier destruction.
- */
- mpq_class d_value;
-
+class CVC4_PUBLIC Rational
+{
+ public:
/**
* Constructs a Rational from a mpq_class object.
* Does a deep copy.
* Assumes that the value is in canonical form, and thus does not
* have to call canonicalize() on the value.
*/
- Rational(const mpq_class& val) : d_value(val) { }
-
-public:
+ Rational(const mpq_class& val) : d_value(val) {}
/**
* Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
static Rational fromDecimal(const std::string& dec);
/** Constructs a rational with the value 0/1. */
- Rational() : d_value(0){
- d_value.canonicalize();
- }
+ Rational() : d_value(0) { d_value.canonicalize(); }
/**
* Constructs a Rational from a C string in a given base (defaults to 10).
* For more information about what is a valid rational string,
* see GMP's documentation for mpq_set_str().
*/
- explicit Rational(const char* s, unsigned base = 10): d_value(s, base) {
+ explicit Rational(const char* s, unsigned base = 10) : d_value(s, base)
+ {
d_value.canonicalize();
}
- Rational(const std::string& s, unsigned base = 10) : d_value(s, base) {
+ Rational(const std::string& s, unsigned base = 10) : d_value(s, base)
+ {
d_value.canonicalize();
}
/**
* Creates a Rational from another Rational, q, by performing a deep copy.
*/
- Rational(const Rational& q) : d_value(q.d_value) {
- d_value.canonicalize();
- }
+ Rational(const Rational& q) : d_value(q.d_value) { d_value.canonicalize(); }
/**
* Constructs a canonical Rational from a numerator.
*/
- Rational(signed int n) : d_value(n,1) {
- d_value.canonicalize();
- }
- Rational(unsigned int n) : d_value(n,1) {
- d_value.canonicalize();
- }
- Rational(signed long int n) : d_value(n,1) {
- d_value.canonicalize();
- }
- Rational(unsigned long int n) : d_value(n,1) {
- d_value.canonicalize();
- }
+ Rational(signed int n) : d_value(n, 1) { d_value.canonicalize(); }
+ Rational(unsigned int n) : d_value(n, 1) { d_value.canonicalize(); }
+ Rational(signed long int n) : d_value(n, 1) { d_value.canonicalize(); }
+ Rational(unsigned long int n) : d_value(n, 1) { d_value.canonicalize(); }
#ifdef CVC4_NEED_INT64_T_OVERLOADS
- Rational(int64_t n) : d_value(static_cast<long>(n), 1) {
+ Rational(int64_t n) : d_value(static_cast<long>(n), 1)
+ {
d_value.canonicalize();
}
- Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1) {
+ Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1)
+ {
d_value.canonicalize();
}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
/**
* Constructs a canonical Rational from a numerator and denominator.
*/
- Rational(signed int n, signed int d) : d_value(n,d) {
+ Rational(signed int n, signed int d) : d_value(n, d)
+ {
d_value.canonicalize();
}
- Rational(unsigned int n, unsigned int d) : d_value(n,d) {
+ Rational(unsigned int n, unsigned int d) : d_value(n, d)
+ {
d_value.canonicalize();
}
- Rational(signed long int n, signed long int d) : d_value(n,d) {
+ Rational(signed long int n, signed long int d) : d_value(n, d)
+ {
d_value.canonicalize();
}
- Rational(unsigned long int n, unsigned long int d) : d_value(n,d) {
+ Rational(unsigned long int n, unsigned long int d) : d_value(n, d)
+ {
d_value.canonicalize();
}
#ifdef CVC4_NEED_INT64_T_OVERLOADS
- Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n), static_cast<long>(d)) {
+ Rational(int64_t n, int64_t d)
+ : d_value(static_cast<long>(n), static_cast<long>(d))
+ {
d_value.canonicalize();
}
- Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d)) {
+ Rational(uint64_t n, uint64_t d)
+ : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d))
+ {
d_value.canonicalize();
}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
- Rational(const Integer& n, const Integer& d) :
- d_value(n.get_mpz(), d.get_mpz())
- {
- d_value.canonicalize();
- }
- Rational(const Integer& n) :
- d_value(n.get_mpz())
+ Rational(const Integer& n, const Integer& d)
+ : d_value(n.get_mpz(), d.get_mpz())
{
d_value.canonicalize();
}
+ Rational(const Integer& n) : d_value(n.get_mpz()) { d_value.canonicalize(); }
~Rational() {}
/**
* Returns a copy of d_value to enable public access of GMP data.
*/
- mpq_class getValue() const
- {
- return d_value;
- }
+ const mpq_class& 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(d_value.get_num());
- }
+ Integer getNumerator() const { return Integer(d_value.get_num()); }
/**
* Returns the value of denominator of the Rational.
* Note that this makes a deep copy of the denominator.
*/
- Integer getDenominator() const {
- return Integer(d_value.get_den());
- }
+ Integer getDenominator() const { return Integer(d_value.get_den()); }
static Maybe<Rational> fromDouble(double d);
* approximate: truncation may occur, overflow may result in
* infinity, and underflow may result in zero.
*/
- double getDouble() const {
- return d_value.get_d();
- }
+ double getDouble() const { return d_value.get_d(); }
- Rational inverse() const {
+ Rational inverse() const
+ {
return Rational(getDenominator(), getNumerator());
}
- int cmp(const Rational& x) const {
- //Don't use mpq_class's cmp() function.
- //The name ends up conflicting with this function.
+ int cmp(const Rational& x) const
+ {
+ // Don't use mpq_class's cmp() function.
+ // The name ends up conflicting with this function.
return mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t());
}
- int sgn() const {
- return mpq_sgn(d_value.get_mpq_t());
- }
+ int sgn() const { return mpq_sgn(d_value.get_mpq_t()); }
- bool isZero() const {
- return sgn() == 0;
- }
+ bool isZero() const { return sgn() == 0; }
- bool isOne() const {
- return mpq_cmp_si(d_value.get_mpq_t(), 1, 1) == 0;
- }
+ bool isOne() const { return mpq_cmp_si(d_value.get_mpq_t(), 1, 1) == 0; }
- bool isNegativeOne() const {
+ bool isNegativeOne() const
+ {
return mpq_cmp_si(d_value.get_mpq_t(), -1, 1) == 0;
}
- Rational abs() const {
- if(sgn() < 0){
+ Rational abs() const
+ {
+ if (sgn() < 0)
+ {
return -(*this);
- }else{
+ }
+ else
+ {
return *this;
}
}
- Integer floor() const {
+ Integer floor() const
+ {
mpz_class q;
mpz_fdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
return Integer(q);
}
- Integer ceiling() const {
+ Integer ceiling() const
+ {
mpz_class q;
mpz_cdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
return Integer(q);
}
- Rational floor_frac() const {
- return (*this) - Rational(floor());
- }
+ Rational floor_frac() const { return (*this) - Rational(floor()); }
- Rational& operator=(const Rational& x){
- if(this == &x) return *this;
+ Rational& operator=(const Rational& x)
+ {
+ if (this == &x) return *this;
d_value = x.d_value;
return *this;
}
- Rational operator-() const{
- return Rational(-(d_value));
- }
+ 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; }
- 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) 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){
+ Rational& operator+=(const Rational& y)
+ {
d_value += y.d_value;
return (*this);
}
- Rational& operator-=(const Rational& y){
+ Rational& operator-=(const Rational& y)
+ {
d_value -= y.d_value;
return (*this);
}
- Rational& operator*=(const Rational& y){
+ Rational& operator*=(const Rational& y)
+ {
d_value *= y.d_value;
return (*this);
}
- Rational& operator/=(const Rational& y){
+ Rational& operator/=(const Rational& y)
+ {
d_value /= y.d_value;
return (*this);
}
- bool isIntegral() const{
- return getDenominator() == 1;
- }
+ bool isIntegral() const { return getDenominator() == 1; }
/** Returns a string representing the rational in the given base. */
- std::string toString(int base = 10) const {
- return d_value.get_str(base);
- }
+ std::string toString(int base = 10) const { return d_value.get_str(base); }
/**
* Computes the hash of the rational from hashes of the numerator and the
* denominator.
*/
- size_t hash() const {
+ size_t hash() const
+ {
size_t numeratorHash = gmpz_hash(d_value.get_num_mpz_t());
size_t denominatorHash = gmpz_hash(d_value.get_den_mpz_t());
return numeratorHash xor denominatorHash;
}
- uint32_t complexity() const {
+ uint32_t complexity() const
+ {
uint32_t numLen = getNumerator().length();
uint32_t denLen = getDenominator().length();
- return numLen + denLen;
+ return numLen + denLen;
}
/** Equivalent to calling (this->abs()).cmp(b.abs()) */
int absCmp(const Rational& q) const;
-};/* class Rational */
+ private:
+ /**
+ * Stores the value of the rational is stored in a C++ GMP rational class.
+ * Using this instead of mpq_t allows for easier destruction.
+ */
+ mpq_class d_value;
-struct RationalHashFunction {
- inline size_t operator()(const CVC4::Rational& r) const {
- return r.hash();
- }
-};/* struct RationalHashFunction */
+}; /* class Rational */
+
+struct RationalHashFunction
+{
+ inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); }
+}; /* struct RationalHashFunction */
CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
-}/* CVC4 namespace */
+} // namespace CVC4
#endif /* CVC4__RATIONAL_H */
projects / cvc5.git / commitdiff