From 541a554ecd4fbf7a3678e61ac0c687581bbd8a4b Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 23 Oct 2025 17:10:47 +0200 Subject: [PATCH] Add finite set API functions to access term constructors from finite_set_decl_plugin.h (#7996) * Initial plan * Add C API for finite sets Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add Python bindings for finite sets Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add C++ bindings for finite sets Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Add documentation for finite set API Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- FINITE_SET_API.md | 154 ++++++++++++++++++++++++++ src/api/CMakeLists.txt | 1 + src/api/api_context.cpp | 1 + src/api/api_context.h | 3 + src/api/api_finite_set.cpp | 169 ++++++++++++++++++++++++++++ src/api/c++/z3++.h | 53 +++++++++ src/api/python/z3/z3.py | 219 ++++++++++++++++++++++++++++++++++++- src/api/z3_api.h | 101 +++++++++++++++++ 8 files changed, 700 insertions(+), 1 deletion(-) create mode 100644 FINITE_SET_API.md create mode 100644 src/api/api_finite_set.cpp diff --git a/FINITE_SET_API.md b/FINITE_SET_API.md new file mode 100644 index 000000000..ede624a00 --- /dev/null +++ b/FINITE_SET_API.md @@ -0,0 +1,154 @@ +# Finite Set API Documentation + +This document describes the finite set API added to Z3. + +## Overview + +The finite set API provides term constructors for finite sets as defined in `finite_set_decl_plugin.h`. +These are distinct from the existing array-based sets and provide a more direct representation for finite sets. + +## C API + +All functions are declared in `src/api/z3_api.h` and implemented in `src/api/api_finite_set.cpp`. + +### Sort Constructor + +- `Z3_sort Z3_mk_finite_set_sort(Z3_context c, Z3_sort elem_sort)` - Create a finite set sort over element sort + +### Sort Queries + +- `bool Z3_is_finite_set_sort(Z3_context c, Z3_sort s)` - Check if a sort is a finite set sort +- `Z3_sort Z3_get_finite_set_sort_basis(Z3_context c, Z3_sort s)` - Get the element sort of a finite set sort + +### Term Constructors + +- `Z3_ast Z3_mk_finite_set_empty(Z3_context c, Z3_sort set_sort)` - Create an empty finite set +- `Z3_ast Z3_mk_finite_set_singleton(Z3_context c, Z3_ast elem)` - Create a singleton set +- `Z3_ast Z3_mk_finite_set_union(Z3_context c, Z3_ast s1, Z3_ast s2)` - Create the union of two sets +- `Z3_ast Z3_mk_finite_set_intersect(Z3_context c, Z3_ast s1, Z3_ast s2)` - Create the intersection +- `Z3_ast Z3_mk_finite_set_difference(Z3_context c, Z3_ast s1, Z3_ast s2)` - Create the set difference +- `Z3_ast Z3_mk_finite_set_member(Z3_context c, Z3_ast elem, Z3_ast set)` - Check membership +- `Z3_ast Z3_mk_finite_set_size(Z3_context c, Z3_ast set)` - Get the cardinality +- `Z3_ast Z3_mk_finite_set_subset(Z3_context c, Z3_ast s1, Z3_ast s2)` - Check subset relation +- `Z3_ast Z3_mk_finite_set_map(Z3_context c, Z3_ast f, Z3_ast set)` - Apply function to all elements +- `Z3_ast Z3_mk_finite_set_filter(Z3_context c, Z3_ast f, Z3_ast set)` - Filter set with predicate +- `Z3_ast Z3_mk_finite_set_range(Z3_context c, Z3_ast low, Z3_ast high)` - Create range [low, high) + +## Python API + +All functions are available in `z3.py`: + +### Classes + +- `FiniteSetSortRef` - Finite set sort reference +- `FiniteSetRef` - Finite set expression reference + +### Functions + +- `FiniteSetSort(elem_sort)` - Create finite set sort +- `FiniteSetEmpty(set_sort)` - Create empty set +- `FiniteSetSingleton(elem)` - Create singleton set +- `FiniteSetUnion(s1, s2)` - Union (also `s1 | s2`) +- `FiniteSetIntersect(s1, s2)` - Intersection (also `s1 & s2`) +- `FiniteSetDifference(s1, s2)` - Difference (also `s1 - s2`) +- `FiniteSetMember(elem, set)` - Membership test +- `FiniteSetSize(set)` - Cardinality +- `FiniteSetSubset(s1, s2)` - Subset test +- `FiniteSetMap(f, set)` - Map function over set +- `FiniteSetFilter(f, set)` - Filter set +- `FiniteSetRange(low, high)` - Create range +- `is_finite_set(expr)` - Check if expression is a finite set +- `is_finite_set_sort(sort)` - Check if sort is a finite set sort + +### Example + +```python +from z3 import * + +# Create a finite set sort over integers +int_set = FiniteSetSort(IntSort()) + +# Create sets +a = Const('a', int_set) +b = Const('b', int_set) +s1 = FiniteSetSingleton(IntVal(1)) + +# Use operators +union = a | b +intersect = a & b +diff = a - b + +# Use with solver +solver = Solver() +solver.add(FiniteSetSize(a) == 2) +solver.add(FiniteSetMember(IntVal(1), a)) +print(solver.check()) +print(solver.model()) +``` + +## C++ API + +All functions are declared and implemented inline in `src/api/c++/z3++.h`: + +### Context Methods + +- `sort context::finite_set_sort(sort& s)` - Create finite set sort + +### Free Functions + +- `expr finite_set_empty(sort const& s)` - Create empty set +- `expr finite_set_singleton(expr const& e)` - Create singleton +- `expr finite_set_union(expr const& a, expr const& b)` - Union +- `expr finite_set_intersect(expr const& a, expr const& b)` - Intersection +- `expr finite_set_difference(expr const& a, expr const& b)` - Difference +- `expr finite_set_member(expr const& e, expr const& s)` - Membership +- `expr finite_set_size(expr const& s)` - Size +- `expr finite_set_subset(expr const& a, expr const& b)` - Subset +- `expr finite_set_map(expr const& f, expr const& s)` - Map +- `expr finite_set_filter(expr const& f, expr const& s)` - Filter +- `expr finite_set_range(expr const& low, expr const& high)` - Range + +### Example + +```cpp +#include + +z3::context c; +z3::sort int_sort = c.int_sort(); +z3::sort fs_sort = c.finite_set_sort(int_sort); + +z3::expr a = c.constant("a", fs_sort); +z3::expr b = c.constant("b", fs_sort); +z3::expr union_ab = finite_set_union(a, b); + +z3::solver s(c); +s.add(finite_set_size(a) == 2); +std::cout << s.check() << std::endl; +``` + +## Other Language Bindings + +The C#, Java, JavaScript, OCaml, and Julia bindings are auto-generated from the C API through +the `scripts/update_api.py` script during the build process. The `def_API` macros in `z3_api.h` +provide the metadata needed for auto-generation. + +## Implementation Details + +- The finite set plugin is registered in `src/ast/reg_decl_plugins.cpp` +- The `finite_set_util` is added to the API context in `src/api/api_context.h` +- Core implementation is in `src/ast/finite_set_decl_plugin.h/cpp` + +## SMT-LIB2 Syntax + +The finite set operations map to SMT-LIB2 symbols: +- `set.empty` - empty set +- `set.singleton` - singleton set +- `set.union` - union +- `set.intersect` - intersection +- `set.difference` - difference +- `set.in` - membership +- `set.size` - cardinality +- `set.subset` - subset +- `set.map` - map operation +- `set.filter` - filter operation +- `set.range` - integer range diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index a537bb3b9..c1e78f473 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -44,6 +44,7 @@ z3_add_component(api api_context.cpp api_datalog.cpp api_datatype.cpp + api_finite_set.cpp api_fpa.cpp api_goal.cpp api_log.cpp diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 82d65a5dd..6dc42f5e3 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -133,6 +133,7 @@ namespace api { m_fpa_util(m()), m_sutil(m()), m_recfun(m()), + m_finite_set_util(m()), m_ast_trail(m()), m_pmanager(m_limit) { diff --git a/src/api/api_context.h b/src/api/api_context.h index e570daca3..780372588 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -31,6 +31,7 @@ Revision History: #include "ast/fpa_decl_plugin.h" #include "ast/recfun_decl_plugin.h" #include "ast/special_relations_decl_plugin.h" +#include "ast/finite_set_decl_plugin.h" #include "ast/rewriter/seq_rewriter.h" #include "params/smt_params.h" #include "smt/smt_kernel.h" @@ -77,6 +78,7 @@ namespace api { fpa_util m_fpa_util; seq_util m_sutil; recfun::util m_recfun; + finite_set_util m_finite_set_util; // Support for old solver API smt_params m_fparams; @@ -146,6 +148,7 @@ namespace api { datatype_util& dtutil() { return m_dt_plugin->u(); } seq_util& sutil() { return m_sutil; } recfun::util& recfun() { return m_recfun; } + finite_set_util& fsutil() { return m_finite_set_util; } family_id get_basic_fid() const { return basic_family_id; } family_id get_array_fid() const { return m_array_fid; } family_id get_arith_fid() const { return arith_family_id; } diff --git a/src/api/api_finite_set.cpp b/src/api/api_finite_set.cpp new file mode 100644 index 000000000..9dbecfdae --- /dev/null +++ b/src/api/api_finite_set.cpp @@ -0,0 +1,169 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + api_finite_set.cpp + +Abstract: + + API for finite sets. + +Author: + + Copilot 2025-01-21 + +Revision History: + +--*/ +#include "api/z3.h" +#include "api/api_log_macros.h" +#include "api/api_context.h" +#include "api/api_util.h" +#include "ast/ast_pp.h" + +extern "C" { + + Z3_sort Z3_API Z3_mk_finite_set_sort(Z3_context c, Z3_sort elem_sort) { + Z3_TRY; + LOG_Z3_mk_finite_set_sort(c, elem_sort); + RESET_ERROR_CODE(); + parameter param(to_sort(elem_sort)); + sort* ty = mk_c(c)->m().mk_sort(mk_c(c)->fsutil().get_family_id(), FINITE_SET_SORT, 1, ¶m); + mk_c(c)->save_ast_trail(ty); + RETURN_Z3(of_sort(ty)); + Z3_CATCH_RETURN(nullptr); + } + + bool Z3_API Z3_is_finite_set_sort(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_is_finite_set_sort(c, s); + RESET_ERROR_CODE(); + return mk_c(c)->fsutil().is_finite_set(to_sort(s)); + Z3_CATCH_RETURN(false); + } + + Z3_sort Z3_API Z3_get_finite_set_sort_basis(Z3_context c, Z3_sort s) { + Z3_TRY; + LOG_Z3_get_finite_set_sort_basis(c, s); + RESET_ERROR_CODE(); + sort* elem_sort = nullptr; + if (!mk_c(c)->fsutil().is_finite_set(to_sort(s), elem_sort)) { + SET_ERROR_CODE(Z3_INVALID_ARG, "expected finite set sort"); + RETURN_Z3(nullptr); + } + RETURN_Z3(of_sort(elem_sort)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_empty(Z3_context c, Z3_sort set_sort) { + Z3_TRY; + LOG_Z3_mk_finite_set_empty(c, set_sort); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_empty(to_sort(set_sort)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_singleton(Z3_context c, Z3_ast elem) { + Z3_TRY; + LOG_Z3_mk_finite_set_singleton(c, elem); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_singleton(to_expr(elem)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_union(Z3_context c, Z3_ast s1, Z3_ast s2) { + Z3_TRY; + LOG_Z3_mk_finite_set_union(c, s1, s2); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_union(to_expr(s1), to_expr(s2)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_intersect(Z3_context c, Z3_ast s1, Z3_ast s2) { + Z3_TRY; + LOG_Z3_mk_finite_set_intersect(c, s1, s2); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_intersect(to_expr(s1), to_expr(s2)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_difference(Z3_context c, Z3_ast s1, Z3_ast s2) { + Z3_TRY; + LOG_Z3_mk_finite_set_difference(c, s1, s2); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_difference(to_expr(s1), to_expr(s2)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_member(Z3_context c, Z3_ast elem, Z3_ast set) { + Z3_TRY; + LOG_Z3_mk_finite_set_member(c, elem, set); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_in(to_expr(elem), to_expr(set)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_size(Z3_context c, Z3_ast set) { + Z3_TRY; + LOG_Z3_mk_finite_set_size(c, set); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_size(to_expr(set)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_subset(Z3_context c, Z3_ast s1, Z3_ast s2) { + Z3_TRY; + LOG_Z3_mk_finite_set_subset(c, s1, s2); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_subset(to_expr(s1), to_expr(s2)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_map(Z3_context c, Z3_ast f, Z3_ast set) { + Z3_TRY; + LOG_Z3_mk_finite_set_map(c, f, set); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_map(to_expr(f), to_expr(set)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_filter(Z3_context c, Z3_ast f, Z3_ast set) { + Z3_TRY; + LOG_Z3_mk_finite_set_filter(c, f, set); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_filter(to_expr(f), to_expr(set)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + + Z3_ast Z3_API Z3_mk_finite_set_range(Z3_context c, Z3_ast low, Z3_ast high) { + Z3_TRY; + LOG_Z3_mk_finite_set_range(c, low, high); + RESET_ERROR_CODE(); + app* a = mk_c(c)->fsutil().mk_range(to_expr(low), to_expr(high)); + mk_c(c)->save_ast_trail(a); + RETURN_Z3(of_ast(a)); + Z3_CATCH_RETURN(nullptr); + } + +}; diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 9fb84236d..a943e08f0 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -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 diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 051265a78..104647284 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -678,6 +678,8 @@ def is_sort(s : Any) -> bool: def _to_sort_ref(s, ctx): if z3_debug(): _z3_assert(isinstance(s, Sort), "Z3 Sort expected") + if Z3_is_finite_set_sort(ctx.ref(), s): + return FiniteSetSortRef(s, ctx) k = _sort_kind(ctx, s) if k == Z3_BOOL_SORT: return BoolSortRef(s, ctx) @@ -1184,7 +1186,11 @@ def _to_expr_ref(a, ctx): k = Z3_get_ast_kind(ctx_ref, a) if k == Z3_QUANTIFIER_AST: return QuantifierRef(a, ctx) - sk = Z3_get_sort_kind(ctx_ref, Z3_get_sort(ctx_ref, a)) + # Check for finite set sort before checking sort kind + s = Z3_get_sort(ctx_ref, a) + if Z3_is_finite_set_sort(ctx_ref, s): + return FiniteSetRef(a, ctx) + sk = Z3_get_sort_kind(ctx_ref, s) if sk == Z3_BOOL_SORT: return BoolRef(a, ctx) if sk == Z3_INT_SORT: @@ -5147,6 +5153,217 @@ def IsSubset(a, b): return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx) +######################################### +# +# Finite Sets +# +######################################### + + +class FiniteSetSortRef(SortRef): + """Finite set sort.""" + + def element_sort(self): + """Return the element sort of this finite set sort.""" + return _to_sort_ref(Z3_get_finite_set_sort_basis(self.ctx_ref(), self.ast), self.ctx) + + def cast(self, val): + """Try to cast val as a finite set expression.""" + if is_expr(val): + if self.eq(val.sort()): + return val + else: + _z3_assert(False, "Cannot cast to finite set sort") + if isinstance(val, set): + elem_sort = self.element_sort() + result = FiniteSetEmpty(self) + for e in val: + result = FiniteSetUnion(result, FiniteSetSingleton(_py2expr(e, self.ctx, elem_sort))) + return result + _z3_assert(False, "Cannot cast to finite set sort") + + def subsort(self, other): + return False + + def is_int(self): + return False + + def is_bool(self): + return False + + def is_datatype(self): + return False + + def is_array(self): + return False + + def is_bv(self): + return False + + +def is_finite_set(a): + """Return True if a is a Z3 finite set expression. + >>> s = FiniteSetSort(IntSort()) + >>> is_finite_set(FiniteSetEmpty(s)) + True + >>> is_finite_set(IntVal(1)) + False + """ + return isinstance(a, FiniteSetRef) + + +def is_finite_set_sort(s): + """Return True if s is a Z3 finite set sort. + >>> is_finite_set_sort(FiniteSetSort(IntSort())) + True + >>> is_finite_set_sort(IntSort()) + False + """ + return isinstance(s, FiniteSetSortRef) + + +class FiniteSetRef(ExprRef): + """Finite set expression.""" + + def sort(self): + return FiniteSetSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx) + + def __or__(self, other): + """Return the union of self and other.""" + return FiniteSetUnion(self, other) + + def __and__(self, other): + """Return the intersection of self and other.""" + return FiniteSetIntersect(self, other) + + def __sub__(self, other): + """Return the set difference of self and other.""" + return FiniteSetDifference(self, other) + + +def FiniteSetSort(elem_sort): + """Create a finite set sort over element sort elem_sort. + >>> s = FiniteSetSort(IntSort()) + >>> s + FiniteSet(Int) + """ + return FiniteSetSortRef(Z3_mk_finite_set_sort(elem_sort.ctx_ref(), elem_sort.ast), elem_sort.ctx) + + +def FiniteSetEmpty(set_sort): + """Create an empty finite set of the given sort. + >>> s = FiniteSetSort(IntSort()) + >>> FiniteSetEmpty(s) + set.empty + """ + ctx = set_sort.ctx + return FiniteSetRef(Z3_mk_finite_set_empty(ctx.ref(), set_sort.ast), ctx) + + +def FiniteSetSingleton(elem): + """Create a singleton finite set containing elem. + >>> FiniteSetSingleton(IntVal(1)) + set.singleton(1) + """ + ctx = elem.ctx + return FiniteSetRef(Z3_mk_finite_set_singleton(ctx.ref(), elem.as_ast()), ctx) + + +def FiniteSetUnion(s1, s2): + """Create the union of two finite sets. + >>> a = Const('a', FiniteSetSort(IntSort())) + >>> b = Const('b', FiniteSetSort(IntSort())) + >>> FiniteSetUnion(a, b) + set.union(a, b) + """ + ctx = _ctx_from_ast_arg_list([s1, s2]) + return FiniteSetRef(Z3_mk_finite_set_union(ctx.ref(), s1.as_ast(), s2.as_ast()), ctx) + + +def FiniteSetIntersect(s1, s2): + """Create the intersection of two finite sets. + >>> a = Const('a', FiniteSetSort(IntSort())) + >>> b = Const('b', FiniteSetSort(IntSort())) + >>> FiniteSetIntersect(a, b) + set.intersect(a, b) + """ + ctx = _ctx_from_ast_arg_list([s1, s2]) + return FiniteSetRef(Z3_mk_finite_set_intersect(ctx.ref(), s1.as_ast(), s2.as_ast()), ctx) + + +def FiniteSetDifference(s1, s2): + """Create the set difference of two finite sets. + >>> a = Const('a', FiniteSetSort(IntSort())) + >>> b = Const('b', FiniteSetSort(IntSort())) + >>> FiniteSetDifference(a, b) + set.difference(a, b) + """ + ctx = _ctx_from_ast_arg_list([s1, s2]) + return FiniteSetRef(Z3_mk_finite_set_difference(ctx.ref(), s1.as_ast(), s2.as_ast()), ctx) + + +def FiniteSetMember(elem, set): + """Check if elem is a member of the finite set. + >>> a = Const('a', FiniteSetSort(IntSort())) + >>> FiniteSetMember(IntVal(1), a) + set.in(1, a) + """ + ctx = _ctx_from_ast_arg_list([elem, set]) + return BoolRef(Z3_mk_finite_set_member(ctx.ref(), elem.as_ast(), set.as_ast()), ctx) + + +def FiniteSetSize(set): + """Get the size (cardinality) of a finite set. + >>> a = Const('a', FiniteSetSort(IntSort())) + >>> FiniteSetSize(a) + set.size(a) + """ + ctx = set.ctx + return ArithRef(Z3_mk_finite_set_size(ctx.ref(), set.as_ast()), ctx) + + +def FiniteSetSubset(s1, s2): + """Check if s1 is a subset of s2. + >>> a = Const('a', FiniteSetSort(IntSort())) + >>> b = Const('b', FiniteSetSort(IntSort())) + >>> FiniteSetSubset(a, b) + set.subset(a, b) + """ + ctx = _ctx_from_ast_arg_list([s1, s2]) + return BoolRef(Z3_mk_finite_set_subset(ctx.ref(), s1.as_ast(), s2.as_ast()), ctx) + + +def FiniteSetMap(f, set): + """Apply function f to all elements of the finite set. + >>> f = Function('f', IntSort(), IntSort()) + >>> a = Const('a', FiniteSetSort(IntSort())) + >>> FiniteSetMap(f, a) + set.map(f, a) + """ + ctx = _ctx_from_ast_arg_list([f, set]) + return FiniteSetRef(Z3_mk_finite_set_map(ctx.ref(), f.as_ast(), set.as_ast()), ctx) + + +def FiniteSetFilter(f, set): + """Filter a finite set using predicate f. + >>> f = Function('f', IntSort(), BoolSort()) + >>> a = Const('a', FiniteSetSort(IntSort())) + >>> FiniteSetFilter(f, a) + set.filter(f, a) + """ + ctx = _ctx_from_ast_arg_list([f, set]) + return FiniteSetRef(Z3_mk_finite_set_filter(ctx.ref(), f.as_ast(), set.as_ast()), ctx) + + +def FiniteSetRange(low, high): + """Create a finite set of integers in the range [low, high). + >>> FiniteSetRange(IntVal(0), IntVal(5)) + set.range(0, 5) + """ + ctx = _ctx_from_ast_arg_list([low, high]) + return FiniteSetRef(Z3_mk_finite_set_range(ctx.ref(), low.as_ast(), high.as_ast()), ctx) + + ######################################### # # Datatypes diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9de58e057..8d0ab3f20 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -3389,6 +3389,107 @@ extern "C" { Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2); /**@}*/ + /** @name Finite Sets */ + /**@{*/ + /** + \brief Create a finite set sort. + + def_API('Z3_mk_finite_set_sort', SORT, (_in(CONTEXT), _in(SORT))) + */ + Z3_sort Z3_API Z3_mk_finite_set_sort(Z3_context c, Z3_sort elem_sort); + + /** + \brief Check if a sort is a finite set sort. + + def_API('Z3_is_finite_set_sort', BOOL, (_in(CONTEXT), _in(SORT))) + */ + bool Z3_API Z3_is_finite_set_sort(Z3_context c, Z3_sort s); + + /** + \brief Get the element sort of a finite set sort. + + def_API('Z3_get_finite_set_sort_basis', SORT, (_in(CONTEXT), _in(SORT))) + */ + Z3_sort Z3_API Z3_get_finite_set_sort_basis(Z3_context c, Z3_sort s); + + /** + \brief Create an empty finite set of the given sort. + + def_API('Z3_mk_finite_set_empty', AST, (_in(CONTEXT), _in(SORT))) + */ + Z3_ast Z3_API Z3_mk_finite_set_empty(Z3_context c, Z3_sort set_sort); + + /** + \brief Create a singleton finite set. + + def_API('Z3_mk_finite_set_singleton', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_finite_set_singleton(Z3_context c, Z3_ast elem); + + /** + \brief Create the union of two finite sets. + + def_API('Z3_mk_finite_set_union', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_finite_set_union(Z3_context c, Z3_ast s1, Z3_ast s2); + + /** + \brief Create the intersection of two finite sets. + + def_API('Z3_mk_finite_set_intersect', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_finite_set_intersect(Z3_context c, Z3_ast s1, Z3_ast s2); + + /** + \brief Create the set difference of two finite sets. + + def_API('Z3_mk_finite_set_difference', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_finite_set_difference(Z3_context c, Z3_ast s1, Z3_ast s2); + + /** + \brief Check if an element is a member of a finite set. + + def_API('Z3_mk_finite_set_member', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_finite_set_member(Z3_context c, Z3_ast elem, Z3_ast set); + + /** + \brief Get the size (cardinality) of a finite set. + + def_API('Z3_mk_finite_set_size', AST, (_in(CONTEXT), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_finite_set_size(Z3_context c, Z3_ast set); + + /** + \brief Check if one finite set is a subset of another. + + def_API('Z3_mk_finite_set_subset', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_finite_set_subset(Z3_context c, Z3_ast s1, Z3_ast s2); + + /** + \brief Apply a function to all elements of a finite set. + + def_API('Z3_mk_finite_set_map', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_finite_set_map(Z3_context c, Z3_ast f, Z3_ast set); + + /** + \brief Filter a finite set using a predicate. + + def_API('Z3_mk_finite_set_filter', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_finite_set_filter(Z3_context c, Z3_ast f, Z3_ast set); + + /** + \brief Create a finite set of integers in the range [low, high). + + def_API('Z3_mk_finite_set_range', AST, (_in(CONTEXT), _in(AST), _in(AST))) + */ + Z3_ast Z3_API Z3_mk_finite_set_range(Z3_context c, Z3_ast low, Z3_ast high); + /**@}*/ + /** @name Numerals */ /**@{*/ /**