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

#6319

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-09-19 03:07:51 -07:00
parent d6d34a8962
commit fce4d2ad90
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/euf_internalize.cpp
View file

@ -264,7 +264,11 @@ namespace euf {
sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id()); sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id());
if (sz <= 1) if (sz <= 1)
return; return;
if (sz <= distinct_max_args) { sort* srt = e->get_arg(0)->get_sort();
auto sort_sz = srt->get_num_elements();
if (sort_sz.is_finite() && sort_sz.size() <= sz)
s().add_clause(0, nullptr, st);
else if (sz <= distinct_max_args) {
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
for (unsigned j = i + 1; j < sz; ++j) { for (unsigned j = i + 1; j < sz; ++j) {
expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr()); expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr());
@ -274,8 +278,7 @@ namespace euf {
} }
} }
else { else {
// dist-f(x_1) = v_1 & ... & dist-f(x_n) = v_n // dist-f(x_1) = v_1 & ... & dist-f(x_n) = v_n
sort* srt = e->get_arg(0)->get_sort();
SASSERT(!m.is_bool(srt)); SASSERT(!m.is_bool(srt));
sort_ref u(m.mk_fresh_sort("distinct-elems"), m); sort_ref u(m.mk_fresh_sort("distinct-elems"), m);
func_decl_ref f(m.mk_fresh_func_decl("dist-f", "", 1, &srt, u), m); func_decl_ref f(m.mk_fresh_func_decl("dist-f", "", 1, &srt, u), m);