def Hex.GraphIso.Nauty.Sparse.splitSingleton {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) : RefineSt n

A singleton splitter: untouched vertices keep their order and touched vertices are written in reverse order, as in HITS[--k].

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.splitNontrivial {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) : RefineSt n

Count only vertices in touched nontrivial cells. Rows of hits are cleared on first touch, without a full vertex scan for each splitter.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.refineWith {n : Nat} (g : Graph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) : RefineSt n

refine_sg, including its shallow distance split and preference for singleton splitters among the first ten active entries.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.Sparse.refine {n : Nat} (g : Graph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : RefineSt n

Standalone refinement with freshly initialized scratch storage.

Equations

• Hex.GraphIso.Nauty.Sparse.refine g level lab ptn active numcells = Hex.GraphIso.Nauty.Sparse.refineWith g level lab ptn active numcells (Hex.GraphIso.Nauty.Sparse.Scratch.fresh n)