4b2ab1a79f3949a751e56862da903382ec7f7fce
1 /********************* */
2 /*! \file integer_gmp_imp.h
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief A multiprecision integer constant; wraps a GMP multiprecision
17 ** A multiprecision integer constant; wraps a GMP multiprecision integer.
20 #include "cvc4_public.h"
22 #ifndef __CVC4__INTEGER_H
23 #define __CVC4__INTEGER_H
27 #include "util/gmp_util.h"
36 * Stores the value of the rational is stored in a C++ GMP integer class.
37 * Using this instead of mpz_t allows for easier destruction.
42 * Gets a reference to the gmp data that backs up the integer.
43 * Only accessible to friend classes.
45 const mpz_class
& get_mpz() const { return d_value
; }
48 * Constructs an Integer by copying a GMP C++ primitive.
50 Integer(const mpz_class
& val
) : d_value(val
) {}
54 /** Constructs a rational with the value 0. */
55 Integer() : d_value(0){}
58 * Constructs a Integer from a C string.
59 * Throws std::invalid_argument if the string is not a valid rational.
60 * For more information about what is a valid rational string,
61 * see GMP's documentation for mpq_set_str().
63 explicit Integer(const char * s
, int base
= 10): d_value(s
,base
) {}
64 Integer(const std::string
& s
, unsigned base
= 10) : d_value(s
, base
) {}
66 Integer(const Integer
& q
) : d_value(q
.d_value
) {}
68 Integer( signed int z
) : d_value(z
) {}
69 Integer(unsigned int z
) : d_value(z
) {}
70 Integer( signed long int z
) : d_value(z
) {}
71 Integer(unsigned long int z
) : d_value(z
) {}
76 Integer
& operator=(const Integer
& x
){
77 if(this == &x
) return *this;
82 bool operator==(const Integer
& y
) const {
83 return d_value
== y
.d_value
;
86 Integer
operator-() const{
87 return Integer(-(d_value
));
91 bool operator!=(const Integer
& y
) const {
92 return d_value
!= y
.d_value
;
95 bool operator< (const Integer
& y
) const {
96 return d_value
< y
.d_value
;
99 bool operator<=(const Integer
& y
) const {
100 return d_value
<= y
.d_value
;
103 bool operator> (const Integer
& y
) const {
104 return d_value
> y
.d_value
;
107 bool operator>=(const Integer
& y
) const {
108 return d_value
>= y
.d_value
;
112 Integer
operator+(const Integer
& y
) const{
113 return Integer( d_value
+ y
.d_value
);
116 Integer
operator-(const Integer
& y
) const {
117 return Integer( d_value
- y
.d_value
);
120 Integer
operator*(const Integer
& y
) const {
121 return Integer( d_value
* y
.d_value
);
123 Integer
operator/(const Integer
& y
) const {
124 return Integer( d_value
/ y
.d_value
);
126 Integer
operator%(const Integer
& y
) const {
127 return Integer( d_value
% y
.d_value
);
130 /** Raise this Integer to the power <code>exp</code>.
132 * @param exp the exponent
134 Integer
pow(unsigned long int exp
) const {
136 mpz_pow_ui(result
.get_mpz_t(),d_value
.get_mpz_t(),exp
);
137 return Integer( result
);
140 std::string
toString(int base
= 10) const{
141 return d_value
.get_str(base
);
144 //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
146 long getLong() const { return d_value
.get_si(); }
147 unsigned long getUnsignedLong() const {return d_value
.get_ui(); }
150 * Computes the hash of the node from the first word of the
151 * numerator, the denominator.
153 size_t hash() const {
154 return gmpz_hash(d_value
.get_mpz_t());
157 friend class CVC4::Rational
;
158 };/* class Integer */
160 struct IntegerHashStrategy
{
161 static inline size_t hash(const CVC4::Integer
& i
) {
164 };/* struct IntegerHashStrategy */
166 std::ostream
& operator<<(std::ostream
& os
, const Integer
& n
);
168 }/* CVC4 namespace */
170 #endif /* __CVC4__INTEGER_H */