mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-05 22:06:03 +00:00
Code Activity

Implement finite_set is_fully_interp to check element sort

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2025-10-15 19:38:59 +00:00
parent 5a9025ade7
commit f7a8260356
2 changed files with 39 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/finite_set_decl_plugin.cpp
View file

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

33
src/test/finite_set.cpp
View file

@ -127,7 +127,40 @@ static void tst_finite_set_map_select() {
ENSURE(selected_set->get_sort() == finite_set_int.get());
}
static void tst_finite_set_is_fully_interp() {
ast_manager m;
reg_decl_plugins(m);
finite_set_util fsets(m);
arith_util arith(m);
// 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);
ENSURE(m.is_fully_interp(int_sort));
ENSURE(m.is_fully_interp(finite_set_int));
// 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_fully_interp();
}