mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

extended debugging for sat.euf

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-22 17:05:27 -05:00
parent c24d445886
commit 4c6d7158cb
2 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -612,8 +612,7 @@ namespace arith {
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(verbose_stream()));
IF_VERBOSE(0, verbose_stream() << mdl << "\n");
IF_VERBOSE(0, ctx.display_validation_failure(verbose_stream(), mdl, n));
UNREACHABLE();
}
}

2
src/sat/smt/euf_solver.h
View file

@ -160,7 +160,6 @@ namespace euf {
void collect_dependencies(user_sort& us, deps_t& deps);
void values2model(deps_t const& deps, model_ref& mdl);
void validate_model(model& mdl);
void display_validation_failure(std::ostream& out, model& mdl, enode* n);
// solving
void propagate_literals();
@ -409,6 +408,7 @@ namespace euf {
obj_map<expr, enode*> const& values2root();
void model_updated(model_ref& mdl);
expr* node2value(enode* n) const;
void display_validation_failure(std::ostream& out, model& mdl, enode* n);
// diagnostics
func_decl_ref_vector const& unhandled_functions() { return m_unhandled_functions; }