被MiniZinc中的MiniZinc符号所迷惑

Question

我在不同的地方见过“点-点”符号(..)。在下面的示例中，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) ( .... )循环中使用forall(i in 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