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