mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

add model validation

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-11-11 17:34:43 -08:00
parent b5aab7ec2a
commit 16db8bf49e
1 changed files with 15 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -34,6 +34,7 @@ namespace euf {
values2model(deps, mdl); values2model(deps, mdl);
for (auto* mb : m_solvers) for (auto* mb : m_solvers)
mb->finalize_model(*mdl); mb->finalize_model(*mdl);
// validate_model(*mdl);
} }
bool solver::include_func_interp(func_decl* f) { bool solver::include_func_interp(func_decl* f) {
@ -196,5 +197,19 @@ namespace euf {
return m_values2root; return m_values2root;
} }
void solver::validate_model(model& mdl) {
for (enode* n : m_egraph.nodes()) {
expr* e = n->get_expr();
if (!m.is_bool(e))
continue;
unsigned id = n->get_root_id();
bool tt = m.is_true(m_values.get(id));
if (mdl.is_true(e) != tt) {
IF_VERBOSE(0, verbose_stream() << "Failed to evaluate " << id << " " << mk_bounded_pp(e, m) << "\n");
}
}
}
} }