From 5169e552fa5a059eaa245b9792d94d11f631be3b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 17 Oct 2025 15:09:12 +0200 Subject: [PATCH] rename finite_set_value_factor to finite_set_factory. Fix type bugs when creating unions of values --- src/model/CMakeLists.txt | 2 +- ...lue_factory.cpp => finite_set_factory.cpp} | 10 ++-- ...t_value_factory.h => finite_set_factory.h} | 4 +- src/model/model.cpp | 4 +- src/smt/theory_finite_set.cpp | 53 +++++++++---------- src/smt/theory_finite_set.h | 10 ++-- 6 files changed, 42 insertions(+), 41 deletions(-) rename src/model/{finite_set_value_factory.cpp => finite_set_factory.cpp} (84%) rename src/model/{finite_set_value_factory.h => finite_set_factory.h} (75%) diff --git a/src/model/CMakeLists.txt b/src/model/CMakeLists.txt index 436a3c69f..12fce27e8 100644 --- a/src/model/CMakeLists.txt +++ b/src/model/CMakeLists.txt @@ -2,7 +2,7 @@ z3_add_component(model SOURCES array_factory.cpp datatype_factory.cpp - finite_set_value_factory.cpp + finite_set_factory.cpp func_interp.cpp model2expr.cpp model_core.cpp diff --git a/src/model/finite_set_value_factory.cpp b/src/model/finite_set_factory.cpp similarity index 84% rename from src/model/finite_set_value_factory.cpp rename to src/model/finite_set_factory.cpp index 54b7555f0..7e263663a 100644 --- a/src/model/finite_set_value_factory.cpp +++ b/src/model/finite_set_factory.cpp @@ -3,22 +3,22 @@ Copyright (c) 2025 Microsoft Corporation Module Name: - finite_set_value_factory.cpp + finite_set_factory.cpp Abstract: Factory for creating finite set values --*/ -#include "model/finite_set_value_factory.h" +#include "model/finite_set_factory.h" #include "model/model_core.h" -finite_set_value_factory::finite_set_value_factory(ast_manager & m, family_id fid, model_core & md): +finite_set_factory::finite_set_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) { +expr * finite_set_factory::get_some_value(sort * s) { // Check if we already have a value for this sort value_set * vset = nullptr; SASSERT(u.is_finite_set(s)); @@ -30,7 +30,7 @@ expr * finite_set_value_factory::get_some_value(sort * s) { /** * create sets {}, {a}, {b}, {a,b}, {c}, {a,c}, {b,c}, {a,b,c}, {d}, ... */ -expr * finite_set_value_factory::get_fresh_value(sort * s) { +expr * finite_set_factory::get_fresh_value(sort * s) { sort* elem_sort = nullptr; VERIFY(u.is_finite_set(s, elem_sort)); diff --git a/src/model/finite_set_value_factory.h b/src/model/finite_set_factory.h similarity index 75% rename from src/model/finite_set_value_factory.h rename to src/model/finite_set_factory.h index 9ae5f462f..d2d73a4b1 100644 --- a/src/model/finite_set_value_factory.h +++ b/src/model/finite_set_factory.h @@ -18,10 +18,10 @@ Abstract: /** \brief Factory for finite set values. */ -class finite_set_value_factory : public struct_factory { +class finite_set_factory : public struct_factory { finite_set_util u; public: - finite_set_value_factory(ast_manager & m, family_id fid, model_core & md); + finite_set_factory(ast_manager & m, family_id fid, model_core & md); expr * get_some_value(sort * s) override; diff --git a/src/model/model.cpp b/src/model/model.cpp index d847ccb88..3b1769ef1 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -40,7 +40,7 @@ Revision History: #include "model/numeral_factory.h" #include "model/fpa_factory.h" #include "model/char_factory.h" -#include "model/finite_set_value_factory.h" +#include "model/finite_set_factory.h" model::model(ast_manager & m): @@ -112,7 +112,7 @@ 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())); - m_factories.register_plugin(alloc(finite_set_value_factory, m, m.get_family_id("finite_set"), *this)); + m_factories.register_plugin(alloc(finite_set_factory, m, m.get_family_id("finite_set"), *this)); //m_factories.register_plugin(alloc(char_factory, m, char_decl_plugin(m).get_family_id()); } family_id fid = s->get_family_id(); diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 13b6617eb..21ca5153b 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -180,7 +180,7 @@ namespace smt { */ void theory_finite_set::add_immediate_axioms(app* term) { expr *elem = nullptr, *set = nullptr; - unsigned sz = m_lemmas.size(); + unsigned sz = m_theory_axioms.size(); if (u.is_in(term, elem, set) && u.is_empty(set)) add_membership_axioms(elem, set); else if (u.is_subset(term)) @@ -189,8 +189,8 @@ namespace smt { m_axioms.in_singleton_axiom(elem, term); // Assert all new lemmas as clauses - for (unsigned i = sz; i < m_lemmas.size(); ++i) - assert_clause(m_lemmas[i]); + for (unsigned i = sz; i < m_theory_axioms.size(); ++i) + assert_clause(m_theory_axioms[i]); } /** @@ -252,9 +252,7 @@ namespace smt { for (auto e : set) elems.push_back(e->get_expr()); std::sort(elems.begin(), elems.end(), [](expr *a, expr *b) { return a->get_id() < b->get_id(); }); - expr* s = nullptr; - for (auto v : elems) - s = s ? u.mk_union(s, v) : v; + expr *s = mk_union(elems.size(), elems.data(), n->get_expr()->get_sort()); trail.push_back(s); enode *n2 = nullptr; if (!set_reprs.find(s, n2)) { @@ -272,6 +270,13 @@ namespace smt { return false; } + app* theory_finite_set::mk_union(unsigned num_elems, expr* const* elems, sort* set_sort) { + app *s = nullptr; + for (unsigned i = 0; i < num_elems; ++i) + s = s ? u.mk_union(s, u.mk_singleton(elems[i])) : u.mk_singleton(elems[i]); + return s ? s : u.mk_empty(set_sort); + } + bool theory_finite_set::is_new_axiom(expr* a, expr* b) { struct insert_obj_pair_table : public trail { @@ -282,10 +287,10 @@ namespace smt { table.erase({a, b}); } }; - if (m_lemma_exprs.contains({a, b})) + if (m_theory_axiom_exprs.contains({a, b})) return false; - m_lemma_exprs.insert({a, b}); - ctx.push_trail(insert_obj_pair_table(m_lemma_exprs, a, b)); + m_theory_axiom_exprs.insert({a, b}); + ctx.push_trail(insert_obj_pair_table(m_theory_axiom_exprs, a, b)); return true; } @@ -328,8 +333,8 @@ namespace smt { void theory_finite_set::add_clause(expr_ref_vector const& clause) { TRACE(finite_set, tout << "add_clause: " << clause << "\n"); - ctx.push_trail(push_back_vector(m_lemmas)); - m_lemmas.push_back(clause); + ctx.push_trail(push_back_vector(m_theory_axioms)); + m_theory_axioms.push_back(clause); } theory * theory_finite_set::mk_fresh(context * new_ctx) { @@ -344,7 +349,7 @@ namespace smt { TRACE(finite_set, tout << "init_model\n";); // Model generation will use default interpretation for sets // The model will be constructed based on the membership literals that are true - m_factory = alloc(finite_set_value_factory, m, u.get_family_id(), mg.get_model()); + m_factory = alloc(finite_set_factory, m, u.get_family_id(), mg.get_model()); mg.register_factory(m_factory); collect_members(); } @@ -379,13 +384,12 @@ namespace smt { } struct finite_set_value_proc : model_value_proc { - finite_set_util& u; + theory_finite_set &th; sort *s = nullptr; obj_hashtable* m_elements = nullptr; - finite_set_value_proc(finite_set_util& u, sort* s, obj_hashtable* elements) : - u(u), s(s), - m_elements(elements) {} + finite_set_value_proc(theory_finite_set &th, sort *s, obj_hashtable *elements) + : th(th), s(s), m_elements(elements) {} void get_dependencies(buffer &result) override { if (!m_elements) @@ -397,14 +401,9 @@ namespace smt { app *mk_value(model_generator &mg, expr_ref_vector const &values) override { SASSERT(values.size() == m_elements->size()); if (values.empty()) - return u.mk_empty(s); + return th.u.mk_empty(s); SASSERT(m_elements); - app *r = nullptr; - for (auto v : values) { - app *e = u.mk_singleton(v); - r = r ? u.mk_union(r, e) : e; - } - return r; + return th.mk_union(values.size(), values.data(), s); } }; @@ -413,7 +412,7 @@ namespace smt { obj_hashtable*elements = nullptr; sort *s = n->get_expr()->get_sort(); m_set_members.find(n->get_root(), elements); - return alloc(finite_set_value_proc, u, s, elements); + return alloc(finite_set_value_proc, *this, s, elements); } /** @@ -423,7 +422,7 @@ namespace smt { * */ bool theory_finite_set::instantiate_false_lemma() { - for (auto const& clause : m_lemmas) { + for (auto const& clause : m_theory_axioms) { bool all_false = all_of(clause, [&](expr *e) { return ctx.find_assignment(e) == l_false; }); if (!all_false) continue; @@ -442,7 +441,7 @@ namespace smt { */ bool theory_finite_set::instantiate_unit_propagation() { bool propagated = false; - for (auto const &clause : m_lemmas) { + for (auto const &clause : m_theory_axioms) { expr *undef = nullptr; bool is_unit_propagating = true; for (auto e : clause) { @@ -473,7 +472,7 @@ namespace smt { * The solver will case split on the unassigned literals to satisfy the lemma. */ bool theory_finite_set::instantiate_free_lemma() { - for (auto const& clause : m_lemmas) { + for (auto const& clause : m_theory_axioms) { if (any_of(clause, [&](expr *e) { return ctx.find_assignment(e) == l_true; })) continue; assert_clause(clause); diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index e32cb507d..419348d4c 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -90,17 +90,18 @@ theory_finite_set.cpp. #include "ast/rewriter/finite_set_axioms.h" #include "util/obj_pair_hashtable.h" #include "smt/smt_theory.h" -#include "model/finite_set_value_factory.h" +#include "model/finite_set_factory.h" namespace smt { class theory_finite_set : public theory { friend class theory_finite_set_test; + friend struct finite_set_value_proc; finite_set_util u; finite_set_axioms m_axioms; obj_hashtable m_elements; // set of all 'x' where there is an 'x in S' atom - vector m_lemmas; - obj_pair_hashtable m_lemma_exprs; - finite_set_value_factory *m_factory = nullptr; + vector m_theory_axioms; + obj_pair_hashtable m_theory_axiom_exprs; + finite_set_factory *m_factory = nullptr; obj_map *> m_set_members; protected: @@ -130,6 +131,7 @@ namespace smt { bool add_membership_axioms(); bool assume_eqs(); bool is_new_axiom(expr *a, expr *b); + app *mk_union(unsigned num_elems, expr *const *elems, sort* set_sort); // model construction void collect_members();