132: A Layout Problem

language ESSENCE 1.2.0
$ prob132.essence: A Layout Problem
$ Problem details available in:
$   Exploiting Symmetries Within Constraint Satisfaction Search
$   P. Meseguer, C. Torras
$   Artificial Intelligence, Volume 129, Number 1, June 2001, pp. 133-163
$
$ 01 August 2007
$

$ x_max: maximum x dimension
$ y_max: maximum y dimension
$ n_shapes: the number of shapes to fit in to the grid
given x_max, y_max, n_shapes : int(1..)

$ Shape: identifiers for individual shapes
$ X: a position on the x-axis
$ Y: a position on the y-axis
$ Cell: the domain consisting of cells on the grid
letting Shape be domain int(1..n_shapes),
        X be domain int(1..x_max),
        Y be domain int(1..y_max),
        Cell be domain tuple (X,Y)

$ grid: the set of pairs of x and y coordinates that make up the grid shape
$ form: the form of each shape, as a set of pairs of x and y coordinates
given grid : set of Cell,
      form : function (total) Shape --> set of Cell

$ layout: a mapping from each cell in the grid to the shape id occupying it
find layout : function Cell --> Shape

such that
$ only cells in the grid are part of the layout
    forAll c in defined(layout) . c in grid,
$ the cells that map to a shape match the shape's form.
$ this is long and complicated because we need the minimum x and y coordinates
$ (min(sx) and min(sy)) that map to each shape, and i can't think of a nicer way
$ of getting them...
    forAll s : Shape . exists sx : set of X . exists sy : set of Y .
        (forAll (x,y) : Cell . x in sx /\ y in sy <-> (x,y) in preImage(layout,s)) /\
        forAll (x,y) in form(s) . layout((min(sx) + x,min(sy) + y)) = s,
$ a shape has exactly the right number of cells mapping to it
    forAll s : Shape . |form(s)| = |preImage(layout,s)|