mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 06:33:23 +00:00
Code Activity

Fix term-ite models in theory_fpa. Fixes #2857.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2020-01-13 19:24:31 +00:00
parent 0e096c55a9
commit 77689ed002
No known key found for this signature in database
GPG key ID: BCF6360F86294467
2 changed files with 32 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/smt/theory_fpa.cpp
View file

@ -728,6 +728,33 @@ namespace smt {
mg.register_factory(m_factory); mg.register_factory(m_factory);
} }
enode* theory_fpa::ensure_enode(expr* e) {
context& ctx = get_context();
if (!ctx.e_internalized(e)) {
ctx.internalize(e, false);
}
enode* n = ctx.get_enode(e);
ctx.mark_as_relevant(n);
return n;
}
app* theory_fpa::get_ite_value(expr* e) {
ast_manager & m = get_manager();
expr* e1, *e2, *e3;
while (m.is_ite(e, e1, e2, e3)) {
if (get_root(e2) == get_root(e)) {
e = e2;
}
else if (get_root(e3) == get_root(e)) {
e = e3;
}
else {
break;
}
}
return to_app(e);
}
model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) { model_value_proc * theory_fpa::mk_value(enode * n, model_generator & mg) {
TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) << TRACE("t_fpa", tout << "mk_value for: " << mk_ismt2_pp(n->get_owner(), get_manager()) <<
" (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";); " (sort " << mk_ismt2_pp(get_manager().get_sort(n->get_owner()), get_manager()) << ")\n";);
@ -735,7 +762,7 @@ namespace smt {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context(); context & ctx = get_context();
app_ref owner(m); app_ref owner(m);
owner = n->get_owner(); owner = get_ite_value(n->get_owner());
// If the owner is not internalized, it doesn't have an enode associated. // If the owner is not internalized, it doesn't have an enode associated.
SASSERT(ctx.e_internalized(owner)); SASSERT(ctx.e_internalized(owner));

4
src/smt/theory_fpa.h
View file

@ -196,6 +196,10 @@ namespace smt {
app_ref wrap(expr * e); app_ref wrap(expr * e);
app_ref unwrap(expr * e, sort * s); app_ref unwrap(expr * e, sort * s);
enode* ensure_enode(expr* e);
enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
app* get_ite_value(expr* e);
}; };
}; };