examples/sudoku.mlw

   1
   2 (** {1 An Efficient Sudoku Solver }
   3
   4     Author: Claude Marché       (Inria)
   5             Guillaume Melquiond (Inria) *)
   6
   7
   8 (** {2 A theory of 9x9 grids} *)
   9
  10 module Grid
  11
  12   use int.Int
  13   use map.Map
  14
  15   (** A grid is a map from integers to integers *)
  16   type grid = map int int
  17
  18   (** valid indexes are 0..80 *)
  19   predicate is_index (i:int) = 0 <= i < 81
  20
  21   (** valid values are 0..9. 0 denotes an empty cell *)
  22   predicate valid_values (g:grid) =
  23     forall i. is_index i -> 0 <= g[i] <= 9
  24
  25   (** extensional equality of grids and sub-grids *)
  26   predicate grid_eq_sub (g1 g2:grid) (a b:int) =
  27     forall j. a <= j < b -> g1[j] = g2[j]
  28
  29   predicate grid_eq (g1 g2:grid) = grid_eq_sub g1 g2 0 81
  30
  31   lemma grid_eq_sub:
  32     forall g1 g2 a b. 0 <= a <= 81 /\ 0 <= b <= 81 /\
  33         grid_eq g1 g2 -> grid_eq_sub g1 g2 a b
  34
  35   (** {3 Grid "Chunks"}
  36
  37    A chunk is either a column, a row or a square.
  38
  39    A chunk is defined by a starting index s and a set of 9 offsets
  40    {o0,..,o8}, that thus denotes a set of 9 cells {s+o0,..,s+o8} in a
  41    grid.
  42
  43    Each cell of the grid belongs to 3 chunks, one of each kind.  For
  44    each cell index, there is a unique starting index respectively for
  45    the column, the row and the square it belongs to.
  46
  47   *)
  48
  49   use array.Array
  50
  51   type sudoku_chunks =
  52     { column_start : array int;
  53       column_offsets : array int;
  54       row_start : array int;
  55       row_offsets : array int;
  56       square_start : array int;
  57       square_offsets : array int;
  58     }
  59
  60   (** Chunks must point to valid indexes of the grid *)
  61   predicate chunk_valid_indexes (start:array int) (offsets:array int) =
  62     start.length = 81 /\ offsets.length = 9 /\
  63     forall i o:int. is_index i /\ 0 <= o < 9 ->
  64       is_index(start[i] + offsets[o])
  65
  66   (** Chunks (of the same kind column, row or square) with distinct
  67       starting cells must be disjoint *)
  68   predicate disjoint_chunks (start:array int) (offsets:array int) =
  69     start.length = 81 /\ offsets.length = 9 /\
  70     forall i1 i2 o:int.
  71        is_index i1 /\ is_index i2 /\ 0 <= o < 9 ->
  72        let s1 = start[i1] in
  73        let s2 = start[i2] in
  74        s1 <> s2 -> i1 <> s2 + offsets[o]
  75
  76   (** A sudoku grid is well formed when chunks are valid and disjoint *)
  77   predicate well_formed_sudoku (s:sudoku_chunks) =
  78     chunk_valid_indexes s.column_start s.column_offsets /\
  79     chunk_valid_indexes s.row_start s.row_offsets /\
  80     chunk_valid_indexes s.square_start s.square_offsets /\
  81     disjoint_chunks s.column_start s.column_offsets /\
  82     disjoint_chunks s.row_start s.row_offsets /\
  83     disjoint_chunks s.square_start s.square_offsets
  84
  85   (** {3 Valid Sudoku Solutions} *)
  86
  87   (** `valid_chunk g i start offsets` is true whenever the chunk
  88   denoted by `start,offsets` from cell `i` is "valid" in grid `g`, in
  89   the sense that it contains at most one occurrence of each number
  90   between 1 and 9 *)
  91
  92   predicate valid_chunk (g:grid) (i:int)
  93     (start:array int) (offsets:array int) =
  94     let s = start[i] in
  95     forall o1 o2 : int. 0 <= o1 < 9 /\ 0 <= o2 < 9 /\ o1 <> o2 ->
  96       let i1 = s + offsets[o1] in
  97       let i2 = s + offsets[o2] in
  98       1 <= Map.get g i1 <= 9 /\ 1 <= Map.get g i2 <= 9 ->
  99       Map.get g i1 <> Map.get g i2
 100
 101   predicate valid_column (s:sudoku_chunks) (g:grid) (i:int) =
 102     valid_chunk g i s.column_start s.column_offsets
 103
 104   predicate valid_row (s:sudoku_chunks) (g:grid) (i:int) =
 105     valid_chunk g i s.row_start s.row_offsets
 106
 107   predicate valid_square (s:sudoku_chunks) (g:grid) (i:int) =
 108     valid_chunk g i s.square_start s.square_offsets
 109
 110   (** `valid g` is true when all chunks are valid *)
 111   predicate valid (s:sudoku_chunks) (g : grid) =
 112     forall i : int. is_index i ->
 113       valid_column s g i /\ valid_row s g i /\ valid_square s g i
 114
 115   (** `full g` is true when all cells are filled *)
 116   predicate full (g : grid) =
 117     forall i : int. is_index i -> 1 <= Map.get g i <= 9
 118
 119   (** `included g1 g2` *)
 120   predicate included (g1 g2 : grid) =
 121     forall i : int. is_index i /\ 1 <= Map.get g1 i <= 9 ->
 122       Map.get g2 i = Map.get g1 i
 123
 124   (** validity is monotonic w.r.t. inclusion *)
 125   lemma subset_valid_chunk :
 126     forall g h : grid. included g h ->
 127       forall i:int, s o:array int. is_index i /\
 128       chunk_valid_indexes s o /\ valid_chunk h i s o ->
 129         valid_chunk g i s o
 130
 131   lemma subset_valid :
 132     forall s g h.
 133       well_formed_sudoku s /\ included g h /\ valid s h -> valid s g
 134
 135   (** A solution of a grid `data` is a full grid `sol`
 136      that is valid and includes `data` *)
 137   predicate is_solution_for (s:sudoku_chunks) (sol:grid) (data:grid) =
 138     included data sol /\ full sol /\ valid s sol
 139
 140
 141 end
 142
 143
 144 (** {2 Concrete Values of Chunks for the Classical Sudoku Grid} *)
 145 module TheClassicalSudokuGrid
 146
 147   use Grid
 148   use map.Map
 149   use int.Int
 150
 151   use array.Array
 152
 153   let classical_sudoku () : sudoku_chunks
 154     ensures { well_formed_sudoku result }
 155   =
 156     (* column start *)
 157     let cs = Array.make 81 0 in
 158     cs[ 0]<-0; cs[ 1]<-1; cs[ 2]<-2; cs[ 3]<-3; cs[ 4]<-4; cs[ 5]<-5;
 159     cs[ 6]<-6; cs[ 7]<-7; cs[ 8]<-8; cs[ 9]<-0; cs[10]<-1; cs[11]<-2;
 160     cs[12]<-3; cs[13]<-4; cs[14]<-5; cs[15]<-6; cs[16]<-7; cs[17]<-8;
 161     cs[18]<-0; cs[19]<-1; cs[20]<-2; cs[21]<-3; cs[22]<-4; cs[23]<-5;
 162     cs[24]<-6; cs[25]<-7; cs[26]<-8; cs[27]<-0; cs[28]<-1; cs[29]<-2;
 163     cs[30]<-3; cs[31]<-4; cs[32]<-5; cs[33]<-6; cs[34]<-7; cs[35]<-8;
 164     cs[36]<-0; cs[37]<-1; cs[38]<-2; cs[39]<-3; cs[40]<-4; cs[41]<-5;
 165     cs[42]<-6; cs[43]<-7; cs[44]<-8; cs[45]<-0; cs[46]<-1; cs[47]<-2;
 166     cs[48]<-3; cs[49]<-4; cs[50]<-5; cs[51]<-6; cs[52]<-7; cs[53]<-8;
 167     cs[54]<-0; cs[55]<-1; cs[56]<-2; cs[57]<-3; cs[58]<-4; cs[59]<-5;
 168     cs[60]<-6; cs[61]<-7; cs[62]<-8; cs[63]<-0; cs[64]<-1; cs[65]<-2;
 169     cs[66]<-3; cs[67]<-4; cs[68]<-5; cs[69]<-6; cs[70]<-7; cs[71]<-8;
 170     cs[72]<-0; cs[73]<-1; cs[74]<-2; cs[75]<-3; cs[76]<-4; cs[77]<-5;
 171     cs[78]<-6; cs[79]<-7; cs[80]<-8;
 172     (* column offset *)
 173     let co = Array.make 9 0 in
 174     co[ 0]<-0; co[ 1]<-9; co[ 2]<-18; co[ 3]<-27; co[ 4]<-36; co[
 175     5]<-45; co[ 6]<-54; co[ 7]<-63; co[ 8]<-72;
 176     (* row start *)
 177     let rs = Array.make 81 0 in
 178     rs[ 0]<- 0; rs[ 1]<- 0; rs[ 2]<- 0; rs[ 3]<- 0; rs[ 4]<-0; rs[5]<-0;
 179     rs[ 6]<- 0; rs[ 7]<- 0; rs[ 8]<- 0; rs[ 9]<- 9; rs[10]<-9; rs[11]<-9;
 180     rs[12]<- 9; rs[13]<- 9; rs[14]<- 9; rs[15]<- 9; rs[16]<-9; rs[17]<-9;
 181     rs[18]<-18; rs[19]<-18; rs[20]<-18; rs[21]<-18; rs[22]<-18;
 182     rs[23]<-18; rs[24]<-18; rs[25]<-18; rs[26]<-18; rs[27]<-27;
 183     rs[28]<-27; rs[29]<-27; rs[30]<-27; rs[31]<-27; rs[32]<-27;
 184     rs[33]<-27; rs[34]<-27; rs[35]<-27; rs[36]<-36; rs[37]<-36;
 185     rs[38]<-36; rs[39]<-36; rs[40]<-36; rs[41]<-36; rs[42]<-36;
 186     rs[43]<-36; rs[44]<-36; rs[45]<-45; rs[46]<-45; rs[47]<-45;
 187     rs[48]<-45; rs[49]<-45; rs[50]<-45; rs[51]<-45; rs[52]<-45;
 188     rs[53]<-45; rs[54]<-54; rs[55]<-54; rs[56]<-54; rs[57]<-54;
 189     rs[58]<-54; rs[59]<-54; rs[60]<-54; rs[61]<-54; rs[62]<-54;
 190     rs[63]<-63; rs[64]<-63; rs[65]<-63; rs[66]<-63; rs[67]<-63;
 191     rs[68]<-63; rs[69]<-63; rs[70]<-63; rs[71]<-63; rs[72]<-72;
 192     rs[73]<-72; rs[74]<-72; rs[75]<-72; rs[76]<-72; rs[77]<-72;
 193     rs[78]<-72; rs[79]<-72; rs[80]<-72;
 194     (* row offset *)
 195     let ro = Array.make 9 0 in
 196     ro[ 0]<-0; ro[ 1]<-1; ro[ 2]<-2; ro[ 3]<-3; ro[ 4]<-4; ro[ 5]<-5;
 197     ro[ 6]<-6; ro[ 7]<-7; ro[ 8]<-8;
 198     (* square start *)
 199     let ss = Array.make 81 0 in
 200     ss[ 0]<- 0; ss[ 1]<- 0; ss[ 2]<- 0; ss[ 3]<- 3; ss[ 4]<- 3;
 201     ss[ 5]<- 3; ss[ 6]<- 6; ss[ 7]<- 6; ss[ 8]<- 6; ss[ 9]<- 0;
 202     ss[10]<- 0; ss[11]<- 0; ss[12]<- 3; ss[13]<- 3; ss[14]<- 3; ss[15]<- 6;
 203     ss[16]<- 6; ss[17]<- 6; ss[18]<- 0; ss[19]<- 0; ss[20]<- 0;
 204     ss[21]<- 3; ss[22]<- 3; ss[23]<- 3; ss[24]<- 6; ss[25]<- 6;
 205     ss[26]<- 6; ss[27]<-27; ss[28]<-27; ss[29]<-27; ss[30]<-30;
 206     ss[31]<-30; ss[32]<-30; ss[33]<-33; ss[34]<-33; ss[35]<-33;
 207     ss[36]<-27; ss[37]<-27; ss[38]<-27; ss[39]<-30; ss[40]<-30;
 208     ss[41]<-30; ss[42]<-33; ss[43]<-33; ss[44]<-33; ss[45]<-27;
 209     ss[46]<-27; ss[47]<-27; ss[48]<-30; ss[49]<-30; ss[50]<-30;
 210     ss[51]<-33; ss[52]<-33; ss[53]<-33; ss[54]<-54; ss[55]<-54;
 211     ss[56]<-54; ss[57]<-57; ss[58]<-57; ss[59]<-57; ss[60]<-60;
 212     ss[61]<-60; ss[62]<-60; ss[63]<-54; ss[64]<-54; ss[65]<-54;
 213     ss[66]<-57; ss[67]<-57; ss[68]<-57; ss[69]<-60; ss[70]<-60;
 214     ss[71]<-60; ss[72]<-54; ss[73]<-54; ss[74]<-54; ss[75]<-57;
 215     ss[76]<-57; ss[77]<-57; ss[78]<-60; ss[79]<-60; ss[80]<-60;
 216     (* square offset *)
 217     let sqo = Array.make 9 0 in
 218     sqo[0]<-0; sqo[1]<-1; sqo[2]<-2; sqo[3]<-9; sqo[4]<-10;
 219     sqo[5]<-11; sqo[6]<-18; sqo[7]<-19; sqo[8]<-20;
 220     { column_start = cs; column_offsets = co;
 221       row_start    = rs; row_offsets    = ro;
 222       square_start = ss; square_offsets = sqo; }
 223
 224 end
 225
 226
 227
 228 (** {2 A Sudoku Solver} *)
 229
 230 module Solver
 231
 232   use Grid
 233   use array.Array
 234   use int.Int
 235
 236   (** predicate for the loop invariant of next function *)
 237   predicate valid_chunk_up_to (g:grid) (i:int)
 238     (start:array int) (offsets:array int) (off:int) =
 239     let s = start[i] in
 240     forall o1 o2 : int.
 241       0 <= o1 < off /\ 0 <= o2 < off /\ o1 <> o2 ->
 242       let i1 = s + offsets[o1] in
 243       let i2 = s + offsets[o2] in
 244       1 <= Map.get g i1 <= 9 /\ 1 <= Map.get g i2 <= 9 ->
 245       Map.get g i1 <> Map.get g i2
 246
 247   exception Invalid
 248
 249   use array.Array
 250
 251   (** `check_valid_chunk g i start offsets` checks the validity
 252       of the chunk that includes `i` *)
 253   let check_valid_chunk (g:array int) (i:int)
 254     (start:array int) (offsets:array int) : unit
 255     requires { g.length = 81 }
 256     requires { valid_values g.elts }
 257     requires { is_index i }
 258     requires { chunk_valid_indexes start offsets }
 259     ensures { valid_chunk g.elts i start offsets }
 260     raises { Invalid -> not (valid_chunk g.elts i start offsets) }
 261   =
 262     let s = start[i] in
 263     let b = Array.make 10 False in
 264     for off = 0 to 8 do
 265       invariant { valid_chunk_up_to g.elts i start offsets off }
 266       invariant { forall o:int. 0 <= o < off ->
 267          let v = g[s + offsets[o]] in
 268          1 <= v <= 9 -> b[v] = True }
 269       invariant { forall j:int. 1 <= j <= 9 ->
 270          b[j] = True ->
 271          exists o:int.
 272            0 <= o < off /\ Map.get g.elts (s + offsets[o]) = j }
 273       let v = g[s + offsets[off]] in
 274       if 1 <= v && v <= 9 then
 275          begin
 276            if b[v] then raise Invalid;
 277             b[v] <- True
 278          end
 279     done
 280
 281   (** predicate for the loop invariant of next function *)
 282   predicate valid_up_to (s:sudoku_chunks) (g:grid) (i:int) =
 283     forall j : int. 0 <= j < i ->
 284       valid_column s g j /\ valid_row s g j /\ valid_square s g j
 285
 286   (** `check_valid s g` checks if the (possibly partially filled) grid
 287       `g` is valid. (This function is not needed by the solver) *)
 288   let check_valid (s:sudoku_chunks) (g : array int) : bool
 289     requires { well_formed_sudoku s }
 290     requires { g.length = 81 }
 291     requires { valid_values g.elts }
 292     ensures { result <-> valid s g.elts }
 293   =
 294    try
 295     for i = 0 to 80 do
 296       invariant { valid_up_to s g.elts i }
 297       check_valid_chunk g i s.column_start s.column_offsets;
 298       check_valid_chunk g i s.row_start s.row_offsets;
 299       check_valid_chunk g i s.square_start s.square_offsets
 300     done;
 301     True
 302     with Invalid -> False
 303     end
 304
 305   (** `full_up_to g i` is true when all cells `0..i-1` in grid `g` are
 306       non empty *)
 307   predicate full_up_to (g : grid) (i : int) = forall j :
 308   int. 0 <= j < i -> 1 <= Map.get g j <= 9
 309
 310   lemma full_up_to_change :
 311     forall g i x. is_index i /\ full_up_to g i
 312     -> 1 <= x <= 9 -> full_up_to (Map.set g i x) (i+1)
 313
 314   let rec lemma full_up_to_frame (g1 g2:grid) (i:int)
 315     requires { 0 <= i <= 81 }
 316     requires { grid_eq_sub g1 g2 0 i }
 317     requires { full_up_to g1 i }
 318     variant  { i }
 319     ensures  { full_up_to g2 i }
 320   = if i > 0 then
 321       begin
 322         assert { full_up_to g1 (i-1) };
 323         full_up_to_frame g1 g2 (i-1)
 324       end
 325
 326   let lemma full_up_to_frame_all (g1 g2:grid) (i:int)
 327     requires { 0 <= i <= 81 }
 328     requires { grid_eq g1 g2 }
 329     requires { full_up_to g1 i }
 330     ensures  { full_up_to g2 i }
 331   = assert { grid_eq_sub g1 g2 0 i }
 332
 333   let lemma valid_chunk_frame (start:array int) (offsets:array int) (g1 g2:grid) (i:int)
 334     requires { chunk_valid_indexes start offsets }
 335     requires { 0 <= i < 81 }
 336     requires { grid_eq g1 g2 }
 337     requires { valid_chunk g1 i start offsets }
 338     ensures  { valid_chunk g2 i start offsets }
 339   = ()
 340
 341   let rec lemma valid_up_to_frame (s:sudoku_chunks) (g1 g2:grid) (i:int)
 342     requires { well_formed_sudoku s }
 343     requires { 0 <= i <= 81 }
 344     requires { grid_eq g1 g2 }
 345     requires { valid_up_to s g1 i }
 346     variant  { i }
 347     ensures  { valid_up_to s g2 i }
 348   = if i > 0 then
 349       begin
 350         assert { valid_up_to s g1 (i-1) };
 351         valid_up_to_frame s g1 g2 (i-1);
 352         valid_chunk_frame s.column_start s.column_offsets g1 g2 (i-1);
 353         valid_chunk_frame s.row_start s.row_offsets g1 g2 (i-1);
 354         valid_chunk_frame s.square_start s.square_offsets g1 g2 (i-1);
 355       end
 356
 357
 358
 359 (** how to prove the "hard" property : if
 360
 361    `valid_up_to s g i`
 362
 363 and
 364
 365   `h = g[i <- k`    (with 1 <= k <= 9)]
 366
 367 and
 368
 369   `valid_column s h i /\ valid_row s h i /\ valid_square s h i`
 370
 371 then
 372
 373   `valid_up_to s h (i+1)`
 374
 375 then the problem is that one should prove that for each `j` in `0..i-1` :
 376
 377   `valid_column s h j /\ valid_row s h j /\ valid_square s h j`
 378
 379 this is true but with 2 different possible reasons:
 380
 381   if `column_start j = column_start i` then
 382     `valid_column s h j` is true because `valid_column s h i` is true
 383   else
 384     `valid_column s h j` is true because `valid_column s g j` is true
 385     because `valid_column s h j` does not depend on `h[i]`
 386
 387 *)
 388
 389
 390
 391   lemma valid_unchanged_chunks:
 392     forall g : grid, i1 i2 k:int, start offsets:array int.
 393       disjoint_chunks start offsets ->
 394       is_index i1 /\ is_index i2 /\ 1 <= k <= 9 ->
 395       let s1 = start[i1] in
 396       let s2 = start[i2] in
 397       let h = Map.set g i1 k in
 398       s1 <> s2 /\ valid_chunk g i2 start offsets ->
 399       valid_chunk h i2 start offsets
 400
 401   lemma valid_changed_chunks:
 402     forall g : grid, i1 i2 k:int, start offsets:array int.
 403       is_index i1 /\ is_index i2 /\ 1 <= k <= 9 ->
 404       let s1 = start[i1] in
 405       let s2 = start[i2] in
 406       let h = Map.set g i1 k in
 407       s1 = s2 /\ valid_chunk h i1 start offsets ->
 408       valid_chunk h i2 start offsets
 409
 410
 411   let ghost valid_up_to_change (s:sudoku_chunks) (g:grid) (i x : int)
 412     requires {  well_formed_sudoku s }
 413     requires { is_index i }
 414     requires { valid_up_to s g i }
 415     requires { 1 <= x <= 9 }
 416     requires { valid_column s (Map.set g i x) i }
 417     requires { valid_row s (Map.set g i x) i }
 418     requires { valid_square s (Map.set g i x) i }
 419     ensures  { valid_up_to s (Map.set g i x) (i+1) }
 420   = ()
 421
 422
 423   (** {3 The main solver loop} *)
 424   exception SolutionFound
 425
 426   let rec solve_aux (s:sudoku_chunks) (g : array int) (i : int)
 427     requires { well_formed_sudoku s }
 428     requires { g.length = 81 }
 429     requires { valid_values g.elts }
 430     requires { 0 <= i <= 81 }
 431     requires { valid_up_to s g.elts i }
 432     requires { full_up_to g.elts i }
 433     writes  { g }
 434     variant { 81 - i }
 435     ensures { grid_eq (old g).elts g.elts }
 436     ensures { forall h : grid. included g.elts h /\ full h -> not (valid s h) }
 437     raises { SolutionFound -> is_solution_for s g.elts (old g).elts }
 438   = if i = 81 then raise SolutionFound;
 439     (* assert { is_index i }; *)
 440     if g[i] <> 0 then
 441       try
 442         (* assert { 1 <= g[i] <= 9 }; *)
 443         check_valid_chunk g i s.column_start s.column_offsets;
 444         check_valid_chunk g i s.row_start s.row_offsets;
 445         check_valid_chunk g i s.square_start s.square_offsets;
 446         solve_aux s g (i + 1)
 447       with Invalid -> ()
 448       end
 449     else
 450       begin
 451       let ghost old_g = g.elts in
 452       for k = 1 to 9 do
 453         invariant { grid_eq old_g (Map.set g.elts i 0) }
 454         invariant { full_up_to g.elts i }
 455         invariant { (* for completeness *)
 456           forall k'. 1 <= k' < k ->
 457           let g' = Map.set old_g i k' in
 458           forall h : grid. included g' h /\ full h -> not (valid s h) }
 459         g[i] <- k;
 460         valid_up_to_frame s old_g (Map.set g.elts i 0) i;
 461         try
 462           check_valid_chunk g i s.column_start s.column_offsets;
 463           check_valid_chunk g i s.row_start s.row_offsets;
 464           check_valid_chunk g i s.square_start s.square_offsets;
 465             (* the hard part: see lemma valid_up_to_change *)
 466           assert { let grid' = Map.set old_g i k in
 467             grid_eq grid' g.elts &&
 468             valid_chunk grid' i s.column_start s.column_offsets &&
 469             valid_chunk grid' i s.row_start s.row_offsets &&
 470             valid_chunk grid' i s.square_start s.square_offsets &&
 471             valid_up_to s grid' (i+1) };
 472           valid_up_to_change s old_g i k;
 473           solve_aux s g (i + 1)
 474         with Invalid ->
 475           assert { (* for completeness *)
 476             not (valid s (Map.set old_g i k)) };
 477           assert { (* for completeness *)
 478             let g' = Map.set old_g i k in
 479             forall h : grid. included g' h /\ full h -> not (valid s h) }
 480         end
 481       done;
 482       g[i] <- 0;
 483       assert { (* for completeness *)
 484         forall h:grid. included old_g h /\ full h ->
 485           let k' = Map.get h i in
 486           let g' = Map.set old_g i k' in
 487           included g' h }
 488       end
 489
 490   exception NoSolution
 491
 492   let solve (s:sudoku_chunks) (g : array int)
 493     requires { well_formed_sudoku s }
 494     requires { g.length = 81 }
 495     requires { valid_values g.elts }
 496     writes   { g }
 497     ensures  { result = g }
 498     ensures  { is_solution_for s g.elts (old g).elts }
 499     raises   { NoSolution ->
 500       forall h : grid. included g.elts h /\ full h -> not (valid s h)  }
 501   =
 502     try solve_aux s g 0;
 503         raise NoSolution
 504     with SolutionFound -> g
 505     end
 506
 507   let check_then_solve (s:sudoku_chunks) (g : array int)
 508     requires { well_formed_sudoku s }
 509     requires { g.length = 81 }
 510     requires { valid_values g.elts }
 511     writes   { g }
 512     ensures  { result = g }
 513     ensures  { is_solution_for s g.elts (old g).elts }
 514     raises   { NoSolution ->
 515       forall h : grid. included g.elts h /\ full h -> not (valid s h)  }
 516   =
 517     if check_valid s g then solve s g else raise NoSolution
 518
 519 end
 520
 521 (* Proof in progress
 522 module RandomSolver
 523
 524   (* a variant: solve using a random order of cells *)
 525
 526   use Grid
 527   use array.Array
 528   use int.Int
 529   use random.Random
 530
 531   use Solver
 532
 533   let rec solve_aux (s:sudoku_chunks) (randoffset:int) (g : array int) (i : int)
 534     requires { well_formed_sudoku s }
 535     requires { 0 <= randoffset <= 80 }
 536     requires { g.length = 81 }
 537     requires { valid_values g.elts }
 538     requires { 0 <= i <= 81 }
 539     requires { valid_up_to s g.elts i }
 540     requires { full_up_to g.elts i }
 541     writes  { g }
 542     variant { 81 - i }
 543     ensures { grid_eq (old g).elts g.elts }
 544     ensures { forall h : grid. included g.elts h /\ full h -> not (valid s h) }
 545     raises { SolutionFound -> is_solution_for s g.elts (old g).elts }
 546   = if i = 81 then raise SolutionFound;
 547     (* assert { is_index i }; *)
 548     let j = i + randoffset in
 549     let j = if j >= 81 then j - 81 else j in
 550     (* assert { is_index j }; *)
 551     if g[j] <> 0 then
 552       try
 553         (* assert { 1 <= g[j] <= 9 }; *)
 554         Solver.check_valid_chunk g j s.column_start s.column_offsets;
 555         check_valid_chunk g j s.row_start s.row_offsets;
 556         check_valid_chunk g j s.square_start s.square_offsets;
 557         solve_aux s randoffset g (i + 1)
 558       with Invalid -> ()
 559       end
 560     else
 561       begin
 562       label L in
 563       for k = 1 to 9 do
 564         invariant { grid_eq (g at L).elts (Map.set g.elts j 0) }
 565         invariant { full_up_to g.elts i } (* TODO i -> j *)
 566         invariant { (* for completeness *)
 567           forall k'. 1 <= k' < k ->
 568           let g' = Map.set (g at L).elts i k' in (* TODO i -> j *)
 569           forall h : grid. included g' h /\ full h -> not (valid s h) }
 570         g[j] <- k;
 571         try
 572           check_valid_chunk g j s.column_start s.column_offsets;
 573           check_valid_chunk g j s.row_start s.row_offsets;
 574           check_valid_chunk g j s.square_start s.square_offsets;
 575             (* the hard part: see lemma valid_up_to_change *)
 576             (* TODO i -> j *)
 577           assert { let grid' = Map.set (g at L).elts i k in
 578             grid_eq grid' g.elts &&
 579             valid_chunk grid' i s.column_start s.column_offsets &&
 580             valid_chunk grid' i s.row_start s.row_offsets &&
 581             valid_chunk grid' i s.square_start s.square_offsets &&
 582             valid_up_to s grid' (i+1) };
 583           assert { valid_up_to s g.elts (i+1) };
 584           solve_aux s randoffset g (i + 1)
 585         with Invalid ->
 586           assert { (* for completeness *)
 587             not (valid s (Map.set (g at L).elts i k)) };
 588           assert { (* for completeness *)
 589             let g' = Map.set (g at L).elts i k in
 590             forall h : grid. included g' h /\ full h -> not (valid s h) }
 591         end
 592       done;
 593       g[j] <- 0;
 594       assert { (* for completeness *)
 595         forall h:grid. included (g at L).elts h /\ full h ->
 596           let k' = Map.get h i in
 597           let g' = Map.set (g at L).elts i k' in
 598           included g' h }
 599       end
 600
 601   exception NoSolution
 602
 603   let solve (s:sudoku_chunks) (g : array int)
 604     requires { well_formed_sudoku s }
 605     requires { g.length = 81 }
 606     requires { valid_values g.elts }
 607     writes   { g }
 608     ensures  { result = g }
 609     ensures  { is_solution_for s g.elts (old g).elts }
 610     raises   { NoSolution ->
 611       forall h : grid. included g.elts h /\ full h -> not (valid s h)  }
 612   =
 613     try
 614       let randoffset = 27 in
 615       solve_aux s randoffset g 0;
 616       raise NoSolution
 617     with SolutionFound -> g
 618     end
 619
 620   let check_then_solve (s:sudoku_chunks) (g : array int)
 621     requires { well_formed_sudoku s }
 622     requires { g.length = 81 }
 623     requires { valid_values g.elts }
 624     writes   { g }
 625     ensures  { result = g }
 626     ensures  { is_solution_for s g.elts (old g).elts }
 627     raises   { NoSolution ->
 628       forall h : grid. included g.elts h /\ full h -> not (valid s h)  }
 629   =
 630     if check_valid s g then solve s g else raise NoSolution
 631
 632 end
 633 *)
 634
 635
 636 (** {2 Some Tests} *)
 637
 638 module Test
 639
 640   use Grid
 641   use TheClassicalSudokuGrid
 642
 643   use Solver
 644   use map.Map
 645   use array.Array
 646
 647   (** Solving the empty grid: easy, yet not trivial *)
 648   let test0 ()
 649     raises { NoSolution -> true }
 650   = let a = Array.make 81 0 in
 651     solve (classical_sudoku()) a
 652 (* a possible solution:
 653   1, 2, 3, 4, 5, 6, 7, 8, 9,
 654   4, 5, 6, 7, 8, 9, 1, 2, 3,
 655   7, 8, 9, 1, 2, 3, 4, 5, 6,
 656   2, 1, 4, 3, 6, 5, 8, 9, 7,
 657   3, 6, 5, 8, 9, 7, 2, 1, 4,
 658   8, 9, 7, 2, 1, 4, 3, 6, 5,
 659   5, 3, 1, 6, 4, 2, 9, 7, 8,
 660   6, 4, 2, 9, 7, 8, 5, 3, 1,
 661   9, 7, 8, 5, 3, 1, 6, 4, 2
 662 *)
 663
 664 (** A grid known to be solvable *)
 665 (*
 666 2 0 9 0 0 0 0 1 0
 667 0 0 0 0 6 0 0 0 0
 668 0 5 3 8 0 2 7 0 0
 669 3 0 0 0 0 0 0 0 0
 670 0 0 0 0 7 5 0 0 3
 671 0 4 1 2 0 8 9 0 0
 672 0 0 4 0 9 0 0 2 0
 673 8 0 0 0 0 1 0 0 5
 674 0 0 0 0 0 0 0 7 6
 675 *)
 676
 677   let test1 ()
 678     raises { NoSolution -> true }
 679   = let a = Array.make 81 0 in
 680     a[0] <- 2;
 681     a[2] <- 9;
 682     a[7] <- 1;
 683     a[13] <- 6;
 684     a[19] <- 5;
 685     a[20] <- 3;
 686     a[21] <- 8;
 687     a[23] <- 2;
 688     a[24] <- 7;
 689     a[27] <- 3;
 690     a[40] <- 7;
 691     a[41] <- 5;
 692     a[44] <- 3;
 693     a[46] <- 4;
 694     a[47] <- 1;
 695     a[48] <- 2;
 696     a[50] <- 8;
 697     a[51] <- 9;
 698     a[56] <- 4;
 699     a[58] <- 9;
 700     a[61] <- 2;
 701     a[63] <- 8;
 702     a[68] <- 1;
 703     a[71] <- 5;
 704     a[79] <- 7;
 705     a[80] <- 6;
 706     assert { valid_values a.Array.elts };
 707     solve (classical_sudoku()) a
 708
 709 (* the solution:
 710
 711   2, 6, 9, 3, 5, 7, 8, 1, 4,
 712   1, 8, 7, 9, 6, 4, 5, 3, 2,
 713   4, 5, 3, 8, 1, 2, 7, 6, 9,
 714   3, 7, 5, 6, 4, 9, 2, 8, 1,
 715   9, 2, 8, 1, 7, 5, 6, 4, 3,
 716   6, 4, 1, 2, 3, 8, 9, 5, 7,
 717   7, 1, 4, 5, 9, 6, 3, 2, 8,
 718   8, 3, 6, 7, 2, 1, 4, 9, 5,
 719   5, 9, 2, 4, 8, 3, 1, 7, 6
 720
 721 *)
 722
 723   (** A trivially unsolvable grid *)
 724   let test2 ()
 725     raises { NoSolution -> true }
 726   = let a = Array.make 81 1 in
 727     solve (classical_sudoku()) a
 728
 729 end
 730
 731 (***
 732 Local Variables:
 733 compile-command: "why3 ide --extra-config ../share/strategies.conf sudoku.mlw"
 734 End:
 735 *)