diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index c0fa954ff..84f2e9c1b 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -3356,8 +3356,8 @@ proof * ast_manager::mk_th_lemma( } pr = mk_app(get_family_name(tid), args.size(), args.data(), mk_proof_sort()); args.reset(); - args.push_back(pr.get()); args.append(num_proofs, (expr**) proofs); + args.push_back(pr.get()); args.push_back(fact); return mk_app(basic_family_id, PR_TH_LEMMA, parameters.size(), parameters.data(), args.size(), args.data()); } diff --git a/src/ast/ast.h b/src/ast/ast.h index 9dd564206..b9562c5e4 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2328,7 +2328,7 @@ public: unsigned get_num_parents(proof const * p) const { SASSERT(is_proof(p)); unsigned n = p->get_num_args(); - return !has_fact(p) ? n : n - 1; + return p->get_decl()->get_decl_kind() == PR_TH_LEMMA ? n - 2 : !has_fact(p) ? n : n - 1; } proof * get_parent(proof const * p, unsigned idx) const { SASSERT(is_proof(p)); return to_app(p->get_arg(idx)); } proof * mk_true_proof(); diff --git a/src/ast/rewriter/finite_set_axioms.h b/src/ast/rewriter/finite_set_axioms.h index e9d304b41..c7f4d18c7 100644 --- a/src/ast/rewriter/finite_set_axioms.h +++ b/src/ast/rewriter/finite_set_axioms.h @@ -12,6 +12,7 @@ Abstract: --*/ +#pragma once #include "ast/rewriter/th_rewriter.h" struct theory_axiom { diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt index 6d0e86b77..a3732f7f6 100644 --- a/src/smt/CMakeLists.txt +++ b/src/smt/CMakeLists.txt @@ -58,6 +58,7 @@ z3_add_component(smt theory_datatype.cpp theory_dense_diff_logic.cpp theory_finite_set.cpp + theory_finite_set_size.cpp theory_diff_logic.cpp theory_dl.cpp theory_dummy.cpp diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp index 205733907..1900620aa 100644 --- a/src/smt/theory_finite_set.cpp +++ b/src/smt/theory_finite_set.cpp @@ -27,7 +27,8 @@ namespace smt { theory_finite_set::theory_finite_set(context& ctx): theory(ctx, ctx.get_manager().mk_family_id("finite_set")), u(m), - m_axioms(m), m_find(*this) + m_axioms(m), m_find(*this), + m_cardinality_solver(*this) { // Setup the add_clause callback for axioms std::function add_clause_fn = @@ -108,6 +109,10 @@ namespace smt { } else if (u.is_range(e)) { + } + else if (u.is_size(e)) { + auto f = to_app(e)->get_decl(); + m_cardinality_solver.add_set_size(f); } return r; } @@ -246,7 +251,13 @@ namespace smt { 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";); - m_find.merge(v1, v2); // triggers merge_eh, which triggers incremental generation of theory axioms + auto n1 = get_enode(v1); + auto n2 = get_enode(v2); + if (u.is_finite_set(n1->get_expr()) && u.is_finite_set(n2->get_expr())) { + m_eqs.push_back({v1, v2}); + ctx.push_trail(push_back_vector(m_eqs)); + m_find.merge(v1, v2); // triggers merge_eh, which triggers incremental generation of theory axioms + } } /** @@ -266,6 +277,8 @@ namespace smt { return; if (are_forced_distinct(n1, n2)) return; + m_diseqs.push_back({v1, v2}); + ctx.push_trail(push_back_vector(m_diseqs)); m_axioms.extensionality_axiom(e1, e2); } } @@ -301,8 +314,41 @@ namespace smt { if (assume_eqs()) return FC_CONTINUE; + + switch (m_cardinality_solver.final_check()) { + case l_true: break; + case l_false: return FC_CONTINUE; + case l_undef: return FC_GIVEUP; + } - return FC_DONE; + return is_fully_solved() ? FC_DONE : FC_GIVEUP; + } + + /** + * Determine if the constraints are fully solved. + * They can be fully solved if: + * - the model that is going to be produced satisfies all constraints + * The model will always satisfy the constraints if: + * - there is no occurrence of set.map + * - there is not both set.size and set.filter + */ + bool theory_finite_set::is_fully_solved() { + bool has_map = false, has_filter = false, has_size = false; + for (unsigned v = 0; v < get_num_vars(); ++v) { + auto n = get_enode(v); + auto e = n->get_expr(); + if (u.is_filter(e)) + has_filter = true; + if (u.is_map(e)) + has_map = true; + if (u.is_size(e)) + has_size = true; + } + if (has_map) + return false; // todo use more expensive model check here + if (has_filter && has_size) + return false; // tood use more expensive model check here + return true; } diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h index 65928ac76..713b3095f 100644 --- a/src/smt/theory_finite_set.h +++ b/src/smt/theory_finite_set.h @@ -75,12 +75,6 @@ When introducing select and map, decidability can be lost. For Boolean lattice constraints given by equality, subset, strict subset and union, intersections, the theory solver uses a stand-alone satisfiability checker for Boolean algebras to close branches. -Instructions for copilot: - -1. Override relevant methods for smt::theory. Add them to the signature and add stubs or implementations in -theory_finite_set.cpp. -2. In final_check_eh add instantiation of theory axioms following the outline in the inference rules above. - An example of how to instantiate axioms is in theory_arrays_base.cpp and theroy_datatypes.cpp and other theory files. --*/ #pragma once @@ -92,12 +86,16 @@ theory_finite_set.cpp. #include "util/obj_pair_hashtable.h" #include "util/union_find.h" #include "smt/smt_theory.h" +#include "smt/theory_finite_set_size.h" #include "model/finite_set_factory.h" namespace smt { + class context; + class theory_finite_set : public theory { using th_union_find = union_find; friend class theory_finite_set_test; + friend class theory_finite_set_size; friend struct finite_set_value_proc; struct var_data { @@ -135,18 +133,16 @@ namespace smt { } }; - struct range { - rational lo, hi; - }; - finite_set_util u; finite_set_axioms m_axioms; th_union_find m_find; theory_clauses m_clauses; + theory_finite_set_size m_cardinality_solver; finite_set_factory *m_factory = nullptr; obj_map *> m_set_members; ptr_vector m_set_in_decls; ptr_vector m_var_data; + svector> m_diseqs, m_eqs; stats m_stats; protected: @@ -172,6 +168,13 @@ 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); @@ -189,6 +192,7 @@ namespace smt { bool assume_eqs(); bool is_new_axiom(expr *a, expr *b); app *mk_union(unsigned num_elems, expr *const *elems, sort* set_sort); + bool is_fully_solved(); // model construction void collect_members(); diff --git a/src/smt/theory_finite_set_size.cpp b/src/smt/theory_finite_set_size.cpp new file mode 100644 index 000000000..d1071bc1f --- /dev/null +++ b/src/smt/theory_finite_set_size.cpp @@ -0,0 +1,412 @@ + +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + theory_finite_set_size.cpp + +Abstract: + + Theory solver for finite sets. + Implements axiom schemas for finite set operations. + +--*/ + +#include "smt/theory_finite_set.h" +#include "smt/theory_finite_set_size.h" +#include "smt/smt_context.h" +#include "smt/smt_model_generator.h" +#include "smt/smt_arith_value.h" +#include "ast/ast_pp.h" + +namespace smt { + + theory_finite_set_size::theory_finite_set_size(theory_finite_set& th): + m(th.m), ctx(th.ctx), th(th), u(m), m_assumption(m) {} + + void theory_finite_set_size::add_set_size(func_decl* f) { + if (!m_set_size_decls.contains(f)) { + m_set_size_decls.push_back(f); + ctx.push_trail(push_back_trail(m_set_size_decls)); + } + } + + void theory_finite_set_size::initialize_solver() { + struct clear_solver : public trail { + theory_finite_set_size &s; + public: + clear_solver(theory_finite_set_size &s) : s(s) {} + void undo() override { + s.m_solver = nullptr; + s.n2b.reset(); + s.m_assumptions.reset(); + } + }; + ctx.push_trail(clear_solver(*this)); + m_solver = alloc(context, m, ctx.get_fparams(), ctx.get_params()); + // collect all expressons that use cardinality constraints + // collect cone of influence of sets terminals used in cardinality constraints + // for every visited uninterpreted set variable add a Boolean variable + // for every visited set expression add definitions as constraints to m_cardinality solver + // introduce fresh variables for set membership constraints + // assume that distinct enodes in set memberships produce different sets + // assert added disequalities + // assert equalities based on union-find equalities + // assert set membership constraints by in + + enode_vector ns; + collect_subexpressions(ns); + create_singleton_sets_from_membership(ns); + // + // we now got all subexpressions from equalities, disequalities, set.in + // + // associate a Boolean variable with every set enode + expr_ref_vector bs(m); + for (auto n : ns) { + std::ostringstream strm; + strm << enode_pp(n, ctx); + symbol name = symbol(strm.str()); + expr_ref b(m.mk_const(name, m.mk_bool_sort()), m); + bs.push_back(b); + n2b.insert(n, b); + } + + add_def_axioms(ns); + add_singleton_axioms(ns); // (set.in x s) -> |{x}| = 1 + add_diseq_axioms(ns); // |x\y| > 0 or |y\x| > 0 + add_eq_axioms(ns); + + TRACE(finite_set, display(tout)); + } + + /** + * For every (supported) set expression ensure associated Boolean expressions follow semantics + */ + void theory_finite_set_size::add_def_axioms(enode_vector const& ns) { + for (auto n : ns) { + expr *e = n->get_expr(); + if (u.is_union(e)) { + auto a = n2b[n->get_arg(0)]; + auto b = n2b[n->get_arg(1)]; + m_solver->assert_expr(m.mk_iff(n2b[n], m.mk_or(a, b))); + } + else if (u.is_intersect(e)) { + auto a = n2b[n->get_arg(0)]; + auto b = n2b[n->get_arg(1)]; + m_solver->assert_expr(m.mk_iff(n2b[n], m.mk_and(a, b))); + } + else if (u.is_difference(e)) { + auto a = n2b[n->get_arg(0)]; + auto not_b = m.mk_not(n2b[n->get_arg(1)]); + m_solver->assert_expr(m.mk_iff(n2b[n], m.mk_and(a, not_b))); + } + } + } + + enode* theory_finite_set_size::mk_singleton(enode* n) { + expr_ref s(u.mk_singleton(n->get_expr()), m); + ctx.ensure_internalized(s); + ctx.mark_as_relevant(s.get()); + return ctx.get_enode(s); + } + + enode* theory_finite_set_size::mk_diff(enode* a, enode* b) { + expr_ref d(u.mk_difference(a->get_expr(), b->get_expr()), m); + ctx.ensure_internalized(d); + ctx.mark_as_relevant(d.get()); + return ctx.get_enode(d); + } + + /** + * For every set membership (set.in x s) add axiom for (set.subset (set.singleton x) s) + */ + + void theory_finite_set_size::add_singleton_axioms(enode_vector const &ns) { + for (auto n : ns) { + for (auto p : enode::parents(n)) { + if (!u.is_in(p->get_expr())) + continue; + if (!ctx.is_relevant(p)) + continue; + auto v = ctx.get_assignment(p); + if (v == l_undef) + continue; + auto e = p->get_arg(0)->get_root(); + auto s = mk_singleton(e); + SASSERT(n2b.contains(e)); + SASSERT(n2b.contains(s)); + auto is_in = m.mk_implies(n2b[s], n2b[p->get_arg(1)]); + if (v == l_false) + is_in = m.mk_not(is_in); + in lit(p, v == l_true); + expr* b = m.mk_const(symbol("set.in"), m.mk_bool_sort()); + m_assumptions.insert(b, lit); + m_solver->assert_expr(is_in); + } + } + } + + /** + * For every asserted equality ensure equivalence + */ + void theory_finite_set_size::add_eq_axioms(enode_vector const &ns) { + for (auto [a, b] : th.m_eqs) { + auto x = th.get_enode(a); + auto y = th.get_enode(b); + if (n2b.contains(x) && n2b.contains(y)) { + eq e = {a, b}; + auto t = m.mk_const(symbol("eq"), m.mk_bool_sort()); + m_assumptions.insert(t, e); + m_solver->assert_expr(m.mk_implies(t, m.mk_iff(n2b[x], n2b[y]))); + } + } + } + + /* + * For every disequality include the assertions x = y or |x\y| >= 1 or |y\z| >= 1 + * The expressions x\y and y\x are created when ns is created. + */ + void theory_finite_set_size::add_diseq_axioms(enode_vector const &ns) { + for (auto [a, b] : th.m_diseqs) { + auto x = th.get_enode(a); + auto y = th.get_enode(b); + if (n2b.contains(x) && n2b.contains(y)) { + diseq d = {a, b}; + auto b = m.mk_const(symbol("!="), m.mk_bool_sort()); + m_assumptions.insert(b, d); + m_solver->assert_expr(m.mk_implies(b, m.mk_not(m.mk_iff(n2b[x], n2b[y])))); + arith_util a(m); + auto d1 = mk_diff(x, y); + auto d2 = mk_diff(y, x); + expr_ref sz1(u.mk_size(d1->get_expr()), m); + expr_ref sz2(u.mk_size(d2->get_expr()), m); + literal l_eq = th.mk_literal(m.mk_eq(x->get_expr(), y->get_expr())); + literal l1 = th.mk_literal(a.mk_ge(sz1, a.mk_int(1))); + literal l2 = th.mk_literal(a.mk_ge(sz2, a.mk_int(1))); + ctx.mk_th_axiom(th.get_id(), l_eq, l1, l2); + } + } + } + + /** + * Walk the cone of influence of expresions that depend on ns + */ + void theory_finite_set_size::collect_subexpressions(enode_vector& ns) { + + // initialize disequality watch list + u_map v2diseqs, v2eqs; + for (auto [a, b] : th.m_diseqs) { + v2diseqs.insert_if_not_there(a, unsigned_vector()).push_back(b); + v2diseqs.insert_if_not_there(b, unsigned_vector()).push_back(a); + } + for (auto [a, b] : th.m_eqs) { + v2eqs.insert_if_not_there(a, unsigned_vector()).push_back(b); + v2eqs.insert_if_not_there(b, unsigned_vector()).push_back(a); + } + + auto add_expression = [&](enode *e) { + if (!ctx.is_relevant(e)) + return; + if (e->is_marked()) + return; + e->set_mark(); + ns.push_back(e); + }; + + auto is_setop = [&](enode *n) { + auto e = n->get_expr(); + return u.is_union(e) || u.is_intersect(e) || u.is_difference(e); + }; + + for (auto f : m_set_size_decls) { + for (auto n : ctx.enodes_of(f)) { + SASSERT(u.is_size(n->get_expr())); + add_expression(n->get_arg(0)); + } + } + for (unsigned i = 0; i < ns.size(); ++i) { + auto n = ns[i]; + // add children under set operations + if (is_setop(n)) + for (auto arg : enode::args(n)) + add_expression(arg); + // add parents that are operations and use n + for (auto p : enode::parents(n)) + if (is_setop(p) && any_of(enode::args(p), [n](auto a){ + return a == n;})) + add_expression(p); + // add equalities and disequalities + auto v = th.get_th_var(n); + if (v2eqs.contains(v)) { + auto const &other = v2eqs[v]; + for (auto w : other) + add_expression(th.get_enode(w)); + } + if (v2diseqs.contains(v)) { + auto const &other = v2diseqs[v]; + for (auto w : other) { + auto n2 = th.get_enode(w); + add_expression(n2); + add_expression(mk_diff(n, n2)); + add_expression(mk_diff(n2, n)); + } + } + } + for (auto n : ns) + n->unset_mark(); + } + + void theory_finite_set_size::create_singleton_sets_from_membership(enode_vector& ns) { + unsigned sz = ns.size(); + enode_vector to_unmark; + for (unsigned i = 0; i < sz; ++i) { + auto n = ns[i]; + for (auto p : enode::parents(n)) { + if (!u.is_in(p->get_expr())) + continue; + auto e = p->get_arg(0)->get_root(); + if (e->is_marked()) + continue; + e->set_mark(); + to_unmark.push_back(e); + ns.push_back(mk_singleton(e)); + } + } + for (auto n : to_unmark) + n->unset_mark(); + } + + /** + * Base implementation: + * Enumerate all satisfying assignments to m_solver for atoms based on |s| + * Extract Core from enumeration + * Assert Core => |s_i| = sum_ij n_ij for each |s_i| cardinality expression + * NB. Soundness of using Core has not been rigorously established. + * Incremental algorithm: + * Enumerate N assignments at a time. + * Associate tracking literal C_i with current assignment. + * Assume C_i + * Assert !C_0, .. , !C_{i-1}, C_i => /\_i |s_i| = sum_j n_ij and /\ n_j >= 0 + * Incremental algorithm with blocking clauses (sketch) + * If /\_i |s_i| = sum_j n_ij and /\ n_j >= 0 is unsat + * Then, instead of asserting sum constraint assert + * C_i <=> \/_j core_j + * where core_j come from covering of LRA conflict + */ + lbool theory_finite_set_size::run_solver() { + expr_ref_vector asms(m); + for (auto [k, v] : m_assumptions) + asms.push_back(k); + + expr_ref_vector slack_exprs(m); + obj_map slack_sums; + arith_util a(m); + for (auto f : m_set_size_decls) { + for (auto n : ctx.enodes_of(f)) { + slack_sums.insert(n->get_expr(), a.mk_int(0)); + } + } + + while (true) { + lbool r = m_solver->check(asms.size(), asms.data()); + if (r == l_false) { + auto const& core = m_solver->unsat_core(); + literal_vector lits; + for (auto c : core) { + auto exp = m_assumptions[c]; + if (std::holds_alternative(exp)) { + auto [a, b] = *std::get_if(&exp); + lits.push_back(~th.mk_literal(m.mk_eq(th.get_expr(a), th.get_expr(b)))); + } + else if (std::holds_alternative(exp)) { + auto [a, b] = *std::get_if(&exp); + lits.push_back(th.mk_literal(m.mk_eq(th.get_expr(a), th.get_expr(b)))); + } + else if (std::holds_alternative(exp)) { + auto [n, is_pos] = *std::get_if(&exp); + auto lit = th.mk_literal(n->get_expr()); + lits.push_back(is_pos ? ~lit : lit); + } + } + for (auto f : m_set_size_decls) { + for (auto n : ctx.enodes_of(f)) { + expr_ref eq(m.mk_eq(n->get_expr(), slack_sums[n->get_expr()]), m); + auto lit = th.mk_literal(eq); + literal_vector lemma(lits); + lemma.push_back(lit); + ctx.mk_th_axiom(th.get_id(), lemma); + } + } + ctx.push_trail(value_trail(m_solver_ran)); + TRACE(finite_set, ctx.display(tout)); + m_solver_ran = true; + return l_false; + } + if (r != l_true) + return r; + + expr_ref slack(m.mk_fresh_const(symbol("slack"), a.mk_int()), m); + ctx.mk_th_axiom(th.get_id(), th.mk_literal(a.mk_ge(slack, a.mk_int(0)))); // slack is non-negative + model_ref mdl; + m_solver->get_model(mdl); + TRACE(finite_set, tout << *mdl); + expr_ref_vector props(m); + for (auto f : m_set_size_decls) { + for (auto n : ctx.enodes_of(f)) { + auto arg = n->get_arg(0); + auto b = n2b[arg]; + auto b_is_true = mdl->is_true(b); + props.push_back(b_is_true ? b : m.mk_not(b)); + if (b_is_true) { + auto s = slack_sums[n->get_expr()]; + s = a.mk_add(s, slack); + slack_exprs.push_back(s); + slack_sums.insert(n->get_expr(), s); + } + } + } + m_solver->assert_expr(m.mk_not(m.mk_and(props))); + } + return l_undef; + } + + lbool theory_finite_set_size::final_check() { + if (m_set_size_decls.empty()) + return l_true; + if (!m_solver) { + initialize_solver(); + return l_false; + } + if (!m_solver_ran) + return run_solver(); + + // at this point we assume that + // cardinality constraints are satisfied + // by arithmetic solver. + // + // a refinement checks if this is really necessary + // + return l_true; + } + + /** + * Introduce an assumption literal to manage incremental search for solutions + */ + void theory_finite_set_size::add_theory_assumptions(expr_ref_vector &assumptions) { + if (m_set_size_decls.empty()) + return; + m_assumption = m.mk_fresh_const(symbol("set.size.solver"), m.mk_bool_sort()); + assumptions.push_back(m_assumption); + } + + bool theory_finite_set_size::should_research(expr_ref_vector& unsat_core) { + return unsat_core.contains(m_assumption); + } + + std::ostream& theory_finite_set_size::display(std::ostream& out) { + if (m_solver) + m_solver->display(out); + return out; + } +} // namespace smt \ No newline at end of file diff --git a/src/smt/theory_finite_set_size.h b/src/smt/theory_finite_set_size.h new file mode 100644 index 000000000..bffd55598 --- /dev/null +++ b/src/smt/theory_finite_set_size.h @@ -0,0 +1,73 @@ + +/*++ +Copyright (c) 2025 Microsoft Corporation + +Module Name: + + theory_finite_set_size.h + +Abstract: + + sub-solver for cardinality constraints of finite sets + +--*/ + +#pragma once + +#include "ast/ast.h" +#include "ast/ast_pp.h" +#include "ast/finite_set_decl_plugin.h" +#include "ast/rewriter/finite_set_axioms.h" +#include "util/obj_pair_hashtable.h" +#include "util/union_find.h" +#include "smt/smt_theory.h" +#include "model/finite_set_factory.h" + +namespace smt { + class context; + class theory_finite_set; + + class theory_finite_set_size { + struct diseq { + theory_var x, y; + }; + struct eq { + theory_var x, y; + }; + struct in { + enode *n; + bool is_pos; + }; + using tracking_literal = std::variant; + ast_manager &m; + context &ctx; + theory_finite_set &th; + finite_set_util u; + scoped_ptr m_solver; + bool m_solver_ran = false; + ptr_vector m_set_size_decls; + obj_map n2b; + obj_map m_assumptions; + expr_ref m_assumption; + + void collect_subexpressions(enode_vector& ns); + void create_singleton_sets_from_membership(enode_vector& ns); + void add_def_axioms(enode_vector const &ns); + void add_singleton_axioms(enode_vector const &ns); + void add_eq_axioms(enode_vector const &ns); + void add_diseq_axioms(enode_vector const &ns); + enode *mk_singleton(enode* n); + enode *mk_diff(enode *a, enode *b); + void initialize_solver(); + + lbool run_solver(); + + 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); + }; +} \ No newline at end of file