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;

int : moving_op_of_obj_max_size;
array [1..n_moving_obj] of 0..moving_op_of_obj_max_size : moving_op_of_obj_sizes;
array [1..n_moving_obj, 1..moving_op_of_obj_max_size] of 1..n_operations : moving_op_of_obj; % Операции перемещения затрагивающие данный объект.

array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..moving_op_of_obj_max_size : current_moving_operation; % Текущая операция операция перемещения, в которой задействован данный объект.
    % Текущая операция лежит в множестве тех, которые затрагивают данный объект.
    constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) (
        current_moving_operation[obj, t] <= moving_op_of_obj_sizes[obj]
    );

    % Если операция, затрагивающая данный объект, выполняется - то именно она текущая операция перемещения для этого объекта.
    constraint forall (obj in 1..n_moving_obj, op_no in 1..moving_op_of_obj_sizes[obj], t in 0..(n_intervals + 1)) (
        (op_status[moving_op_of_obj[obj, op_no], t]) -> (current_moving_operation[obj, t] = op_no)
    );

    % Если объект движется, то выполняется какая-то операция перемещения, касаящаяся этого объекта.
    constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) (
        (current_moving_operation[obj, t] > 0) ->
            (exists (op_no in 1..moving_op_of_obj_sizes[obj]) (op_status[moving_op_of_obj[obj, op_no], t]))
    );

array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_m_obj_in_movement_before_start; % Находится ли объект в движении перед началом интервала.
    % В начале никто не движется.
    constraint forall (obj in 1..n_moving_obj) (not is_m_obj_in_movement_before_start[obj, 0]);
    % Перед первым интервалом все тоже стоят на месте.
    constraint forall (obj in 1..n_moving_obj) (not is_m_obj_in_movement_before_start[obj, 1]);

    % Если в предыдущем интервале объект не движется - то в начале этого он не движется, иначе он движется если предыдущая операция не закончилась.
    constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) (
        if (current_moving_operation[obj, t - 1] = 0) then
            is_m_obj_in_movement_before_start[obj, t] = false
        else
            is_m_obj_in_movement_before_start[obj, t] = (current_moving_operation[obj, t - 1] == current_moving_operation[obj, t])
        endif
    );

array [1..n_operations] of 1..n_locations : operations_destination; % Локация в которой окажется объект после завершения операции.

% Теперь m_obj_loc означает где объект стоит или куда он движется перед началом определённого интервала.
array [1..n_moving_obj, 0..(n_intervals + 1)] of var 1..n_locations : m_obj_loc; % Moving object location.
    % За фиктивный нулевой интервал объект не успевает ничего сделать с начальным положением.
    constraint forall (obj in 1..n_moving_obj) (
        m_obj_loc[obj, 1] = m_obj_loc[obj, 0]
    );

    % Направление движения/местоположение объекта может измениться только если перед этим началась операция перемещения.
    constraint forall (obj in 1..n_moving_obj, t in 2..(n_intervals + 1)) (
        if ((current_moving_operation[obj, t - 1] != current_moving_operation[obj, t - 2]) /\
            (current_moving_operation[obj, t - 1] != 0)) then
            m_obj_loc[obj, t] = operations_destination[moving_op_of_obj[obj, current_moving_operation[obj, t - 1]]]
        else
            m_obj_loc[obj, t] = m_obj_loc[obj, t - 1]
        endif
    );

% Начальное состояние.
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] = false /\ op_fin[op, j] = false);
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 int : operations_duration;
array [1..n_operations] of 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]))
                /\
            (not op_status[i, j + len])
        )
    )) /\
    (forall (j in (n_intervals - len + 2)..(n_intervals + 1)) (op_start[i, j] == false))
);

% Наличие всех ресурсов на месте во время начала операции перемещения.

int : operations_resources_max_size;
array [1..n_operations] of 0..operations_resources_max_size : operations_resources_sizes;
array [1..n_operations, 1..operations_resources_max_size] of 1..n_moving_obj : operations_resources;
array [1..n_operations, 1..operations_resources_max_size] of 0..n_locations : operations_resources_start_loc; % Положения ресурсов в момент начала операции.

constraint forall (op in 1..n_operations, t in 1..n_intervals) (
    forall (op_res_id in 1..operations_resources_sizes[op]) (
        (op_start[op, t]) -> ((m_obj_loc[operations_resources[op, op_res_id], t] == operations_resources_start_loc[op, op_res_id]) /\
                              (not is_m_obj_in_movement_before_start[operations_resources[op, op_res_id], t]))
    )
);

% Конфликтующие операции.
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] == false
);

% Грузообработка.
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]
);
constraint forall (storage in 1..n_obj_with_storage, t in 0..(n_intervals + 1), 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) ( % Initial values.
    storage_used_volume[storage, 0, cargo] = initial_storage_vol[storage, cargo]
);

constraint forall (storage in 1..n_obj_with_storage, cargo in 1..n_cargo_types) ( % Final values.
    if final_storage_vol[storage, cargo] >= 0 then
        storage_used_volume[storage, n_intervals + 1, cargo] == final_storage_vol[storage, cargo]
    else true
    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_loading_op] of int : loading_op_delta;
