mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

fixup tabu checks to revised representation

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-05 14:24:41 -08:00
parent 71a4801c1d
commit b3e410b5e4
2 changed files with 9 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/ast/sls/sls_bv_valuation.cpp
View file

@ -217,10 +217,9 @@ namespace sls {
SASSERT(!has_overflow(src)); SASSERT(!has_overflow(src));
src.copy_to(nw, dst); src.copy_to(nw, dst);
sup_feasible(dst); sup_feasible(dst);
if (in_range(dst)) { if (can_set(dst))
SASSERT(can_set(dst));
return true; return true;
}
if (dst < m_lo && m_lo < m_hi) // dst < lo < hi if (dst < m_lo && m_lo < m_hi) // dst < lo < hi
return false; return false;
if (is_zero(m_hi)) if (is_zero(m_hi))
@ -238,10 +237,8 @@ namespace sls {
src.copy_to(nw, dst); src.copy_to(nw, dst);
dst.set_bw(bw); dst.set_bw(bw);
inf_feasible(dst); inf_feasible(dst);
if (in_range(dst)) { if (can_set(dst))
SASSERT(can_set(dst));
return true; return true;
}
if (dst > m_lo) if (dst > m_lo)
return false; return false;
@ -350,10 +347,8 @@ namespace sls {
dst[i] = (~m_is_fixed[i] & dst[i]) | (m_is_fixed[i] & m_bits[i]); dst[i] = (~m_is_fixed[i] & dst[i]) | (m_is_fixed[i] & m_bits[i]);
clear_overflow_bits(dst); clear_overflow_bits(dst);
repair_sign_bits(dst); repair_sign_bits(dst);
if (in_range(dst)) { if (try_set(dst))
set(eval, dst);
return true; return true;
}
bool repaired = false; bool repaired = false;
dst.set_bw(bw); dst.set_bw(bw);
if (m_lo < m_hi) { if (m_lo < m_hi) {
@ -373,10 +368,7 @@ namespace sls {
dst.set(i, false); dst.set(i, false);
} }
repair_sign_bits(dst); repair_sign_bits(dst);
if (in_range(dst)) { repaired = try_set(dst);
set(eval, dst);
repaired = true;
}
dst.set_bw(0); dst.set_bw(0);
return repaired; return repaired;
} }
@ -450,10 +442,9 @@ namespace sls {
bool bv_valuation::set_random(random_gen& r) { bool bv_valuation::set_random(random_gen& r) {
get_variant(m_tmp, r); get_variant(m_tmp, r);
repair_sign_bits(m_tmp); repair_sign_bits(m_tmp);
if (in_range(m_tmp)) { if (try_set(m_tmp))
set(eval, m_tmp);
return true; return true;
}
for (unsigned i = 0; i < nw; ++i) for (unsigned i = 0; i < nw; ++i)
m_tmp[i] = random_bits(r); m_tmp[i] = random_bits(r);
clear_overflow_bits(m_tmp); clear_overflow_bits(m_tmp);

2
src/ast/sls/sls_bv_valuation.h
View file

@ -336,7 +336,7 @@ namespace sls {
out << m_bits; out << m_bits;
out << " ev: " << eval; out << " ev: " << eval;
if (!is_zero(m_is_fixed)) if (!is_zero(m_is_fixed))
out << " fix:" << m_is_fixed << " " << m_fixed_values; out << " fixed bits: " << m_is_fixed << " fixed value: " << m_fixed_values;
if (m_lo != m_hi) if (m_lo != m_hi)
out << " [" << m_lo << ", " << m_hi << "["; out << " [" << m_lo << ", " << m_hi << "[";
return out; return out;