diff --git a/src/model/array_factory.cpp b/src/model/array_factory.cpp index 3030eeafd..8c0759538 100644 --- a/src/model/array_factory.cpp +++ b/src/model/array_factory.cpp @@ -63,8 +63,8 @@ void array_factory::get_some_args_for(sort * s, ptr_buffer & 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()) - return *(set->begin()); + if (m_sort2value_set.find(s, set) && !set->set.empty()) + 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->size() >= 2); - - value_set::iterator it = set->begin(); + SASSERT(set); + SASSERT(set->set.size() >= 2); + + 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); - if (set->empty()) { + auto& [set, values] = get_value_set(s); + if (set.empty()) { // easy case return get_some_value(s); } diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index 39e4b6da3..be4ecc385 100644 --- a/src/model/datatype_factory.cpp +++ b/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()) - return *(set->begin()); + if (m_sort2value_set.find(s, set) && !set->set.empty()) + return *(set->set.begin()); func_decl * c = m_util.get_non_rec_constructor(s); ptr_vector 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); - if (set->empty()) + auto& [set, values] = get_value_set(s); + 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); - if (set->empty()) { + auto& [set, values] = get_value_set(s); + 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";); - if (found_fresh_arg && set->contains(new_value)) + CTRACE(datatype, found_fresh_arg && set.contains(new_value), tout << "seen: " << new_value << "\n";); + 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; diff --git a/src/model/struct_factory.cpp b/src/model/struct_factory.cpp index 31f86f883..77171a9fa 100644 --- a/src/model/struct_factory.cpp +++ b/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()); } void struct_factory::register_value(expr * new_value) { sort * s = new_value->get_sort(); - value_set * set = get_value_set(s); - if (!set->contains(new_value)) { - m_values.push_back(new_value); - set->insert(new_value); + auto& [set, values] = get_value_set(s); + if (!set.contains(new_value)) { + values.push_back(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); - switch (set->size()) { + auto& [set, values] = get_value_set(s); + 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::iterator it = set->begin(); + obj_hashtable::iterator it = set.begin(); v1 = *it; ++it; v2 = *it; diff --git a/src/model/struct_factory.h b/src/model/struct_factory.h index f8235a89b..1ac90ffe8 100644 --- a/src/model/struct_factory.h +++ b/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 value_set; - typedef obj_map sort2value_set; + struct value_set { + obj_hashtable set; + expr_ref_vector values; + value_set(ast_manager &m) : values(m) {} + }; + using sort2value_set = obj_map; model_core & m_model; sort2value_set m_sort2value_set; - expr_ref_vector m_values; sort_ref_vector m_sorts; - ptr_vector m_sets; + scoped_ptr_vector 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); diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index f485079de..cef570b78 100644 --- a/src/smt/theory_finite_set.cpp +++ b/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"