mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #7121

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-02-16 09:59:57 +07:00
parent 2b14793213
commit 84d592c1f2
1 changed files with 11 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/converters/generic_model_converter.cpp
View file

@ -43,6 +43,7 @@ void generic_model_converter::operator()(model_ref & md) {
expr_ref val(m); expr_ref val(m);
unsigned arity; unsigned arity;
bool reset_ev = false; bool reset_ev = false;
obj_map<sort, ptr_vector<expr>> uninterpreted;
for (unsigned i = m_entries.size(); i-- > 0; ) { for (unsigned i = m_entries.size(); i-- > 0; ) {
entry const& e = m_entries[i]; entry const& e = m_entries[i];
switch (e.m_instruction) { switch (e.m_instruction) {
@ -63,6 +64,13 @@ void generic_model_converter::operator()(model_ref & md) {
reset_ev = old_val != nullptr; reset_ev = old_val != nullptr;
md->register_decl(e.m_f, val); md->register_decl(e.m_f, val);
} }
// corner case when uninterpreted constants are eliminated
sort* s = e.m_f->get_range();
if (m.is_uninterp(s) && !md->has_uninterpreted_sort(s)) {
uninterpreted.insert_if_not_there(s, {});
if (!uninterpreted[s].contains(val))
uninterpreted[s].push_back(val);
}
} }
else { else {
func_interp * old_val = md->get_func_interp(e.m_f); func_interp * old_val = md->get_func_interp(e.m_f);
@ -84,6 +92,9 @@ void generic_model_converter::operator()(model_ref & md) {
break; break;
} }
} }
for (auto const& [s, u] : uninterpreted) {
md->register_usort(s, u.size(), u.data());
}
TRACE("model_converter", tout << "after generic_model_converter\n"; model_v2_pp(tout, *md);); TRACE("model_converter", tout << "after generic_model_converter\n"; model_v2_pp(tout, *md););
} }