From 8b55214817b8b2d86b117f654ce660808a1873df Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Oct 2025 21:59:14 +0200 Subject: [PATCH] Simplify empty set creation in finite_set_value_factory Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic. --- src/model/finite_set_value_factory.cpp | 32 ++++---------------------- 1 file changed, 5 insertions(+), 27 deletions(-) diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp index 9ad208d02..b6534e6b1 100644 --- a/src/model/finite_set_value_factory.cpp +++ b/src/model/finite_set_value_factory.cpp @@ -12,7 +12,7 @@ Abstract: --*/ #include "model/finite_set_value_factory.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): 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()) 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; + expr * empty = m_util.mk_empty(s); + register_value(empty); + return empty; } 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 (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; - } - } + // TODO: finite_set singleton with fresh values // For finite domains, we may not be able to generate fresh values // if all values have been exhausted