Documentation

HexGraphIso.Nauty.Sparse.RefineParts

source
def Hex.GraphIso.Nauty.Sparse.Refinement.queue {n : Nat} (active : VSet n) :
Array Nat
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Hex.GraphIso.Nauty.Sparse.Refinement.start {n : Nat} (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) :
    RefineSt n
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Hex.GraphIso.Nauty.Sparse.Refinement.indexed {n : Nat} (level : Nat) (s : RefineSt n) :
      RefineSt n
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Hex.GraphIso.Nauty.Sparse.Refinement.distanceStart {n : Nat} (g : Graph n) (s : RefineSt n) :
        RefineSt n
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Hex.GraphIso.Nauty.Sparse.Refinement.distance {n : Nat} (level : Nat) (s : RefineSt n) :
          RefineSt n
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Hex.GraphIso.Nauty.Sparse.Refinement.loop {n : Nat} (g : Graph n) (level : Nat) (s : RefineSt n) :
            RefineSt n
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def Hex.GraphIso.Nauty.Sparse.Refinement.finish {n : Nat} (s : RefineSt n) :
              RefineSt n
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Hex.GraphIso.Nauty.Sparse.refineWith_parts {n : Nat} (g : Graph n) (level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) (scratch : Scratch) :
                refineWith g level lab ptn active numcells scratch = have s := Refinement.start lab ptn active numcells scratch; if s.queue.isEmpty = true then { lab := s.lab, ptn := s.ptn, active := s.active, queue := s.queue, cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := cleanup s.longcode } else have r := Refinement.indexed level s; if (decide (level ≤ 2) && s.queue.size == 1 && decide (ptn[s.queue[0]!]! ≤ level) && decide (numcells ≤ n / 8)) = true then Refinement.finish (Refinement.loop g level (Refinement.distance level (Refinement.distanceStart g r))) else Refinement.finish (Refinement.loop g level r)

                The proof blocks compose to exactly the executed refinement function, including the early empty-queue return and shallow-distance guards.