Peaceful chess queen armies: Difference between revisions

<lang ats>(********************************************************************)

#define ATS_DYNLOADFLAG 0

#include "share/atspre_define.hats"

#include "share/atspre_staload.hats"

staload UN = "prelude/SATS/unsafe.sats"

#define NIL list_vt_nil ()

#define :: list_vt_cons

#ifndef NDEBUG #then

(* Safety is relatively unimportant in this program.

Therefore I have made it so you can put ‘-DATS NDEBUG=1’ on

your patscc command line, to skip some assertloc tests. *)

#define NDEBUG 0

#endif

(********************************************************************)

#define EMPTY 0

#define BLACK 1

#define WHITE ~1

stadef is_color (c : int) : bool = (~1 <= c && c <= 1)

stadef reverse_color (c : int) : int = ~c

typedef color_t (tk : tkind, c : int) =

[is_color c]

g1int (tk, c)

typedef color_t (tk : tkind) =

[c : int | is_color c]

g1int (tk, c)

fn {tk : tkind}

reverse_color {c : int | is_color c}

(c : g1int (tk, c)) :<>

[c_rev : int | is_color c_rev;

c_rev == reverse_color c]

g1int (tk, c_rev) =

(* This template is a fancy way to say ‘minus’. *)

~c

(********************************************************************)

(* Matrix indices will run from 0..n-1 rather than 1..n. *)

#define SIDE_MAX 16 (* The maximum side size. For

efficiency, please make it a

power of two. *)

#define BOARD_SIZE 256 (* The storage size for a board. *)

prval _ = prop_verify {SIDE_MAX * SIDE_MAX == BOARD_SIZE} ()

fn {tk : tkind}

row_index {k : int | 0 <= k; k < BOARD_SIZE}

(k : g1int (tk, k)) :<>

[i : int | 0 <= i; i < SIDE_MAX]

g1int (tk, i) =

(* Let the C compiler convert this to bitmasking. *)

g1int_nmod (k, g1i2i SIDE_MAX)

fn {tk : tkind}

column_index {k : int | 0 <= k; k < BOARD_SIZE}

(k : g1int (tk, k)) :<>

[i : int | 0 <= i; i < SIDE_MAX]

g1int (tk, i) =

(* Let the C compiler convert this to a shift. *)

k / g1i2i SIDE_MAX

fn {tk : tkind}

storage_index {i, j : int | 0 <= i; i < SIDE_MAX;

0 <= j; j < SIDE_MAX}

(i : g1int (tk, i),

j : g1int (tk, j)) :<>

[k : int | 0 <= k; k < BOARD_SIZE]

g1int (tk, k) =

(* Let the C compiler convert this to a shift and add. *)

i + (j * g1i2i SIDE_MAX)

(********************************************************************)

extern fn {tk_index : tkind}

test_equiv$reindex_i

{i, j : int | 0 <= i; 0 <= j}

{n : int | 0 <= n; n <= SIDE_MAX;

i < n; j < n}

(i : g1int (tk_index, i),

j : g1int (tk_index, j),

n : g1int (tk_index, n)) :<>

[i1 : int | 0 <= i1; i1 < SIDE_MAX]

g1int (tk_index, i1)

extern fn {tk_index : tkind}

test_equiv$reindex_j

{i, j : int | 0 <= i; 0 <= j}

{n : int | 0 <= n; n <= SIDE_MAX;

i < n; j < n}

(i : g1int (tk_index, i),

j : g1int (tk_index, j),

n : g1int (tk_index, n)) :<>

[j1 : int | 0 <= j1; j1 < SIDE_MAX]

g1int (tk_index, j1)

extern fn {tk_color : tkind}

test_equiv$recolor

{c : int | is_color c}

(c : g1int (tk_color, c)) :<>

[c1 : int | is_color c1]

g1int (tk_color, c1)

fn {tk_index, tk_color : tkind}

test_equiv {n : int | 0 <= n; n <= SIDE_MAX}

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n)) :

bool =

let

macdef reindex_i = test_equiv$reindex_i<tk_index>

macdef reindex_j = test_equiv$reindex_j<tk_index>

