Langford-positional.essence

language Essence 1.3
$ prob024.essence: Langford's Number Problem
$ Problem details available at http://www.csplib.org/Problems/prob024

$ numbers 1 to n, each appearing k times in a sequence (of length k*n)
given k : int(2..)
given n : int(1..)

letting number be domain int(1..n)
letting repetition be domain int(1..k)
letting position be domain int(1..k*n)

$ The positions of all repetitions of all numbers
find pos : function (total, injective)
                    tuple (number, repetition) --> position

$ Occurrences of number i must be i+1 places apart.
$ So if the number 4 appers at position 3,
$ the next occurrence of it must be at position 8,
$ leaving a gap of 4 positions.
such that
    forAll i : number .
        forAll j : int(2..k) .
            pos(tuple (i,j)) = pos(tuple (i,j-1)) + i + 1

$ Symmetry breaking.
$ The first occurrence of the number 1 is closer to the beginning than
$ the last occurrence of the number 1 is to the end.
such that
    pos(tuple (1,1)) - 1 < k*n - pos(tuple (1,k))