# 2.9. FlatZinc and Flattening¶

Constraint solvers do not directly support MiniZinc models, rather in order to run a MiniZinc model, it is translated into a simple subset of MiniZinc called FlatZinc. FlatZinc reflects the fact that most constraint solvers only solve satisfaction problems of the form \(\bar{exists} c_1 \wedge \cdots \wedge c_m\) or optimization problems of the form \(\text{minimize } z \text{ subject to } c_1 \wedge \cdots \wedge c_m\), where \(c_i\) are primitive constraints and \(z\) is an integer or float expression in a restricted form.

The `minizinc` tool includes the MiniZinc *compiler*, which
takes a MiniZinc model and data files and creates
a flattened FlatZinc model which is equivalent to the MiniZinc model with
the given data, and that appears in the restricted form discussed above.
Normally the construction of a FlatZinc model which is sent to a solver is
hidden from the user but you can view the result of flattening a model
`model.mzn` with
its data `data.dzn` as follows:

```
minizinc -c model.mzn data.dzn
```

which creates a FlatZinc model called `model.fzn`.

In this chapter we explore the process of translation from MiniZinc to FlatZinc.

## 2.9.1. Flattening Expressions¶

The restrictions of the underlying solver mean that complex expressions in
MiniZinc need to be *flattened* to only use conjunctions of primitive
constraints which do not themselves contain structured terms.

Consider the following model for ensuring that two circles in a rectangular box do not overlap:

```
float: width; % width of rectangle to hold circles
float: height; % height of rectangle to hold circles
float: r1;
var r1..width-r1: x1; % (x1,y1) is center of circle of radius r1
var r1..height-r1: y1;
float: r2;
var r2..width-r2: x2; % (x2,y2) is center of circle of radius r2
var r2..height-r2: y2;
% centers are at least r1 + r2 apart
constraint (x1-x2)*(x1-x2) + (y1-y2)*(y1-y2) >= (r1+r2)*(r1+r2);
solve satisfy;
```

### 2.9.1.1. Simplification and Evaluation¶

Given the data file

```
width = 10.0;
height = 8.0;
r1 = 2.0;
r2 = 3.0;
```

the translation to FlatZinc first simplifies the model by replacing all the parameters by their values, and evaluating any fixed expression. After this simplification the values of parameters are not longer needed. An exception to this is large arrays of parametric values. If they are used more than once, then the parameter is retained to avoid duplicating the large expression.

After simplification the variable and parameter declarations parts of the model of Listing 2.9.1 become

```
var 2.0 .. 8.0: x1;
var 2.0 .. 6.0: y1;
var 3.0 .. 7.0: x2;
var 3.0 .. 5.0: y2;
```

### 2.9.1.2. Defining Subexpressions¶

Now no constraint solver directly handles complex constraint expressions
like the one in Listing 2.9.1.
Instead, each subexpression in the expression is named, and we create a
constraint to construct the value of each expression. Let’s examine the
subexpressions of the constraint expression. `(x1 - x2)`

is a
subexpression, if we name if `FLOAT01`

we can define it as
`constraint FLOAT01 = x1 - x2;`

Notice that this expression occurs
twice in the model. We only need to construct the value once, we can then
reuse it. This is called *common subexpression elimination*.
The subexpression `(x1 - x2)*(x1 - x2)`

can be named
`FLOAT02`

and we can define it as
`constraint FLOAT02 = FLOAT01 * FLOAT01;`

We can similarly name `constraint FLOAT03 = y1 - y2;`

and
`constraint FLOAT04 = FLOAT03 * FLOAT03;`

and finally `constraint FLOAT05 = FLOAT02 * FLOAT04;`

.
The inequality constraint itself becomes
`constraint FLOAT05 >= 25.0;`

since `(r1+r2)*(r1 + r2)`

is calculated as `25.0`

.
The flattened constraint is hence

```
constraint FLOAT01 = x1 - x2;
constraint FLOAT02 = FLOAT01 * FLOAT01;
constraint FLOAT03 = y1 - y2;
constraint FLOAT04 = FLOAT03 * FLOAT03;
constraint FLOAT05 = FLOAT02 * FLOAT04;
constraint FLOAT05 >= 25.0
```

### 2.9.1.3. FlatZinc constraint form¶

