1 files changed, 6 insertions, 148 deletions
diff --git a/src/util/integer.h b/src/util/integer.h
index d1921f597..c57450d5f 100644
--- a/src/util/integer.h
+++ b/src/util/integer.h
@@ -16,151 +16,9 @@
  ** A multiprecision integer constant.
  **/
 
-#include "cvc4_public.h"
-
-#ifndef __CVC4__INTEGER_H
-#define __CVC4__INTEGER_H
-
-#include <string>
-#include <iostream>
-#include "util/gmp_util.h"
-
-namespace CVC4 {
-
-class Rational;
-
-class 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; }
-
-  /**
-   * 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){}
-
-  /**
-   * 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().
-   */
-  explicit Integer(const char * s, int base = 10): d_value(s,base) {}
-  Integer(const std::string& s, unsigned base = 10) : d_value(s, base) {}
-
-  Integer(const Integer& q) : d_value(q.d_value) {}
-
-  Integer(  signed int z) : d_value(z) {}
-  Integer(unsigned int z) : d_value(z) {}
-  Integer(  signed long int z) : d_value(z) {}
-  Integer(unsigned long int z) : d_value(z) {}
-
-  ~Integer() {}
-
-
-  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;
-  }
-
-  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) const {
-    return Integer( d_value * y.d_value );
-  }
-  Integer operator/(const Integer& y) const {
-    return Integer( d_value / y.d_value );
-  }
-
-  /** Raise this Integer to the power <code>exp</code>.
-   *
-   * @param exp the exponent
-   */
-  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 );
-  }
-
-  std::string toString(int base = 10) const{
-    return d_value.get_str(base);
-  }
-
-  //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
-
-  long getLong() const { return d_value.get_si(); }
-  unsigned long getUnsignedLong() const {return d_value.get_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());
-  }
-
-  friend class CVC4::Rational;
-};/* class Integer */
-
-struct IntegerHashStrategy {
-  static inline size_t hash(const CVC4::Integer& i) {
-    return i.hash();
-  }
-};/* struct IntegerHashStrategy */
-
-std::ostream& operator<<(std::ostream& os, const Integer& n);
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__INTEGER_H */
+#ifdef __CVC4__USE_GMP_IMP
+#include "util/integer_gmp_imp.h"
+#endif
+#ifdef __CVC4__USE_CLN_IMP
+#include "util/integer_cln_imp.h"
+#endif