00001
00005 package edu.mit.csail.sdg.squander.examples.sudoku;
00006
00007 import edu.mit.csail.sdg.annotations.Ensures;
00008 import edu.mit.csail.sdg.annotations.Invariant;
00009 import edu.mit.csail.sdg.annotations.Modifies;
00010 import edu.mit.csail.sdg.squander.Squander;
00011 import edu.mit.csail.sdg.squander.annotations.Options;
00012 import edu.mit.csail.sdg.squander.log.Log.Level;
00013 import edu.mit.csail.sdg.squander.options.GlobalOptions;
00014
00020 @Invariant({
00021 "this.grid[int][int] in {x : int | x >= 0 && x <= this.n}"
00022 })
00023 public class Sudoku5 {
00024
00025 private int[][] grid;
00026 private final int n;
00027 @SuppressWarnings("unused")
00028 private final int m;
00029 private final int[] nums;
00030
00031 public Sudoku5(int n) {
00032 assert Math.sqrt(n) * Math.sqrt(n) == n : "n must be a square number";
00033 this.n = n;
00034 this.m = (int) Math.sqrt(n);
00035 this.nums = new int[n];
00036 for (int i = 0; i < n; i++)
00037 nums[i] = i + 1;
00038 this.grid = new int[n][n];
00039 }
00040
00041 @Ensures("this.grid = @old(this.grid) + row -> col -> value")
00042 @Modifies("this.grid[int].elems")
00043 public void setCellValue(int row, int col, int value) {
00044 grid[row][col] = value;
00045 }
00046
00047 @Ensures("return = this.grid[row][col]")
00048 public int getCellValue(int row, int col) {
00049 return grid[row][col];
00050 }
00051
00052 @Ensures({
00053 "all x : int | all y : int | @old(this.grid[x][y] > 0) => x -> y -> @old(this.grid[x][y]) in this.grid.elems.elems",
00054 "all x : int | x >= 0 && x < this.n" +
00055 "=> (this.nums[int] = this.grid[x][int]) && (this.nums[int] = this.grid[int][x])",
00056 "all i1 : int | all i2 : int | i1 >= 0 && i1 < this.m && i2 >= 0 && i2 < this.m " +
00057 "=> this.nums[int] = this.grid[{x : int | x >= i1*this.m && x < (i1+1)*this.m}][{y : int | y >= i2*this.m && y < (i2+1)*this.m}]"
00058 })
00059 @Modifies("this.grid[int].elems")
00060 @Options(ensureAllInts=false)
00061 public void solve() {
00062 Squander.exe(this);
00063 }
00064
00065 public String printSimple() {
00066 StringBuilder sb = new StringBuilder();
00067 for (int i = 0; i < n; i++)
00068 for (int j = 0; j < n; j++)
00069 sb.append(getCellValue(i, j)).append(" ");
00070 return sb.toString().trim();
00071 }
00072
00073 @Override
00074 public String toString() {
00075 StringBuilder sb = new StringBuilder();
00076 int m = (int) Math.sqrt(n);
00077 for (int i = 0; i < n; i++) {
00078 if (i % m == 0)
00079 printHLine(sb, n, m);
00080 for (int j = 0; j < n; j++) {
00081 if (j % m == 0)
00082 sb.append("| ");
00083 sb.append(getCellValue(i, j)).append(" ");
00084 }
00085 sb.append("|\n");
00086 }
00087 printHLine(sb, n, m);
00088 return sb.toString();
00089 }
00090
00091 private void printHLine(StringBuilder sb, int n2, int m) {
00092 for (int i = 0; i < n; i++) {
00093 if (i % m == 0)
00094 sb.append("+-");
00095 sb.append("--");
00096 }
00097 sb.append("+\n");
00098 }
00099
00100 public static Sudoku5 parse(String puzzle) {
00101 String[] vals = puzzle.replaceAll("\\|", " ").split("\\s+");
00102 assert (vals.length > 0);
00103 int n = Integer.parseInt(vals[0]);
00104 assert vals.length == n*n + 1 : "must provide exactly " + n*n + " cell values";
00105 Sudoku5 sudoku = new Sudoku5(n);
00106 for (int i = 0; i < n; i++)
00107 for (int j = 0; j < n; j++) {
00108 int val = Integer.parseInt(vals[1 + i*n + j]);
00109 if (val > 0)
00110 sudoku.setCellValue(i, j, val);
00111 }
00112 return sudoku;
00113 }
00114
00115 public static void main(String[] args) {
00116 GlobalOptions.INSTANCE.log_level = Level.NONE;
00117 Sudoku5 sudoku = Sudoku5.parse("4 | 0 1 0 0 |" +
00118 "| 0 0 3 0 |" +
00119 "| 0 3 0 0 |" +
00120 "| 0 0 4 0 |");
00121
00122
00123
00124
00125
00126
00127
00128
00129
00130 System.out.println(sudoku);
00131 sudoku.solve();
00132 System.out.println(sudoku);
00133 }
00134
00135 }