array [1..n_loading_op] of 1..n_operations : loading_op_n; % Номера среди общего списка операций.
/*
    array [1..n_obj_with_storage, 1..n_cargo_types] of set of 1..n_loading_op : involved_operations;

    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]
            )
        )
    );
*/

int : involved_operations_max_size;
array [1..n_obj_with_storage, 1..n_cargo_types] of 0..involved_operations_max_size : involved_operations_sizes;
array [1..n_obj_with_storage, 1..n_cargo_types, 1..involved_operations_max_size] of 1..n_loading_op : involved_operations;

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_no in 1..involved_operations_sizes[storage, cargo]) (
            loading_op_delta[involved_operations[storage, cargo, inv_op_no]] *
            op_status[loading_op_n[involved_operations[storage, cargo, inv_op_no]], t]
        )
    )
);

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

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

/* Сломано...
% Ограничение на совершение полезной операции при движении назад (окончание отшвартовки - "полезная операция").

array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..n_locations : next_m_obj_loc; % Позиция движущегося объекта на ближайшей остановке.
    constraint forall (obj in 1..n_moving_obj) (next_m_obj_loc[obj, n_intervals + 1] = m_obj_loc[obj, n_intervals + 1]);

    constraint forall (obj in 1..n_moving_obj, t in 0..n_intervals) (
        next_m_obj_loc[obj, t] =
            if (m_obj_loc[obj, t] = 0) then
                next_m_obj_loc[obj, t + 1]
            else
                m_obj_loc[obj, t]
            endif
    );

array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..n_locations : prev_m_obj_loc; % Строго предыдущая позиция объекта.
    constraint forall (obj in 1..n_moving_obj) (prev_m_obj_loc[obj, 0] = 0);

    constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) (
        prev_m_obj_loc[obj, t] =
            if ((m_obj_loc[obj, t - 1] != 0) /\ (m_obj_loc[obj, t] != m_obj_loc[obj, t - 1])) then
                m_obj_loc[obj, t - 1]
            else
                prev_m_obj_loc[obj, t - 1]
            endif
    );

array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_m_obj_useful; % Был ли объект задействован в "полезной" операции (не движении в качестве главного объекта).

int : obj_useful_operations_max_size;
array [1..n_moving_obj] of 0..obj_useful_operations_max_size : obj_useful_operations_sizes;
array [1..n_moving_obj, 1..obj_useful_operations_max_size] of 1..n_operations : obj_useful_operations; % Все полезные операции касающиеся данного объекта.

    constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) (
        is_m_obj_useful[obj, t] = exists (useful_op_no in 1..obj_useful_operations_sizes[obj])
                                         (op_status[obj_useful_operations[obj, useful_op_no], t])
    );

array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_m_obj_in_movement; % Находится ли объект в движении в течении интервала.
    constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) (
        is_m_obj_in_movement[obj, t] = exists (moving_op_no in 1..moving_op_of_obj_sizes[obj]) (op_status[moving_op_of_obj[obj, moving_op_no], t])
    );

array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_interval_useful; % Была ли на текущем интервале полезная операция.
    % Ось времени нарежим по моментам начал свершившихся операций перемещения соответствующего движущегося объекта. Речь идёт о интервале который включает в себя данный атомарный промежуток времени.
    % !!! Важен только самый правый элемент интервала!!! (Значения на времени покрывающимся операцией движения могут быть 0 если они не с правого края интервала.)
    % И в фиктивном нуле false.

    constraint forall (obj in 1..n_moving_obj) (is_interval_useful[obj, 0] = false);

    constraint forall (obj in 1..n_moving_obj, t in 1..(n_intervals + 1)) (
        is_interval_useful[obj, t] =
            if (is_m_obj_in_movement[obj, t]) then
                is_m_obj_useful[obj, t]
            else
                is_m_obj_useful[obj, t] \/ is_interval_useful[obj, t - 1]
            endif
    );

constraint forall (obj in 1..n_moving_obj, t in 1..n_intervals) ( % Само ограничение.
    ((prev_m_obj_loc[obj, t]     != 0)                 /\
     (next_m_obj_loc[obj, t + 1] != m_obj_loc[obj, t]) /\
     (next_m_obj_loc[obj, t + 1] == prev_m_obj_loc[obj, t])
    ) -> is_interval_useful[obj, t - 1]
);
*/
solve minimize sum(is_not_terminated);

output [show(sum(is_not_terminated)), "\n",
        "op_status = ", 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",
        "is_not_terminated = ", show(is_not_terminated), "\n\n",
        "storage_used_volume = ", show(storage_used_volume), "\n\n",
        "is_m_obj_in_movement_before_start = ", show(is_m_obj_in_movement_before_start), "\n\n",
        "current_moving_operation = ", show(current_moving_operation), "\n\n"
%        "prev_m_obj_loc = ", show(prev_m_obj_loc), "\n\n",
%        "next_m_obj_loc = ", show(next_m_obj_loc), "\n\n",
%        "is_interval_useful = ", show(is_interval_useful), "\n\n"
        ];