mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-09 23:52:02 +00:00
Code Activity

Simplify empty set creation in finite_set_value_factory

Browse source 
Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic.
This commit is contained in:
Nikolaj Bjorner 2025-10-15 21:59:14 +02:00 • committed by GitHub
parent ea3dc7e217
commit 8b55214817
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 27 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/model/finite_set_value_factory.cpp
View file

@ -12,7 +12,7 @@ Abstract:
--*/ --*/
#include "model/finite_set_value_factory.h" #include "model/finite_set_value_factory.h"
#include "model/model_core.h" #include "model/model_core.h"
#include "ast/array_decl_plugin.h" #include "ast/finite_set_decl_plugin.h"
finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md): finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md):
struct_factory(m, fid, md), struct_factory(m, fid, md),
@ -25,14 +25,9 @@ expr * finite_set_value_factory::get_some_value(sort * s) {
if (m_sort2value_set.find(s, set) && !set->empty()) if (m_sort2value_set.find(s, set) && !set->empty())
return *(set->begin()); return *(set->begin());
// For sets, return an empty set expr * empty = m_util.mk_empty(s);
if (m_util.is_array(s)) { register_value(empty);
expr * empty = m_util.mk_empty_set(s); return empty;
register_value(empty);
return empty;
}
return nullptr;
} }
expr * finite_set_value_factory::get_fresh_value(sort * s) { expr * finite_set_value_factory::get_fresh_value(sort * s) {
@ -42,24 +37,7 @@ expr * finite_set_value_factory::get_fresh_value(sort * s) {
// If no values have been generated yet, use get_some_value // If no values have been generated yet, use get_some_value
if (set->empty()) if (set->empty())
return get_some_value(s); return get_some_value(s);
// TODO: finite_set singleton with fresh values
// 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;
}
}
// For finite domains, we may not be able to generate fresh values // For finite domains, we may not be able to generate fresh values
// if all values have been exhausted // if all values have been exhausted