From 3b8d92b17c17aadfa920f36a1ab631e36c70e00e Mon Sep 17 00:00:00 2001 From: Tim King Date: Fri, 26 Mar 2010 22:37:12 +0000 Subject: Added GMP backed Rational and Integer classes, and white box tests for them. You may have to reconfigure after this update. --- src/util/Makefile.am | 6 +- src/util/integer.cpp | 7 ++ src/util/integer.h | 157 +++++++++++++++++++++++++++++++++++++++++++++ src/util/rational.cpp | 8 +++ src/util/rational.h | 172 ++++++++++++++++++++++++++++++++++++++++++++++++++ 5 files changed, 349 insertions(+), 1 deletion(-) create mode 100644 src/util/integer.cpp create mode 100644 src/util/integer.h create mode 100644 src/util/rational.cpp create mode 100644 src/util/rational.h (limited to 'src') 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 +#include + + +#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 (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 +#include +#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 */ + -- cgit v1.2.3