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

cleanup

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-04-10 19:09:30 -07:00
parent 974ea7b68d
commit 510534dbd4
3 changed files with 36 additions and 45 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -924,15 +924,15 @@ namespace bv {
bool try_above = m_rand(2) == 0; bool try_above = m_rand(2) == 0;
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_tmp2, m_rand)) if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_rand))
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_tmp2, m_rand)) if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_rand))
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_tmp2, m_rand)) if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_rand))
return true; return true;
} }
return false; return false;
@ -1007,7 +1007,6 @@ namespace bv {
bool sls_eval::try_repair_bxor(bvect const& e, bvval& a, bvval const& b) { bool sls_eval::try_repair_bxor(bvect const& e, bvval& a, bvval const& b) {
for (unsigned i = 0; i < a.nw; ++i) for (unsigned i = 0; i < a.nw; ++i)
m_tmp[i] = e[i] ^ b.bits()[i]; m_tmp[i] = e[i] ^ b.bits()[i];
a.clear_overflow_bits(m_tmp);
return a.set_repair(random_bool(), m_tmp); return a.set_repair(random_bool(), m_tmp);
} }
@ -1230,14 +1229,14 @@ namespace bv {
if (b < p2) { if (b < p2) {
bool coin = m_rand(2) == 0; bool coin = m_rand(2) == 0;
if (coin) if (coin)
r = a.set_random_at_least(p2, m_tmp3, m_rand); r = a.set_random_at_least(p2, m_rand);
if (!r) if (!r)
r = a.set_random_at_most(b, m_tmp3, m_rand); r = a.set_random_at_most(b, m_rand);
if (!coin && !r) if (!coin && !r)
r = a.set_random_at_least(p2, m_tmp3, m_rand); r = a.set_random_at_least(p2, m_rand);
} }
else else
r = a.set_random_in_range(p2, b, m_tmp3, m_rand); r = a.set_random_in_range(p2, b, m_rand);
return r; return r;
} }
@ -1257,16 +1256,16 @@ namespace bv {
bool r = false; bool r = false;
if (p2 < b) if (p2 < b)
// random b <= x < p2 // random b <= x < p2
r = a.set_random_in_range(b, p2_1, m_tmp3, m_rand); r = a.set_random_in_range(b, p2_1, m_rand);
else { else {
// random b <= x or x < p2 // random b <= x or x < p2
bool coin = m_rand(2) == 0; bool coin = m_rand(2) == 0;
if (coin) if (coin)
r = a.set_random_at_most(p2_1, m_tmp3, m_rand); r = a.set_random_at_most(p2_1,m_rand);
if (!r) if (!r)
r = a.set_random_at_least(b, m_tmp3, m_rand); r = a.set_random_at_least(b, m_rand);
if (!r && !coin) if (!r && !coin)
r = a.set_random_at_most(p2_1, m_tmp3, m_rand); r = a.set_random_at_most(p2_1, m_rand);
} }
p2_1.set_bw(0); p2_1.set_bw(0);
return r; return r;
@ -1282,28 +1281,28 @@ namespace bv {
bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) { bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
if (e) { if (e) {
// a <= t // a <= t
return a.set_random_at_most(b.bits(), m_tmp, m_rand); return a.set_random_at_most(b.bits(), m_rand);
} }
else { else {
// a > t // a > t
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;
return a.set_random_at_least(m_tmp, m_tmp2, m_rand); return a.set_random_at_least(m_tmp, m_rand);
} }
} }
bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) { bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
if (e) { if (e) {
// a >= t // a >= t
return a.set_random_at_least(b.bits(), m_tmp, m_rand); return a.set_random_at_least(b.bits(), m_rand);
} }
else { else {
// a < t // a < t
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);
return a.set_random_at_most(m_tmp, m_tmp2, m_rand); return a.set_random_at_most(m_tmp, m_rand);
} }
} }
@ -1377,7 +1376,6 @@ namespace bv {
unsigned n = b.bits().to_nat(e.bw); unsigned n = b.bits().to_nat(e.bw);
for (unsigned i = e.bw; i-- > e.bw - n;) for (unsigned i = e.bw; i-- > e.bw - n;)
t.set(i, a.get_bit(i)); t.set(i, a.get_bit(i));
a.clear_overflow_bits(t);
if (a.set_repair(random_bool(), t)) if (a.set_repair(random_bool(), t))
return true; return true;
} }
@ -1527,7 +1525,6 @@ namespace bv {
t[i] = a.bits()[i]; t[i] = a.bits()[i];
t.set(b.bw - 1, a.is_ones(e)); t.set(b.bw - 1, a.is_ones(e));
} }
a.clear_overflow_bits(t);
if (a.set_repair(random_bool(), t)) if (a.set_repair(random_bool(), t))
return true; return true;
} }
@ -1541,13 +1538,10 @@ namespace bv {
a.get_variant(t, m_rand); a.get_variant(t, m_rand);
t.set(b.bw - 1, a.is_ones(e)); t.set(b.bw - 1, a.is_ones(e));
} }
a.clear_overflow_bits(t);
if (a.set_repair(random_bool(), t)) if (a.set_repair(random_bool(), t))
return true; return true;
} }
return a.set_random(m_rand);
a.get_variant(t, m_rand);
return a.set_repair(random_bool(), t);
} }
/* /*
@ -1645,7 +1639,6 @@ namespace bv {
m_tmp2.set(b.msb(m_tmp2), false); m_tmp2.set(b.msb(m_tmp2), false);
while (a.set_add(m_tmp3, m_tmp, m_tmp2)) while (a.set_add(m_tmp3, m_tmp, m_tmp2))
m_tmp2.set(b.msb(m_tmp2), false); m_tmp2.set(b.msb(m_tmp2), false);
a.clear_overflow_bits(m_tmp3);
return a.set_repair(true, m_tmp3); return a.set_repair(true, m_tmp3);
} }
else { else {
@ -1723,7 +1716,6 @@ namespace bv {
m_tmp[i] = random_bits(); m_tmp[i] = random_bits();
a.set_sub(m_tmp2, a.bits(), e); a.set_sub(m_tmp2, a.bits(), e);
set_div(m_tmp2, m_tmp, a.bw, m_tmp3, m_tmp4); set_div(m_tmp2, m_tmp, a.bw, m_tmp3, m_tmp4);
a.clear_overflow_bits(m_tmp3);
return b.set_repair(random_bool(), m_tmp3); return b.set_repair(random_bool(), m_tmp3);
} }
} }

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

@ -244,34 +244,35 @@ namespace bv {
return true; return true;
} }
bool sls_valuation::set_random_at_most(bvect const& src, bvect& tmp, random_gen& r) { bool sls_valuation::set_random_at_most(bvect const& src, random_gen& r) {
if (!get_at_most(src, tmp)) if (!get_at_most(src, m_tmp))
return false; return false;
if (is_zero(tmp) || (0 != r(10))) if (is_zero(m_tmp) || (0 != r(10)))
return try_set(tmp); return try_set(m_tmp);
// random value below tmp // random value below tmp
set_random_below(tmp, r); set_random_below(m_tmp, r);
return (can_set(tmp) || get_at_most(src, tmp)) && try_set(tmp); return (can_set(m_tmp) || get_at_most(src, m_tmp)) && try_set(m_tmp);
} }
bool sls_valuation::set_random_at_least(bvect const& src, bvect& tmp, random_gen& r) { bool sls_valuation::set_random_at_least(bvect const& src, random_gen& r) {
if (!get_at_least(src, tmp)) if (!get_at_least(src, m_tmp))
return false; return false;
if (is_ones(tmp) || (0 != r(10))) if (is_ones(m_tmp) || (0 != r(10)))
return try_set(tmp); return try_set(m_tmp);
// random value at least tmp // random value at least tmp
set_random_above(tmp, r); set_random_above(m_tmp, r);
return (can_set(tmp) || get_at_least(src, tmp)) && try_set(tmp); return (can_set(m_tmp) || get_at_least(src, m_tmp)) && try_set(m_tmp);
} }
bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r) { bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r) {
if (0 == r() % 2) { bvect& tmp = m_tmp;
if (0 == r(2)) {
if (!get_at_least(lo, tmp)) if (!get_at_least(lo, tmp))
return false; return false;
SASSERT(in_range(tmp)); SASSERT(in_range(tmp));
@ -342,7 +343,7 @@ namespace bv {
bool sls_valuation::set_repair(bool try_down, bvect& dst) { bool sls_valuation::set_repair(bool try_down, bvect& dst) {
for (unsigned i = 0; i < nw; ++i) for (unsigned i = 0; i < nw; ++i)
dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]); dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]);
clear_overflow_bits(dst);
repair_sign_bits(dst); repair_sign_bits(dst);
if (in_range(dst)) { if (in_range(dst)) {
set(eval, dst); set(eval, dst);
@ -674,6 +675,4 @@ namespace bv {
c += get_num_1bits(src[i]); c += get_num_1bits(src[i]);
return c == 1; return c == 1;
} }
} }

6
src/ast/sls/sls_valuation.h
View file

@ -226,9 +226,9 @@ namespace bv {
bool get_at_most(bvect const& src, bvect& dst) const; bool get_at_most(bvect const& src, bvect& dst) const;
bool get_at_least(bvect const& src, bvect& dst) const; bool get_at_least(bvect const& src, bvect& dst) const;
bool set_random_at_most(bvect const& src, bvect& tmp, random_gen& r); bool set_random_at_most(bvect const& src, random_gen& r);
bool set_random_at_least(bvect const& src, bvect& tmp, random_gen& r); bool set_random_at_least(bvect const& src, random_gen& r);
bool set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r); bool set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r);
bool set_repair(bool try_down, bvect& dst); bool set_repair(bool try_down, bvect& dst);
void set_random_above(bvect& dst, random_gen& r); void set_random_above(bvect& dst, random_gen& r);