law dfs_none

minebender-game@1.0.0.0 · proof_solver.bend:1018

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B
import minebender-game@1.0.0.0/solver.bend as S
import minebender-game@1.0.0.0/proof_cells.bend as PS

1018# If the search finds nothing, no consistent layout completes the partial
1019# layout (given that every unassigned cell is still to do).
1020law dfs_none:
1021  for +todo: List<&2, S.Todo>
1022  for +part: T.Grid(Maybe<&2, Bool>)
1023  for +w: Nat
1024  for +h: Nat
1025  for +n: Nat
1026  for +rows: T.Grid(T.Seen)
1027  for +its: List<&2, S.Item>
1028  for +layout: T.Grid(Bool)
1029  for e: {S.dfs(todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Grid(Bool)>}
1030  for +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}
1031  for +shL: {B.shaped(Bool, w, h, layout) == True{} : Bool}
1032  for +cov: {covers(w, h, todo, part) == True{} : Bool}
1033  for +comp: {completes(w, h, part, layout) == True{} : Bool}
1034  for +chk: {S.check(S.Ctx{w, h, n, rows, its}, layout) == True{} : Bool}
1035  for +tok: {todos_ok(todo, layout) == True{} : Bool}
1036  for +ton: {todos_onb(PS.WH{w, h}, todo) == True{} : Bool}
1037  for +ion: {items_onb(PS.WH{w, h}, its) == True{} : Bool}
1038  Empty