mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 19:52:29 +00:00
Code Activity

Implement get_fresh_value algorithm for finite_set_value_factory (#7987)

Browse source 
* Initial plan

* Implement get_fresh_value algorithm for finite_set_value_factory

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Replace values.back() with values.get(N) as requested

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2025-10-17 14:46:04 +02:00 • committed by GitHub
parent df62e5e9e6
commit 8dd91e4698
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 28 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

46
src/model/finite_set_value_factory.cpp
View file

@ -30,34 +30,40 @@ expr * finite_set_value_factory::get_some_value(sort * s) {
expr * finite_set_value_factory::get_fresh_value(sort * s) { expr * finite_set_value_factory::get_fresh_value(sort * s) {
sort* elem_sort = nullptr; sort* elem_sort = nullptr;
VERIFY(u.is_finite_set(s, elem_sort)); VERIFY(u.is_finite_set(s, elem_sort));
// Get a fresh value for a finite set sort
auto& [set, values] = get_value_set(s); auto& [set, values] = get_value_set(s);
// If no values have been generated yet, use get_some_value // Case 1: If no values have been generated yet, return empty set
if (set.empty()) { if (values.size() == 0) {
auto r = u.mk_empty(s); auto r = u.mk_empty(s);
register_value(r); register_value(r);
return r; return r;
} }
auto e = m_model.get_fresh_value(elem_sort);
if (e) { // Helper lambda to check if a number is a power of 2
auto is_power_of_2 = [](unsigned n) {
return n > 0 && (n & (n - 1)) == 0;
};
// Case 2: If values.size() is a power of 2, create a fresh singleton
if (is_power_of_2(values.size())) {
auto e = m_model.get_fresh_value(elem_sort);
if (!e)
return nullptr;
register_value(e);
auto r = u.mk_singleton(e); auto r = u.mk_singleton(e);
register_value(e); // register e so we can access the finite domain within this class
register_value(r); register_value(r);
return r; return r;
} }
auto& [set_e, values_e] = get_value_set(elem_sort);
unsigned next_index = values.size(); // Case 3: Find greatest power of 2 N < values.size() and create union
SASSERT(next_index >= 1 + values_e.size()); // we already generated the empty set and all singletons // Find the greatest N that is a power of 2 and N < values.size()
unsigned N = 1;
// Course Task of 10-16-25: while (N * 2 < values.size()) {
// For finite domains, we may not be able to generate fresh values N *= 2;
// if all values have been exhausted }
// create sets based on next_index
// assume that values_e contains all the values of the element sort auto r = u.mk_union(values.get(values.size() - N), values.get(N));
// and they have already been generated. register_value(r);
// Figure out if we are creating two, three, or more element sets return r;
// and map next_index into the elements in a uniqe way.
return nullptr;
} }

2
src/test/finite_set.cpp
View file

@ -200,6 +200,8 @@ static void tst_finite_set_is_fully_interp() {
ast_manager m; ast_manager m;
reg_decl_plugins(m); reg_decl_plugins(m);
finite_set_util fsets(m);
// Test with Bool sort (should be fully interpreted) // Test with Bool sort (should be fully interpreted)
sort_ref bool_sort(m.mk_bool_sort(), m); sort_ref bool_sort(m.mk_bool_sort(), m);
parameter bool_param(bool_sort.get()); parameter bool_param(bool_sort.get());