1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
|
/********************* */
/*! \file integer_cln_imp.cpp
** \verbatim
** Top contributors (to current version):
** Tim King, Aina Niemetz, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include "util/integer.h"
#include <sstream>
#include <string>
#include "cvc4autoconfig.h"
#ifndef CVC4_CLN_IMP
# error "This source should only ever be built if CVC4_CLN_IMP is on !"
#endif /* CVC4_CLN_IMP */
#include "base/cvc4_assert.h"
using namespace std;
namespace CVC4 {
signed int Integer::s_fastSignedIntMin = -(1<<29);
signed int Integer::s_fastSignedIntMax = (1<<29)-1;
signed long Integer::s_slowSignedIntMin = (signed long) std::numeric_limits<signed int>::min();
signed long Integer::s_slowSignedIntMax = (signed long) std::numeric_limits<signed int>::max();
unsigned int Integer::s_fastUnsignedIntMax = (1<<29)-1;
unsigned long Integer::s_slowUnsignedIntMax = (unsigned long) std::numeric_limits<unsigned int>::max();
unsigned long Integer::s_signedLongMin = std::numeric_limits<signed long>::min();
unsigned long Integer::s_signedLongMax = std::numeric_limits<signed long>::max();
unsigned long Integer::s_unsignedLongMax = std::numeric_limits<unsigned long>::max();
Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
cln::cl_byte range(amount, size);
cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1
Integer temp(allones);
return Integer(cln::deposit_field(allones, d_value, range));
}
Integer Integer::exactQuotient(const Integer& y) const {
DebugCheckArgument(y.divides(*this), y);
return Integer( cln::exquo(d_value, y.d_value) );
}
void Integer::parseInt(const std::string& s, unsigned base)
{
cln::cl_read_flags flags;
flags.syntax = cln::syntax_integer;
flags.lsyntax = cln::lsyntax_standard;
flags.rational_base = base;
if(base == 0) {
// infer base in a manner consistent with GMP
if(s[0] == '0') {
flags.lsyntax = cln::lsyntax_commonlisp;
std::string st = s;
if(s[1] == 'X' || s[1] == 'x') {
st.replace(0, 2, "#x");
} else if(s[1] == 'B' || s[1] == 'b') {
st.replace(0, 2, "#b");
} else {
st.replace(0, 1, "#o");
}
readInt(flags, st, base);
return;
} else {
flags.rational_base = 10;
}
}
readInt(flags, s, base);
}
void Integer::readInt(const cln::cl_read_flags& flags,
const std::string& s,
unsigned base)
{
try {
// Removing leading zeroes, CLN has a bug for these inputs up to and
// including CLN v1.3.2.
// See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
size_t pos = s.find_first_not_of('0');
if(pos == std::string::npos) {
d_value = read_integer(flags, "0", NULL, NULL);
} else {
const char* cstr = s.c_str();
const char* start = cstr + pos;
const char* end = cstr + s.length();
d_value = read_integer(flags, start, end, NULL);
}
} catch(...) {
std::stringstream ss;
ss << "Integer() failed to parse value \"" << s << "\" in base " << base;
throw std::invalid_argument(ss.str());
}
}
bool Integer::fitsSignedInt() const {
// http://www.ginac.de/CLN/cln.html#Conversions
// TODO improve performance
Assert(s_slowSignedIntMin <= s_fastSignedIntMin);
Assert(s_fastSignedIntMin <= s_fastSignedIntMax);
Assert(s_fastSignedIntMax <= s_slowSignedIntMax);
return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax) &&
(d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax);
}
bool Integer::fitsUnsignedInt() const {
// TODO improve performance
Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax);
return sgn() >= 0 &&
(d_value <= s_fastUnsignedIntMax || d_value <= s_slowUnsignedIntMax);
}
signed int Integer::getSignedInt() const {
// ensure there isn't overflow
CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
return cln::cl_I_to_int(d_value);
}
unsigned int Integer::getUnsignedInt() const {
// ensure there isn't overflow
CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
return cln::cl_I_to_uint(d_value);
}
bool Integer::fitsSignedLong() const {
return d_value <= s_signedLongMax && d_value >= s_signedLongMin;
}
bool Integer::fitsUnsignedLong() const {
return sgn() >= 0 && d_value <= s_unsignedLongMax;
}
Integer Integer::pow(unsigned long int exp) const {
if (exp == 0) {
return Integer(1);
} else {
Assert(exp > 0);
cln::cl_I result = cln::expt_pos(d_value, exp);
return Integer(result);
}
}
Integer Integer::modAdd(const Integer& y, const Integer& m) const
{
cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
cln::cl_MI xm = ry->canonhom(d_value);
cln::cl_MI ym = ry->canonhom(y.d_value);
cln::cl_MI res = xm + ym;
return Integer(ry->retract(res));
}
Integer Integer::modMultiply(const Integer& y, const Integer& m) const
{
cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
cln::cl_MI xm = ry->canonhom(d_value);
cln::cl_MI ym = ry->canonhom(y.d_value);
cln::cl_MI res = xm * ym;
return Integer(ry->retract(res));
}
Integer Integer::modInverse(const Integer& m) const
{
PrettyCheckArgument(m > 0, m, "m must be greater than zero");
cln::cl_modint_ring ry = cln::find_modint_ring(m.d_value);
cln::cl_MI xm = ry->canonhom(d_value);
/* normalize to modulo m for coprime check */
cln::cl_I x = ry->retract(xm);
if (x == 0 || cln::gcd(x, m.d_value) != 1)
{
return Integer(-1);
}
cln::cl_MI res = cln::recip(xm);
return Integer(ry->retract(res));
}
} /* namespace CVC4 */
|