macdef recolor = test_equiv$recolor<tk_color>

fun

loopj {j : int | ~1 <= j; j < n} .<j + 1>.

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n),

j : g1int (tk_index, j)) :

bool =

if j < g1i2i 0 then

true

else

let

fun loopi {i : int | ~1 <= i; i < n} .<i + 1>.

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n),

j : g1int (tk_index, j),

i : g1int (tk_index, i)) :

bool =

if i < g1i2i 0 then

true

else

let

val ka = storage_index<tk_index> (i, j)

val color_a = a[ka]

val i1 = test_equiv$reindex_i<tk_index> (i, j, n)

val j1 = test_equiv$reindex_j<tk_index> (i, j, n)

val kb = storage_index<tk_index> (i1, j1)

val color_b = recolor b[kb]

in

if color_a = color_b then

loopi (a, b, n, j, pred i)

else

false

end

in

if loopi (a, b, n, j, g1i2i (pred n)) then

loopj (a, b, n, pred j)

else

false

end

in

loopj (a, b, n, g1i2i (pred n))

end

fn {tk_index, tk_color : tkind}

test_equiv_rotate0

{n : int | 0 <= n; n <= SIDE_MAX}

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n)) :

bool =

let

(* No rotations or reflections. *)

implement

test_equiv$reindex_i<tk_index> (i, j, n) = i

implement

test_equiv$reindex_j<tk_index> (i, j, n) = j

in

test_equiv<tk_index, tk_color> (a, b, n)

end

fn {tk_index, tk_color : tkind}

test_equiv_rotate90

{n : int | 0 <= n; n <= SIDE_MAX}

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n)) :

bool =

let

(* Matrix rotation counterclockwise by 90 degrees. *)

implement

test_equiv$reindex_i<tk_index> {i, j} {n} (i, j, n) = pred n - j

implement

test_equiv$reindex_j<tk_index> (i, j, n) = i

in

test_equiv<tk_index, tk_color> (a, b, n)

end

fn {tk_index, tk_color : tkind}

test_equiv_rotate180

{n : int | 0 <= n; n <= SIDE_MAX}

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n)) :

bool =

let

(* Matrix rotation by 180 degrees. *)

implement

test_equiv$reindex_i<tk_index> {i, j} {n} (i, j, n) = pred n - i

implement

test_equiv$reindex_j<tk_index> {i, j} {n} (i, j, n) = pred n - j

in

test_equiv<tk_index, tk_color> (a, b, n)

end

fn {tk_index, tk_color : tkind}

test_equiv_rotate270

{n : int | 0 <= n; n <= SIDE_MAX}

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n)) :

bool =

let

(* Matrix rotation counterclockwise by 270 degrees. *)

implement

test_equiv$reindex_i<tk_index> (i, j, n) = j

implement

test_equiv$reindex_j<tk_index> {i, j} {n} (i, j, n) = pred n - i

in

test_equiv<tk_index, tk_color> (a, b, n)

end

fn {tk_index, tk_color : tkind}

test_equiv_reflecti

{n : int | 0 <= n; n <= SIDE_MAX}

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n)) :

bool =

let

(* Reverse the order of the rows. *)

implement

test_equiv$reindex_i<tk_index> {i, j} {n} (i, j, n) = pred n - i

implement

test_equiv$reindex_j<tk_index> (i, j, n) = j

in

test_equiv<tk_index, tk_color> (a, b, n)

end

fn {tk_index, tk_color : tkind}

test_equiv_reflectj

{n : int | 0 <= n; n <= SIDE_MAX}

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n)) :

bool =

let

(* Reverse the order of the columns. *)

implement

test_equiv$reindex_i<tk_index> (i, j, n) = i

implement

test_equiv$reindex_j<tk_index> {i, j} {n} (i, j, n) = pred n - j

in

test_equiv<tk_index, tk_color> (a, b, n)

end

fn {tk_index, tk_color : tkind}

test_equiv_reflect_diag_down

{n : int | 0 <= n; n <= SIDE_MAX}

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n)) :

bool =

let

