mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-29 02:03:49 +00:00
Code Activity

Fix set.size soundness: cardinality lower bound for concrete distinct members (#10246)

Browse source 
`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` ✓ |

<!-- START COPILOT CODING AGENT SUFFIX -->

- Fixes #10232

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nikolaj@cs.stanford.edu>
This commit is contained in:
Copilot 2026-07-27 15:05:49 -07:00 • committed by GitHub
parent 7e3f948c5c
commit d652bd3fc6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 68 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/ast/rewriter/finite_set_axioms.cpp
View file

@ -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);
}
}

59
src/smt/theory_finite_set_size.cpp
View file

@ -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<in>(v))
continue;
auto& in_val = std::get<in>(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
} // namespace smt