From d652bd3fc63f2c6b50f3053c6e05259169b9c96c Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Mon, 27 Jul 2026 15:05:49 -0700 Subject: [PATCH] Fix set.size soundness: cardinality lower bound for concrete distinct members (#10246) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `set.size` reported `sat` for `(= 1 (set.size (set.union (set.singleton 1) (set.singleton 2))))` — a soundness bug, not just a performance gap. The returned model did not satisfy the constraint. ## Root cause In `theory_finite_set_size::run_solver()`, the cardinality sub-solver enumerates propositional models of the membership structure and sums fresh "slack" variables to represent `set.size`. All slacks were bounded only by `>= 0`, so the arithmetic solver could freely assign `size = 1` even when two distinct concrete members were independently asserted: - **Model M₁** (`{1}` active, `{2}` inactive) — element 1 is a concrete witness → slack must be `≥ 1` - **Model M₂** (`{1}` inactive, `{2}` active) — element 2 is a concrete witness → slack must be `≥ 1` Without this enforcement: `slack₁ = 1, slack₂ = 0` satisfied `size = 1`. With it: `size ≥ 2`. ## Changes - **`src/smt/theory_finite_set_size.cpp`** — In `run_solver()`, after retrieving the propositional model, check if exactly one singleton equivalence class is active *and* a positive `set.in` assertion exists for that element in an active set. If so, assert `slack >= 1` instead of `>= 0`. This is sound: the concrete member witnesses the slot contains at least one element. - **`src/ast/rewriter/finite_set_axioms.cpp`** — Add the missing monotonicity lower bounds for union: ``` |A ∪ B| ≥ |A| and |A ∪ B| ≥ |B| ``` These complement the existing upper bound `|A ∪ B| ≤ |A| + |B|` and let the arithmetic solver derive `|{1} ∪ {2}| ≥ 2` directly from the singleton axiom `|{i}| = 1`. ## Verified cases | Query | Before | After | |---|---|---| | `(= 1 (set.size (set.union (set.singleton 1) (set.singleton 2))))` | `sat` ❌ | `unsat` ✓ | | `(= 2 (set.size (set.union (set.singleton 1) (set.singleton 2))))` | `sat` ✓ | `sat` ✓ | | `set.in 1 s ∧ set.in 2 s ∧ (= 1 (set.size s))` | `sat` ❌ | `unsat` ✓ | | `¬(>= (set.size (set.union ...)) 2)` | `sat` ❌ | `unsat` ✓ | - Fixes #10232 --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: Nikolaj Bjorner --- src/ast/rewriter/finite_set_axioms.cpp | 18 +++++--- src/smt/theory_finite_set_size.cpp | 59 ++++++++++++++++++++++++-- 2 files changed, 68 insertions(+), 9 deletions(-) diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp index 98824a22b1..6af20f873d 100644 --- a/src/ast/rewriter/finite_set_axioms.cpp +++ b/src/ast/rewriter/finite_set_axioms.cpp @@ -345,11 +345,17 @@ void finite_set_axioms::size_ub_axiom(expr *sz) { else if (u.is_empty(e)) add_unit("size", e, m.mk_eq(sz, a.mk_int(0))); else if (u.is_union(e, x, y)) { - { - auto _seq342_0 = u.mk_size(x); - auto _seq342_1 = u.mk_size(y); - ineq = a.mk_le(sz, a.mk_add(_seq342_0, _seq342_1)); - } + // upper bound: |A ∪ B| ≤ |A| + |B| + auto szx = u.mk_size(x); + auto szy = u.mk_size(y); + ineq = a.mk_le(sz, a.mk_add(szx, szy)); + m_rewriter(ineq); + add_unit("size", e, ineq); + // lower bounds: |A ∪ B| ≥ |A| and |A ∪ B| ≥ |B| + ineq = a.mk_le(szx, sz); + m_rewriter(ineq); + add_unit("size", e, ineq); + ineq = a.mk_le(szy, sz); m_rewriter(ineq); add_unit("size", e, ineq); } @@ -421,4 +427,4 @@ void finite_set_axioms::extensionality_axiom(expr *a, expr* b) { // (a != b) => (x in diff_ab != x in diff_ba) add_ternary("extensionality", a, b, a_eq_b, ndiff_in_a, ndiff_in_b); add_ternary("extensionality", a, b, a_eq_b, diff_in_a, diff_in_b); -} \ No newline at end of file +} diff --git a/src/smt/theory_finite_set_size.cpp b/src/smt/theory_finite_set_size.cpp index d9c4a9ddff..f08ea3a606 100644 --- a/src/smt/theory_finite_set_size.cpp +++ b/src/smt/theory_finite_set_size.cpp @@ -365,11 +365,64 @@ namespace smt { 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); + // Determine whether this propositional model has a "definite member": + // an element known to be in some active set, whose singleton is the + // only active singleton. When true, at least one concrete element + // witnesses the pattern, so the slack lower-bound is 1 instead of 0. + // + // Conditions for a definite member: + // (a) Exactly one equivalence class of singletons is active in the model. + // (b) There is a positive membership assertion (set.in e s) where + // - e belongs to that singleton class, and + // - the set s is active in the model. + // + // When multiple distinct singleton classes are simultaneously active the + // pattern requires an element to be in several disjoint singletons at once + // (impossible for distinct concrete values), so we conservatively use lb=0. + + enode *active_elem_root = nullptr; + bool multiple_singleton_classes = false; + for (auto& [en, b] : n2b) { + if (!u.is_singleton(en->get_expr())) + continue; + if (!mdl->is_true(b)) + continue; + auto elem_root = en->get_arg(0)->get_root(); + if (!active_elem_root) { + active_elem_root = elem_root; + } else if (active_elem_root != elem_root) { + multiple_singleton_classes = true; + break; + } + } + + bool has_definite_member = false; + if (!multiple_singleton_classes && active_elem_root) { + for (auto& [k, v] : m_assumptions) { + if (!std::holds_alternative(v)) + continue; + auto& in_val = std::get(v); + if (!in_val.is_pos) + continue; + if (in_val.n->get_arg(0)->get_root() != active_elem_root) + continue; + auto set_en = in_val.n->get_arg(1); + if (!n2b.contains(set_en)) + continue; + if (!mdl->is_true(n2b[set_en])) + continue; + has_definite_member = true; + break; + } + } + + expr_ref slack(m.mk_fresh_const(symbol("slack"), a.mk_int()), m); + int slack_lb = has_definite_member ? 1 : 0; + ctx.mk_th_axiom(th.get_id(), th.mk_literal(a.mk_ge(slack, a.mk_int(slack_lb)))); + expr_ref_vector props(m); for (auto f : m_set_size_decls) { @@ -475,4 +528,4 @@ namespace smt { m_solver->display(out << "set.size-solver\n"); return out; } -} // namespace smt \ No newline at end of file +} // namespace smt