Function models_up_to_symmetry 

pub fn models_up_to_symmetry(
    num_vars: usize,
    clauses: &[Vec<Lit>],
    cap: usize,
) -> SymmetricCount

Enumerate the solution set up to symmetry, and count it exactly. Find a model (via the full arsenal), record it as an orbit representative, then BLOCK its entire symmetry orbit and repeat until unsatisfiable. Because every orbit is removed in one step, the representatives are the essentially- distinct solutions and the exact model count is the sum of the orbit sizes — so an instance with 2^Θ(n) models is counted by enumerating only its (far fewer) orbits. Sound: each representative is a re-checked model, each orbit a genuine set of models (the generators are automorphisms), so the orbits partition the model set. The representative count agrees with Burnside (crate::sym_break::count_models_modulo_symmetry) — two independent routes to the orbit count.