mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 21:57:00 +00:00
Code Activity

fixup finite domain search

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-16 20:59:28 -07:00
parent 8ababafe42
commit 0218a15f2e
1 changed files with 8 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

14
src/ast/sls/sls_datatype_plugin.cpp
View file

@ -323,21 +323,23 @@ namespace sls {
continue; continue;
auto con = get_constructor(n); auto con = get_constructor(n);
if (!con) { if (!con) {
m_values.setx(id, m_model->get_fresh_value(e->get_sort())); auto v = m_model->get_fresh_value(e->get_sort());
if (!v)
v = m_model->get_some_value(e->get_sort());
SASSERT(v);
m_values.setx(id, v);
TRACE("dt", tout << "Fresh interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n"); TRACE("dt", tout << "Fresh interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n");
continue; continue;
} }
auto f = con->get_decl(); auto f = con->get_decl();
args.reset(); args.reset();
for (auto arg : euf::enode_args(con)) { for (auto arg : euf::enode_args(con)) {
if (dt.is_datatype(arg->get_sort())) { if (dt.is_datatype(arg->get_sort()))
auto val_arg = m_values.get(arg->get_root_id()); args.push_back(m_values.get(arg->get_root_id()));
SASSERT(val_arg);
args.push_back(val_arg);
}
else else
args.push_back(ctx.get_value(arg->get_expr())); args.push_back(ctx.get_value(arg->get_expr()));
} }
SASSERT(all_of(args, [&](expr* e) { return e != nullptr; }));
m_values.setx(id, m.mk_app(f, args)); m_values.setx(id, m.mk_app(f, args));
TRACE("dt", tout << "Patched interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n"); TRACE("dt", tout << "Patched interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n");
} }