mirror of
https://github.com/Z3Prover/z3
synced 2025-04-27 10:55:50 +00:00
na
This commit is contained in:
Nikolaj Bjorner
parent
e19a7f71aa
commit
c0e885931c
2 changed files with 147 additions and 24 deletions
|
|
@ -34,10 +34,71 @@ u256 u256::operator*(u256 const& other) const {
|
|||
return u256(result);
|
||||
}
|
||||
|
||||
u256 u256::operator<<(uint64_t sh) const {
|
||||
u256 r;
|
||||
if (0 == sh || sh >= 256)
|
||||
;
|
||||
else if (sh >= 176)
|
||||
r.m_num[3] = m_num[0] << (sh - 176);
|
||||
else if (sh >= 128) {
|
||||
sh -= 128;
|
||||
r.m_num[2] = m_num[0] << sh;
|
||||
r.m_num[3] = (m_num[1] << sh) | (m_num[0] >> (64 - sh));
|
||||
}
|
||||
else if (sh >= 64) {
|
||||
sh -= 64;
|
||||
r.m_num[1] = m_num[0] << sh;
|
||||
r.m_num[2] = (m_num[1] << sh) | (m_num[0] >> (64 - sh));
|
||||
r.m_num[3] = (m_num[2] << sh) | (m_num[1] >> (64 - sh));
|
||||
}
|
||||
else {
|
||||
r.m_num[0] = m_num[0] << sh;
|
||||
r.m_num[1] = (m_num[1] << sh) | (m_num[0] >> (64 - sh));
|
||||
r.m_num[2] = (m_num[2] << sh) | (m_num[1] >> (64 - sh));
|
||||
r.m_num[3] = (m_num[3] << sh) | (m_num[2] >> (64 - sh));
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
u256 u256::operator>>(uint64_t sh) const {
|
||||
u256 r;
|
||||
if (0 == sh || sh >= 256)
|
||||
;
|
||||
else if (sh >= 176)
|
||||
r.m_num[0] = m_num[3] >> (sh - 176);
|
||||
else if (sh >= 128) {
|
||||
sh -= 128;
|
||||
r.m_num[0] = (m_num[2] >> sh) | (m_num[3] << (64 - sh));
|
||||
r.m_num[1] = (m_num[3] >> sh);
|
||||
}
|
||||
else if (sh >= 64) {
|
||||
sh -= 64;
|
||||
r.m_num[0] = (m_num[1] >> sh) | (m_num[2] << (64 - sh));
|
||||
r.m_num[1] = (m_num[2] >> sh) | (m_num[3] << (64 - sh));
|
||||
r.m_num[2] = (m_num[3] >> sh);
|
||||
}
|
||||
else {
|
||||
r.m_num[0] = (m_num[0] >> sh) | (m_num[1] << (64 - sh));
|
||||
r.m_num[1] = (m_num[1] >> sh) | (m_num[2] << (64 - sh));
|
||||
r.m_num[2] = (m_num[2] >> sh) | (m_num[3] << (64 - sh));
|
||||
r.m_num[3] = (m_num[3] >> sh);
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
u256 u256::operator&(u256 const& other) const {
|
||||
u256 r;
|
||||
for (unsigned i = 0; i < 4; ++i)
|
||||
r.m_num[i] = m_num[i] & other.m_num[i];
|
||||
return r;
|
||||
}
|
||||
|
||||
|
||||
|
||||
u256& u256::operator*=(u256 const& other) {
|
||||
uint64_t result[8];
|
||||
Hacl_Bignum256_mul(const_cast<uint64_t*>(m_num), const_cast<uint64_t*>(other.m_num), result);
|
||||
std::uninitialized_copy(m_num, m_num + sizeof(*this), result);
|
||||
std::uninitialized_copy(m_num, m_num + 4, result);
|
||||
return *this;
|
||||
}
|
||||
|
||||
|
|
@ -58,22 +119,34 @@ u256& u256::inv() {
|
|||
return *this;
|
||||
}
|
||||
|
||||
u256 u256::mod(u256 const& other) const {
|
||||
if (other.is_zero())
|
||||
throw default_exception("mod 0 is not defined");
|
||||
if (other.is_one())
|
||||
return u256();
|
||||
|
||||
u256 r;
|
||||
uint64_t a[8];
|
||||
a[4] = a[5] = a[6] = a[7] = 0;
|
||||
|
||||
if (!other.is_even()) {
|
||||
std::uninitialized_copy(m_num, m_num + 4, a);
|
||||
VERIFY(Hacl_Bignum256_mod(const_cast<uint64_t*>(other.m_num), a, r.m_num));
|
||||
return r;
|
||||
}
|
||||
unsigned tz = other.trailing_zeros();
|
||||
u256 thz = *this >> tz;
|
||||
u256 n = other >> tz;
|
||||
SASSERT(!n.is_even() && n > 1);
|
||||
std::uninitialized_copy(thz.m_num, thz.m_num + 4, a);
|
||||
VERIFY(Hacl_Bignum256_mod(const_cast<uint64_t*>(n.m_num), a, r.m_num));
|
||||
r = r << tz;
|
||||
r += *this & ((u256(1) << tz) - 1);
|
||||
return r;
|
||||
}
|
||||
|
||||
u256 u256::mul_inverse() const {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
||||
/*
|
||||
Write `a mod n` in `res`.
|
||||
|
||||
The argument a is meant to be a 512-bit bignum, i.e. uint64_t[8].
|
||||
The argument n and the outparam res are meant to be 256-bit bignums, i.e. uint64_t[4].
|
||||
|
||||
The function returns false if any of the following preconditions are violated,
|
||||
true otherwise.
|
||||
• 1 < n
|
||||
• n % 2 = 1
|
||||
VERIFY(Hacl_Bignum256_mod(uint64_t *n, uint64_t *a, uint64_t *res));
|
||||
*/
|
||||
|
||||
return *this;
|
||||
}
|
||||
|
||||
|
|
@ -88,9 +161,55 @@ unsigned u256::trailing_zeros() const {
|
|||
}
|
||||
|
||||
u256 u256::gcd(u256 const& other) const {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
if (is_zero())
|
||||
return other;
|
||||
if (other.is_zero())
|
||||
return *this;
|
||||
if (is_one())
|
||||
return *this;
|
||||
if (other.is_one())
|
||||
return other;
|
||||
u256 x = *this;
|
||||
u256 y = other;
|
||||
unsigned tz = x.trailing_zeros();
|
||||
unsigned shift = std::min(y.trailing_zeros(), tz);
|
||||
x = x >> tz;
|
||||
if (x == 1)
|
||||
return x << shift;
|
||||
if (y == 1)
|
||||
return y << shift;
|
||||
if (x == y)
|
||||
return x << shift;
|
||||
do {
|
||||
tz = y.trailing_zeros();
|
||||
y = y >> tz;
|
||||
if (x > y)
|
||||
std::swap(x, y);
|
||||
y -= x;
|
||||
}
|
||||
while (!y.is_zero());
|
||||
return x << shift;
|
||||
}
|
||||
|
||||
|
||||
bool u256::operator<(u256 const& other) const {
|
||||
return 0 != Hacl_Bignum256_lt_mask(const_cast<uint64_t*>(m_num), const_cast<uint64_t*>(other.m_num));
|
||||
}
|
||||
|
||||
bool u256::operator<(uint64_t other) const {
|
||||
uint64_t _other[4];
|
||||
_other[0] = other;
|
||||
_other[1] = _other[2] = _other[3] = 0;
|
||||
return 0 != Hacl_Bignum256_lt_mask(const_cast<uint64_t*>(m_num), _other);
|
||||
}
|
||||
|
||||
bool u256::operator>(uint64_t other) const {
|
||||
uint64_t _other[4];
|
||||
_other[0] = other;
|
||||
_other[1] = _other[2] = _other[3] = 0;
|
||||
return 0 != Hacl_Bignum256_lt_mask(_other, const_cast<uint64_t*>(m_num));
|
||||
}
|
||||
|
||||
|
||||
std::ostream& u256::display(std::ostream& out) const {
|
||||
rational n;
|
||||
|
|
|
|||
|
|
@ -14,7 +14,11 @@ public:
|
|||
u256 operator+(u256 const& other) const { u256 r = *this; return r += other; }
|
||||
u256 operator-(u256 const& other) const { u256 r = *this; return r -= other; }
|
||||
u256 operator-() const { u256 r = *this; return r.inv(); }
|
||||
u256 operator<<(uint64_t sh) const;
|
||||
u256 operator>>(uint64_t sh) const;
|
||||
u256 operator&(u256 const& other) const;
|
||||
|
||||
u256 mod(u256 const& other) const;
|
||||
u256 mul_inverse() const;
|
||||
unsigned trailing_zeros() const;
|
||||
u256 gcd(u256 const& other) const;
|
||||
|
|
@ -27,17 +31,17 @@ public:
|
|||
u256& inv(); /* unary minus */
|
||||
|
||||
// comparisons
|
||||
bool operator==(u256 const& other) const;
|
||||
bool operator!=(u256 const& other) const;
|
||||
bool operator==(u256 const& other) const { return m_num[0] == other.m_num[0] && m_num[1] == other.m_num[1] && m_num[2] == other.m_num[2] && m_num[3] == other.m_num[3]; }
|
||||
bool operator!=(u256 const& other) const { return !(*this == other); }
|
||||
bool operator<(u256 const& other) const;
|
||||
bool operator<=(u256 const& other) const;
|
||||
bool operator>(u256 const& other) const;
|
||||
bool operator>=(u256 const& other) const;
|
||||
bool operator<=(u256 const& other) const { return !(other < *this); }
|
||||
bool operator>(u256 const& other) const { return other < *this; }
|
||||
bool operator>=(u256 const& other) const { return !(*this < other); }
|
||||
|
||||
bool operator<(uint64_t other) const;
|
||||
bool operator<=(uint64_t other) const;
|
||||
bool operator<=(uint64_t other) const { return !(*this > other); }
|
||||
bool operator>(uint64_t other) const;
|
||||
bool operator>=(uint64_t other) const;
|
||||
bool operator>=(uint64_t other) const { return !(*this < other); }
|
||||
|
||||
bool is_zero() const { return m_num[0] == 0 && m_num[1] == 0 && m_num[2] == 0 && m_num[3] == 0; }
|
||||
bool is_one() const { return m_num[0] == 1 && m_num[1] == 0 && m_num[2] == 0 && m_num[3] == 0; }
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue