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