Allow for better interaction of Integer/Rational with mpz_class/mpq_class. (#4612)

4 files changed, 633 insertions, 644 deletions

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index dc4a13137..a6ed6f14a 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -24,6 +24,7 @@
 #include <cln/integer.h>
 #include <cln/integer_io.h>
 #include <cln/modinteger.h>
+
 #include <iostream>
 #include <limits>
 #include <sstream>
@@ -35,53 +36,22 @@ namespace CVC4 {
 
 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)
   {
@@ -95,13 +65,13 @@ public:
 
   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 */
 
@@ -110,103 +80,90 @@ public:
   /**
    * 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));
@@ -214,13 +171,11 @@ public:
 
   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));
   }
@@ -228,20 +183,26 @@ public:
   /**
    * 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;
@@ -250,43 +211,53 @@ public:
   /**
    * 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)
@@ -300,9 +271,10 @@ public:
    * 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;
   }
 
@@ -310,9 +282,10 @@ public:
    * 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;
   }
 
@@ -321,14 +294,13 @@ public:
    */
   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>.
@@ -340,7 +312,8 @@ public:
   /**
    * 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);
   }
@@ -348,7 +321,8 @@ public:
   /**
    * 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);
   }
@@ -380,7 +354,8 @@ public:
   /**
    * 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);
   }
@@ -388,31 +363,24 @@ public:
   /**
    * 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]));
       }
     }
@@ -420,31 +388,21 @@ public:
     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;
@@ -460,20 +418,26 @@ public:
 
   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);
   }
@@ -482,9 +446,7 @@ public:
    * 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.
@@ -492,15 +454,14 @@ public:
    * @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);
@@ -510,53 +471,101 @@ public:
    * 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 */
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index f5da13f06..e42781c5f 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -20,9 +20,9 @@
 #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"
@@ -31,29 +31,18 @@ namespace CVC4 {
 
 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.
@@ -66,13 +55,13 @@ public:
 
   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 */
 
@@ -81,91 +70,82 @@ public:
   /**
    * 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);
@@ -174,25 +154,25 @@ public:
   /**
    * 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
@@ -200,17 +180,16 @@ public:
    */
   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);
@@ -219,72 +198,91 @@ public:
   /**
    * 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)
@@ -298,9 +296,10 @@ public:
    * 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;
   }
 
@@ -308,13 +307,13 @@ public:
    * 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)
    */
@@ -323,7 +322,8 @@ public:
   /**
    * 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);
@@ -332,34 +332,25 @@ public:
   /**
    * 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;
   }
 
@@ -368,7 +359,8 @@ public:
    *
    * @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);
@@ -377,7 +369,8 @@ public:
   /**
    * 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);
@@ -386,7 +379,8 @@ public:
   /**
    * 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);
@@ -420,7 +414,8 @@ public:
    * 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;
   }
@@ -428,13 +423,9 @@ public:
   /**
    * 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;
 
@@ -448,18 +439,22 @@ public:
 
   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;
   }
@@ -468,9 +463,7 @@ public:
    * 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.
@@ -478,66 +471,88 @@ public:
    * @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 */
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index f4394bbee..9b391008a 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -20,19 +20,19 @@
 #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"
@@ -54,24 +54,14 @@ namespace CVC4 {
  ** 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>).
@@ -82,14 +72,13 @@ public:
   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)
   {
@@ -98,11 +87,14 @@ public:
     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());
     }
   }
@@ -113,11 +105,14 @@ public:
     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());
     }
   }
@@ -125,78 +120,76 @@ public:
   /**
    * 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);
@@ -206,138 +199,126 @@ public:
    * 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;
@@ -350,27 +331,31 @@ public:
    * 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 */
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 3a3b89c92..26315d11d 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -25,9 +25,9 @@
  * 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"
@@ -51,23 +51,16 @@ namespace CVC4 {
  ** 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>).
@@ -78,9 +71,7 @@ public:
   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).
@@ -89,41 +80,35 @@ public:
    * 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 */
@@ -131,63 +116,60 @@ public:
   /**
    * 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);
 
@@ -196,166 +178,164 @@ public:
    * 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 */