mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

fix overflow

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-01-11 16:42:58 -08:00
parent 3d33d28f8c
commit 1acaed69c6
2 changed files with 26 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/sat/smt/polysat/viable.cpp
View file

@ -88,6 +88,7 @@ namespace polysat {
m_explain_kind = explain_t::none;
m_num_bits = c.size(v);
m_fixed_bits.init(v);
m_explain.reset();
init_overlaps(v);
check_fixed_bits(v, value);
check_disequal_lin(v, value);
@ -97,6 +98,7 @@ namespace polysat {
entry* e = find_overlap(w, layer, value);
if (!e)
continue;
m_explain.push_back({ e, value });
m_explain_kind = explain_t::assignment;
return false;
@ -113,9 +115,7 @@ namespace polysat {
init_overlaps(v);
m_explain_kind = explain_t::none;
for (unsigned rounds = 0; rounds < 10; ) {
auto n = find_overlap(lo);
if (m_explain_kind == explain_t::conflict)
@ -191,18 +191,24 @@ namespace polysat {
unsigned b_width = e->bit_width;
SASSERT(b_width <= v_width);
auto hi = e->interval.hi_val();
auto lo = e->interval.lo_val();
auto const& hi = e->interval.hi_val();
auto const& lo = e->interval.lo_val();
if (b_width == v_width) {
val = hi;
SASSERT(0 <= val && val <= c.var2pdd(m_var).max_value());
return;
}
auto p2b = rational::power_of_two(b_width);
rational val2 = clear_lower_bits(val, b_width);
if (lo <= mod(val, p2b) && hi < lo)
val2 += p2b;
val = val2 + hi;
if (lo <= mod(val, p2b) && hi < lo) {
val2 += p2b;
if (val2 == rational::power_of_two(v_width))
val2 = 0;
}
val = val2 + hi;
SASSERT(0 <= hi && hi < p2b);
SASSERT(0 <= val && val <= c.var2pdd(m_var).max_value());
}

14
src/util/rational.h
View file

@ -98,7 +98,19 @@ public:
void display_hex(std::ostream & out, unsigned num_bits) const { SASSERT(is_int()); return m().display_hex(out, m_val.numerator(), num_bits); }
void display_bin(std::ostream & out, unsigned num_bits) const { SASSERT(is_int()); return m().display_bin(out, m_val.numerator(), num_bits); }
struct as_bin_wrapper {
rational const& r;
unsigned bw;
};
as_bin_wrapper as_bin(unsigned bw) const { return as_bin_wrapper{*this, bw}; }
friend inline std::ostream& operator<<(std::ostream& out, as_bin_wrapper const& ab) {
ab.r.display_bin(out, ab.bw);
return out;
}
std::ostream& display_bin(std::ostream& out, unsigned num_bits) const { SASSERT(is_int()); m().display_bin(out, m_val.numerator(), num_bits); return out; }
bool is_uint64() const { return m().is_uint64(m_val); }