Merge pull request #8703 from Z3Prover/copilot/fix-finite-set-apis

Add FiniteSet API support to Go, OCaml, and JavaScript/TypeScript bindings

src/api/go/finiteset.go

@@ -0,0 +1,78 @@
+package z3
+
+/*
+#include "z3.h"
+*/
+import "C"
+
+// Finite set operations
+
+// MkFiniteSetSort creates a finite set sort with the given element sort.
+func (c *Context) MkFiniteSetSort(elemSort *Sort) *Sort {
+	return newSort(c, C.Z3_mk_finite_set_sort(c.ptr, elemSort.ptr))
+}
+
+// IsFiniteSetSort returns true if the given sort is a finite set sort.
+func (c *Context) IsFiniteSetSort(s *Sort) bool {
+	return bool(C.Z3_is_finite_set_sort(c.ptr, s.ptr))
+}
+
+// GetFiniteSetSortBasis returns the element sort of a finite set sort.
+func (c *Context) GetFiniteSetSortBasis(s *Sort) *Sort {
+	return newSort(c, C.Z3_get_finite_set_sort_basis(c.ptr, s.ptr))
+}
+
+// MkFiniteSetEmpty creates an empty finite set of the given sort.
+func (c *Context) MkFiniteSetEmpty(setSort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_empty(c.ptr, setSort.ptr))
+}
+
+// MkFiniteSetSingleton creates a singleton finite set containing the given element.
+func (c *Context) MkFiniteSetSingleton(elem *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_singleton(c.ptr, elem.ptr))
+}
+
+// MkFiniteSetUnion creates the union of two finite sets.
+func (c *Context) MkFiniteSetUnion(s1, s2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_union(c.ptr, s1.ptr, s2.ptr))
+}
+
+// MkFiniteSetIntersect creates the intersection of two finite sets.
+func (c *Context) MkFiniteSetIntersect(s1, s2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_intersect(c.ptr, s1.ptr, s2.ptr))
+}
+
+// MkFiniteSetDifference creates the set difference of two finite sets (s1 \ s2).
+func (c *Context) MkFiniteSetDifference(s1, s2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_difference(c.ptr, s1.ptr, s2.ptr))
+}
+
+// MkFiniteSetMember creates a membership predicate: elem ∈ set.
+func (c *Context) MkFiniteSetMember(elem, set *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_member(c.ptr, elem.ptr, set.ptr))
+}
+
+// MkFiniteSetSize creates an expression for the cardinality of a finite set.
+func (c *Context) MkFiniteSetSize(set *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_size(c.ptr, set.ptr))
+}
+
+// MkFiniteSetSubset creates a subset predicate: s1 ⊆ s2.
+func (c *Context) MkFiniteSetSubset(s1, s2 *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_subset(c.ptr, s1.ptr, s2.ptr))
+}
+
+// MkFiniteSetMap applies a function to all elements of a finite set.
+func (c *Context) MkFiniteSetMap(f, set *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_map(c.ptr, f.ptr, set.ptr))
+}
+
+// MkFiniteSetFilter filters a finite set using a predicate function.
+func (c *Context) MkFiniteSetFilter(f, set *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_filter(c.ptr, f.ptr, set.ptr))
+}
+
+// MkFiniteSetRange creates a finite set of integers in the range [low, high].
+func (c *Context) MkFiniteSetRange(low, high *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_finite_set_range(c.ptr, low.ptr, high.ptr))
+}

src/api/js/src/high-level/high-level.ts

@@ -123,6 +123,9 @@ import {
   DatatypeSort,
   DatatypeExpr,
   DatatypeCreation,
+  FiniteSet,
+  FiniteSetSort,
+  FiniteSetCreation,
 } from './types';
 import { allSatisfy, assert, assertExhaustive } from './utils';
 
@@ -305,6 +308,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         case Z3_sort_kind.Z3_ARRAY_SORT:
           return new ArraySortImpl(ast);
         default:
+          if (Z3.is_finite_set_sort(contextPtr, ast)) {
+            return new FiniteSetSortImpl(ast);
+          }
           return new SortImpl(ast);
       }
     }
@@ -350,6 +356,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         case Z3_sort_kind.Z3_ARRAY_SORT:
           return new ArrayImpl(ast);
         default:
+          if (Z3.is_finite_set_sort(contextPtr, Z3.get_sort(contextPtr, ast))) {
+            return new FiniteSetImpl(ast);
+          }
           return new ExprImpl(ast);
       }
     }
