From 299bbb81a1091b0a5071882f58a57fbcc8df776b Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 29 Oct 2025 23:19:28 +0000
Subject: [PATCH 1/5] Initial plan
From e85eaaefc1247b1891c19d772ce4050d91e7d4f5 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 29 Oct 2025 23:42:34 +0000
Subject: [PATCH 2/5] Add finite set API support for Java and C#
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
src/api/dotnet/Context.cs | 174 ++++++++++++++++++++++++++++++++
src/api/dotnet/FiniteSetSort.cs | 53 ++++++++++
src/api/java/Context.java | 139 +++++++++++++++++++++++++
src/api/java/FiniteSetSort.java | 42 ++++++++
4 files changed, 408 insertions(+)
create mode 100644 src/api/dotnet/FiniteSetSort.cs
create mode 100644 src/api/java/FiniteSetSort.java
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 49f183428..549b86193 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2442,6 +2442,180 @@ namespace Microsoft.Z3
#endregion
+ #region Finite Sets
+
+ ///
+ /// Create a finite set sort over the given element sort.
+ ///
+ public FiniteSetSort MkFiniteSetSort(Sort elemSort)
+ {
+ Debug.Assert(elemSort != null);
+
+ CheckContextMatch(elemSort);
+ return new FiniteSetSort(this, elemSort);
+ }
+
+ ///
+ /// Check if a sort is a finite set sort.
+ ///
+ public bool IsFiniteSetSort(Sort s)
+ {
+ Debug.Assert(s != null);
+
+ CheckContextMatch(s);
+ return Native.Z3_is_finite_set_sort(nCtx, s.NativeObject) != 0;
+ }
+
+ ///
+ /// Get the element sort (basis) of a finite set sort.
+ ///
+ public Sort GetFiniteSetSortBasis(Sort s)
+ {
+ Debug.Assert(s != null);
+
+ CheckContextMatch(s);
+ return Sort.Create(this, Native.Z3_get_finite_set_sort_basis(nCtx, s.NativeObject));
+ }
+
+ ///
+ /// Create an empty finite set.
+ ///
+ public Expr MkFiniteSetEmpty(Sort setSort)
+ {
+ Debug.Assert(setSort != null);
+
+ CheckContextMatch(setSort);
+ return Expr.Create(this, Native.Z3_mk_finite_set_empty(nCtx, setSort.NativeObject));
+ }
+
+ ///
+ /// Create a singleton finite set.
+ ///
+ public Expr MkFiniteSetSingleton(Expr elem)
+ {
+ Debug.Assert(elem != null);
+
+ CheckContextMatch(elem);
+ return Expr.Create(this, Native.Z3_mk_finite_set_singleton(nCtx, elem.NativeObject));
+ }
+
+ ///
+ /// Create the union of two finite sets.
+ ///
+ public Expr MkFiniteSetUnion(Expr s1, Expr s2)
+ {
+ Debug.Assert(s1 != null);
+ Debug.Assert(s2 != null);
+
+ CheckContextMatch(s1);
+ CheckContextMatch(s2);
+ return Expr.Create(this, Native.Z3_mk_finite_set_union(nCtx, s1.NativeObject, s2.NativeObject));
+ }
+
+ ///
+ /// Create the intersection of two finite sets.
+ ///
+ public Expr MkFiniteSetIntersect(Expr s1, Expr s2)
+ {
+ Debug.Assert(s1 != null);
+ Debug.Assert(s2 != null);
+
+ CheckContextMatch(s1);
+ CheckContextMatch(s2);
+ return Expr.Create(this, Native.Z3_mk_finite_set_intersect(nCtx, s1.NativeObject, s2.NativeObject));
+ }
+
+ ///
+ /// Create the difference of two finite sets.
+ ///
+ public Expr MkFiniteSetDifference(Expr s1, Expr s2)
+ {
+ Debug.Assert(s1 != null);
+ Debug.Assert(s2 != null);
+
+ CheckContextMatch(s1);
+ CheckContextMatch(s2);
+ return Expr.Create(this, Native.Z3_mk_finite_set_difference(nCtx, s1.NativeObject, s2.NativeObject));
+ }
+
+ ///
+ /// Check for membership in a finite set.
+ ///
+ public BoolExpr MkFiniteSetMember(Expr elem, Expr set)
+ {
+ Debug.Assert(elem != null);
+ Debug.Assert(set != null);
+
+ CheckContextMatch(elem);
+ CheckContextMatch(set);
+ return (BoolExpr)Expr.Create(this, Native.Z3_mk_finite_set_member(nCtx, elem.NativeObject, set.NativeObject));
+ }
+
+ ///
+ /// Get the cardinality of a finite set.
+ ///
+ public Expr MkFiniteSetSize(Expr set)
+ {
+ Debug.Assert(set != null);
+
+ CheckContextMatch(set);
+ return Expr.Create(this, Native.Z3_mk_finite_set_size(nCtx, set.NativeObject));
+ }
+
+ ///
+ /// Check if one finite set is a subset of another.
+ ///
+ public BoolExpr MkFiniteSetSubset(Expr s1, Expr s2)
+ {
+ Debug.Assert(s1 != null);
+ Debug.Assert(s2 != null);
+
+ CheckContextMatch(s1);
+ CheckContextMatch(s2);
+ return (BoolExpr)Expr.Create(this, Native.Z3_mk_finite_set_subset(nCtx, s1.NativeObject, s2.NativeObject));
+ }
+
+ ///
+ /// Map a function over all elements in a finite set.
+ ///
+ public Expr MkFiniteSetMap(Expr f, Expr set)
+ {
+ Debug.Assert(f != null);
+ Debug.Assert(set != null);
+
+ CheckContextMatch(f);
+ CheckContextMatch(set);
+ return Expr.Create(this, Native.Z3_mk_finite_set_map(nCtx, f.NativeObject, set.NativeObject));
+ }
+
+ ///
+ /// Filter a finite set with a predicate.
+ ///
+ public Expr MkFiniteSetFilter(Expr f, Expr set)
+ {
+ Debug.Assert(f != null);
+ Debug.Assert(set != null);
+
+ CheckContextMatch(f);
+ CheckContextMatch(set);
+ return Expr.Create(this, Native.Z3_mk_finite_set_filter(nCtx, f.NativeObject, set.NativeObject));
+ }
+
+ ///
+ /// Create a finite set containing integers in the range [low, high].
+ ///
+ public Expr MkFiniteSetRange(Expr low, Expr high)
+ {
+ Debug.Assert(low != null);
+ Debug.Assert(high != null);
+
+ CheckContextMatch(low);
+ CheckContextMatch(high);
+ return Expr.Create(this, Native.Z3_mk_finite_set_range(nCtx, low.NativeObject, high.NativeObject));
+ }
+
+ #endregion
+
#region Sequence, string and regular expressions
///
diff --git a/src/api/dotnet/FiniteSetSort.cs b/src/api/dotnet/FiniteSetSort.cs
new file mode 100644
index 000000000..dda981cf9
--- /dev/null
+++ b/src/api/dotnet/FiniteSetSort.cs
@@ -0,0 +1,53 @@
+/*++
+Copyright (c) 2024 Microsoft Corporation
+
+Module Name:
+
+ FiniteSetSort.cs
+
+Abstract:
+
+ Z3 Managed API: Finite Set Sorts
+
+Author:
+
+ GitHub Copilot
+
+Notes:
+
+--*/
+
+using System.Diagnostics;
+using System;
+
+namespace Microsoft.Z3
+{
+ ///
+ /// Finite set sorts.
+ ///
+ public class FiniteSetSort : Sort
+ {
+ #region Internal
+ internal FiniteSetSort(Context ctx, IntPtr obj)
+ : base(ctx, obj)
+ {
+ Debug.Assert(ctx != null);
+ }
+
+ internal FiniteSetSort(Context ctx, Sort elemSort)
+ : base(ctx, Native.Z3_mk_finite_set_sort(ctx.nCtx, elemSort.NativeObject))
+ {
+ Debug.Assert(ctx != null);
+ Debug.Assert(elemSort != null);
+ }
+ #endregion
+
+ ///
+ /// Get the element sort (basis) of this finite set sort.
+ ///
+ public Sort Basis
+ {
+ get { return Sort.Create(Context, Native.Z3_get_finite_set_sort_basis(Context.nCtx, NativeObject)); }
+ }
+ }
+}
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 691ecd737..d410b5c39 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -2052,6 +2052,145 @@ public class Context implements AutoCloseable {
}
+ /**
+ * Finite Sets
+ */
+
+ /**
+ * Create a finite set sort over the given element sort.
+ **/
+ public final FiniteSetSort mkFiniteSetSort(Sort elemSort)
+ {
+ checkContextMatch(elemSort);
+ return new FiniteSetSort(this, elemSort);
+ }
+
+ /**
+ * Check if a sort is a finite set sort.
+ **/
+ public final boolean isFiniteSetSort(Sort s)
+ {
+ checkContextMatch(s);
+ return Native.isFiniteSetSort(nCtx(), s.getNativeObject());
+ }
+
+ /**
+ * Get the element sort (basis) of a finite set sort.
+ **/
+ public final Sort getFiniteSetSortBasis(Sort s)
+ {
+ checkContextMatch(s);
+ return Sort.create(this, Native.getFiniteSetSortBasis(nCtx(), s.getNativeObject()));
+ }
+
+ /**
+ * Create an empty finite set.
+ **/
+ public final Expr mkFiniteSetEmpty(Sort setSort)
+ {
+ checkContextMatch(setSort);
+ return Expr.create(this, Native.mkFiniteSetEmpty(nCtx(), setSort.getNativeObject()));
+ }
+
+ /**
+ * Create a singleton finite set.
+ **/
+ public final Expr mkFiniteSetSingleton(Expr elem)
+ {
+ checkContextMatch(elem);
+ return Expr.create(this, Native.mkFiniteSetSingleton(nCtx(), elem.getNativeObject()));
+ }
+
+ /**
+ * Create the union of two finite sets.
+ **/
+ public final Expr mkFiniteSetUnion(Expr s1, Expr s2)
+ {
+ checkContextMatch(s1);
+ checkContextMatch(s2);
+ return Expr.create(this, Native.mkFiniteSetUnion(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+ }
+
+ /**
+ * Create the intersection of two finite sets.
+ **/
+ public final Expr mkFiniteSetIntersect(Expr s1, Expr s2)
+ {
+ checkContextMatch(s1);
+ checkContextMatch(s2);
+ return Expr.create(this, Native.mkFiniteSetIntersect(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+ }
+
+ /**
+ * Create the difference of two finite sets.
+ **/
+ public final Expr mkFiniteSetDifference(Expr s1, Expr s2)
+ {
+ checkContextMatch(s1);
+ checkContextMatch(s2);
+ return Expr.create(this, Native.mkFiniteSetDifference(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+ }
+
+ /**
+ * Check for membership in a finite set.
+ **/
+ public final BoolExpr mkFiniteSetMember(Expr elem, Expr set)
+ {
+ checkContextMatch(elem);
+ checkContextMatch(set);
+ return (BoolExpr) Expr.create(this, Native.mkFiniteSetMember(nCtx(), elem.getNativeObject(), set.getNativeObject()));
+ }
+
+ /**
+ * Get the cardinality of a finite set.
+ **/
+ public final Expr mkFiniteSetSize(Expr set)
+ {
+ checkContextMatch(set);
+ return Expr.create(this, Native.mkFiniteSetSize(nCtx(), set.getNativeObject()));
+ }
+
+ /**
+ * Check if one finite set is a subset of another.
+ **/
+ public final BoolExpr mkFiniteSetSubset(Expr s1, Expr s2)
+ {
+ checkContextMatch(s1);
+ checkContextMatch(s2);
+ return (BoolExpr) Expr.create(this, Native.mkFiniteSetSubset(nCtx(), s1.getNativeObject(), s2.getNativeObject()));
+ }
+
+ /**
+ * Map a function over all elements in a finite set.
+ **/
+ public final Expr mkFiniteSetMap(Expr f, Expr set)
+ {
+ checkContextMatch(f);
+ checkContextMatch(set);
+ return Expr.create(this, Native.mkFiniteSetMap(nCtx(), f.getNativeObject(), set.getNativeObject()));
+ }
+
+ /**
+ * Filter a finite set with a predicate.
+ **/
+ public final Expr mkFiniteSetFilter(Expr f, Expr set)
+ {
+ checkContextMatch(f);
+ checkContextMatch(set);
+ return Expr.create(this, Native.mkFiniteSetFilter(nCtx(), f.getNativeObject(), set.getNativeObject()));
+ }
+
+ /**
+ * Create a finite set containing integers in the range [low, high].
+ **/
+ public final Expr mkFiniteSetRange(Expr low, Expr high)
+ {
+ checkContextMatch(low);
+ checkContextMatch(high);
+ return Expr.create(this, Native.mkFiniteSetRange(nCtx(), low.getNativeObject(), high.getNativeObject()));
+ }
+
+
/**
* Sequences, Strings and regular expressions.
*/
diff --git a/src/api/java/FiniteSetSort.java b/src/api/java/FiniteSetSort.java
new file mode 100644
index 000000000..031199539
--- /dev/null
+++ b/src/api/java/FiniteSetSort.java
@@ -0,0 +1,42 @@
+/**
+Copyright (c) 2024 Microsoft Corporation
+
+Module Name:
+
+ FiniteSetSort.java
+
+Abstract:
+
+Author:
+
+ GitHub Copilot
+
+Notes:
+
+**/
+
+package com.microsoft.z3;
+
+/**
+ * Finite set sorts.
+ **/
+public class FiniteSetSort extends Sort
+{
+ FiniteSetSort(Context ctx, long obj)
+ {
+ super(ctx, obj);
+ }
+
+ FiniteSetSort(Context ctx, Sort elemSort)
+ {
+ super(ctx, Native.mkFiniteSetSort(ctx.nCtx(), elemSort.getNativeObject()));
+ }
+
+ /**
+ * Get the element sort (basis) of this finite set sort.
+ **/
+ public Sort getBasis()
+ {
+ return Sort.create(getContext(), Native.getFiniteSetSortBasis(getContext().nCtx(), getNativeObject()));
+ }
+}
From f1d91f44ca3ed7d6bc43ff004d562b4e84e9a1e5 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Wed, 29 Oct 2025 23:50:44 +0000
Subject: [PATCH 3/5] Add documentation and examples for finite set APIs
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
FINITE_SET_API_EXAMPLES.md | 140 +++++++++++++++++++++++++++++++++++++
1 file changed, 140 insertions(+)
create mode 100644 FINITE_SET_API_EXAMPLES.md
diff --git a/FINITE_SET_API_EXAMPLES.md b/FINITE_SET_API_EXAMPLES.md
new file mode 100644
index 000000000..e180fb7f4
--- /dev/null
+++ b/FINITE_SET_API_EXAMPLES.md
@@ -0,0 +1,140 @@
+# Finite Set API Examples
+
+This document provides usage examples for the finite set API in Java and C#.
+
+## Java Example
+
+```java
+import com.microsoft.z3.*;
+
+public class FiniteSetExample {
+ public static void main(String[] args) {
+ try (Context ctx = new Context()) {
+ // Create finite set sort over integers
+ Sort intSort = ctx.getIntSort();
+ FiniteSetSort intSetSort = ctx.mkFiniteSetSort(intSort);
+
+ // Check if it's a finite set sort
+ boolean isFiniteSet = ctx.isFiniteSetSort(intSetSort);
+ System.out.println("Is finite set sort: " + isFiniteSet);
+
+ // Get the element sort (basis)
+ Sort basis = ctx.getFiniteSetSortBasis(intSetSort);
+ System.out.println("Element sort: " + basis);
+
+ // Create sets
+ Expr emptySet = ctx.mkFiniteSetEmpty(intSetSort);
+ IntExpr one = ctx.mkInt(1);
+ IntExpr two = ctx.mkInt(2);
+ Expr singleton1 = ctx.mkFiniteSetSingleton(one);
+ Expr singleton2 = ctx.mkFiniteSetSingleton(two);
+
+ // Set operations
+ Expr union = ctx.mkFiniteSetUnion(singleton1, singleton2);
+ Expr intersect = ctx.mkFiniteSetIntersect(union, singleton1);
+ Expr difference = ctx.mkFiniteSetDifference(union, singleton1);
+
+ // Set queries
+ BoolExpr member = ctx.mkFiniteSetMember(one, union);
+ Expr size = ctx.mkFiniteSetSize(union);
+ BoolExpr subset = ctx.mkFiniteSetSubset(singleton1, union);
+
+ // Create integer range [1..10]
+ Expr range = ctx.mkFiniteSetRange(ctx.mkInt(1), ctx.mkInt(10));
+
+ // Solve with finite sets
+ Solver solver = ctx.mkSolver();
+ solver.add(ctx.mkFiniteSetMember(one, union));
+ solver.add(ctx.mkEq(ctx.mkFiniteSetSize(union), ctx.mkInt(2)));
+ Status status = solver.check();
+ System.out.println("Solver result: " + status);
+ }
+ }
+}
+```
+
+## C# Example
+
+```csharp
+using System;
+using Microsoft.Z3;
+
+class FiniteSetExample
+{
+ static void Main(string[] args)
+ {
+ using (Context ctx = new Context())
+ {
+ // Create finite set sort over integers
+ Sort intSort = ctx.IntSort;
+ FiniteSetSort intSetSort = ctx.MkFiniteSetSort(intSort);
+
+ // Check if it's a finite set sort
+ bool isFiniteSet = ctx.IsFiniteSetSort(intSetSort);
+ Console.WriteLine($"Is finite set sort: {isFiniteSet}");
+
+ // Get the element sort (basis)
+ Sort basis = ctx.GetFiniteSetSortBasis(intSetSort);
+ // Or use the property:
+ Sort basis2 = intSetSort.Basis;
+ Console.WriteLine($"Element sort: {basis}");
+
+ // Create sets
+ Expr emptySet = ctx.MkFiniteSetEmpty(intSetSort);
+ IntExpr one = ctx.MkInt(1);
+ IntExpr two = ctx.MkInt(2);
+ Expr singleton1 = ctx.MkFiniteSetSingleton(one);
+ Expr singleton2 = ctx.MkFiniteSetSingleton(two);
+
+ // Set operations
+ Expr union = ctx.MkFiniteSetUnion(singleton1, singleton2);
+ Expr intersect = ctx.MkFiniteSetIntersect(union, singleton1);
+ Expr difference = ctx.MkFiniteSetDifference(union, singleton1);
+
+ // Set queries
+ BoolExpr member = ctx.MkFiniteSetMember(one, union);
+ Expr size = ctx.MkFiniteSetSize(union);
+ BoolExpr subset = ctx.MkFiniteSetSubset(singleton1, union);
+
+ // Create integer range [1..10]
+ Expr range = ctx.MkFiniteSetRange(ctx.MkInt(1), ctx.MkInt(10));
+
+ // Solve with finite sets
+ Solver solver = ctx.MkSolver();
+ solver.Add(ctx.MkFiniteSetMember(one, union));
+ solver.Add(ctx.MkEq(ctx.MkFiniteSetSize(union), ctx.MkInt(2)));
+ Status status = solver.Check();
+ Console.WriteLine($"Solver result: {status}");
+ }
+ }
+}
+```
+
+## API Methods
+
+### Sort Operations
+- **Java**: `mkFiniteSetSort(Sort elemSort)`, `isFiniteSetSort(Sort s)`, `getFiniteSetSortBasis(Sort s)`
+- **C#**: `MkFiniteSetSort(Sort elemSort)`, `IsFiniteSetSort(Sort s)`, `GetFiniteSetSortBasis(Sort s)`
+
+### Set Constructors
+- **Java**: `mkFiniteSetEmpty(Sort setSort)`, `mkFiniteSetSingleton(Expr elem)`, `mkFiniteSetRange(Expr low, Expr high)`
+- **C#**: `MkFiniteSetEmpty(Sort setSort)`, `MkFiniteSetSingleton(Expr elem)`, `MkFiniteSetRange(Expr low, Expr high)`
+
+### Set Operations
+- **Java**: `mkFiniteSetUnion(Expr s1, Expr s2)`, `mkFiniteSetIntersect(Expr s1, Expr s2)`, `mkFiniteSetDifference(Expr s1, Expr s2)`
+- **C#**: `MkFiniteSetUnion(Expr s1, Expr s2)`, `MkFiniteSetIntersect(Expr s1, Expr s2)`, `MkFiniteSetDifference(Expr s1, Expr s2)`
+
+### Set Queries
+- **Java**: `mkFiniteSetMember(Expr elem, Expr set)`, `mkFiniteSetSize(Expr set)`, `mkFiniteSetSubset(Expr s1, Expr s2)`
+- **C#**: `MkFiniteSetMember(Expr elem, Expr set)`, `MkFiniteSetSize(Expr set)`, `MkFiniteSetSubset(Expr s1, Expr s2)`
+
+### Set Transformations
+- **Java**: `mkFiniteSetMap(Expr f, Expr set)`, `mkFiniteSetFilter(Expr f, Expr set)`
+- **C#**: `MkFiniteSetMap(Expr f, Expr set)`, `MkFiniteSetFilter(Expr f, Expr set)`
+
+## Notes
+
+- Finite sets are distinct from array-based sets and provide a more direct representation
+- The finite set sort extends `Sort` directly (not `ArraySort`)
+- All operations follow the SMT-LIB2 finite set theory syntax
+- Native bindings are auto-generated from the C API during build
From 8871390b5cf171925a9c4158fd12fc6a37e5f80d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner
Date: Wed, 29 Oct 2025 16:54:16 -0700
Subject: [PATCH 4/5] Delete FINITE_SET_API_EXAMPLES.md
---
FINITE_SET_API_EXAMPLES.md | 140 -------------------------------------
1 file changed, 140 deletions(-)
delete mode 100644 FINITE_SET_API_EXAMPLES.md
diff --git a/FINITE_SET_API_EXAMPLES.md b/FINITE_SET_API_EXAMPLES.md
deleted file mode 100644
index e180fb7f4..000000000
--- a/FINITE_SET_API_EXAMPLES.md
+++ /dev/null
@@ -1,140 +0,0 @@
-# Finite Set API Examples
-
-This document provides usage examples for the finite set API in Java and C#.
-
-## Java Example
-
-```java
-import com.microsoft.z3.*;
-
-public class FiniteSetExample {
- public static void main(String[] args) {
- try (Context ctx = new Context()) {
- // Create finite set sort over integers
- Sort intSort = ctx.getIntSort();
- FiniteSetSort intSetSort = ctx.mkFiniteSetSort(intSort);
-
- // Check if it's a finite set sort
- boolean isFiniteSet = ctx.isFiniteSetSort(intSetSort);
- System.out.println("Is finite set sort: " + isFiniteSet);
-
- // Get the element sort (basis)
- Sort basis = ctx.getFiniteSetSortBasis(intSetSort);
- System.out.println("Element sort: " + basis);
-
- // Create sets
- Expr emptySet = ctx.mkFiniteSetEmpty(intSetSort);
- IntExpr one = ctx.mkInt(1);
- IntExpr two = ctx.mkInt(2);
- Expr singleton1 = ctx.mkFiniteSetSingleton(one);
- Expr singleton2 = ctx.mkFiniteSetSingleton(two);
-
- // Set operations
- Expr union = ctx.mkFiniteSetUnion(singleton1, singleton2);
- Expr intersect = ctx.mkFiniteSetIntersect(union, singleton1);
- Expr difference = ctx.mkFiniteSetDifference(union, singleton1);
-
- // Set queries
- BoolExpr member = ctx.mkFiniteSetMember(one, union);
- Expr size = ctx.mkFiniteSetSize(union);
- BoolExpr subset = ctx.mkFiniteSetSubset(singleton1, union);
-
- // Create integer range [1..10]
- Expr range = ctx.mkFiniteSetRange(ctx.mkInt(1), ctx.mkInt(10));
-
- // Solve with finite sets
- Solver solver = ctx.mkSolver();
- solver.add(ctx.mkFiniteSetMember(one, union));
- solver.add(ctx.mkEq(ctx.mkFiniteSetSize(union), ctx.mkInt(2)));
- Status status = solver.check();
- System.out.println("Solver result: " + status);
- }
- }
-}
-```
-
-## C# Example
-
-```csharp
-using System;
-using Microsoft.Z3;
-
-class FiniteSetExample
-{
- static void Main(string[] args)
- {
- using (Context ctx = new Context())
- {
- // Create finite set sort over integers
- Sort intSort = ctx.IntSort;
- FiniteSetSort intSetSort = ctx.MkFiniteSetSort(intSort);
-
- // Check if it's a finite set sort
- bool isFiniteSet = ctx.IsFiniteSetSort(intSetSort);
- Console.WriteLine($"Is finite set sort: {isFiniteSet}");
-
- // Get the element sort (basis)
- Sort basis = ctx.GetFiniteSetSortBasis(intSetSort);
- // Or use the property:
- Sort basis2 = intSetSort.Basis;
- Console.WriteLine($"Element sort: {basis}");
-
- // Create sets
- Expr emptySet = ctx.MkFiniteSetEmpty(intSetSort);
- IntExpr one = ctx.MkInt(1);
- IntExpr two = ctx.MkInt(2);
- Expr singleton1 = ctx.MkFiniteSetSingleton(one);
- Expr singleton2 = ctx.MkFiniteSetSingleton(two);
-
- // Set operations
- Expr union = ctx.MkFiniteSetUnion(singleton1, singleton2);
- Expr intersect = ctx.MkFiniteSetIntersect(union, singleton1);
- Expr difference = ctx.MkFiniteSetDifference(union, singleton1);
-
- // Set queries
- BoolExpr member = ctx.MkFiniteSetMember(one, union);
- Expr size = ctx.MkFiniteSetSize(union);
- BoolExpr subset = ctx.MkFiniteSetSubset(singleton1, union);
-
- // Create integer range [1..10]
- Expr range = ctx.MkFiniteSetRange(ctx.MkInt(1), ctx.MkInt(10));
-
- // Solve with finite sets
- Solver solver = ctx.MkSolver();
- solver.Add(ctx.MkFiniteSetMember(one, union));
- solver.Add(ctx.MkEq(ctx.MkFiniteSetSize(union), ctx.MkInt(2)));
- Status status = solver.Check();
- Console.WriteLine($"Solver result: {status}");
- }
- }
-}
-```
-
-## API Methods
-
-### Sort Operations
-- **Java**: `mkFiniteSetSort(Sort elemSort)`, `isFiniteSetSort(Sort s)`, `getFiniteSetSortBasis(Sort s)`
-- **C#**: `MkFiniteSetSort(Sort elemSort)`, `IsFiniteSetSort(Sort s)`, `GetFiniteSetSortBasis(Sort s)`
-
-### Set Constructors
-- **Java**: `mkFiniteSetEmpty(Sort setSort)`, `mkFiniteSetSingleton(Expr elem)`, `mkFiniteSetRange(Expr low, Expr high)`
-- **C#**: `MkFiniteSetEmpty(Sort setSort)`, `MkFiniteSetSingleton(Expr elem)`, `MkFiniteSetRange(Expr low, Expr high)`
-
-### Set Operations
-- **Java**: `mkFiniteSetUnion(Expr s1, Expr s2)`, `mkFiniteSetIntersect(Expr s1, Expr s2)`, `mkFiniteSetDifference(Expr s1, Expr s2)`
-- **C#**: `MkFiniteSetUnion(Expr s1, Expr s2)`, `MkFiniteSetIntersect(Expr s1, Expr s2)`, `MkFiniteSetDifference(Expr s1, Expr s2)`
-
-### Set Queries
-- **Java**: `mkFiniteSetMember(Expr elem, Expr set)`, `mkFiniteSetSize(Expr set)`, `mkFiniteSetSubset(Expr s1, Expr s2)`
-- **C#**: `MkFiniteSetMember(Expr elem, Expr set)`, `MkFiniteSetSize(Expr set)`, `MkFiniteSetSubset(Expr s1, Expr s2)`
-
-### Set Transformations
-- **Java**: `mkFiniteSetMap(Expr f, Expr set)`, `mkFiniteSetFilter(Expr f, Expr set)`
-- **C#**: `MkFiniteSetMap(Expr f, Expr set)`, `MkFiniteSetFilter(Expr f, Expr set)`
-
-## Notes
-
-- Finite sets are distinct from array-based sets and provide a more direct representation
-- The finite set sort extends `Sort` directly (not `ArraySort`)
-- All operations follow the SMT-LIB2 finite set theory syntax
-- Native bindings are auto-generated from the C API during build
From f234acd7d9cb6e7f71e95350c255daab969b2754 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 30 Oct 2025 15:47:32 +0000
Subject: [PATCH 5/5] Add FiniteSetSort files to CMakeLists.txt build
configurations
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
src/api/dotnet/CMakeLists.txt | 1 +
src/api/java/CMakeLists.txt | 1 +
2 files changed, 2 insertions(+)
diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index d3cb87bc7..c309f4027 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -64,6 +64,7 @@ set(Z3_DOTNET_ASSEMBLY_SOURCES_IN_SRC_TREE
FiniteDomainExpr.cs
FiniteDomainNum.cs
FiniteDomainSort.cs
+ FiniteSetSort.cs
Fixedpoint.cs
FPExpr.cs
FPNum.cs
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index c5221014f..2afd6ad56 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -115,6 +115,7 @@ set(Z3_JAVA_JAR_SOURCE_FILES
FiniteDomainExpr.java
FiniteDomainNum.java
FiniteDomainSort.java
+ FiniteSetSort.java
Fixedpoint.java
FPExpr.java
FPNum.java