MiniZinc: type error: expected `array[int] of int', actual `array[int] of var opt int

Question

I am trying to write a predicate that performs the same operation as circuit, but ignores zeros in the array, and I keep getting the following error:

MiniZinc: type error: initialisation value for 'x_without_0' has invalid type-inst: expected 'array[int] of int', actual 'array[int] of var opt int'

in the code:

% [0,5,2,0,7,0,3,0] -> true
% [0,5,2,0,4,0,3,0] -> false (no circuit)
% [0,5,2,0,3,0,8,7] -> false (two circuits)
predicate circuit_ignoring_0(array[int] of var int: x) =
  let { 
        array[int] of int: x_without_0 = [x[i] | i in 1..length(x) where x[i] != 0],
        int: lbx = min(x_without_0),
        int: ubx = max(x_without_0),
        int: len = length(x_without_0),
        array[1..len] of var lbx..ubx: order
  } in
  alldifferent(x_without_0) /\
  alldifferent(order) /\

  order[1] = x_without_0[1] /\ 
  forall(i in 2..len) (
     order[i] = x_without_0[order[i-1]]
  )
  /\  % last value is the minimum (symmetry breaking)
  order[ubx] = lbx
;

I am using MiniZinc v2.0.11

Edit

Per Kobbe's suggestion that it was an issue with having a variable length array, I used "the usual workaround" of keeping the order array the same size as the original array x, and using a parameter, nnonzeros, to keep track of the part of the array I care about:

set of int: S = index_set(x),
int: u = max(S),
var int: nnonzeros = among(x, S),
array[S] of var 0..u: order

Answer 1

This kind of answers your question:

The problem you are experiencing is that your array size is dependent on a var. This means that MiniZinc can not really know the size of the array is should create and the opt type is used. I would suggest that you stay away from the opt type if you do not know how to handle it.

Generally the solution is to make some workaround where your arrays are not dependent of the size of an var. My solution is most often to pad the array, i.e [2,0,5,0,8] -> [2,2,5,5,8], if the application allows it, or

var int : a;
[i * bool2int(i == a) in 1..5]

if you are okay with zeroes in your answer (I guess not in this case).

Furthermore, the alldifferent_except_0 could be in interest for you, or at least you can look how alldifferent_except_0 solves the problem with zeroes in the answer.

predicate alldifferent_except_0(array [int] of var int: vs) =
forall ( i, j in index_set(vs) where i < j ) ( 
    vs[i]!=0 /\ vs[j]!=0 -> vs[i]!=vs[j] 
)

from MiniZinc documentation