Flattening as its final step converts the form of the constraint to a
standard FlatZinc form which is always \(p(a_1, \ldots, a_n)\) where
`p`

is the name of the primitive constraint and \(a_1, \ldots, a_n\) are the
arguments. FlatZinc tries to use a minimum of different constraint forms so
for example the constraint `FLOAT01 = x1 - x2`

is first rewritten to
`FLOAT01 + x2 = x1`

and then output using the `float_plus`

primitive
constraint. The resulting constraint form is as follows:

```
constraint float_plus(FLOAT01, x2, x1);
constraint float_plus(FLOAT03, y2, y1);
constraint float_plus(FLOAT02, FLOAT04, FLOAT05);
constraint float_times(FLOAT01, FLOAT01, FLOAT02);
constraint float_times(FLOAT03, FLOAT03, FLOAT04);
```

### 2.9.1.4. Bounds analysis¶

We are still missing one thing, the
declarations for the introduced variables `FLOAT01`

, …,
`FLOAT05`

. While these could just be declared as
`var float`

, in order to make the solver’s task easier MiniZinc tries to
determine upper and lower bounds on newly introduced variables, by a simple
bounds analysis. For example since `FLOAT01 = x1 - x2`

and \(2.0 \leq\) `x1`

\(\leq 8.0\) and \(3.0 \leq\) `x2`

\(\leq 7.0\) then we can see that
\(-5.0 \leq\) `FLOAT0`

\(\leq 5.0\). Given this information we can see that
\(-25.0 \leq\) `FLOAT02`

\(\leq 25.0\) (although note that if we recognized that the
multiplication was in fact a squaring we could give the much more accurate
bounds \(0.0 \leq\) `FLOAT02`

\(\leq 25.0\)).

The alert reader may have noticed a discrepancy between the flattened form
of the constraints in Defining Subexpressions and FlatZinc constraint form. In
the latter there is no inequality constraint. Since unary inequalities can
be fully represented by the bounds of a variable, the inequality forces the
lower bound of `FLOAT05`

to be `25.0`

and is then redundant. The final
flattened form of the model of Listing 2.9.1 is:

```
% Variables
var 2.0 .. 8.0: x1;
var 2.0 .. 6.0: y1;
var 3.0 .. 7.0: x2;
var 3.0 .. 5.0: y2;
%
var -5.0..5.0: FLOAT01;
var -25.0..25.0: FLOAT02;
var -3.0..3.0: FLOAT03;
var -9.0..9.0: FLOAT04;
var 25.0..34.0: FLOAT05;
% Constraints
constraint float_plus(FLOAT01, x2, x1);
constraint float_plus(FLOAT03, y2, y1);
constraint float_plus(FLOAT02, FLOAT04, FLOAT05);
constraint float_times(FLOAT01, FLOAT01, FLOAT02);
constraint float_times(FLOAT03, FLOAT03, FLOAT04);
%
solve satisfy;
```

### 2.9.1.5. Objectives¶

MiniZinc flattens minimization or maximization objectives just like constraints. The objective expression is flattened and a variable is created for it, just as for other expressions. In the FlatZinc output the solve item is always on a single variable. See Let Expressions for an example.

## 2.9.2. Linear Expressions¶

One of the most important form of constraints, widely used for modelling, are linear constraints of the form

where \(a_i\) are integer or floating point constants, and \(x_i\) are integer or floating point variables. They are highly expressive, and are the only class of constraint supported by (integer) linear programming constraint solvers. The translator from MiniZinc to FlatZinc tries to create linear constraints, rather than break up linear constraints into many subexpressions.

```
int: d = -1;
var 0..10: x;
var -3..6: y;
var 3..8: z;
constraint 3*x - y + x * z <= 19 + d * (x + y + z) - 4*d;
solve satisfy;
```

Consider the model shown in Listing 2.9.2. Rather than create variables for all the subexpressions \(3*x\), \(3*x - y\), \(x * z\), \(3*x - y + x*z\), \(x + y + z\), \(d * (x + y + z)\), \(19 + d * (x + y + z)\), and \(19 + d * (x + y + z) - 4*d\) translation will attempt to create a large linear constraint which captures as much as possible of the constraint in a single FlatZinc constraint.

