1 /********************* */
2 /*! \file integer_cln_imp.cpp
4 ** Original author: Tim King
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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 Integer
Integer::oneExtend(uint32_t size
, uint32_t amount
) const {
44 DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size
), size
);
45 cln::cl_byte
range(amount
, size
);
46 cln::cl_I allones
= (cln::cl_I(1) << (size
+ amount
))- 1; // 2^size - 1
47 Integer
temp(allones
);
49 return Integer(cln::deposit_field(allones
, d_value
, range
));
53 Integer
Integer::exactQuotient(const Integer
& y
) const {
54 DebugCheckArgument(y
.divides(*this), y
);
55 return Integer( cln::exquo(d_value
, y
.d_value
) );
59 void Integer::parseInt(const std::string
& s
, unsigned base
) throw(std::invalid_argument
) {
60 cln::cl_read_flags flags
;
61 flags
.syntax
= cln::syntax_integer
;
62 flags
.lsyntax
= cln::lsyntax_standard
;
63 flags
.rational_base
= base
;
65 // infer base in a manner consistent with GMP
67 flags
.lsyntax
= cln::lsyntax_commonlisp
;
69 if(s
[1] == 'X' || s
[1] == 'x') {
70 st
.replace(0, 2, "#x");
71 } else if(s
[1] == 'B' || s
[1] == 'b') {
72 st
.replace(0, 2, "#b");
74 st
.replace(0, 1, "#o");
76 readInt(flags
, st
, base
);
79 flags
.rational_base
= 10;
82 readInt(flags
, s
, base
);
85 void Integer::readInt(const cln::cl_read_flags
& flags
, const std::string
& s
, unsigned base
) throw(std::invalid_argument
) {
87 // Removing leading zeroes, CLN has a bug for these inputs up to and
88 // including CLN v1.3.2.
89 // See http://www.ginac.de/CLN/cln.git/?a=commit;h=4a477b0cc3dd7fbfb23b25090ff8c8869c8fa21a for details.
90 size_t pos
= s
.find_first_not_of('0');
91 if(pos
== std::string::npos
) {
92 d_value
= read_integer(flags
, "0", NULL
, NULL
);
94 const char* cstr
= s
.c_str();
95 const char* start
= cstr
+ pos
;
96 const char* end
= cstr
+ s
.length();
97 d_value
= read_integer(flags
, start
, end
, NULL
);
100 std::stringstream ss
;
101 ss
<< "Integer() failed to parse value \"" << s
<< "\" in base " << base
;
102 throw std::invalid_argument(ss
.str());
106 bool Integer::fitsSignedInt() const {
107 // http://www.ginac.de/CLN/cln.html#Conversions
108 // TODO improve performance
109 Assert(s_slowSignedIntMin
<= s_fastSignedIntMin
);
110 Assert(s_fastSignedIntMin
<= s_fastSignedIntMax
);
111 Assert(s_fastSignedIntMax
<= s_slowSignedIntMax
);
113 return (d_value
<= s_fastSignedIntMax
|| d_value
<= s_slowSignedIntMax
) &&
114 (d_value
>= s_fastSignedIntMin
|| d_value
>= s_slowSignedIntMax
);
117 bool Integer::fitsUnsignedInt() const {
118 // TODO improve performance
119 Assert(s_fastUnsignedIntMax
<= s_slowUnsignedIntMax
);
121 (d_value
<= s_fastUnsignedIntMax
|| d_value
<= s_slowUnsignedIntMax
);
124 signed int Integer::getSignedInt() const {
125 // ensure there isn't overflow
126 CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()");
127 return cln::cl_I_to_int(d_value
);
130 unsigned int Integer::getUnsignedInt() const {
131 // ensure there isn't overflow
132 CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
133 return cln::cl_I_to_uint(d_value
);
136 } /* namespace CVC4 */