Function count_models_modulo_symmetry 

pub fn count_models_modulo_symmetry(
    num_vars: usize,
    clauses: &[Vec<Lit>],
) -> Option<usize>

The number of essentially-distinct solutions — models counted up to the formula’s symmetry: the orbit count of the solution set (#SAT modulo G). The complete lex-leader keeps exactly one model per orbit, so counting the symmetry-broken formula’s models is the orbit count. None if the symmetry group is too large to enumerate for the complete break. The counting face of symmetry breaking — and, by Burnside, (1/|G|)·Σ_σ #{models fixed by σ}.