MiniZinc中的'm..n`符號混淆

Question

我在不同的地方看到了「dot-dot」符號（..）。在以下示例中，0..n告訴我們決策變量的域（在這種情況下，是數組s的條目）。

int: n; 
array[0..n-1] of var 0..n: s; 

另一個例子是在for循環：

constraint forall(i in 0..sequence_length)(
    t[i] = sum(k in 0..sequence_length)((bool2int(t[k] == i))) 
); 

事實上，我們甚至可以這樣做

par var 1..5: x 

我的感覺是表達m..n一般使用當我們定義一個變量（而不是一個參數）時，我們想要指定變量的域。但在第二種情況下，我們沒有定義任何變量。那麼我們什麼時候使用m..n？它究竟是什麼（例如它是否有類型？）？

Answer 1

m..n表示設定的（連續的）整數從m到n。它也可以明確寫成{m,m+1,m+2,...,n-1,n}。

使用一組作爲域，例如

var 0..5: x; 

可以寫成

var {0,1,2,3,4,5}: x; 

或（這可能是一個奇怪的風格）：

var {1,5,2,3,0,4}: x; 

但都代表了一組0..5。

當在forall(i in m..n) (....)循環使用m..n這意味着i分配從m到n。

一組總是被排序爲這個小模型顯示：

solve satisfy; 
constraint 
    forall(i in {0,4,3,1,2,5}) (
     trace("i: \(i)\n") 
    ) 
; 

的trace函數打印以下，即有序：

i: 0 i: 1 i: 2 i: 3 i: 4 i: 5