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