From 454a8c340657585b9271083cc785e8a5a2b1e32d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 Oct 2025 13:18:35 +0200
Subject: [PATCH] =?UTF-8?q?Revert=20"Add=20finite=5Fset=5Fvalue=5Ffactory?=
 =?UTF-8?q?=20for=20creating=20finite=20set=20values=20in=20model=20?=
 =?UTF-8?q?=E2=80=A6"=20(#7985)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This reverts commit 05ffc0a77be2c565d09c9bc12bc0a35fd61bbe80.
---
 src/model/finite_set_value_factory.cpp | 58 --------------------------
 src/model/finite_set_value_factory.h   | 30 -------------
 src/model/model.cpp                    |  3 ++
 3 files changed, 3 insertions(+), 88 deletions(-)
 delete mode 100644 src/model/finite_set_value_factory.cpp
 delete 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
deleted file mode 100644
index df9ef46bc..000000000
--- a/src/model/finite_set_value_factory.cpp
+++ /dev/null
@@ -1,58 +0,0 @@
-/*++
-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
deleted file mode 100644
index 8dbbc7aae..000000000
--- a/src/model/finite_set_value_factory.h
+++ /dev/null
@@ -1,30 +0,0 @@
-/*++
-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;
-};
-
diff --git a/src/model/model.cpp b/src/model/model.cpp
index 4b8a8f89d..1c650ef04 100644
--- a/src/model/model.cpp
+++ b/src/model/model.cpp
@@ -111,11 +111,14 @@ value_factory* model::get_factory(sort* s) {
         m_factories.register_plugin(alloc(arith_factory, m));
         m_factories.register_plugin(alloc(seq_factory, m, su.get_family_id(), *this));
         m_factories.register_plugin(alloc(fpa_value_factory, m, fu.get_family_id()));
+<<<<<<< HEAD
 <<<<<<< HEAD
         m_factories.register_plugin(alloc(finite_set_factory, m, m.get_family_id("finite_set"), *this));
 =======
         m_factories.register_plugin(alloc(finite_set_value_factory, m, m.mk_family_id("finite_set"), *this));
 >>>>>>> 05ffc0a77 (Add finite_set_value_factory for creating finite set values in model generation (#7981))
+=======
+>>>>>>> 62ee7ccf6 (Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985))
         //m_factories.register_plugin(alloc(char_factory, m, char_decl_plugin(m).get_family_id());
     }
     family_id fid = s->get_family_id();