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