include "globals.mzn";
include "flatzinc.mzn";
int: c; % number of customers
set of int: Custs = 1..c;
array[Custs,Custs] of bool: F;
array[Custs] of var Custs: s; % customer start time
array[Custs] of var Custs: e :: is_output; % customer end time
array[Custs] of var Custs: x;
var Custs: stacks :: is_output; % number of stacks required
array[Custs,Custs] of var bool: so; % whether customer started before certain time
array[Custs,Custs] of var bool: eo; % whether customer ended after certain time
array[Custs,Custs] of var bool: o; % whether customer was open at certain time
constraint inverse(e,x) :: domain;
constraint forall (i in Custs) (minimum(s[i], [e[j] | j in Custs where F[i,j]]));
constraint forall (i, t in Custs) (so[i,t] = (s[i] <= t));
constraint forall (i, t in Custs) (eo[i,t] = (e[i] >= t));
constraint forall (i, t in Custs) (o[i,t] = (so[i,t] /\ eo[i,t]));
constraint forall (t in Custs) (stacks >= sum (i in Custs) (bool2int(o[i,t])));
% Dominance breaking constraints
array[Custs,Custs] of var bool: r; % whether customer was ready to close at certain time
% if all customers sharing a product has already opened and we have not closed, we are ready to close now
constraint forall (i, t in Custs) (
r[i,t] = forall ([so[j,t] | j in Custs where F[i,j]] ++ [eo[i,t]]));
% If none of the lex better customers are ready to close now but we are, we close now
constraint forall (i in Custs, t in 1..c-1) (
bool_clause([r[j,t] | j in 1..i-1], [r[i,t], eo[i,t+1]]));
solve :: int_search(x, input_order, indomain_min, complete) minimize stacks;