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
|
/********************* */
/*! \file integer_gmp_imp.cpp
** \verbatim
** Top contributors (to current version):
** Tim King, Aina Niemetz, Liana Hadarean
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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 A multi-precision rational constant.
**
** A multi-precision rational constant.
**/
#include "util/integer.h"
#include <cmath>
#include <sstream>
#include <string>
#include "cvc4autoconfig.h"
#include "base/check.h"
#include "util/rational.h"
#ifndef CVC4_GMP_IMP
# error "This source should only ever be built if CVC4_GMP_IMP is on !"
#endif /* CVC4_GMP_IMP */
using namespace std;
namespace CVC4 {
Integer::Integer(const char* s, unsigned base)
: d_value(s, base)
{}
Integer::Integer(const std::string& s, unsigned base)
: d_value(s, base)
{}
bool Integer::fitsSignedInt() const {
return d_value.fits_sint_p();
}
bool Integer::fitsUnsignedInt() const {
return d_value.fits_uint_p();
}
signed int Integer::getSignedInt() const {
// ensure there isn't overflow
CheckArgument(d_value <= std::numeric_limits<int>::max(), this,
"Overflow detected in Integer::getSignedInt().");
CheckArgument(d_value >= std::numeric_limits<int>::min(), this,
"Overflow detected in Integer::getSignedInt().");
CheckArgument(fitsSignedInt(), this,
"Overflow detected in Integer::getSignedInt().");
return (signed int) d_value.get_si();
}
unsigned int Integer::getUnsignedInt() const {
// ensure there isn't overflow
CheckArgument(d_value <= std::numeric_limits<unsigned int>::max(), this,
"Overflow detected in Integer::getUnsignedInt()");
CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this,
"Overflow detected in Integer::getUnsignedInt()");
CheckArgument(fitsSignedInt(), this,
"Overflow detected in Integer::getUnsignedInt()");
return (unsigned int) d_value.get_ui();
}
bool Integer::fitsSignedLong() const {
return d_value.fits_slong_p();
}
bool Integer::fitsUnsignedLong() const {
return d_value.fits_ulong_p();
}
Integer Integer::oneExtend(uint32_t size, uint32_t amount) const {
// check that the size is accurate
DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size);
mpz_class res = d_value;
for (unsigned i = size; i < size + amount; ++i) {
mpz_setbit(res.get_mpz_t(), i);
}
return Integer(res);
}
Integer Integer::exactQuotient(const Integer& y) const {
DebugCheckArgument(y.divides(*this), y);
mpz_class q;
mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
return Integer( q );
}
Integer Integer::modAdd(const Integer& y, const Integer& m) const
{
mpz_class res;
mpz_add(res.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
mpz_mod(res.get_mpz_t(), res.get_mpz_t(), m.d_value.get_mpz_t());
return Integer(res);
}
Integer Integer::modMultiply(const Integer& y, const Integer& m) const
{
mpz_class res;
mpz_mul(res.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t());
mpz_mod(res.get_mpz_t(), res.get_mpz_t(), m.d_value.get_mpz_t());
return Integer(res);
}
Integer Integer::modInverse(const Integer& m) const
{
PrettyCheckArgument(m > 0, m, "m must be greater than zero");
mpz_class res;
if (mpz_invert(res.get_mpz_t(), d_value.get_mpz_t(), m.d_value.get_mpz_t())
== 0)
{
return Integer(-1);
}
return Integer(res);
}
} /* namespace CVC4 */
|
