structure Hex.GraphIso.Nauty.Sparse.Storage (n : Nat) extends Hex.GraphIso.Nauty.Sparse.Rows n : Type

Canonical rows and scratch storage carried by the shared search. Scratch is independent of the partition nest restored during backtracking.

• offsets : Array Nat
• neighbors : Array Nat
• scratch : Scratch

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instInhabitedStorage {a✝ : Nat} : Inhabited (Storage a✝)

Equations

• Hex.GraphIso.Nauty.Sparse.instInhabitedStorage = { default := Hex.GraphIso.Nauty.Sparse.instInhabitedStorage.default }

def Hex.GraphIso.Nauty.Sparse.Storage.update {n : Nat} (g : Graph n) (s : Storage n) (lab : Array Nat) (same : Nat) : Storage n

Equations

• Hex.GraphIso.Nauty.Sparse.Storage.update g s lab same = { toRows := Hex.GraphIso.Nauty.Sparse.updatecan g s.toRows lab same, scratch := s.scratch }

def Hex.GraphIso.Nauty.Sparse.Storage.invalidate {n : Nat} (s : Storage n) : Storage n

Equations

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

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Sparse.State (n : Nat) : Type

Equations

• Hex.GraphIso.Nauty.Sparse.State n = Hex.GraphIso.Nauty.SearchState n (Hex.GraphIso.Nauty.Sparse.Storage n)

def Hex.GraphIso.Nauty.Sparse.visit {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : Nat × Nat × State n

Count the node and run the sparse refinement dispatch.

Equations

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

def Hex.GraphIso.Nauty.Sparse.chooseTarget {n : Nat} (first : Bool) (g : Graph n) (tcLevel level numcells : Nat) (st : State n) : Int × VSet n × Nat × State n

The shared target guards, with targetcell_sg as the graph dispatch.

Equations

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

def Hex.GraphIso.Nauty.Sparse.classify {n : Nat} (g : Graph n) (level numcells : Nat) (st : State n) : Leaf × State n

nauty's five classifications, using sparse automorphism and canonical row tests. Every other transition is shared with dense nauty.

Equations

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

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.policy {n : Nat} : Generic.Policy (State n) n

Equations

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

def Hex.GraphIso.Nauty.Sparse.initial {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : State n

Initial shared bookkeeping and a compressed canonical store.

Equations

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

def Hex.GraphIso.Nauty.Sparse.runState {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : Exit × State n

The pinned sparse search, retaining its final exit and diagnostic state.

Equations

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

def Hex.GraphIso.Nauty.Sparse.finish {n : Nat} (g : Graph n) (st : State n) : State n

Finish the pending canonical rows, preserving the raw sparse row order.

Equations

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

def Hex.GraphIso.Nauty.Sparse.run {n : Nat} (g : Graph n) (lab : Array Nat) (ends : List Nat) : State n

Equations

• Hex.GraphIso.Nauty.Sparse.run g lab ends = Hex.GraphIso.Nauty.Sparse.finish g (Hex.GraphIso.Nauty.Sparse.runState g lab ends).snd

@[specialize #[]]

def Hex.GraphIso.Nauty.Sparse.initialPartitionWith {α : Type u_1} (n k : Nat) (colors : Array α) (color : α → Nat) : Array Nat × List Nat

Stable colour buckets in O(n + k) time. Valid colourings use every bucket; the empty graph has no buckets.

Equations

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

def Hex.GraphIso.Nauty.Sparse.initialPartition (n k : Nat) (colors : Array Nat) : Array Nat × List Nat

Equations

• Hex.GraphIso.Nauty.Sparse.initialPartition n k colors = Hex.GraphIso.Nauty.Sparse.initialPartitionWith n k colors id