mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-13 09:31:14 +00:00
Code Activity

Improve documentation for Z3_OP_FINITE_SET_EXT and Z3_OP_FINITE_SET_MAP_INVERSE

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

4
src/api/z3_api.h
View file

@ -1002,9 +1002,9 @@ typedef enum
- Z3_OP_FINITE_SET_RANGE: Range operation for finite sets of integers. - Z3_OP_FINITE_SET_RANGE: Range operation for finite sets of integers.
- Z3_OP_FINITE_SET_EXT: Finite set extensionality. - 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 of a finite set map operation. - 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 - 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