Circular or missing definition of is_defined_var in FlatZinc

[kletzi]

Using optimization level O1 can lead to defined vars in the FlatZinc that have a circular definition or a missing definition in combination with array access:

array[1..2] of var 1..2: arr;
var 1..2: index;
constraint arr[index] = arr[2];
constraint index == arr[2];

solve satisfy;

leads to the following fzn:

var 1..2: X_INTRODUCED_0_;
var 1..2: index:: output_var:: is_defined_var;
array [1..2] of var int: arr:: output_array([1..2]) = [X_INTRODUCED_0_,index];
constraint array_var_int_element(index,arr,index):: defines_var(index);
solve  satisfy;

The definition for index is:
[X_INTRODUCED_0_, index][index] == index
This works for index=1 and index=2, so it does not uniquely define index.

A similar scenario occurs without constraint index == arr[2].

If this constraint is replaced by constraint index == 2, then the fzn looks as follows:

var 1..2: X_INTRODUCED_0_;
var 1..2: X_INTRODUCED_1_:: is_defined_var;
array [1..2] of var int: arr:: output_array([1..2]) = [X_INTRODUCED_0_,X_INTRODUCED_1_];
solve  satisfy;

Now X_INTRODUCED_1_ is marked as is_defined_var, but there is no definition at all.

Note that all examples work with optimization level O0.

We originally encountered this issue for CVRP in the MiniZinc benchmarks with instance simple2.dzn.

[guidotack]

I've pushed a fix for the circular defines_var. I can't reproduce the problem with index == 2, could you post the exact model you used to produce the FlatZinc that contains a is_defined_var but no defines_var?

[kletzi]

Thank you for the fast fix. I got the second part of the issue with the following input:

array[1..2] of var 1..2: arr;
var 1..2: index;
constraint arr[index] = arr[2];
constraint index == 2;

solve satisfy;