mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

#5532

Browse source 
ensure re-internalization for predicates that are replayed.
Theory internalization is currently not considered in depth.
This commit is contained in:
Nikolaj Bjorner 2021-09-05 00:24:34 -07:00
parent 3021da87cf
commit 3764eb1959
2 changed files with 25 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -266,14 +266,25 @@ namespace euf {
void solver::display_validation_failure(std::ostream& out, model& mdl, enode* n) { 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"; out << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(n->get_expr()) << "\n";
for (auto* arg : euf::enode_args(n)) { euf::enode_vector nodes;
expr_ref val = mdl(arg->get_expr()); nodes.push_back(n);
for (unsigned i = 0; i < nodes.size(); ++i) {
euf::enode* r = nodes[i];
if (r->is_marked1())
continue;
r->mark1();
for (auto* arg : euf::enode_args(r))
nodes.push_back(arg);
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);
out << bpp(arg) << "\n" << sval << "\n"; out << bpp(r) << " := " << sval << " " << mdl(r->get_root()->get_expr()) << "\n";
} }
for (euf::enode* r : nodes)
r->unmark1();
out << mdl << "\n"; out << mdl << "\n";
s().display(out);
} }
void solver::validate_model(model& mdl) { void solver::validate_model(model& mdl) {

13
src/sat/smt/euf_solver.cpp
View file

@ -454,6 +454,9 @@ namespace euf {
bool give_up = false; bool give_up = false;
bool cont = false; bool cont = false;
if (unit_propagate())
return sat::check_result::CR_CONTINUE;
if (!init_relevancy()) if (!init_relevancy())
give_up = true; give_up = true;
@ -591,9 +594,13 @@ namespace euf {
else else
lit = si.internalize(e, true); lit = si.internalize(e, true);
VERIFY(lit.var() == v); VERIFY(lit.var() == v);
if (is_app(e)) if (!m_egraph.find(e) && (!m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e))) {
for (expr* arg : *to_app(e)) ptr_buffer<euf::enode> args;
e_internalize(arg); if (is_app(e))
for (expr* arg : *to_app(e))
args.push_back(e_internalize(arg));
mk_enode(e, args.size(), args.data());
}
attach_lit(lit, e); attach_lit(lit, e);
} }