Flattening creates linear expressions as a single unit rather than building intermediate variables for each subexpression. It also simplifies the linear expression created. Extracting the linear expression from the constraints leads to

```
var 0..80: INT01;
constraint 4*x + z + INT01 <= 23;
constraint INT01 = x * z;
```

Notice how the *nonlinear expression* \(x \times z\) is extracted as a
new subexpression and given a name, while the remaining terms are collected
together so that each variable appears exactly once (and indeed variable \(y\)
whose terms cancel is eliminated).

Finally each constraint is written to FlatZinc form obtaining:

```
var 0..80: INT01;
constraint int_lin_le([1,4,1],[INT01,x,z],23);
constraint int_times(x,z,INT01);
```

## 2.9.3. Unrolling Expressions¶

Most models require creating a number of constraints which is dependent on the input data. MiniZinc supports these models with array types, list and set comprehensions, and aggregation functions.

Consider the following aggregate expression from the production scheduling example of Listing 2.2.2.

```
int: mproducts = max (p in Products)
(min (r in Resources where consumption[p,r] > 0)
(capacity[r] div consumption[p,r]));
```

Since this uses generator call syntax we can rewrite it to equivalent form which is processed by the compiler:

```
int: mproducts = max([ min [ capacity[r] div consumption[p,r]
| r in Resources where consumption[p,r] > 0])
| p in Products]);
```

Given the data

```
nproducts = 2;
nresources = 5;
capacity = [4000, 6, 2000, 500, 500];
consumption= [| 250, 2, 75, 100, 0,
| 200, 0, 150, 150, 75 |];
```

this first builds the array for `p = 1`

```
[ capacity[r] div consumption[p,r]
| r in 1..5 where consumption[p,r] > 0]
```

which is `[16, 3, 26, 5]`

and then calculates the minimum as 3.
It then builds the same array for `p = 2`

which is
`[20, 13, 3, 6]`

and calculates the minimum as 3. It then constructs the
array `[3, 3]`

and calculates the maximum as 3.
There is no representation of `mproducts`

in the output FlatZinc,
this evaluation is simply used to replace `mproducts`

by the
calculated value 3.

The most common form of aggregate expression in a constraint model is
`forall`

. Forall expressions are unrolled into multiple constraints.

Consider the MiniZinc fragment

```
array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
constraint forall(i,j in 1..8 where i < j)(v[i] != v[j])
```

which arises from the SEND-MORE-MONEY example of Listing 2.2.4
using a default decomposition for `alldifferent`

.
The `forall`

expression creates a constraint for each \(i, j\) pair which meet
the requirement \(i < j\), thus creating

```
constraint v[1] != v[2]; % S != E
constraint v[1] != v[3]; % S != N
...
constraint v[1] != v[8]; % S != Y
constraint v[2] != v[3]; % E != N
...
constraint v[7] != v[8]; % R != Y
```

In FlatZinc form this is

```
constraint int_neq(S,E);
constraint int_neq(S,N);
...
constraint int_neq(S,Y);
constraint int_neq(E,N);
...
constraint int_neq(R,Y);
```

Notice how the temporary array variables `v[i]`

are replaced by the
original variables in the output FlatZinc.

## 2.9.4. Arrays¶

One dimensional arrays
in MiniZinc can have arbitrary indices as long as they are
contiguous integers. In FlatZinc all arrays are indexed from `1..l`

where `l`

is the length of the array. This means that array lookups need to
be translated to the FlatZinc view of indices.

Consider the following MiniZinc model for balancing a seesaw
of length `2 * l2`

,
with a child of weight `cw`

kg using exactly `m`

1kg weights.

```
int: cw; % child weight
int: l2; % half seesaw length
int: m; % number of 1kg weight
array[-l2..l2] of var 0..max(m,cw): w; % weight at each point
var -l2..l2: p; % position of child
constraint sum(i in -l2..l2)(i * w[i]) = 0; % balance
constraint sum(i in -l2..l2)(w[i]) = m + cw; % all weights used
constraint w[p] = cw; % child is at position p
solve satisfy;
```

Given `cw = 2`

, `l2 = 2`

, and `m = 3`

the unrolling produces the constraints

