Skip to content

Commit 17bf744

Browse files
committed
#407: add InterruptedException into examples.
1 parent 7659db3 commit 17bf744

File tree

3 files changed

+14
-8
lines changed

3 files changed

+14
-8
lines changed

src/org/sosy_lab/java_smt/example/Binoxxo.java

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -193,7 +193,7 @@ private List<BooleanFormula> getAssignments(S symbols, char[][] grid) {
193193
/** convert one user-given value at given coordinate into a constraint for the solver. */
194194
abstract BooleanFormula getAssignment(S symbols, int row, int col, char value);
195195

196-
abstract char getValue(S symbols, Model model, int row, int col);
196+
abstract char getValue(S symbols, Model model, int row, int col) throws InterruptedException;
197197

198198
/**
199199
* Solves a Binoxxo using the given grid values and returns a possible solution. Return <code>
@@ -324,7 +324,8 @@ BooleanFormula getAssignment(IntegerFormula[][] symbols, int row, int col, char
324324
}
325325

326326
@Override
327-
char getValue(IntegerFormula[][] symbols, Model model, int row, int col) {
327+
char getValue(IntegerFormula[][] symbols, Model model, int row, int col)
328+
throws InterruptedException {
328329
@Nullable BigInteger value = model.evaluate(symbols[row][col]);
329330
return value == null ? '.' : value.intValue() == 0 ? 'O' : 'X';
330331
}
@@ -421,7 +422,8 @@ BooleanFormula getAssignment(BooleanFormula[][] symbols, int row, int col, char
421422
}
422423

423424
@Override
424-
char getValue(BooleanFormula[][] symbols, Model model, int row, int col) {
425+
char getValue(BooleanFormula[][] symbols, Model model, int row, int col)
426+
throws InterruptedException {
425427
@Nullable Boolean value = model.evaluate(symbols[row][col]);
426428
return value == null ? '.' : value ? 'X' : 'O';
427429
}

src/org/sosy_lab/java_smt/example/NQueens.java

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -260,7 +260,8 @@ private List<BooleanFormula> diagonalRule(BooleanFormula[][] symbols) {
260260
* @param col the column index of the cell to check.
261261
* @return true if a queen is placed on the cell, false otherwise.
262262
*/
263-
private boolean getValue(BooleanFormula[][] symbols, Model model, int row, int col) {
263+
private boolean getValue(BooleanFormula[][] symbols, Model model, int row, int col)
264+
throws InterruptedException {
264265
return Boolean.TRUE.equals(model.evaluate(symbols[row][col]));
265266
}
266267

src/org/sosy_lab/java_smt/example/Sudoku.java

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -195,7 +195,7 @@ private List<BooleanFormula> getAssignments(S symbols, Integer[][] grid) {
195195
/** convert one user-given value at given coordinate into a constraint for the solver. */
196196
abstract BooleanFormula getAssignment(S symbols, int row, int col, Integer value);
197197

198-
abstract Integer getValue(S symbols, Model model, int row, int col);
198+
abstract Integer getValue(S symbols, Model model, int row, int col) throws InterruptedException;
199199

200200
/**
201201
* Solves a sudoku using the given grid values and returns a possible solution. Return <code>
@@ -314,7 +314,8 @@ BooleanFormula getAssignment(IntegerFormula[][] symbols, int row, int col, Integ
314314
}
315315

316316
@Override
317-
Integer getValue(IntegerFormula[][] symbols, Model model, int row, int col) {
317+
Integer getValue(IntegerFormula[][] symbols, Model model, int row, int col)
318+
throws InterruptedException {
318319
return model.evaluate(symbols[row][col]).intValue();
319320
}
320321
}
@@ -413,7 +414,8 @@ BooleanFormula getAssignment(BooleanFormula[][][] symbols, int row, int col, Int
413414
}
414415

415416
@Override
416-
Integer getValue(BooleanFormula[][][] symbols, Model model, int row, int col) {
417+
Integer getValue(BooleanFormula[][][] symbols, Model model, int row, int col)
418+
throws InterruptedException {
417419
for (int value = 0; value < SIZE; value++) {
418420
if (model.evaluate(symbols[row][col][value])) {
419421
return value + 1; // off-by-one!
@@ -516,7 +518,8 @@ BooleanFormula getAssignment(EnumerationFormula[][] symbols, int row, int col, I
516518
}
517519

518520
@Override
519-
Integer getValue(EnumerationFormula[][] symbols, Model model, int row, int col) {
521+
Integer getValue(EnumerationFormula[][] symbols, Model model, int row, int col)
522+
throws InterruptedException {
520523
String value = model.evaluate(symbols[row][col]);
521524
for (int i = 0; i < VALUES.length; i++) {
522525
if (VALUES[i].equals(value)) {

0 commit comments

Comments
 (0)