1 /*++
2 Copyright (c) 2006 Microsoft Corporation
3
4 Module Name:
5
6 integer.h
7
8 Abstract:
9
10 machine s_integer wrapper
11
12 Author:
13
14 Leonardo de Moura (leonardo) 2007-06-01.
15
16 Revision History:
17
18 --*/
19 #pragma once
20
21 #include "util/rational.h"
22
23 class s_integer {
24 int m_val;
25 static s_integer m_zero;
26 static s_integer m_one;
27 static s_integer m_minus_one;
28 public:
29
hash()30 unsigned hash() const {
31 return m_val;
32 }
33
operatorhash_proc34 struct hash_proc { unsigned operator()(s_integer const& r) const { return r.hash(); } };
operatoreq_proc35 struct eq_proc { bool operator()(s_integer const& r1, s_integer const& r2) const { return r1 == r2; } };
36
swap(s_integer & n)37 void swap(s_integer & n) {
38 std::swap(m_val, n.m_val);
39 }
40
41 std::string to_string() const;
42
43 public:
s_integer()44 s_integer(): m_val(0) {}
s_integer(int n)45 explicit s_integer(int n):m_val(n) {}
46 struct i64 {};
s_integer(int64_t i,i64)47 explicit s_integer(int64_t i, i64):m_val(static_cast<int>(i)) {}
48 struct ui64 {};
s_integer(uint64_t i,ui64)49 explicit s_integer(uint64_t i, ui64):m_val(static_cast<int>(i)) {}
50 explicit s_integer(const char * str);
s_integer(const rational & r)51 explicit s_integer(const rational & r):m_val(static_cast<int>(r.get_int64())) {}
52
reset()53 void reset() { m_val = 0; }
54
is_big()55 static bool is_big() { return false; }
is_int()56 static bool is_int() { return true; }
is_s_integer()57 static bool is_s_integer() { return true; }
is_int64()58 static bool is_int64() { return true; }
is_uint64()59 static bool is_uint64() { return true; }
get_int()60 int get_int() const { return m_val; }
get_int64()61 int64_t get_int64() const { return m_val; }
get_uint64()62 uint64_t get_uint64() const { return m_val; }
is_unsigned()63 static bool is_unsigned() { return true; }
get_unsigned()64 unsigned get_unsigned() const { return static_cast<unsigned>(m_val); }
get_s_integer()65 s_integer const& get_s_integer() const { return *this; }
get_infinitesimal()66 s_integer const& get_infinitesimal() const { return zero(); }
is_rational()67 static bool is_rational() { return true; }
get_rational()68 s_integer const& get_rational() const { return *this; }
numerator(const s_integer & r)69 friend inline s_integer numerator(const s_integer & r) { return r; }
denominator(const s_integer & r)70 friend inline s_integer denominator(const s_integer & r) { return one(); }
71 s_integer & operator+=(const s_integer & r) { m_val += r.m_val; return *this; }
72 s_integer & operator-=(const s_integer & r) { m_val -= r.m_val; return *this; }
73 s_integer & operator*=(const s_integer & r) { m_val *= r.m_val; return *this; }
74 s_integer & operator/=(const s_integer & r) { m_val /= r.m_val; return *this; }
75 s_integer & operator%=(const s_integer & r) { m_val %= r.m_val; return *this; }
div(const s_integer & r1,const s_integer & r2)76 friend inline s_integer div(const s_integer & r1, const s_integer & r2) { return s_integer(r1.m_val / r2.m_val); }
mod(const s_integer & r1,const s_integer & r2)77 friend inline s_integer mod(const s_integer & r1, const s_integer & r2) {
78 s_integer r = r1;
79 r %= r2;
80 if (r.is_neg()) {
81 r += r2;
82 }
83 return r;
84 }
85 s_integer & operator++() { m_val++; return *this; }
86 const s_integer operator++(int) { s_integer tmp(*this); ++(*this); return tmp; }
87 s_integer & operator--() { m_val--; return *this; }
88 const s_integer operator--(int) { s_integer tmp(*this); --(*this); return tmp; }
89 friend inline bool operator==(const s_integer & r1, const s_integer & r2) { return r1.m_val == r2.m_val; }
90 friend inline bool operator<(const s_integer & r1, const s_integer & r2) { return r1.m_val < r2.m_val; }
neg()91 void neg() { m_val = -m_val; }
is_zero()92 bool is_zero() const { return m_val == 0; }
is_one()93 bool is_one() const { return m_val == 1; }
is_minus_one()94 bool is_minus_one() const { return m_val == -1; }
is_neg()95 bool is_neg() const { return m_val < 0; }
is_pos()96 bool is_pos() const { return m_val > 0; }
is_nonneg()97 bool is_nonneg() const {return m_val >= 0; }
is_nonpos()98 bool is_nonpos() const { return m_val <= 0; }
is_even()99 bool is_even() const { return (!(m_val & 0x1)); }
floor(const s_integer & r)100 friend inline s_integer floor(const s_integer & r) { return r; }
ceil(const s_integer & r)101 friend inline s_integer ceil(const s_integer & r) { return r; }
expt(int n)102 s_integer expt(int n) const {
103 s_integer result(1);
104 for (int i = 0; i < n; i++) {
105 result *= *this;
106 }
107 return result;
108 }
109
zero()110 static const s_integer & zero() { return m_zero; }
one()111 static const s_integer & one() { return m_one; }
minus_one()112 static const s_integer & minus_one() { return m_minus_one; }
113 // Perform: this += c * k
addmul(const s_integer & c,const s_integer & k)114 void addmul(const s_integer & c, const s_integer & k) { m_val += c.m_val * k.m_val; }
submul(const s_integer & c,const s_integer & k)115 void submul(const s_integer & c, const s_integer & k) { m_val -= c.m_val * k.m_val; }
116 friend inline std::ostream & operator<<(std::ostream & target, const s_integer & r) {
117 target << r.m_val;
118 return target;
119 }
120
to_rational()121 rational to_rational() const { return rational(m_val); }
122 };
123
124 inline bool operator!=(const s_integer & r1, const s_integer & r2) { return !operator==(r1, r2); }
125 inline bool operator>(const s_integer & r1, const s_integer & r2) { return operator<(r2, r1); }
126 inline bool operator<=(const s_integer & r1, const s_integer & r2) { return !operator>(r1, r2); }
127 inline bool operator>=(const s_integer & r1, const s_integer & r2) { return !operator<(r1, r2); }
128 inline s_integer operator+(const s_integer & r1, const s_integer & r2) { return s_integer(r1) += r2; }
129 inline s_integer operator-(const s_integer & r1, const s_integer & r2) { return s_integer(r1) -= r2; }
130 inline s_integer operator-(const s_integer & r) { s_integer result(r); result.neg(); return result; }
131 inline s_integer operator*(const s_integer & r1, const s_integer & r2) { return s_integer(r1) *= r2; }
132 inline s_integer operator/(const s_integer & r1, const s_integer & r2) { return s_integer(r1) /= r2; }
133 inline s_integer operator%(const s_integer & r1, const s_integer & r2) { return s_integer(r1) %= r2; }
134 s_integer power(const s_integer & r, unsigned p);
135 s_integer gcd(const s_integer & r1, const s_integer & r2);
136 s_integer lcm(const s_integer & r1, const s_integer & r2);
abs(const s_integer & r)137 inline s_integer abs(const s_integer & r) {
138 s_integer result(r);
139 if (result.is_neg()) {
140 result.neg();
141 }
142 return result;
143 }
144
145
146