(* Transpose the matrix around its main diagonal. *)

implement

test_equiv$reindex_i<tk_index> (i, j, n) = j

implement

test_equiv$reindex_j<tk_index> (i, j, n) = i

in

test_equiv<tk_index, tk_color> (a, b, n)

end

fn {tk_index, tk_color : tkind}

test_equiv_reflect_diag_up

{n : int | 0 <= n; n <= SIDE_MAX}

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n)) :

bool =

let

(* Transpose the matrix around its main skew diagonal. *)

implement

test_equiv$reindex_i<tk_index> {i, j} {n} (i, j, n) = pred n - j

implement

test_equiv$reindex_j<tk_index> {i, j} {n} (i, j, n) = pred n - i

in

test_equiv<tk_index, tk_color> (a, b, n)

end

fn {tk_index, tk_color : tkind}

board_equiv {n : int | 0 <= n; n <= SIDE_MAX}

(a : &(@[color_t tk_color][BOARD_SIZE]),

b : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n),

rotation_equiv_classes : bool) :

bool =

let

(* Leave the colors unchanged. *)

implement test_equiv$recolor<tk_color> (c) = c

(* Test without rotations or reflections. *)

val equiv = test_equiv_rotate0<tk_index, tk_color> (a, b, n)

in

if ~rotation_equiv_classes then

equiv

else

let

(* Leave the colors unchanged. *)

implement test_equiv$recolor<tk_color> (c) = c

val equiv =

(equiv ||

test_equiv_rotate90<tk_index, tk_color> (a, b, n) ||

test_equiv_rotate180<tk_index, tk_color> (a, b, n) ||

test_equiv_rotate270<tk_index, tk_color> (a, b, n) ||

test_equiv_reflecti<tk_index, tk_color> (a, b, n) ||

test_equiv_reflectj<tk_index, tk_color> (a, b, n) ||

test_equiv_reflect_diag_down<tk_index, tk_color> (a, b, n) ||

test_equiv_reflect_diag_up<tk_index, tk_color> (a, b, n))

(* Reverse the colors of b in each test. *)

implement test_equiv$recolor<tk_color> (c) = reverse_color c

val equiv =

(equiv ||

test_equiv_rotate0<tk_index, tk_color> (a, b, n) ||

test_equiv_rotate90<tk_index, tk_color> (a, b, n) ||

test_equiv_rotate180<tk_index, tk_color> (a, b, n) ||

test_equiv_rotate270<tk_index, tk_color> (a, b, n) ||

test_equiv_reflecti<tk_index, tk_color> (a, b, n) ||

test_equiv_reflectj<tk_index, tk_color> (a, b, n) ||

test_equiv_reflect_diag_down<tk_index, tk_color> (a, b, n) ||

test_equiv_reflect_diag_up<tk_index, tk_color> (a, b, n))

in

equiv

end

end

(********************************************************************)

fn {tk_index : tkind}

fprint_rule {n : int | 0 <= n; n <= SIDE_MAX}

(f : FILEref,

n : g1int (tk_index, n)) :

void =

let

fun

loop {j : int | 0 <= j; j <= n} .<n - j>.

(j : g1int (tk_index, j)) :

void =

if j <> n then

begin

fileref_puts (f, "----+");

loop (succ j)

end

in

fileref_puts (f, "+");

loop (g1i2i 0)

end

fn {tk_index, tk_color : tkind}

fprint_board {n : int | 0 <= n; n <= SIDE_MAX}

(f : FILEref,

a : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n)) :

void =

if n <> 0 then

let

fun

loopi {i : int | ~1 <= i; i < n} .<i + 1>.

(f : FILEref,

a : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n),

i : g1int (tk_index, i)) :

void =

if i <> ~1 then

let

fun

loopj {j : int | 0 <= j; j <= n} .<n - j>.

(f : FILEref,

a : &(@[color_t tk_color][BOARD_SIZE]),

n : g1int (tk_index, n),

i : g1int (tk_index, i),

j : g1int (tk_index, j)) :

void =

if j <> n then

let

val k = storage_index<tk_index> (i, j)

val color = a[k]

val representation =

