diff --git a/constraints/conversion_0.mzn b/constraints/conversion_0.mzn index 65c4a6ef1d02eec1e2521cf388bf5caa1b2eb003..2ac921959fb3d21ea81f3d53f49531390cb531b2 100644 --- a/constraints/conversion_0.mzn +++ b/constraints/conversion_0.mzn @@ -12,15 +12,24 @@ 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; +int : arrival_op_max_size; +array [1..n_moving_obj, 1..n_locations, 1..arrival_op_max_size] of 1..n_operations : arrival_op; +array [1..n_moving_obj, 1..n_locations] of 0..arrival_op_max_size : arrival_op_sizes; + +int : departure_op_max_size; +array [1..n_moving_obj, 1..n_locations, 1..departure_op_max_size] of 1..n_operations : departure_op; +array [1..n_moving_obj, 1..n_locations] of 0..departure_op_max_size : departure_op_sizes; % Определение 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]]) (not op_status[k, j - 1]))) + (m_obj_loc[obj, j] == m_obj_loc[obj, j - 1] /\ + (forall (k in 1..departure_op_sizes[obj, m_obj_loc[obj, j]]) + (not op_status[departure_op[obj, m_obj_loc[obj, j], k], j - 1])) + ) \/ - (exists (k in arrival_op[obj, m_obj_loc[obj, j]]) (op_fin[k, j - 1])) + (exists (k in 1..arrival_op_sizes[obj, m_obj_loc[obj, j]]) + (op_fin[arrival_op[obj, m_obj_loc[obj, j], k], j - 1])) )); % Начальное состояние. @@ -173,18 +182,11 @@ array [1..n_moving_obj, 0..(n_intervals + 1)] of var 0..n_locations : prev_m_obj endif ); -int : n_useful_op; -array [1..n_useful_op] of 1..n_moving_obj : useful_op_obj; -array [1..n_useful_op] of 1..n_operations : useful_op_id; - array [1..n_moving_obj] of set of 1..n_operations : obj_useful_operations; % Все полезные операции касающиеся данного объекта. array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_m_obj_useful; % Был ли объект задействован в "полезной" операции (не движении в качестве главного объекта). - constraint forall (i in 1..n_useful_op, t in 0..(n_intervals + 1)) ( - op_status[useful_op_id[i], t] -> is_m_obj_useful[useful_op_obj[i], t] - ); - constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) ( % Недопущение "ложного срабатывания" is_m_obj_useful. - is_m_obj_useful[obj, t] -> exists (useful_op in obj_useful_operations[obj]) (op_status[useful_op, t]) + constraint forall (obj in 1..n_moving_obj, t in 0..(n_intervals + 1)) ( + is_m_obj_useful[obj, t] = exists (useful_op in obj_useful_operations[obj]) (op_status[useful_op, t]) ); array [1..n_moving_obj, 0..(n_intervals + 1)] of var bool : is_obj_in_moving; diff --git a/src/inport/ConversionUtil.java b/src/inport/ConversionUtil.java index fd57e5e534d89be71703dced1ffbf94944571ff1..da0bc8ca72750d19bda5ba6c0098ec977cf0a1d2 100644 --- a/src/inport/ConversionUtil.java +++ b/src/inport/ConversionUtil.java @@ -48,6 +48,45 @@ public class ConversionUtil { ); } + static private void write2DArrayOfSetAs3DArray(FileWriter writer, + String name, + ArrayList>> operations) throws IOException { + int maxSize = 0; + ArrayList> sizes = new ArrayList<>(); + + int dim1 = operations.size(); + int dim2 = 0; + + for (ArrayList> a1 : operations) { + dim2 = a1.size(); + ArrayList locSizes = new ArrayList<>(); + for (ArrayList a2 : a1) { + maxSize = Math.max(maxSize, a2.size()); + locSizes.add(a2.size()); + } + sizes.add(locSizes); + } + writer.write(name + "_max_size = " + maxSize + ";\n"); + write2DArrayOfInt(writer, name + "_sizes", sizes); + + writer.write(name + " = array3d(1.." + dim1 + ", 1.." + dim2 + ", 1.." + name + "_max_size, ["); + + boolean isFirst = true; + for (ArrayList> a1 : operations) { + for (ArrayList a2 : a1) { + for (int i = 0; i < maxSize; i++) { + if (isFirst) { + isFirst = false; + } else { + writer.write(", "); + } + writer.write(Integer.toString(i < a2.size() ? a2.get(i) : 1)); + } + } + } + writer.write("]);\n"); + } + static private void locWrite2DArray(FileWriter writer, String name, ArrayList> operations, @@ -261,8 +300,9 @@ public class ConversionUtil { } } } - write2DArrayOfSet(writer, "arrival_op", arrivalOp); - write2DArrayOfSet(writer, "departure_op", departureOp); + write2DArrayOfSetAs3DArray(writer, "arrival_op", arrivalOp); + write2DArrayOfSetAs3DArray(writer, "departure_op", departureOp); + writer.write("\n"); } { // Начальные положения объектов. ArrayList initialStates = integerArray(movingObjects.size(), 0); @@ -520,18 +560,12 @@ public class ConversionUtil { writer.write("\n"); } { // Ограничение на необходимость полезной операции между движениями к одному пункту назначения. - ArrayList usefulOpObj = new ArrayList<>(); - ArrayList usefulOpId = new ArrayList<>(); - ArrayList> objUsefulOperations = new ArrayList<>(); ArrayList> movingOpOfObj = new ArrayList<>(); - BiConsumer addUsOp = (MovingObject obj, Integer op) -> { - usefulOpObj.add(mObjToN.apply(obj)); - usefulOpId.add(op); + BiConsumer addUsOp = (MovingObject obj, Integer op) -> objUsefulOperations.get(mObjToN.apply(obj)).add(op + 1); - }; for (int i = 0; i < movingObjects.size(); i++) { movingOpOfObj.add(new TreeSet<>()); @@ -568,10 +602,6 @@ public class ConversionUtil { } } - writer.write("n_useful_op = " + usefulOpObj.size() + ";\n"); - writeArray(writer, "useful_op_obj", usefulOpObj, (Integer i) -> i + 1); - writeArray(writer, "useful_op_id", usefulOpId, (Integer i) -> i + 1); - writeArray(writer, "obj_useful_operations", objUsefulOperations, ConversionUtil::setToString); writeArray(writer, "moving_op_of_obj", movingOpOfObj, ConversionUtil::setToString); writer.write("\n");