This segfaults - workshop 12 -

[dedmedved]

Whilst working back from worked example to solution, this code triggered an error

MiniZinc error: Memory violation detected (segmentation fault).
This is a bug. Please file a bug report using the MiniZinc bug tracker.
Process finished with non-zero exit code -1073740791.

`
% include "gecode.mzn";
% Warning the village
int: n = 10 ; % number of houses
set of int: HOUSE = 1..n;
array[HOUSE] of int: x = [0, 3, 4, 6, 2, 8, 4, 3, 1, 6];
array[HOUSE] of int: y = [7, 3, 6, 2, 0, 5, 2, 4, 1, 9] ;
int: limit = 40 ; % max time allowed

int: m = 3; % number of messengers
set of int: MESSENGER = 1..m;
array[MESSENGER] of var HOUSE: messenger = [7, 5, 10] ; % who are the messengers
% array[MESSENGER] of var HOUSE: messenger = [5, 7, 10] ; % who are the messengers
% constraint strictly_increasing(messenger) ;

% nodes
% 1..N are villagers
% n+1..n+m are end trip node
set of int: NODE = 1..n+m;
array[NODE] of var NODE: next = [11, 13, 6, 12, 9, 4, 3, 2, 8, 1, 5, 10, 7] ; % next node visited after this one
var 0..limit: endtime;
array[NODE] of var NODE: prev; % next node visited after this one
constraint inverse(prev,next);

include "all_different.mzn";
constraint all_different(next);
constraint all_different(messenger);
include "globals.mzn";

% % no self loops
% constraint forall( i in NODE) ( next[i] != i);
% % no simple loops in non-dummy nodes
% constraint forall( i in HOUSE) ( next[i] != prev[i]);
constraint forall( i in 1..m) ( next[n+i] in messenger);

constraint circuit(next);
solve satisfy;

% split houses into m sets so that i and next[i] are in the same set
array[NODE] of var NODE: circuit_set;
% constraint forall(i in MESSENGER) (has_element(messenger[i],circuit_set));
constraint forall( i in NODE where next[i] <= n) ( circuit_set[next[i]] = circuit_set[i]);
constraint forall( i in MESSENGER) ( circuit_set[next[n+i]] = messenger[i]);

array[MESSENGER] of var int: costs; % the cost of each trip

output("perl grapher.pl "++ concat([format(messenger[i])++" " | i in MESSENGER ]) ++ " && graph.jpg \n");
% output("perl grapher.pl "++ concat([format(prev[i])++" " | i in NODE ]) ++ " && graph.jpg \n");
% output("perl grapher.pl "++ concat([format(c_prev[i])++" " | i in NODE ]) ++ " && graph.jpg\n");
output("perl grapher.pl "++ concat([format( if next[i] <= n then next[i] else 0 endif )++" " | i in NODE ]) ++ " && graph.jpg \n");
output("perl grapher.pl "++ concat([format( if prev[i] <= n then prev[i] else 0 endif )++" " | i in NODE ]) ++ " && graph.jpg \n");

% output("perl grapher.pl "++ concat([format(c_next[i])++" " | i in NODE ]) ++ " && graph.jpg \n");

output("(next)\n");
output("(prev)\n");
% output( "(first) (second) (third) \n");
output ("(circuit_set) \n");
output ("(cnext) \n");

% constraint forall( i in MESSENGER, n in NODES ) ( output ( if circuit_set[i] = i );

% array[NODE] of var NODE: cnext = [ if next[i] > n then circuit_set[next[i]] else next[i] endif | i in NODE] ;
array[NODE] of var NODE: cprev = [ if prev[i] > n then i else prev[i] endif | i in NODE] ;
array[NODE] of var NODE: cnext = [ if next[i] > n then i else next[i] endif | i in NODE] ;
% array[NODE] of var NODE: cloop = [ if cnext[i] = i then cprev[i] else cnext[i] endif | i in NODE] ;
array[NODE] of var NODE: loopprev = [ if cnext[i] = i then circuit_set[i] else 0 endif | i in NODE] ;

output("perl grapher.pl "++ concat([format(cnext[i]) ++ " " | i in HOUSE ]) ++ " && graph.jpg \n");
output("perl grapher.pl "++ concat([format(cprev[i]) ++ " " | i in HOUSE ]) ++ " && graph.jpg \n");
% output("perl grapher.pl "++ concat([format(cloop[i]) ++ " " | i in HOUSE ]) ++ " && graph.jpg \n"

% output("perl grapher.pl "++ concat([format(loopprev[i]) ++ " " | i in HOUSE ]) ++ " && graph.jpg \n");

`

[dedmedved]

The line at fault can be fixed

array[NODE] of var int: loopprev = [ if cnext[i] == i then circuit_set[i] else 0 endif | i in NODE] ;

from

array[NODE] of var NODE: loopprev = [ if cnext[i] = i then circuit_set[i] else 0 endif | i in NODE] ;#

[cyderize]

The segfault has been fixed in develop and will be part of the next release. Thanks!

It should also be noted that in the (original) line

array[NODE] of var NODE: loopprev = [ if cnext[i] = i then circuit_set[i] else 0 endif | i in NODE] ;

The domain is var NODE which is 1..n+m so the 0 in the if-then-else will be out of range causing unsatisfiability, whereas declaring it as an unbounded var int will allow 0 here.