mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +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:41:20 -07:00
parent 6143070157
commit 8ababafe42
2 changed files with 20 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -313,6 +313,7 @@ namespace sls {
// assign fresh values to uninterpeted nodes
for (euf::enode* n : deps.top_sorted()) {
TRACE("dt", tout << g->bpp(n) << "\n");
SASSERT(n->is_root());
expr* e = n->get_expr();
if (!dt.is_datatype(e))
@ -321,24 +322,11 @@ namespace sls {
if (m_values.get(id, nullptr))
continue;
auto con = get_constructor(n);
if (con)
continue;
m_values.setx(id, m_model->get_fresh_value(e->get_sort()));
TRACE("dt", tout << "Fresh interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n");
}
// finally populate values to other nodes.
for (euf::enode* n : deps.top_sorted()) {
SASSERT(n->is_root());
unsigned id = n->get_id();
expr* e = n->get_expr();
if (!dt.is_datatype(e))
continue;
if (m_values.get(id))
continue;
euf::enode* con = get_constructor(n);
if (!con)
if (!con) {
m_values.setx(id, m_model->get_fresh_value(e->get_sort()));
TRACE("dt", tout << "Fresh interpretation " << g->bpp(n) << " <- " << mk_bounded_pp(m_values.get(id), m) << "\n");
continue;
}
auto f = con->get_decl();
args.reset();
for (auto arg : euf::enode_args(con)) {
@ -388,12 +376,15 @@ namespace sls {
svector<color_t> color;
unsigned_vector dfsnum;
svector<std::tuple<unsigned, euf::enode*, unsigned>> todo;
obj_map<sort, ptr_vector<expr>> sorts;
for (auto n : g->nodes()) {
if (!n->is_root())
continue;
expr* e = n->get_expr();
if (!dt.is_datatype(e))
continue;
sort* s = e->get_sort();
sorts.insert_if_not_there(s, ptr_vector<expr>()).push_back(e);
auto c = color.get(e->get_id(), white);
SASSERT(c != grey);
@ -458,13 +449,14 @@ namespace sls {
}
//
// sort_size sz = dt.et_datatype_size(s);
// if (sz.is_finite())
// - sz.size() < |T of sort s|
// - ensure that there are at most sz.size() distinct elements.
// - not distinct(t1, ..., tn) where n = sz.size() + 1
//
for (auto const& [s, elems] : sorts) {
auto sz = s->get_num_elements();
if (!sz.is_finite() || sz.size() >= elems.size())
continue;
ctx.add_constraint(m.mk_not(m.mk_distinct((unsigned)sz.size() + 1, elems.data())));
}
return false;
}

10
src/ast/sls/sls_euf_plugin.cpp
View file

@ -433,14 +433,12 @@ namespace sls {
auto n = to_app(e)->get_num_args();
expr_ref_vector eqs(m);
for (unsigned i = 0; i < n; ++i) {
auto arg = to_app(e)->get_arg(i);
auto a = ctx.get_value(arg);
auto a = m_g->find(to_app(e)->get_arg(i));
for (unsigned j = i + 1; j < n; ++j) {
auto argb = to_app(e)->get_arg(j);
auto b = ctx.get_value(argb);
if (a == b)
auto b = m_g->find(to_app(e)->get_arg(j));
if (a->get_root() == b->get_root())
goto done_distinct;
eqs.push_back(m.mk_eq(arg, argb));
eqs.push_back(m.mk_eq(a->get_expr(), b->get_expr()));
}
}
// distinct(a, b, c) or a = b or a = c or b = c