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