diff options
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 5 | ||||
-rw-r--r-- | src/util/bitvector.cpp | 16 | ||||
-rw-r--r-- | src/util/bitvector.h | 99 | ||||
-rw-r--r-- | src/util/gmp_util.h | 28 | ||||
-rw-r--r-- | src/util/integer.cpp | 2 | ||||
-rw-r--r-- | src/util/integer.h | 14 | ||||
-rw-r--r-- | src/util/rational.h | 9 |
7 files changed, 154 insertions, 19 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 6597c8b48..7820acb0a 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -25,4 +25,7 @@ libutil_la_SOURCES = \ rational.h \ rational.cpp \ integer.h \ - integer.cpp + integer.cpp \ + bitvector.h \ + bitvector.cpp \ + gmp_util.h diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp new file mode 100644 index 000000000..bea06f71a --- /dev/null +++ b/src/util/bitvector.cpp @@ -0,0 +1,16 @@ +/* + * bitvector.cpp + * + * Created on: Apr 5, 2010 + * Author: dejan + */ + +#include "bitvector.h" + +namespace CVC4 { + +std::ostream& operator <<(std::ostream& os, const BitVector& bv) { + return os << bv.toString(); +} + +} diff --git a/src/util/bitvector.h b/src/util/bitvector.h new file mode 100644 index 000000000..3859fa407 --- /dev/null +++ b/src/util/bitvector.h @@ -0,0 +1,99 @@ +/* + * bitvector.h + * + * Created on: Mar 31, 2010 + * Author: dejan + */ + +#ifndef __CVC4__BITVECTOR_H_ +#define __CVC4__BITVECTOR_H_ + +#include <string> +#include <iostream> +#include "util/gmp_util.h" + +namespace CVC4 { + +class BitVector { + +private: + + unsigned d_size; + mpz_class d_value; + + BitVector(unsigned size, const mpz_class& val) : d_size(size), d_value(val) {} + +public: + + BitVector(unsigned size = 0) + : d_size(size), d_value(0) {} + + BitVector(unsigned size, unsigned int z) + : d_size(size), d_value(z) {} + + BitVector(unsigned size, unsigned long int z) + : d_size(size), d_value(z) {} + + BitVector(unsigned size, const BitVector& q) + : d_size(size), d_value(q.d_value) {} + + ~BitVector() {} + + BitVector& operator =(const BitVector& x) { + if(this == &x) + return *this; + d_value = x.d_value; + return *this; + } + + bool operator ==(const BitVector& y) const { + if (d_size != y.d_size) return false; + return d_value == y.d_value; + } + + bool operator !=(const BitVector& y) const { + if (d_size == y.d_size) return false; + return d_value != y.d_value; + } + + BitVector operator +(const BitVector& y) const { + return BitVector(std::max(d_size, y.d_size), d_value + y.d_value); + } + + BitVector operator -(const BitVector& y) const { + return *this + ~y + 1; + } + + BitVector operator -() const { + return ~(*this) + 1; + } + + BitVector operator *(const BitVector& y) const { + return BitVector(d_size, d_value * y.d_value); + } + + BitVector operator ~() const { + return BitVector(d_size, d_value); + } + + size_t hash() const { + return gmpz_hash(d_value.get_mpz_t()); + } + + std::string toString(unsigned int base = 2) const { + return d_value.get_str(base); + } +}; + +struct BitVectorHashStrategy { + static inline size_t hash(const BitVector& bv) { + return bv.hash(); + } +}; + +std::ostream& operator <<(std::ostream& os, const BitVector& bv); + +} + + +#endif /* __CVC4__BITVECTOR_H_ */ diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h new file mode 100644 index 000000000..1849974cd --- /dev/null +++ b/src/util/gmp_util.h @@ -0,0 +1,28 @@ +/* + * gmp.h + * + * Created on: Apr 5, 2010 + * Author: dejan + */ + +#ifndef __CVC4__GMP_H_ +#define __CVC4__GMP_H_ + +#include <gmpxx.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; + } + +} + +#endif /* __CVC4__GMP_H_ */ diff --git a/src/util/integer.cpp b/src/util/integer.cpp index 3a7851eec..a26f2108f 100644 --- a/src/util/integer.cpp +++ b/src/util/integer.cpp @@ -23,6 +23,6 @@ using namespace CVC4; -std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n){ +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 index c1e5d90ea..2aa8b711a 100644 --- a/src/util/integer.h +++ b/src/util/integer.h @@ -18,22 +18,12 @@ #ifndef __CVC4__INTEGER_H #define __CVC4__INTEGER_H -#include <gmpxx.h> #include <string> +#include <iostream> +#include "util/gmp_util.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 { diff --git a/src/util/rational.h b/src/util/rational.h index 48b00899a..e4f0e2bb7 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -24,9 +24,8 @@ #ifndef __CVC4__RATIONAL_H #define __CVC4__RATIONAL_H -#include <gmpxx.h> #include <string> -#include "integer.h" +#include "util/integer.h" namespace CVC4 { @@ -76,20 +75,20 @@ 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) { 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) { d_value.canonicalize(); } - Rational(const Integer& n, const Integer& d): + Rational(const Integer& n, const Integer& d) : d_value(n.get_mpz(), d.get_mpz()) { d_value.canonicalize(); |