structure
Hex.GraphIso.Nauty.Sparse.Index.Tail
(n first last upto : Nat)
(oldlab hits oldstarts oldends : Array Nat)
(s : RefineSt n)
:
Completed count runs through upto, with the next count change located.
The partition boundary at upto may still await the next outer iteration.
- window : «Sort».Window oldlab s.lab first (last + 1)
- sorted : «Sort».Sorted s.lab hits first (last + 1 - first)
Instances For
theorem
Hex.GraphIso.Nauty.Sparse.Index.Tail.transfer
{n first last upto : Nat}
{oldlab hits oldstarts oldends : Array Nat}
{s t : RefineSt n}
(h : Tail n first last upto oldlab hits oldstarts oldends s)
(hl : t.lab = s.lab)
(hs : t.cellstart = s.cellstart)
(he : t.cellend = s.cellend)
(hh : t.hits = s.hits)
:
Tail n first last upto oldlab hits oldstarts oldends t
theorem
Hex.GraphIso.Nauty.Sparse.Index.Tail.run
{n first last upto : Nat}
{oldlab hits oldstarts oldends : Array Nat}
{s : RefineSt n}
{b : Nat}
(h : Tail n first last upto oldlab hits oldstarts oldends s)
(hu : upto < last)
(ha : upto + 1 ≤ b)
(hb : b ≤ last)
(hk : hits[s.lab[b]!]! = hits[s.lab[upto + 1]!]!)
(hn : b = last ∨ hits[s.lab[b]!]! ≠ hits[s.lab[b + 1]!]!)
:
Sorted counts and equal endpoint values identify every vertex of the run found by the inner scan.
theorem
Hex.GraphIso.Nauty.Sparse.Index.Tail.extend
{n first last upto : Nat}
{oldlab hits oldstarts oldends : Array Nat}
{s : RefineSt n}
{b : Nat}
{starts : Array Nat}
(h : Tail n first last upto oldlab hits oldstarts oldends s)
(hp : oldlab.toList.Perm (List.range n))
(hu : upto < last)
(hbn : last < n)
(ha : upto + 1 ≤ b)
(hb : b ≤ last)
(hk : hits[s.lab[b]!]! = hits[s.lab[upto + 1]!]!)
(hn : b = last ∨ hits[s.lab[b]!]! ≠ hits[s.lab[b + 1]!]!)
(hs : Scatter n s.lab s.cellstart starts (upto + 1 + 1) (b + 1) (upto + 1))
:
Tail n first last b oldlab hits oldstarts oldends
{ lab := s.lab, ptn := s.ptn, active := s.active, queue := s.queue,
cellstart := starts.setIfInBounds s.lab[upto + 1]! (if upto + 1 = b then n else upto + 1),
cellend := s.cellend.setIfInBounds (upto + 1) b, indexed := s.indexed, hits := s.hits, marks := s.marks,
vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }
Completing the inner scatter and writing its first vertex and endpoint extends the cache by exactly the discovered run.