mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-08 00:41:56 +00:00
Code Activity

Rename set.filter to set.select

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-10-05 20:03:17 +00:00
parent 495cdba9af
commit 5135fd3408
3 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/finite_set_decl_plugin.cpp
View file

@ -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_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_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_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); 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_SIZE:
case OP_FINITE_SET_SUBSET: case OP_FINITE_SET_SUBSET:
case OP_FINITE_SET_MAP: case OP_FINITE_SET_MAP:
case OP_FINITE_SET_FILTER: case OP_FINITE_SET_SELECT:
case OP_FINITE_SET_RANGE: case OP_FINITE_SET_RANGE:
return mk_finite_set_op(k, arity, domain, range); return mk_finite_set_op(k, arity, domain, range);
default: default:

10
src/ast/finite_set_decl_plugin.h
View file

@ -21,7 +21,7 @@ Operators:
set.size : (FiniteSet S) -> Int set.size : (FiniteSet S) -> Int
set.subset : (FiniteSet S) (FiniteSet S) -> Bool set.subset : (FiniteSet S) (FiniteSet S) -> Bool
set.map : (S -> T) (FiniteSet S) -> (FiniteSet T) 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) set.range : Int Int -> (FiniteSet Int)
--*/ --*/
@ -43,7 +43,7 @@ enum finite_set_op_kind {
OP_FINITE_SET_SIZE, OP_FINITE_SET_SIZE,
OP_FINITE_SET_SUBSET, OP_FINITE_SET_SUBSET,
OP_FINITE_SET_MAP, OP_FINITE_SET_MAP,
OP_FINITE_SET_FILTER, OP_FINITE_SET_SELECT,
OP_FINITE_SET_RANGE, OP_FINITE_SET_RANGE,
LAST_FINITE_SET_OP 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_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_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_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); } 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); return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP, arr, set);
} }
app * mk_filter(expr* arr, expr* set) { app * mk_select(expr* arr, expr* set) {
return m_manager.mk_app(m_fid, OP_FINITE_SET_FILTER, arr, set); return m_manager.mk_app(m_fid, OP_FINITE_SET_SELECT, arr, set);
} }
app * mk_range(expr* low, expr* high) { app * mk_range(expr* low, expr* high) {

16
src/test/finite_set.cpp
View file

@ -85,7 +85,7 @@ static void tst_finite_set_basic() {
ENSURE(m.is_bool(subset_expr->get_sort())); 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; ast_manager m;
reg_decl_plugins(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_map(mapped_set.get()));
ENSURE(fsets.is_finite_set(mapped_set->get_sort())); 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); sort_ref arr_int_bool(autil.mk_array_sort(int_sort, bool_sort), m);
// Create a const array for filter (conceptually represents predicate) // Create a const array for select (conceptually represents predicate)
app_ref arr_filter(autil.mk_const_array(arr_int_bool, m.mk_true()), m); 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); app_ref selected_set(fsets.mk_select(arr_select, range_set), m);
ENSURE(fsets.is_filter(filtered_set.get())); ENSURE(fsets.is_select(selected_set.get()));
ENSURE(filtered_set->get_sort() == finite_set_int.get()); ENSURE(selected_set->get_sort() == finite_set_int.get());
} }
void tst_finite_set() { void tst_finite_set() {
tst_finite_set_basic(); tst_finite_set_basic();
tst_finite_set_map_filter(); tst_finite_set_map_select();
} }