mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

adding factory for model initialization

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-10-16 22:43:20 +02:00
parent 9e79fe0a51
commit 981c7d27ea
3 changed files with 96 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/finite_set_decl_plugin.cpp
View file

@ -173,11 +173,8 @@ void finite_set_decl_plugin::get_sort_names(svector<builtin_name>& 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, &param, 0, nullptr);
}
parameter param(s);
return m_manager->mk_app(m_family_id, OP_FINITE_SET_EMPTY, 1, &param, 0, nullptr);
}
return nullptr;
}

89
src/smt/theory_finite_set.cpp
View file

@ -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<enode>));
m_set_members.find(set)->insert(x);
}
}
}
struct finite_set_value_proc : model_value_proc {
finite_set_util& u;
sort *s = nullptr;
obj_hashtable<enode>* m_elements = nullptr;
finite_set_value_proc(finite_set_util& u, sort* s, obj_hashtable<enode>* elements) :
u(u), s(s),
m_elements(elements) {}
void get_dependencies(buffer<model_value_dependency> &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;
obj_hashtable<enode>*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);
}
/**

10
src/smt/theory_finite_set.h
View file

@ -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<enode> m_elements; // set of all 'x' where there is an 'x in S' atom
vector<expr_ref_vector> m_lemmas;
obj_pair_hashtable<expr, expr> m_lemma_exprs;
finite_set_value_factory *m_factory = nullptr;
obj_map<enode, obj_hashtable<enode> *> 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;
@ -126,9 +130,13 @@ namespace smt {
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