mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

bail on first model validation failure

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-08-28 17:08:30 -07:00
parent 4f064ee5d6
commit e7fcbd9563
2 changed files with 17 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -263,6 +263,18 @@ namespace euf {
return m_values.get(n->get_root_id(), nullptr);
}
void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) {
out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
for (auto* arg : euf::enode_args(n)) {
expr_ref val = mdl(arg->get_expr());
expr_ref sval(m);
th_rewriter rw(m);
rw(val, sval);
out << bpp(arg) << "\n" << sval << "\n";
}
out << mdl << "\n";
}
void solver::validate_model(model& mdl) {
bool first = true;
for (enode* n : m_egraph.nodes()) {
@ -278,24 +290,12 @@ namespace euf {
continue;
if (!tt && !mdl.is_true(e))
continue;
IF_VERBOSE(0,
verbose_stream() << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
for (auto* arg : euf::enode_args(n)) {
expr_ref val = mdl(arg->get_expr());
expr_ref sval(m);
th_rewriter rw(m);
rw(val, sval);
verbose_stream() << bpp(arg) << "\n" << sval << "\n";
});
CTRACE("euf", first,
tout << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n";
s().display(tout);
tout << mdl << "\n";);
IF_VERBOSE(0, display_validation_failure(verbose_stream(), mdl, n););
CTRACE("euf", first, display_validation_failure(tout, mdl, n););
(void)first;
exit(1);
first = false;
}
}
}

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

@ -157,6 +157,7 @@ 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();