Function abstract_signature 

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

Symmetry-break any cover to its abstract signature: discover its automorphisms, quotient the rules to orbit-types (clause_orbits), and probe the certified shadows in turn — counting, then parity, then cutting-planes. shadow = None means no shadow recognizes it (it falls through to the general certified CDCL core). A maximally symmetric family collapses to a few rule-types decided by one shadow; an unstructured one spreads across many types with no shadow — but still has a backdoor.