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

na

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-08-27 11:45:27 -07:00
parent 3bcd98b653
commit 4146e938e8
2 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -640,13 +640,6 @@ namespace bv {
if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) { if (e->get_family_id() == bv.get_family_id() && try_repair_bv(e, i)) {
commit_eval(to_app(e->get_arg(i))); commit_eval(to_app(e->get_arg(i)));
ctx.new_value_eh(e->get_arg(i)); ctx.new_value_eh(e->get_arg(i));
if (bv.is_bv(e)) {
auto& val = eval(e);
if (val.eval != val.bits()) {
commit_eval(e);
ctx.new_value_eh(e);
}
}
return true; return true;
} }
return false; return false;
@ -852,6 +845,7 @@ namespace bv {
} }
else { else {
bool try_above = m_rand(2) == 0; bool try_above = m_rand(2) == 0;
m_tmp.set_bw(a.bw);
if (try_above) { if (try_above) {
a.set_add(m_tmp, b.bits(), m_one); a.set_add(m_tmp, b.bits(), m_one);
if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_rand)) if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_rand))
@ -1249,6 +1243,7 @@ namespace bv {
} }
else { else {
// a > t // a > t
m_tmp.set_bw(a.bw);
a.set_add(m_tmp, b.bits(), m_one); a.set_add(m_tmp, b.bits(), m_one);
if (a.is_zero(m_tmp)) if (a.is_zero(m_tmp))
return false; return false;
@ -1263,6 +1258,7 @@ namespace bv {
} }
else { else {
// a < t // a < t
m_tmp.set_bw(a.bw);
if (b.is_zero()) if (b.is_zero())
return false; return false;
a.set_sub(m_tmp, b.bits(), m_one); a.set_sub(m_tmp, b.bits(), m_one);
@ -1895,6 +1891,9 @@ namespace bv {
void sls_eval::commit_eval(app* e) { void sls_eval::commit_eval(app* e) {
if (!bv.is_bv(e)) if (!bv.is_bv(e))
return; return;
//verbose_stream() << mk_bounded_pp(e, m) << " " << wval(e) << "\n";
//
// SASSERT(wval(e).commit_eval());
VERIFY(wval(e).commit_eval()); VERIFY(wval(e).commit_eval());
} }

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

@ -140,6 +140,11 @@ namespace sls {
verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n"; verbose_stream() << "incorrect eval #" << e->get_id() << " " << mk_bounded_pp(e, m) << "\n";
} }
SASSERT(m_eval.eval_is_correct(e)); SASSERT(m_eval.eval_is_correct(e));
if (m.is_bool(e)) {
if (ctx.is_true(e) != m_eval.bval1(e))
ctx.flip(ctx.atom2bool_var(e));
}
else
ctx.new_value_eh(e); ctx.new_value_eh(e);
} }
else if (bv.is_bv(e)) { else if (bv.is_bv(e)) {