if color = g1i2i BLACK then

"| B "

else if color = g1i2i WHITE then

"| W "

else

"| "

in

fileref_puts (f, representation);

loopj (f, a, n, i, succ j)

end

in

fileref_puts (f, "\n");

loopj (f, a, n, i, g1i2i 0);

fileref_puts (f, "|\n");

fprint_rule (f, n);

loopi (f, a, n, pred i)

end

in

fprint_rule (f, n);

loopi (f, a, n, pred n)

end

(********************************************************************)

(* M2_MAX equals the maximum number of queens of either color.

Thus it is the maximum of 2*m, where m is the number of queens

in an army. *)

#define M2_MAX BOARD_SIZE

(* The even-index queens are BLACK, the odd-index queens are WHITE. *)

vtypedef board_record_vt (tk_color : tkind,

p : addr) =

@{

pf = @[color_t tk_color][BOARD_SIZE] @ p,

pfgc = mfree_gc_v p |

p = ptr p

}

vtypedef board_record_vt (tk_color : tkind) =

[p : addr | null < p]

board_record_vt (tk_color, p)

vtypedef board_record_list_vt (tk_color : tkind,

n : int) =

list_vt (board_record_vt tk_color, n)

vtypedef board_record_list_vt (tk_color : tkind) =

[n : int]

board_record_list_vt (tk_color, n)

fn

board_record_vt_free

{tk_color : tkind}

{p : addr}

(record : board_record_vt (tk_color, p)) :

void =

let

val @{

pf = pf,

pfgc = pfgc |

p = p

} = record

in

array_ptr_free (pf, pfgc | p)

end

overload free with board_record_vt_free

fn

board_record_list_vt_free

{tk_color : tkind}

{n : int}

(lst : board_record_list_vt (tk_color, n)) :

void =

let

fun

loop {n : int | 0 <= n} .<n>.

(lst : board_record_list_vt (tk_color, n)) :

void =

case+ lst of

| ~ NIL => ()

| ~ head :: tail =>

begin

free head;

loop tail

end

prval _ = lemma_list_vt_param lst

in

loop lst

end

fn {tk_index, tk_color : tkind}

any_board_equiv {n : int | 0 <= n; n <= SIDE_MAX}

(board : &(@[color_t tk_color][BOARD_SIZE]),

lst : !board_record_list_vt tk_color,

n : g1int (tk_index, n),

rotation_equiv_classes : bool) :

bool =

let

macdef board_equiv = board_equiv<tk_index, tk_color>

fun

loop {k : int | 0 <= k} .<k>.

(board : &(@[color_t tk_color][BOARD_SIZE]),

lst : !board_record_list_vt (tk_color, k),

n : g1int (tk_index, n)) :

bool =

case+ lst of

| NIL => false

| head :: tail =>

if board_equiv (!(head.p), board, n,

rotation_equiv_classes) then

true

else

loop (board, tail, n)

prval _ = lemma_list_vt_param lst

in

loop (board, lst, n)

end

fn {tk_index, tk_color : tkind}

queens_to_board

{count : int | 0 <= count; count <= M2_MAX}

(queens : &(@[g1int tk_index][M2_MAX]),

count : int count) :

[p : addr | null < p]

board_record_vt (tk_color, p) =

let

typedef color_t = color_t tk_color

fun

loop {k : int | ~1 <= k; k < count} .<k + 1>.

(queens : &(@[g1int tk_index][M2_MAX]),

board : &(@[color_t tk_color][BOARD_SIZE]),

k : int k) :

void =

if 0 <= k then

let

val [coords : int] coords = queens[k]

#if NDEBUG <> 0 #then

prval _ = $UN.prop_assert {0 <= coords} ()

prval _ = $UN.prop_assert {coords < BOARD_SIZE} ()

#else

val _ = assertloc (g1i2i 0 <= coords)

val _ = assertloc (coords < g1i2i BOARD_SIZE)

#endif

in

if g1int_nmod (k, 2) = 0 then

board[coords] := g1i2i BLACK

else

board[coords] := g1i2i WHITE;

loop (queens, board, pred k)

