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)|