mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-07 14:55:06 +00:00
Code Activity

Add Z3_decl_kind enumeration for finite_set operators

Browse source 
- 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>
This commit is contained in:
copilot-swe-agent[bot] 2025-10-29 23:46:17 +00:00
parent ffe9b9b5c3
commit 69b836afce
2 changed files with 60 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/api/api_ast.cpp
View file

@ -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()) if (mk_c(c)->recfun().get_family_id() == _d->get_family_id())
return Z3_OP_RECURSIVE; return Z3_OP_RECURSIVE;

41
src/api/z3_api.h
View file

@ -980,6 +980,32 @@ typedef enum
3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE, 3 = 011 = Z3_OP_FPA_RM_TOWARD_NEGATIVE,
4 = 100 = Z3_OP_FPA_RM_TOWARD_ZERO. 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.
- Z3_OP_FINITE_SET_MAP_INVERSE: Inverse of a finite set map operation.
- Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional - Z3_OP_INTERNAL: internal (often interpreted) symbol, but no additional
information is exposed. Tools may use the string representation of the information is exposed. Tools may use the string representation of the
function declaration to obtain more information. function declaration to obtain more information.
@ -1315,6 +1341,21 @@ typedef enum {
Z3_OP_FPA_BVWRAP, Z3_OP_FPA_BVWRAP,
Z3_OP_FPA_BV2RM, 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_INTERNAL,
Z3_OP_RECURSIVE, Z3_OP_RECURSIVE,