@@ -638,6 +647,18 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       return isSeq(obj) && obj.isString();
     }
 
+    function isFiniteSetSort(obj: unknown): obj is FiniteSetSort<Name> {
+      const r = obj instanceof FiniteSetSortImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
+    function isFiniteSet(obj: unknown): obj is FiniteSet<Name> {
+      const r = obj instanceof FiniteSetImpl;
+      r && _assertContext(obj);
+      return r;
+    }
+
     function isProbe(obj: unknown): obj is Probe<Name> {
       const r = obj instanceof ProbeImpl;
       r && _assertContext(obj);
@@ -1104,6 +1125,32 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       },
     };
 
+    const FiniteSet = {
+      sort<ElemSort extends Sort<Name>>(elemSort: ElemSort): FiniteSetSort<Name, ElemSort> {
+        return new FiniteSetSortImpl<ElemSort>(check(Z3.mk_finite_set_sort(contextPtr, elemSort.ptr)));
+      },
+      const<ElemSort extends Sort<Name>>(name: string, elemSort: ElemSort): FiniteSet<Name, ElemSort> {
+        return new FiniteSetImpl<ElemSort>(
+          check(Z3.mk_const(contextPtr, _toSymbol(name), FiniteSet.sort(elemSort).ptr)),
+        );
+      },
+      consts<ElemSort extends Sort<Name>>(names: string | string[], elemSort: ElemSort): FiniteSet<Name, ElemSort>[] {
+        if (typeof names === 'string') {
+          names = names.split(' ');
+        }
+        return names.map(name => FiniteSet.const(name, elemSort));
+      },
+      empty<ElemSort extends Sort<Name>>(sort: ElemSort): FiniteSet<Name, ElemSort> {
+        return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_empty(contextPtr, FiniteSet.sort(sort).ptr)));
+      },
+      singleton<ElemSort extends Sort<Name>>(elem: Expr<Name>): FiniteSet<Name, ElemSort> {
+        return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_singleton(contextPtr, elem.ast)));
+      },
+      range(low: Expr<Name>, high: Expr<Name>): FiniteSet<Name, Sort<Name>> {
+        return new FiniteSetImpl(check(Z3.mk_finite_set_range(contextPtr, low.ast, high.ast)));
+      },
+    };
+
     const Datatype = Object.assign(
       (name: string): DatatypeImpl => {
         return new DatatypeImpl(ctx, name);
@@ -4310,6 +4357,65 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       }
     }
 
+    ////////////////////////////
+    // Finite Sets
+    ////////////////////////////
+
+    class FiniteSetSortImpl<ElemSort extends Sort<Name> = Sort<Name>>
+      extends SortImpl
+      implements FiniteSetSort<Name, ElemSort>
+    {
+      declare readonly __typename: 'FiniteSetSort';
+
+      elemSort(): ElemSort {
+        return _toSort(check(Z3.get_finite_set_sort_basis(contextPtr, this.ptr))) as ElemSort;
+      }
+
+      cast(other: Expr<Name>): Expr<Name> {
+        _assertContext(other);
+        return other;
+      }
+    }
+
+    class FiniteSetImpl<ElemSort extends Sort<Name> = Sort<Name>>
+      extends ExprImpl<Z3_ast, FiniteSetSortImpl<ElemSort>>
+      implements FiniteSet<Name, ElemSort>
+    {
+      declare readonly __typename: 'FiniteSet';
+
+      union(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort> {
+        return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_union(contextPtr, this.ast, other.ast)));
+      }
+
+      intersect(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort> {
+        return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_intersect(contextPtr, this.ast, other.ast)));
+      }
+
+      diff(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort> {
+        return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_difference(contextPtr, this.ast, other.ast)));
+      }
+
+      contains(elem: Expr<Name>): Bool<Name> {
+        return new BoolImpl(check(Z3.mk_finite_set_member(contextPtr, elem.ast, this.ast)));
+      }
+
+      size(): Expr<Name> {
+        return new ExprImpl(check(Z3.mk_finite_set_size(contextPtr, this.ast)));
+      }
+
+      subsetOf(other: FiniteSet<Name, ElemSort>): Bool<Name> {
+        return new BoolImpl(check(Z3.mk_finite_set_subset(contextPtr, this.ast, other.ast)));
+      }
+
+      map(f: Expr<Name>): FiniteSet<Name, Sort<Name>> {
+        return new FiniteSetImpl(check(Z3.mk_finite_set_map(contextPtr, f.ast, this.ast)));
+      }
+
+      filter(f: Expr<Name>): FiniteSet<Name, ElemSort> {
+        return new FiniteSetImpl<ElemSort>(check(Z3.mk_finite_set_filter(contextPtr, f.ast, this.ast)));
+      }
+    }
+
     ////////////////////////////
     // Datatypes
     ////////////////////////////
