diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 028231fba..b91e4af3a 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -173,11 +173,8 @@ void finite_set_decl_plugin::get_sort_names(svector& sort_names, s expr * finite_set_decl_plugin::get_some_value(sort * s) { if (is_finite_set(s)) { // Return empty set for the given sort - sort* element_sort = get_element_sort(s); - if (element_sort) { - parameter param(element_sort); - return m_manager->mk_app(m_family_id, OP_FINITE_SET_EMPTY, 1, ¶m, 0, nullptr); - } + parameter param(s); + return m_manager->mk_app(m_family_id, OP_FINITE_SET_EMPTY, 1, ¶m, 0, nullptr); } return nullptr; } diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index cef570b78..abfe11503 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -36,6 +36,16 @@ namespace smt { m_axioms.set_add_clause(add_clause_fn); } + theory_finite_set::~theory_finite_set() { + reset_set_members(); + } + + void theory_finite_set::reset_set_members() { + for (auto [k, s] : m_set_members) + dealloc(s); + m_set_members.reset(); + } + /** * Boolean atomic formulas for finite sets are one of: * (set.in x S) @@ -108,6 +118,12 @@ namespace smt { return true; } + void theory_finite_set::apply_sort_cnstr(enode* n, sort* s) { + SASSERT(u.is_finite_set(s)); + if (!is_attached_to_var(n)) + ctx.attach_th_var(n, this, mk_var(n)); + } + void theory_finite_set::new_eq_eh(theory_var v1, theory_var v2) { TRACE(finite_set, tout << "new_eq_eh: v" << v1 << " = v" << v2 << "\n";); // When two sets are equal, propagate membership constraints @@ -275,15 +291,78 @@ 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()); + mg.register_factory(m_factory); + collect_members(); } + + + void theory_finite_set::collect_members() { + // This method can be used to collect all elements that are members of sets + // and ensure that the model factory has values for them. + // For now, we rely on the default model construction. + reset_set_members(); + for (auto x : m_elements) { + if (!ctx.is_relevant(x)) + continue; + x = x->get_root(); + // TODO: use marking of x to avoid duplicate work + for (auto p : enode::parents(x)) { + if (!ctx.is_relevant(p)) + continue; + if (!u.is_in(p->get_expr())) + continue; + if (ctx.get_assignment(p->get_expr()) != l_true) + continue; + enode *elem = nullptr, *set = nullptr; + set = p->get_arg(1)->get_root(); + elem = p->get_arg(0)->get_root(); + if (elem != x) + continue; + if (!m_set_members.contains(set)) + m_set_members.insert(set, alloc(obj_hashtable)); + m_set_members.find(set)->insert(x); + } + } + } + + struct finite_set_value_proc : model_value_proc { + finite_set_util& u; + 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) {} + + void get_dependencies(buffer &result) override { + if (!m_elements) + return; + for (auto v : *m_elements) + result.push_back(model_value_dependency(v)); + } + + 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); + 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; + } + }; + model_value_proc * theory_finite_set::mk_value(enode * n, model_generator & mg) { - TRACE(finite_set, tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";); - - // For now, return nullptr to use default model construction - // A complete implementation would construct explicit set values - // based on true membership literals - return nullptr; + TRACE(finite_set, tout << "mk_value: " << mk_pp(n->get_expr(), m) << "\n";); + 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); } /** diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 3ac6acff5..d017bb416 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -90,6 +90,7 @@ 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" namespace smt { class theory_finite_set : public theory { @@ -99,6 +100,8 @@ namespace smt { 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; + obj_map *> m_set_members; protected: // Override relevant methods from smt::theory @@ -106,6 +109,7 @@ namespace smt { bool internalize_term(app * term) override; void new_eq_eh(theory_var v1, theory_var v2) override; void new_diseq_eh(theory_var v1, theory_var v2) override; + void apply_sort_cnstr(enode *n, sort *s) override; final_check_status final_check_eh() override; theory * mk_fresh(context * new_ctx) override; @@ -125,10 +129,14 @@ namespace smt { void add_immediate_axioms(app *atom); bool add_membership_axioms(); bool add_extensionality_axioms(); + + // model construction + void collect_members(); + void reset_set_members(); public: theory_finite_set(context& ctx); - ~theory_finite_set() override {} + ~theory_finite_set() override; }; } // namespace smt