Merge f234acd7d9 into 98090fbf50

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)); }
+        }
+    }
+}

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

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.
      */

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()));
+    }
+}