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

update debugging information for new core

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-10-21 15:24:44 -07:00
parent ad5fa9433f
commit 53adc2afee
2 changed files with 13 additions and 33 deletions
Download patch file Download diff file Expand all files Collapse all files

34
src/sat/smt/arith_solver.cpp
View file

@ -561,6 +561,9 @@ namespace arith {
void solver::dbg_finalize_model(model& mdl) { void solver::dbg_finalize_model(model& mdl) {
if (m_not_handled) if (m_not_handled)
return; return;
// this is already handled in general in euf_model.cpp
return;
bool found_bad = false; bool found_bad = false;
for (unsigned v = 0; v < get_num_vars(); ++v) { for (unsigned v = 0; v < get_num_vars(); ++v) {
if (!is_bool(v)) if (!is_bool(v))
@ -583,35 +586,8 @@ namespace arith {
if (!found_bad && value == get_phase(n->bool_var())) if (!found_bad && value == get_phase(n->bool_var()))
continue; continue;
TRACE("arith", TRACE("arith", ctx.display_validation_failure(tout << *b << "\n", mdl, n));
ptr_vector<expr> nodes; IF_VERBOSE(0, ctx.display_validation_failure(verbose_stream() << *b << "\n", mdl, n));
expr_mark marks;
nodes.push_back(n->get_expr());
for (unsigned i = 0; i < nodes.size(); ++i) {
expr* r = nodes[i];
if (marks.is_marked(r))
continue;
marks.mark(r);
if (is_app(r))
for (expr* arg : *to_app(r))
nodes.push_back(arg);
expr_ref rval(m);
expr_ref mval = mdl(r);
if (ctx.get_egraph().find(r))
rval = mdl(ctx.get_egraph().find(r)->get_root()->get_expr());
tout << r->get_id() << ": " << mk_bounded_pp(r, m, 1) << " := " << mval;
if (rval != mval) tout << " " << rval;
tout << "\n";
});
TRACE("arith",
tout << eval << " " << value << " " << ctx.bpp(n) << "\n";
tout << mdl << "\n";
s().display(tout););
IF_VERBOSE(0,
verbose_stream() << eval << " " << value << " " << ctx.bpp(n) << "\n";
verbose_stream() << n->bool_var() << " " << n->value() << " " << get_phase(n->bool_var()) << " " << ctx.bpp(n) << "\n";
verbose_stream() << *b << "\n";);
IF_VERBOSE(0, ctx.display_validation_failure(verbose_stream(), mdl, n));
UNREACHABLE(); UNREACHABLE();
} }
} }

10
src/sat/smt/euf_model.cpp
View file

@ -287,17 +287,20 @@ namespace euf {
nodes.push_back(n); nodes.push_back(n);
for (unsigned i = 0; i < nodes.size(); ++i) { for (unsigned i = 0; i < nodes.size(); ++i) {
euf::enode* r = nodes[i]; euf::enode* r = nodes[i];
if (r->is_marked1()) if (!r || r->is_marked1())
continue; continue;
r->mark1(); r->mark1();
for (auto* arg : euf::enode_args(r)) if (is_app(r->get_expr()))
nodes.push_back(arg); for (auto* arg : *r->get_app())
nodes.push_back(get_enode(arg));
expr_ref val = mdl(r->get_expr()); expr_ref val = mdl(r->get_expr());
expr_ref sval(m); expr_ref sval(m);
th_rewriter rw(m); th_rewriter rw(m);
rw(val, sval); rw(val, sval);
expr_ref mval = mdl(r->get_root()->get_expr()); expr_ref mval = mdl(r->get_root()->get_expr());
if (mval != sval) { if (mval != sval) {
if (r->bool_var() != sat::null_bool_var)
out << "b" << r->bool_var() << " ";
out << bpp(r) << " :=\neval: " << sval << "\nmval: " << mval << "\n"; out << bpp(r) << " :=\neval: " << sval << "\nmval: " << mval << "\n";
continue; continue;
} }
@ -309,6 +312,7 @@ namespace euf {
out << bpp(r) << " :=\neval: " << sval << "\nmval: " << bval << "\n"; out << bpp(r) << " :=\neval: " << sval << "\nmval: " << bval << "\n";
} }
for (euf::enode* r : nodes) for (euf::enode* r : nodes)
if (r)
r->unmark1(); r->unmark1();
out << mdl << "\n"; out << mdl << "\n";
} }