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

Question

I have seen the "dot-dot" notation (..) in different places. In the following example, 0..n tells us the domain of the decision variable (which in this case, are the entries of the array s).

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

Another example would be in the for-loop:

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

In fact, we can even do something like

par var 1..5: x

My feeling is that the expression m..n is generally used when we define a variable (instead of a parameter), and we want to specify the domain of the variable. But in the second case, we are not defining any variable. So when do we use m..n? What is it exactly (e.g. does it have a type?)?

Answer 1

m..n denotes the set of (consecutive) integers from m to n. It could also be written explicitly as {m,m+1,m+2,...,n-1,n}.

Using a set as the domain, e.g.

var 0..5: x;

could be written as

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

or (which is probably a weird style):

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

but both represents the set 0..5.

When using m..n in a forall(i in m..n) ( .... ) loop it means that i is assigned from m to n.

A set is always ordered as this little model shows:

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

The trace function prints the following, i.e. ordered:

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