New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Only the first iteration of a forall-constraint is applied if it contains a let-statement with a par array indexed by a var-array indexed by the forall's range. #166

Closed
einarjohan opened this Issue Jun 2, 2017 · 0 comments

Comments

Projects
None yet
1 participant
@einarjohan

einarjohan commented Jun 2, 2017

This is a somewhat convoluted corner-case issue that seems to have been introduced in MiniZinc v2.1.3:

If you have a forall-constraint with a let-statement, where the let statement accesses an array that is indexed by a nother var array that is itself indexed by the variable introduced by the forall-statement,
then only the first iteration of the forall gets applied.

Since that's a sentence that was rather confusing to write, I'll refer to the following example code, which attempts to make v_arr_1's elements equal v_arr_2's elements:

set of int: indices = 1..2;

% Just a pair of arrays that we'll use to
% demonstrate the symptom.
array[indices] of var indices: v_arr_1;
array[indices] of var indices: v_arr_2;

% This MUST be var to demonstrate the problem
array[indices] of var indices: dummy_indices;
% This can also be non-var, and still demonstrate the problem:
array[indices] of var indices: dummy = [1, 2];

var indices: index_var;

constraint forall(index in indices) (
  let {
    % We _must_ use the "index" from the forall-statement here to trigger the
    % problem, also foo must be declared before the other variables.
    var int: foo = dummy[dummy_indices[index]],
    var int: v_arr_1_value = v_arr_1[index],
    var int: v_arr_2_value = v_arr_2[index]
  } in (v_arr_1_value == v_arr_2_value)
);

% This is caught as an inconsistency
% constraint (v_arr_1[1] != v_arr_2[1]);
% This is NOT caught as an inconsistency, unless we skip assigning foo in
% the let statement above
constraint (v_arr_1[2] != v_arr_2[2]);

solve satisfy;

% The problematic FlatZinc result is as follows, note how the first index _is_ constrained
% to be the same value between the arrays, while the second (and indeed any further if we go to
% i.e. 1..3, is not:
% array [1..2] of var int: v_arr_1:: output_array([1..2]) = [X_INTRODUCED_2_,X_INTRODUCED_1_];
% array [1..2] of var int: v_arr_2:: output_array([1..2]) = [X_INTRODUCED_2_,X_INTRODUCED_3_];

MiniZinc up to and including version 2.1.2 errors out on this as an inconsistent model (complaining about the != constraint, while 2.1.3 and up seems to only apply the constraint in the forall to index 1, yielding the FlatZinc result showed in the above example.

Interestingly, if we move foo's declaration down to after both v_arr_1_value and v_arr_2_value, this issue no longer pops up.

Similarly, the array lookup must be indexed by var array indexed by the forall-variable, although the outer array can be either var or par.

guidotack added a commit that referenced this issue Jun 12, 2017

Fix un-trailing for let expressions, which could sometimes cause inco…
…rrect code to be emitted when lets are evaluated in nested loops. Fixes #166.

@guidotack guidotack closed this in da5509c Sep 22, 2017

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment