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

[WIP] Add finite set operators to Z3_decl_kind enumeration (#8004)

Browse source 
* 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>
This commit is contained in:
Copilot 2025-10-29 16:52:38 -07:00 • committed by GitHub
parent 4536985bf7
commit 450412c854
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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())
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,
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,