Merges the cln-test branch into the main branch.

The current commit allows for switching in between GMP and CLN by changing a flag manually in configure.ac.  A configure time flag has not yet been added for deciding between the two.

To get this to work you will need to install cln in some form (for Ubuntu users the packages are libcln6(lucid)/libcln5 on karmic and libcln-dev).  You will also need to install pkg-config. You will need to rerun ./autogen.sh, and reconfigure.

11 files changed, 1058 insertions, 392 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 644376f25..1446412ce 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -25,9 +25,15 @@ libutil_la_SOURCES = \
 	configuration.h \
 	configuration.cpp \
 	rational.h \
-	rational.cpp \
 	integer.h \
-	integer.cpp \
+	rational_cln_imp.h \
+	integer_cln_imp.h \
+	rational_cln_imp.cpp \
+	integer_cln_imp.cpp \
+	rational_gmp_imp.h \
+	integer_gmp_imp.h \
+	rational_gmp_imp.cpp \
+	integer_gmp_imp.cpp \
 	bitvector.h \
 	bitvector.cpp \
 	gmp_util.h \
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
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
new file mode 100644
index 000000000..35293bb84
--- /dev/null
+++ b/src/util/integer_cln_imp.cpp
@@ -0,0 +1,34 @@
+/*********************                                                        */
+/*! \file integer.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A multiprecision rational constant.
+ **
+ ** A multiprecision rational constant.
+ ** This stores the rational as a pair of multiprecision integers,
+ ** one for the numerator and one for the denominator.
+ ** The number is always stored so that the gcd of the numerator and denominator
+ ** is 1.  (This is referred to as referred to as canonical form in GMP's
+ ** literature.) A consquence is that that the numerator and denominator may be
+ ** different than the values used to construct the Rational.
+ **/
+#ifdef __CVC4__USE_CLN_IMP
+
+#include "util/integer.h"
+
+using namespace CVC4;
+
+std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
+  return os << n.toString();
+}
+
+#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
new file mode 100644
index 000000000..2154952f0
--- /dev/null
+++ b/src/util/integer_cln_imp.h
@@ -0,0 +1,229 @@
+/*********************                                                        */
+/*! \file integer.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A multiprecision integer constant.
+ **
+ ** A multiprecision integer constant.
+ **/
+
+#ifdef __CVC4__USE_CLN_IMP
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__INTEGER_H
+#define __CVC4__INTEGER_H
+
+#include <string>
+#include <iostream>
+#include <cln/integer.h>
+#include <sstream>
+#include <cln/input.h>
+#include <cln/integer_io.h>
+#include "util/Assert.h"
+#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.
+   */
+  cln::cl_I 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; }
+  const cln::cl_I& get_cl_I() const { return d_value; }
+ 
+  /**
+   * Constructs an Integer by copying a GMP C++ primitive.
+   */
+  //Integer(const mpz_class& val) : d_value(val) {}
+  Integer(const cln::cl_I& 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) throw (std::invalid_argument){
+    cln::cl_read_flags flags;
+    flags.syntax = cln::syntax_integer;
+    flags.lsyntax = cln::lsyntax_standard;
+    flags.rational_base = base;
+    try{
+      d_value = read_integer(flags, s, NULL, NULL);
+    }catch(...){
+      std::stringstream ss;
+      ss << "Integer() failed to parse value \"" <<s << "\" in base=" <<base;
+      throw std::invalid_argument(ss.str());
+    }
+  }
+
+  Integer(const std::string& s, int base = 10) throw (std::invalid_argument) {
+    cln::cl_read_flags flags;
+    flags.syntax = cln::syntax_integer;
+    flags.lsyntax = cln::lsyntax_standard;
+    flags.rational_base = base;
+    try{
+      d_value = read_integer(flags, s.c_str(), NULL, NULL);
+    }catch(...){
+      std::stringstream ss;
+      ss << "Integer() failed to parse value \"" <<s << "\" in base=" <<base;
+      throw std::invalid_argument(ss.str());
+    }
+  }
+
+  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 );
+  }
+
+  /** Raise this Integer to the power <code>exp</code>.
+   *
+   * @param exp the exponent
+   */
+  Integer pow(unsigned long int exp) const {
+    if(exp > 0){
+      cln::cl_I result= cln::expt_pos(d_value,exp);
+      return Integer( result );
+    }else if(exp == 0){
+      return Integer( 1 );
+    }else{
+      Unimplemented();
+    }
+  }
+
+  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:
+      Unhandled();
+      break;
+    }
+    std::string output = ss.str();
+    for( unsigned i = 0; i <= output.length(); ++i){
+      if(isalpha(output[i])){
+        output.replace(i, 1, 1, tolower(output[i]));
+      }
+    }
+
+    return output;
+  }
+
+  //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
+
+  long getLong() const { return cln::cl_I_to_long(d_value); }
+  unsigned long getUnsignedLong() const {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);
+  }
+
+  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 */
+
+#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/integer.cpp b/src/util/integer_gmp_imp.cpp
index 85075fd39..7bda7f02a 100644
--- a/src/util/integer.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -22,6 +22,7 @@
  ** different than the values used to construct the Rational.
  **/
 
