minebender-game

Releases (1)

• 1.0.0.0 indexed

Definitions (1,011)

proof_speed.bend

• def dfs2_eq.node
• law dfs2_eqWith the counts right and every cell on the board, the counting search answers exactly as the plain one.

proof_sums.bend

• def smapEach element plus one.
• law map_append
• law range_consrange(1+n) is 0 followed by 1..n.
• def rsum
• def gsumThe sum of f over the grid, row by row.
• def csumThe sum of f over the cells ps of the grid.
• def rsum_at
• law csum_append
• law csum_row0
• law csum_row_shift
• law csum_shift
• law rsum_at_shift
• law rsum_at_full
• law gsum_cells_go
• law grid_sumSumming over a w-by-h grid row by row equals summing over its cells.

proof_walk.bend

• def and4
• law and4_d
• law and4_c
• law and4_b
• law and4_a
• law and4_intro
• law lsame_sound
• law lsame_refl
• law walk_snocExtending a walk to c by one step from c (a zero) to r.
• law rev_acc
• law rev_cons
• law walk_onA walk ends on the board when it starts there.
• law walk_safeA walk from a safe cell only reaches safe cells.

solver.bend

• type ItemA revealed cell, and for a number, the cells it counts.
• type TodoA hidden cell to assign, and the numbers around it.
• type Ctx
• def items.put
• def itemsThe revealed cells of ps.
• def item_ok
• def items_ok
• def checkThe layout is consistent with what the player knows.
• def start.cell
• def start.row
• def startWhat the revealed cells fix: no mine under a number, one under a Boom.
• def fill.row
• def fill
• def look
• def is_true
• def is_none
• def one_if
• def row_true
• def row_none
• def part_true
• def part_none
• def true_among
• def none_among
• def betweenk is still reachable from what is fixed: t mines, f unassigned cells.
• def item_open
• def items_open
• def open_okSome completion of the partial layout may still be consistent.
• def ctx_n
• def dfs.or
• def dfs.when
• def dfs.free
• def leaf
• def dfsA consistent layout completing the partial one, assigning the cells of `todo` in order (cells already assigned are skipped).
• def dfs2The same search, carrying the mines t and unassigned cells f of the partial layout instead of recounting the whole grid at every step.
• def is_hidden
• def hidden_cells
• def is_number
• def around.put
• def aroundThe numbers of `is` that count c.
• def todos
• def has_rel
• def nearsThe cells next to a number.
• def farsThe other cells.
• def orderThe cells next to a number first, then the rest.
• def todo_c
• def rel_gridThe numbers around each cell next to one; Nil elsewhere.
• type ReachA breadth-first walk over cells linked by a number: the cells to visit, the cells reached (latest first) and a grid of the cells reached.
• def reach.add.go
• def reach.addReach p, if it is next to a number and not reached yet.
• def reach.ns
• def reach.items
• def reach.runVisit cells until none is left to visit (fuel: more than the cells).
• def reach.order
• def reach.start
• def linkedThe cells linked to c through numbers, nearest first (none when c is next to no number).
• def groups.go
• def groupsThe cells next to a number, one group of linked cells at a time.
• def with_c
• def gatherThe todos of ts for the cells qs, in the order of qs.
• def rotts from its k-th element on, then the first k.
• def spinHow far to rotate the far cells for c: searches for nearby cells start about n cells apart, so their layouts mine different far cells.
• type PlanWhat every search of a solve shares: the cells next to a number and the rest, the groups, the plain order, and the numbers around each cell.
• def plan
• def plan_todoThe order of the search for c.
• def covered
• def searchA consistent layout with a mine on c, if there is one.
• def loop.if
• def loop.found
• def loopThe first cell of hs that no consistent layout mines, given layouts `found` already shown consistent.
• def solve.go