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

reformat code to remove brackets

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-05-09 13:48:28 -07:00
parent 12e45c9d17
commit f6ab5a61ac
1 changed files with 19 additions and 27 deletions

46
src/smt/proto_model/proto_model.cpp
View file

@ -288,42 +288,33 @@ bool proto_model::is_finite(sort * s) const {
}
expr * proto_model::get_some_value(sort * s) {
if (m.is_uninterp(s)) {
return m_user_sort_factory->get_some_value(s);
}
else if (value_factory * f = get_factory(s->get_family_id())) {
return f->get_some_value(s);
}
else {
if (m.is_uninterp(s))
return m_user_sort_factory->get_some_value(s);
else if (value_factory * f = get_factory(s->get_family_id()))
return f->get_some_value(s);
else
// there is no factory for the family id, then assume s is uninterpreted.
return m_user_sort_factory->get_some_value(s);
}
return m_user_sort_factory->get_some_value(s);
}
bool proto_model::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
if (m.is_uninterp(s)) {
return m_user_sort_factory->get_some_values(s, v1, v2);
}
else if (value_factory * f = get_factory(s->get_family_id())) {
return f->get_some_values(s, v1, v2);
}
else {
return false;
}
if (m.is_uninterp(s))
return m_user_sort_factory->get_some_values(s, v1, v2);
else if (value_factory * f = get_factory(s->get_family_id()))
return f->get_some_values(s, v1, v2);
else
return false;
}
expr * proto_model::get_fresh_value(sort * s) {
if (m.is_uninterp(s)) {
return m_user_sort_factory->get_fresh_value(s);
}
else if (value_factory * f = get_factory(s->get_family_id())) {
return f->get_fresh_value(s);
}
else {
if (m.is_uninterp(s))
return m_user_sort_factory->get_fresh_value(s);
else if (value_factory * f = get_factory(s->get_family_id()))
return f->get_fresh_value(s);
else
// Use user_sort_factory if the theory has no support for model construnction.
// This is needed when dummy theories are used for arithmetic or arrays.
return m_user_sort_factory->get_fresh_value(s);
}
return m_user_sort_factory->get_fresh_value(s);
}
void proto_model::register_value(expr * n) {
@ -354,6 +345,7 @@ void proto_model::compress() {
void proto_model::complete_partial_func(func_decl * f, bool use_fresh) {
func_interp * fi = get_func_interp(f);
if (fi && fi->is_partial()) {
verbose_stream() << "complete " << f->get_name() << " " << use_fresh << "\n";
expr * else_value;
if (use_fresh) {
else_value = get_fresh_value(f->get_range());