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