@[irreducible]

def Hex.GraphIso.Nauty.node {n : Nat} (first : Bool) (ctx : Ctx n) (inf tcLevel fuel level numcells : Nat) (st : Search n) : Exit × Search n

Refine a node, classify it, and sweep its surviving children. Only the leftmost child of a first-path node remains on the first path.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.node first ctx inf tcLevel 0 level numcells st = (Hex.GraphIso.Nauty.Generic.Exit.fuel, st)

@[irreducible]

def Hex.GraphIso.Nauty.sweep {n : Nat} (first : Bool) (ctx : Ctx n) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (tv? : Option Nat) (tcell : VSet n) (index : Nat) (st : Search n) : Exit × Nat × Search n

Visit remaining target vertices in order, rereading the cell after each prune. The orbit index includes skipped vertices on the first path. Nodes return an unwind or fuel, so the done arm after a child is unreachable.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 none tcell index st = (Hex.GraphIso.Nauty.Generic.Exit.done, index, st)
• Hex.GraphIso.Nauty.sweep first ctx inf tcLevel fuel 0 level numcells tc tv1 (some val) tcell index st = (Hex.GraphIso.Nauty.Generic.Exit.fuel, index, st)

def Hex.GraphIso.Nauty.initial (n : Nat) (lab0 : Array Nat) (cellEnds : List Nat) : Search n

Allocate the search globals, including the reusable permutation.

Equations

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

def Hex.GraphIso.Nauty.runState (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : Exit × Search n

Run the search and retain the final state and exit for diagnostics. On a valid nonempty input, cell count is at least the level: refinement never decreases it and each child increases it. Thus node depth is at most n, so node fuel n + 2 suffices. A sweep visits at most n vertices in strictly increasing order, so sweep fuel n + 1 suffices.

Equations

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

def Hex.GraphIso.Nauty.finish {n : Nat} (ctx : Ctx n) (st : Search n) : TraceRun n

Read the canonical result and trace, updating the remaining rows.

Equations

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

def Hex.GraphIso.Nauty.runTraced (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : TraceRun n

Run the search with the certificate producer's result type.

Equations

• Hex.GraphIso.Nauty.runTraced n g lab0 cellEnds = Hex.GraphIso.Nauty.finish { g := g } (Hex.GraphIso.Nauty.runState n g lab0 cellEnds).snd

def Hex.GraphIso.Nauty.run (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : RunResult n

Run the search, discarding the trace.

Equations

• Hex.GraphIso.Nauty.run n g lab0 cellEnds = (Hex.GraphIso.Nauty.runTraced n g lab0 cellEnds).result

def Hex.GraphIso.Nauty.runColoredTraced {n k : Nat} (G : Colored n k) : TraceRun n

Run the search on a coloured graph, retaining the trace.

Equations

• Hex.GraphIso.Nauty.runColoredTraced G = match Hex.GraphIso.Nauty.initialPartition G with | (lab0, cellEnds) => Hex.GraphIso.Nauty.runTraced n (Hex.GraphIso.Nauty.rowsOf G) lab0 cellEnds

def Hex.GraphIso.Nauty.runColored {n k : Nat} (G : Colored n k) : RunResult n

Run the search on a coloured graph.

Equations

• Hex.GraphIso.Nauty.runColored G = (Hex.GraphIso.Nauty.runColoredTraced G).result

def Hex.GraphIso.Nauty.searchResult? {n k : Nat} (G : Colored n k) : Option (CanonResult n k)

The nauty-compatible canonical result: the checked label from canonlab and the relabelled coloured graph. none only if the raw search output fails the label check, which conformance shows does not occur.

Equations

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