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

Add C++ bindings for finite sets

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-10-21 20:23:13 +00:00
parent d9c354f809
commit 4029161cb4
1 changed files with 53 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

53
src/api/c++/z3++.h
View file

@ -274,6 +274,10 @@ namespace z3 {
\brief Return a regular expression sort over sequences \c seq_sort.
*/
sort re_sort(sort& seq_sort);
/**
\brief Return a finite set sort over element sort \c s.
*/
sort finite_set_sort(sort& s);
/**
\brief Return an array sort for arrays from \c d to \c r.
@ -3494,6 +3498,7 @@ namespace z3 {
inline sort context::char_sort() { Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); }
inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
inline sort context::finite_set_sort(sort& s) { Z3_sort r = Z3_mk_finite_set_sort(m_ctx, s); check_error(); return sort(*this, r); }
inline sort context::fpa_sort(unsigned ebits, unsigned sbits) { Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }
template<>
@ -4065,6 +4070,54 @@ namespace z3 {
MK_EXPR2(Z3_mk_set_subset, a, b);
}
// finite set operations
inline expr finite_set_empty(sort const& s) {
Z3_ast r = Z3_mk_finite_set_empty(s.ctx(), s);
s.check_error();
return expr(s.ctx(), r);
}
inline expr finite_set_singleton(expr const& e) {
MK_EXPR1(Z3_mk_finite_set_singleton, e);
}
inline expr finite_set_union(expr const& a, expr const& b) {
MK_EXPR2(Z3_mk_finite_set_union, a, b);
}
inline expr finite_set_intersect(expr const& a, expr const& b) {
MK_EXPR2(Z3_mk_finite_set_intersect, a, b);
}
inline expr finite_set_difference(expr const& a, expr const& b) {
MK_EXPR2(Z3_mk_finite_set_difference, a, b);
}
inline expr finite_set_member(expr const& e, expr const& s) {
MK_EXPR2(Z3_mk_finite_set_member, e, s);
}
inline expr finite_set_size(expr const& s) {
MK_EXPR1(Z3_mk_finite_set_size, s);
}
inline expr finite_set_subset(expr const& a, expr const& b) {
MK_EXPR2(Z3_mk_finite_set_subset, a, b);
}
inline expr finite_set_map(expr const& f, expr const& s) {
MK_EXPR2(Z3_mk_finite_set_map, f, s);
}
inline expr finite_set_filter(expr const& f, expr const& s) {
MK_EXPR2(Z3_mk_finite_set_filter, f, s);
}
inline expr finite_set_range(expr const& low, expr const& high) {
MK_EXPR2(Z3_mk_finite_set_range, low, high);
}
// sequence and regular expression operations.
// union is +
// concat is overloaded to handle sequences and regular expressions