include "globals.mzn";

int : n_intervals;
int : n_operations;
int : n_locations;
int : n_moving_obj;

array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_status;
array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_start;
array [1..n_operations, 0..(n_intervals + 1)] of var bool : op_fin;

% 0 - локация не определена.
array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..n_locations : m_obj_loc; % Moving object location.

array [1..n_moving_obj, 1..n_locations] of set of 1..n_operations : arrival_op;
array [1..n_moving_obj, 1..n_locations] of set of 1..n_operations : departure_op;

% Определение m_obj_loc.
constraint forall (obj in 1..n_moving_obj, j in 1..(n_intervals + 1))
    ((m_obj_loc[obj, j] != 0) -> (
        (m_obj_loc[obj, j] == m_obj_loc[obj, j - 1] /\ (forall (k in departure_op[obj, m_obj_loc[obj, j]]) (op_status[k, j - 1] == 0)))
            \/
        (not (forall (k in arrival_op[obj, m_obj_loc[obj, j]]) (op_fin[k, j - 1] == 0)))
    ));

% Начальное состояние.
array [1..n_moving_obj] of var 0..n_locations : initial_m_obj_loc;
constraint forall (i in 1..n_moving_obj) (m_obj_loc[i, 0] = initial_m_obj_loc[i]);

% Конечное состояние.
array [1..n_moving_obj] of var 0..n_locations : final_m_obj_loc;
constraint forall (i in 1..n_moving_obj) (
    (final_m_obj_loc[i] != 0) ->
        (m_obj_loc[i, n_intervals + 1] = final_m_obj_loc[i])
);

constraint forall (i in 1..n_operations, j in {0, n_intervals + 1}) (op_status[i, j] == 0); % Краевые значения.

% Определение op_start и op_fin.
constraint forall (op in 1..n_operations, j in {0, n_intervals + 1})
    (op_start[op, j] == 0 /\ op_fin[op, j] == 0);
constraint forall (i in 1..n_operations, j in 1..(n_intervals + 1)) (op_start[i, j] = (op_status[i, j] /\ not op_status[i, j - 1]));
constraint forall (i in 1..n_operations, j in 1..n_intervals      ) (op_fin  [i, j] = (op_status[i, j] /\ not op_status[i, j + 1]));

% Непрерывность перемещения и швартовки.
array [1..n_operations] of var int : operations_duration;
array [1..n_operations] of var bool : is_continuous_operation;

constraint forall (i in 1..n_operations where is_continuous_operation[i]) (
    let {var int : len = operations_duration[i]} in
    (forall (j in 1..(n_intervals - len + 1)) (
        (op_start[i, j] == 1) -> (
            (forall (k in 1..(len - 1))
                (op_status[i, j + k] == 1)
            ) /\
            (op_status[i, j + len] == 0)
        )
    )) /\
    (forall (j in (n_intervals - len + 2)..(n_intervals + 1))
        (op_start[i, j] == 0)
   )
);

% Наличие всех ресурсов на месте во время начала операции перемещения.
array [1..n_operations] of set of 1..n_moving_obj : operations_resources;
array [1..n_operations] of 0..n_locations : operations_start_loc;

constraint forall (op in 1..n_operations, j in 1..n_intervals) (
    forall (obj in operations_resources[op]) (
        (op_start[op, j]) -> (m_obj_loc[obj, j] == operations_start_loc[op])
    )
);

% Конфликтующие операции.
int : n_conflicting_op;

array [1..n_conflicting_op] of 1..n_operations : confl_op_1;
array [1..n_conflicting_op] of 1..n_operations : confl_op_2;

constraint forall (t in 0..(n_intervals + 1), i in 1..n_conflicting_op) (
    (op_status[confl_op_1[i], t] -> not op_status[confl_op_2[i], t])
);

% Окна непогоды.
int : n_bad_weather_windows;
array [1..n_bad_weather_windows] of 1..n_operations : bw_op;
array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_start;
array [1..n_bad_weather_windows] of 0..(n_intervals + 1) : bw_fin; % Включительно.

constraint forall (i in 1..n_bad_weather_windows, t in bw_start[i]..bw_fin[i]) (
    op_status[bw_op[i], t] == 0
);

% Грузообработка.
int : n_cargo_types;
int : n_obj_with_storage;
array [1..n_obj_with_storage, 0..(n_intervals + 1), 1..n_cargo_types] of var int : storage_used_volume; % Первые n_moving_obj соответствуют наполненности соответствующих движущихся объектов.

% Ограничения на вместимость.
array [1..n_obj_with_storage] of int : max_storage_vol;
constraint forall (storage in 1..n_obj_with_storage, t in 0..(n_intervals + 1)) (
    (sum (cargo in 1..n_cargo_types) (storage_used_volume[storage, t, cargo]) <= max_storage_vol[storage])
        /\
    (forall (cargo in 1..n_cargo_types) (0 <= storage_used_volume[storage, t, cargo]))
);

% Ограничения на граничные значения.
array [1..n_obj_with_storage, 1..n_cargo_types] of int : initial_storage_vol;
array [1..n_obj_with_storage, 1..n_cargo_types] of int : final_storage_vol;
constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types) (
    (storage_used_volume[storage, 0, cargo] = initial_storage_vol[storage, cargo])
        /\
    (if final_storage_vol[storage, cargo] >= 0 then
        (storage_used_volume[storage, (n_intervals + 1), cargo] == final_storage_vol[storage, cargo])
    endif)
);

% Изменение грузов в хранилищах.
array [1..n_obj_with_storage, 0..(n_intervals + 1), 1..n_cargo_types] of int : cargo_flows;

int : n_loading_op;
array [1..n_obj_with_storage, 1..n_cargo_types] of set of 1..n_loading_op : involved_operations;
array [1..n_loading_op] of int : loading_op_delta;
array [1..n_loading_op] of 1..n_operations : loading_op_n; % Номера среди общего списка операций.

constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types, t in 1..(n_intervals + 1)) (
    storage_used_volume[storage, t, cargo] == (
        storage_used_volume[storage, t - 1, cargo] +
        cargo_flows[storage, t, cargo] +
        sum (inv_op in involved_operations[storage, cargo]) (
            loading_op_delta[inv_op] * op_status[loading_op_n[inv_op], t]
        )
    )
);

% Критерий оптимизации
array [0..(n_intervals + 1)] of var bool : is_not_terminated;
constraint (is_not_terminated[0] == 0 /\ is_not_terminated[n_intervals + 1] == 0);

constraint forall (t in 1..n_intervals) (
    is_not_terminated[t] == (
        (exists (op in 1..n_operations) (op_status[op, t] == 1))
            \/
        is_not_terminated[t + 1]
    )
);

solve minimize sum(is_not_terminated);

output [show(sum(is_not_terminated)), "\n",
        show(op_status), "\n\n",
        "m_obj_loc = ", show(m_obj_loc), "\n\n",
        "op_fin = ", show(op_fin), "\n\n",
        "op_start = ", show(op_start), "\n\n",
        "arrival_op = ", show(arrival_op), "\n\n",
        "departure_op = ", show(departure_op), "\n\n",
        "is_not_terminated = ", show(is_not_terminated), "\n\n",
        "storage_used_volume = ", show(storage_used_volume), "\n\n"
        ];