2.8.0: Issue with parameters in FlatZinc arrays

[informarte]

Consider this problem:

include "member.mzn";

int: N = 3;

array [1..N] of var bool: x;

var bool: y;
constraint member(x, y);

constraint x = array1d(1..3, [true, false, false]);
constraint y = true;

solve satisfy;

output ["x = ", show(x), "\n", "y = ", show(y)];

MiniZinc 2.8.0 (using Gecode as backend) reports the following:

Error: undefined identifier for type bool X_INTRODUCED_0_ in line no. 5
Error: undefined identifier for type bool X_INTRODUCED_1_ in line no. 5
Error: undefined identifier for type bool X_INTRODUCED_2_ in line no. 5
Error: undefined identifier x in line no. 6
=====ERROR=====

Using Chuffed results in similar error messages.

The result of flattening looks ok to me:

predicate fzn_member_bool(array [int] of var bool: x,var bool: y);
bool: X_INTRODUCED_0_ = true;
bool: X_INTRODUCED_1_ = false;
bool: X_INTRODUCED_2_ = false;
array [1..3] of var bool: x:: output_array([1..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_];
constraint fzn_member_bool(x,true);
solve  satisfy;

MiniZinc 2.7.6 works fine on the above problem, but the FlatZinc output looks a bit different:

predicate fzn_member_bool(array [int] of var bool: x,var bool: y);
var bool: X_INTRODUCED_0_;
var bool: X_INTRODUCED_1_;
var bool: X_INTRODUCED_2_;
array [1..3] of var bool: x:: output_array([1..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_];
constraint fzn_member_bool(x,true);
constraint bool_eq(X_INTRODUCED_0_,true);
constraint bool_eq(X_INTRODUCED_1_,false);
constraint bool_eq(X_INTRODUCED_2_,false);
solve  satisfy;

[Dekker1]

The problem is that the FlatZinc in this case still contains

bool: X_INTRODUCED_0_ = true;
bool: X_INTRODUCED_1_ = false;
bool: X_INTRODUCED_2_ = false;

This is not allowed according to the spec (and probably ignored in the Gecode and Chuffed parsers). Normally this is correctly rewritten when finalising the FlatZinc, but something must be going wrong.

[Dekker1]

In bisect it looks like 63f220f is the commit that caused the issue. I will further investigate what happened

[cyderize]

The problem is that the FlatZinc in this case still contains

bool: X_INTRODUCED_0_ = true;
bool: X_INTRODUCED_1_ = false;
bool: X_INTRODUCED_2_ = false;

This is not allowed according to the spec (and probably ignored in the Gecode and Chuffed parsers). Normally this is correctly rewritten when finalising the FlatZinc, but something must be going wrong.

Is that not allowed in the spec? The example in the docs seems to have this exact thing in it

[Dekker1]

Yes, you are right. Looking at the grammar there is nothing preventing this. Maybe it is just an informal rule that we've generally held (that only par-arrays are put into FlatZinc) that those parsers have come to rely on.