Lightweight state for finite coverage search

@[reducible, inline]

abbrev Erdos97Octagon.RawIncidence.StaticDirectCoverage.RowAssignment : Type

One assigned centre and its eight-bit target-row mask.

Equations

• Erdos97Octagon.RawIncidence.StaticDirectCoverage.RowAssignment = (Erdos97Octagon.Vertex × UInt64)

structure Erdos97Octagon.RawIncidence.StaticDirectCoverage.PairState : Type

Packed state recording which unordered pairs have occurred once or twice.

• seenOnce : UInt64

  Pairs that have occurred in at least one assigned row.

• seenTwice : UInt64

  Pairs that have occurred in at least two assigned rows.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.PairState.empty : PairState

The empty pair-occurrence state.

Equations

• Erdos97Octagon.RawIncidence.StaticDirectCoverage.PairState.empty = { seenOnce := 0, seenTwice := 0 }

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.PairState.compatible (state : PairState) (pairMask : UInt64) : Bool

Whether adding a row preserves pair sparsity.

Equations

• state.compatible pairMask = (state.seenTwice &&& pairMask == 0)

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.PairState.add (state : PairState) (pairMask : UInt64) : PairState

Update pair occurrences after accepting one row.

Equations

• state.add pairMask = { seenOnce := state.seenOnce ||| pairMask, seenTwice := state.seenTwice ||| state.seenOnce &&& pairMask }

structure Erdos97Octagon.RawIncidence.StaticDirectCoverage.ColumnState : Type

Packed byte counters for the number of assigned rows selecting each target.

• counts : UInt64

  Eight one-byte column counters.

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.ColumnState.empty : ColumnState

The empty column-count state.

Equations

• Erdos97Octagon.RawIncidence.StaticDirectCoverage.ColumnState.empty = { counts := 0 }

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.columnIncrements (row : UInt64) : UInt64

Packed increments contributed by one target-row mask.

Equations

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

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.ColumnState.add (state : ColumnState) (row : UInt64) : ColumnState

Update packed column counts after accepting one row.

Equations

• state.add row = { counts := state.counts + Erdos97Octagon.RawIncidence.StaticDirectCoverage.columnIncrements row }

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.ColumnState.count (state : ColumnState) (target : Vertex) : ℕ

Read one packed column counter.

Equations

• state.count target = (state.counts >>> UInt64.ofNat (8 * ↑target) &&& 255).toNat

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.remainingColumnCapacity (remaining : List Vertex) (target : Vertex) : ℕ

Number of remaining rows that can still select a target.

Equations

• Erdos97Octagon.RawIncidence.StaticDirectCoverage.remainingColumnCapacity remaining target = (List.filter (fun (x : Erdos97Octagon.Vertex) => decide (x ≠ target)) remaining).length

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.ColumnState.feasible (state : ColumnState) (remaining : List Vertex) : Bool

Fast packed check that every column can still finish with exactly four entries.

Equations

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

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.selectedByAssignmentsB (assignments : List RowAssignment) (centre target : Vertex) : Bool

Whether a target is selected by an assigned row.

Equations

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

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.assignmentColumnCount (assignments : List RowAssignment) (target : Vertex) : ℕ

Number of assigned rows selecting one target, computed from the semantic prefix.

Equations

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

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.columnFeasibleB (assignments : List RowAssignment) (remaining : List Vertex) : Bool

Semantic check that every column can still finish with exactly four entries.

Equations

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

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.patternExtendsAssignmentsB (assignments : List RowAssignment) (summary : PatternSummary) : Bool

Full semantic check that a packed pattern extends the assigned partial table.

Equations

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

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.hardEqualsAssignmentsB (assignments : List RowAssignment) (summary : HardSummary) : Bool

Full semantic check that an exact-table code equals all assigned rows.

Equations

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

def Erdos97Octagon.RawIncidence.StaticDirectCoverage.addRowCode (code row : UInt64) (centre : Vertex) : UInt64

Add one row to a packed 64-bit incidence-table prefix.

Equations

• Erdos97Octagon.RawIncidence.StaticDirectCoverage.addRowCode code row centre = code ||| (row &&& 255) <<< UInt64.ofNat (8 * ↑centre)