vstte10_queens.mlw 6.5 KB
Newer Older
1 2 3 4
(*
   VSTTE'10 competition http://www.macs.hw.ac.uk/vstte10/Competition.html
   Problem 4: N-queens

5 6
   Author: Jean-Christophe Filliatre (CNRS)
   Tool:   Why3 (see http://why3.lri.fr/)
7
*)
8

9
module NQueens
10

11
  use import int.Int
12
  use import array.Array
13

Andrei Paskevich's avatar
Andrei Paskevich committed
14
  predicate eq_board (b1 b2: array int) (pos: int) =
15 16
    forall q:int. 0 <= q < pos -> b1[q] = b2[q]

17 18
  lemma eq_board_set:
    forall b: array int, pos q i: int.
19 20
    pos <= q -> eq_board b b[q <- i] pos

21 22
  lemma eq_board_sym:
    forall b1 b2: array int, pos: int.
23 24
    eq_board b1 b2 pos -> eq_board b2 b1 pos

25 26
  lemma eq_board_trans:
    forall b1 b2 b3: array int, pos: int.
27 28
    eq_board b1 b2 pos -> eq_board b2 b3 pos -> eq_board b1 b3 pos

29 30
  lemma eq_board_extension:
    forall b1 b2: array int, pos: int.
31 32
    eq_board b1 b2 pos -> b1[pos] = b2[pos] -> eq_board b1 b2 (pos+1)

Andrei Paskevich's avatar
Andrei Paskevich committed
33 34 35
  predicate consistent_row (board: array int) (pos: int) (q: int) =
    board[q] <> board[pos] /\
    board[q] - board[pos] <> pos - q /\
36
    board[pos] - board[q] <> pos - q
37

38 39 40
  lemma consistent_row_eq:
    forall b1 b2: array int, pos: int.
    eq_board b1 b2 (pos+1) -> forall q: int. 0 <= q < pos ->
41
      consistent_row b1 pos q -> consistent_row b2 pos q
42

Andrei Paskevich's avatar
Andrei Paskevich committed
43
  predicate is_consistent (board: array int) (pos: int) =
44 45
    forall q:int. 0 <= q < pos -> consistent_row board pos q

46
  exception Inconsistent int
47

48 49 50 51
  let check_is_consistent (board: array int) (pos: int)
    requires { 0 <= pos < length board }
    ensures { result=True <-> is_consistent board pos }
  = try
52
      for q = 0 to pos - 1 do
53 54 55
        invariant { forall j:int. 0 <= j < q -> consistent_row board pos j }
        let bq   = board[q]   in
        let bpos = board[pos] in
56 57 58
        if bq        = bpos    then raise (Inconsistent q);
        if bq - bpos = pos - q then raise (Inconsistent q);
        if bpos - bq = pos - q then raise (Inconsistent q)
59 60
      done;
      True
61 62
    with Inconsistent q ->
      assert { not (consistent_row board pos q) };
63 64
      False
    end
65

Andrei Paskevich's avatar
Andrei Paskevich committed
66
  predicate is_board (board: array int) (pos: int) =
67
    forall q:int. 0 <= q < pos -> 0 <= board[q] < length board
68

Andrei Paskevich's avatar
Andrei Paskevich committed
69 70
  predicate solution (board: array int) (pos: int) =
    is_board board pos /\
71 72
    forall q:int. 0 <= q < pos -> is_consistent board q

73 74
  lemma solution_eq_board:
    forall b1 b2: array int, pos: int. length b1 = length b2 ->
75
    eq_board b1 b2 pos -> solution b1 pos -> solution b2 pos
76

77 78
  exception Solution

79 80 81 82 83 84 85 86
  let rec bt_queens (board: array int) (n: int) (pos: int) variant { n - pos }
    requires { length board = n /\ 0 <= pos <= n /\ solution board pos }
    ensures { (* no solution *)
      eq_board board (old board) pos /\
      forall b:array int. length b = n -> is_board b n ->
        eq_board board b pos -> not (solution b n) }
    raises { Solution -> solution board n }
  = 'Init:
87 88
    if pos = n then raise Solution;
    for i = 0 to n - 1 do
89
      invariant {
90
        eq_board board (at board 'Init) pos /\
91
        forall b:array int. length b = n -> is_board b n ->
92
          eq_board board b pos -> 0 <= b[pos] < i -> not (solution b n) }
93
      board[pos] <- i;
94 95 96
      if check_is_consistent board pos then bt_queens board n (pos+1)
    done

97
  let queens (board: array int) (n: int)
98
    requires { length board = n }
99 100 101
    ensures { forall b:array int. length b = n -> is_board b n -> not (solution b n) }
    raises { Solution -> solution board n }
  = bt_queens board n 0
102

MARCHE Claude's avatar
MARCHE Claude committed
103 104 105 106 107 108 109 110 111 112 113

  exception BenchFailure

  let test8 () raises { BenchFailure -> true } =
    let a = Array.make 8 0 in
    try
      queens a 8;
      raise BenchFailure
    with Solution -> a
    end

114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148
  (** variant: counting solutions (not part of the competition)

      TODO: prove soundness i.e. we indeed count the number of solutions *)

  use import ref.Refint

  let rec count_bt_queens (board: array int) (n: int) (pos: int) : int
    variant  { n - pos }
    requires { length board = n /\ 0 <= pos <= n /\ solution board pos }
    ensures  { eq_board board (old board) pos }
  = 'Init:
    if pos = n then
      1
    else begin
      let s = ref 0 in
      for i = 0 to n - 1 do
        invariant { eq_board board (at board 'Init) pos }
        board[pos] <- i;
        if check_is_consistent board pos then
          s += count_bt_queens board n (pos+1)
      done;
      !s
    end

  let count_queens (board: array int) (n: int) : int
    requires { length board = n }
    ensures  { true }
  = count_bt_queens board n 0

  let test_count_8 () =
    let a = Array.make 8 0 in
    count_queens a 8

end

149
(** counting solutions with 63-bit machine integers *)
150

151
module NQueens63
152 153 154 155 156

  use import ref.Refint
  use import mach.array.Array63
  use import mach.int.Int63

Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
157
  predicate is_board (board: array63 int63) (pos: int) =
158 159 160
    forall q: int. 0 <= q < pos ->
    0 <= to_int board[q] < to_int (length board)

161
  exception MInconsistent
162

163
  let check_is_consistent (board: array63 int63) (pos: int63)
164 165 166
    requires { 0 <= to_int pos < to_int (length board) }
    requires { is_board board (to_int pos + 1) }
  = try
167 168 169 170 171 172 173 174 175 176 177 178
      let q = ref (of_int 0) in
      while !q < pos do
        invariant { 0 <= to_int !q <= to_int pos }
        invariant { is_board board (to_int pos + 1) }
        variant   { to_int pos - to_int !q }
        let bq   = board[!q]   in
        let bpos = board[pos] in
        if bq        = bpos     then raise MInconsistent;
        if bq - bpos = pos - !q then raise MInconsistent;
        if bpos - bq = pos - !q then raise MInconsistent;
        q := !q + of_int 1
      done;
179
      True
180
    with MInconsistent ->
181 182 183
      False
    end

184
  use mach.peano.Peano as P
185

186
  let rec count_bt_queens
Jean-Christophe Filliatre's avatar
Jean-Christophe Filliatre committed
187
    (solutions: ref P.t) (board: array63 int63) (n: int63) (pos: int63)
188 189 190 191 192 193 194
    requires { to_int (length board) = to_int n }
    requires { 0 <= to_int pos <= to_int n }
    requires { is_board board (to_int pos) }
    variant  { to_int n - to_int pos }
    ensures  { is_board board (to_int pos) }
  =
    if eq pos n then
195 196 197 198 199 200 201 202
      solutions := P.succ !solutions
    else
      let i = ref (of_int 0) in
      while !i < n do
        invariant { 0 <= to_int !i <= to_int n }
        invariant { is_board board (to_int pos) }
        variant   { to_int n - to_int !i }
        board[pos] <- !i;
203 204
        if check_is_consistent board pos then
          count_bt_queens solutions board n (pos + of_int 1);
205 206 207
        i := !i + of_int 1
      done

208 209
  let count_queens (n: int63) : P.t
    requires { to_int n >= 0 }
210
    ensures  { true }
211 212
  =
     let solutions = ref (P.zero ()) in
213
     let board = Array63.make n (of_int 0) in
214
     count_bt_queens solutions board n (of_int 0);
215
     !solutions
216

217
  let test_count_8 () =
218
    let n = of_int 8 in
219
    count_queens n
220

221
end
222