restructure base class struct_factory so that enumeration of values for a sort comes together with hash-table access. This allows to use the enumeration view during value creations for finite sets

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/model/array_factory.cpp

@@ -63,8 +63,8 @@ void array_factory::get_some_args_for(sort * s, ptr_buffer<expr> & args) {
 expr * array_factory::get_some_value(sort * s) {
     TRACE(array_factory, tout << mk_pp(s, m_manager) << "\n";);
     value_set * set = nullptr;
-    if (m_sort2value_set.find(s, set) && !set->empty())
+    if (m_sort2value_set.find(s, set) && !set->set.empty())
-        return *(set->begin());
+        return *(set->set.begin());
     func_interp * fi;
     expr * val = mk_array_interp(s, fi);
     fi->set_else(m_model.get_some_value(get_array_range(s)));
@@ -75,7 +75,7 @@ bool array_factory::mk_two_diff_values_for(sort * s) {
     TRACE(array_factory, tout << mk_pp(s, m_manager) << "\n";);
     DEBUG_CODE({
         value_set * set = 0;
-        SASSERT(!m_sort2value_set.find(s, set) || set->size() <= 1);
+        SASSERT(!m_sort2value_set.find(s, set) || set->set.size() <= 1);
     });
     expr_ref r1(m_manager);
     expr_ref r2(m_manager);
@@ -92,24 +92,24 @@ bool array_factory::mk_two_diff_values_for(sort * s) {
     fi2->insert_entry(args.data(), r2);
     DEBUG_CODE({
         value_set * set = 0;
-        SASSERT(m_sort2value_set.find(s, set) && set->size() >= 2);
+        SASSERT(m_sort2value_set.find(s, set) && set->set.size() >= 2);
     });
     return true;
 }
 
 bool array_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
     value_set * set = nullptr;
-    if (!m_sort2value_set.find(s, set) || set->size() < 2) {
+    if (!m_sort2value_set.find(s, set) || set->set.size() < 2) {
         if (!mk_two_diff_values_for(s)) {
             TRACE(array_factory_bug, tout << "could not create diff values: " << mk_pp(s, m_manager) << "\n";);
             return false;
         }
     }
     m_sort2value_set.find(s, set);
-    SASSERT(set != 0);
+    SASSERT(set);
-    SASSERT(set->size() >= 2);
+    SASSERT(set->set.size() >= 2);
-    
+
-    value_set::iterator it = set->begin();
+    auto it = set->set.begin();
     v1 = *it;
     ++it;
     v2 = *it;
@@ -126,8 +126,8 @@ bool array_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
 // is set with the result of some entry.
 //
 expr * array_factory::get_fresh_value(sort * s) {
-    value_set * set = get_value_set(s);
+    auto& [set, values] = get_value_set(s);
-    if (set->empty()) {
+    if (set.empty()) {
         // easy case 
         return get_some_value(s);
     }

src/model/datatype_factory.cpp

@@ -30,8 +30,8 @@ expr * datatype_factory::get_some_value(sort * s) {
     if (!m_util.is_datatype(s))
         return m_model.get_some_value(s);
     value_set * set = nullptr;
-    if (m_sort2value_set.find(s, set) && !set->empty())
+    if (m_sort2value_set.find(s, set) && !set->set.empty())
-        return *(set->begin());
+        return *(set->set.begin());
     func_decl * c = m_util.get_non_rec_constructor(s);
     ptr_vector<expr> args;
     unsigned num  = c->get_arity();
@@ -50,11 +50,11 @@ expr * datatype_factory::get_last_fresh_value(sort * s) {
     expr * val = nullptr;
     if (m_last_fresh_value.find(s, val)) 
         return val;
-    value_set * set = get_value_set(s);
+    auto& [set, values] = get_value_set(s);
-    if (set->empty())
+    if (set.empty())
         val = get_some_value(s);
     else 
-        val = *(set->begin());
+        val = *(set.begin());
     if (m_util.is_recursive(s))
         m_last_fresh_value.insert(s, val);
     return val;
@@ -78,8 +78,8 @@ bool datatype_factory::is_subterm_of_last_value(app* e) {
 expr * datatype_factory::get_almost_fresh_value(sort * s) {
     if (!m_util.is_datatype(s))
         return m_model.get_some_value(s);
-    value_set * set = get_value_set(s);
+    auto& [set, values] = get_value_set(s);
-    if (set->empty()) {
+    if (set.empty()) {
         expr * val = get_some_value(s);
         SASSERT(val);
         if (m_util.is_recursive(s))
@@ -117,7 +117,7 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
         }
         if (recursive || found_fresh_arg) {
             app * new_value = m_manager.mk_app(constructor, args);
-            SASSERT(!found_fresh_arg || !set->contains(new_value));
+            SASSERT(!found_fresh_arg || !set.contains(new_value));
             register_value(new_value);
             if (m_util.is_recursive(s)) {
                 if (is_subterm_of_last_value(new_value)) {
@@ -140,10 +140,10 @@ expr * datatype_factory::get_fresh_value(sort * s) {
     if (!m_util.is_datatype(s))
         return m_model.get_fresh_value(s);
     TRACE(datatype, tout << "generating fresh value for: " << s->get_name() << "\n";);
-    value_set * set = get_value_set(s);
+    auto& [set, values] = get_value_set(s);
     // Approach 0) 
     // if no value for s was generated so far, then used get_some_value
-    if (set->empty()) {
+    if (set.empty()) {
         expr * val = get_some_value(s);
         if (m_util.is_recursive(s))
             m_last_fresh_value.insert(s, val);
@@ -178,12 +178,11 @@ expr * datatype_factory::get_fresh_value(sort * s) {
             expr * some_arg = m_model.get_some_value(s_arg);
             args.push_back(some_arg);
         }
-
         new_value = m_manager.mk_app(constructor, args);
-        CTRACE(datatype, found_fresh_arg && set->contains(new_value), tout << "seen: " << new_value << "\n";);
+        CTRACE(datatype, found_fresh_arg && set.contains(new_value), tout << "seen: " << new_value << "\n";);
-        if (found_fresh_arg && set->contains(new_value))
+        if (found_fresh_arg && set.contains(new_value))
             goto retry_value;
-        if (!set->contains(new_value)) {
+        if (!set.contains(new_value)) {
             register_value(new_value);
             if (m_util.is_recursive(s))
                 m_last_fresh_value.insert(s, new_value);
@@ -241,7 +240,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
                     new_value = m_manager.mk_app(constructor, args);
                     TRACE(datatype, tout << "potential new value: " << mk_pp(new_value, m_manager) << "\n";);
                     m_last_fresh_value.insert(s, new_value);
-                    if (!set->contains(new_value)) {
+                    if (!set.contains(new_value)) {
                         register_value(new_value);
                         TRACE(datatype, tout << "2. result: " << mk_pp(new_value, m_manager) << "\n";);
                         return new_value;

src/model/struct_factory.cpp

@@ -19,41 +19,39 @@ Revision History:
 #include "model/struct_factory.h"
 #include "model/model_core.h"
 
-struct_factory::value_set * struct_factory::get_value_set(sort * s) {
+struct_factory::value_set& struct_factory::get_value_set(sort * s) {
     value_set * set = nullptr;
     if (!m_sort2value_set.find(s, set)) {
-        set = alloc(value_set);
+        set = alloc(value_set, m_model.get_manager());
         m_sort2value_set.insert(s, set);
         m_sorts.push_back(s);
         m_sets.push_back(set);
     }
     SASSERT(set != 0);
-    return set;
+    return *set;
 }
 
 struct_factory::struct_factory(ast_manager & m, family_id fid, model_core & md):
     value_factory(m, fid),
     m_model(md),
-    m_values(m),
     m_sorts(m) {
 }
 
 struct_factory::~struct_factory() {
-    std::for_each(m_sets.begin(), m_sets.end(), delete_proc<value_set>());
 }
 
 void struct_factory::register_value(expr * new_value) {
     sort * s        = new_value->get_sort();
-    value_set * set = get_value_set(s);
+    auto& [set, values] = get_value_set(s);
-    if (!set->contains(new_value)) {
+    if (!set.contains(new_value)) {
-        m_values.push_back(new_value);
+        values.push_back(new_value);
-        set->insert(new_value);
+        set.insert(new_value);
     }
 }
 
 bool struct_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
-    value_set * set = get_value_set(s);
+    auto& [set, values] = get_value_set(s);
-    switch (set->size()) {
+    switch (set.size()) {
     case 0:
         v1 = get_fresh_value(s);
         v2 = get_fresh_value(s);
@@ -63,7 +61,7 @@ bool struct_factory::get_some_values(sort * s, expr_ref & v1, expr_ref & v2) {
         v2 = get_fresh_value(s);
         return v2 != 0;
     default:
-        obj_hashtable<expr>::iterator it = set->begin();
+        obj_hashtable<expr>::iterator it = set.begin();
         v1 = *it;
         ++it;
         v2 = *it;

src/model/struct_factory.h

@@ -20,6 +20,7 @@ Revision History:
 
 #include "model/value_factory.h"
 #include "util/obj_hashtable.h"
+#include "util/scoped_ptr_vector.h"
 
 class model_core;
 
@@ -28,16 +29,19 @@ class model_core;
 */
 class struct_factory : public value_factory {
 protected:
-    typedef obj_hashtable<expr> value_set;
+    struct value_set {
-    typedef obj_map<sort, value_set *> sort2value_set;
+        obj_hashtable<expr> set;
+        expr_ref_vector values;
+        value_set(ast_manager &m) : values(m) {}
+    };
+    using sort2value_set = obj_map<sort, value_set *>;
 
     model_core &          m_model;
     sort2value_set        m_sort2value_set;
-    expr_ref_vector       m_values;
     sort_ref_vector       m_sorts;
-    ptr_vector<value_set> m_sets;
+    scoped_ptr_vector<value_set> m_sets;
     
-    value_set * get_value_set(sort * s);
+    value_set& get_value_set(sort * s);
 
 public:
     struct_factory(ast_manager & m, family_id fid, model_core & md);

src/smt/theory_finite_set.cpp

@@ -10,12 +10,6 @@ Abstract:
     Theory solver for finite sets.
     Implements axiom schemas for finite set operations.
 
-Author:
-
-    GitHub Copilot Agent 2025
-
-Revision History:
-
 --*/
 
 #include "smt/theory_finite_set.h"