From 4c6d7158cbc05665a6d10bede1ffb81269b4db8f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Sep 2022 17:05:27 -0500 Subject: [PATCH] extended debugging for sat.euf --- src/sat/smt/arith_solver.cpp | 3 +-- src/sat/smt/euf_solver.h | 2 +- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index cec3f49e7..c5730c19c 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -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(); } } diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 91b348e50..089c896cb 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -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 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; }