mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

support AC parsing

Browse source 
By tagging union and intersection as AC we allow parsing set union and intersection as n-ary functions.
The internal representation remains binary.
This commit is contained in:
Nikolaj Bjorner 2025-10-17 14:49:32 +02:00
parent 8dd91e4698
commit d6908a3d4b
1 changed files with 9 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/ast/finite_set_decl_plugin.cpp
View file

@ -125,7 +125,12 @@ func_decl * finite_set_decl_plugin::mk_finite_set_op(decl_kind k, unsigned arity
polymorphism::util poly_util(m);
sort_ref rng(m);
poly_util.match(*m_sigs[k], arity, domain, range, rng);
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
func_decl_info info(m_family_id, k);
if (k == OP_FINITE_SET_UNION || k == OP_FINITE_SET_INTERSECT) {
info.set_commutative(true);
info.set_associative(true);
}
return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, info);
}
func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
@ -144,9 +149,10 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param
range = to_sort(parameters[0].get_ast());
}
return mk_empty(range);
case OP_FINITE_SET_SINGLETON:
case OP_FINITE_SET_UNION:
case OP_FINITE_SET_INTERSECT:
return mk_finite_set_op(k, 2, domain, range);
case OP_FINITE_SET_SINGLETON:
case OP_FINITE_SET_DIFFERENCE:
case OP_FINITE_SET_IN:
case OP_FINITE_SET_SIZE: