From 495cdba9af133ab195693a05e3cc3a02eef5d318 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 5 Oct 2025 17:19:36 +0000 Subject: [PATCH] Rename finite_sets to finite_set everywhere including file names Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/CMakeLists.txt | 2 +- ..._plugin.cpp => finite_set_decl_plugin.cpp} | 38 +++++++++---------- ...decl_plugin.h => finite_set_decl_plugin.h} | 24 ++++++------ src/ast/reg_decl_plugins.cpp | 6 +-- src/test/CMakeLists.txt | 2 +- src/test/{finite_sets.cpp => finite_set.cpp} | 18 ++++----- src/test/main.cpp | 2 +- 7 files changed, 46 insertions(+), 46 deletions(-) rename src/ast/{finite_sets_decl_plugin.cpp => finite_set_decl_plugin.cpp} (85%) rename src/ast/{finite_sets_decl_plugin.h => finite_set_decl_plugin.h} (91%) rename src/test/{finite_sets.cpp => finite_set.cpp} (93%) diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 86f82b29a..6a50c3b05 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -28,7 +28,7 @@ z3_add_component(ast expr_map.cpp expr_stat.cpp expr_substitution.cpp - finite_sets_decl_plugin.cpp + finite_set_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_set_decl_plugin.cpp similarity index 85% rename from src/ast/finite_sets_decl_plugin.cpp rename to src/ast/finite_set_decl_plugin.cpp index ab0bac6fe..4753f1662 100644 --- a/src/ast/finite_sets_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -3,7 +3,7 @@ Copyright (c) 2025 Microsoft Corporation Module Name: - finite_sets_decl_plugin.cpp + finite_set_decl_plugin.cpp Abstract: @@ -17,27 +17,27 @@ Revision History: --*/ #include -#include "ast/finite_sets_decl_plugin.h" +#include "ast/finite_set_decl_plugin.h" #include "ast/arith_decl_plugin.h" #include "ast/array_decl_plugin.h" #include "util/warning.h" -finite_sets_decl_plugin::finite_sets_decl_plugin(): +finite_set_decl_plugin::finite_set_decl_plugin(): m_init(false) { } -finite_sets_decl_plugin::~finite_sets_decl_plugin() { +finite_set_decl_plugin::~finite_set_decl_plugin() { for (psig* s : m_sigs) dealloc(s); } -bool finite_sets_decl_plugin::is_sort_param(sort* s, unsigned& idx) { +bool finite_set_decl_plugin::is_sort_param(sort* s, unsigned& idx) { return s->get_name().is_numerical() && (idx = s->get_name().get_num(), true); } -bool finite_sets_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { +bool finite_set_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { if (s == sP) return true; unsigned idx; if (is_sort_param(sP, idx)) { @@ -64,7 +64,7 @@ bool finite_sets_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP } } -void finite_sets_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { +void finite_set_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { m_binding.reset(); ast_manager& m = *m_manager; @@ -108,7 +108,7 @@ void finite_sets_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, s } } -void finite_sets_decl_plugin::init() { +void finite_set_decl_plugin::init() { if (m_init) return; ast_manager& m = *m_manager; array_util autil(m); @@ -147,7 +147,7 @@ void finite_sets_decl_plugin::init() { m_sigs[OP_FINITE_SET_RANGE] = alloc(psig, m, "set.range", 0, 2, intintT, setInt); } -sort * finite_sets_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { +sort * finite_set_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)"); @@ -166,7 +166,7 @@ sort * finite_sets_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, pa return nullptr; } -sort * finite_sets_decl_plugin::get_element_sort(sort* finite_set_sort) const { +sort * finite_set_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; @@ -178,7 +178,7 @@ sort * finite_sets_decl_plugin::get_element_sort(sort* finite_set_sort) const { return to_sort(params[0].get_ast()); } -func_decl * finite_sets_decl_plugin::mk_empty(sort* element_sort) { +func_decl * finite_set_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; @@ -186,14 +186,14 @@ func_decl * finite_sets_decl_plugin::mk_empty(sort* element_sort) { func_decl_info(m_family_id, OP_FINITE_SET_EMPTY, 1, ¶m)); } -func_decl * finite_sets_decl_plugin::mk_finite_set_op(decl_kind k, unsigned arity, sort * const * domain, sort* range) { +func_decl * finite_set_decl_plugin::mk_finite_set_op(decl_kind k, unsigned arity, sort * const * domain, sort* range) { ast_manager& m = *m_manager; sort_ref rng(m); match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k)); } -func_decl * finite_sets_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, +func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { @@ -222,7 +222,7 @@ func_decl * finite_sets_decl_plugin::mk_func_decl(decl_kind k, unsigned num_para } } -void finite_sets_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { +void finite_set_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { init(); for (unsigned i = 0; i < m_sigs.size(); ++i) { if (m_sigs[i]) @@ -230,11 +230,11 @@ void finite_sets_decl_plugin::get_op_names(svector& op_names, symb } } -void finite_sets_decl_plugin::get_sort_names(svector& sort_names, symbol const & logic) { +void finite_set_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) { +expr * finite_set_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); @@ -246,16 +246,16 @@ expr * finite_sets_decl_plugin::get_some_value(sort * s) { return nullptr; } -bool finite_sets_decl_plugin::is_fully_interp(sort * s) const { +bool finite_set_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 { +bool finite_set_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 { +bool finite_set_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_set_decl_plugin.h similarity index 91% rename from src/ast/finite_sets_decl_plugin.h rename to src/ast/finite_set_decl_plugin.h index 1205a6ddb..e411099dc 100644 --- a/src/ast/finite_sets_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -3,7 +3,7 @@ Copyright (c) 2025 Microsoft Corporation Module Name: - finite_sets_decl_plugin.h + finite_set_decl_plugin.h Abstract: Declaration plugin for finite sets signatures @@ -29,11 +29,11 @@ Operators: #include "ast/ast.h" -enum finite_sets_sort_kind { +enum finite_set_sort_kind { FINITE_SET_SORT }; -enum finite_sets_op_kind { +enum finite_set_op_kind { OP_FINITE_SET_EMPTY, OP_FINITE_SET_SINGLETON, OP_FINITE_SET_UNION, @@ -48,7 +48,7 @@ enum finite_sets_op_kind { LAST_FINITE_SET_OP }; -class finite_sets_decl_plugin : public decl_plugin { +class finite_set_decl_plugin : public decl_plugin { struct psig { symbol m_name; unsigned m_num_params; @@ -77,11 +77,11 @@ class finite_sets_decl_plugin : public decl_plugin { sort * get_element_sort(sort* finite_set_sort) const; public: - finite_sets_decl_plugin(); - ~finite_sets_decl_plugin() override; + finite_set_decl_plugin(); + ~finite_set_decl_plugin() override; decl_plugin * mk_fresh() override { - return alloc(finite_sets_decl_plugin); + return alloc(finite_set_decl_plugin); } void finalize() override { @@ -118,11 +118,11 @@ public: bool is_unique_value(app* e) const override; }; -class finite_sets_recognizers { +class finite_set_recognizers { protected: family_id m_fid; public: - finite_sets_recognizers(family_id fid):m_fid(fid) {} + finite_set_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()); } @@ -139,11 +139,11 @@ public: 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 { +class finite_set_util : public finite_set_recognizers { ast_manager& m_manager; public: - finite_sets_util(ast_manager& m): - finite_sets_recognizers(m.mk_family_id("finite_sets")), m_manager(m) {} + finite_set_util(ast_manager& m): + finite_set_recognizers(m.mk_family_id("finite_set")), m_manager(m) {} ast_manager& get_manager() const { return m_manager; } diff --git a/src/ast/reg_decl_plugins.cpp b/src/ast/reg_decl_plugins.cpp index 961d95e81..18b3e79cb 100644 --- a/src/ast/reg_decl_plugins.cpp +++ b/src/ast/reg_decl_plugins.cpp @@ -29,7 +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" +#include "ast/finite_set_decl_plugin.h" void reg_decl_plugins(ast_manager & m) { if (!m.get_plugin(m.mk_family_id(symbol("arith")))) { @@ -65,7 +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)); + if (!m.get_plugin(m.mk_family_id(symbol("finite_set")))) { + m.register_plugin(symbol("finite_set"), alloc(finite_set_decl_plugin)); } } diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 2298653bf..ac9585b1a 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -54,7 +54,7 @@ add_executable(test-z3 expr_substitution.cpp ext_numeral.cpp f2n.cpp - finite_sets.cpp + finite_set.cpp factor_rewriter.cpp finder.cpp fixed_bit_vector.cpp diff --git a/src/test/finite_sets.cpp b/src/test/finite_set.cpp similarity index 93% rename from src/test/finite_sets.cpp rename to src/test/finite_set.cpp index 78789e04a..977c60f06 100644 --- a/src/test/finite_sets.cpp +++ b/src/test/finite_set.cpp @@ -3,7 +3,7 @@ Copyright (c) 2025 Microsoft Corporation Module Name: - tst_finite_sets.cpp + tst_finite_set.cpp Abstract: @@ -17,16 +17,16 @@ Revision History: --*/ #include "ast/ast.h" -#include "ast/finite_sets_decl_plugin.h" +#include "ast/finite_set_decl_plugin.h" #include "ast/reg_decl_plugins.h" #include "ast/arith_decl_plugin.h" #include "ast/array_decl_plugin.h" -static void tst_finite_sets_basic() { +static void tst_finite_set_basic() { ast_manager m; reg_decl_plugins(m); - finite_sets_util fsets(m); + finite_set_util fsets(m); arith_util arith(m); // Test creating a finite set sort @@ -85,11 +85,11 @@ static void tst_finite_sets_basic() { ENSURE(m.is_bool(subset_expr->get_sort())); } -static void tst_finite_sets_map_filter() { +static void tst_finite_set_map_filter() { ast_manager m; reg_decl_plugins(m); - finite_sets_util fsets(m); + finite_set_util fsets(m); arith_util arith(m); array_util autil(m); @@ -127,7 +127,7 @@ static void tst_finite_sets_map_filter() { ENSURE(filtered_set->get_sort() == finite_set_int.get()); } -void tst_finite_sets() { - tst_finite_sets_basic(); - tst_finite_sets_map_filter(); +void tst_finite_set() { + tst_finite_set_basic(); + tst_finite_set_map_filter(); } diff --git a/src/test/main.cpp b/src/test/main.cpp index feddbd9fd..d7ff6cf71 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -282,5 +282,5 @@ int main(int argc, char ** argv) { TST(scoped_vector); TST(sls_seq_plugin); TST(ho_matcher); - TST(finite_sets); + TST(finite_set); }