@@ -4902,6 +5008,8 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       isSeq,
       isStringSort,
       isString,
+      isFiniteSetSort,
+      isFiniteSet,
       isArraySort,
       isArray,
       isConstArray,
@@ -4932,6 +5040,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       Re,
       Array,
       Set,
+      FiniteSet,
       Datatype,
 
       ////////////////

src/api/js/src/high-level/types.ts

@@ -52,7 +52,8 @@ export type AnyExpr<Name extends string = 'main'> =
   | FPNum<Name>
   | FPRM<Name>
   | Seq<Name>
-  | Re<Name>;
+  | Re<Name>
+  | FiniteSet<Name>;
 /** @hidden */
 export type AnyAst<Name extends string = 'main'> = AnyExpr<Name> | AnySort<Name> | FuncDecl<Name>;
 
@@ -330,6 +331,12 @@ export interface Context<Name extends string = 'main'> {
   /** @category Functions */
   isString(obj: unknown): obj is Seq<Name>;
 
+  /** @category Functions */
+  isFiniteSetSort(obj: unknown): obj is FiniteSetSort<Name>;
+
+  /** @category Functions */
+  isFiniteSet(obj: unknown): obj is FiniteSet<Name>;
+
   /** @category Functions */
   isProbe(obj: unknown): obj is Probe<Name>;
 
@@ -468,6 +475,8 @@ export interface Context<Name extends string = 'main'> {
   /** @category Expressions */
   readonly Set: SMTSetCreation<Name>;
   /** @category Expressions */
+  readonly FiniteSet: FiniteSetCreation<Name>;
+  /** @category Expressions */
   readonly Datatype: DatatypeCreation<Name>;
 
   ////////////////
@@ -1750,7 +1759,8 @@ export interface Sort<Name extends string = 'main'> extends Ast<Name, Z3_sort> {
     | FPSort['__typename']
     | FPRMSort['__typename']
     | SeqSort['__typename']
-    | ReSort['__typename'];
+    | ReSort['__typename']
+    | FiniteSetSort['__typename'];
 
   kind(): Z3_sort_kind;
 
@@ -1879,7 +1889,8 @@ export interface Expr<Name extends string = 'main', S extends Sort<Name> = AnySo
     | Seq['__typename']
     | Re['__typename']
     | SMTArray['__typename']
-    | DatatypeExpr['__typename'];
+    | DatatypeExpr['__typename']
+    | FiniteSet['__typename'];
 
   get sort(): S;
 
@@ -2783,6 +2794,60 @@ export interface SMTSet<Name extends string = 'main', ElemSort extends AnySort<N
   contains(elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>): Bool<Name>;
   subsetOf(b: SMTSet<Name, ElemSort>): Bool<Name>;
 }
+//////////////////////////////////////////
+//
+// Finite Sets
+//
+//////////////////////////////////////////
+
+/**
+ * Represents a finite set sort
+ *
+ * @typeParam ElemSort The sort of elements in the finite set
+ * @category Finite Sets
+ */
+export interface FiniteSetSort<Name extends string = 'main', ElemSort extends Sort<Name> = Sort<Name>>
+  extends Sort<Name> {
+  readonly __typename: 'FiniteSetSort';
+  /** Returns the element sort of this finite set sort */
+  elemSort(): ElemSort;
+}
+
+/** @category Finite Sets */
+export interface FiniteSetCreation<Name extends string> {
+  sort<ElemSort extends Sort<Name>>(elemSort: ElemSort): FiniteSetSort<Name, ElemSort>;
+
+  const<ElemSort extends Sort<Name>>(name: string, elemSort: ElemSort): FiniteSet<Name, ElemSort>;
+
+  consts<ElemSort extends Sort<Name>>(names: string | string[], elemSort: ElemSort): FiniteSet<Name, ElemSort>[];
+
+  empty<ElemSort extends Sort<Name>>(sort: ElemSort): FiniteSet<Name, ElemSort>;
+
+  singleton<ElemSort extends Sort<Name>>(elem: Expr<Name>): FiniteSet<Name, ElemSort>;
+
+  range(low: Expr<Name>, high: Expr<Name>): FiniteSet<Name, Sort<Name>>;
+}
+
+/**
+ * Represents a finite set expression
+ *
+ * @typeParam ElemSort The sort of elements in the finite set
+ * @category Finite Sets
+ */
+export interface FiniteSet<Name extends string = 'main', ElemSort extends Sort<Name> = Sort<Name>>
+  extends Expr<Name, FiniteSetSort<Name, ElemSort>, Z3_ast> {
+  readonly __typename: 'FiniteSet';
+
+  union(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort>;
+  intersect(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort>;
+  diff(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort>;
+  contains(elem: Expr<Name>): Bool<Name>;
+  size(): Expr<Name>;
+  subsetOf(other: FiniteSet<Name, ElemSort>): Bool<Name>;
+  map(f: Expr<Name>): FiniteSet<Name, Sort<Name>>;
+  filter(f: Expr<Name>): FiniteSet<Name, ElemSort>;
+}
+
 //////////////////////////////////////////
 //
 // Datatypes

src/api/ml/z3.ml

@@ -1311,6 +1311,24 @@ struct
   let mk_char_is_digit = Z3native.mk_char_is_digit
 end
 
+module FiniteSet =
+struct
+  let mk_sort = Z3native.mk_finite_set_sort
+  let is_finite_set_sort = Z3native.is_finite_set_sort
+  let get_sort_basis = Z3native.get_finite_set_sort_basis
+  let mk_empty = Z3native.mk_finite_set_empty
+  let mk_singleton = Z3native.mk_finite_set_singleton
+  let mk_union = Z3native.mk_finite_set_union
+  let mk_intersect = Z3native.mk_finite_set_intersect
+  let mk_difference = Z3native.mk_finite_set_difference
+  let mk_member = Z3native.mk_finite_set_member
+  let mk_size = Z3native.mk_finite_set_size
+  let mk_subset = Z3native.mk_finite_set_subset
+  let mk_map = Z3native.mk_finite_set_map
+  let mk_filter = Z3native.mk_finite_set_filter
+  let mk_range = Z3native.mk_finite_set_range
+end
+
 module FloatingPoint =
 struct
   module RoundingMode =

src/api/ml/z3.mli

@@ -2058,6 +2058,53 @@ sig
 
 end
 
+(** Finite Sets *)
+module FiniteSet :
+sig
+  (** Create a finite set sort with the given element sort. *)
+  val mk_sort : context -> Sort.sort -> Sort.sort
+
+  (** Test if a sort is a finite set sort. *)
+  val is_finite_set_sort : context -> Sort.sort -> bool
+
+  (** Get the element sort of a finite set sort. *)
+  val get_sort_basis : context -> Sort.sort -> Sort.sort
+
+  (** Create an empty finite set of the given sort. *)
+  val mk_empty : context -> Sort.sort -> Expr.expr
+
+  (** Create a singleton finite set containing the given element. *)
+  val mk_singleton : context -> Expr.expr -> Expr.expr
+
+  (** Create the union of two finite sets. *)
+  val mk_union : context -> Expr.expr -> Expr.expr -> Expr.expr
+
+  (** Create the intersection of two finite sets. *)
+  val mk_intersect : context -> Expr.expr -> Expr.expr -> Expr.expr
+
+  (** Create the set difference of two finite sets (s1 \ s2). *)
+  val mk_difference : context -> Expr.expr -> Expr.expr -> Expr.expr
+
+  (** Create a membership predicate: elem ∈ set. *)
+  val mk_member : context -> Expr.expr -> Expr.expr -> Expr.expr
+
+  (** Create an expression for the cardinality of a finite set. *)
+  val mk_size : context -> Expr.expr -> Expr.expr
+
+  (** Create a subset predicate: s1 ⊆ s2. *)
+  val mk_subset : context -> Expr.expr -> Expr.expr -> Expr.expr
+
+  (** Apply a function to all elements of a finite set. *)
+  val mk_map : context -> Expr.expr -> Expr.expr -> Expr.expr
+
+  (** Filter a finite set using a predicate function. *)
+  val mk_filter : context -> Expr.expr -> Expr.expr -> Expr.expr
+
+  (** Create a finite set of integers in the range [low, high]. *)
+  val mk_range : context -> Expr.expr -> Expr.expr -> Expr.expr
+
+end
+
 (** Floating-Point Arithmetic *)
 module FloatingPoint :
 sig