mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fixup repairs

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-27 04:30:18 -07:00
parent 6488e33915
commit a0ae5c8d5e
3 changed files with 22 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -777,8 +777,8 @@ namespace bv {
return try_repair_zero_ext(assign_value(e), wval(e, 0));
case OP_SIGN_EXT:
return try_repair_sign_ext(assign_value(e), wval(e, 0));
case OP_CONCAT:
return try_repair_concat(assign_value(e), wval(e, 0), wval(e, 1), i);
case OP_CONCAT:
return try_repair_concat(e, i);
case OP_EXTRACT: {
unsigned hi, lo;
expr* arg;
@ -1218,18 +1218,18 @@ namespace bv {
a.set_sub(p2_1, p2, m_one);
p2_1.set_bw(a.bw);
bool r = false;
if (p2 < b)
if (b < p2)
// random b <= x < p2
r = a.set_random_in_range(b, p2_1, m_rand);
else {
// random b <= x or x < p2
bool coin = m_rand(2) == 0;
if (coin)
r = a.set_random_at_most(p2_1,m_rand);
r = a.set_random_at_most(p2_1, m_rand);
if (!r)
r = a.set_random_at_least(b, m_rand);
r = a.set_random_at_least(b, m_rand);
if (!r && !coin)
r = a.set_random_at_most(p2_1, m_rand);
r = a.set_random_at_most(p2_1, m_rand);
}
p2_1.set_bw(0);
return r;
@ -1790,21 +1790,16 @@ namespace bv {
return a.try_set(m_tmp);
}
bool sls_eval::try_repair_concat(bvect const& e, bvval& a, bvval& b, unsigned idx) {
bool r = false;
if (idx == 0) {
for (unsigned i = 0; i < a.bw; ++i)
m_tmp.set(i, e.get(i + b.bw));
a.clear_overflow_bits(m_tmp);
r = a.try_set(m_tmp);
}
else {
for (unsigned i = 0; i < b.bw; ++i)
m_tmp.set(i, e.get(i));
b.clear_overflow_bits(m_tmp);
r = b.try_set(m_tmp);
}
return r;
bool sls_eval::try_repair_concat(app* e, unsigned idx) {
unsigned bw = 0;
auto& ve = assign_value(e);
for (unsigned j = 0; j < idx; ++j)
bw += bv.get_bv_size(e->get_arg(j));
auto& a = wval(e, idx);
for (unsigned i = 0; i < a.bw; ++i)
m_tmp.set(i, ve.get(i + bw));
a.clear_overflow_bits(m_tmp);
return a.try_set(m_tmp);
}
//

2
src/ast/sls/bv_sls_eval.h
View file

@ -104,7 +104,7 @@ namespace bv {
bool try_repair_umul_ovfl(bool e, bvval& a, bvval& b, unsigned i);
bool try_repair_zero_ext(bvect const& e, bvval& a);
bool try_repair_sign_ext(bvect const& e, bvval& a);
bool try_repair_concat(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_concat(app* e, unsigned i);
bool try_repair_extract(bvect const& e, bvval& a, unsigned lo);
bool try_repair_comp(bvect const& e, bvval& a, bvval& b, unsigned i);
bool try_repair_eq(bool is_true, bvval& a, bvval const& b);

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

@ -279,14 +279,10 @@ namespace bv {
SASSERT(in_range(tmp));
if (hi < tmp)
return false;
if (is_ones(tmp) || (0 == r() % 2))
return try_set(tmp);
set_random_above(tmp, r);
round_down(tmp, [&](bvect const& t) { return hi >= t && in_range(t); });
if (in_range(tmp) && lo <= tmp && hi >= tmp)
return try_set(tmp);
return get_at_least(lo, tmp) && hi >= tmp && try_set(tmp);
if (in_range(tmp) || get_at_least(lo, tmp))
return lo <= tmp && tmp <= hi && try_set(tmp);
}
else {
if (!get_at_most(hi, tmp))
@ -294,14 +290,12 @@ namespace bv {
SASSERT(in_range(tmp));
if (lo > tmp)
return false;
if (is_zero(tmp) || (0 == r() % 2))
return try_set(tmp);
set_random_below(tmp, r);
round_up(tmp, [&](bvect const& t) { return lo <= t && in_range(t); });
if (in_range(tmp) && lo <= tmp && hi >= tmp)
return try_set(tmp);
return get_at_most(hi, tmp) && lo <= tmp && try_set(tmp);
if (in_range(tmp) || get_at_most(hi, tmp))
return lo <= tmp && tmp <= hi && try_set(tmp);
}
return false;
}
void sls_valuation::round_down(bvect& dst, std::function<bool(bvect const&)> const& is_feasible) {