def solver_tok

minebender-game@1.0.0.0 · proof_solver.bend:2525

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_base.bend as P

2525def solver_tok(+w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +layout: T.Grid(Bool),
2526  chk: {S.check(S.Ctx{w, h, n, rows, S.items(w, h, rows, B.cells(w, h))}, layout) == True{} : Bool}) ->
2527  {todos_ok(S.order(S.todos(S.items(w, h, rows, B.cells(w, h)), S.hidden_cells(rows, B.cells(w, h)))), layout) == True{} : Bool}:
2528  +its = S.items(w, h, rows, B.cells(w, h))
2529  +t0 = S.todos(its, S.hidden_cells(rows, B.cells(w, h)))
2530  +a = Bool.and(Bool.and(B.shaped(Bool, w, h, layout), B.shaped(T.Seen, w, h, rows)), Nat.is_eq(B.total_mines(layout), n))
2531  +iok = P.and_true_r(a, S.items_ok(its, layout), chk)
2532  +ta = todos_ok_all(its, S.hidden_cells(rows, B.cells(w, h)), layout, iok)
2533  tok_append(S.nears(t0), S.fars(t0), layout, tok_order(t0, layout, ta), tok_order_f(t0, layout, ta))