mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

Refactor verbose logging and fix logic in range adjustment functions in sls bv modules

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-05 12:19:42 -07:00
parent 02393c3a5a
commit 0308a92ea6
5 changed files with 81 additions and 112 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/ast/sls/sls_bv_eval.cpp
View file

@ -885,15 +885,15 @@ namespace sls {
auto const& uninterp = terms.uninterp_occurs(e);
if (uninterp.empty())
return false;
for (auto e : uninterp)
verbose_stream() << mk_bounded_pp(e, m) << " ";
verbose_stream() << "\n";
// for (auto e : uninterp)
// verbose_stream() << mk_bounded_pp(e, m) << " ";
// verbose_stream() << "\n";
expr* t = uninterp[m_rand() % uninterp.size()];
auto& v = wval(t);
if (v.set_random(m_rand)) {
verbose_stream() << "set random " << mk_bounded_pp(t, m) << "\n";
//verbose_stream() << "set random " << mk_bounded_pp(t, m) << "\n";
ctx.new_value_eh(t);
return true;
}
@ -1908,8 +1908,8 @@ namespace sls {
// set a outside of [hi:lo] to random values with preference to 0 or 1 bits
//
bool bv_eval::try_repair_extract(bvect const& e, bvval& a, unsigned lo) {
//verbose_stream() << "repair extract a[" << lo << ":" << lo + e.bw - 1 << "] = " << e << "\n";
if (m_rand(m_config.m_prob_randomize_extract) <= 100) {
// verbose_stream() << "repair extract a[" << lo << ":" << lo + e.bw - 1 << "] = " << e << "\n";
if (false && m_rand(m_config.m_prob_randomize_extract) <= 100) {
a.get_variant(m_tmp, m_rand);
if (0 == (m_rand(2))) {
auto bit = 0 == (m_rand(2));
@ -1927,11 +1927,11 @@ namespace sls {
for (unsigned i = 0; i < e.bw; ++i)
m_tmp.set(i + lo, e.get(i));
m_tmp.set_bw(a.bw);
//verbose_stream() << a << " := " << m_tmp << "\n";
// verbose_stream() << a << " := " << m_tmp << "\n";
if (m_rand(5) != 0 && a.try_set(m_tmp))
return true;
bool ok = a.set_random(m_rand);
//verbose_stream() << "set random " << ok << " " << a << "\n";
// verbose_stream() << "set random " << ok << " " << a << "\n";
return ok;
}
@ -1982,7 +1982,7 @@ namespace sls {
for (unsigned i = 0; i < v.nw; ++i) {
if (0 != (v.fixed[i] & (v.bits()[i] ^ v.eval[i]))) {
verbose_stream() << "Fail to set " << mk_bounded_pp(e, m) << " " << i << " " << v.fixed[i] << " " << v.bits()[i] << " " << v.eval[i] << "\n";
//verbose_stream() << "Fail to set " << mk_bounded_pp(e, m) << " " << i << " " << v.fixed[i] << " " << v.bits()[i] << " " << v.eval[i] << "\n";
v.bits().copy_to(v.nw, v.eval);
return false;
@ -1991,9 +1991,9 @@ namespace sls {
//verbose_stream() << "repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
if (v.commit_eval())
return true;
verbose_stream() << "could not repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
for (expr* arg : *to_app(e))
verbose_stream() << mk_bounded_pp(arg, m) << " " << wval(arg) << "\n";
//verbose_stream() << "could not repair up " << mk_bounded_pp(e, m) << " " << v << "\n";
//for (expr* arg : *to_app(e))
// verbose_stream() << mk_bounded_pp(arg, m) << " " << wval(arg) << "\n";
v.bits().copy_to(v.nw, v.eval);
return false;
}
@ -2007,12 +2007,6 @@ namespace sls {
void bv_eval::commit_eval(expr* p, app* e) {
if (!bv.is_bv(e))
return;
if (e->get_id() == 5) {
//verbose_stream() << e->get_id() << " " << mk_bounded_pp(e, m) << " " << wval(e) << "\n";
//verbose_stream() << "parent " << mk_bounded_pp(p, m) << " := " << wval(p) << "\n";
}
//
SASSERT(wval(e).commit_eval());
VERIFY(wval(e).commit_eval());
}
@ -2103,7 +2097,7 @@ namespace sls {
bool is_true = ctx.is_true(e);
bool is_true_new = bval1(to_app(e));
bool is_true_old = bval1_tmp(to_app(e));
verbose_stream() << "parent " << mk_bounded_pp(e, m) << " " << is_true << " " << is_true_new << " " << is_true_old << "\n";
// verbose_stream() << "parent " << mk_bounded_pp(e, m) << " " << is_true << " " << is_true_new << " " << is_true_old << "\n";
if (is_true == is_true_new && is_true_new != is_true_old)
++make_count;
if (is_true == is_true_old && is_true_new != is_true_old)

2
src/ast/sls/sls_bv_fixed.cpp
View file

@ -41,8 +41,6 @@ namespace sls {
ev.m_fixed.setx(a->get_id(), true, false);
}
for (auto e : ctx.subterms())
propagate_range_up(e);
}

4
src/ast/sls/sls_bv_plugin.cpp
View file

@ -166,10 +166,10 @@ namespace sls {
else if (bv.is_bv(e)) {
log(e, true, false);
IF_VERBOSE(5, verbose_stream() << "repair-up "; trace_repair(true, e));
verbose_stream() << "set random " << m_eval.wval(e) << " --> ";
//verbose_stream() << "set random " << m_eval.wval(e) << " --> ";
auto& v = m_eval.wval(e);
m_eval.set_random(e);
verbose_stream() << m_eval.wval(e) << "\n";
//verbose_stream() << m_eval.wval(e) << "\n";
ctx.new_value_eh(e);
}
else

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

@ -592,59 +592,86 @@ namespace sls {
return index;
}
// The least a' >= a, such that the fixed bits in bits agree with a'.
// 0 if there is no such a'.
void bv_valuation::inf_feasible(bvect& a) const {
unsigned lo_index = diff_index(a);
if (lo_index != 0) {
lo_index--;
SASSERT(a.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))
a.set(i, false);
else if (fixed.get(i))
a.set(i, m_bits.get(i));
}
if (!a.get(lo_index)) {
for (unsigned i = lo_index + 1; i < bw; ++i)
if (!fixed.get(i) && !a.get(i)) {
a.set(i, true);
break;
}
if (lo_index == 0)
return;
--lo_index;
// decrement a[lo_index:0] maximally
SASSERT(a.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))
a.set(i, false);
else if (fixed.get(i))
a.set(i, m_bits.get(i));
}
// the previous value of a[lo_index] was 0.
// a[lo_index:0] was incremented, so no need to adjust bits a[:lo_index+1]
if (a.get(lo_index))
return;
// find the minimal increment within a[:lo_index+1]
for (unsigned i = lo_index + 1; i < bw; ++i) {
if (!fixed.get(i) && !a.get(i)) {
a.set(i, true);
return;
}
}
// there is no feasiable value a' >= a, so find the least
// feasiable value a' >= 0.
for (unsigned i = 0; i < bw; ++i)
if (!fixed.get(i))
a.set(i, false);
}
// The greatest a' <= a, such that the fixed bits in bits agree with a'.
// the greatest a' <= -1 if there is no such a'.
void bv_valuation::sup_feasible(bvect& a) const {
unsigned hi_index = diff_index(a);
if (hi_index != 0) {
hi_index--;
SASSERT(a.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))
a.set(i, true);
else if (fixed.get(i))
a.set(i, m_bits.get(i));
}
if (a.get(hi_index)) {
for (unsigned i = hi_index + 1; i < bw; ++i)
if (!fixed.get(i) && a.get(i)) {
a.set(i, false);
break;
}
if (hi_index == 0)
return;
--hi_index;
SASSERT(a.get(hi_index) != m_bits.get(hi_index));
SASSERT(fixed.get(hi_index));
// increment a[hi_index:0] maximally
for (unsigned i = 0; i <= hi_index; ++i) {
if (!fixed.get(i))
a.set(i, true);
else if (fixed.get(i))
a.set(i, m_bits.get(i));
}
// If a[hi_index:0] was decremented, then no need to adjust bits a[:hi_index+1]
if (!a.get(hi_index))
return;
// find the minimal decrement within a[:hi_index+1]
for (unsigned i = hi_index + 1; i < bw; ++i) {
if (!fixed.get(i) && a.get(i)) {
a.set(i, false);
return;
}
}
// a[hi_index:0] was incremented, but a[:hi_index+1] cannot be decremented.
}
void bv_valuation::tighten_range() {
// verbose_stream() << "tighten " << m_lo << " " << m_hi << " " << m_bits << "\n";
if (m_lo == m_hi)
return;
if (!in_range(m_bits))
m_bits = m_lo;
if (is_zero(m_hi))
return;
@ -658,59 +685,8 @@ namespace sls {
add1(hi1);
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))
m_bits = m_lo;
m_lo.copy_to(nw, m_bits);
if (mod(lo() + 1, rational::power_of_two(bw)) == hi())
for (unsigned i = 0; i < nw; ++i)
@ -720,6 +696,7 @@ namespace sls {
if (hi() < rational::power_of_two(i))
fixed.set(i, true);
// verbose_stream() << "post tighten " << m_lo << " " << m_hi << " " << m_bits << "\n";
SASSERT(well_formed());
}

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

@ -166,8 +166,8 @@ namespace sls {
bool has_range() const { return m_lo != m_hi; }
void tighten_range();
void save_value() { m_tmp = m_bits; }
void restore_value() { m_bits = m_tmp; }
void save_value() { m_bits.copy_to(nw, m_tmp); }
void restore_value() { m_tmp.copy_to(nw, m_bits); }
void clear_overflow_bits(bvect& bits) const {
SASSERT(nw > 0);