inductive Hex.GraphIso.Nauty.Generic.Exit : Type

Completion of a sweep, an unwind to a level with an optional short prune, or exhaustion of the recursion bound.

• done : Exit
• unwind (target : Nat) (short : Bool) : Exit
• fuel : Exit

def Hex.GraphIso.Nauty.Generic.instBEqExit.beq : Exit → Exit → Bool

Equations

• Hex.GraphIso.Nauty.Generic.instBEqExit.beq Hex.GraphIso.Nauty.Generic.Exit.done Hex.GraphIso.Nauty.Generic.Exit.done = true
• Hex.GraphIso.Nauty.Generic.instBEqExit.beq (Hex.GraphIso.Nauty.Generic.Exit.unwind a a_1) (Hex.GraphIso.Nauty.Generic.Exit.unwind b b_1) = (a == b && a_1 == b_1)
• Hex.GraphIso.Nauty.Generic.instBEqExit.beq Hex.GraphIso.Nauty.Generic.Exit.fuel Hex.GraphIso.Nauty.Generic.Exit.fuel = true
• Hex.GraphIso.Nauty.Generic.instBEqExit.beq x✝¹ x✝ = false

@[instance_reducible]

instance Hex.GraphIso.Nauty.Generic.instBEqExit : BEq Exit

Equations

• Hex.GraphIso.Nauty.Generic.instBEqExit = { beq := Hex.GraphIso.Nauty.Generic.instBEqExit.beq }

@[instance_reducible]

instance Hex.GraphIso.Nauty.Generic.instReprExit : Repr Exit

Equations

• Hex.GraphIso.Nauty.Generic.instReprExit = { reprPrec := Hex.GraphIso.Nauty.Generic.instReprExit.repr }

def Hex.GraphIso.Nauty.Generic.instReprExit.repr : Exit → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.GraphIso.Nauty.Generic.instInhabitedExit : Inhabited Exit

Equations

• Hex.GraphIso.Nauty.Generic.instInhabitedExit = { default := Hex.GraphIso.Nauty.Generic.instInhabitedExit.default }

inductive Hex.GraphIso.Nauty.Generic.Leaf : Type

The five node classifications in nauty's processnode. A better leaf carries the number of adjacency rows shared with the incumbent.

• internal : Leaf
• autoFirst : Leaf
• autoCanon : Leaf
• better (sr : Nat) : Leaf
• bad : Leaf

def Hex.GraphIso.Nauty.Generic.instBEqLeaf.beq : Leaf → Leaf → Bool

Equations

• Hex.GraphIso.Nauty.Generic.instBEqLeaf.beq Hex.GraphIso.Nauty.Generic.Leaf.internal Hex.GraphIso.Nauty.Generic.Leaf.internal = true
• Hex.GraphIso.Nauty.Generic.instBEqLeaf.beq Hex.GraphIso.Nauty.Generic.Leaf.autoFirst Hex.GraphIso.Nauty.Generic.Leaf.autoFirst = true
• Hex.GraphIso.Nauty.Generic.instBEqLeaf.beq Hex.GraphIso.Nauty.Generic.Leaf.autoCanon Hex.GraphIso.Nauty.Generic.Leaf.autoCanon = true
• Hex.GraphIso.Nauty.Generic.instBEqLeaf.beq (Hex.GraphIso.Nauty.Generic.Leaf.better a) (Hex.GraphIso.Nauty.Generic.Leaf.better b) = (a == b)
• Hex.GraphIso.Nauty.Generic.instBEqLeaf.beq Hex.GraphIso.Nauty.Generic.Leaf.bad Hex.GraphIso.Nauty.Generic.Leaf.bad = true
• Hex.GraphIso.Nauty.Generic.instBEqLeaf.beq x✝¹ x✝ = false

@[instance_reducible]

instance Hex.GraphIso.Nauty.Generic.instBEqLeaf : BEq Leaf

Equations

• Hex.GraphIso.Nauty.Generic.instBEqLeaf = { beq := Hex.GraphIso.Nauty.Generic.instBEqLeaf.beq }

def Hex.GraphIso.Nauty.Generic.instReprLeaf.repr : Leaf → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Hex.GraphIso.Nauty.Generic.instReprLeaf : Repr Leaf

Equations

• Hex.GraphIso.Nauty.Generic.instReprLeaf = { reprPrec := Hex.GraphIso.Nauty.Generic.instReprLeaf.repr }

@[instance_reducible]

instance Hex.GraphIso.Nauty.Generic.instInhabitedLeaf : Inhabited Leaf

Equations

• Hex.GraphIso.Nauty.Generic.instInhabitedLeaf = { default := Hex.GraphIso.Nauty.Generic.instInhabitedLeaf.default }

class Hex.GraphIso.Nauty.Generic.Policy (σ : Type) (n : outParam Nat) {γ : outParam Type} : Type

The local operations of an individualization-refinement search. The state includes the partition and any policy-specific bookkeeping. Sweep entries are indices below n; a policy may interpret them as vertex labels or target-cell offsets.

