012: Nonogram

language ESSENCE 1.3.0

$ Problem Nonogram
$
$ Problem details available at http://www.csplib.org/Problems/prob012/
$
$ Essence model by Andrew Martin
$
$ Licenced under CC-BY-4.0 : http://creativecommons.org/licenses/by/4.0/

given nGrid : int(1..)
given maxRules : int(1..)

letting dGrid be domain int(1..nGrid)
letting dRules be domain int(1..maxRules)

given rowRules : matrix indexed by [dGrid, dRules] of int(0..)
given colRules : matrix indexed by [dGrid, dRules] of int(0..)

$ gird is 1 if cell is filled, 0 otherwise.
find grid : matrix indexed by [dGrid, dGrid] of int(0..1)

such that
    $ FOR EACH COLUMN
    forAll column : dGrid .

        $ SUM OF ELEMENTS IN COLUMN MUST EQUAL SUM OF HINTS IN RULE
        ((sum i : dGrid . grid[i][column]) = (sum j : dRules . colRules[column][j]))
        /\

        $ THERE EXISTS A MAPPING FROM dRULES TO dGRID
        exists startingIndexes : matrix indexed by [dRules] of dGrid

            $ FOR EACH RULE
            . forAll ruleIndex : dRules

                $ EITHER - RULE IS ZERO
                . colRules[column][ruleIndex] = 0

                    $ OR
                    \/

                    $EACH RULE STARTS AT A POSITION > THE LAST RULE
                    $OR IS THE FIRST RULE
                    ((ruleIndex = 1
                    \/
                    startingIndexes[ruleIndex] > startingIndexes[ruleIndex - 1])
                    /\

                    $RANGE IN LOCATION GIVEN MUST BE ALL 1's
                    $sum of all elements in range is equal to size of range
                    ( (sum i : int(startingIndexes[ruleIndex]..(startingIndexes[ruleIndex] + colRules[column][ruleIndex] - 1) ) . grid[i][column]) = colRules[column][ruleIndex])
                    $ RANGE MUST BE CONTAINED BY 0's
                    /\
                    (startingIndexes[ruleIndex] = 1
                    \/
                    grid[(startingIndexes[ruleIndex])-1][column] = 0)
                    /\
                    ((startingIndexes[ruleIndex] + colRules[column][ruleIndex] - 1) = nGrid
                    \/
                    grid[(startingIndexes[ruleIndex] + colRules[column][ruleIndex])][column] = 0) )


such that

    $ FOR EACH ROW
    forAll row : dGrid .

        $ SUM OF ELEMENTS IN COLUMN MUST EQUAL SUM OF HINTS IN RULE
        ((sum i : dGrid . grid[row][i]) = (sum j : dRules . rowRules[row][j]))
        /\

        $ THERE EXISTS A MAPPING FROM dRULES TO dGRID
        exists startingIndexes : matrix indexed by [dRules] of int(0..nGrid)

            $ FOR EACH RULE
            . forAll ruleIndex : dRules

                $ EITHER - RULE IS ZERO
                . rowRules[row][ruleIndex] = 0

                    $ OR
                    \/

                    $EACH ELEMENT IS > PREV ELEMENT OR THE FIRST ELEMENT
                    (( ruleIndex = 1
                    \/
                    startingIndexes[ruleIndex] > startingIndexes[ruleIndex - 1])
                    /\

                    $RANGE IN LOCATION GIVEN MUST BE ALL 1's
                    ( (sum i : int(startingIndexes[ruleIndex]..(startingIndexes[ruleIndex] + rowRules[row][ruleIndex] - 1) ) . grid[row][i]) = rowRules[row][ruleIndex])
                    $ RANGE MUST BE CONTAINED BY 0's
                    /\
                    (startingIndexes[ruleIndex] = 1
                    \/
                    grid[row][(startingIndexes[ruleIndex])-1] = 0)
                    /\
                    ((startingIndexes[ruleIndex] + rowRules[row][ruleIndex] - 1) = nGrid
                    \/
                    grid[row][(startingIndexes[ruleIndex] + rowRules[row][ruleIndex])] = 0) )