end

val @(pf, pfgc | p) = array_ptr_alloc<color_t> (i2sz BOARD_SIZE)

val _ = array_initize_elt<color_t> (!p, i2sz BOARD_SIZE,

g1i2i EMPTY)

val _ = loop (queens, !p, pred count)

in

@{

pf = pf,

pfgc = pfgc |

p = p

}

end

fn {tk : tkind}

queen_would_fit_in

{count : int | 0 <= count; count <= M2_MAX}

{i, j : int | 0 <= i; i < SIDE_MAX;

0 <= j; j < SIDE_MAX}

(queens : &(@[g1int tk][M2_MAX]),

count : int count,

i : g1int (tk, i),

j : g1int (tk, j)) :

bool =

(* Would a new queen at (i,j) be feasible? *)

if count = 0 then

true

else

let

fun

loop {k : int | ~1 <= k; k < count}

(queens : &(@[g1int tk][M2_MAX]),

k : int k) :

bool =

if k < 0 then

true

else

let

val [coords : int] coords = queens[k]

#if NDEBUG <> 0 #then

prval _ = $UN.prop_assert {0 <= coords} ()

prval _ = $UN.prop_assert {coords < BOARD_SIZE} ()

#else

val _ = assertloc (g1i2i 0 <= coords)

val _ = assertloc (coords < g1i2i BOARD_SIZE)

#endif

val i1 = row_index<tk> coords

val j1 = column_index<tk> coords

in

if g1int_nmod (k, 2) = g1int_nmod (count, 2) then

(* The two queens are of the same color. They may not

share the same square. *)

begin

if i <> i1 || j <> j1 then

loop (queens, pred k)

else

false

end

else

(* The two queens are of different colors. They may not

share the same square nor attack each other. *)

begin

if (i <> i1 &&

j <> j1 &&

i + j <> i1 + j1 &&

i - j <> i1 - j1) then

loop (queens, pred k)

else

false

end

end

in

loop (queens, pred count)

end

fn {tk : tkind}

latest_queen_fits_in

{count : int | 1 <= count; count <= M2_MAX}

(queens : &(@[g1int tk][M2_MAX]),

count : int count) :

bool =

let

val [coords : int] coords = queens[pred count]

#if NDEBUG <> 0 #then

prval _ = $UN.prop_assert {0 <= coords} ()

prval _ = $UN.prop_assert {coords < BOARD_SIZE} ()

#else

val _ = assertloc (g1i2i 0 <= coords)

val _ = assertloc (coords < g1i2i BOARD_SIZE)

#endif

val i = row_index<tk> coords

val j = column_index<tk> coords

in

queen_would_fit_in<tk> (queens, pred count, i, j)

end

fn {tk_index, tk_color : tkind}

find_solutions

{m : int | 0 <= m; 2 * m <= M2_MAX}

{n : int | 0 <= n; n <= SIDE_MAX}

{max_solutions : int | 0 <= max_solutions}

(f : FILEref,

m : int m,

n : g1int (tk_index, n),

rotation_equiv_classes : bool,

max_solutions : int max_solutions) :

[num_solutions : int | 0 <= num_solutions;

num_solutions <= max_solutions]

@(int num_solutions,

board_record_list_vt (tk_color, num_solutions)) =

(* This template function both prints the solutions and returns

them as a linked list. *)

if m = 0 then

@(0, NIL)

else if max_solutions = 0 then

@(0, NIL)

else

let

macdef latest_queen_fits_in = latest_queen_fits_in<tk_index>

macdef queens_to_board = queens_to_board<tk_index, tk_color>

macdef fprint_board = fprint_board<tk_index, tk_color>

macdef any_board_equiv = any_board_equiv<tk_index, tk_color>

macdef row_index = row_index<tk_index>

macdef column_index = column_index<tk_index>

macdef storage_index = storage_index<tk_index>

fnx

loop {num_solutions : int | 0 <= num_solutions;

num_solutions <= max_solutions}

{num_queens : int | 0 <= num_queens;

num_queens <= 2 * m}

