diff options
Diffstat (limited to 'src/util/integer_gmp_imp.h')
-rw-r--r-- | src/util/integer_gmp_imp.h | 168 |
1 files changed, 168 insertions, 0 deletions
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 */ |