diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index a537bb3b9..c1e78f473 100644 --- a/src/api/CMakeLists.txt +++ b/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 diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index 82d65a5dd..6dc42f5e3 100644 --- a/src/api/api_context.cpp +++ b/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) { diff --git a/src/api/api_context.h b/src/api/api_context.h index e570daca3..780372588 100644 --- a/src/api/api_context.h +++ b/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; } diff --git a/src/api/api_finite_set.cpp b/src/api/api_finite_set.cpp new file mode 100644 index 000000000..9dbecfdae --- /dev/null +++ b/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, ¶m); + 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); + } + +}; diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 9de58e057..8d0ab3f20 100644 --- a/src/api/z3_api.h +++ b/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 */ /**@{*/ /**