(solutions : board_record_list_vt (tk_color,

num_solutions),

num_solutions : int num_solutions,

queens : &(@[g1int tk_index][M2_MAX]),

num_queens : int num_queens) :

[num_solutions1 : int | 0 <= num_solutions1;

num_solutions1 <= max_solutions]

@(int num_solutions1,

board_record_list_vt (tk_color, num_solutions1)) =

if num_queens = 0 then

@(num_solutions, solutions)

else if num_solutions = max_solutions then

@(num_solutions, solutions)

else if latest_queen_fits_in (queens, num_queens) then

begin

if num_queens = 2 * m then

let

val board = queens_to_board (queens, num_queens)

val equiv_solution =

any_board_equiv (!(board.p), solutions, n,

rotation_equiv_classes)

in

if ~equiv_solution then

begin

fprintln! (f, "Solution ",

succ num_solutions);

fprint_board (f, !(board.p), n);

fileref_puts (f, "\n\n");

move_a_queen (board :: solutions,

succ num_solutions,

queens, num_queens)

end

else

begin

free board;

move_a_queen (solutions, num_solutions,

queens, num_queens)

end

end

else

add_another_queen (solutions, num_solutions,

queens, num_queens)

end

else

move_a_queen (solutions, num_solutions,

queens, num_queens)

and

add_another_queen

{num_solutions : int |

0 <= num_solutions;

num_solutions <= max_solutions}

{num_queens : int | 0 <= num_queens;

num_queens + 1 <= 2 * m}

(solutions : board_record_list_vt

(tk_color, num_solutions),

num_solutions : int num_solutions,

queens : &(@[g1int tk_index][M2_MAX]),

num_queens : int num_queens) :

[num_solutions1 : int | 0 <= num_solutions1;

num_solutions1 <= max_solutions]

@(int num_solutions1,

board_record_list_vt (tk_color, num_solutions1)) =

let

val coords = storage_index (g1i2i 0, g1i2i 0)

in

queens[num_queens] := coords;

loop (solutions, num_solutions, queens, succ num_queens)

end

and

move_a_queen {num_solutions : int |

0 <= num_solutions;

num_solutions <= max_solutions}

{num_queens : int | 0 <= num_queens;

num_queens <= 2 * m}

(solutions : board_record_list_vt

(tk_color, num_solutions),

num_solutions : int num_solutions,

queens : &(@[g1int tk_index][M2_MAX]),

num_queens : int num_queens) :

[num_solutions1 : int | 0 <= num_solutions1;

num_solutions1 <= max_solutions]

@(int num_solutions1,

board_record_list_vt (tk_color, num_solutions1)) =

if num_queens = 0 then

loop (solutions, num_solutions, queens, num_queens)

else

let

val [coords : int] coords = queens[pred num_queens]

#if NDEBUG <> 0 #then

prval _ = $UN.prop_assert {0 <= coords} ()

prval _ = $UN.prop_assert {coords < BOARD_SIZE} ()

#else

val _ = assertloc (g1i2i 0 <= coords)

val _ = assertloc (coords < g1i2i BOARD_SIZE)

#endif

val [i : int] i = row_index coords

val [j : int] j = column_index coords

prval _ = prop_verify {0 <= i} ()

prval _ = prop_verify {i < SIDE_MAX} ()

prval _ = prop_verify {0 <= j} ()

prval _ = prop_verify {j < SIDE_MAX} ()

#if NDEBUG <> 0 #then

prval _ = $UN.prop_assert {i < n} ()

prval _ = $UN.prop_assert {j < n} ()

#else

val _ = $effmask_exn assertloc (i < n)

val _ = $effmask_exn assertloc (j < n)

#endif

in

if j = pred n then

begin

if i = pred n then

(* Backtrack. *)

move_a_queen (solutions, num_solutions,

queens, pred num_queens)

else

let

val coords = storage_index (succ i, j)

in

queens[pred num_queens] := coords;

loop (solutions, num_solutions,

queens, num_queens)

end

end

else

let

#if NDEBUG <> 0 #then

prval _ = $UN.prop_assert {j < n - 1} ()

#else

val _ = $effmask_exn assertloc (j < pred n)

