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

reshuffle priorities on multiplication allow non-determinism.

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-04-03 08:19:57 -07:00
parent 01e47bfe26
commit 972d35204c
2 changed files with 63 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

24
src/ast/sls/bv_sls_eval.cpp
View file

@ -1049,16 +1049,16 @@ namespace bv {
if (b.is_zero(e)) { if (b.is_zero(e)) {
a.get_variant(m_tmp, m_rand); a.get_variant(m_tmp, m_rand);
for (unsigned i = 0; i < b.bw - parity_b; ++i) if (m_rand(10) != 0)
m_tmp.set(i, false); for (unsigned i = 0; i < b.bw - parity_b; ++i)
m_tmp.set(i, false);
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
if (b.is_zero()) if (b.is_zero() || m_rand(20) == 0) {
return a.set_random(m_rand); a.get_variant(m_tmp, m_rand);
return a.set_repair(random_bool(), m_tmp);
if (m_rand(20) == 0) }
return a.set_random(m_rand);
#if 0 #if 0
verbose_stream() << "solve for " << e << "\n"; verbose_stream() << "solve for " << e << "\n";
@ -1342,11 +1342,11 @@ namespace bv {
return false; return false;
} }
bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) { bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) {
if (i == 0) if (i == 0)
return try_repair_ashr0(e, a, b); return try_repair_ashr0(e, a, b);
else else
return try_repair_ashr1(e, a, b); return try_repair_ashr1(e, a, b);
} }
bool sls_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) { bool sls_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) {

64
src/ast/sls/sls_valuation.cpp
View file

@ -497,8 +497,6 @@ namespace bv {
} }
void sls_valuation::add_range(rational l, rational h) { void sls_valuation::add_range(rational l, rational h) {
//return;
//verbose_stream() << *this << " " << l << " " << h << " --> \n";
l = mod(l, rational::power_of_two(bw)); l = mod(l, rational::power_of_two(bw));
h = mod(h, rational::power_of_two(bw)); h = mod(h, rational::power_of_two(bw));
@ -555,17 +553,6 @@ namespace bv {
// //
// update bits based on ranges // update bits based on ranges
// tighten lo/hi based on fixed bits.
// lo[bit_i] != fixedbit[bit_i]
// let bit_i be most significant bit position of disagreement.
// if fixedbit = 1, lo = 0, increment lo
// if fixedbit = 0, lo = 1, lo := fixed & bits
// (hi-1)[bit_i] != fixedbit[bit_i]
// if fixedbit = 0, hi-1 = 1, set hi-1 := 0, maximize below bit_i
// if fixedbit = 1, hi-1 = 0, hi := fixed & bits
// tighten fixed bits based on lo/hi
// lo + 1 = hi -> set bits = lo
// lo < hi, set most significant bits based on hi
// //
unsigned sls_valuation::diff_index(bvect const& a) const { unsigned sls_valuation::diff_index(bvect const& a) const {
@ -638,6 +625,57 @@ namespace bv {
add1(hi1); add1(hi1);
hi1.copy_to(nw, m_hi); hi1.copy_to(nw, m_hi);
/*
unsigned lo_index = 0, hi_index = 0;
for (unsigned i = nw; i-- > 0; ) {
auto lo_diff = (fixed[i] & (m_bits[i] ^ m_lo[i]));
if (lo_diff != 0 && lo_index == 0)
lo_index = 1 + i * 8 * sizeof(digit_t) + log2(lo_diff);
auto hi_diff = (fixed[i] & (m_bits[i] ^ hi1[i]));
if (hi_diff != 0 && hi_index == 0)
hi_index = 1 + i * 8 * sizeof(digit_t) + log2(hi_diff);
}
if (lo_index != 0) {
lo_index--;
SASSERT(m_lo.get(lo_index) != m_bits.get(lo_index));
SASSERT(fixed.get(lo_index));
for (unsigned i = 0; i <= lo_index; ++i) {
if (!fixed.get(i))
m_lo.set(i, false);
else if (fixed.get(i))
m_lo.set(i, m_bits.get(i));
}
if (!m_bits.get(lo_index)) {
for (unsigned i = lo_index + 1; i < bw; ++i)
if (!fixed.get(i) && !m_lo.get(i)) {
m_lo.set(i, true);
break;
}
}
}
if (hi_index != 0) {
hi_index--;
SASSERT(hi1.get(hi_index) != m_bits.get(hi_index));
SASSERT(fixed.get(hi_index));
for (unsigned i = 0; i <= hi_index; ++i) {
if (!fixed.get(i))
hi1.set(i, true);
else if (fixed.get(i))
hi1.set(i, m_bits.get(i));
}
if (m_bits.get(hi_index)) {
for (unsigned i = hi_index + 1; i < bw; ++i)
if (!fixed.get(i) && hi1.get(i)) {
hi1.set(i, false);
break;
}
}
add1(hi1);
hi1.copy_to(nw, m_hi);
}
*/
if (has_range() && !in_range(m_bits)) if (has_range() && !in_range(m_bits))
m_bits = m_lo; m_bits = m_lo;