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

Question

Я пытаюсь написать предикат, который выполняет ту же операцию, что и circuit, но игнорирует нули в массиве, и я получаю следующее сообщение об ошибке:

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'

в коде:

% [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 
; 

Я использую MiniZinc v2.0.11

Edit

предложение Per Kobbe, что это была проблема с наличием переменного массива длиной, я использовал "the usual workaround" по поддержанию order массива тот же размера, что и исходный массив x, и с помощью параметра, nnonzeros, чтобы следить часть массива я забочусь о:

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

Этот вид ответов на ваш вопрос:

проблема вы испытываете, что размер массива зависит от var. Это означает, что MiniZinc не может действительно знать, какой размер массива должен создать, и используется тип opt. Я бы посоветовал вам держаться подальше от типа opt, если вы не знаете, как с ним справиться.

Как правило, решение заключается в том, чтобы сделать некоторое обходное решение, когда ваши массивы не зависят от размера var. Мое решение чаще всего раздуть массив, т.е. [2,0,5,0,8] -> [2,2,5,5,8], если приложение позволяет, или

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

если вы все в порядке с нулями в вашем ответе (я думаю, не в этом случае).

alldifferent_except_0 может интересовать вас, или как минимум можете посмотреть, как alldifferent_except_0 решает проблему с нулями в ответе.

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] 
) 

из MiniZinc documentation