theorem
Hex.GraphIso.Nauty.scatter_eq
{n : Nat}
{κ : Type}
(ref : Array Nat)
(st : SearchState n κ)
:
scatter ref st = { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts, autos := st.autos,
wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc,
firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows,
compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst,
gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel,
allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes,
tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators,
numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace,
workperm := List.foldl (fun (a : Array Nat) (i : Nat) => a.set! ref[i]! st.lab[i]!) st.workperm (List.range n) }
Scattering updates only the permutation workspace.
theorem
Hex.GraphIso.Nauty.scatter_get
{n : Nat}
{κ : Type}
{ref : Array Nat}
{st : SearchState n κ}
(hinj : ∀ (i j : Nat), i < n → j < n → ref[i]! = ref[j]! → i = j)
(hbound : ∀ (i : Nat), i < n → ref[i]! < st.workperm.size)
{i : Nat}
(hi : i < n)
:
Each reference vertex receives the corresponding current vertex.
theorem
Hex.GraphIso.Nauty.scatter_map
{n : Nat}
{κ : Type}
{ref : Array Nat}
{st : SearchState n κ}
(hwork : st.workperm.size = n)
(href : ref.size = n)
(hrefPerm : ref.toList.Perm (List.range n))
(i : Nat)
:
A permutation reference assigns every position of the current labelling.
theorem
Hex.GraphIso.Nauty.scatter_checked
{n : Nat}
{ctx : Ctx n}
{ref : Array Nat}
{st : Search n}
(hwork : st.workperm.size = n)
(href : ref.size = n)
(hrefPerm : ref.toList.Perm (List.range n))
(hlab : st.lab.size = n)
(hlabPerm : st.lab.toList.Perm (List.range n))
(hrows : leafRows ctx ref = leafRows ctx st.lab)
:
Equal leaf rows validate the scatter independently of its old contents.
theorem
Hex.GraphIso.Nauty.scatter_isautom
{n : Nat}
{ctx : Ctx n}
{ref : Array Nat}
{st : Search n}
(hwork : st.workperm.size = n)
(href : ref.size = n)
(hrefPerm : ref.toList.Perm (List.range n))
(hlab : st.lab.size = n)
(hlabPerm : st.lab.toList.Perm (List.range n))
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
(hcheck : isautom ctx (scatter ref st).workperm = true)
:
A successful automorphism scan validates the reusable scatter.