def Hex.GraphIso.Nauty.Sparse.bestcell {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level : Nat) : Nat

bestcell_sg: first nontrivial cell with the greatest number of nontrivial joins. The source includes joins to the cell itself.

Equations

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

def Hex.GraphIso.Nauty.Sparse.targetcell {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) : Nat

Honour a valid hint, otherwise use sparse best-cell selection through the target level and the first nontrivial cell at greater depths.

Equations

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

def Hex.GraphIso.Nauty.Sparse.maketargetcell {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) : Nat × VSet n × Nat

Equations

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

def Hex.GraphIso.Nauty.Sparse.bestcellCached {n : Nat} (g : Graph n) (lab : Array Nat) (scratch : Scratch) : Nat × Scratch

The same joins and tie order as bestcell, reusing the vertex-to-cell indices and endpoints maintained by refinement.

Equations

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

def Hex.GraphIso.Nauty.Sparse.maketargetCached {n : Nat} (g : Graph n) (lab ptn : Array Nat) (level tcLevel : Nat) (hint : Int) (scratch : Scratch) : Nat × VSet n × Nat × Scratch

Use cached partition data only when it describes the current refinement. Empty-active entry and invalidated search states retain the standalone path.

Equations

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