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

Refactor sls bv evaluation and fix logic checks for bit operations

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-06 01:06:52 -07:00
parent fe7dcb0394
commit 1d3891f8d6
3 changed files with 22 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -926,15 +926,15 @@ namespace sls {
m_tmp.set_bw(a.bw); 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.set_random_at_least(m_tmp, m_rand) && m_tmp != b.bits())
return true; return true;
} }
a.set_sub(m_tmp, b.bits(), m_one); a.set_sub(m_tmp, b.bits(), m_one);
if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_rand)) if (a.set_random_at_most(m_tmp, m_rand) && m_tmp != b.bits())
return true; return true;
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.set_random_at_least(m_tmp, m_rand) && m_tmp != b.bits())
return true; return true;
} }
return false; return false;
@ -1001,9 +1001,11 @@ namespace sls {
}; };
fold_oper(m_tmp2, t, i, f); fold_oper(m_tmp2, t, i, f);
bvval& a = wval(t, i); bvval& a = wval(t, i);
m_tmp.set_bw(a.bw);
for (unsigned j = 0; j < a.nw; ++j) for (unsigned j = 0; j < a.nw; ++j)
m_tmp[j] = e[j] & (~m_tmp2[j] | random_bits()); m_tmp[j] = e[j] & (~m_tmp2[j] | random_bits());
//verbose_stream() << wval(t) << " " << m_tmp << "\n";
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }

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

@ -32,6 +32,8 @@ namespace sls {
for (auto e : ctx.subterms()) for (auto e : ctx.subterms())
set_fixed(e); set_fixed(e);
//ctx.display(verbose_stream());
for (auto lit : ctx.unit_literals()) { for (auto lit : ctx.unit_literals()) {
auto a = ctx.atom(lit.var()); auto a = ctx.atom(lit.var());
if (!a) if (!a)
@ -40,9 +42,12 @@ namespace sls {
init_range(to_app(a), lit.sign()); init_range(to_app(a), lit.sign());
ev.m_fixed.setx(a->get_id(), true, false); ev.m_fixed.setx(a->get_id(), true, false);
} }
//ctx.display(verbose_stream());
for (auto e : ctx.subterms()) for (auto e : ctx.subterms())
propagate_range_up(e); propagate_range_up(e);
//ctx.display(verbose_stream());
} }
void bv_fixed::propagate_range_up(expr* e) { void bv_fixed::propagate_range_up(expr* e) {
@ -150,17 +155,17 @@ namespace sls {
return false; return false;
} }
bool bv_fixed::init_eq(expr* t, rational const& a, bool sign) { bool bv_fixed::init_eq(expr* t, rational const& a, bool sign) {
unsigned lo, hi; unsigned lo, hi;
rational b(0); rational b(0);
// verbose_stream() << mk_bounded_pp(t, m) << " == " << a << "\n";
expr* s = nullptr; expr* s = nullptr;
if (sign) if (sign && true)
// 1 <= t - a // 1 <= t - a
init_range(nullptr, rational(1), t, -a, false); init_range(nullptr, rational(1), t, -a, false);
else if (!sign)
// t - a <= 0 // t - a <= 0
init_range(t, -a, nullptr, rational::zero(), false); init_range(t, -a, nullptr, rational::zero(), false);
if (!sign && bv.is_bv_not(t, s)) { if (!sign && bv.is_bv_not(t, s)) {
for (unsigned i = 0; i < bv.get_bv_size(s); ++i) for (unsigned i = 0; i < bv.get_bv_size(s); ++i)
if (!a.get_bit(i)) if (!a.get_bit(i))
@ -178,11 +183,13 @@ namespace sls {
} }
if (bv.is_extract(t, lo, hi, s)) { if (bv.is_extract(t, lo, hi, s)) {
if (hi == lo) { if (hi == lo) {
sign = sign ? a == 1 : a == 0; auto sign1 = sign ? a == 1 : a == 0;
auto& val = ev.wval(s); auto& val = ev.wval(s);
if (val.try_set_bit(lo, !sign)) if (val.try_set_bit(lo, !sign1))
val.fixed.set(lo, true); val.fixed.set(lo, true);
val.tighten_range(); val.tighten_range();
} }
else if (!sign) { else if (!sign) {
auto& val = ev.wval(s); auto& val = ev.wval(s);
@ -190,8 +197,7 @@ namespace sls {
if (val.try_set_bit(i, a.get_bit(i - lo))) if (val.try_set_bit(i, a.get_bit(i - lo)))
val.fixed.set(i, true); val.fixed.set(i, true);
val.tighten_range(); val.tighten_range();
// verbose_stream() << lo << " " << hi << " " << val << " := " << a << "\n"; }
}
if (!sign && hi + 1 == bv.get_bv_size(s)) { if (!sign && hi + 1 == bv.get_bv_size(s)) {
// s < 2^lo * (a + 1) // s < 2^lo * (a + 1)

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

@ -673,10 +673,7 @@ namespace sls {
// verbose_stream() << "tighten " << m_lo << " " << m_hi << " " << m_bits << "\n"; // verbose_stream() << "tighten " << m_lo << " " << m_hi << " " << m_bits << "\n";
if (m_lo == m_hi) if (m_lo == m_hi)
return; return;
if (is_zero(m_hi))
return;
inf_feasible(m_lo); inf_feasible(m_lo);