diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 8ec24bc9b..701e531b1 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -68,7 +68,7 @@ void finite_set_decl_plugin::init() { m_sigs[OP_FINITE_SET_SIZE] = alloc(polymorphism::psig, m, "set.size", 1, 1, &setA, intT); m_sigs[OP_FINITE_SET_SUBSET] = alloc(polymorphism::psig, m, "set.subset", 1, 2, setAsetA, boolT); m_sigs[OP_FINITE_SET_MAP] = alloc(polymorphism::psig, m, "set.map", 2, 2, arrABsetA, setB); - m_sigs[OP_FINITE_SET_SELECT] = alloc(polymorphism::psig, m, "set.select", 1, 2, arrABoolsetA, setA); + m_sigs[OP_FINITE_SET_FILTER] = alloc(polymorphism::psig, m, "set.filter", 1, 2, arrABoolsetA, setA); m_sigs[OP_FINITE_SET_RANGE] = alloc(polymorphism::psig, m, "set.range", 0, 2, intintT, setInt); m_sigs[OP_FINITE_SET_DIFF] = alloc(polymorphism::psig, m, "set.diff", 1, 2, setAsetA, A); // m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, "set.map_inverse", 2, 3, arrABsetBsetA, A); @@ -158,7 +158,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_SELECT: + case OP_FINITE_SET_FILTER: case OP_FINITE_SET_RANGE: case OP_FINITE_SET_DIFF: return mk_finite_set_op(k, arity, domain, range); diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index 384217667..5eec15d27 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.select : (S -> Bool) (FiniteSet S) -> (FiniteSet S) + set.filter : (S -> Bool) (FiniteSet S) -> (FiniteSet S) set.range : Int Int -> (FiniteSet Int) set.diff : (FiniteSet S) (FiniteSet S) -> S @@ -45,7 +45,7 @@ enum finite_set_op_kind { OP_FINITE_SET_SIZE, OP_FINITE_SET_SUBSET, OP_FINITE_SET_MAP, - OP_FINITE_SET_SELECT, + OP_FINITE_SET_FILTER, OP_FINITE_SET_RANGE, OP_FINITE_SET_DIFF, OP_FINITE_SET_MAP_INVERSE, @@ -131,7 +131,7 @@ public: bool is_size(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_SIZE); } bool is_subset(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_SUBSET); } bool is_map(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_MAP); } - bool is_select(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_SELECT); } + bool is_filter(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_FILTER); } bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_RANGE); } MATCH_UNARY(is_singleton); @@ -142,7 +142,7 @@ public: MATCH_BINARY(is_in); MATCH_BINARY(is_subset); MATCH_BINARY(is_map); - MATCH_BINARY(is_select); + MATCH_BINARY(is_filter); MATCH_BINARY(is_range); }; @@ -191,8 +191,8 @@ public: return m_manager.mk_app(m_fid, OP_FINITE_SET_MAP, arr, set); } - app * mk_select(expr* arr, expr* set) { - return m_manager.mk_app(m_fid, OP_FINITE_SET_SELECT, arr, set); + app * mk_filter(expr* arr, expr* set) { + return m_manager.mk_app(m_fid, OP_FINITE_SET_FILTER, arr, set); } app * mk_range(expr* low, expr* high) { diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index f16d619e8..3d2a8d222 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -230,11 +230,11 @@ void finite_set_axioms::in_map_image_axiom(expr *x, expr *a) { m_add_clause(clause); } -// a := set.select(p, b) +// a := set.filter(p, b) // (x in a) <=> (x in b) and p(x) -void finite_set_axioms::in_select_axiom(expr *x, expr *a) { +void finite_set_axioms::in_filter_axiom(expr *x, expr *a) { expr* p = nullptr, *b = nullptr; - if (!u.is_select(a, p, b)) + if (!u.is_filter(a, p, b)) return; expr_ref x_in_a(u.mk_in(x, a), m); diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h index 250179911..99eb39066 100644 --- a/src/ast/rewriter/finite_set_axioms.h +++ b/src/ast/rewriter/finite_set_axioms.h @@ -57,9 +57,9 @@ public: // (x in b) => f(x) in a void in_map_image_axiom(expr *x, expr *a); - // a := set.select(p, b) + // a := set.filter(p, b) // (x in a) <=> (x in b) and p(x) - void in_select_axiom(expr *x, expr *a); + void in_filter_axiom(expr *x, expr *a); // a := set.subset(b, c) // (a) <=> (set.intersect(b, c) = b) diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 9140c4013..fbcec80b4 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -561,8 +561,8 @@ namespace smt { m_axioms.in_map_axiom(elem, set); m_axioms.in_map_image_axiom(elem, set); } - else if (u.is_select(set)) { - m_axioms.in_select_axiom(elem, set); + else if (u.is_filter(set)) { + m_axioms.in_filter_axiom(elem, set); } } diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index ff6cf8176..7ee4ec564 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -53,7 +53,8 @@ Abstract: ----------------------------------------------- x in v4 => f(x) in v3 - x in v1 a tern, v1 ~ v3, v3 := (set.select p v4) + + x in v1 is a term, v1 ~ v3, v3 == (set.filter p v4) ----------------------------------------------- x in v3 <=> p(x) and x in v4 diff --git a/src/test/finite_set.cpp b/src/test/finite_set.cpp index da0ce93d4..e2e28e8a4 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_select() { +static void tst_finite_set_map_filter() { ast_manager m; reg_decl_plugins(m); @@ -116,15 +116,15 @@ static void tst_finite_set_map_select() { ENSURE(fsets.is_map(mapped_set.get())); ENSURE(fsets.is_finite_set(mapped_set->get_sort())); - // Create Array (Int Bool) sort for select + // Create Array (Int Bool) sort for filter sort_ref arr_int_bool(autil.mk_array_sort(int_sort, bool_sort), 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); + // Create a const array for filter (conceptually represents predicate) + app_ref arr_filter(autil.mk_const_array(arr_int_bool, m.mk_true()), m); - 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()); + 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()); } static void tst_finite_set_is_value() { @@ -221,7 +221,7 @@ static void tst_finite_set_is_fully_interp() { void tst_finite_set() { tst_finite_set_basic(); - tst_finite_set_map_select(); + tst_finite_set_map_filter(); tst_finite_set_is_value(); tst_finite_set_is_fully_interp(); }