From 85e1a39c09df4e180957c478ba1fcdc403bcca07 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Thu, 16 Oct 2025 13:16:54 +0200 Subject: [PATCH] Add finite_set_value_factory for creating finite set values in model generation (#7981) * Initial plan * Add finite_set_value_factory implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Remove unused dl_decl_plugin variable and include Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Update copyright and add TODOs in finite_set_value_factory Updated copyright information and added TODO comments for handling in finite_set_value_factory methods. * Update copyright information in finite_set_value_factory.h Updated copyright year from 2006 to 2025. * Implement finite_set_value_factory using array_util to create singleton sets Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Simplify empty set creation in finite_set_value_factory Refactor finite_set_value_factory to simplify empty set handling and remove array-specific logic. * Change family ID for finite_set_value_factory * Fix build error by restoring array_decl_plugin include and implementation Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> * Update finite_set_value_factory.h * Add SASSERT for finite set check in factory Added assertion to check if the sort is a finite set. * Rename member variable from m_util to u * Refactor finite_set_value_factory for value handling * Use register_value instead of direct set insertion Replaced direct insertion into set with register_value calls. * Update finite_set_value_factory.cpp --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/model/finite_set_value_factory.cpp | 58 ++++++++++++++++++++++++++ src/model/finite_set_value_factory.h | 30 +++++++++++++ 2 files changed, 88 insertions(+) create mode 100644 src/model/finite_set_value_factory.cpp create mode 100644 src/model/finite_set_value_factory.h diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_value_factory.cpp new file mode 100644 index 000000000..df9ef46bc --- /dev/null +++ b/src/model/finite_set_value_factory.cpp @@ -0,0 +1,58 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + finite_set_value_factory.cpp + +Abstract: + + Factory for creating finite set values + +--*/ +#include "model/finite_set_value_factory.h" +#include "model/model_core.h" + +finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md): + struct_factory(m, fid, md), + u(m) { +} + +expr * finite_set_value_factory::get_some_value(sort * s) { + // Check if we already have a value for this sort + value_set * set = nullptr; + SASSERT(u.is_finite_set(s)); + #if 0 + if (m_sort2value_set.find(s, set) && !set->empty()) + return *(set->begin()); + #endif + 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 + + return nullptr; + #if 0 + value_set * set = get_value_set(s); + + // If no values have been generated yet, use get_some_value + if (set->empty()) { + auto r = u.mk_empty(s); + register_value(r); + return r; + } + auto e = md.get_fresh_value(elem_sort); + if (e) { + auto r = u.mk_singleton(e); + register_value(r); + return r; + } + + // For finite domains, we may not be able to generate fresh values + // if all values have been exhausted + return nullptr; + #endif +} diff --git a/src/model/finite_set_value_factory.h b/src/model/finite_set_value_factory.h new file mode 100644 index 000000000..8dbbc7aae --- /dev/null +++ b/src/model/finite_set_value_factory.h @@ -0,0 +1,30 @@ +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + finite_set_value_factory.h + +Abstract: + + Factory for creating finite set values + +--*/ +#pragma once + +#include "model/struct_factory.h" +#include "ast/finite_set_decl_plugin.h" + +/** + \brief Factory for finite set values. +*/ +class finite_set_value_factory : public struct_factory { + finite_set_util u; +public: + finite_set_value_factory(ast_manager & m, family_id fid, model_core & md); + + expr * get_some_value(sort * s) override; + + expr * get_fresh_value(sort * s) override; +}; +