Skip to content

Commit

Permalink
fixes to bv-sls
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Apr 7, 2024
1 parent d7c0e17 commit bab7ca2
Show file tree
Hide file tree
Showing 8 changed files with 267 additions and 274 deletions.
31 changes: 18 additions & 13 deletions src/ast/sls/bv_sls.cpp
View file
Expand Up @@ -124,6 +124,7 @@ namespace bv {
};
m_eval.init_eval(m_terms.assertions(), eval);
init_repair();
// m_engine_init = false;
}

std::pair<bool, app*> sls::next_to_repair() {
Expand Down Expand Up @@ -161,17 +162,18 @@ namespace bv {
lbool sls::search1() {
// init and init_eval were invoked
unsigned n = 0;
for (; n++ < m_config.m_max_repairs && m.inc(); ) {
for (; n < m_config.m_max_repairs && m.inc(); ) {
auto [down, e] = next_to_repair();
if (!e)
return l_true;

trace_repair(down, e);

IF_VERBOSE(20, trace_repair(down, e));
++m_stats.m_moves;

if (down)
if (down) {
try_repair_down(e);
++n;
}
else
try_repair_up(e);
}
Expand All @@ -181,12 +183,13 @@ namespace bv {
lbool sls::search2() {
lbool res = l_undef;
if (m_stats.m_restarts == 0)
res = m_engine();
res = m_engine(),
m_engine_init = true;
else if (m_stats.m_restarts % 1000 == 0)
res = m_engine.search_loop();
res = m_engine.search_loop(),
m_engine_init = true;
if (res != l_undef)
m_engine_model = true;
m_engine_init = true;
return res;
}

Expand All @@ -203,7 +206,7 @@ namespace bv {
if (res != l_undef)
break;
trace();
// res = search2();
//res = search2();
if (res != l_undef)
break;
reinit_eval();
Expand All @@ -223,6 +226,7 @@ namespace bv {
VERIFY(m_eval.wval(e).commit_eval());
}

IF_VERBOSE(3, verbose_stream() << "done\n");
for (auto p : m_terms.parents(e))
m_repair_up.insert(p->get_id());

Expand Down Expand Up @@ -256,6 +260,7 @@ namespace bv {
}
}
}
IF_VERBOSE(3, verbose_stream() << "init-repair " << mk_bounded_pp(e, m) << "\n");
// repair was not successful, so reset the state to find a different way to repair
init_repair();
}
Expand All @@ -265,7 +270,7 @@ namespace bv {
if (m_terms.is_assertion(e))
m_repair_roots.insert(e->get_id());
else if (!m_eval.repair_up(e)) {
//m_repair_roots.insert(e->get_id());
IF_VERBOSE(2, verbose_stream() << "repair-up "; trace_repair(true, e));
init_repair();
}
else {
Expand Down Expand Up @@ -366,14 +371,14 @@ namespace bv {
m_engine.updt_params(q);
}

void sls::trace_repair(bool down, expr* e) {
IF_VERBOSE(20,
std::ostream& sls::trace_repair(bool down, expr* e) {
verbose_stream() << (down ? "d #" : "u #")
<< e->get_id() << ": "
<< mk_bounded_pp(e, m, 1) << " ";
if (bv.is_bv(e)) verbose_stream() << m_eval.wval(e) << " " << (m_eval.is_fixed0(e) ? "fixed " : " ");
if (m.is_bool(e)) verbose_stream() << m_eval.bval0(e) << " ";
verbose_stream() << "\n");
verbose_stream() << "\n";
return verbose_stream();
}

void sls::trace() {
Expand Down
2 changes: 1 addition & 1 deletion src/ast/sls/bv_sls.h
View file
Expand Up @@ -68,7 +68,7 @@ namespace bv {
void reinit_eval();
void init_repair();
void trace();
void trace_repair(bool down, expr* e);
std::ostream& trace_repair(bool down, expr* e);

indexed_uint_set m_to_repair;
void init_repair_candidates();
Expand Down
70 changes: 18 additions & 52 deletions src/ast/sls/bv_sls_eval.cpp
View file
Expand Up @@ -1351,55 +1351,18 @@ namespace bv {
return false;
}

bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) {
if (true) {
bool sls_eval::try_repair_ashr(bvect const& e, bvval & a, bvval& b, unsigned i) {
if (i == 0)
return try_repair_ashr0(e, a, b);
else
return try_repair_ashr1(e, a, b);
}

if (i == 0) {
unsigned sh = b.to_nat(b.bw);
if (sh == 0)
return a.try_set(e);
else if (sh >= b.bw) {
if (e.get(a.bw - 1))
return a.try_set_bit(a.bw - 1, true);
else
return a.try_set_bit(a.bw - 1, false);
}
else {
// e = a >> sh
// a[bw-1:sh] = e[bw-sh-1:0]
// a[sh-1:0] = a[sh-1:0]
// ignore sign
for (unsigned i = sh; i < a.bw; ++i)
m_tmp.set(i, e.get(i - sh));
for (unsigned i = 0; i < sh; ++i)
m_tmp.set(i, a.get_bit(i));
a.clear_overflow_bits(m_tmp);
return a.try_set(m_tmp);
}
}
else {
// NB. blind sub-range of possible values for b
SASSERT(i == 1);
unsigned sh = m_rand(a.bw + 1);
b.set(m_tmp, sh);
return b.try_set(m_tmp);
}
}

bool sls_eval::try_repair_lshr(bvect const& e, bvval& a, bvval& b, unsigned i) {
#if 0
return try_repair_ashr(e, a, b, i);
#else
if (i == 0)
return try_repair_lshr0(e, a, b);
else
return try_repair_lshr1(e, a, b);
#endif
}

/**
Expand Down Expand Up @@ -1427,22 +1390,25 @@ namespace bv {
return true;
}


unsigned sh = b.to_nat(b.bw);
if (sh == 0 && a.try_set(e))
return true;
else if (sh >= b.bw)
return true;
else if (sh < b.bw && m_rand(20) != 0) {
// e = a >> sh
// a[bw-1:sh] = e[bw-sh-1:0]
// a[sh-1:0] = a[sh-1:0]
for (unsigned i = sh; i < a.bw; ++i)
t.set(i, e.get(i - sh));
for (unsigned i = 0; i < sh; ++i)
t.set(i, a.get_bit(i));
a.clear_overflow_bits(t);
if (a.try_set(t))
if (m_rand(20) != 0) {
if (sh == 0 && a.try_set(e))
return true;
else if (sh >= b.bw)
return true;
else if (sh < b.bw && m_rand(20) != 0) {
// e = a >> sh
// a[bw-1:sh] = e[bw-sh-1:0]
// a[sh-1:0] = a[sh-1:0]
for (unsigned i = sh; i < a.bw; ++i)
t.set(i, e.get(i - sh));
for (unsigned i = 0; i < sh; ++i)
t.set(i, a.get_bit(i));
a.clear_overflow_bits(t);
if (a.try_set(t))
return true;
}
}

//bool r = try_repair_ashr(e, a, const_cast<bvval&>(b), 0);
Expand Down

0 comments on commit bab7ca2

Please sign in to comment.