mirror of
https://github.com/Z3Prover/z3
synced 2025-07-22 20:32:05 +00:00
This commit is contained in:
parent
92ec81d108
commit
9989ef6553
1 changed files with 3 additions and 3 deletions
|
@ -77,12 +77,12 @@ namespace euf {
|
||||||
}
|
}
|
||||||
|
|
||||||
bool solver::include_func_interp(func_decl* f) {
|
bool solver::include_func_interp(func_decl* f) {
|
||||||
if (f->is_skolem())
|
|
||||||
return false;
|
|
||||||
if (f->get_family_id() == null_family_id)
|
if (f->get_family_id() == null_family_id)
|
||||||
return true;
|
return true;
|
||||||
if (f->get_family_id() == m.get_basic_family_id())
|
if (f->get_family_id() == m.get_basic_family_id())
|
||||||
return false;
|
return false;
|
||||||
|
if (f->is_skolem())
|
||||||
|
return false;
|
||||||
euf::th_model_builder* mb = func_decl2solver(f);
|
euf::th_model_builder* mb = func_decl2solver(f);
|
||||||
return mb && mb->include_func_interp(f);
|
return mb && mb->include_func_interp(f);
|
||||||
}
|
}
|
||||||
|
@ -190,7 +190,7 @@ namespace euf {
|
||||||
if (!is_app(e))
|
if (!is_app(e))
|
||||||
continue;
|
continue;
|
||||||
app* a = to_app(e);
|
app* a = to_app(e);
|
||||||
func_decl* f = a->get_decl();
|
func_decl* f = a->get_decl();
|
||||||
if (!include_func_interp(f))
|
if (!include_func_interp(f))
|
||||||
continue;
|
continue;
|
||||||
if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(f))
|
if (m.is_bool(e) && is_uninterp_const(e) && mdl->get_const_interp(f))
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue