sudoku.mlw 23.4 KB
Newer Older
1

2 3 4 5
(** {1 An Efficient Sudoku Solver }

    Author: Claude Marché       (Inria)
            Guillaume Melquiond (Inria) *)
6 7 8 9


(** {2 A theory of 9x9 grids} *)

10
module Grid
11

12 13
  use int.Int
  use map.Map
14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48

  (** A grid is a map from integers to integers *)
  type grid = map int int

  (** valid indexes are 0..80 *)
  predicate is_index (i:int) = 0 <= i < 81

  (** valid values are 0..9. 0 denotes an empty cell *)
  predicate valid_values (g:grid) =
    forall i. is_index i -> 0 <= g[i] <= 9

  (** extensional equality of grids and sub-grids *)
  predicate grid_eq_sub (g1 g2:grid) (a b:int) =
    forall j. a <= j < b -> g1[j] = g2[j]

  predicate grid_eq (g1 g2:grid) = grid_eq_sub g1 g2 0 81

  lemma grid_eq_sub:
    forall g1 g2 a b. 0 <= a <= 81 /\ 0 <= b <= 81 /\
        grid_eq g1 g2 -> grid_eq_sub g1 g2 a b

  (** {3 Grid "Chunks"}

   A chunk is either a column, a row or a square.

   A chunk is defined by a starting index s and a set of 9 offsets
   {o0,..,o8}, that thus denotes a set of 9 cells {s+o0,..,s+o8} in a
   grid.

   Each cell of the grid belongs to 3 chunks, one of each kind.  For
   each cell index, there is a unique starting index respectively for
   the column, the row and the square it belongs to.

  *)

49
  use array.Array
50

51
  type sudoku_chunks =
52 53 54 55 56 57
    { column_start : array int;
      column_offsets : array int;
      row_start : array int;
      row_offsets : array int;
      square_start : array int;
      square_offsets : array int;
58 59 60
    }

  (** Chunks must point to valid indexes of the grid *)
61 62 63 64
  predicate chunk_valid_indexes (start:array int) (offsets:array int) =
    start.length = 81 /\ offsets.length = 9 /\
    forall i o:int. is_index i /\ 0 <= o < 9 ->
      is_index(start[i] + offsets[o])
65 66 67

  (** Chunks (of the same kind column, row or square) with distinct
      starting cells must be disjoint *)
68 69
  predicate disjoint_chunks (start:array int) (offsets:array int) =
    start.length = 81 /\ offsets.length = 9 /\
70 71
    forall i1 i2 o:int.
       is_index i1 /\ is_index i2 /\ 0 <= o < 9 ->
72 73 74
       let s1 = start[i1] in
       let s2 = start[i2] in
       s1 <> s2 -> i1 <> s2 + offsets[o]
75 76 77 78 79 80 81 82 83 84 85 86

  (** A sudoku grid is well formed when chunks are valid and disjoint *)
  predicate well_formed_sudoku (s:sudoku_chunks) =
    chunk_valid_indexes s.column_start s.column_offsets /\
    chunk_valid_indexes s.row_start s.row_offsets /\
    chunk_valid_indexes s.square_start s.square_offsets /\
    disjoint_chunks s.column_start s.column_offsets /\
    disjoint_chunks s.row_start s.row_offsets /\
    disjoint_chunks s.square_start s.square_offsets

  (** {3 Valid Sudoku Solutions} *)

87 88
  (** `valid_chunk g i start offsets` is true whenever the chunk
  denoted by `start,offsets` from cell `i` is "valid" in grid `g`, in
89 90 91 92
  the sense that it contains at most one occurence of each number
  between 1 and 9 *)

  predicate valid_chunk (g:grid) (i:int)
93
    (start:array int) (offsets:array int) =
94 95 96 97
    let s = start[i] in
    forall o1 o2 : int. 0 <= o1 < 9 /\ 0 <= o2 < 9 /\ o1 <> o2 ->
      let i1 = s + offsets[o1] in
      let i2 = s + offsets[o2] in
98 99
      1 <= Map.get g i1 <= 9 /\ 1 <= Map.get g i2 <= 9 ->
      Map.get g i1 <> Map.get g i2
100 101 102 103 104 105 106 107 108 109

  predicate valid_column (s:sudoku_chunks) (g:grid) (i:int) =
    valid_chunk g i s.column_start s.column_offsets

  predicate valid_row (s:sudoku_chunks) (g:grid) (i:int) =
    valid_chunk g i s.row_start s.row_offsets

  predicate valid_square (s:sudoku_chunks) (g:grid) (i:int) =
    valid_chunk g i s.square_start s.square_offsets

110
  (** `valid g` is true when all chunks are valid *)
111 112 113 114
  predicate valid (s:sudoku_chunks) (g : grid) =
    forall i : int. is_index i ->
      valid_column s g i /\ valid_row s g i /\ valid_square s g i

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 125 126

  (** validity is monotonic w.r.t. inclusion *)
  lemma subset_valid_chunk :
    forall g h : grid. included g h ->
127
      forall i:int, s o:array int. is_index i /\
128 129 130 131
      chunk_valid_indexes s o /\ valid_chunk h i s o ->
        valid_chunk g i s o

  lemma subset_valid :
132
    forall s g h.
133 134
      well_formed_sudoku s /\ included g h /\ valid s h -> valid s g

135 136
  (** A solution of a grid `data` is a full grid `sol`
     that is valid and includes `data` *)
137 138 139 140 141 142 143 144
  predicate is_solution_for (s:sudoku_chunks) (sol:grid) (data:grid) =
    included data sol /\ full sol /\ valid s sol


end


(** {2 Concrete Values of Chunks for the Classical Sudoku Grid} *)
145
module TheClassicalSudokuGrid
146

147 148 149
  use Grid
  use map.Map
  use int.Int
150

151
  use array.Array
152

153 154 155
  let classical_sudoku () : sudoku_chunks
    ensures { well_formed_sudoku result }
  =
156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
    (* column start *)
    let cs = Array.make 81 0 in
    cs[ 0]<-0; cs[ 1]<-1; cs[ 2]<-2; cs[ 3]<-3; cs[ 4]<-4; cs[ 5]<-5;
    cs[ 6]<-6; cs[ 7]<-7; cs[ 8]<-8; cs[ 9]<-0; cs[10]<-1; cs[11]<-2;
    cs[12]<-3; cs[13]<-4; cs[14]<-5; cs[15]<-6; cs[16]<-7; cs[17]<-8;
    cs[18]<-0; cs[19]<-1; cs[20]<-2; cs[21]<-3; cs[22]<-4; cs[23]<-5;
    cs[24]<-6; cs[25]<-7; cs[26]<-8; cs[27]<-0; cs[28]<-1; cs[29]<-2;
    cs[30]<-3; cs[31]<-4; cs[32]<-5; cs[33]<-6; cs[34]<-7; cs[35]<-8;
    cs[36]<-0; cs[37]<-1; cs[38]<-2; cs[39]<-3; cs[40]<-4; cs[41]<-5;
    cs[42]<-6; cs[43]<-7; cs[44]<-8; cs[45]<-0; cs[46]<-1; cs[47]<-2;
    cs[48]<-3; cs[49]<-4; cs[50]<-5; cs[51]<-6; cs[52]<-7; cs[53]<-8;
    cs[54]<-0; cs[55]<-1; cs[56]<-2; cs[57]<-3; cs[58]<-4; cs[59]<-5;
    cs[60]<-6; cs[61]<-7; cs[62]<-8; cs[63]<-0; cs[64]<-1; cs[65]<-2;
    cs[66]<-3; cs[67]<-4; cs[68]<-5; cs[69]<-6; cs[70]<-7; cs[71]<-8;
    cs[72]<-0; cs[73]<-1; cs[74]<-2; cs[75]<-3; cs[76]<-4; cs[77]<-5;
    cs[78]<-6; cs[79]<-7; cs[80]<-8;
    (* column offset *)
    let co = Array.make 9 0 in
    co[ 0]<-0; co[ 1]<-9; co[ 2]<-18; co[ 3]<-27; co[ 4]<-36; co[
    5]<-45; co[ 6]<-54; co[ 7]<-63; co[ 8]<-72;
    (* row start *)
    let rs = Array.make 81 0 in
    rs[ 0]<- 0; rs[ 1]<- 0; rs[ 2]<- 0; rs[ 3]<- 0; rs[ 4]<-0; rs[5]<-0;
    rs[ 6]<- 0; rs[ 7]<- 0; rs[ 8]<- 0; rs[ 9]<- 9; rs[10]<-9; rs[11]<-9;
    rs[12]<- 9; rs[13]<- 9; rs[14]<- 9; rs[15]<- 9; rs[16]<-9; rs[17]<-9;
    rs[18]<-18; rs[19]<-18; rs[20]<-18; rs[21]<-18; rs[22]<-18;
    rs[23]<-18; rs[24]<-18; rs[25]<-18; rs[26]<-18; rs[27]<-27;
    rs[28]<-27; rs[29]<-27; rs[30]<-27; rs[31]<-27; rs[32]<-27;
    rs[33]<-27; rs[34]<-27; rs[35]<-27; rs[36]<-36; rs[37]<-36;
    rs[38]<-36; rs[39]<-36; rs[40]<-36; rs[41]<-36; rs[42]<-36;
    rs[43]<-36; rs[44]<-36; rs[45]<-45; rs[46]<-45; rs[47]<-45;
    rs[48]<-45; rs[49]<-45; rs[50]<-45; rs[51]<-45; rs[52]<-45;
    rs[53]<-45; rs[54]<-54; rs[55]<-54; rs[56]<-54; rs[57]<-54;
    rs[58]<-54; rs[59]<-54; rs[60]<-54; rs[61]<-54; rs[62]<-54;
    rs[63]<-63; rs[64]<-63; rs[65]<-63; rs[66]<-63; rs[67]<-63;
    rs[68]<-63; rs[69]<-63; rs[70]<-63; rs[71]<-63; rs[72]<-72;
    rs[73]<-72; rs[74]<-72; rs[75]<-72; rs[76]<-72; rs[77]<-72;
    rs[78]<-72; rs[79]<-72; rs[80]<-72;
    (* row offset *)
    let ro = Array.make 9 0 in
    ro[ 0]<-0; ro[ 1]<-1; ro[ 2]<-2; ro[ 3]<-3; ro[ 4]<-4; ro[ 5]<-5;
    ro[ 6]<-6; ro[ 7]<-7; ro[ 8]<-8;
    (* square start *)
    let ss = Array.make 81 0 in
    ss[ 0]<- 0; ss[ 1]<- 0; ss[ 2]<- 0; ss[ 3]<- 3; ss[ 4]<- 3;
    ss[ 5]<- 3; ss[ 6]<- 6; ss[ 7]<- 6; ss[ 8]<- 6; ss[ 9]<- 0;
    ss[10]<- 0; ss[11]<- 0; ss[12]<- 3; ss[13]<- 3; ss[14]<- 3; ss[15]<- 6;
    ss[16]<- 6; ss[17]<- 6; ss[18]<- 0; ss[19]<- 0; ss[20]<- 0;
    ss[21]<- 3; ss[22]<- 3; ss[23]<- 3; ss[24]<- 6; ss[25]<- 6;
    ss[26]<- 6; ss[27]<-27; ss[28]<-27; ss[29]<-27; ss[30]<-30;
    ss[31]<-30; ss[32]<-30; ss[33]<-33; ss[34]<-33; ss[35]<-33;
    ss[36]<-27; ss[37]<-27; ss[38]<-27; ss[39]<-30; ss[40]<-30;
    ss[41]<-30; ss[42]<-33; ss[43]<-33; ss[44]<-33; ss[45]<-27;
    ss[46]<-27; ss[47]<-27; ss[48]<-30; ss[49]<-30; ss[50]<-30;
    ss[51]<-33; ss[52]<-33; ss[53]<-33; ss[54]<-54; ss[55]<-54;
    ss[56]<-54; ss[57]<-57; ss[58]<-57; ss[59]<-57; ss[60]<-60;
    ss[61]<-60; ss[62]<-60; ss[63]<-54; ss[64]<-54; ss[65]<-54;
    ss[66]<-57; ss[67]<-57; ss[68]<-57; ss[69]<-60; ss[70]<-60;
    ss[71]<-60; ss[72]<-54; ss[73]<-54; ss[74]<-54; ss[75]<-57;
    ss[76]<-57; ss[77]<-57; ss[78]<-60; ss[79]<-60; ss[80]<-60;
    (* square offset *)
217 218 219
    let sqo = Array.make 9 0 in
    sqo[0]<-0; sqo[1]<-1; sqo[2]<-2; sqo[3]<-9; sqo[4]<-10;
    sqo[5]<-11; sqo[6]<-18; sqo[7]<-19; sqo[8]<-20;
220 221
    { column_start = cs; column_offsets = co;
      row_start    = rs; row_offsets    = ro;
222
      square_start = ss; square_offsets = sqo; }
223 224 225 226 227 228 229 230 231

end



(** {2 A Sudoku Solver} *)

module Solver

232 233 234
  use Grid
  use array.Array
  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 240 241 242 243
    let s = start[i] in
    forall o1 o2 : int.
      0 <= o1 < off /\ 0 <= o2 < off /\ o1 <> o2 ->
      let i1 = s + offsets[o1] in
      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 248

  exception Invalid

249
  use array.Array
250

251 252
  (** `check_valid_chunk g i start offsets` checks the validity
      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 256 257 258 259 260 261
    requires { g.length = 81 }
    requires { valid_values g.elts }
    requires { is_index i }
    requires { chunk_valid_indexes start offsets }
    ensures { valid_chunk g.elts i start offsets }
    raises { Invalid -> not (valid_chunk g.elts i start offsets) }
  =
262
    let s = start[i] in
263 264 265 266
    let b = Array.make 10 False in
    for off = 0 to 8 do
      invariant { valid_chunk_up_to g.elts i start offsets off }
      invariant { forall o:int. 0 <= o < off ->
267
         let v = g[s + offsets[o]] in
268 269 270 271
         1 <= v <= 9 -> b[v] = True }
      invariant { forall j:int. 1 <= j <= 9 ->
         b[j] = True ->
         exists o:int.
272 273
           0 <= o < off /\ Map.get g.elts (s + offsets[o]) = j }
      let v = g[s + offsets[off]] in
274 275
      if 1 <= v && v <= 9 then
         begin
MARCHE Claude's avatar
MARCHE Claude committed
276
           if b[v] then raise Invalid;
277 278 279 280
            b[v] <- True
         end
    done

281
  (** predicate for the loop invariant of next function *)
282 283 284 285
  predicate valid_up_to (s:sudoku_chunks) (g:grid) (i:int) =
    forall j : int. 0 <= j < i ->
      valid_column s g j /\ valid_row s g j /\ valid_square s g j

286 287
  (** `check_valid s g` checks if the (possibly partially filled) grid
      `g` is valid. (This function is not needed by the solver) *)
288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304
  let check_valid (s:sudoku_chunks) (g : array int) : bool
    requires { well_formed_sudoku s }
    requires { g.length = 81 }
    requires { valid_values g.elts }
    ensures { result <-> valid s g.elts }
  =
   try
    for i = 0 to 80 do
      invariant { valid_up_to s g.elts i }
      check_valid_chunk g i s.column_start s.column_offsets;
      check_valid_chunk g i s.row_start s.row_offsets;
      check_valid_chunk g i s.square_start s.square_offsets
    done;
    True
    with Invalid -> False
    end

305
  (** `full_up_to g i` is true when all cells `0..i-1` in grid `g` are
306
      non empty *)
307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332
  predicate full_up_to (g : grid) (i : int) = forall j :
  int. 0 <= j < i -> 1 <= Map.get g j <= 9

  lemma full_up_to_change :
    forall g i x. is_index i /\ full_up_to g i
    -> 1 <= x <= 9 -> full_up_to (Map.set g i x) (i+1)

  let rec lemma full_up_to_frame (g1 g2:grid) (i:int)
    requires { 0 <= i <= 81 }
    requires { grid_eq_sub g1 g2 0 i }
    requires { full_up_to g1 i }
    variant  { i }
    ensures  { full_up_to g2 i }
  = if i > 0 then
      begin
        assert { full_up_to g1 (i-1) };
        full_up_to_frame g1 g2 (i-1)
      end

  let lemma full_up_to_frame_all (g1 g2:grid) (i:int)
    requires { 0 <= i <= 81 }
    requires { grid_eq g1 g2 }
    requires { full_up_to g1 i }
    ensures  { full_up_to g2 i }
  = assert { grid_eq_sub g1 g2 0 i }

MARCHE Claude's avatar
MARCHE Claude committed
333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356
  let lemma valid_chunk_frame (start:array int) (offsets:array int) (g1 g2:grid) (i:int)
    requires { chunk_valid_indexes start offsets }
    requires { 0 <= i < 81 }
    requires { grid_eq g1 g2 }
    requires { valid_chunk g1 i start offsets }
    ensures  { valid_chunk g2 i start offsets }
  = ()

  let rec lemma valid_up_to_frame (s:sudoku_chunks) (g1 g2:grid) (i:int)
    requires { well_formed_sudoku s }
    requires { 0 <= i <= 81 }
    requires { grid_eq g1 g2 }
    requires { valid_up_to s g1 i }
    variant  { i }
    ensures  { valid_up_to s g2 i }
  = if i > 0 then
      begin
        assert { valid_up_to s g1 (i-1) };
        valid_up_to_frame s g1 g2 (i-1);
	valid_chunk_frame s.column_start s.column_offsets g1 g2 (i-1);
	valid_chunk_frame s.row_start s.row_offsets g1 g2 (i-1);
	valid_chunk_frame s.square_start s.square_offsets g1 g2 (i-1);
      end

357 358 359 360


(** how to prove the "hard" property : if

361
   `valid_up_to s g i`
362 363 364

and

365
  `h = g[i <- k`    (with 1 <= k <= 9)]
366 367 368

and

369
  `valid_column s h i /\ valid_row s h i /\ valid_square s h i`
370 371 372

then

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 380

this is true but with 2 different possible reasons:

381 382
  if `column_start j = column_start i` then
    `valid_column s h j` is true because `valid_column s h i` is true
383
  else
384 385
    `valid_column s h j` is true because `valid_column s g j` is true
    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 394
      disjoint_chunks start offsets ->
      is_index i1 /\ is_index i2 /\ 1 <= k <= 9 ->
395 396
      let s1 = start[i1] in
      let s2 = start[i2] in
397 398 399 400 401
      let h = Map.set g i1 k in
      s1 <> s2 /\ valid_chunk g i2 start offsets ->
      valid_chunk h i2 start offsets

  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 405
      let s1 = start[i1] in
      let s2 = start[i2] in
406 407 408 409 410
      let h = Map.set g i1 k in
      s1 = s2 /\ valid_chunk h i1 start offsets ->
      valid_chunk h i2 start offsets


MARCHE Claude's avatar
MARCHE Claude committed
411 412 413 414 415 416 417 418 419 420
  let ghost valid_up_to_change (s:sudoku_chunks) (g:grid) (i x : int)
    requires {  well_formed_sudoku s }
    requires { is_index i }
    requires { valid_up_to s g i }
    requires { 1 <= x <= 9 }
    requires { valid_column s (Map.set g i x) i }
    requires { valid_row s (Map.set g i x) i }
    requires { valid_square s (Map.set g i x) i }
    ensures  { valid_up_to s (Map.set g i x) (i+1) }
  = ()
421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450


  (** {3 The main solver loop} *)
  exception SolutionFound

  let rec solve_aux (s:sudoku_chunks) (g : array int) (i : int)
    requires { well_formed_sudoku s }
    requires { g.length = 81 }
    requires { valid_values g.elts }
    requires { 0 <= i <= 81 }
    requires { valid_up_to s g.elts i }
    requires { full_up_to g.elts i }
    writes  { g }
    variant { 81 - i }
    ensures { grid_eq (old g).elts g.elts }
    ensures { forall h : grid. included g.elts h /\ full h -> not (valid s h) }
    raises { SolutionFound -> is_solution_for s g.elts (old g).elts }
  = if i = 81 then raise SolutionFound;
    (* assert { is_index i }; *)
    if g[i] <> 0 then
      try
        (* assert { 1 <= g[i] <= 9 }; *)
        check_valid_chunk g i s.column_start s.column_offsets;
        check_valid_chunk g i s.row_start s.row_offsets;
        check_valid_chunk g i s.square_start s.square_offsets;
        solve_aux s g (i + 1)
      with Invalid -> ()
      end
    else
      begin
MARCHE Claude's avatar
MARCHE Claude committed
451
      let ghost old_g = g.elts in
452
      for k = 1 to 9 do
MARCHE Claude's avatar
MARCHE Claude committed
453
        invariant { grid_eq old_g (Map.set g.elts i 0) }
454 455 456
        invariant { full_up_to g.elts i }
        invariant { (* for completeness *)
          forall k'. 1 <= k' < k ->
MARCHE Claude's avatar
MARCHE Claude committed
457
          let g' = Map.set old_g i k' in
458 459
          forall h : grid. included g' h /\ full h -> not (valid s h) }
        g[i] <- k;
MARCHE Claude's avatar
MARCHE Claude committed
460
	valid_up_to_frame s old_g (Map.set g.elts i 0) i;
461 462 463 464
        try
          check_valid_chunk g i s.column_start s.column_offsets;
          check_valid_chunk g i s.row_start s.row_offsets;
          check_valid_chunk g i s.square_start s.square_offsets;
465
            (* the hard part: see lemma valid_up_to_change *)
MARCHE Claude's avatar
MARCHE Claude committed
466
          assert { let grid' = Map.set old_g i k in
467 468
            grid_eq grid' g.elts &&
            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) };
MARCHE Claude's avatar
MARCHE Claude committed
472
          valid_up_to_change s old_g i k;
473 474 475
          solve_aux s g (i + 1)
        with Invalid ->
          assert { (* for completeness *)
MARCHE Claude's avatar
MARCHE Claude committed
476
            not (valid s (Map.set old_g i k)) };
477
          assert { (* for completeness *)
MARCHE Claude's avatar
MARCHE Claude committed
478
            let g' = Map.set old_g i k in
479 480 481 482 483
            forall h : grid. included g' h /\ full h -> not (valid s h) }
        end
      done;
      g[i] <- 0;
      assert { (* for completeness *)
MARCHE Claude's avatar
MARCHE Claude committed
484
        forall h:grid. included old_g h /\ full h ->
485
          let k' = Map.get h i in
MARCHE Claude's avatar
MARCHE Claude committed
486
          let g' = Map.set old_g i k' in
487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506
          included g' h }
      end

  exception NoSolution

  let solve (s:sudoku_chunks) (g : array int)
    requires { well_formed_sudoku s }
    requires { g.length = 81 }
    requires { valid_values g.elts }
    writes   { g }
    ensures  { result = g }
    ensures  { is_solution_for s g.elts (old g).elts }
    raises   { NoSolution ->
      forall h : grid. included g.elts h /\ full h -> not (valid s h)  }
  =
    try solve_aux s g 0;
        raise NoSolution
    with SolutionFound -> g
    end

MARCHE Claude's avatar
MARCHE Claude committed
507 508 509 510 511 512 513 514 515 516
  let check_then_solve (s:sudoku_chunks) (g : array int)
    requires { well_formed_sudoku s }
    requires { g.length = 81 }
    requires { valid_values g.elts }
    writes   { g }
    ensures  { result = g }
    ensures  { is_solution_for s g.elts (old g).elts }
    raises   { NoSolution ->
      forall h : grid. included g.elts h /\ full h -> not (valid s h)  }
  =
517 518 519 520
    if check_valid s g then solve s g else raise NoSolution

end

MARCHE Claude's avatar
MARCHE Claude committed
521
(* Proof in progress
522 523 524 525
module RandomSolver

  (* a variant: solve using a random order of cells *)

526 527 528
  use Grid
  use array.Array
  use int.Int
529 530
  use random.Random

531
  use Solver
532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561

  let rec solve_aux (s:sudoku_chunks) (randoffset:int) (g : array int) (i : int)
    requires { well_formed_sudoku s }
    requires { 0 <= randoffset <= 80 }
    requires { g.length = 81 }
    requires { valid_values g.elts }
    requires { 0 <= i <= 81 }
    requires { valid_up_to s g.elts i }
    requires { full_up_to g.elts i }
    writes  { g }
    variant { 81 - i }
    ensures { grid_eq (old g).elts g.elts }
    ensures { forall h : grid. included g.elts h /\ full h -> not (valid s h) }
    raises { SolutionFound -> is_solution_for s g.elts (old g).elts }
  = if i = 81 then raise SolutionFound;
    (* assert { is_index i }; *)
    let j = i + randoffset in
    let j = if j >= 81 then j - 81 else j in
    (* assert { is_index j }; *)
    if g[j] <> 0 then
      try
        (* assert { 1 <= g[j] <= 9 }; *)
        Solver.check_valid_chunk g j s.column_start s.column_offsets;
        check_valid_chunk g j s.row_start s.row_offsets;
        check_valid_chunk g j s.square_start s.square_offsets;
        solve_aux s randoffset g (i + 1)
      with Invalid -> ()
      end
    else
      begin
MARCHE Claude's avatar
MARCHE Claude committed
562
      label L in
563
      for k = 1 to 9 do
MARCHE Claude's avatar
MARCHE Claude committed
564
        invariant { grid_eq (g at L).elts (Map.set g.elts j 0) }
565 566 567
        invariant { full_up_to g.elts i } (* TODO i -> j *)
        invariant { (* for completeness *)
          forall k'. 1 <= k' < k ->
MARCHE Claude's avatar
MARCHE Claude committed
568
          let g' = Map.set (g at L).elts i k' in (* TODO i -> j *)
569 570 571 572 573 574 575 576
          forall h : grid. included g' h /\ full h -> not (valid s h) }
        g[j] <- k;
        try
          check_valid_chunk g j s.column_start s.column_offsets;
          check_valid_chunk g j s.row_start s.row_offsets;
          check_valid_chunk g j s.square_start s.square_offsets;
            (* the hard part: see lemma valid_up_to_change *)
            (* TODO i -> j *)
MARCHE Claude's avatar
MARCHE Claude committed
577
          assert { let grid' = Map.set (g at L).elts i k in
578 579 580 581 582 583 584 585 586
            grid_eq grid' g.elts &&
            valid_chunk grid' i s.column_start s.column_offsets &&
            valid_chunk grid' i s.row_start s.row_offsets &&
            valid_chunk grid' i s.square_start s.square_offsets &&
            valid_up_to s grid' (i+1) };
          assert { valid_up_to s g.elts (i+1) };
          solve_aux s randoffset g (i + 1)
        with Invalid ->
          assert { (* for completeness *)
MARCHE Claude's avatar
MARCHE Claude committed
587
            not (valid s (Map.set (g at L).elts i k)) };
588
          assert { (* for completeness *)
MARCHE Claude's avatar
MARCHE Claude committed
589
            let g' = Map.set (g at L).elts i k in
590 591 592 593 594
            forall h : grid. included g' h /\ full h -> not (valid s h) }
        end
      done;
      g[j] <- 0;
      assert { (* for completeness *)
MARCHE Claude's avatar
MARCHE Claude committed
595
        forall h:grid. included (g at L).elts h /\ full h ->
596
          let k' = Map.get h i in
MARCHE Claude's avatar
MARCHE Claude committed
597
          let g' = Map.set (g at L).elts i k' in
598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616
          included g' h }
      end

  exception NoSolution

  let solve (s:sudoku_chunks) (g : array int)
    requires { well_formed_sudoku s }
    requires { g.length = 81 }
    requires { valid_values g.elts }
    writes   { g }
    ensures  { result = g }
    ensures  { is_solution_for s g.elts (old g).elts }
    raises   { NoSolution ->
      forall h : grid. included g.elts h /\ full h -> not (valid s h)  }
  =
    try
      let randoffset = 27 in
      solve_aux s randoffset g 0;
      raise NoSolution
MARCHE Claude's avatar
MARCHE Claude committed
617 618
    with SolutionFound -> g
    end
619 620 621 622 623 624 625 626 627 628 629 630

  let check_then_solve (s:sudoku_chunks) (g : array int)
    requires { well_formed_sudoku s }
    requires { g.length = 81 }
    requires { valid_values g.elts }
    writes   { g }
    ensures  { result = g }
    ensures  { is_solution_for s g.elts (old g).elts }
    raises   { NoSolution ->
      forall h : grid. included g.elts h /\ full h -> not (valid s h)  }
  =
    if check_valid s g then solve s g else raise NoSolution
631 632

end
MARCHE Claude's avatar
MARCHE Claude committed
633
*)
634 635 636


(** {2 Some Tests} *)
637

638 639
module Test

640 641
  use Grid
  use TheClassicalSudokuGrid
642

643 644 645
  use Solver
  use map.Map
  use array.Array
646 647 648 649 650

  (** Solving the empty grid: easy, yet not trivial *)
  let test0 ()
    raises { NoSolution -> true }
  = let a = Array.make 81 0 in
651
    solve (classical_sudoku()) a
652 653 654 655 656 657 658 659 660 661 662 663 664
(* a possible solution:
  1, 2, 3, 4, 5, 6, 7, 8, 9,
  4, 5, 6, 7, 8, 9, 1, 2, 3,
  7, 8, 9, 1, 2, 3, 4, 5, 6,
  2, 1, 4, 3, 6, 5, 8, 9, 7,
  3, 6, 5, 8, 9, 7, 2, 1, 4,
  8, 9, 7, 2, 1, 4, 3, 6, 5,
  5, 3, 1, 6, 4, 2, 9, 7, 8,
  6, 4, 2, 9, 7, 8, 5, 3, 1,
  9, 7, 8, 5, 3, 1, 6, 4, 2
*)

(** A grid known to be solvable *)
665
(*
666 667 668 669 670 671 672 673 674 675 676 677 678 679
2 0 9 0 0 0 0 1 0
0 0 0 0 6 0 0 0 0
0 5 3 8 0 2 7 0 0
3 0 0 0 0 0 0 0 0
0 0 0 0 7 5 0 0 3
0 4 1 2 0 8 9 0 0
0 0 4 0 9 0 0 2 0
8 0 0 0 0 1 0 0 5
0 0 0 0 0 0 0 7 6
*)

  let test1 ()
    raises { NoSolution -> true }
  = let a = Array.make 81 0 in
MARCHE Claude's avatar
MARCHE Claude committed
680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706
    a[0] <- 2;
    a[2] <- 9;
    a[7] <- 1;
    a[13] <- 6;
    a[19] <- 5;
    a[20] <- 3;
    a[21] <- 8;
    a[23] <- 2;
    a[24] <- 7;
    a[27] <- 3;
    a[40] <- 7;
    a[41] <- 5;
    a[44] <- 3;
    a[46] <- 4;
    a[47] <- 1;
    a[48] <- 2;
    a[50] <- 8;
    a[51] <- 9;
    a[56] <- 4;
    a[58] <- 9;
    a[61] <- 2;
    a[63] <- 8;
    a[68] <- 1;
    a[71] <- 5;
    a[79] <- 7;
    a[80] <- 6;
    assert { valid_values a.Array.elts };
707
    solve (classical_sudoku()) a
MARCHE Claude's avatar
MARCHE Claude committed
708

709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726
(* the solution:

  2, 6, 9, 3, 5, 7, 8, 1, 4,
  1, 8, 7, 9, 6, 4, 5, 3, 2,
  4, 5, 3, 8, 1, 2, 7, 6, 9,
  3, 7, 5, 6, 4, 9, 2, 8, 1,
  9, 2, 8, 1, 7, 5, 6, 4, 3,
  6, 4, 1, 2, 3, 8, 9, 5, 7,
  7, 1, 4, 5, 9, 6, 3, 2, 8,
  8, 3, 6, 7, 2, 1, 4, 9, 5,
  5, 9, 2, 4, 8, 3, 1, 7, 6

*)

  (** A trivially unsolvable grid *)
  let test2 ()
    raises { NoSolution -> true }
  = let a = Array.make 81 1 in
727
    solve (classical_sudoku()) a
728 729 730 731 732

end

(***
Local Variables:
733
compile-command: "why3 ide --extra-config ../share/strategies.conf sudoku.mlw"
734 735
End:
*)