```
array[-2..2] of var 0..3: w;
var -2..2: p
constraint -2*w[-2] + -1*w[-1] + 0*w[0] + 1*w[1] + 2*w[2] = 0;
constraint w[-2] + w[-1] + w[0] + w[1] + w[2] = 5;
constraint w[p] = 2;
```

But FlatZinc insists that the `w`

array starts at index 1.
This means we need to rewrite all the array accesses to use the new index
value. For fixed array lookups this is easy, for variable array lookups we
may need to create a new variable. The result for the equations above is

```
array[1..5] of var 0..3: w;
var -2..2: p
var 1..5: INT01;
constraint -2*w[1] + -1*w[2] + 0*w[3] + 1*w[4] + 2*w[5] = 0;
constraint w[1] + w[2] + w[3] + w[4] + w[5] = 5;
constraint w[INT01] = 2;
constraint INT01 = p + 3;
```

Finally we rewrite the constraints into FlatZinc form. Note how the variable
array index lookup is mapped to `array_var_int_element`

.

```
array[1..5] of var 0..3: w;
var -2..2: p
var 1..5: INT01;
constraint int_lin_eq([2, 1, -1, -2], [w[1], w[2], w[4], w[5]], 0);
constraint int_lin_eq([1, 1, 1, 1, 1], [w[1],w[2],w[3],w[4],w[5]], 5);
constraint array_var_int_element(INT01, w, 2);
constraint int_lin_eq([-1, 1], [INT01, p], -3);
```

Multidimensional arrays are supported by MiniZinc, but only single dimension arrays are supported by FlatZinc (at present). This means that multidimensional arrays must be mapped to single dimension arrays, and multidimensional array access must be mapped to single dimension array access.

Consider the Laplace equation constraints defined for a finite element plate model in Listing 2.2.1:

```
set of int: HEIGHT = 0..h;
set of int: CHEIGHT = 1..h-1;
set of int: WIDTH = 0..w;
set of int: CWIDTH = 1..w-1;
array[HEIGHT,WIDTH] of var float: t; % temperature at point (i,j)
var float: left; % left edge temperature
var float: right; % right edge temperature
var float: top; % top edge temperature
var float: bottom; % bottom edge temperature
% equation
% Laplace equation: each internal temp. is average of its neighbours
constraint forall(i in CHEIGHT, j in CWIDTH)(
4.0*t[i,j] = t[i-1,j] + t[i,j-1] + t[i+1,j] + t[i,j+1]);
```

Assuming `w = 4`

and `h = 4`

this creates the constraints

```
array[0..4,0..4] of var float: t; % temperature at point (i,j)
constraint 4.0*t[1,1] = t[0,1] + t[1,0] + t[2,1] + t[1,2];
constraint 4.0*t[1,2] = t[0,2] + t[1,1] + t[2,2] + t[1,3];
constraint 4.0*t[1,3] = t[0,3] + t[1,2] + t[2,3] + t[1,4];
constraint 4.0*t[2,1] = t[1,1] + t[2,0] + t[3,1] + t[2,2];
constraint 4.0*t[2,2] = t[1,2] + t[2,1] + t[3,2] + t[2,3];
constraint 4.0*t[2,3] = t[1,3] + t[2,2] + t[3,3] + t[2,4];
constraint 4.0*t[3,1] = t[2,1] + t[3,0] + t[4,1] + t[3,2];
constraint 4.0*t[3,2] = t[2,2] + t[3,1] + t[4,2] + t[3,3];
constraint 4.0*t[3,3] = t[2,3] + t[3,2] + t[4,3] + t[3,4];
```

The 2 dimensional array of 25 elements is converted to a one dimensional
array and the indices are changed accordingly: so index `[i,j]`

becomes
`[i * 5 + j + 1]`

.

```
array [1..25] of var float: t;
constraint 4.0*t[7] = t[2] + t[6] + t[12] + t[8];
constraint 4.0*t[8] = t[3] + t[7] + t[13] + t[9];
constraint 4.0*t[9] = t[4] + t[8] + t[14] + t[10];
constraint 4.0*t[12] = t[7] + t[11] + t[17] + t[13];
constraint 4.0*t[13] = t[8] + t[12] + t[18] + t[14];
constraint 4.0*t[14] = t[9] + t[13] + t[19] + t[15];
constraint 4.0*t[17] = t[12] + t[16] + t[22] + t[18];
constraint 4.0*t[18] = t[13] + t[17] + t[23] + t[19];
constraint 4.0*t[19] = t[14] + t[18] + t[24] + t[20];
```

