mirror of
https://github.com/Z3Prover/z3
synced 2026-06-02 15:17:54 +00:00
add functions that create unique sets for model construction based on solving cardinality constraints
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
parent
1d3f6a7c70
commit
ba13460511
6 changed files with 108 additions and 23 deletions
|
|
@ -699,6 +699,7 @@ namespace smt {
|
|||
m_factory = alloc(finite_set_factory, m, u.get_family_id(), mg.get_model());
|
||||
mg.register_factory(m_factory);
|
||||
collect_members();
|
||||
m_cardinality_solver.init_model(mg);
|
||||
}
|
||||
|
||||
void theory_finite_set::collect_members() {
|
||||
|
|
@ -776,6 +777,7 @@ namespace smt {
|
|||
|
||||
struct finite_set_value_proc : model_value_proc {
|
||||
theory_finite_set &th;
|
||||
app_ref m_unique_value;
|
||||
enode *n = nullptr;
|
||||
obj_map<enode, bool>* m_elements = nullptr;
|
||||
|
||||
|
|
@ -792,9 +794,14 @@ namespace smt {
|
|||
}
|
||||
|
||||
finite_set_value_proc(theory_finite_set &th, enode *n, obj_map<enode, bool> *elements)
|
||||
: th(th), n(n), m_elements(elements) {}
|
||||
: th(th), m_unique_value(th.m), n(n), m_elements(elements) {}
|
||||
|
||||
finite_set_value_proc(theory_finite_set &th, app* value)
|
||||
: th(th), m_unique_value(value, th.m) {}
|
||||
|
||||
void get_dependencies(buffer<model_value_dependency> &result) override {
|
||||
if (m_unique_value)
|
||||
return;
|
||||
if (!m_elements)
|
||||
return;
|
||||
bool ur = use_range();
|
||||
|
|
@ -804,6 +811,8 @@ namespace smt {
|
|||
}
|
||||
|
||||
app *mk_value(model_generator &mg, expr_ref_vector const &values) override {
|
||||
if (m_unique_value)
|
||||
return m_unique_value;
|
||||
auto s = n->get_sort();
|
||||
if (values.empty())
|
||||
return th.u.mk_empty(s);
|
||||
|
|
@ -849,6 +858,9 @@ namespace smt {
|
|||
|
||||
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";);
|
||||
app *value = m_cardinality_solver.get_unique_value(n->get_expr());
|
||||
if (value)
|
||||
return alloc(finite_set_value_proc, *this, value);
|
||||
obj_map<enode, bool>*elements = nullptr;
|
||||
n = n->get_root();
|
||||
m_set_members.find(n, elements);
|
||||
|
|
|
|||
|
|
@ -169,14 +169,6 @@ namespace smt {
|
|||
void collect_statistics(::statistics & st) const override {
|
||||
m_stats.collect_statistics(st);
|
||||
}
|
||||
void add_theory_assumptions(expr_ref_vector& assumptions) override {
|
||||
m_cardinality_solver.add_theory_assumptions(assumptions);
|
||||
}
|
||||
|
||||
bool should_research(expr_ref_vector& unsat_core) override {
|
||||
return m_cardinality_solver.should_research(unsat_core);
|
||||
}
|
||||
|
||||
|
||||
void add_in_axioms(theory_var v1, theory_var v2);
|
||||
void add_in_axioms(enode *in, var_data *d);
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ Abstract:
|
|||
namespace smt {
|
||||
|
||||
theory_finite_set_size::theory_finite_set_size(theory_finite_set& th):
|
||||
m(th.m), ctx(th.ctx), th(th), u(m), bs(m), m_assumption(m) {}
|
||||
m(th.m), ctx(th.ctx), th(th), u(m), bs(m), m_assumption(m), m_slacks(m), m_pinned(m) {}
|
||||
|
||||
void theory_finite_set_size::add_set_size(func_decl* f) {
|
||||
if (!m_set_size_decls.contains(f)) {
|
||||
|
|
@ -42,6 +42,10 @@ namespace smt {
|
|||
s.n2b.reset();
|
||||
s.m_assumptions.reset();
|
||||
s.bs.reset();
|
||||
s.m_slacks.reset();
|
||||
s.m_slack_members.reset();
|
||||
s.m_pinned.reset();
|
||||
s.m_unique_values.reset();
|
||||
}
|
||||
};
|
||||
ctx.push_trail(clear_solver(*this));
|
||||
|
|
@ -310,6 +314,8 @@ namespace smt {
|
|||
for (auto [k, v] : m_assumptions)
|
||||
asms.push_back(k);
|
||||
|
||||
m_slacks.reset();
|
||||
m_slack_members.reset();
|
||||
expr_ref_vector slack_exprs(m);
|
||||
obj_map<expr, expr *> slack_sums;
|
||||
arith_util a(m);
|
||||
|
|
@ -365,6 +371,7 @@ namespace smt {
|
|||
model_ref mdl;
|
||||
m_solver->get_model(mdl);
|
||||
|
||||
|
||||
expr_ref_vector props(m);
|
||||
for (auto f : m_set_size_decls) {
|
||||
for (auto n : ctx.enodes_of(f)) {
|
||||
|
|
@ -380,6 +387,14 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
}
|
||||
m_slacks.push_back(slack);
|
||||
ptr_vector<expr> members;
|
||||
for (auto [n, b] : n2b) {
|
||||
expr *e = n->get_expr();
|
||||
if (is_uninterp_const(e) && mdl->is_true(b))
|
||||
members.push_back(e);
|
||||
}
|
||||
m_slack_members.push_back(members);
|
||||
TRACE(finite_set, tout << *mdl << "\nPropositional model:\n" << props << "\n");
|
||||
m_solver->assert_expr(m.mk_not(m.mk_and(props)));
|
||||
}
|
||||
|
|
@ -406,15 +421,53 @@ namespace smt {
|
|||
return l_true;
|
||||
}
|
||||
|
||||
/**
|
||||
* Placeholder to introduce an assumption literal to manage incremental search for solutions
|
||||
*/
|
||||
void theory_finite_set_size::add_theory_assumptions(expr_ref_vector &assumptions) {
|
||||
|
||||
}
|
||||
|
||||
bool theory_finite_set_size::should_research(expr_ref_vector& unsat_core) {
|
||||
return false;
|
||||
//
|
||||
// construct model based on set variables that have cardinality constraints
|
||||
// In this case the model construction is not explicit. It uses unique sets
|
||||
// to represent sets of given cardinality.
|
||||
//
|
||||
void theory_finite_set_size::init_model(model_generator &mg) {
|
||||
if (!m_solver || !m_solver_ran)
|
||||
return;
|
||||
TRACE(finite_set, tout << "Constructing model for finite set cardinalities\n";);
|
||||
//
|
||||
// construct model based on set variables that have cardinality constraints
|
||||
// slack -> (set variable x truth assignment)*
|
||||
// slack -> integer assignment from arithmetic solver
|
||||
// u.mk_unique_set(unique_index, slack_value, type);
|
||||
// add to model of set variables that are true for slack.
|
||||
//
|
||||
arith_value av(m);
|
||||
av.init(&ctx);
|
||||
rational value;
|
||||
arith_util a(m);
|
||||
SASSERT(m_slacks.size() == m_slack_members.size());
|
||||
unsigned unique_index = 0;
|
||||
for (unsigned i = 0; i < m_slacks.size(); ++i) {
|
||||
auto s = m_slacks.get(i);
|
||||
//
|
||||
// slack s is equivalent to some integer value
|
||||
// create a unique set corresponding to this slack value.
|
||||
// The signature of the unique set is given by the sets that are
|
||||
// satisfiable in the propositional assignment where the slack variable
|
||||
// was introduced.
|
||||
//
|
||||
if (av.get_value_equiv(s, value)) {
|
||||
if (value == 0)
|
||||
continue;
|
||||
if (m_slack_members[i].empty())
|
||||
continue;
|
||||
|
||||
++unique_index;
|
||||
for (auto e : m_slack_members[i]) {
|
||||
app *unique_value = u.mk_unique_set(a.mk_int(unique_index), a.mk_int(value), e->get_sort());
|
||||
if (m_unique_values.contains(e))
|
||||
unique_value = u.mk_union(m_unique_values[e], unique_value);
|
||||
m_unique_values.insert(e, unique_value);
|
||||
m_pinned.push_back(unique_value);
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
std::ostream& theory_finite_set_size::display(std::ostream& out) const {
|
||||
|
|
|
|||
|
|
@ -50,6 +50,10 @@ namespace smt {
|
|||
obj_map<enode, expr *> n2b;
|
||||
obj_map<expr, tracking_literal> m_assumptions;
|
||||
expr_ref m_assumption;
|
||||
expr_ref_vector m_slacks;
|
||||
vector<ptr_vector<expr>> m_slack_members;
|
||||
obj_map<expr, app *> m_unique_values;
|
||||
app_ref_vector m_pinned;
|
||||
|
||||
void collect_subexpressions(enode_vector& ns);
|
||||
void add_def_axioms(enode_vector const &ns);
|
||||
|
|
@ -65,9 +69,11 @@ namespace smt {
|
|||
public:
|
||||
theory_finite_set_size(theory_finite_set &th);
|
||||
void add_set_size(func_decl *f);
|
||||
void add_theory_assumptions(expr_ref_vector &assumptions);
|
||||
bool should_research(expr_ref_vector &unsat_core);
|
||||
lbool final_check();
|
||||
std::ostream &display(std::ostream &out) const;
|
||||
void init_model(model_generator &mg);
|
||||
app *get_unique_value(expr *n) {
|
||||
return m_unique_values.contains(n) ? m_unique_values[n] : nullptr;
|
||||
}
|
||||
};
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue