Add finite set API support for C# and Java bindings (#8003)

* Initial plan

* Add finite set API support for Java and C#

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add documentation and examples for finite set APIs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Delete FINITE_SET_API_EXAMPLES.md

* Add FiniteSetSort files to CMakeLists.txt build configurations

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>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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

src/api/dotnet/Context.cs

@@ -2442,6 +2442,180 @@ namespace Microsoft.Z3
 
         #endregion
 
+        #region Finite Sets
+
+        /// <summary>
+        /// Create a finite set sort over the given element sort.
+        /// </summary>
+        public FiniteSetSort MkFiniteSetSort(Sort elemSort)
+        {
+            Debug.Assert(elemSort != null);
+
+            CheckContextMatch(elemSort);
+            return new FiniteSetSort(this, elemSort);
+        }
+
+        /// <summary>
+        /// Check if a sort is a finite set sort.
+        /// </summary>
+        public bool IsFiniteSetSort(Sort s)
+        {
+            Debug.Assert(s != null);
+
+            CheckContextMatch(s);
+            return Native.Z3_is_finite_set_sort(nCtx, s.NativeObject) != 0;
+        }
+
+        /// <summary>
+        /// Get the element sort (basis) of a finite set sort.
+        /// </summary>
+        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));
+        }
+
+        /// <summary>
+        /// Create an empty finite set.
+        /// </summary>
+        public Expr MkFiniteSetEmpty(Sort setSort)
+        {
+            Debug.Assert(setSort != null);
+
+            CheckContextMatch(setSort);
+            return Expr.Create(this, Native.Z3_mk_finite_set_empty(nCtx, setSort.NativeObject));
+        }
+
+        /// <summary>
+        /// Create a singleton finite set.
+        /// </summary>
+        public Expr MkFiniteSetSingleton(Expr elem)
+        {
+            Debug.Assert(elem != null);
+
+            CheckContextMatch(elem);
+            return Expr.Create(this, Native.Z3_mk_finite_set_singleton(nCtx, elem.NativeObject));
+        }
+
+        /// <summary>
+        /// Create the union of two finite sets.
+        /// </summary>
+        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));
+        }
+
+        /// <summary>
+        /// Create the intersection of two finite sets.
+        /// </summary>
+        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));
+        }
+
+        /// <summary>
+        /// Create the difference of two finite sets.
+        /// </summary>
+        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));
+        }
+
+        /// <summary>
+        /// Check for membership in a finite set.
+        /// </summary>
+        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));
+        }
+
+        /// <summary>
+        /// Get the cardinality of a finite set.
+        /// </summary>
+        public Expr MkFiniteSetSize(Expr set)
+        {
+            Debug.Assert(set != null);
+
+            CheckContextMatch(set);
+            return Expr.Create(this, Native.Z3_mk_finite_set_size(nCtx, set.NativeObject));
+        }
+
+        /// <summary>
+        /// Check if one finite set is a subset of another.
+        /// </summary>
+        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));
+        }
+
+        /// <summary>
+        /// Map a function over all elements in a finite set.
+        /// </summary>
+        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));
+        }
+
+        /// <summary>
+        /// Filter a finite set with a predicate.
+        /// </summary>
+        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));
+        }
+
+        /// <summary>
+        /// Create a finite set containing integers in the range [low, high].
+        /// </summary>
+        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
 
         /// <summary>

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
+{
+    /// <summary>
+    /// Finite set sorts.
+    /// </summary>
+    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
+
+        /// <summary>
+        /// Get the element sort (basis) of this finite set sort.
+        /// </summary>
+        public Sort Basis
+        {
+            get { return Sort.Create(Context, Native.Z3_get_finite_set_sort_basis(Context.nCtx, NativeObject)); }
+        }
+    }
+}