00001
00005 package edu.mit.csail.sdg.squander.examples.sudoku;
00006
00007 import java.util.Arrays;
00008
00009 import edu.mit.csail.sdg.annotations.Ensures;
00010 import edu.mit.csail.sdg.annotations.Invariant;
00011 import edu.mit.csail.sdg.annotations.Modifies;
00012 import edu.mit.csail.sdg.annotations.Returns;
00013 import edu.mit.csail.sdg.squander.Squander;
00014 import edu.mit.csail.sdg.squander.annotations.Options;
00015
00016
00017 @Invariant({
00018 "all i : int | all j : int | i >= 0 && i < this.n && j >= 0 && j < this.n => (" +
00019 " this.rows[i].cells[j] = this.cols[j].cells[i] &&" +
00020 " this.rows[i].cells[j] = this.grids[(i/this.m)*this.m + j/this.m].cells[(i%this.m)*this.m + j%this.m])"
00021 })
00022 public class Sudoku2 {
00023
00024 @Invariant("all v : int | v > 0 && v <= this.cells.length => lone this.cells.elems.v")
00025 static class CellGroup {
00026 int[] cells;
00027
00028 public CellGroup(int n) {
00029 this.cells = new int[n];
00030 }
00031
00032 @Override
00033 public String toString() {
00034 return Arrays.toString(cells);
00035 }
00036
00037 }
00038
00039 private final int n;
00040 @SuppressWarnings("unused")
00041 private final int m;
00042
00043 private CellGroup[] rows;
00044 private CellGroup[] cols;
00045 private CellGroup[] grids;
00046
00047 public Sudoku2(int n) {
00048 assert Math.sqrt(n) * Math.sqrt(n) == n : "n must be a square number";
00049 this.n = n;
00050 this.m = (int) Math.sqrt(n);
00051 init();
00052 }
00053
00054 @Ensures("all i : int | all j : int | (i = row & j = col) ? this.rows[i].cells[col] = val : this.rows[i].cells[col] = @old(this.rows[i].cells[col])")
00055 public void setCellValue(int row, int col, int val) {
00056 if (val < 1 || val > n)
00057 val = 0;
00058 int m = (int) Math.sqrt(n);
00059 rows[row].cells[col] = val;
00060 cols[col].cells[row] = val;
00061 grids[(row/m)*m + col/m].cells[(row%m)*m + col%m] = val;
00062 assert repOK();
00063 }
00064
00065 @Returns("this.rows[row].cells[col]")
00066 public int getCellValue(int row, int col) {
00067 return rows[row].cells[col];
00068 }
00069
00070 @Ensures({
00071
00072 "all g : CellGroup | all i : int | i >= 0 && i < this.n => g.cells[i] > 0 && g.cells[i] <= this.n",
00073 "all g : CellGroup | all i : int | i >= 0 && i < this.n && @old(g.cells[i] != 0) => g.cells[i] = @old(g.cells[i])"
00074 })
00075 @Modifies("CellGroup.cells.elems")
00076 @Options(ensureAllInts=false)
00077 public void solve() {
00078 Squander.exe(this);
00079 }
00080
00081 public boolean repOK() {
00082 int m = (int) Math.sqrt(n);
00083 for (int i = 0; i < n; i++) {
00084 for (int j = 0; j < n; j++) {
00085 if (rows[i].cells[j] != cols[j].cells[i])
00086 return false;
00087 if (grids[(i/m)*m + j/m].cells[(i%m)*m + j%m] != rows[i].cells[j])
00088 return false;
00089 }
00090 }
00091 return true;
00092 }
00093
00094 public String printSimple() {
00095 StringBuilder sb = new StringBuilder();
00096 for (int i = 0; i < n; i++)
00097 for (int j = 0; j < n; j++)
00098 sb.append(getCellValue(i, j)).append(" ");
00099 return sb.toString().trim();
00100 }
00101
00102 @Override
00103 public String toString() {
00104 StringBuilder sb = new StringBuilder();
00105 int m = (int) Math.sqrt(n);
00106 for (int i = 0; i < n; i++) {
00107 if (i % m == 0)
00108 printHLine(sb, n, m);
00109 for (int j = 0; j < n; j++) {
00110 if (j % m == 0)
00111 sb.append("| ");
00112 sb.append(getCellValue(i, j)).append(" ");
00113 }
00114 sb.append("|\n");
00115 }
00116 printHLine(sb, n, m);
00117 return sb.toString();
00118 }
00119
00120 private void printHLine(StringBuilder sb, int n2, int m) {
00121 for (int i = 0; i < n; i++) {
00122 if (i % m == 0)
00123 sb.append("+-");
00124 sb.append("--");
00125 }
00126 sb.append("+\n");
00127 }
00128
00129 private void init() {
00130 rows = new CellGroup[n];
00131 cols = new CellGroup[n];
00132 grids = new CellGroup[n];
00133 for (int i = 0; i < n; i++) {
00134 rows[i] = new CellGroup(n);
00135 cols[i] = new CellGroup(n);
00136 grids[i] = new CellGroup(n);
00137 }
00138 }
00139
00140 public static Sudoku2 parse(String puzzle) {
00141 String[] vals = puzzle.replaceAll("\\|", " ").split("\\s+");
00142 assert (vals.length > 0);
00143 int n = Integer.parseInt(vals[0]);
00144 assert vals.length == n*n + 1 : "must provide exactly " + n*n + " cell values";
00145 Sudoku2 sudoku = new Sudoku2(n);
00146 for (int i = 0; i < n; i++)
00147 for (int j = 0; j < n; j++)
00148 sudoku.setCellValue(i, j, Integer.parseInt(vals[1 + i*n + j]));
00149 return sudoku;
00150 }
00151
00152 public static void main(String[] args) {
00153
00154 Sudoku2 sudoku = Sudoku2.parse("9 | 8 0 0 6 0 0 0 0 2 |" +
00155 "| 0 4 0 0 5 0 0 1 0 |" +
00156 "| 0 0 0 7 0 0 0 0 3 |" +
00157 "| 0 9 0 0 0 4 0 0 6 |" +
00158 "| 2 0 0 0 0 0 0 0 8 |" +
00159 "| 7 0 0 0 1 0 0 5 0 |" +
00160 "| 3 0 0 0 0 9 0 0 0 |" +
00161 "| 0 1 0 0 8 0 0 9 0 |" +
00162 "| 4 0 0 0 0 2 0 0 5 |");
00163 System.out.println(sudoku);
00164 sudoku.solve();
00165 assert sudoku.repOK();
00166 System.out.println(sudoku);
00167 }
00168
00169 }