diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp index 0d322b683..bb49ff18e 100644 --- a/src/ast/finite_set_decl_plugin.cpp +++ b/src/ast/finite_set_decl_plugin.cpp @@ -40,6 +40,7 @@ finite_set_decl_plugin::finite_set_decl_plugin(): m_names[OP_FINITE_SET_RANGE] = "set.range"; m_names[OP_FINITE_SET_EXT] = "set.diff"; m_names[OP_FINITE_SET_MAP_INVERSE] = "set.map.inverse"; + m_names[OP_FINITE_SET_UNIQUE_SET] = "set.unique"; } finite_set_decl_plugin::~finite_set_decl_plugin() { @@ -87,6 +88,7 @@ void finite_set_decl_plugin::init() { m_sigs[OP_FINITE_SET_RANGE] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_RANGE], 0, 2, intintT, setInt); m_sigs[OP_FINITE_SET_EXT] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_EXT], 1, 2, setAsetA, A); m_sigs[OP_FINITE_SET_MAP_INVERSE] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_MAP_INVERSE], 2, 3, arrABBsetA, A); + m_sigs[OP_FINITE_SET_UNIQUE_SET] = alloc(polymorphism::psig, m, m_names[OP_FINITE_SET_UNIQUE_SET], 1, 2, intintT, setA); } sort * finite_set_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { @@ -183,6 +185,15 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param range = to_sort(parameters[0].get_ast()); } return mk_empty(range); + case OP_FINITE_SET_UNIQUE_SET: + if (!range) { + if ((num_parameters != 1 || !parameters[0].is_ast() || !is_sort(parameters[0].get_ast()))) { + m_manager->raise_exception("set.unique requires one sort parameter"); + return nullptr; + } + range = to_sort(parameters[0].get_ast()); + } + return mk_finite_set_op(k, arity, domain, range); case OP_FINITE_SET_UNION: case OP_FINITE_SET_INTERSECT: return mk_finite_set_op(k, 2, domain, range); @@ -204,7 +215,7 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param void finite_set_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { for (unsigned i = 0; i < m_names.size(); ++i) - if (m_names[i]) + if (m_names[i] && i != OP_FINITE_SET_UNIQUE_SET) op_names.push_back(builtin_name(std::string(m_names[i]), i)); } @@ -326,3 +337,9 @@ func_decl *finite_set_util::mk_range_decl() { return m_manager.mk_func_decl(m_fid, OP_FINITE_SET_RANGE, 0, nullptr, 2, domain, nullptr); } +app* finite_set_util::mk_unique_set(expr* index, expr* cardinality, sort* s) { + parameter params[1] = { parameter(s) }; + expr *args[2] = {index, cardinality}; + return m_manager.mk_app(m_fid, OP_FINITE_SET_UNIQUE_SET, 1, params, 2, args); +} + diff --git a/src/ast/finite_set_decl_plugin.h b/src/ast/finite_set_decl_plugin.h index df851472e..ec927dfa9 100644 --- a/src/ast/finite_set_decl_plugin.h +++ b/src/ast/finite_set_decl_plugin.h @@ -49,6 +49,7 @@ enum finite_set_op_kind { OP_FINITE_SET_RANGE, OP_FINITE_SET_EXT, OP_FINITE_SET_MAP_INVERSE, + OP_FINITE_SET_UNIQUE_SET, LAST_FINITE_SET_OP }; @@ -134,6 +135,7 @@ public: bool is_map(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_MAP); } bool is_filter(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_FILTER); } bool is_range(expr const* n) const { return is_app_of(n, m_fid, OP_FINITE_SET_RANGE); } + bool is_unique_set(expr const *n) const { return is_app_of(n, m_fid, OP_FINITE_SET_UNIQUE_SET); } MATCH_UNARY(is_singleton); MATCH_UNARY(is_size); @@ -145,6 +147,7 @@ public: MATCH_BINARY(is_map); MATCH_BINARY(is_filter); MATCH_BINARY(is_range); + MATCH_BINARY(is_unique_set); }; class finite_set_util : public finite_set_recognizers { @@ -211,7 +214,9 @@ public: func_decl *mk_range_decl(); - app * mk_range(expr* low, expr* high) { + app *mk_range(expr *low, expr *high) { return m_manager.mk_app(m_fid, OP_FINITE_SET_RANGE, low, high); } + + app *mk_unique_set(expr *s1, expr *s2, sort *s); }; diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 14208074e..47898a7b2 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -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* m_elements = nullptr; @@ -792,9 +794,14 @@ namespace smt { } finite_set_value_proc(theory_finite_set &th, enode *n, obj_map *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 &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*elements = nullptr; n = n->get_root(); m_set_members.find(n, elements); diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 212068385..6ba1cc4c7 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -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); diff --git a/src/smt/theory_finite_set_size.cpp b/src/smt/theory_finite_set_size.cpp index 2dba543a0..0eb27edf2 100644 --- a/src/smt/theory_finite_set_size.cpp +++ b/src/smt/theory_finite_set_size.cpp @@ -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 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 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 { diff --git a/src/smt/theory_finite_set_size.h b/src/smt/theory_finite_set_size.h index 9e2f7497c..2be7f1f0d 100644 --- a/src/smt/theory_finite_set_size.h +++ b/src/smt/theory_finite_set_size.h @@ -50,6 +50,10 @@ namespace smt { obj_map n2b; obj_map m_assumptions; expr_ref m_assumption; + expr_ref_vector m_slacks; + vector> m_slack_members; + obj_map 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; + } }; } \ No newline at end of file