## 2.9.5. Reification¶

FlatZinc models involve only variables and parameter declarations
and a series of primitive constraints. Hence when we model in MiniZinc
with Boolean connectives other than conjunction, something has to be done.
The core approach to handling complex formulae that use
connectives other than conjunction is by
*reification*.
Reifying a constraint \(c\) creates a new constraint equivalent to \(b \leftrightarrow c\)
where the Boolean variable \(b\) is `true`

if the constraint holds and `false`

if it doesn’t hold.

Once we have the capability to *reify* constraints the treatment of
complex formulae is not different from arithmetic expressions. We create a
name for each subexpression and a flat constraint to constrain the name to
take the value of its subexpression.

Consider the following constraint expression that occurs in the jobshop scheduling example of Listing 2.2.10.

```
constraint %% ensure no overlap of tasks
forall(j in 1..tasks) (
forall(i,k in 1..jobs where i < k) (
s[i,j] + d[i,j] <= s[k,j] \/
s[k,j] + d[k,j] <= s[i,j]
) );
```

Given the data file

```
jobs = 2;
tasks = 3;
d = [| 5, 3, 4 | 2, 6, 3 |]
```

then the unrolling creates

```
constraint s[1,1] + 5 <= s[2,1] \/ s[2,1] + 2 <= s[1,1];
constraint s[1,2] + 3 <= s[2,2] \/ s[2,2] + 6 <= s[1,2];
constraint s[1,3] + 4 <= s[2,3] \/ s[2,3] + 3 <= s[1,3];
```

Reification of the constraints that appear in the disjunction creates new Boolean variables to define the values of each expression.

```
array[1..2,1..3] of var 0..23: s;
constraint BOOL01 <-> s[1,1] + 5 <= s[2,1];
constraint BOOL02 <-> s[2,1] + 2 <= s[1,1];
constraint BOOL03 <-> s[1,2] + 3 <= s[2,2];
constraint BOOL04 <-> s[2,2] + 6 <= s[1,2];
constraint BOOL05 <-> s[1,3] + 4 <= s[2,3];
constraint BOOL06 <-> s[2,3] + 3 <= s[1,3];
constraint BOOL01 \/ BOOL02;
constraint BOOL03 \/ BOOL04;
constraint BOOL05 \/ BOOL06;
```

Each primitive constraint can now be mapped to the FlatZinc form.
Note how the two dimensional array `s`

is mapped to a one dimensional form.

```
array[1..6] of var 0..23: s;
constraint int_lin_le_reif([1, -1], [s[1], s[4]], -5, BOOL01);
constraint int_lin_le_reif([-1, 1], [s[1], s[4]], -2, BOOL02);
constraint int_lin_le_reif([1, -1], [s[2], s[5]], -3, BOOL03);
constraint int_lin_le_reif([-1, 1], [s[2], s[5]], -6, BOOL04);
constraint int_lin_le_reif([1, -1], [s[3], s[6]], -4, BOOL05);
constraint int_lin_le_reif([-1, 1], [s[3], s[6]], -3, BOOL06);
constraint bool_clause([BOOL01, BOOL02], []);
constraint bool_clause([BOOL03, BOOL04], []);
constraint bool_clause([BOOL05, BOOL06], []);
```

The `int_lin_le_reif`

is the reified form of the linear constraint
`int_lin_le`

.

Most FlatZinc primitive constraints \(p(\bar{x})\) have a reified form
\(\mathit{p\_reif}(\bar{x},b)\) which takes an additional final argument \(b\)
and defines the constraint \(b \leftrightarrow p(\bar{x})\).
FlatZinc primitive constraints which define functional relationships,
like `int_plus`

and `int_plus`

, do
not need to support reification. Instead, the equality with the result of the function is reified.

Another important use of reification arises when we use the coercion
function `bool2int`

(either explicitly, or implicitly by using a Boolean
expression as an integer expression). Flattening creates a Boolean
variable to hold the value of the Boolean expression argument, as well as an
integer variable (restricted to `0..1`

) to hold this value.

Consider the magic series problem of Listing 2.2.14.

