|
1 | 1 | language Essence 1.3
|
2 | 2 |
|
3 |
| -given nbDom : int(1..) |
4 |
| -letting dom be domain int(1..nbDom) |
5 |
| -given bound : int(1..100) |
6 |
| -letting Postion be domain (int(1..bound),int(1..bound)) |
| 3 | +given numDigits : int |
| 4 | +given dimension : int |
7 | 5 |
|
8 |
| -given numClues : int(1..bound**2) |
9 |
| -letting Clue be domain int(1..numClues) |
10 |
| -letting Arg be domain int(1..numClues) |
| 6 | +letting digit be domain int(0..9) |
| 7 | +letting number be domain int(0..10**numDigits) |
11 | 8 |
|
12 |
| -letting Type be new type enum {Add, Modulo} |
13 |
| -$ locations |
14 |
| -given l : function (total,injective) Clue --> (Type, Arg, Arg, Postion ) |
| 9 | +find grid : matrix indexed by [int(1..dimension), int(1..dimension)] of int(0..9) |
| 10 | +branching on [grid] |
15 | 11 |
|
16 | 12 |
|
17 |
| -find grid : matrix indexed by [int(1..bound),int(1..bound)] of dom |
| 13 | +$ the black blocks |
| 14 | +given blackCells : set of (int, int) |
| 15 | +such that |
| 16 | + forAll (row, col) in blackCells . grid[row,col] = 0 |
| 17 | + |
| 18 | + |
| 19 | +given acrossClueCoords : set of ( int $ seq |
| 20 | + , int $ the row |
| 21 | + , int $ the starting column |
| 22 | + , int $ the ending column |
| 23 | + ) |
| 24 | +letting acrossIndex be domain int([i[1] | i <- acrossClueCoords]) |
| 25 | +find across : matrix indexed by [acrossIndex] of number |
| 26 | +find acrossDigits : matrix indexed by [acrossIndex] of sequence (maxSize numDigits) of digit |
| 27 | +such that |
| 28 | + forAll (seq, row, colStart, colEnd) in acrossClueCoords . |
| 29 | + acrossDigits[seq] = [ grid[row,col] | col : int(colStart..colEnd) ] |
| 30 | + |
| 31 | + |
| 32 | +given downClueCoords : set of ( int $ seq |
| 33 | + , int $ the col |
| 34 | + , int $ the starting row |
| 35 | + , int $ the ending row |
| 36 | + ) |
| 37 | +letting downIndex be domain int([i[1] | i <- downClueCoords]) |
| 38 | +find down : matrix indexed by [downIndex ] of number |
| 39 | +find downDigits : matrix indexed by [downIndex ] of sequence (maxSize numDigits) of digit |
| 40 | +such that |
| 41 | + forAll (seq, col, rowStart, rowEnd) in downClueCoords . |
| 42 | + downDigits[seq] = [ grid[row,col] | row : int(rowStart..rowEnd) ] |
| 43 | + |
| 44 | +$ connecting digits to numbers |
| 45 | +such that |
| 46 | + forAll n : acrossIndex . |
| 47 | + across[n] = sum (i,d) in acrossDigits[n] . (10**max([0,|acrossDigits[n]|-i])) * d, |
| 48 | + forAll n : downIndex . |
| 49 | + down[n] = sum (i,d) in downDigits[n] . (10**max([0,|downDigits[n]|-i])) * d |
18 | 50 |
|
19 | 51 |
|
| 52 | +$ first digits are >1 |
| 53 | +$ this is probably implied, but having it just in case. |
20 | 54 | such that
|
| 55 | + forAll n : acrossIndex . acrossDigits[n](1) > 0, |
| 56 | + forAll n : downIndex . downDigits[n](1) > 0 |
| 57 | + |
| 58 | + |
| 59 | +letting AD be new type enum {A, D} |
| 60 | +letting CLUE be domain |
| 61 | + variant |
| 62 | + { is_constant : int |
| 63 | + , is_square : bool |
| 64 | + , is_prime : bool |
| 65 | + , plus_constant : (int, AD, int) |
| 66 | + , minus_constant : (int, AD, int) |
| 67 | + , times_constant : (int, AD, int) |
| 68 | + , div_constant : (int, AD, int) |
| 69 | + , times : (int, AD, int, AD) |
| 70 | + } |
| 71 | +given clues : set of (AD, int, CLUE) |
| 72 | + |
| 73 | +$ clues |
| 74 | +such that |
| 75 | + forAll (targetKind, targetNum, clue) in clues . |
| 76 | + and( |
| 77 | + [ targetKind = A -> and( |
| 78 | + [ active(clue, is_constant) -> across[targetNum] = clue[is_constant] |
| 79 | + , active(clue, is_square ) -> exists i : number . i**2 = across[targetNum] |
| 80 | + , active(clue, is_prime ) -> and([ across[targetNum] % i != 0 |
| 81 | + | i : number |
| 82 | + , i >= 2 |
| 83 | + , i**2 <= across[targetNum] |
| 84 | + ]) |
| 85 | + , active(clue, plus_constant) -> and( |
| 86 | + [ clue[plus_constant ][2] = A -> across[targetNum] = across[clue[plus_constant ][1]] + clue[plus_constant ][3] |
| 87 | + , clue[plus_constant ][2] = D -> across[targetNum] = down [clue[plus_constant ][1]] + clue[plus_constant ][3] |
| 88 | + ]) |
| 89 | + , active(clue, minus_constant) -> and( |
| 90 | + [ clue[minus_constant][2] = A -> across[targetNum] = across[clue[minus_constant][1]] - clue[minus_constant][3] |
| 91 | + , clue[minus_constant][2] = D -> across[targetNum] = down [clue[minus_constant][1]] - clue[minus_constant][3] |
| 92 | + ]) |
| 93 | + , active(clue, times_constant) -> and( |
| 94 | + [ clue[times_constant][2] = A -> across[targetNum] = across[clue[times_constant][1]] * clue[times_constant][3] |
| 95 | + , clue[times_constant][2] = D -> across[targetNum] = down [clue[times_constant][1]] * clue[times_constant][3] |
| 96 | + ]) |
| 97 | + , active(clue, div_constant) -> and( |
| 98 | + [ clue[div_constant ][2] = A -> across[targetNum] = across[clue[div_constant ][1]] / clue[div_constant ][3] |
| 99 | + , clue[div_constant ][2] = D -> across[targetNum] = down [clue[div_constant ][1]] / clue[div_constant ][3] |
| 100 | + ]) |
| 101 | + , active(clue, times) -> and( |
| 102 | + [ (clue[times][2], clue[times][4]) = (A, A) -> across[targetNum] = across[clue[times][1]] * across[clue[times][3]] |
| 103 | + , (clue[times][2], clue[times][4]) = (A, D) -> across[targetNum] = across[clue[times][1]] * down [clue[times][3]] |
| 104 | + , (clue[times][2], clue[times][4]) = (D, A) -> across[targetNum] = down [clue[times][1]] * across[clue[times][3]] |
| 105 | + , (clue[times][2], clue[times][4]) = (D, D) -> across[targetNum] = down [clue[times][1]] * down [clue[times][3]] |
| 106 | + ]) |
| 107 | + ]) |
| 108 | + |
| 109 | + , targetKind = D -> and( |
| 110 | + [ active(clue, is_constant) -> down[targetNum] = clue[is_constant] |
| 111 | + , active(clue, is_square ) -> exists i : number . i**2 = down[targetNum] |
21 | 112 |
|
22 |
| -forAll i : Clue . ( |
23 |
| - l(i)[1] = Add -> |
24 |
| - grid[ l(i)[4,1], l(i)[4,2] ] = |
25 |
| - grid[ l( l(i)[2] )[4,1] , l( l(i)[2] )[4,2] ] |
26 |
| - + grid[ l( l(i)[3] )[4,1] , l( l(i)[3] )[4,2] ] ) /\ ( |
27 |
| - |
28 |
| - l(i)[1] = Modulo -> |
29 |
| - grid[ l(i)[4,1], l(i)[4,2] ] = |
30 |
| - grid[ l( l(i)[2] )[4,1] , l( l(i)[2] )[4,2] ] |
31 |
| - % grid[ l( l(i)[3] )[4,1] , l( l(i)[3] )[4,2] ] |
32 |
| -) |
| 113 | + , active(clue, is_prime ) -> and([ down[targetNum] % i != 0 |
| 114 | + | i : number |
| 115 | + , i >= 2 |
| 116 | + , i**2 <= down[targetNum] |
| 117 | + ]) |
| 118 | + , active(clue, plus_constant) -> and( |
| 119 | + [ clue[plus_constant ][2] = A -> down[targetNum] = across[clue[plus_constant ][1]] + clue[plus_constant ][3] |
| 120 | + , clue[plus_constant ][2] = D -> down[targetNum] = down [clue[plus_constant ][1]] + clue[plus_constant ][3] |
| 121 | + ]) |
| 122 | + , active(clue, minus_constant) -> and( |
| 123 | + [ clue[minus_constant][2] = A -> down[targetNum] = across[clue[minus_constant][1]] - clue[minus_constant][3] |
| 124 | + , clue[minus_constant][2] = D -> down[targetNum] = down [clue[minus_constant][1]] - clue[minus_constant][3] |
| 125 | + ]) |
| 126 | + , active(clue, times_constant) -> and( |
| 127 | + [ clue[times_constant][2] = A -> down[targetNum] = across[clue[times_constant][1]] * clue[times_constant][3] |
| 128 | + , clue[times_constant][2] = D -> down[targetNum] = down [clue[times_constant][1]] * clue[times_constant][3] |
| 129 | + ]) |
| 130 | + , active(clue, div_constant) -> and( |
| 131 | + [ clue[div_constant ][2] = A -> down[targetNum] = across[clue[div_constant ][1]] / clue[div_constant ][3] |
| 132 | + , clue[div_constant ][2] = D -> down[targetNum] = down [clue[div_constant ][1]] / clue[div_constant ][3] |
| 133 | + ]) |
| 134 | + , active(clue, times) -> and( |
| 135 | + [ (clue[times][2], clue[times][4]) = (A, A) -> down[targetNum] = across[clue[times][1]] * across[clue[times][3]] |
| 136 | + , (clue[times][2], clue[times][4]) = (A, D) -> down[targetNum] = across[clue[times][1]] * down [clue[times][3]] |
| 137 | + , (clue[times][2], clue[times][4]) = (D, A) -> down[targetNum] = down [clue[times][1]] * across[clue[times][3]] |
| 138 | + , (clue[times][2], clue[times][4]) = (D, D) -> down[targetNum] = down [clue[times][1]] * down [clue[times][3]] |
| 139 | + ]) |
| 140 | + ]) |
| 141 | + ]) |
0 commit comments