From 450412c85405a09f1be793b908458e6371f773d6 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Wed, 29 Oct 2025 16:52:38 -0700 Subject: [PATCH] [WIP] Add finite set operators to Z3_decl_kind enumeration (#8004) * Initial plan * Add Z3_decl_kind enumeration for finite_set operators - Added Z3_OP_FINITE_SET_* enumeration values (0xc000 range) to z3_api.h - Added documentation for all 13 finite_set operators - Added translation cases in api_ast.cpp for mapping internal finite_set enum values to external Z3_decl_kind values - All operators tested and working correctly Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Improve documentation for Z3_OP_FINITE_SET_EXT and Z3_OP_FINITE_SET_MAP_INVERSE - Clarified that Z3_OP_FINITE_SET_EXT returns a witness element demonstrating two sets are different (extensionality) - Clarified that Z3_OP_FINITE_SET_MAP_INVERSE relates to pre-image reasoning 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> --- src/api/api_ast.cpp | 19 +++++++++++++++++++ src/api/z3_api.h | 41 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 60 insertions(+) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 36f8cc34f..f22716b19 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -1467,6 +1467,25 @@ extern "C" { } } + if (mk_c(c)->fsutil().get_family_id() == _d->get_family_id()) { + switch(_d->get_decl_kind()) { + case OP_FINITE_SET_EMPTY: return Z3_OP_FINITE_SET_EMPTY; + case OP_FINITE_SET_SINGLETON: return Z3_OP_FINITE_SET_SINGLETON; + case OP_FINITE_SET_UNION: return Z3_OP_FINITE_SET_UNION; + case OP_FINITE_SET_INTERSECT: return Z3_OP_FINITE_SET_INTERSECT; + case OP_FINITE_SET_DIFFERENCE: return Z3_OP_FINITE_SET_DIFFERENCE; + case OP_FINITE_SET_IN: return Z3_OP_FINITE_SET_IN; + case OP_FINITE_SET_SIZE: return Z3_OP_FINITE_SET_SIZE; + case OP_FINITE_SET_SUBSET: return Z3_OP_FINITE_SET_SUBSET; + case OP_FINITE_SET_MAP: return Z3_OP_FINITE_SET_MAP; + case OP_FINITE_SET_FILTER: return Z3_OP_FINITE_SET_FILTER; + case OP_FINITE_SET_RANGE: return Z3_OP_FINITE_SET_RANGE; + case OP_FINITE_SET_EXT: return Z3_OP_FINITE_SET_EXT; + case OP_FINITE_SET_MAP_INVERSE: return Z3_OP_FINITE_SET_MAP_INVERSE; + default: return Z3_OP_INTERNAL; + } + } + if (mk_c(c)->recfun().get_family_id() == _d->get_family_id()) return Z3_OP_RECURSIVE; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index ce9c2ce68..d2a41e27e 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -980,6 +980,32 @@ typedef enum 3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE, 4 = 100 = Z3_OP_FPA_RM_TOWARD_ZERO. + - Z3_OP_FINITE_SET_EMPTY: Empty finite set. + + - Z3_OP_FINITE_SET_SINGLETON: Finite set containing a single element. + + - Z3_OP_FINITE_SET_UNION: Union of two finite sets. + + - Z3_OP_FINITE_SET_INTERSECT: Intersection of two finite sets. + + - Z3_OP_FINITE_SET_DIFFERENCE: Difference of two finite sets. + + - Z3_OP_FINITE_SET_IN: Membership predicate for finite sets. + + - Z3_OP_FINITE_SET_SIZE: Cardinality of a finite set. + + - Z3_OP_FINITE_SET_SUBSET: Subset predicate for finite sets. + + - Z3_OP_FINITE_SET_MAP: Map operation on finite sets. + + - Z3_OP_FINITE_SET_FILTER: Filter operation on finite sets. + + - Z3_OP_FINITE_SET_RANGE: Range operation for finite sets of integers. + + - Z3_OP_FINITE_SET_EXT: Finite set extensionality. Returns a witness element that is in one set but not the other, demonstrating that two sets are different. + + - Z3_OP_FINITE_SET_MAP_INVERSE: Inverse image under a finite set map operation. Related to reasoning about the pre-image of elements under set mappings. + - Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional information is exposed. Tools may use the string representation of the function declaration to obtain more information. @@ -1315,6 +1341,21 @@ typedef enum { Z3_OP_FPA_BVWRAP, Z3_OP_FPA_BV2RM, + // Finite Sets + Z3_OP_FINITE_SET_EMPTY = 0xc000, + Z3_OP_FINITE_SET_SINGLETON, + Z3_OP_FINITE_SET_UNION, + Z3_OP_FINITE_SET_INTERSECT, + Z3_OP_FINITE_SET_DIFFERENCE, + Z3_OP_FINITE_SET_IN, + Z3_OP_FINITE_SET_SIZE, + Z3_OP_FINITE_SET_SUBSET, + Z3_OP_FINITE_SET_MAP, + Z3_OP_FINITE_SET_FILTER, + Z3_OP_FINITE_SET_RANGE, + Z3_OP_FINITE_SET_EXT, + Z3_OP_FINITE_SET_MAP_INVERSE, + Z3_OP_INTERNAL, Z3_OP_RECURSIVE,