```
int: n;
array[0..n-1] of var 0..n: s;
constraint forall(i in 0..n-1) (
s[i] = (sum(j in 0..n-1)(bool2int(s[j]=i))));
```

Given `n = 2`

the unrolling creates

```
constraint s[0] = bool2int(s[0] = 0) + bool2int(s[1] = 0);
constraint s[1] = bool2int(s[0] = 1) + bool2int(s[1] = 1);
```

and flattening creates

```
constraint BOOL01 <-> s[0] = 0;
constraint BOOL03 <-> s[1] = 0;
constraint BOOL05 <-> s[0] = 1;
constraint BOOL07 <-> s[1] = 1;
constraint INT02 = bool2int(BOOL01);
constraint INT04 = bool2int(BOOL03);
constraint INT06 = bool2int(BOOL05);
constraint INT08 = bool2int(BOOL07);
constraint s[0] = INT02 + INT04;
constraint s[1] = INT06 + INT08;
```

The final FlatZinc form is

```
var bool: BOOL01;
var bool: BOOL03;
var bool: BOOL05;
var bool: BOOL07;
var 0..1: INT02;
var 0..1: INT04;
var 0..1: INT06;
var 0..1: INT08;
array [1..2] of var 0..2: s;
constraint int_eq_reif(s[1], 0, BOOL01);
constraint int_eq_reif(s[2], 0, BOOL03);
constraint int_eq_reif(s[1], 1, BOOL05);
constraint int_eq_reif(s[2], 1, BOOL07);
constraint bool2int(BOOL01, INT02);
constraint bool2int(BOOL03, INT04);
constraint bool2int(BOOL05, INT06);
constraint bool2int(BOOL07, INT08);
constraint int_lin_eq([-1, -1, 1], [INT02, INT04, s[1]], 0);
constraint int_lin_eq([-1, -1, 1], [INT06, INT08, s[2]], 0);
solve satisfy;
```

## 2.9.6. Predicates¶

An important factor in the support for MiniZinc by many different solvers is that global constraints (and indeed FlatZinc constraints) can be specialized for the particular solver.

Each solver will either specify a predicate without a definition, or with a
definition. For example a solver that has a builtin global `alldifferent`

predicate, will include the definition

```
predicate alldifferent(array[int] of var int:x);
```

in its globals library, while a solver using the default decomposition will have the definition

```
predicate alldifferent(array[int] of var int:x) =
forall(i,j in index_set(x) where i < j)(x[i] != x[j]);
```

Predicate calls \(p(\bar{t})\) are flattened by first constructing variables \(v_i\) for each argument terms \(t_i\). If the predicate has no definition we simply use a call to the predicate with the constructed arguments: \(p(\bar{v})\). If the predicate has a definition \(p(\bar{x}) = \phi(\bar{x})\) then we replace the predicate call \(p(\bar{t})\) with the body of the predicate with the formal arguments replaced by the argument variables, that is \(\phi(\bar{v})\). Note that if a predicate call \(p(\bar{t})\) appears in a reified position and it has no definition, we check for the existence of a reified version of the predicate \(\mathit{p\_reif}(\bar{x},b)\) in which case we use that.

Consider the `alldifferent`

constraint in the
SEND-MORE-MONEY example of Listing 2.2.4

```
constraint alldifferent([S,E,N,D,M,O,R,Y]);
```

If the solver has a builtin `alldifferent`

we simply construct a new variable
for the argument, and replace it in the call.

```
array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
constraint alldifferent(v);
```

Notice that bounds analysis attempts to find tight bounds on the new array
variable. The reason for constructing the array argument is if we use the
same array twice the FlatZinc solver does not have to construct it twice.
In this case since it is not used twice a later stage of the translation
will replace `v`

by its definition.

What if the solver uses the default definition of `alldifferent`

?
Then the variable `v`

is defined as usual, and the predicate call is
replaced by a renamed copy where `v`

replaces the formal argument `x`

.
The resulting code is

```
array[1..8] of var 0..9: v = [S,E,N,D,M,O,R,Y];
constraint forall(i,j in 1..8 where i < j)(v[i] != v[j])
```

which we examined in Unrolling Expressions.

Consider the following constraint, where `alldifferent`

appears in a reified
position.

