Download
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]]
])
])
])
This work is licensed under a Creative Commons Attribution 4.0 International License.