Add finite set API functions to access term constructors from finite_set_decl_plugin.h (#7996)

* Initial plan

* Add C API for finite sets

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

* Add Python bindings for finite sets

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

* Add C++ bindings for finite sets

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

* Add documentation for finite set API

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>

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

src/api/CMakeLists.txt

@@ -44,6 +44,7 @@ z3_add_component(api
     api_context.cpp
     api_datalog.cpp
     api_datatype.cpp
+    api_finite_set.cpp
     api_fpa.cpp
     api_goal.cpp
     api_log.cpp

src/api/api_context.cpp

@@ -133,6 +133,7 @@ namespace api {
         m_fpa_util(m()),
         m_sutil(m()),
         m_recfun(m()),
+        m_finite_set_util(m()),
         m_ast_trail(m()),
         m_pmanager(m_limit) {
 

src/api/api_context.h

@@ -31,6 +31,7 @@ Revision History:
 #include "ast/fpa_decl_plugin.h"
 #include "ast/recfun_decl_plugin.h"
 #include "ast/special_relations_decl_plugin.h"
+#include "ast/finite_set_decl_plugin.h"
 #include "ast/rewriter/seq_rewriter.h"
 #include "params/smt_params.h"
 #include "smt/smt_kernel.h"
@@ -77,6 +78,7 @@ namespace api {
         fpa_util                   m_fpa_util;
         seq_util                   m_sutil;
         recfun::util               m_recfun;
+        finite_set_util            m_finite_set_util;
 
         // Support for old solver API
         smt_params                 m_fparams;
@@ -146,6 +148,7 @@ namespace api {
         datatype_util& dtutil() { return m_dt_plugin->u(); }
         seq_util& sutil() { return m_sutil; }
         recfun::util& recfun() { return m_recfun; }
+        finite_set_util& fsutil() { return m_finite_set_util; }
         family_id get_basic_fid() const { return basic_family_id; }
         family_id get_array_fid() const { return m_array_fid; }
         family_id get_arith_fid() const { return arith_family_id; }

src/api/api_finite_set.cpp

@@ -0,0 +1,169 @@
+/*++
+Copyright (c) 2025 Microsoft Corporation
+
+Module Name:
+
+    api_finite_set.cpp
+
+Abstract:
+
+    API for finite sets.
+
+Author:
+
+    Copilot 2025-01-21
+
+Revision History:
+
+--*/
+#include "api/z3.h"
+#include "api/api_log_macros.h"
+#include "api/api_context.h"
+#include "api/api_util.h"
+#include "ast/ast_pp.h"
+
+extern "C" {
+
+    Z3_sort Z3_API Z3_mk_finite_set_sort(Z3_context c, Z3_sort elem_sort) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_sort(c, elem_sort);
+        RESET_ERROR_CODE();
+        parameter param(to_sort(elem_sort));
+        sort* ty = mk_c(c)->m().mk_sort(mk_c(c)->fsutil().get_family_id(), FINITE_SET_SORT, 1, &param);
+        mk_c(c)->save_ast_trail(ty);
+        RETURN_Z3(of_sort(ty));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    bool Z3_API Z3_is_finite_set_sort(Z3_context c, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_is_finite_set_sort(c, s);
+        RESET_ERROR_CODE();
+        return mk_c(c)->fsutil().is_finite_set(to_sort(s));
+        Z3_CATCH_RETURN(false);
+    }
+
+    Z3_sort Z3_API Z3_get_finite_set_sort_basis(Z3_context c, Z3_sort s) {
+        Z3_TRY;
+        LOG_Z3_get_finite_set_sort_basis(c, s);
+        RESET_ERROR_CODE();
+        sort* elem_sort = nullptr;
+        if (!mk_c(c)->fsutil().is_finite_set(to_sort(s), elem_sort)) {
+            SET_ERROR_CODE(Z3_INVALID_ARG, "expected finite set sort");
+            RETURN_Z3(nullptr);
+        }
+        RETURN_Z3(of_sort(elem_sort));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_empty(Z3_context c, Z3_sort set_sort) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_empty(c, set_sort);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_empty(to_sort(set_sort));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_singleton(Z3_context c, Z3_ast elem) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_singleton(c, elem);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_singleton(to_expr(elem));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_union(Z3_context c, Z3_ast s1, Z3_ast s2) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_union(c, s1, s2);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_union(to_expr(s1), to_expr(s2));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_intersect(Z3_context c, Z3_ast s1, Z3_ast s2) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_intersect(c, s1, s2);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_intersect(to_expr(s1), to_expr(s2));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_difference(Z3_context c, Z3_ast s1, Z3_ast s2) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_difference(c, s1, s2);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_difference(to_expr(s1), to_expr(s2));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_member(Z3_context c, Z3_ast elem, Z3_ast set) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_member(c, elem, set);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_in(to_expr(elem), to_expr(set));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_size(Z3_context c, Z3_ast set) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_size(c, set);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_size(to_expr(set));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_subset(Z3_context c, Z3_ast s1, Z3_ast s2) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_subset(c, s1, s2);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_subset(to_expr(s1), to_expr(s2));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_map(Z3_context c, Z3_ast f, Z3_ast set) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_map(c, f, set);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_map(to_expr(f), to_expr(set));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_filter(Z3_context c, Z3_ast f, Z3_ast set) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_filter(c, f, set);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_filter(to_expr(f), to_expr(set));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+    Z3_ast Z3_API Z3_mk_finite_set_range(Z3_context c, Z3_ast low, Z3_ast high) {
+        Z3_TRY;
+        LOG_Z3_mk_finite_set_range(c, low, high);
+        RESET_ERROR_CODE();
+        app* a = mk_c(c)->fsutil().mk_range(to_expr(low), to_expr(high));
+        mk_c(c)->save_ast_trail(a);
+        RETURN_Z3(of_ast(a));
+        Z3_CATCH_RETURN(nullptr);
+    }
+
+};

src/api/c++/z3++.h

@@ -274,6 +274,10 @@ namespace z3 {
            \brief Return a regular expression sort over sequences \c seq_sort.
          */
         sort re_sort(sort& seq_sort);
+        /**
+           \brief Return a finite set sort over element sort \c s.
+         */
+        sort finite_set_sort(sort& s);
         /**
            \brief Return an array sort for arrays from \c d to \c r.
 
@@ -3494,6 +3498,7 @@ namespace z3 {
     inline sort context::char_sort() { Z3_sort s = Z3_mk_char_sort(m_ctx); check_error(); return sort(*this, s); }
     inline sort context::seq_sort(sort& s) { Z3_sort r = Z3_mk_seq_sort(m_ctx, s); check_error(); return sort(*this, r); }
     inline sort context::re_sort(sort& s) { Z3_sort r = Z3_mk_re_sort(m_ctx, s); check_error(); return sort(*this, r); }
+    inline sort context::finite_set_sort(sort& s) { Z3_sort r = Z3_mk_finite_set_sort(m_ctx, s); check_error(); return sort(*this, r); }
     inline sort context::fpa_sort(unsigned ebits, unsigned sbits) { Z3_sort s = Z3_mk_fpa_sort(m_ctx, ebits, sbits); check_error(); return sort(*this, s); }
 
     template<>
@@ -4065,6 +4070,54 @@ namespace z3 {
         MK_EXPR2(Z3_mk_set_subset, a, b);
     }
 
+    // finite set operations
+
+    inline expr finite_set_empty(sort const& s) {
+        Z3_ast r = Z3_mk_finite_set_empty(s.ctx(), s);
+        s.check_error();
+        return expr(s.ctx(), r);
+    }
+
+    inline expr finite_set_singleton(expr const& e) {
+        MK_EXPR1(Z3_mk_finite_set_singleton, e);
+    }
+
+    inline expr finite_set_union(expr const& a, expr const& b) {
+        MK_EXPR2(Z3_mk_finite_set_union, a, b);
+    }
+
+    inline expr finite_set_intersect(expr const& a, expr const& b) {
+        MK_EXPR2(Z3_mk_finite_set_intersect, a, b);
+    }
+
+    inline expr finite_set_difference(expr const& a, expr const& b) {
+        MK_EXPR2(Z3_mk_finite_set_difference, a, b);
+    }
+
+    inline expr finite_set_member(expr const& e, expr const& s) {
+        MK_EXPR2(Z3_mk_finite_set_member, e, s);
+    }
+
+    inline expr finite_set_size(expr const& s) {
+        MK_EXPR1(Z3_mk_finite_set_size, s);
+    }
+
+    inline expr finite_set_subset(expr const& a, expr const& b) {
+        MK_EXPR2(Z3_mk_finite_set_subset, a, b);
+    }
+
+    inline expr finite_set_map(expr const& f, expr const& s) {
+        MK_EXPR2(Z3_mk_finite_set_map, f, s);
+    }
+
+    inline expr finite_set_filter(expr const& f, expr const& s) {
+        MK_EXPR2(Z3_mk_finite_set_filter, f, s);
+    }
+
+    inline expr finite_set_range(expr const& low, expr const& high) {
+        MK_EXPR2(Z3_mk_finite_set_range, low, high);
+    }
+
     // sequence and regular expression operations.
     // union is +
     // concat is overloaded to handle sequences and regular expressions

src/api/python/z3/z3.py

@@ -678,6 +678,8 @@ def is_sort(s : Any) -> bool:
 def _to_sort_ref(s, ctx):
     if z3_debug():
         _z3_assert(isinstance(s, Sort), "Z3 Sort expected")
+    if Z3_is_finite_set_sort(ctx.ref(), s):
+        return FiniteSetSortRef(s, ctx)
     k = _sort_kind(ctx, s)
     if k == Z3_BOOL_SORT:
         return BoolSortRef(s, ctx)
@@ -1184,7 +1186,11 @@ def _to_expr_ref(a, ctx):
     k = Z3_get_ast_kind(ctx_ref, a)
     if k == Z3_QUANTIFIER_AST:
         return QuantifierRef(a, ctx)
-    sk = Z3_get_sort_kind(ctx_ref, Z3_get_sort(ctx_ref, a))
+    # Check for finite set sort before checking sort kind
+    s = Z3_get_sort(ctx_ref, a)
+    if Z3_is_finite_set_sort(ctx_ref, s):
+        return FiniteSetRef(a, ctx)
+    sk = Z3_get_sort_kind(ctx_ref, s)
     if sk == Z3_BOOL_SORT:
         return BoolRef(a, ctx)
     if sk == Z3_INT_SORT:
@@ -5147,6 +5153,217 @@ def IsSubset(a, b):
     return BoolRef(Z3_mk_set_subset(ctx.ref(), a.as_ast(), b.as_ast()), ctx)
 
 
+#########################################
+#
+# Finite Sets
+#
+#########################################
+
+
+class FiniteSetSortRef(SortRef):
+    """Finite set sort."""
+
+    def element_sort(self):
+        """Return the element sort of this finite set sort."""
+        return _to_sort_ref(Z3_get_finite_set_sort_basis(self.ctx_ref(), self.ast), self.ctx)
+
+    def cast(self, val):
+        """Try to cast val as a finite set expression."""
+        if is_expr(val):
+            if self.eq(val.sort()):
+                return val
+            else:
+                _z3_assert(False, "Cannot cast to finite set sort")
+        if isinstance(val, set):
+            elem_sort = self.element_sort()
+            result = FiniteSetEmpty(self)
+            for e in val:
+                result = FiniteSetUnion(result, FiniteSetSingleton(_py2expr(e, self.ctx, elem_sort)))
+            return result
+        _z3_assert(False, "Cannot cast to finite set sort")
+
+    def subsort(self, other):
+        return False
+
+    def is_int(self):
+        return False
+
+    def is_bool(self):
+        return False
+
+    def is_datatype(self):
+        return False
+
+    def is_array(self):
+        return False
+
+    def is_bv(self):
+        return False
+
+
+def is_finite_set(a):
+    """Return True if a is a Z3 finite set expression.
+    >>> s = FiniteSetSort(IntSort())
+    >>> is_finite_set(FiniteSetEmpty(s))
+    True
+    >>> is_finite_set(IntVal(1))
+    False
+    """
+    return isinstance(a, FiniteSetRef)
+
+
+def is_finite_set_sort(s):
+    """Return True if s is a Z3 finite set sort.
+    >>> is_finite_set_sort(FiniteSetSort(IntSort()))
+    True
+    >>> is_finite_set_sort(IntSort())
+    False
+    """
+    return isinstance(s, FiniteSetSortRef)
+
+
+class FiniteSetRef(ExprRef):
+    """Finite set expression."""
+
+    def sort(self):
+        return FiniteSetSortRef(Z3_get_sort(self.ctx_ref(), self.as_ast()), self.ctx)
+
+    def __or__(self, other):
+        """Return the union of self and other."""
+        return FiniteSetUnion(self, other)
+
+    def __and__(self, other):
+        """Return the intersection of self and other."""
+        return FiniteSetIntersect(self, other)
+
+    def __sub__(self, other):
+        """Return the set difference of self and other."""
+        return FiniteSetDifference(self, other)
+
+
+def FiniteSetSort(elem_sort):
+    """Create a finite set sort over element sort elem_sort.
+    >>> s = FiniteSetSort(IntSort())
+    >>> s
+    FiniteSet(Int)
+    """
+    return FiniteSetSortRef(Z3_mk_finite_set_sort(elem_sort.ctx_ref(), elem_sort.ast), elem_sort.ctx)
+
+
+def FiniteSetEmpty(set_sort):
+    """Create an empty finite set of the given sort.
+    >>> s = FiniteSetSort(IntSort())
+    >>> FiniteSetEmpty(s)
+    set.empty
+    """
+    ctx = set_sort.ctx
+    return FiniteSetRef(Z3_mk_finite_set_empty(ctx.ref(), set_sort.ast), ctx)
+
+
+def FiniteSetSingleton(elem):
+    """Create a singleton finite set containing elem.
+    >>> FiniteSetSingleton(IntVal(1))
+    set.singleton(1)
+    """
+    ctx = elem.ctx
+    return FiniteSetRef(Z3_mk_finite_set_singleton(ctx.ref(), elem.as_ast()), ctx)
+
+
+def FiniteSetUnion(s1, s2):
+    """Create the union of two finite sets.
+    >>> a = Const('a', FiniteSetSort(IntSort()))
+    >>> b = Const('b', FiniteSetSort(IntSort()))
+    >>> FiniteSetUnion(a, b)
+    set.union(a, b)
+    """
+    ctx = _ctx_from_ast_arg_list([s1, s2])
+    return FiniteSetRef(Z3_mk_finite_set_union(ctx.ref(), s1.as_ast(), s2.as_ast()), ctx)
+
+
+def FiniteSetIntersect(s1, s2):
+    """Create the intersection of two finite sets.
+    >>> a = Const('a', FiniteSetSort(IntSort()))
+    >>> b = Const('b', FiniteSetSort(IntSort()))
+    >>> FiniteSetIntersect(a, b)
+    set.intersect(a, b)
+    """
+    ctx = _ctx_from_ast_arg_list([s1, s2])
+    return FiniteSetRef(Z3_mk_finite_set_intersect(ctx.ref(), s1.as_ast(), s2.as_ast()), ctx)
+
+
+def FiniteSetDifference(s1, s2):
+    """Create the set difference of two finite sets.
+    >>> a = Const('a', FiniteSetSort(IntSort()))
+    >>> b = Const('b', FiniteSetSort(IntSort()))
+    >>> FiniteSetDifference(a, b)
+    set.difference(a, b)
+    """
+    ctx = _ctx_from_ast_arg_list([s1, s2])
+    return FiniteSetRef(Z3_mk_finite_set_difference(ctx.ref(), s1.as_ast(), s2.as_ast()), ctx)
+
+
+def FiniteSetMember(elem, set):
+    """Check if elem is a member of the finite set.
+    >>> a = Const('a', FiniteSetSort(IntSort()))
+    >>> FiniteSetMember(IntVal(1), a)
+    set.in(1, a)
+    """
+    ctx = _ctx_from_ast_arg_list([elem, set])
+    return BoolRef(Z3_mk_finite_set_member(ctx.ref(), elem.as_ast(), set.as_ast()), ctx)
+
+
+def FiniteSetSize(set):
+    """Get the size (cardinality) of a finite set.
+    >>> a = Const('a', FiniteSetSort(IntSort()))
+    >>> FiniteSetSize(a)
+    set.size(a)
+    """
+    ctx = set.ctx
+    return ArithRef(Z3_mk_finite_set_size(ctx.ref(), set.as_ast()), ctx)
+
+
+def FiniteSetSubset(s1, s2):
+    """Check if s1 is a subset of s2.
+    >>> a = Const('a', FiniteSetSort(IntSort()))
+    >>> b = Const('b', FiniteSetSort(IntSort()))
+    >>> FiniteSetSubset(a, b)
+    set.subset(a, b)
+    """
+    ctx = _ctx_from_ast_arg_list([s1, s2])
+    return BoolRef(Z3_mk_finite_set_subset(ctx.ref(), s1.as_ast(), s2.as_ast()), ctx)
+
+
+def FiniteSetMap(f, set):
+    """Apply function f to all elements of the finite set.
+    >>> f = Function('f', IntSort(), IntSort())
+    >>> a = Const('a', FiniteSetSort(IntSort()))
+    >>> FiniteSetMap(f, a)
+    set.map(f, a)
+    """
+    ctx = _ctx_from_ast_arg_list([f, set])
+    return FiniteSetRef(Z3_mk_finite_set_map(ctx.ref(), f.as_ast(), set.as_ast()), ctx)
+
+
+def FiniteSetFilter(f, set):
+    """Filter a finite set using predicate f.
+    >>> f = Function('f', IntSort(), BoolSort())
+    >>> a = Const('a', FiniteSetSort(IntSort()))
+    >>> FiniteSetFilter(f, a)
+    set.filter(f, a)
+    """
+    ctx = _ctx_from_ast_arg_list([f, set])
+    return FiniteSetRef(Z3_mk_finite_set_filter(ctx.ref(), f.as_ast(), set.as_ast()), ctx)
+
+
+def FiniteSetRange(low, high):
+    """Create a finite set of integers in the range [low, high).
+    >>> FiniteSetRange(IntVal(0), IntVal(5))
+    set.range(0, 5)
+    """
+    ctx = _ctx_from_ast_arg_list([low, high])
+    return FiniteSetRef(Z3_mk_finite_set_range(ctx.ref(), low.as_ast(), high.as_ast()), ctx)
+
+
 #########################################
 #
 # Datatypes

src/api/z3_api.h

@@ -3389,6 +3389,107 @@ extern "C" {
     Z3_ast Z3_API Z3_mk_array_ext(Z3_context c, Z3_ast arg1, Z3_ast arg2);
     /**@}*/
 
+    /** @name Finite Sets */
+    /**@{*/
+    /**
+       \brief Create a finite set sort.
+
+       def_API('Z3_mk_finite_set_sort', SORT, (_in(CONTEXT), _in(SORT)))
+    */
+    Z3_sort Z3_API Z3_mk_finite_set_sort(Z3_context c, Z3_sort elem_sort);
+
+    /**
+       \brief Check if a sort is a finite set sort.
+
+       def_API('Z3_is_finite_set_sort', BOOL, (_in(CONTEXT), _in(SORT)))
+    */
+    bool Z3_API Z3_is_finite_set_sort(Z3_context c, Z3_sort s);
+
+    /**
+       \brief Get the element sort of a finite set sort.
+
+       def_API('Z3_get_finite_set_sort_basis', SORT, (_in(CONTEXT), _in(SORT)))
+    */
+    Z3_sort Z3_API Z3_get_finite_set_sort_basis(Z3_context c, Z3_sort s);
+
+    /**
+       \brief Create an empty finite set of the given sort.
+
+       def_API('Z3_mk_finite_set_empty', AST, (_in(CONTEXT), _in(SORT)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_empty(Z3_context c, Z3_sort set_sort);
+
+    /**
+       \brief Create a singleton finite set.
+
+       def_API('Z3_mk_finite_set_singleton', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_singleton(Z3_context c, Z3_ast elem);
+
+    /**
+       \brief Create the union of two finite sets.
+
+       def_API('Z3_mk_finite_set_union', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_union(Z3_context c, Z3_ast s1, Z3_ast s2);
+
+    /**
+       \brief Create the intersection of two finite sets.
+
+       def_API('Z3_mk_finite_set_intersect', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_intersect(Z3_context c, Z3_ast s1, Z3_ast s2);
+
+    /**
+       \brief Create the set difference of two finite sets.
+
+       def_API('Z3_mk_finite_set_difference', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_difference(Z3_context c, Z3_ast s1, Z3_ast s2);
+
+    /**
+       \brief Check if an element is a member of a finite set.
+
+       def_API('Z3_mk_finite_set_member', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_member(Z3_context c, Z3_ast elem, Z3_ast set);
+
+    /**
+       \brief Get the size (cardinality) of a finite set.
+
+       def_API('Z3_mk_finite_set_size', AST, (_in(CONTEXT), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_size(Z3_context c, Z3_ast set);
+
+    /**
+       \brief Check if one finite set is a subset of another.
+
+       def_API('Z3_mk_finite_set_subset', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_subset(Z3_context c, Z3_ast s1, Z3_ast s2);
+
+    /**
+       \brief Apply a function to all elements of a finite set.
+
+       def_API('Z3_mk_finite_set_map', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_map(Z3_context c, Z3_ast f, Z3_ast set);
+
+    /**
+       \brief Filter a finite set using a predicate.
+
+       def_API('Z3_mk_finite_set_filter', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_filter(Z3_context c, Z3_ast f, Z3_ast set);
+
+    /**
+       \brief Create a finite set of integers in the range [low, high).
+
+       def_API('Z3_mk_finite_set_range', AST, (_in(CONTEXT), _in(AST), _in(AST)))
+    */
+    Z3_ast Z3_API Z3_mk_finite_set_range(Z3_context c, Z3_ast low, Z3_ast high);
+    /**@}*/
+
     /** @name Numerals */
     /**@{*/
     /**