#endif

in

if i = pred n then

let

val coords = storage_index (g1i2i 0, succ j)

in

queens[pred num_queens] := coords;

loop (solutions, num_solutions,

queens, num_queens)

end

else

let

val coords = storage_index (succ i, j)

in

queens[pred num_queens] := coords;

loop (solutions, num_solutions,

queens, num_queens)

end

end

end

var queens = @[g1int tk_index][M2_MAX] (g1i2i 0)

in

queens[0] := storage_index (g1i2i 0, g1i2i 0);

loop (NIL, 0, queens, 1)

end

(********************************************************************)

%{^

#include <stdlib.h>

#include <limits.h>

%}

implement

main0 (argc, argv) =

let

stadef tk_index = int_kind

stadef tk_color = int_kind

macdef usage_error (status) =

begin

println! ("Usage: ", argv[0],

" M N IGNORE_EQUIVALENTS [MAX_SOLUTIONS]");

exit (,(status))

end

val max_max_solutions =

$extval ([i : int | 0 <= i] int i, "INT_MAX")

in

if 4 <= argc then

let

val m = $extfcall (int, "atoi", argv[1])

val m = g1ofg0 m

val _ = if m < 0 then usage_error (2)

val _ = assertloc (0 <= m)

val _ =

if M2_MAX < 2 * m then

begin

println! (argv[0], ": M cannot be larger than ",

M2_MAX / 2);

usage_error (2)

end

val _ = assertloc (2 * m <= M2_MAX)

val n = $extfcall (int, "atoi", argv[2])

val n = g1ofg0 n

val _ = if n < 0 then usage_error (2)

val _ = assertloc (0 <= n)

val _ =

if SIDE_MAX < n then

begin

println! (argv[0], ": N cannot be larger than ",

SIDE_MAX);

usage_error (2)

end

val _ = assertloc (n <= SIDE_MAX)

val ignore_equivalents =

if argv[3] = "T" || argv[3] = "t" || argv[3] = "1" then

true

else if argv[3] = "F" || argv[3] = "f" || argv[3] = "0" then

false

else

begin

println! (argv[0],

": select T=t=1 or F=f=0 ",

"for IGNORE_EQUIVALENTS");

usage_error (2);

false

end

in

if argc = 5 then

let

val max_solutions = $extfcall (int, "atoi", argv[4])

val max_solutions = g1ofg0 max_solutions

val max_solutions = max (0, max_solutions)

val @(num_solutions, solutions) =

find_solutions<tk_index, tk_color>

(stdout_ref, m, n, ignore_equivalents,

max_solutions)

in

board_record_list_vt_free solutions

end

else

let

val @(num_solutions, solutions) =

find_solutions<tk_index, tk_color>

(stdout_ref, m, n, ignore_equivalents,

max_max_solutions)

in

board_record_list_vt_free solutions

end

end

else

usage_error (1)

end

(********************************************************************)</lang>

{{out}}

$ patscc -DATS NDEBUG=1 -O3 -fno-stack-protector -march=native -DATS_MEMALLOC_LIBC -o peaceful_queens peaceful_queens.dats && ./peaceful_queens 4 5 T

<pre>Solution 1

+----+----+----+----+----+

| B | | | | B |

+----+----+----+----+----+

| | | W | | |

+----+----+----+----+----+

| | W | | W | |

+----+----+----+----+----+

| | | W | | |

+----+----+----+----+----+

| B | | | | B |

+----+----+----+----+----+

Solution 2

+----+----+----+----+----+

| B | | B | | |

+----+----+----+----+----+

| | | | | W |

+----+----+----+----+----+

| | W | | W | |

+----+----+----+----+----+

| | | | | W |

+----+----+----+----+----+

| B | | B | | |

+----+----+----+----+----+

Solution 3

+----+----+----+----+----+

| | W | | W | |

+----+----+----+----+----+

| | | | | W |

+----+----+----+----+----+

| B | | B | | |

+----+----+----+----+----+

| | | | | W |

+----+----+----+----+----+

| B | | B | | |

+----+----+----+----+----+

</pre>