mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

avoid rationals for addition in checked_int64

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-19 20:41:42 -08:00
parent 07031798ec
commit 620bd81269
1 changed files with 28 additions and 38 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

66
src/util/checked_int64.h
View file

@ -116,58 +116,48 @@ public:
const checked_int64 operator--(int) { checked_int64 tmp(*this); --(*this); return tmp; }
checked_int64& operator+=(checked_int64 const& other) {
if (CHECK && m_value > 0 && other.m_value > 0 &&
(m_value > INT_MAX || other.m_value > INT_MAX)) {
rational r(r64(m_value) + r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
}
m_value = r.get_int64();
return *this;
if (CHECK) {
uint64 x = static_cast<uint64>(m_value);
uint64 y = static_cast<uint64>(other.m_value);
int64 r = static_cast<int64>(x + y);
if (m_value > 0 && other.m_value > 0 && r <= 0) throw overflow_exception();
if (m_value < 0 && other.m_value < 0 && r >= 0) throw overflow_exception();
m_value = r;
}
if (CHECK && m_value < 0 && other.m_value < 0 &&
(m_value < INT_MIN || other.m_value < INT_MIN)) {
rational r(r64(m_value) + r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
}
m_value = r.get_int64();
return *this;
else {
m_value += other.m_value;
}
m_value += other.m_value;
return *this;
}
checked_int64& operator-=(checked_int64 const& other) {
if (CHECK && m_value > 0 && other.m_value < 0 &&
(m_value > INT_MAX || other.m_value < INT_MIN)) {
rational r(r64(m_value) - r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
}
m_value = r.get_int64();
return *this;
if (CHECK) {
uint64 x = static_cast<uint64>(m_value);
uint64 y = static_cast<uint64>(other.m_value);
int64 r = static_cast<int64>(x - y);
if (m_value > 0 && other.m_value < 0 && r <= 0) throw overflow_exception();
if (m_value < 0 && other.m_value > 0 && r >= 0) throw overflow_exception();
m_value = r;
}
if (CHECK && m_value < 0 && other.m_value > 0 &&
(m_value < INT_MIN || other.m_value > INT_MAX)) {
rational r(r64(m_value) - r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
}
m_value = r.get_int64();
return *this;
else {
m_value -= other.m_value;
}
m_value -= other.m_value;
return *this;
}
checked_int64& operator*=(checked_int64 const& other) {
if (CHECK) {
rational r(r64(m_value) * r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
if (INT_MIN < m_value && m_value <= INT_MAX && INT_MIN < other.m_value && other.m_value <= INT_MAX) {
m_value *= other.m_value;
}
// TBD: could be tuned by using known techniques or 128-bit arithmetic.
else {
rational r(r64(m_value) * r64(other.m_value));
if (!r.is_int64()) {
throw overflow_exception();
}
m_value = r.get_int64();
}
m_value = r.get_int64();
}
else {
m_value *= other.m_value;