00001
00005 package edu.mit.csail.sdg.squander.examples.chess;
00006
00007 import java.util.Collection;
00008 import java.util.HashSet;
00009 import java.util.Set;
00010
00011 import edu.mit.csail.sdg.annotations.Ensures;
00012 import edu.mit.csail.sdg.annotations.Modifies;
00013 import edu.mit.csail.sdg.squander.Squander;
00014 import edu.mit.csail.sdg.squander.annotations.Options;
00015
00016 import static edu.mit.csail.sdg.squander.examples.chess.ChessBoardMan.dx;
00017 import static edu.mit.csail.sdg.squander.examples.chess.ChessBoardMan.dy;
00018
00024 public class ChessBoard {
00025
00031 public static class Cell {
00032 public int i, j;
00033
00034 public Cell(int i, int j) {
00035 this.i = i;
00036 this.j = j;
00037 }
00038
00039 @Override
00040 public String toString() {
00041 return String.format("(%s, %s)", i, j);
00042 }
00043 }
00044
00045
00049 @Ensures({
00050 "all k : int | k >= 0 && k < n => lone (Cell@i) . k",
00051 "all k : int | k >= 0 && k < n => lone (Cell@j) . k",
00052 "all q1 : result.elts | no q2 : result.elts - q1 | " +
00053 " q1.i == q2.i || q1.i - q1.j == q2.i - q2.j || " +
00054 " q1.j == q2.j || q1.i + q1.j == q2.i + q2.j"
00055 })
00056 @Modifies({
00057 "Cell.i [result.elts][{k : int | k >= 0 && k < n}]",
00058 "Cell.j [result.elts][{k : int | k >= 0 && k < n}]"
00059 })
00060 private static void nqueens2(int n, Set<Cell> result) {
00061 Squander.exe(null, n, result);
00062 }
00063
00064 public static Set<Cell> nqueens_int(int n) {
00065 Set<Cell> result = new HashSet<Cell>();
00066 for (int i = 0; i < n; i++)
00067 result.add(new Cell(i, 0));
00068 nqueens2(n, result);
00069 return result;
00070 }
00071
00075 @Ensures({
00076 "all k : int | k >= 0 && k < n => lone (Cell@i) . k",
00077 "all k : int | k >= 0 && k < n => lone (Cell@j) . k",
00078 "all q1 : Cell | all q2 : Cell - q1 | " +
00079 " q1.i != q2.i && q1.j != q2.j && " +
00080 " #((^INC.(q1.i) @+ ^INC.(q2.i)) @- (^INC.(q1.i) @& ^INC.(q2.i))) !=" +
00081 " #((^INC.(q1.j) @+ ^INC.(q2.j)) @- (^INC.(q1.j) @& ^INC.(q2.j)))"
00082 })
00083 @Modifies({
00084 "Cell.i [result.elts][{k : int | k >= 0 && k < n}]",
00085 "Cell.j [result.elts][{k : int | k >= 0 && k < n}]"
00086 })
00087 @Options(ensureAllInts = false)
00088 private static void nqueens(int n, Set<Cell> result) {
00089 Squander.exe(null, n, result);
00090 }
00091
00092 public static Set<Cell> nqueens_rel(int n) {
00093 Set<Cell> result = new HashSet<Cell>();
00094 for (int i = 0; i < n; i++)
00095 result.add(new Cell(i, 0));
00096 nqueens(n, result);
00097 return result;
00098 }
00099
00103 @Ensures({
00104 "result.elems[int] = @old(result.elems[int])",
00105 "all k : int | k >= 0 && k < n * m - 1 => (" +
00106 " ((result[k+1].i = result[k].i + 2) && (result[k+1].j = result[k].j + 1)) || " +
00107 " ((result[k+1].i = result[k].i + 1) && (result[k+1].j = result[k].j + 2)) || " +
00108 " ((result[k+1].i = result[k].i - 1) && (result[k+1].j = result[k].j + 2)) || " +
00109 " ((result[k+1].i = result[k].i - 2) && (result[k+1].j = result[k].j + 1)) || " +
00110 " ((result[k+1].i = result[k].i - 2) && (result[k+1].j = result[k].j - 1)) || " +
00111 " ((result[k+1].i = result[k].i - 1) && (result[k+1].j = result[k].j - 2)) || " +
00112 " ((result[k+1].i = result[k].i + 1) && (result[k+1].j = result[k].j - 2)) || " +
00113 " ((result[k+1].i = result[k].i + 2) && (result[k+1].j = result[k].j - 1))" +
00114 ")"
00115 })
00116 @Modifies("result.elems")
00117 public static void knightsTour(int n, int m, Cell[] result) {
00118 Squander.exe(null, n, m, result);
00119 }
00120
00124 @Ensures({
00125 "result.elems[int] = @old(result.elems[int])",
00126 "all k : int | k >= 0 && k < n * m - 1 => (" +
00127 " result[k+1] in next[result[k].i * m + result[k].j].elts" +
00128 ")"
00129 })
00130 @Modifies("result.elems")
00131 @Options(ensureAllInts=false)
00132 public static void knightsTour2(int n, int m, Cell[] result, Set<Cell>[] next) {
00133 Squander.exe(null, n, m, result, next);
00134 }
00135
00136 public static Cell[] knightsTour(int n, int m) {
00137 Cell[] walk = new Cell[n*m];
00138 for (int i = 0; i < n; i++)
00139 for (int j = 0; j < m; j++)
00140 walk[i*m + j] = new Cell(i, j);
00141 knightsTour(n, m, walk);
00142 return walk;
00143 }
00144
00145 @SuppressWarnings("unchecked")
00146 public static Cell[] knightsTour2(int n, int m) {
00147 Cell[] walk = new Cell[n*m];
00148 Set<Cell>[] next = new Set[n*m];
00149 for (int i = 0; i < n; i++) {
00150 for (int j = 0; j < m; j++) {
00151 next[i*m + j] = new HashSet<Cell>();
00152 walk[i*m + j] = new Cell(i, j);
00153 }
00154 }
00155 for (int i = 0; i < n; i++) {
00156 for (int j = 0;j < m; j++) {
00157 for (int k = 0; k < dx.length; k++) {
00158 int ii = i + dx[k];
00159 int jj = j + dy[k];
00160 if (ii >= 0 && ii < n && jj >=0 && jj < m)
00161 next[i*m + j].add(walk[ii*m + jj]);
00162 }
00163 }
00164 }
00165 knightsTour2(n, m, walk, next);
00166 return walk;
00167 }
00168
00169 public static void printNQueens(Collection<Cell> queens) {
00170 int n = queens.size();
00171 boolean[][] board = new boolean[n][n];
00172 for (Cell c : queens) {
00173 board[c.i][c.j] = true;
00174 }
00175 for (int i = 0; i < n; i++) {
00176 for (int j = 0; j < n; j++) {
00177 if (board[i][j])
00178 System.out.print(" Q");
00179 else
00180 System.out.print(" .");
00181 }
00182 System.out.println();
00183 }
00184 }
00185
00186 public static void main(String[] args) {
00187 int n = 5;
00188 int m = 5;
00189 if (args.length > 1) {
00190 n = Integer.parseInt(args[0]);
00191 m = Integer.parseInt(args[1]);
00192 }
00193 Cell[] tour = knightsTour(n, m);
00194 int[][] board = new int[n][m];
00195 assert tour.length == n*m;
00196 int idx = 1;
00197 for (Cell c : tour)
00198 board[c.i][c.j] = idx++;
00199 for (int i = 0; i < n; i++) {
00200 for (int j = 0; j < m; j++) {
00201 System.out.print(board[i][j] + " ");
00202 }
00203 System.out.println();
00204 }
00205 }
00206
00207 }