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