• visit : γ → Nat → Nat → σ → Nat × Nat × σ

  Refine a node and return its cell count and code.

• recordFirst : Nat → Nat → σ → σ

  Save a first-path refinement code.

• compareCodes : Nat → Nat → σ → σ

  Compare an off-path refinement code with the reference paths.

• chooseTarget : Bool → γ → Nat → Nat → Nat → σ → Int × VSet n × Nat × σ

  Choose a target cell, its sweep entries, and its size.

• firstterminal : Nat → σ → σ

  Install the first discrete leaf.

• classify : γ → Nat → Nat → σ → Leaf × σ

  Classify an off-path node.

• leafExit : Leaf → Nat → σ → Exit × σ

  Act on a node classification.

• cheapCheck : Bool → Nat → σ → σ

  Update the cheap-automorphism boundary.

• child : Bool → Nat → Nat → Nat → σ → σ

  Individualize the child identified by a sweep entry.

• afterChildFirst : Nat → Nat → σ → σ

  Update first-path controls after the leftmost child.

• leaveChild : Nat → σ → σ

  Remove a child's temporary bookkeeping.

• orbit : σ → Nat → Nat

  Read the representative used to skip a sweep entry.

• shortprune : VSet n → σ → VSet n

  Restrict the remaining sweep entries using the newest pair.

• longprune : VSet n → σ → VSet n

  Restrict the remaining sweep entries using the stored pairs.

• recover : Nat → Nat → σ → σ

  Restore the parent partition and comparison controls.

• afterSweep : Bool → Nat → Nat → Nat → σ → σ

  Finish a complete sweep.

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Generic.NodeFn (σ : Type) : Type

A node continuation with its recursion bound supplied by the caller.

Equations

• Hex.GraphIso.Nauty.Generic.NodeFn σ = (Bool → Nat → Nat → σ → Hex.GraphIso.Nauty.Generic.Exit × σ)

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Generic.SweepFn (σ : Type) (n : Nat) : Type

A sweep continuation with both recursion bounds supplied by the caller.

Equations

• Hex.GraphIso.Nauty.Generic.SweepFn σ n = (Bool → Nat → Nat → Nat → Nat → Option Nat → Hex.GraphIso.Nauty.VSet n → Nat → σ → Hex.GraphIso.Nauty.Generic.Exit × Nat × σ)

def Hex.GraphIso.Nauty.Generic.nodeStep {n : Nat} {σ γ : Type} [Policy σ n] (ctx : γ) (tcLevel : Nat) (next : SweepFn σ n) (first : Bool) (level numcells : Nat) (st : σ) : Exit × σ

The local node operations, followed by a supplied child sweep.

Equations

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

def Hex.GraphIso.Nauty.Generic.resume {n : Nat} {σ γ : Type} [Policy σ n] (inf : Nat) (next : SweepFn σ n) (first : Bool) (level numcells tc tv1 tv : Nat) (cell : VSet n) (index : Nat) (st : σ) : Exit × Nat × σ

Apply the long filter, recover the parent, and visit the next surviving entry.

Equations

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

def Hex.GraphIso.Nauty.Generic.advance {n : Nat} {σ γ : Type} [Policy σ n] (inf : Nat) (next : SweepFn σ n) (first : Bool) (level numcells tc tv1 tv : Nat) (cell : VSet n) (index : Nat) (st : σ) (exit : Exit) : Exit × Nat × σ

Consume a child's exit after fixed-point cleanup, passing a deeper unwind outward or filtering and resuming the current sweep.

Equations

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

def Hex.GraphIso.Nauty.Generic.sweepStep {n : Nat} {σ γ : Type} [Policy σ n] (inf : Nat) (descend : NodeFn σ) (next : SweepFn σ n) (first : Bool) (level numcells tc tv1 tv : Nat) (tcell : VSet n) (index : Nat) (st : σ) : Exit × Nat × σ

One target vertex, followed by supplied node and sweep continuations.

Equations

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

@[irreducible]

def Hex.GraphIso.Nauty.Generic.node {n : Nat} {σ γ : Type} [Policy σ n] (first : Bool) (ctx : γ) (inf tcLevel fuel level numcells : Nat) (st : σ) : Exit × σ

Refine a node, classify it, and sweep its surviving children.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Generic.node first ctx inf tcLevel 0 level numcells st = (Hex.GraphIso.Nauty.Generic.Exit.fuel, st)

@[irreducible]

def Hex.GraphIso.Nauty.Generic.sweep {n : Nat} {σ γ : Type} [Policy σ n] (first : Bool) (ctx : γ) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (tv? : Option Nat) (tcell : VSet n) (index : Nat) (st : σ) : Exit × Nat × σ

Sweep surviving vertices, transporting exits below this level.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.Generic.sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 none tcell index st = (Hex.GraphIso.Nauty.Generic.Exit.done, index, st)
• Hex.GraphIso.Nauty.Generic.sweep first ctx inf tcLevel fuel 0 level numcells tc tv1 (some val) tcell index st = (Hex.GraphIso.Nauty.Generic.Exit.fuel, index, st)