def Hex.GraphIso.Nauty.Sparse.Target.row {n : Nat} (g : Graph n) (lab : Array Nat) (s : Scratch) (first : Nat) : List Nat

The cell indices met by the representative vertex's adjacency row.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Target.score {n : Nat} (g : Graph n) (lab : Array Nat) (s : Scratch) (keys : List Nat) (first : Nat) : Nat

The number of partial joins, including a join to the cell itself.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Target.select (score : Nat → Nat) (best : Nat × Nat) (k : Nat) : Nat × Nat

Strict improvement retains the earliest cell on ties.

Equations

• Hex.GraphIso.Nauty.Sparse.Target.select score best k = if score k > best.snd then (k, score k) else best

def Hex.GraphIso.Nauty.Sparse.Target.best (keys : List Nat) (score : Nat → Nat) (empty : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.Sparse.Target.best keys score empty = if keys.isEmpty = true then empty else (List.foldl (Hex.GraphIso.Nauty.Sparse.Target.select score) (keys.headD 0, 0) keys).fst

theorem Hex.GraphIso.Nauty.Sparse.bestcellCached_spec {n : Nat} (G : SparseGraph n) (lab ptn : Array Nat) (level : Nat) (s : Scratch) (l : Label n) (hl : Label.ofArray? n lab = some l) (hptn : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hidx : Index.Valid n lab ptn level s.cellstart s.cellend) (hsize : s.hits.size = n) : (bestcellCached (Graph.ofGraph G) lab s).fst = Target.best (Target.nontrivial (cells ptn level n)) (Target.score (Graph.ofGraph G) lab s (Target.nontrivial (cells ptn level n))) n

Cached target selection attains the first maximum partial-join score. The reused hit array may initially contain arbitrary values.