Add C API for finite sets

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

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/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 */
     /**@{*/
     /**