pub fn normalize(clauses: &CanonClauses) -> (CanonClauses, Vec<(u32, u32)>)Expand description
Deterministic name-normalization: rename variables by first appearance over the sorted clause list, iterated to a fixpoint of (rename, sort). Returns the normalized set and the renaming.