Finite chronological forest-search program

The work representation uses the existing positional occurrence records: unary constraint and port positions, binary original names. Only final result positions are converted to binary global indices. Every loop traverses an actual list or its length. The stopped event occupies a separate small field: the completed log stays in the same encoding throughout the iteration.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.WorkExpansion : Type

One work expansion: its positional input record and ordered positional output records.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.encWorkExpansion : (ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ) ↪ List Bool

A unary-position input record is framed; its framed output list follows. Names stay binary.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.WorkLog : Type

Completed work expansions, newest first.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.encWorkLog : List ((ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ)) ↪ List Bool

A framed list of the documented work expansions.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.ScanState : Type

Work scan state: ordered children and the optional first meeting port.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.encScanState : List (ℕ × ℕ × ℕ) × Option (ℕ × ℕ × ℕ) ↪ List Bool

The child list is framed, followed by an option tag and a positional meeting record.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.Event : Type

Small terminal data: current input, current children, and meeting output.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.encEvent : (ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ) × ℕ × ℕ × ℕ ↪ List Bool

Input and children are framed in order, followed by the meeting record.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.State : Type

Log and remaining ports, followed by running / exhausted / meeting status.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.EdgeForest.encState : List ((ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ)) × List (ℕ × ℕ × ℕ) × Option (Option ((ℕ × ℕ × ℕ) × List (ℕ × ℕ × ℕ) × ℕ × ℕ × ℕ)) ↪ List Bool

Log and remaining list stay in fixed framed fields. The two option tags distinguish running, exhausted and meeting; event data never duplicate or reframe the completed log.

def Cslib.Complexity.CSP.EdgeForest.roots (input : Input) : List ℕ

Original roots, retaining first positional occurrence order.

def Cslib.Complexity.CSP.EdgeForest.used (es : WorkLog) : List EdgeAugmenting.Record

Used positional records in the source log's order.

def Cslib.Complexity.CSP.EdgeForest.children (es : WorkLog) : List ℕ

Discovered variables in the source log's order.

def Cslib.Complexity.CSP.EdgeForest.visited (rs : List ℕ) (es : WorkLog) (v : ℕ) : Bool

Root/discovery membership, including children already inserted at the current copy.

def Cslib.Complexity.CSP.EdgeForest.parentConstraint (es : WorkLog) (v : ℕ) : Option ℕ

First actual parent output's original constraint position; timestamps are irrelevant here.

def Cslib.Complexity.CSP.EdgeForest.root (es : WorkLog) (v : ℕ) : ℕ

Follow parents through older records, computing just the root of the actual ancestry walk.

def Cslib.Complexity.CSP.EdgeForest.partners (input : Input) (a : EdgeAugmenting.Record) : List EdgeAugmenting.Record

Feasible same-constraint, distinct-variable partners in actual incidence order. The validity check is global, including on invalid inputs and malformed explicit relation tables.

def Cslib.Complexity.CSP.EdgeForest.scanStep (rs : List ℕ) (es : WorkLog) (a : EdgeAugmenting.Record) (s : ScanState) (b : EdgeAugmenting.Record) : ScanState

One scan step. A meeting freezes both ordered children and the first meeting output.

def Cslib.Complexity.CSP.EdgeForest.scan (rs : List ℕ) (es : WorkLog) (a : EdgeAugmenting.Record) (outputs bs : List EdgeAugmenting.Record) : ScanState

Scan actual partners using a finite left fold.

def Cslib.Complexity.CSP.EdgeForest.step (input : Input) (s : State) : State

One outer step. Noncanonical external states whose chosen port is not an actual occurrence stop immediately; this guard gives uniform growth on every state, without scanning its index.

def Cslib.Complexity.CSP.EdgeForest.finishExpansion (F : Logic.PL.CSP Logic.PL.CSP.Table ℕ) (e : WorkExpansion) : ExpansionCode

Convert a work expansion's positional records into binary global occurrence positions.

def Cslib.Complexity.CSP.EdgeForest.finish (input : Input) (s : State) : Option ResultCode

Finalize once, after the loop. Classification uses roots of the actual older ancestries.

def Cslib.Complexity.CSP.EdgeForest.run (input : Input) : Option ResultCode

Total native forest search. Exactly the actual occurrence width is accepted. The outer clock is one more than the actual occurrence count, so the final exhaustion check is paid for.

theorem Cslib.Complexity.CSP.EdgeForest.run_eq_none_of_length (input : Input) (h : input.labels.length ≠ input.body.incidenceList.length) : run input = none

Reject either short or long occurrence buffers.