structure Hex.GraphIso.Nauty.Sparse.Scratch : Type

Arrays retained across refinement calls. Marks use a monotonically increasing generation; counts are cleared when their cell is first touched.

• cellstart : Array Nat
• cellend : Array Nat
• indexed : Bool
• hits : Array Nat
• marks : Array Nat
• vmarks : Array Nat
• stamp : Nat

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instInhabitedScratch : Inhabited Scratch

Equations

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

def Hex.GraphIso.Nauty.Sparse.Scratch.fresh (n : Nat) : Scratch

Equations

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

structure Hex.GraphIso.Nauty.Sparse.RefineSt (n : Nat) : Type

The working state of refine_sg. Only equality with the current generation stamp is observed.

• lab : Array Nat
• ptn : Array Nat
• active : VSet n
• queue : Array Nat
• cellstart : Array Nat
• cellend : Array Nat
• indexed : Bool
• hits : Array Nat
• marks : Array Nat
• vmarks : Array Nat
• stamp : Nat
• numcells : Nat
• longcode : Nat

@[instance_reducible]

instance Hex.GraphIso.Nauty.Sparse.instInhabitedRefineSt {a✝ : Nat} : Inhabited (RefineSt a✝)

Equations

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

def Hex.GraphIso.Nauty.Sparse.RefineSt.toScratch {n : Nat} (s : RefineSt n) : Scratch

Equations

• s.toScratch = { cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp }

def Hex.GraphIso.Nauty.Sparse.RefineSt.push {n : Nat} (s : RefineSt n) (v : Nat) : RefineSt n

Equations

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

def Hex.GraphIso.Nauty.Sparse.RefineSt.hash {n : Nat} (s : RefineSt n) (v : Nat) : RefineSt n

Equations

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

def Hex.GraphIso.Nauty.Sparse.indexCells (n : Nat) (lab ptn : Array Nat) (level : Nat) (starts ends : Array Nat) : Array Nat × Array Nat

Vertex-to-cell indices, using n for singleton vertices, and the last position of each current cell. Entries at other positions are not read.

Equations

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

def Hex.GraphIso.Nauty.Sparse.splitCounts {n : Nat} (level first : Nat) (distance : Bool) (s : RefineSt n) : RefineSt n

Divide one cell by counts or distances. The first two minimum fragments use nauty's three-way insertion; later fragments use its exact indirect sort. distance selects the distinct distance-branch code updates.

Equations

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

def Hex.GraphIso.Nauty.Sparse.splitSingleton {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) : RefineSt n

A singleton splitter: untouched vertices keep their order and touched vertices are written in reverse order, as in HITS[--k].

Equations

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

def Hex.GraphIso.Nauty.Sparse.splitNontrivial {n : Nat} (g : Graph n) (level split : Nat) (s : RefineSt n) : RefineSt n

Count only vertices in touched nontrivial cells. Rows of hits are cleared on first touch, without a full vertex scan for each splitter.

Equations

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

def Hex.GraphIso.Nauty.Sparse.refineWith {n : Nat} (g : Graph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) : RefineSt n

refine_sg, including its shallow distance split and preference for singleton splitters among the first ten active entries.

Equations

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

def Hex.GraphIso.Nauty.Sparse.refine {n : Nat} (g : Graph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : RefineSt n

Standalone refinement with freshly initialized scratch storage.

Equations

• Hex.GraphIso.Nauty.Sparse.refine g level lab ptn active numcells = Hex.GraphIso.Nauty.Sparse.refineWith g level lab ptn active numcells (Hex.GraphIso.Nauty.Sparse.Scratch.fresh n)