diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 7a4a03a27..86f82b29a 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -28,6 +28,7 @@ z3_add_component(ast expr_map.cpp expr_stat.cpp expr_substitution.cpp + finite_sets_decl_plugin.cpp for_each_ast.cpp for_each_expr.cpp format.cpp diff --git a/src/ast/finite_sets_decl_plugin.cpp b/src/ast/finite_sets_decl_plugin.cpp index e69de29bb..0c23f4af9 100644 --- a/src/ast/finite_sets_decl_plugin.cpp +++ b/src/ast/finite_sets_decl_plugin.cpp @@ -0,0 +1,366 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + finite_sets_decl_plugin.cpp + +Abstract: + + Declaration plugin for finite sets + +Author: + + GitHub Copilot Agent 2025 + +Revision History: + +--*/ +#include +#include "ast/finite_sets_decl_plugin.h" +#include "ast/arith_decl_plugin.h" +#include "util/warning.h" + +finite_sets_decl_plugin::finite_sets_decl_plugin(): + m_empty_sym("set.empty"), + m_union_sym("set.union"), + m_intersect_sym("set.intersect"), + m_difference_sym("set.difference"), + m_in_sym("set.in"), + m_size_sym("set.size"), + m_subset_sym("set.subset"), + m_map_sym("set.map"), + m_filter_sym("set.filter"), + m_range_sym("set.range") { +} + +sort * finite_sets_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { + if (k == FINITE_SET_SORT) { + if (num_parameters != 1) { + m_manager->raise_exception("FiniteSet sort expects exactly one parameter (element sort)"); + return nullptr; + } + if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) { + m_manager->raise_exception("FiniteSet sort parameter must be a sort"); + return nullptr; + } + sort * element_sort = to_sort(parameters[0].get_ast()); + sort_size sz = sort_size::mk_very_big(); + sort_info info(m_family_id, FINITE_SET_SORT, sz, num_parameters, parameters); + return m_manager->mk_sort(symbol("FiniteSet"), info); + } + m_manager->raise_exception("unknown finite set sort"); + return nullptr; +} + +sort * finite_sets_decl_plugin::get_element_sort(sort* finite_set_sort) const { + if (finite_set_sort->get_family_id() != m_family_id || + finite_set_sort->get_decl_kind() != FINITE_SET_SORT) { + return nullptr; + } + parameter const* params = finite_set_sort->get_parameters(); + if (!params[0].is_ast() || !is_sort(params[0].get_ast())) { + return nullptr; + } + return to_sort(params[0].get_ast()); +} + +bool finite_sets_decl_plugin::check_finite_set_arguments(unsigned arity, sort * const * domain) { + if (arity == 0) { + return true; + } + + sort* first_sort = domain[0]; + if (first_sort->get_family_id() != m_family_id || + first_sort->get_decl_kind() != FINITE_SET_SORT) { + m_manager->raise_exception("argument is not of FiniteSet sort"); + return false; + } + + for (unsigned i = 1; i < arity; ++i) { + if (domain[i] != first_sort) { + std::ostringstream buffer; + buffer << "arguments " << 1 << " and " << (i+1) << " have different sorts"; + m_manager->raise_exception(buffer.str()); + return false; + } + } + return true; +} + +func_decl * finite_sets_decl_plugin::mk_empty(sort* element_sort) { + parameter param(element_sort); + sort * finite_set_sort = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, ¶m); + sort * const * no_domain = nullptr; + return m_manager->mk_func_decl(m_empty_sym, 0u, no_domain, finite_set_sort, + func_decl_info(m_family_id, OP_FINITE_SET_EMPTY, 1, ¶m)); +} + +func_decl * finite_sets_decl_plugin::mk_union(unsigned arity, sort * const * domain) { + if (arity != 2) { + m_manager->raise_exception("set.union takes exactly two arguments"); + return nullptr; + } + if (!check_finite_set_arguments(arity, domain)) { + return nullptr; + } + return m_manager->mk_func_decl(m_union_sym, arity, domain, domain[0], + func_decl_info(m_family_id, OP_FINITE_SET_UNION)); +} + +func_decl * finite_sets_decl_plugin::mk_intersect(unsigned arity, sort * const * domain) { + if (arity != 2) { + m_manager->raise_exception("set.intersect takes exactly two arguments"); + return nullptr; + } + if (!check_finite_set_arguments(arity, domain)) { + return nullptr; + } + return m_manager->mk_func_decl(m_intersect_sym, arity, domain, domain[0], + func_decl_info(m_family_id, OP_FINITE_SET_INTERSECT)); +} + +func_decl * finite_sets_decl_plugin::mk_difference(unsigned arity, sort * const * domain) { + if (arity != 2) { + m_manager->raise_exception("set.difference takes exactly two arguments"); + return nullptr; + } + if (!check_finite_set_arguments(arity, domain)) { + return nullptr; + } + return m_manager->mk_func_decl(m_difference_sym, arity, domain, domain[0], + func_decl_info(m_family_id, OP_FINITE_SET_DIFFERENCE)); +} + +func_decl * finite_sets_decl_plugin::mk_in(unsigned arity, sort * const * domain) { + if (arity != 2) { + m_manager->raise_exception("set.in takes exactly two arguments"); + return nullptr; + } + if (domain[1]->get_family_id() != m_family_id || + domain[1]->get_decl_kind() != FINITE_SET_SORT) { + m_manager->raise_exception("second argument of set.in must be a FiniteSet"); + return nullptr; + } + + sort* element_sort = get_element_sort(domain[1]); + if (!element_sort) { + m_manager->raise_exception("invalid FiniteSet sort"); + return nullptr; + } + + if (domain[0] != element_sort) { + m_manager->raise_exception("element type does not match set element type"); + return nullptr; + } + + sort* bool_sort = m_manager->mk_bool_sort(); + return m_manager->mk_func_decl(m_in_sym, arity, domain, bool_sort, + func_decl_info(m_family_id, OP_FINITE_SET_IN)); +} + +func_decl * finite_sets_decl_plugin::mk_size(unsigned arity, sort * const * domain) { + if (arity != 1) { + m_manager->raise_exception("set.size takes exactly one argument"); + return nullptr; + } + if (!check_finite_set_arguments(arity, domain)) { + return nullptr; + } + + arith_util arith(*m_manager); + sort * int_sort = arith.mk_int(); + return m_manager->mk_func_decl(m_size_sym, arity, domain, int_sort, + func_decl_info(m_family_id, OP_FINITE_SET_SIZE)); +} + +func_decl * finite_sets_decl_plugin::mk_subset(unsigned arity, sort * const * domain) { + if (arity != 2) { + m_manager->raise_exception("set.subset takes exactly two arguments"); + return nullptr; + } + if (!check_finite_set_arguments(arity, domain)) { + return nullptr; + } + + sort* bool_sort = m_manager->mk_bool_sort(); + return m_manager->mk_func_decl(m_subset_sym, arity, domain, bool_sort, + func_decl_info(m_family_id, OP_FINITE_SET_SUBSET)); +} + +func_decl * finite_sets_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const* domain) { + if (arity != 1) { + m_manager->raise_exception("set.map takes exactly one set argument"); + return nullptr; + } + if (!check_finite_set_arguments(arity, domain)) { + return nullptr; + } + + // Get the element sort of the input set + sort* input_element_sort = get_element_sort(domain[0]); + if (!input_element_sort) { + m_manager->raise_exception("invalid FiniteSet sort"); + return nullptr; + } + + // Check that the function has correct signature + if (f->get_arity() != 1) { + m_manager->raise_exception("set.map function must take exactly one argument"); + return nullptr; + } + if (f->get_domain(0) != input_element_sort) { + m_manager->raise_exception("set.map function domain must match set element type"); + return nullptr; + } + + // Create output set sort with the function's range as element type + sort* output_element_sort = f->get_range(); + parameter param(output_element_sort); + sort* output_set_sort = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, ¶m); + + parameter func_param(f); + return m_manager->mk_func_decl(m_map_sym, arity, domain, output_set_sort, + func_decl_info(m_family_id, OP_FINITE_SET_MAP, 1, &func_param)); +} + +func_decl * finite_sets_decl_plugin::mk_filter(func_decl* f, unsigned arity, sort* const* domain) { + if (arity != 1) { + m_manager->raise_exception("set.filter takes exactly one set argument"); + return nullptr; + } + if (!check_finite_set_arguments(arity, domain)) { + return nullptr; + } + + // Get the element sort of the set + sort* element_sort = get_element_sort(domain[0]); + if (!element_sort) { + m_manager->raise_exception("invalid FiniteSet sort"); + return nullptr; + } + + // Check that the function has correct signature (S -> Bool) + if (f->get_arity() != 1) { + m_manager->raise_exception("set.filter function must take exactly one argument"); + return nullptr; + } + if (f->get_domain(0) != element_sort) { + m_manager->raise_exception("set.filter function domain must match set element type"); + return nullptr; + } + if (!m_manager->is_bool(f->get_range())) { + m_manager->raise_exception("set.filter function must return Bool"); + return nullptr; + } + + parameter func_param(f); + return m_manager->mk_func_decl(m_filter_sym, arity, domain, domain[0], + func_decl_info(m_family_id, OP_FINITE_SET_FILTER, 1, &func_param)); +} + +func_decl * finite_sets_decl_plugin::mk_range(unsigned arity, sort * const * domain) { + if (arity != 2) { + m_manager->raise_exception("set.range takes exactly two arguments"); + return nullptr; + } + + arith_util arith(*m_manager); + sort * int_sort = arith.mk_int(); + + if (domain[0] != int_sort || domain[1] != int_sort) { + m_manager->raise_exception("set.range arguments must be Int"); + return nullptr; + } + + parameter param(int_sort); + sort* output_set_sort = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, ¶m); + + return m_manager->mk_func_decl(m_range_sym, arity, domain, output_set_sort, + func_decl_info(m_family_id, OP_FINITE_SET_RANGE)); +} + +func_decl * finite_sets_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, + parameter const * parameters, + unsigned arity, sort * const * domain, + sort * range) { + switch (k) { + case OP_FINITE_SET_EMPTY: + if (num_parameters != 1 || !parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) { + m_manager->raise_exception("set.empty requires one sort parameter"); + return nullptr; + } + return mk_empty(to_sort(parameters[0].get_ast())); + case OP_FINITE_SET_UNION: + return mk_union(arity, domain); + case OP_FINITE_SET_INTERSECT: + return mk_intersect(arity, domain); + case OP_FINITE_SET_DIFFERENCE: + return mk_difference(arity, domain); + case OP_FINITE_SET_IN: + return mk_in(arity, domain); + case OP_FINITE_SET_SIZE: + return mk_size(arity, domain); + case OP_FINITE_SET_SUBSET: + return mk_subset(arity, domain); + case OP_FINITE_SET_MAP: + if (num_parameters != 1 || !parameters[0].is_ast() || !is_func_decl(parameters[0].get_ast())) { + m_manager->raise_exception("set.map requires one function parameter"); + return nullptr; + } + return mk_map(to_func_decl(parameters[0].get_ast()), arity, domain); + case OP_FINITE_SET_FILTER: + if (num_parameters != 1 || !parameters[0].is_ast() || !is_func_decl(parameters[0].get_ast())) { + m_manager->raise_exception("set.filter requires one function parameter"); + return nullptr; + } + return mk_filter(to_func_decl(parameters[0].get_ast()), arity, domain); + case OP_FINITE_SET_RANGE: + return mk_range(arity, domain); + default: + return nullptr; + } +} + +void finite_sets_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { + op_names.push_back(builtin_name("set.empty", OP_FINITE_SET_EMPTY)); + op_names.push_back(builtin_name("set.union", OP_FINITE_SET_UNION)); + op_names.push_back(builtin_name("set.intersect", OP_FINITE_SET_INTERSECT)); + op_names.push_back(builtin_name("set.difference", OP_FINITE_SET_DIFFERENCE)); + op_names.push_back(builtin_name("set.in", OP_FINITE_SET_IN)); + op_names.push_back(builtin_name("set.size", OP_FINITE_SET_SIZE)); + op_names.push_back(builtin_name("set.subset", OP_FINITE_SET_SUBSET)); + op_names.push_back(builtin_name("set.map", OP_FINITE_SET_MAP)); + op_names.push_back(builtin_name("set.filter", OP_FINITE_SET_FILTER)); + op_names.push_back(builtin_name("set.range", OP_FINITE_SET_RANGE)); +} + +void finite_sets_decl_plugin::get_sort_names(svector& sort_names, symbol const & logic) { + sort_names.push_back(builtin_name("FiniteSet", FINITE_SET_SORT)); +} + +expr * finite_sets_decl_plugin::get_some_value(sort * s) { + if (s->get_family_id() == m_family_id && s->get_decl_kind() == FINITE_SET_SORT) { + // Return empty set for the given sort + sort* element_sort = get_element_sort(s); + if (element_sort) { + parameter param(element_sort); + return m_manager->mk_app(m_family_id, OP_FINITE_SET_EMPTY, 1, ¶m, 0, nullptr); + } + } + return nullptr; +} + +bool finite_sets_decl_plugin::is_fully_interp(sort * s) const { + return s->get_family_id() == m_family_id && s->get_decl_kind() == FINITE_SET_SORT; +} + +bool finite_sets_decl_plugin::is_value(app * e) const { + // Empty set is a value + return is_app_of(e, m_family_id, OP_FINITE_SET_EMPTY); +} + +bool finite_sets_decl_plugin::is_unique_value(app* e) const { + // Empty set is a unique value for its sort + return is_value(e); +} diff --git a/src/ast/finite_sets_decl_plugin.h b/src/ast/finite_sets_decl_plugin.h index c5b484604..c238df34a 100644 --- a/src/ast/finite_sets_decl_plugin.h +++ b/src/ast/finite_sets_decl_plugin.h @@ -24,3 +24,157 @@ Operators: set.range : Int Int -> (FiniteSet Int) --*/ +#pragma once + +#include "ast/ast.h" + +enum finite_sets_sort_kind { + FINITE_SET_SORT +}; + +enum finite_sets_op_kind { + OP_FINITE_SET_EMPTY, + OP_FINITE_SET_UNION, + OP_FINITE_SET_INTERSECT, + OP_FINITE_SET_DIFFERENCE, + OP_FINITE_SET_IN, + OP_FINITE_SET_SIZE, + OP_FINITE_SET_SUBSET, + OP_FINITE_SET_MAP, + OP_FINITE_SET_FILTER, + OP_FINITE_SET_RANGE, + LAST_FINITE_SET_OP +}; + +class finite_sets_decl_plugin : public decl_plugin { + symbol m_empty_sym; + symbol m_union_sym; + symbol m_intersect_sym; + symbol m_difference_sym; + symbol m_in_sym; + symbol m_size_sym; + symbol m_subset_sym; + symbol m_map_sym; + symbol m_filter_sym; + symbol m_range_sym; + + func_decl * mk_empty(sort* element_sort); + func_decl * mk_union(unsigned arity, sort * const * domain); + func_decl * mk_intersect(unsigned arity, sort * const * domain); + func_decl * mk_difference(unsigned arity, sort * const * domain); + func_decl * mk_in(unsigned arity, sort * const * domain); + func_decl * mk_size(unsigned arity, sort * const * domain); + func_decl * mk_subset(unsigned arity, sort * const * domain); + func_decl * mk_map(func_decl* f, unsigned arity, sort* const* domain); + func_decl * mk_filter(func_decl* f, unsigned arity, sort* const* domain); + func_decl * mk_range(unsigned arity, sort * const * domain); + + bool check_finite_set_arguments(unsigned arity, sort * const * domain); + sort * get_element_sort(sort* finite_set_sort) const; + +public: + finite_sets_decl_plugin(); + + decl_plugin * mk_fresh() override { + return alloc(finite_sets_decl_plugin); + } + + // + // Contract for sort: + // parameters[0] - element sort + // + sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override; + + // + // Contract for func_decl: + // For OP_FINITE_SET_MAP and OP_FINITE_SET_FILTER: + // parameters[0] - function declaration + // For others: + // no parameters + func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) override; + + void get_op_names(svector & op_names, symbol const & logic) override; + + void get_sort_names(svector & sort_names, symbol const & logic) override; + + expr * get_some_value(sort * s) override; + + bool is_fully_interp(sort * s) const override; + + bool is_value(app * e) const override; + + bool is_unique_value(app* e) const override; +}; + +class finite_sets_recognizers { +protected: + family_id m_fid; +public: + finite_sets_recognizers(family_id fid):m_fid(fid) {} + family_id get_family_id() const { return m_fid; } + bool is_finite_set(sort* s) const { return is_sort_of(s, m_fid, FINITE_SET_SORT); } + bool is_finite_set(expr* n) const { return is_finite_set(n->get_sort()); } + bool is_empty(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_EMPTY); } + bool is_union(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_UNION); } + bool is_intersect(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_INTERSECT); } + bool is_difference(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_DIFFERENCE); } + bool is_in(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_IN); } + bool is_size(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_SIZE); } + bool is_subset(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_SUBSET); } + bool is_map(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_MAP); } + bool is_filter(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_FILTER); } + bool is_range(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_RANGE); } +}; + +class finite_sets_util : public finite_sets_recognizers { + ast_manager& m_manager; +public: + finite_sets_util(ast_manager& m): + finite_sets_recognizers(m.mk_family_id("finite_sets")), m_manager(m) {} + + ast_manager& get_manager() const { return m_manager; } + + app * mk_empty(sort* element_sort) { + parameter param(element_sort); + return m_manager.mk_app(m_fid, OP_FINITE_SET_EMPTY, 1, ¶m, 0, nullptr); + } + + app * mk_union(expr* s1, expr* s2) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_UNION, s1, s2); + } + + app * mk_intersect(expr* s1, expr* s2) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_INTERSECT, s1, s2); + } + + app * mk_difference(expr* s1, expr* s2) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_DIFFERENCE, s1, s2); + } + + app * mk_in(expr* elem, expr* set) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_IN, elem, set); + } + + app * mk_size(expr* set) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_SIZE, set); + } + + app * mk_subset(expr* s1, expr* s2) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_SUBSET, s1, s2); + } + + app * mk_map(func_decl* f, expr* set) { + parameter param(f); + return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP, 1, ¶m, 1, &set); + } + + app * mk_filter(func_decl* f, expr* set) { + parameter param(f); + return m_manager.mk_app(m_fid, OP_FINITE_SET_FILTER, 1, ¶m, 1, &set); + } + + app * mk_range(expr* low, expr* high) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_RANGE, low, high); + } +}; diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index 8cb0bbe5a..961d95e81 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -29,6 +29,7 @@ Revision History: #include "ast/pb_decl_plugin.h" #include "ast/fpa_decl_plugin.h" #include "ast/special_relations_decl_plugin.h" +#include "ast/finite_sets_decl_plugin.h" void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("arith")))) { @@ -64,4 +65,7 @@ void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("specrels")))) { m.register_plugin(symbol("specrels"), alloc(special_relations_decl_plugin)); } + if (!m.get_plugin(m.mk_family_id(symbol("finite_sets")))) { + m.register_plugin(symbol("finite_sets"), alloc(finite_sets_decl_plugin)); + } }