In chess, a queen attacks positions from where it is, in straight lines up-down and left-right as well as on both its diagonals. It attacks only pieces not of its own colour.






⇖
⇑
⇗



⇐
⇐
♛
⇒
⇒



⇙
⇓
⇘



⇙

⇓

⇘




⇓






The goal of Peaceful chess queen armies is to arrange m black queens and m white queens on an n-by-n square grid, (the board), so that no queen attacks another of a different colour.



Task

 Create a routine to represent two-colour queens on a 2-D board. (Alternating black/white background colours, Unicode chess pieces and other embellishments are not necessary, but may be used at your discretion).
 Create a routine to generate at least one solution to placing m equal numbers of black and white queens on an n square board.
 Display here results for the m=4, n=5 case.


References

 Peaceably Coexisting Armies of Queens (Pdf) by Robert A. Bosch. Optima, the Mathematical Programming Socity newsletter, issue 62.
 A250000 OEIS


(********************************************************************)
 
#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
 
(********************************************************************)