Executable ancestral-path and cycle data at a forest meeting

The two cases at the start of Section 5.3 of [KKR18], arXiv:1602.03124v6, printed pp. 11–12, distinguish a variable lowest common ancestor from a copied-constraint lowest common ancestor. In the latter case the child on the left path becomes the new base after flipping its root path. The final cycle step uses the two actual child ports at the common copied constraint.

Meeting.blossomData computes this information from actual paths; it does not replace the two cases by an arbitrary constraint name or a flag. Timestamps identify copied nodes, so repeated appearances of an original constraint are not conflated. Its Option records the absence of a common root on augmentation events and permits total evaluation of externally constructed malformed meeting records. The blossom validity theorem is a separate obligation.

Main definitions

• Meeting.blossomData: actual cycle, preparatory root path, meeting pivot and LCA child ports.

def Cslib.Logic.PL.CSP.Forest.Ancestry.nodes {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} (p : Ancestry F) : List (DAG.Node F)

The actual variable and copied-constraint nodes of a timestamped ancestral walk. Valid search ancestries have exactly one timestamp per step.

structure Cslib.Logic.PL.CSP.Forest.BlossomData {Rel : Type u_1} {V : Type u_2} (F : CSP Rel V) : Type u_2

Actual cycle, base and root-path preparation for the contraction layer. These are raw executable data; the record itself asserts no blossom-correctness premise.

• ancestor : DAG.Node F

  Copied or variable node that is the lowest common ancestor of the meeting endpoints.

• prepare : F.Walk

  Root-to-base prefix to flip before contraction; empty in the source's variable-LCA case.

• cycle : F.Walk

  Actual closed cycle of positional incidence pairs, oriented from the new base.

• times : List ℕ

  One timestamp per cycle step; orientation is reversed after the meeting copy.

• pivot : ℕ

  Number of steps from the new base through the meeting copied constraint.

• leftPort : Option F.Occurrence

  Actual left child port at a constraint LCA, absent for a variable LCA.

• rightPort : Option F.Occurrence

  Actual right child port at a constraint LCA, absent for a variable LCA.

def Cslib.Logic.PL.CSP.Forest.Meeting.commonNodes {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) : List (DAG.Node F)

Shared ancestral nodes, with both the original constraint position and its timestamp participating in copied-node equality.

def Cslib.Logic.PL.CSP.Forest.Meeting.ancestor? {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) : Option (DAG.Node F)

Last common ancestral node, absent when the endpoints lie in different trees.

def Cslib.Logic.PL.CSP.Forest.Meeting.blossomData {Rel : Type u_1} {V : Type u_2} {F : CSP Rel V} [DecidableEq V] (m : Meeting F) : Option (BlossomData F)

The cycle and preparatory prefix specified at the start of source Section 5.3. In the constraint-LCA case the final step crosses the two actual child ports at that copy; the preparatory path ends at the left child and includes the LCA step.