| 464 | // / Sudoku solving example. |
| 465 | |
| 466 | @SuppressWarnings({"unchecked", "CodeBlock2Expr"}) |
| 467 | void sudokuExample(Context ctx) throws TestFailedException |
| 468 | { |
| 469 | System.out.println("SudokuExample"); |
| 470 | Log.append("SudokuExample"); |
| 471 | |
| 472 | // 9x9 matrix of integer variables |
| 473 | List<List<Expr<IntSort>>> X = IntStream.range(0, 9).mapToObj(i -> IntStream.range(0, 9).mapToObj(j -> |
| 474 | ctx.mkConst(ctx.mkSymbol(String.format("x_%d_%d", i + 1, j + 1)), ctx.getIntSort())) |
| 475 | .collect(Collectors.toList())).collect(Collectors.toList()); |
| 476 | |
| 477 | // each cell contains a value in {1, ..., 9} |
| 478 | List<List<BoolExpr>> cells_c = X.stream().map(r -> r.stream().map(c -> |
| 479 | ctx.mkAnd(ctx.mkLe(ctx.mkInt(1), c), ctx.mkLe(c, ctx.mkInt(9)))) |
| 480 | .collect(Collectors.toList())).collect(Collectors.toList()); |
| 481 | |
| 482 | // each row contains a digit at most once |
| 483 | List<BoolExpr> rows_c = new ArrayList<>(); |
| 484 | for (int i1 = 0; i1 < 9; i1++) { |
| 485 | BoolExpr boolExpr = ctx.mkDistinct(X.get(i1).toArray(new Expr[0])); |
| 486 | rows_c.add(boolExpr); |
| 487 | } |
| 488 | |
| 489 | // each column contains a digit at most once |
| 490 | List<BoolExpr> cols_c = new ArrayList<>(); |
| 491 | for (int idx = 0; idx < 9; idx++) { |
| 492 | int j1 = idx; |
| 493 | BoolExpr boolExpr = ctx.mkDistinct(X.stream().map(r -> r.get(j1)).toArray(Expr[]::new)); |
| 494 | cols_c.add(boolExpr); |
| 495 | } |
| 496 | |
| 497 | // each 3x3 square contains a digit at most once |
| 498 | List<List<BoolExpr>> sq_c = new ArrayList<>(); |
| 499 | for (int i0 = 0; i0 < 3; i0++) { |
| 500 | List<BoolExpr> collect = new ArrayList<>(); |
| 501 | for (int j0 = 0; j0 < 3; j0++) { |
| 502 | List<Expr<IntSort>> list = new ArrayList<>(); |
| 503 | for (int i = 0; i < 3; i++) { |
| 504 | for (int j = 0; j < 3; j++) { |
| 505 | Expr<IntSort> intSortExpr = X.get(3 * i0 + i).get(3 * j0 + j); |
| 506 | list.add(intSortExpr); |
| 507 | } |
| 508 | } |
| 509 | BoolExpr boolExpr = ctx.mkDistinct(list.toArray(new Expr[0])); |
| 510 | collect.add(boolExpr); |
| 511 | } |
| 512 | sq_c.add(collect); |
| 513 | } |
| 514 | |
| 515 | Stream<BoolExpr> sudoku_s = cells_c.stream().flatMap(Collection::stream); |
| 516 | sudoku_s = concat(sudoku_s, rows_c.stream()); |
| 517 | sudoku_s = concat(sudoku_s, cols_c.stream()); |
| 518 | sudoku_s = concat(sudoku_s, sq_c.stream().flatMap(Collection::stream)); |
| 519 | BoolExpr sudoku_c = ctx.mkAnd(sudoku_s.toArray(BoolExpr[]::new)); |
| 520 | |
| 521 | // sudoku instance, we use '0' for empty cells |
| 522 | int[][] instance = { |
| 523 | { 0, 0, 0, 0, 9, 4, 0, 3, 0 }, |