对 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

Confused by the `m..n` notation in MiniZinc