diff options
Diffstat (limited to 'src/util/integer.h')
-rw-r--r-- | src/util/integer.h | 154 |
1 files changed, 6 insertions, 148 deletions
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 |