From 5135fd3408336d76379a90e54460039ef2a949a6 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 5 Oct 2025 20:03:17 +0000 Subject: [PATCH] Rename set.filter to set.select Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/finite_set_decl_plugin.cpp | 4 ++-- src/ast/finite_set_decl_plugin.h | 10 +++++----- src/test/finite_set.cpp | 16 ++++++++-------- 3 files changed, 15 insertions(+), 15 deletions(-) diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 4753f1662..5ae22a84d 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -143,7 +143,7 @@ void finite_set_decl_plugin::init() { m_sigs[OP_FINITE_SET_SIZE] = alloc(psig, m, "set.size", 1, 1, &setA, intT); m_sigs[OP_FINITE_SET_SUBSET] = alloc(psig, m, "set.subset", 1, 2, setAsetA, boolT); m_sigs[OP_FINITE_SET_MAP] = alloc(psig, m, "set.map", 2, 2, arrABsetA, setB); - m_sigs[OP_FINITE_SET_FILTER] = alloc(psig, m, "set.filter", 1, 2, arrABoolsetA, setA); + m_sigs[OP_FINITE_SET_SELECT] = alloc(psig, m, "set.select", 1, 2, arrABoolsetA, setA); m_sigs[OP_FINITE_SET_RANGE] = alloc(psig, m, "set.range", 0, 2, intintT, setInt); } @@ -214,7 +214,7 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param case OP_FINITE_SET_SIZE: case OP_FINITE_SET_SUBSET: case OP_FINITE_SET_MAP: - case OP_FINITE_SET_FILTER: + case OP_FINITE_SET_SELECT: case OP_FINITE_SET_RANGE: return mk_finite_set_op(k, arity, domain, range); default: diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index e411099dc..7239f864a 100644 --- a/src/ast/finite_set_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -21,7 +21,7 @@ Operators: set.size : (FiniteSet S) -> Int set.subset : (FiniteSet S) (FiniteSet S) -> Bool set.map : (S -> T) (FiniteSet S) -> (FiniteSet T) - set.filter : (S -> Bool) (FiniteSet S) -> (FiniteSet S) + set.select : (S -> Bool) (FiniteSet S) -> (FiniteSet S) set.range : Int Int -> (FiniteSet Int) --*/ @@ -43,7 +43,7 @@ enum finite_set_op_kind { OP_FINITE_SET_SIZE, OP_FINITE_SET_SUBSET, OP_FINITE_SET_MAP, - OP_FINITE_SET_FILTER, + OP_FINITE_SET_SELECT, OP_FINITE_SET_RANGE, LAST_FINITE_SET_OP }; @@ -135,7 +135,7 @@ public: 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_select(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_SELECT); } bool is_range(expr* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_RANGE); } }; @@ -184,8 +184,8 @@ public: return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP, arr, set); } - app * mk_filter(expr* arr, expr* set) { - return m_manager.mk_app(m_fid, OP_FINITE_SET_FILTER, arr, set); + app * mk_select(expr* arr, expr* set) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_SELECT, arr, set); } app * mk_range(expr* low, expr* high) { diff --git a/src/test/finite_set.cpp b/src/test/finite_set.cpp index 977c60f06..b7b07f074 100644 --- a/src/test/finite_set.cpp +++ b/src/test/finite_set.cpp @@ -85,7 +85,7 @@ static void tst_finite_set_basic() { ENSURE(m.is_bool(subset_expr->get_sort())); } -static void tst_finite_set_map_filter() { +static void tst_finite_set_map_select() { ast_manager m; reg_decl_plugins(m); @@ -116,18 +116,18 @@ static void tst_finite_set_map_filter() { ENSURE(fsets.is_map(mapped_set.get())); ENSURE(fsets.is_finite_set(mapped_set->get_sort())); - // Create Array (Int Bool) sort for filter + // Create Array (Int Bool) sort for select sort_ref arr_int_bool(autil.mk_array_sort(int_sort, bool_sort), m); - // Create a const array for filter (conceptually represents predicate) - app_ref arr_filter(autil.mk_const_array(arr_int_bool, m.mk_true()), m); + // Create a const array for select (conceptually represents predicate) + app_ref arr_select(autil.mk_const_array(arr_int_bool, m.mk_true()), m); - app_ref filtered_set(fsets.mk_filter(arr_filter, range_set), m); - ENSURE(fsets.is_filter(filtered_set.get())); - ENSURE(filtered_set->get_sort() == finite_set_int.get()); + app_ref selected_set(fsets.mk_select(arr_select, range_set), m); + ENSURE(fsets.is_select(selected_set.get())); + ENSURE(selected_set->get_sort() == finite_set_int.get()); } void tst_finite_set() { tst_finite_set_basic(); - tst_finite_set_map_filter(); + tst_finite_set_map_select(); }