+#ifdef __CVC4__USE_GMP_IMP
 #include "util/integer.h"
 
 using namespace CVC4;
@@ -29,3 +30,4 @@ using namespace CVC4;
 std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
   return os << n.toString();
 }
+#endif /* __CVC4__USE_GMP_IMP */
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
new file mode 100644
index 000000000..7217d0c5a
--- /dev/null
+++ b/src/util/integer_gmp_imp.h
@@ -0,0 +1,168 @@
+/*********************                                                        */
+/*! \file integer.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A multiprecision integer constant.
+ **
+ ** A multiprecision integer constant.
+ **/
+
+#ifdef __CVC4__USE_GMP_IMP
+#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 */
+#endif /* __CVC4__USE_GMP_IMP */
diff --git a/src/util/rational.h b/src/util/rational.h
index feca66da1..73fcb73a3 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -16,245 +16,9 @@
  ** Multi-precision rational constants.
  **/
 
-#include "cvc4_public.h"
-
-#ifndef __CVC4__RATIONAL_H
-#define __CVC4__RATIONAL_H
-
-#include <gmp.h>
-#include <string>
-#include "util/integer.h"
-
-namespace CVC4 {
-
-/**
- ** A multi-precision rational constant.
- ** This stores the rational as a pair of multi-precision integers,
- ** one for the numerator and one for the denominator.
- ** The number is always stored so that the gcd of the numerator and denominator
- ** is 1.  (This is referred to as referred to as canonical form in GMP's
- ** literature.) A consequence is that that the numerator and denominator may be
- ** different than the values used to construct the Rational.
- **
- ** NOTE: The correct way to create a Rational from an int is to use one of the
- ** int numerator/int denominator constructors with the denominator 1.  Trying
- ** to construct a Rational with a single int, e.g., Rational(0), will put you
- ** 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;
-
-  /**
-   * 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:
-
-  /** Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
-   *
-   * @param dec a string encoding a decimal number in the format
-   * <code>[0-9]*\.[0-9]*</code>
-   */
-  static Rational fromDecimal(const std::string& dec);
-
-  /** Constructs a rational with the value 0/1. */
-  Rational() : d_value(0){
-    d_value.canonicalize();
-  }
-
-  /**
-   * 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().
-   */
-  explicit Rational(const char * s, int base = 10): d_value(s,base) {
-    d_value.canonicalize();
-  }
-  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();
-  }
-
-  /**
-   * 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();
-  }
-
-  /**
-   * Constructs a canonical Rational from a numerator and denominator.
-   */
-  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) {
-    d_value.canonicalize();
-  }
-  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) {
-    d_value.canonicalize();
-  }
-
-  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 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());
-  }
-
-  /**
-   * 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());
-  }
-
-  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.
-    return mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t());
-  }
-
-
-  int sgn() {
-    return mpq_sgn(d_value.get_mpq_t());
-  }
-
-  Rational& operator=(const Rational& x){
-    if(this == &x) return *this;
-    d_value = x.d_value;
-    return *this;
-  }
-
-  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;
-  }
-
-
-  
-
-  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){
-    d_value += y.d_value;
-    return (*this);
-  }
-
-  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 {
-    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 numeratorHash = gmpz_hash(d_value.get_num_mpz_t());
-    size_t denominatorHash = gmpz_hash(d_value.get_den_mpz_t());
-
-    return numeratorHash xor denominatorHash;
-  }
-
-};/* class Rational */
-
-struct RationalHashStrategy {
-  static inline size_t hash(const CVC4::Rational& r) {
-    return r.hash();
-  }
-};/* struct RationalHashStrategy */
-
-std::ostream& operator<<(std::ostream& os, const Rational& n);
-
-}/* CVC4 namespace */
-
-#endif /* __CVC4__RATIONAL_H */
+#ifdef __CVC4__USE_GMP_IMP
+#include "util/rational_gmp_imp.h"
+#endif
+#ifdef __CVC4__USE_CLN_IMP
+#include "util/rational_cln_imp.h"
+#endif
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
new file mode 100644
index 000000000..0960b79b9
--- /dev/null
+++ b/src/util/rational_cln_imp.cpp
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file rational_cln_imp.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters, cconway
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A multi-precision rational constant.
+ **
+ ** A multi-precision rational constant.
+ **/
+
+#ifdef __CVC4__USE_CLN_IMP
+
+
+#include "util/integer.h"
+#include "util/rational.h"
+#include <string>
+
+using namespace std;
+using namespace CVC4;
+
+/* Computes a rational given a decimal string. The rational
+ * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
+ */
+Rational Rational::fromDecimal(const string& dec) {
+  // Find the decimal point, if there is one
+  string::size_type i( dec.find(".") );
+  if( i != string::npos ) {
+    /* Erase the decimal point, so we have just the numerator. */
+    Integer numerator( string(dec).erase(i,1) );
+
+    /* Compute the denominator: 10 raise to the number of decimal places */
+    int decPlaces = dec.size() - (i + 1);
+    Integer denominator( Integer(10).pow(decPlaces) );
+
+    return Rational( numerator, denominator );
+  } else {
+    /* No decimal point, assume it's just an integer. */
+    return Rational( dec );
+  }
+}
+
+std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
+  return os << q.toString();
+}
+
+#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
new file mode 100644
index 000000000..347c1d195
--- /dev/null
+++ b/src/util/rational_cln_imp.h
@@ -0,0 +1,286 @@
+/*********************                                                        */
+/*! \file rational.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, mdeters, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Multi-precision rational constants.
+ **
+ ** Multi-precision rational constants.
+ **/
+
+#ifdef __CVC4__USE_CLN_IMP
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__RATIONAL_H
+#define __CVC4__RATIONAL_H
+
+#include <gmp.h>
+#include <string>
+#include <sstream>
+#include <cln/rational.h>
+#include <cln/input.h>
+#include <cln/rational_io.h>
+#include <cln/number_io.h>
+#include "util/Assert.h"
+#include "util/integer.h"
+
+namespace CVC4 {
+
+/**
+ ** A multi-precision rational constant.
+ ** This stores the rational as a pair of multi-precision integers,
+ ** one for the numerator and one for the denominator.
+ ** The number is always stored so that the gcd of the numerator and denominator
+ ** is 1.  (This is referred to as referred to as canonical form in GMP's
+ ** literature.) A consequence is that that the numerator and denominator may be
+ ** different than the values used to construct the Rational.
+ **
+ ** NOTE: The correct way to create a Rational from an int is to use one of the
+ ** int numerator/int denominator constructors with the denominator 1.  Trying
+ ** to construct a Rational with a single int, e.g., Rational(0), will put you
+ ** 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.
+   */
+  cln::cl_RA d_value;
+
+  /**
+   * 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) {  }
+  Rational(const cln::cl_RA& val) : d_value(val) {  }
+
+public:
+
+  /** Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
+   *
+   * @param dec a string encoding a decimal number in the format
+   * <code>[0-9]*\.[0-9]*</code>
+   */
+  static Rational fromDecimal(const std::string& dec);
+
+  /** Constructs a rational with the value 0/1. */
+  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().
+   */
+  explicit Rational(const char * s, int base = 10) throw (std::invalid_argument){
+    cln::cl_read_flags flags;
+
+    flags.syntax = cln::syntax_rational;
+    flags.lsyntax = cln::lsyntax_standard;
+    flags.rational_base = base;
+    try{
+      d_value = read_rational(flags, s, NULL, NULL);
+    }catch(...){
+      std::stringstream ss;
+      ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
+      throw std::invalid_argument(ss.str());
+    }
+  }
+  Rational(const std::string& s, int base = 10) throw (std::invalid_argument){
+    cln::cl_read_flags flags;
+
+    flags.syntax = cln::syntax_rational;
+    flags.lsyntax = cln::lsyntax_standard;
+    flags.rational_base = base;
+    try{
+      d_value = read_rational(flags, s.c_str(), NULL, NULL);
+    }catch(...){
+      std::stringstream ss;
+      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) { }
+
+  /**
+   * Constructs a canonical Rational from a numerator.
+   */
+  Rational(signed int n) : d_value(n) { }
+  Rational(unsigned int n) : d_value(n) { }
+  Rational(signed long int n) : d_value(n) { }
+  Rational(unsigned long int n) : d_value(n) { }
+
+  /**
+   * Constructs a canonical Rational from a numerator and denominator.
+   */
+  Rational(signed int n, signed int d) : d_value(n) {
+    d_value /= d;
+  }
+  Rational(unsigned int n, unsigned int d) : d_value(n) {
+    d_value /= d;
+  }
+  Rational(signed long int n, signed long int d) : d_value(n) {
+    d_value /= d;
+  }
+  Rational(unsigned long int n, unsigned long int d) : d_value(n) {
+    d_value /= d;
+  }
+
+  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() {}
+
+
+  /**
+   * 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));
+  }
+
+  /**
+   * 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));
+  }
+
+  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.
+    return cln::compare(d_value, x.d_value);
+  }
+
+
+  int sgn() {
+    cln::cl_RA sign = cln::signum(d_value);
+    if(sign == 0)
+      return 0;
+    else if(sign == -1)
+      return -1;
+    else if(sign == 1)
+      return 1;
+    else
+      Unreachable();
+  }
+
+  Rational& operator=(const Rational& x){
+    if(this == &x) return *this;
+    d_value = x.d_value;
+    return *this;
+  }
+
+  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;
+  }
+
+
+  
+
+  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){
+    d_value += y.d_value;
+    return (*this);
+  }
+
+  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::stringstream ss;
+    fprint(ss, d_value);
+    return ss.str();
+  }
+
+  /**
+   * Computes the hash of the rational from hashes of the numerator and the
+   * denominator.
+   */
+  size_t hash() const {
+    return equal_hashcode(d_value);
+  }
+
+};/* class Rational */
+
+struct RationalHashStrategy {
+  static inline size_t hash(const CVC4::Rational& r) {
+    return r.hash();
+  }
+};/* struct RationalHashStrategy */
+
+std::ostream& operator<<(std::ostream& os, const Rational& n);
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RATIONAL_H */
+
+#endif /* __CVC4__USE_CLN_IMP */
diff --git a/src/util/rational.cpp b/src/util/rational_gmp_imp.cpp
index beaa184bb..e5ff11c07 100644
--- a/src/util/rational.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -15,6 +15,7 @@
  **
  ** A multi-precision rational constant.
  **/
+#ifdef __CVC4__USE_GMP_IMP
 
 #include "util/integer.h"
 #include "util/rational.h"
@@ -47,3 +48,5 @@ Rational Rational::fromDecimal(const string& dec) {
 std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
   return os << q.toString();
 }
+
+#endif /* __CVC4__USE_GMP_IMP */
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
new file mode 100644
index 000000000..ab88a0d52
--- /dev/null
+++ b/src/util/rational_gmp_imp.h
@@ -0,0 +1,262 @@
+/*********************                                                        */
+/*! \file rational.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, mdeters, cconway
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Multi-precision rational constants.
+ **
+ ** Multi-precision rational constants.
+ **/
+#ifdef __CVC4__USE_GMP_IMP
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__RATIONAL_H
+#define __CVC4__RATIONAL_H
+
+#include <gmp.h>
+#include <string>
+#include "util/integer.h"
+
+namespace CVC4 {
+
+/**
+ ** A multi-precision rational constant.
+ ** This stores the rational as a pair of multi-precision integers,
+ ** one for the numerator and one for the denominator.
+ ** The number is always stored so that the gcd of the numerator and denominator
+ ** is 1.  (This is referred to as referred to as canonical form in GMP's
+ ** literature.) A consequence is that that the numerator and denominator may be
+ ** different than the values used to construct the Rational.
+ **
+ ** NOTE: The correct way to create a Rational from an int is to use one of the
+ ** int numerator/int denominator constructors with the denominator 1.  Trying
+ ** to construct a Rational with a single int, e.g., Rational(0), will put you
+ ** 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;
+
+  /**
+   * 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:
+
+  /** Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
+   *
+   * @param dec a string encoding a decimal number in the format
+   * <code>[0-9]*\.[0-9]*</code>
+   */
+  static Rational fromDecimal(const std::string& dec);
+
+  /** Constructs a rational with the value 0/1. */
+  Rational() : d_value(0){
+    d_value.canonicalize();
+  }
+
+  /**
+   * 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().
+   */
+  explicit Rational(const char * s, int base = 10): d_value(s,base) {
+    d_value.canonicalize();
+  }
+  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();
+  }
+
+  /**
+   * 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();
+  }
+
+  /**
+   * Constructs a canonical Rational from a numerator and denominator.
+   */
+  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) {
+    d_value.canonicalize();
+  }
+  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) {
+    d_value.canonicalize();
+  }
+
+  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 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());
+  }
+
+  /**
+   * 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());
+  }
+
+  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.
+    return mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t());
+  }
+
+
+  int sgn() {
+    return mpq_sgn(d_value.get_mpq_t());
+  }
+
+  Rational& operator=(const Rational& x){
+    if(this == &x) return *this;
+    d_value = x.d_value;
+    return *this;
+  }
+
+  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;
+  }
+
+
+  
+
+  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){
+    d_value += y.d_value;
+    return (*this);
+  }
+
+  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 {
+    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 numeratorHash = gmpz_hash(d_value.get_num_mpz_t());
+    size_t denominatorHash = gmpz_hash(d_value.get_den_mpz_t());
+
+    return numeratorHash xor denominatorHash;
+  }
+
+};/* class Rational */
+
+struct RationalHashStrategy {
+  static inline size_t hash(const CVC4::Rational& r) {
+    return r.hash();
+  }
+};/* struct RationalHashStrategy */
+
+std::ostream& operator<<(std::ostream& os, const Rational& n);
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RATIONAL_H */
+#endif /* __CVC4__USE_GMP_IMP */