% Type-inst synonyms for record types used in the model
type Dimensions = record(int: width, int: height);
type Coordinates = record(var 0..infinity: x, var 0..infinity: y);
type Rectangle = Dimensions ++ Coordinates;
% No overlap predicate
predicate no_overlap(Rectangle: rectA, Rectangle: rectB) =
rectA.x + rectA.width <= rectB.x
\/ rectB.x + rectB.width <= rectA.x
\/ rectA.y + rectA.height <= rectB.y
\/ rectB.y + rectB.height <= rectA.y;
% Instance data
array[_] of Dimensions: rectDim;
Dimensions: area;
% Decision variables
array[index_set(rectDim)] of Coordinates: rectCoord ::no_output;
array[_] of Rectangle: rectangles ::output = [ rectDim[i] ++ rectCoord[i] | i in index_set(rectDim)];
% Constraint: rectangles must be placed within the area
constraint forall(rect in rectangles) (
rect.x + rect.width <= area.width
/\ rect.y + rect.height <= area.height
);
% Constraint: no rectangles can overlap
constraint forall(i, j in index_set(rectangles) where i < j) (
no_overlap(rectangles[i], rectangles[j])
);