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

logging and fixes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-28 15:45:29 -07:00
parent 677b5b4196
commit 43a5b3dde0
6 changed files with 55 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -366,7 +366,7 @@ namespace bv {
unsigned bw = 0;
for (unsigned i = e->get_num_args(); i-- > 0; ) {
auto const& a = wval(e->get_arg(i));
for (unsigned j = 0; j < a.bw; ++j)
for (unsigned j = 0; false && j < a.bw; ++j)
val.eval.set(j + bw, a.get_bit(j));
bw += a.bw;
}
@ -1269,6 +1269,7 @@ namespace bv {
}
bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
verbose_stream() << "try-repair-ule " << e << " " << a << " " << b << "\n";
if (e) {
// a <= t
return a.set_random_at_most(b.bits(), m_rand);
@ -1284,6 +1285,7 @@ namespace bv {
}
bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
verbose_stream() << "try-repair-uge " << e << " " << a << " " << b << "\n";
if (e) {
// a >= t
return a.set_random_at_least(b.bits(), m_rand);
@ -1821,7 +1823,7 @@ namespace bv {
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)
for (unsigned j = e->get_num_args() - 1; 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)
@ -1923,7 +1925,6 @@ namespace bv {
void sls_eval::commit_eval(app* e) {
if (!bv.is_bv(e))
return;
// verbose_stream() << mk_bounded_pp(e, m) << " " << wval(e) << "\n";
//
SASSERT(wval(e).commit_eval());
VERIFY(wval(e).commit_eval());
@ -1939,7 +1940,9 @@ namespace bv {
return false;
if (m.is_bool(e))
return bval0(e) == bval1(e);
if (bv.is_bv(e)) {
if (bv.is_bv(e)) {
if (m.is_ite(e))
return true;
auto const& v = eval(e);
return v.eval == v.bits();
}

18
src/ast/sls/bv_sls_fixed.cpp
View file

@ -285,17 +285,21 @@ namespace bv {
if (!is_app(_e))
return;
auto e = to_app(_e);
if (!bv.is_bv(e))
return;
auto& v = ev.wval(e);
if (all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); })) {
for (unsigned i = 0; i < v.bw; ++i)
v.fixed.set(i, true);
if (e->get_family_id() == bv.get_family_id() && all_of(*e, [&](expr* arg) { return ev.is_fixed0(arg); })) {
if (bv.is_bv(e)) {
auto& v = ev.wval(e);
for (unsigned i = 0; i < v.bw; ++i)
v.fixed.set(i, true);
}
ev.m_fixed.setx(e->get_id(), true, false);
return;
}
if (!bv.is_bv(e))
return;
auto& v = ev.wval(e);
if (m.is_ite(e)) {
auto& val_th = ev.wval(e->get_arg(1));
auto& val_el = ev.wval(e->get_arg(2));

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

@ -85,9 +85,12 @@ namespace sls {
}
bool bv_plugin::is_sat() {
bool is_sat = true;
for (auto t : ctx.subterms())
if (is_app(t) && bv.is_bv(t) && !m_eval.eval_is_correct(to_app(t)))
return false;
if (is_app(t) && bv.is_bv(t) && to_app(t)->get_family_id() == bv.get_fid() && !m_eval.eval_is_correct(to_app(t))) {
ctx.new_value_eh(t);
is_sat = false;
}
return true;
}
@ -107,38 +110,44 @@ namespace sls {
bool bv_plugin::repair_down(app* e) {
unsigned n = e->get_num_args();
bool status = true;
if (n == 0 || m_eval.is_uninterpreted(e) || m_eval.eval_is_correct(e))
return true;
goto done;
if (n == 2) {
auto d1 = get_depth(e->get_arg(0));
auto d2 = get_depth(e->get_arg(1));
unsigned s = ctx.rand(d1 + d2 + 2);
if (s <= d1 && m_eval.repair_down(e, 0))
return true;
goto done;
if (m_eval.repair_down(e, 1))
return true;
goto done;
if (m_eval.repair_down(e, 0))
return true;
goto done;
}
else {
unsigned s = ctx.rand(n);
for (unsigned i = 0; i < n; ++i) {
auto j = (i + s) % n;
if (m_eval.repair_down(e, j))
return true;
goto done;
}
}
return false;
status = false;
done:
log(e, false, status);
return status;
}
void bv_plugin::repair_up(app* e) {
if (m_eval.repair_up(e)) {
if (!m_eval.eval_is_correct(e)) {
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";
}
log(e, true, true);
SASSERT(m_eval.eval_is_correct(e));
if (m.is_bool(e)) {
if (ctx.is_true(e) != m_eval.bval1(e))
@ -148,10 +157,14 @@ namespace sls {
ctx.new_value_eh(e);
}
else if (bv.is_bv(e)) {
log(e, true, false);
IF_VERBOSE(5, verbose_stream() << "repair-up "; trace_repair(true, e));
m_eval.set_random(e);
ctx.new_value_eh(e);
}
else
log(e, true, false);
}
void bv_plugin::repair_literal(sat::literal lit) {
@ -175,4 +188,14 @@ namespace sls {
IF_VERBOSE(2, verbose_stream()
<< "(bvsls :restarts " << m_stats.m_restarts << ")\n");
}
}
void bv_plugin::log(expr* e, bool up_down, bool success) {
// unsigned value = 0;
// if (bv.is_bv(e))
// value = svector_hash<unsigned_hash>()(m_eval.wval(e).bits());
IF_VERBOSE(2, verbose_stream() << mk_bounded_pp(e, m) << " " << (up_down?"u":"d") << " " << (success ? "S" : "F");
// if (bv.is_bv(e)) verbose_stream() << " " << m_eval.wval(e).bits();
verbose_stream() << "\n");
}
}

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

@ -36,6 +36,8 @@ namespace sls {
bool can_propagate();
bool is_bv_predicate(expr* e);
void log(expr* e, bool up_down, bool success);
public:
bv_plugin(context& ctx);
~bv_plugin() override {}

2
src/ast/sls/sls_context.cpp
View file

@ -86,8 +86,6 @@ namespace sls {
if (m_new_constraint || !unsat().empty())
return l_undef;
//verbose_stream() << unsat().size() << " " << m_new_constraint << "\n";
if (all_of(m_plugins, [&](auto* p) { return !p || p->is_sat(); })) {
model_ref mdl = alloc(model, m);
for (expr* e : subterms())

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

@ -135,6 +135,7 @@ namespace bv {
digit_t bits(unsigned i) const { return m_bits[i]; }
bvect const& bits() const { return m_bits; }
bool commit_eval();
bool is_fixed() const { for (unsigned i = bw; i-- > 0; ) if (!fixed.get(i)) return false; return true; }
bool get_bit(unsigned i) const { return m_bits.get(i); }
bool try_set_bit(unsigned i, bool b) {