Added GMP backed Rational and Integer classes, and white box tests for them. You may have to reconfigure after this update.

5 files changed, 349 insertions, 1 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 76414ebe1..f6f8323be 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -20,4 +20,8 @@ libutil_la_SOURCES = \
 	output.h \
 	result.h \
 	unique_id.h \
-	configuration.h
+	configuration.ha \
+	rational.h \
+	rational.cpp \
+	integer.h \
+	integer.cpp
diff --git a/src/util/integer.cpp b/src/util/integer.cpp
new file mode 100644
index 000000000..8fc788eb8
--- /dev/null
+++ b/src/util/integer.cpp
@@ -0,0 +1,7 @@
+#include "util/integer.h"
+
+using namespace CVC4;
+
+std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n){
+  return os << n.toString();
+}
diff --git a/src/util/integer.h b/src/util/integer.h
new file mode 100644
index 000000000..1ac8eab78
--- /dev/null
+++ b/src/util/integer.h
@@ -0,0 +1,157 @@
+/*********************                                                        */
+/** integer.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** 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.
+ **
+ ** A multiprecision integer constant.
+ **/
+#include <gmpxx.h>
+#include <string>
+
+
+#ifndef __CVC4__INTEGER_H
+#define __CVC4__INTEGER_H
+
+namespace CVC4 {
+
+/** Hashes the gmp integer primitive in a word by word fashion. */
+inline size_t gmpz_hash(const mpz_t toHash){
+  size_t hash = 0;
+  for (int i=0, n=mpz_size(toHash); i<n; ++i){
+    mp_limb_t limb = mpz_getlimbn(toHash, i);
+    hash = hash * 2;
+    hash = hash xor limb;
+  }
+  return hash;
+}
+
+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 stribng is not a valid rational.
+   * For more information about what is a vaid rational string,
+   * see GMP's documentation for mpq_set_str().
+   */
+  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 );
+  }
+
+  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 */
+
+std::ostream& operator<<(std::ostream& os, const Integer& n);
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RATIONAL_H */
+
diff --git a/src/util/rational.cpp b/src/util/rational.cpp
new file mode 100644
index 000000000..2f33ed859
--- /dev/null
+++ b/src/util/rational.cpp
@@ -0,0 +1,8 @@
+
+#include "util/rational.h"
+
+using namespace CVC4;
+
+std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
+  return os << q.toString();
+}
diff --git a/src/util/rational.h b/src/util/rational.h
new file mode 100644
index 000000000..e3f760031
--- /dev/null
+++ b/src/util/rational.h
@@ -0,0 +1,172 @@
+/*********************                                                        */
+/** rational.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** 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.
+ **
+ ** A multiprecision rational constant.
+ **/
+
+#include <gmpxx.h>
+#include <string>
+#include "integer.h"
+
+#ifndef __CVC4__RATIONAL_H
+#define __CVC4__RATIONAL_H
+
+namespace CVC4 {
+
+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;
+
+  /**
+   * 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:
+
+  /** Constructs a rational with the value 0/1. */
+  Rational() : d_value(0){
+    d_value.canonicalize();
+  }
+
+  /**
+   * Constructs a Rational from a C string.
+   * Throws std::invalid_argument if the stribng is not a valid rational.
+   * For more information about what is a vaid rational string,
+   * see GMP's documentation for mpq_set_str().
+   */
+  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();
+  }
+
+  Rational(const Rational& q) : d_value(q.d_value) {
+    d_value.canonicalize();
+  }
+
+  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() {}
+
+
+  Integer getNumerator() const {
+    return Integer(d_value.get_num());
+  }
+
+  Integer getDenominator() const{
+    return Integer(d_value.get_den());
+  }
+
+
+  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 );
+  }
+
+  std::string toString(int base = 10) const {
+    return d_value.get_str(base);
+  }
+
+
+  friend std::ostream& operator<<(std::ostream& os, const Rational& n);
+
+
+  /**
+   * Computes the hash of the node from the first word of the
+   * numerator, 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 */
+
+std::ostream& operator<<(std::ostream& os, const Rational& n);
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RATIONAL_H */
+