```
constraint alldifferent([A,B,C]) \/ alldifferent([B,C,D]);
```

If the solver has a reified form of `alldifferent`

this will be flattened to

```
constraint alldifferent_reif([A,B,C],BOOL01);
constraint alldifferent_reif([B,C,D],BOOL02);
constraint bool_clause([BOOL01,BOOL02],[]);
```

Using the default decomposition, the predicate replacement will first create

```
array[1..3] of var int: v1 = [A,B,C];
array[1..3] of var int: v2 = [B,C,D];
constraint forall(i,j in 1..3 where i<j)(v1[i] != v1[j]) \/
forall(i,j in 1..3 where i<j)(v2[i] != v2[j]);
```

which will eventually be flattened to the FlatZinc form

```
constraint int_neq_reif(A,B,BOOL01);
constraint int_neq_reif(A,C,BOOL02);
constraint int_neq_reif(B,C,BOOL03);
constraint array_bool_and([BOOL01,BOOL02,BOOL03],BOOL04);
constraint int_neq_reif(B,D,BOOL05);
constraint int_neq_reif(C,D,BOOL06);
constraint array_bool_and([BOOL03,BOOL05,BOOL06],BOOL07);
constraint bool_clause([BOOL04,BOOL07],[]);
```

Note how common subexpression elimination reuses the
reified inequality `B != C`

(although there is a better translation which
lifts the common constraint to the top level conjunction).

## 2.9.7. Let Expressions¶

Let expressions are a powerful facility of MiniZinc to introduce new variables. This is useful for creating common sub expressions, and for defining local variables for predicates. During flattening let expressions are translated to variable and constraint declarations. The relational semantics of MiniZinc means that these constraints must appear as if conjoined in the first enclosing Boolean expression.

A key feature of let expressions is that each time they are used they create new variables.

Consider the flattening of the code

```
constraint even(u) \/ even(v);
predicate even(var int: x) =
let { var int: y } in x = 2 * y;
```

First the predicate calls are replaced by their definition.

```
constraint (let { var int: y} in u = 2 * y) \/
(let { var int: y} in v = 2 * y);
```

Next let variables are renamed apart

```
constraint (let { var int: y1} in u = 2 * y1) \/
(let { var int: y2} in v = 2 * y2);
```

Finally variable declarations are extracted to the top level

```
var int: y1;
var int: y2;
constraint u = 2 * y1 \/ v = 2 * y2;
```

Once the let expression is removed we can flatten as usual.

Remember that let expressions can define values for newly introduced variables (and indeed must do so for parameters). These implicitly define constraints that must also be flattened.

Consider the complex objective function for wedding seating problem of Listing 2.3.10.

```
solve maximize sum(h in Hatreds)(
let { var Seats: p1 = pos[h1[h]],
var Seats: p2 = pos[h2[h]],
var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));
```

For conciseness we assume only the first two Hatreds, so

```
set of int: Hatreds = 1..2;
array[Hatreds] of Guests: h1 = [groom, carol];
array[Hatreds] of Guests: h2 = [clara, bestman];
```

The first step of flattening is to unroll the `sum`

expression, giving
(we keep the guest names and parameter `Seats`

for clarity only, in
reality they would be replaced by their definition):

```
solve maximize
(let { var Seats: p1 = pos[groom],
var Seats: p2 = pos[clara],
var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1))
+
(let { var Seats: p1 = pos[carol],
var Seats: p2 = pos[bestman],
var 0..1: same = bool2int(p1 <= 6 <-> p2 <= 6) } in
same * abs(p1 - p2) + (1-same) * (abs(13 - p1 - p2) + 1));
```

Next each new variable in a let expression is renamed to be distinct

```
solve maximize
(let { var Seats: p11 = pos[groom],
var Seats: p21 = pos[clara],
var 0..1: same1 = bool2int(p11 <= 6 <-> p21 <= 6) } in
same1 * abs(p11 - p21) + (1-same1) * (abs(13 - p11 - p21) + 1))
+
(let { var Seats: p12 = pos[carol],
var Seats: p22 = pos[bestman],
var 0..1: same2 = bool2int(p12 <= 6 <-> p22 <= 6) } in
same2 * abs(p12 - p22) + (1-same2) * (abs(13 - p12 - p22) + 1));
```

