Closed
Description
On the command line:
$ minizinc --version
MiniZinc to FlatZinc converter, version 2.5.6
Copyright (C) 2014-2021 Monash University, NICTA, Data61
% minizinc Crash.mzn
maxt = 661
Task 1: cook = BOB start = 0 duration = 17 end (LQA) = 16 comes before task 2
Task 2: cook = BOB start = 0 duration = 0 end (LQA) = -1 comes before tasks 3,4
Task 3: cook = BOB start = 0 duration = 0 end (LQA) = -1
Task 4: cook = BOB start = 0 duration = 30 end (LQA) = 29 comes before task 5
Task 5: cook = BOB start = 0 duration = 0 end (LQA) = -1 comes before task 6
Task 6: cook = BOB start = 0 duration = 0 end (LQA) = -1
Task 7: cook = BOB start = 0 duration = 56 end (LQA) = 55 comes before task 8
Task 8: cook = BOB start = 0 duration = 0 end (LQA) = -1 comes before task 9
Task 9: cook = BOB start = 0 duration = 0 end (LQA) = -1
----------
MiniZinc error: Memory violation detected (segmentation fault).
This is a bug. Please file a bug report using the MiniZinc bug tracker.
The code what does is the following (skeleton of the Coursera course, Workshop 10, with additional output magic that I tried to make work).
The error occurs if I try to "fix" the later_relation/2 in fix(later_relation(task,later_task)). The idea is to print a "later" relationship between tasks where several tasks have to be performed to make a single dish. This worked, but I'm now trying to make this readable by moving the later_relation/2 out into a predicate instead of having it inline in the definition of later_tasks, which is much too unreadable (MiniZinc syntax forces you to scan to the end of an array definition to find the iteration variable. Traditional syntax for mathematics paperwork since probably Hilbert, but much less appealing in code, but I digress...)
% tasks' durations on different machines are NOT the same
% all jobs have the same number of tasks
% Average number of machines per task 2.00
COOK = { BOB, CAROL, TED, ALICE };
DISH = { MAPOTOFU, FRIEDEEL, STICKYRICE };
no_tasks = 9;
% steps = [1..3, 4..6, 7..9];
steps = [1..3, {2,4,5,6}, 7..9];
time = [| 17, 25, 0, 0
| 0, 30, 0, 40
| 0, 0,160,150
| 30, 0, 50, 0
| 0, 66, 0, 55
| 0, 0, 65, 78
| 56, 62, 0, 0
| 0, 70, 80, 0
| 0, 0,100, 90 |];
% ---
% Preparing a banquet in the least time
% ---
enum COOK; % the set of cooks available
enum DISH; % the set of all dishes to prepare
int: no_tasks; % total number of tasks
set of int: TASK = 1..no_tasks;
array[DISH] of set of TASK: steps; % steps to making a dish
array[TASK, COOK] of int: time; % amount of time to complete task by cook
% int: maxt_old = sum(array1d(time));
int: maxt = sum( [ max([time[task,cook] | cook in COOK]) | task in TASK ] );
set of int: TIME = 0..maxt;
array[TASK] of var TIME: s; % start time for task
array[TASK] of var COOK: c; % cook for task
var TIME: obj;
% output [ "maxt_old = \(maxt_old)\n" ]; % course given
output [ "maxt = \(maxt)\n" ]; % much more restricted
% ---
% Output magic
% ---
function string: task_set_to_string(set of TASK: s) =
if (card(s) = 0) then "" else join(",",[ show(task) | task in s ]) endif;
int: cook_max_strlen = max([ string_length(show(cook)) | cook in COOK ]);
function string: task_set_to_output(set of TASK: s) =
if (card(s) = 0) then ""
elseif (card(s) = 1) then " comes before task " ++ task_set_to_string(s)
else " comes before tasks " ++ task_set_to_string(s)
endif;
array[TASK] of set of TASK: later_tasks =
[ { later_task | later_task in TASK where fix(later_relation(task,later_task)) } | task in TASK ];
% -------------------------------------------^^^
predicate later_relation(TASK: task, TASK: later_task) =
task < later_task
/\
(
exists([
{ task, later_task } subset steps[dish]
/\
not
exists( [ { task, in_between_task, later_task } subset steps[dish]
/\
task < in_between_task /\ in_between_task < later_task
| in_between_task in TASK ] )
| dish in DISH])
);
output fix([ "Task " ++ show_int(2,task) ++ ":" ++
" cook = " ++ format_justify_string(cook_max_strlen,show(c[task])) ++
" start = " ++ show_int(3,s[task]) ++
" duration = " ++ show_int(3,time[task,c[task]]) ++
" end (LQA) = " ++ show_int(3,s[task]+time[task,c[task]]-1) ++
task_set_to_output(later_tasks[task])
++ "\n" | task in TASK ]);