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

Refactor finite_set_value_factory for value handling

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-10-16 12:54:22 +02:00 • committed by GitHub
parent ab642f4c89
commit 48a8269a8d
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 14 additions and 29 deletions
Download patch file Download diff file Expand all files Collapse all files

41
src/model/finite_set_value_factory.cpp
View file

@ -15,7 +15,7 @@ Abstract:
finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md):
struct_factory(m, fid, md),
m_util(m) {
u(m) {
}
expr * finite_set_value_factory::get_some_value(sort * s) {
@ -24,41 +24,26 @@ expr * finite_set_value_factory::get_some_value(sort * s) {
SASSERT(u.is_finite_set(s));
if (m_sort2value_set.find(s, set) && !set->empty())
return *(set->begin());
// For sets, return an empty set
if (m_util.is_array(s)) {
expr * empty = m_util.mk_empty_set(s);
register_value(empty);
return empty;
}
return nullptr;
return u.mk_empty(s);
}
expr * finite_set_value_factory::get_fresh_value(sort * s) {
sort* elem_sort = nullptr;
VERIFY(u.is_finite_set(s, elem_sort));
// Get a fresh value for a finite set sort
value_set * set = get_value_set(s);
// If no values have been generated yet, use get_some_value
if (set->empty())
return get_some_value(s);
// For sets represented as arrays
if (m_util.is_array(s)) {
// Get the element sort (domain of the array)
sort * elem_sort = get_array_domain(s, 0);
// Try to get a fresh value from the element domain
expr * fresh_elem = m_model.get_fresh_value(elem_sort);
if (fresh_elem != nullptr) {
// Create a singleton set with the fresh element
// Start with an empty set and add the element
expr * empty = m_util.mk_empty_set(s);
expr * args[3] = { empty, fresh_elem, m_manager.mk_true() };
expr * singleton = m_util.mk_store(3, args);
register_value(singleton);
return singleton;
if (set->empty()) {
auto r = u.mk_empty(s);
set->insert(r);
return r;
}
auto e = md.get_fresh_value(elem_sort);
if (e) {
auto r = u.mk_singleton(e);
set->insert(r);
return r;
}
// For finite domains, we may not be able to generate fresh values