Variables in the let expression are extracted to the top level and defining constraints are extracted to the correct level (which in this case is also the top level).

```
var Seats: p11;
var Seats: p21;
var 0..1: same1;
constraint p12 = pos[clara];
constraint p11 = pos[groom];
constraint same1 = bool2int(p11 <= 6 <-> p21 <= 6);
var Seats p12;
var Seats p22;
var 0..1: same2;
constraint p12 = pos[carol];
constraint p22 = pos[bestman];
constraint same2 = bool2int(p12 <= 6 <-> p22 <= 6) } in
solve maximize
same1 * abs(p11 - p21) + (1-same1) * (abs(13 - p11 - p21) + 1))
+
same2 * abs(p12 - p22) + (1-same2) * (abs(13 - p12 - p22) + 1));
```

Now we have constructed equivalent MiniZinc code without the use of let expressions and the flattening can proceed as usual.

As an illustration of let expressions that do not appear at the top level consider the following model

```
var 0..9: x;
constraint x >= 1 -> let { var 2..9: y = x - 1 } in
y + (let { var int: z = x * y } in z * z) < 14;
```

We extract the variable definitions to the top level and the constraints to the first enclosing Boolean context, which here is the right hand side of the implication.

```
var 0..9: x;
var 2..9: y;
var int: z;
constraint x >= 1 -> (y = x - 1 /\ z = x * y /\ y + z * z < 14);
```

Note that if we know that the equation defining a variable definition cannot fail we can extract it to the top level. This will usually make solving substantially faster.

For the example above the constraint `y = x - 1`

can fail since the domain
of `y`

is not big enough for all possible values of `x - 1`

. But the
constraint `z = x * y`

cannot (indeed bounds analysis will give `z`

bounds big enough to hold all possible values of `x * y`

).
A better flattening will give

```
var 0..9: x;
var 2..9: y;
var int: z;
constraint z = x * y;
constraint x >= 1 -> (y = x - 1 /\ y + z * z < 14);
```

Currently the MiniZinc compiler does this by always defining the declared bounds of an introduced variable to be big enough for its defining equation to always hold and then adding bounds constraints in the correct context for the let expression. On the example above this results in

```
var 0..9: x;
var -1..8: y;
var -9..72: z;
constraint y = x - 1;
constraint z = x * y;
constraint x >= 1 -> (y >= 2 /\ y + z * z < 14);
```

This translation leads to more efficient solving since the possibly complex calculation of the let variable is not reified.

Another reason for this approach is that it also works when introduced variables appear in negative contexts (as long as they have a definition). Consider the following example similar to the previous one

```
var 0..9: x;
constraint (let { var 2..9: y = x - 1 } in
y + (let { var int: z = x * y } in z * z) > 14) -> x >= 5;
```

The let expressions appear in a negated context, but each introduced variable is defined. The flattened code is

```
var 0..9: x;
var -1..8: y;
var -9..72: z;
constraint y = x - 1;
constraint z = x * y;
constraint (y >= 2 /\ y + z * z > 14) -> x >= 5;
```

Note the analog to the simple approach to let elimination does not give a correct translation:

```
var 0..9: x;
var 2..9: y;
var int: z;
constraint (y = x - 1 /\ z = x * y /\ y + z * z > 14) -> x >= 5;
```

gives answers for all possible values of `x`

, whereas the original
constraint removes the possibility that `x = 4`

.

The treatment of *constraint items* in let expressions is analogous
to defined variables. One can think of a constraint as equivalent to
defining a new Boolean variable. The definitions of the new Boolean variables
are extracted to the top level, and the Boolean remains in the correct
context.

```
constraint z > 1 -> let { var int: y,
constraint (x >= 0) -> y = x,
constraint (x < 0) -> y = -x
} in y * (y - 2) >= z;
```

is treated like

```
constraint z > 1 -> let { var int: y,
var bool: b1 = ((x >= 0) -> y = x),
var bool: b2 = ((x < 0) -> y = -x),
constraint b1 /\ b2
} in y * (y - 2) >= z;
```

and flattens to

```
constraint b1 = ((x >= 0) -> y = x);
constraint b2 = ((x < 0) -> y = -x);
constraint z > 1 -> (b1 /\ b2 /\ y * (y - 2) >= z);
```