mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 13:07:53 +00:00
Code Activity

Merge branch 'finite-sets' into copilot/update-finite-set-check-function

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-10-16 08:31:53 +02:00 • committed by GitHub
commit a9a61912b9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
3 changed files with 45 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/finite_set_decl_plugin.cpp
View file

@ -183,7 +183,9 @@ expr * finite_set_decl_plugin::get_some_value(sort * s) {
}
bool finite_set_decl_plugin::is_fully_interp(sort * s) const {
return false;
SASSERT(is_finite_set(s));
sort* element_sort = get_element_sort(s);
return element_sort && m_manager->is_fully_interp(element_sort);
}
bool finite_set_decl_plugin::is_value(app * e) const {

21
src/ast/rewriter/finite_set_rewriter.h
View file

@ -33,7 +33,17 @@ where the signature is defined in finite_set_decl_plugin.h.
\brief Cheap rewrite rules for finite sets
*/
class finite_set_rewriter {
friend class finite_set_rewriter_test;
finite_set_util m_util;
// Rewrite rules for set operations
br_status mk_union(unsigned num_args, expr *const *args, expr_ref &result);
br_status mk_intersect(unsigned num_args, expr *const *args, expr_ref &result);
br_status mk_difference(expr *arg1, expr *arg2, expr_ref &result);
br_status mk_subset(expr *arg1, expr *arg2, expr_ref &result);
br_status mk_singleton(expr *arg1, expr_ref &result);
br_status mk_in(expr *arg1, expr *arg2, expr_ref &result);
public:
finite_set_rewriter(ast_manager & m, params_ref const & p = params_ref()):
m_util(m) {
@ -43,15 +53,6 @@ public:
family_id get_fid() const { return m_util.get_family_id(); }
finite_set_util& util() { return m_util; }
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
// Rewrite rules for set operations
br_status mk_union(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_intersect(unsigned num_args, expr * const * args, expr_ref & result);
br_status mk_difference(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_subset(expr * arg1, expr * arg2, expr_ref & result);
br_status mk_singleton(expr *arg1, expr_ref &result);
br_status mk_in(expr *arg1, expr *arg2, expr_ref &result);
br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
};

33
src/test/finite_set.cpp
View file

@ -131,16 +131,21 @@ static void tst_finite_set_is_value() {
ast_manager m;
reg_decl_plugins(m);
finite_set_util fsets(m);
arith_util arith(m);
finite_set_decl_plugin* plugin = static_cast<finite_set_decl_plugin*>(m.get_plugin(fsets.get_family_id()));
// Create Int sort and finite set sort
// Create Int sort and finite set sort
// Test with Int sort (should be fully interpreted)
sort_ref int_sort(arith.mk_int(), m);
parameter int_param(int_sort.get());
sort_ref finite_set_int(m.mk_sort(fsets.get_family_id(), FINITE_SET_SORT, 1, &int_param), m);
// Test 1: Empty set is a value
// Test 1: Empty set is a value
app_ref empty_set(fsets.mk_empty(finite_set_int), m);
ENSURE(plugin->is_value(empty_set.get()));
@ -187,10 +192,34 @@ static void tst_finite_set_is_value() {
// Test 10: Intersect is NOT a value
app_ref intersect_set(fsets.mk_intersect(singleton_five, singleton_seven), m);
ENSURE(!plugin->is_value(intersect_set.get()));
ENSURE(m.is_fully_interp(int_sort));
ENSURE(m.is_fully_interp(finite_set_int));
}
static void tst_finite_set_is_fully_interp() {
ast_manager m;
reg_decl_plugins(m);
// Test with Bool sort (should be fully interpreted)
sort_ref bool_sort(m.mk_bool_sort(), m);
parameter bool_param(bool_sort.get());
sort_ref finite_set_bool(m.mk_sort(fsets.get_family_id(), FINITE_SET_SORT, 1, &bool_param), m);
ENSURE(m.is_fully_interp(bool_sort));
ENSURE(m.is_fully_interp(finite_set_bool));
// Test with uninterpreted sort (should not be fully interpreted)
sort_ref uninterp_sort(m.mk_uninterpreted_sort(symbol("U")), m);
parameter uninterp_param(uninterp_sort.get());
sort_ref finite_set_uninterp(m.mk_sort(fsets.get_family_id(), FINITE_SET_SORT, 1, &uninterp_param), m);
ENSURE(!m.is_fully_interp(uninterp_sort));
ENSURE(!m.is_fully_interp(finite_set_uninterp));
}
void tst_finite_set() {
tst_finite_set_basic();
tst_finite_set_map_select();
tst_finite_set_is_value();
tst_finite_set_is_fully_interp();
}