1 /********************* */
2 /*! \file integer_cln_imp.cpp
4 ** Top contributors (to current version):
5 ** Tim King, Clark Barrett, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 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
) );
63 void Integer::parseInt(const std::string
& s
, unsigned base
) throw(std::invalid_argument
) {
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
, const std::string
& s
, unsigned base
) throw(std::invalid_argument
) {
91 // Removing leading zeroes, CLN has a bug for these inputs up to and
92 // including CLN v1.3.2.
93 // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
94 size_t pos
= s
.find_first_not_of('0');
95 if(pos
== std::string::npos
) {
96 d_value
= read_integer(flags
, "0", NULL
, NULL
);
98 const char* cstr
= s
.c_str();
99 const char* start
= cstr
+ pos
;
100 const char* end
= cstr
+ s
.length();
101 d_value
= read_integer(flags
, start
, end
, NULL
);
104 std::stringstream ss
;
105 ss
<< "Integer() failed to parse value \"" << s
<< "\" in base " << base
;
106 throw std::invalid_argument(ss
.str());
110 bool Integer::fitsSignedInt() const {
111 // http://www.ginac.de/CLN/cln.html#Conversions
112 // TODO improve performance
113 Assert(s_slowSignedIntMin
<= s_fastSignedIntMin
);
114 Assert(s_fastSignedIntMin
<= s_fastSignedIntMax
);
115 Assert(s_fastSignedIntMax
<= s_slowSignedIntMax
);
117 return (d_value
<= s_fastSignedIntMax
|| d_value
<= s_slowSignedIntMax
) &&
118 (d_value
>= s_fastSignedIntMin
|| d_value
>= s_slowSignedIntMax
);
121 bool Integer::fitsUnsignedInt() const {
122 // TODO improve performance
123 Assert(s_fastUnsignedIntMax
<= s_slowUnsignedIntMax
);
125 (d_value
<= s_fastUnsignedIntMax
|| d_value
<= s_slowUnsignedIntMax
);
128 signed int Integer::getSignedInt() const {
129 // ensure there isn't overflow
130 CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
131 return cln::cl_I_to_int(d_value
);
134 unsigned int Integer::getUnsignedInt() const {
135 // ensure there isn't overflow
136 CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
137 return cln::cl_I_to_uint(d_value
);
140 bool Integer::fitsSignedLong() const {
141 return d_value
<= s_signedLongMax
&& d_value
>= s_signedLongMin
;
144 bool Integer::fitsUnsignedLong() const {
145 return sgn() >= 0 && d_value
<= s_unsignedLongMax
;
148 Integer
Integer::pow(unsigned long int exp
) const {
153 cln::cl_I result
= cln::expt_pos(d_value
, exp
);
154 return Integer(result
);
158 Integer
Integer::modAdd(const Integer
& y
, const Integer
& m
) const
160 cln::cl_modint_ring ry
= cln::find_modint_ring(m
.d_value
);
161 cln::cl_MI xm
= ry
->canonhom(d_value
);
162 cln::cl_MI ym
= ry
->canonhom(y
.d_value
);
163 cln::cl_MI res
= xm
+ ym
;
164 return Integer(ry
->retract(res
));
167 Integer
Integer::modMultiply(const Integer
& y
, const Integer
& m
) const
169 cln::cl_modint_ring ry
= cln::find_modint_ring(m
.d_value
);
170 cln::cl_MI xm
= ry
->canonhom(d_value
);
171 cln::cl_MI ym
= ry
->canonhom(y
.d_value
);
172 cln::cl_MI res
= xm
* ym
;
173 return Integer(ry
->retract(res
));
176 Integer
Integer::modInverse(const Integer
& m
) const
178 PrettyCheckArgument(m
> 0, m
, "m must be greater than zero");
179 cln::cl_modint_ring ry
= cln::find_modint_ring(m
.d_value
);
180 cln::cl_MI xm
= ry
->canonhom(d_value
);
181 /* normalize to modulo m for coprime check */
182 cln::cl_I x
= ry
->retract(xm
);
183 if (x
== 0 || cln::gcd(x
, m
.d_value
) != 1)
187 cln::cl_MI res
= cln::recip(xm
);
188 return Integer(ry
->retract(res
));
190 } /* namespace CVC4 */