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

Allocate scratch arrays for a graph of order n.

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

Retain the reusable arrays after refinement.

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

Activate a cell and append its start to the ordered splitter queue.

Equations

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

@[inline]

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

Incorporate one refinement event into nauty's invariant code.

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.