Rewriting of domains to constraints

This transform rewrites domains into constraints where necessary.

The MIR only allows domains in the type-insts of fresh variables without RHS definitions which do not contain structured types (or nested arrays).

For example, var 1..3: x, var set of 1..3, array [1..3] of var 1..3, array [1..3] of var set of 1..3.

Other type-inst domains, such as function parameter domains, function return type-inst domains, domains of par declarations, and domains of declarations with RHS definitions, are transformed into constraints which enforce the domains (or assertions if the declaration is par).

1..3: x;

Becomes:

int: x;
constraint assert(x in 1..3, "Value out of range");

Structured types and arrays need to check domains for each element:

tuple(1..2, 1..3): x;
array [int] of 1..3: y;

Becomes:

tuple(int, int): x;
constraint assert(x.1 in 1..2 /\ x.2 in 1..3, "Value out of range");
array [int] of int: y;
constraint forall (y_i in 1..3) (y_i in y);

The actual implementation also has to ensure that the semantics of when the domain gets evaluated remains consistent with what's expected, so some extra let expressions are often needed to prevent re-evaluation.

Since we also would like to present the user with a useful error/warning message, we also keep track of how to display the variable accessor (e.g. x.1.foo for tuple(record(1..3: foo)): x) and use the mzn_domain_constraint functions to perform the checks.

Unpacking of structured type declarations

Consider the declaration:

tuple(var 1..2, var 1..3): x;

Since the type-inst is for a tuple type, we must rewrite this to not have a domain.

However, since this has no RHS, we do not have to introduce constraints - instead we can unpack x into its constituent variables:

tuple(var int, var int): x = let {
  var 1..2: a;
  var 1..3: b;
} in (a, b);

In the case of an array of structured types, a comprehension can be used. For example:

array [1..3] of tuple(var 1..2, var 1..3): x;

Can be transformed into:

array [1..3] of tuple(var int, var int): x = [
  let {
    var 1..2: a;
    var 1..2: b;
  } in (a, b)
| _ in 1..3];

Index set checking

For arrays, each declared index set needs to be checked against the true index set of the array.

array [1..3, int] of int: x;

Becomes:

array [int, int] of int: x;
constraint assert(index_set_1of2(x) = 1..3, "Index set doesn't match");

Since we again need to produce a useful error message, we perform the index set checks using the mzn_check_index_set function, which can produce an error message mentioning which dimension has the incorrect index set.