Function fused_parity_cardinality_decide 

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

The fused parity + cardinality decision. When a formula carries BOTH a GF(2) linear substructure (recovered XOR equations via extract_xor) AND an at-most-one cardinality substructure (via recover_at_most_one), decide it with the two live theories reasoning TOGETHER on one trail — Gaussian elimination for the parity, cardinality propagation for the counting — the structural attack on minimal-disagreement parity that neither alone cracks. Returns Some(is_sat), or None when either substructure is absent (so a caller falls through to other routes). Sound: the original clauses are solved (Boolean-complete), the theories return only formula-entailed clauses, and a SAT model is re-checked against the clauses (fail-closed). Uses the stateless crate::xor_engine::XorEngine (not IncXor, whose value-blind trail-sync is unsafe without a backing clausal XOR encoding).