tasks a-s

Task/N-queens-problem/Xanadu/n-queens-problem.xanadu

@@ -0,0 +1,69 @@
+int abs(i: int) {
+    if (i >= 0) return i; else return -i;
+}
+
+unit print_dots(n: int) {
+  while (n > 0) { print_string("."); n = n - 1; }
+  return;
+}
+
+{size:int | 0 < size}
+unit print_board (board[size]: int, size: int(size)) {
+  var: int n, row;;
+
+  invariant: [i:nat] (row: int(i))
+  for (row = 0; row < size; row = row + 1) {
+    n = board[row];
+    print_dots(n-1);
+    print_string("Q");
+    print_dots(size - n);
+    print_newline();
+  }
+    print_newline();
+    return;
+}
+
+{size:int, j:int | 0 <= j < size}
+bool test (j: int(j), board[size]: int) {
+  var: int diff, i, qi, qj;;
+
+  qj = board[j];
+
+  invariant: [i:nat] (i: int(i))
+  for (i = 0; i < j; i = i + 1) {
+    qi = board[i]; diff = abs (qi - qj);
+    if (diff == 0) { return false; }
+    else { if (diff == j - i) return false; }
+  }
+  return true;
+}
+
+{size:int | 0 < size}
+nat queen(size: int(size)) {
+  var: int board[], next, row; nat count;;
+
+  count = 0; row = 0; board = alloc(size, 0);
+
+  invariant: [n:nat | n < size] (row: int(n))
+  while (true) {
+    next = board[row]; next = next + 1;
+    if (next > size) {
+      if (row == 0) break; else { board[row] = 0; row = row - 1; }
+    } else {
+      board[row] = next;
+      if (test(row, board)) {
+        row = row + 1;
+        if (row == size) {
+          count = count + 1;
+	  print_board(board, size);
+          row = row - 1;
+        }
+      }
+    }
+  }
+  return count;
+}
+
+int main () {
+  return queen (8);
+}