From 7ab00496124a5e81bc44970b86a7199172215cab Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 21 Oct 2025 20:29:12 +0000
Subject: [PATCH] Add documentation for finite set API

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 FINITE_SET_API.md | 154 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 154 insertions(+)
 create mode 100644 FINITE_SET_API.md

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++.h>
+
+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