annotation indexical_min(var int: x, var int: y);

include "cumulative.mzn";
include "diffn.mzn";
include "prolog.plz";
include "dichotomy.plz";
include "interval_splitting.plz";

int: n;
int: max_size;
array[1..n-1] of var 1..max_size: x;
array[1..n-1] of var 1..max_size: y;
var 0..max_size: w;
var 0..max_size: h;
var 0..max_size * max_size: area;

constraint diffn(x, y, [i+1 | i in 1..n-1], [i+1 | i in 1..n-1]);
constraint cumulative(x, [i+1 | i in 1..n-1], [i+1 | i in 1..n-1], h);
constraint cumulative(y, [i+1 | i in 1..n-1], [i+1 | i in 1..n-1], w);

constraint forall(i in 1..n-1) (x[i] <= w - i /\ y[i] <= h - i);
constraint w * h = area;
constraint sum([(i+1)*(i+1) | i in 1..n-1]) < area;
constraint x[n-1] <= (w - n + 2) div 2;
constraint y[n-1] <= (h + 1) div 2;
constraint w <= h;
constraint w >= 2 * n - 1 \/ h >= (n * n + n - ((w + 1) div 2 - 1) * ((w + 1) div 2 - 1) - ((w + 1) div 2 - 1)) div 2;

interval_splitting_list(L, S, Stop) :-
   (S <= Stop ; S > Stop, L = []).
interval_splitting_list([H | T], S, Stop) :-
   S > Stop,
   interval_splitting(H, max(1, (S * 3) div 10) + 1, 0, max_size),
   interval_splitting_list(T, S - 1, Stop).

:- int_search([area, w], input_order, indomain_min, complete),
   reverse(x, RXs),
   interval_splitting_list(RXs, n, 6),
   %int_search(RXs, input_order, indomain_split, complete),
   reverse(y, RYs),
   interval_splitting_list(RYs, n, 0).
   %int_search(RYs, input_order, indomain_split, complete).

% PhM 02/04/2015: bug dans le code de Thierry: les x et y commencent à 1 et non 0, le rectangle englobant est décalé de 1

output
   ["%Solution found: " ++ show(w) ++ "x" ++ show(h) ++ "(=" ++ show(area) ++ ")\n"]
   ++ ["\\draw (1, 1) rectangle (" ++ show(w+1) ++ ", " ++ show(h+1) ++ ");\n"]
   ++ ["\\draw (" ++ show(x[i]) ++ ", " ++ show(y[i]) ++ ") rectangle ++(" ++ show(i+1) ++ ", " ++ show(i+1) ++ ") ++(" ++ show(-int2float(i+1)/2.0) ++ ", " ++ show(-int2float(i+1)/2.0) ++ ") node {" ++ show(i+1) ++ "};\n" | i in 1..n-1];

n = 14;
max_size = 200;