So, in order to understand, how your MiniZinc model is actually run, we're going to have to understand the process of taking your MiniZinc model, which you've written in this high-level MiniZinc, and what gets sent to the solver, which finally does the solving. And we call this process flattening. And there's lots of parts of this flattening that we're going to go through. So, flattening expressions, unrolling expressions which is what happens with loops, and how we handle arrays, and how we handle reification, and predicates and let expressions. So, that's going to show you the major components of the flattening process. All right. So, if you think about the MiniZinc tool chain, we start off with our model. Right. And some data, and then we have a globals library, which might have some definition of the globals. And then, that's combined together, we send it to this translator. This is what actually happens is, this translator translates your MiniZinc to FlatZinc for a specific solver. So, the globals library here is telling it what specific solver is. And actually creates this FlatZinc file, which is what is sent to the solver. So the solver takes that, it finds a solution, and then actually the solution is combined together with the output file to give you a pretty version of the output. So that's what's happening inside the MiniZinc tool chain. And the critical thing that we're going to talk about here is this process here, where we take your model and data and create a flat model, which is what the solver can understand. Alright. So it's exactly this. We take the model, the data, and the global definitions for the particular solver we're using, and creating a FlatZinc model. And FlatZinc models are very simple. They only have variables and possibly parameters, definitions, they have primitive constraints, so just a single constraint per line. They can have a solve item which is just to say whether we are minimising, or maximising, or just finding a solution. And some annotations on some variables saying, well, we need to know these variables values for the output. We don't actually do the output here, the output is done separately. Okay. So what's the first step? The main step in flattening is flattening expressions, because your model is made up of expressions. So, we need to simplify those expressions, we need to evaluate any expressions which are fixed. So, once we have data, lot of these expressions may just take a fixed value of course, the solver doesn't need to know these things. The solver's aim is to take all of the decision variables and work out their values. It doesn't care about fixed things as much, except that they are used to express the constraints. We also have to name subexpressions right. And that's effectively the flattening, because we're basically going to be able to give the solver just a list of constraints. So, there's no structure in some sense in the solver. We have a new name for each subexpression, and then the solver evaluates a constraint which will evaluate that subexpression. We're also going to have to do bounds analysis, because we're going to introduce these new variables to name subexpressions, and we're going to want to know upper and lower bounds of those. Now, an important thing that we're going to need to do, is common subexpression elimination. So that, if we build an expression again, that we notice it's the same one. So, we don't send two copies of the constraints to define it to the solver. Alright. So, let's have a look at this small model. So, we have a couple of parameters, i and j. We have three different variables here, and we've got this constraint here. Okay. So, let's look at the resulting flat model. So, okay x, y, and z, these are all the same as they were before. So, all the variables are basically going to be sent to the solver as is. So, we've introduced a new intermediate variable, INT01 and it's given some bounds. We've introduced another intermediate variable INT02, we've given it some bounds although we couldn't work out any useful bounds there. And so, INT01 represents this y times z expression here, right? And we can do some bounds calculations on that. Well, if y and z are between zero and two, and zero and three, then this has to be between zero and six. And this expression INT02 is x times y. But since we don't know anything about x, then we can't really say anything about the values of INT02 except that it's an integer. And then we've simplified this expression here to say well INT02, plus INT01. Alright. So, we've inverted the order is less than equal two well, i times j, well, that's just six. So, we actually just evaluated that i times j, this is both parameters, we know their values, we just replace it by six. So, this is the basic flat model. Alright. So, you can see we've done expression evaluation, we've done subexpression naming for INT01, INT02. We've worked the bounds of some of those subexpressions where we could, and we've added constraints to define those subexpressions. And then we've used subexpressions in our constraint. Alright. If we look at the actual results in FlatZinc, it's a little bit more complicated. Right. So, here we've got some annotation. So, is_defined _var here is saying that, this is a variable that we've introduced by the flattener. Similarly here. And this is just the FlatZinc form of the constraints we saw in the previous lot. So these ones here. Of course now, I have to run through all this modification. Right. So, that's y times z, is INT01. And we also have this annotation saying, well this is actually a constraint which defines this variable INT01. And similarly for the other constraint that defines the variable INT02. And then, the form of the linear expression is this one, which is basically saying one times INT02, plus one times INT01 is less than or equal to six. Alright. So that's just the actual FlatZinc form. Okay. So, you can see the subexpression linking. So, we can look at this INT01, and say, well, this is the expression that defines it, right? And it's a defined var. And then we know we will be able to find some constraint which actually defines its value. Alright. So, let's start with a flattening exercise. What do you think will result from flattening this version of the problem? So it's almost exactly the same, we got two parameters i and j, we've here got three variables x, y, and z. They all bounded variables in this case, and then we've got this expression here. Alright. So, first thing, oh, did you notice that there's a common subexpression? So, if we look at this example, x minus i here, and x minus j here, well i and j are both three. So, they really generating the same expression which is x minus three. Right? So, we can call that INT01. And in fact, INT01 will take a value between minus three and two, which is pretty obvious if it's x minus three. Then this multiplication here, just becomes INT01 times INT01, so that's our expression INT02, and then the rest of this constraint is all linear. So, we can keep that as one single linear constraint together. So, if we take INT02, which is just x minus three times x minus three, plus y, plus z, plus six. Of course, so it's i plus j, we can just evaluate those add them up, just give six greater than or equal to zero. We could actually move this six over here to say, greater than or equal to minus six. So, it's very important when we're doing this flattening, that we don't introduce two names for the same expression. And notice here, x minus i, and x minus j, do not look like the same expression, if we just look at our model. But as it turns out, since i and j are both three, they actually do represent the same expression from the point of view of the solver. Alright. And then the FlatZinc that we actually get looks like this, where we can see this x minus three becomes this INT lin equality. This is an integer times, like we've seen before. And then, the last constraint was also an INT linear equality. Okay, so, Common Subexpression Elimination is a very important part of flattening, because having two names for the same variable inside the solver can be very, very expensive. Basically, it's kind of doubling the amount of work the solver might have to do to work out that they actually have to take the same value. Okay, so, when we're flattening, then, our flattener builds an expression to see if it's been used before. And if that's the case, it uses the same name. So this is rather important for small models and efficient models. And it's actually a part of all kind of programming language compilation to look for common subexpressions and eliminate them. But notice, it's not perfect in MiniZinc. So, if we think of x times y, times y minus x, is greater than equal to y minus x, then MiniZinc will notice that this y minus x and this y minus x maybe are the same thing, but it won't notice that actually, x minus y is really the same thing, just the negation of it. So, we'll get this expression here, which equals this FlatZinc, whereas, we could have had something better by realising that x minus y is just minus y minus x. Okay, so, another thing that flattening needs to do is do tight bounds on the variables. So, we're going to introduce these new variables and the tight bounds on the variables is going to help the solver, because it's going to mean there's less decisions to make there. It's also going to reduce the size of unrolling, when we see later. When we'll be unrolling things a variable number of times, the tighter to the bounds we have on those variables, the less unrolling we'll need to do. So, when we're introducing a new intermediate expression, INT01, which is holding the value of this expression, we want to determine the least possible value that that expression could take, and the greatest possible value that expression could take. And then, when we introduce the variable, INT01, we're going to declare it as taking values between l and u. And we've already seen examples of doing that. So, if we think about this example here, we'll have x and y. And x is taking values between minus two and two, and y taking values between zero and four. And we have this sort of quadratic constraint. Then, if we look at what FlatZinc does, it doesn't actually do a great job on working out the bounds. Okay, so, INT01 is x times x, so it's between minus four and four. So, if you take some number which is minus two to two and multiply by another number which is minus two to two, then you're definitely going to get a number between minus four and four. And similarly, INT02 which is y times y, is your number between zero and 16. And then, we add those together, it's less than equal to six. And you can see that we can do a lot better here because, of course, this x squared is certainly going to be positive. So this really should be between zero and four, for example. And we could actually take this value since INT02 could never take a value of 16. Because once we're adding a positive number, INT01 and INT02 are both positive together, and they're less than equal to six. And in fact, this could not be bigger than six. So, this could be improved and we have presolve for MiniZinc which eventually will be coming and improve this, so you won't see this kind of behaviour. We'll get better bounds analysis. So, that's the kind of bounds analysis we'd like to get in the end, right? Once we know that this is positive, and then we know that this is at most six, that's going to tell that y cannot take a value outside the value zero to two. Because if we do, then we'd square, we get a number bigger than zero to six. And you can see, what we've done here is actually, reduced the bounds on decision variables, not just on intermediate variables. And that is certainly going to help the solver. Alright, so, linear constraints are basically the most common constraint that we generate in our models. And so, they're very important. So, if we have this kind of example, we have to look for linear constraints. Here, k is a fixed parameter, and this thing here, which sort of maybe doesn't look exactly like a linear constraint is actually linear. Since this is fixed, then this is just a linear term. And this is a linear term. Because this is linear, we multiply by a constant. So, if we do a naive translation of this, we would break it into lots of little bits. We'd introduce a local variable for this y minus z, and then, introduce another local variable for this two times that thing. Then we'd have x plus this that would be a local variable to represent this expression. And we take that and add z to it, and we get a local variable representing that expression. And then, we take four times z, make a local variable for this expression, and then we say this is less than equal to this. But actually, we don't really want to do that. The solvers can handle a linear constraint directly, a complex linear constraint. What we want to do is simplify this down to this linear form, right? So, it's minus one times x. So, we've collected together the x terms, is single x minus 2x, so overall, minus one times x, it's two times y, and it's minus three times z by moving this 4z over here to the other side. That's the constraint we want to send to the solver, not all these little constraints. Okay, and that's just a single INT linear less than or equal to constraint in FlatZinc format. Alright. So, unrolling is important. So, models are typically not fixed size. The size of the actual final model that goes to the solver depends on the data in the model. And so, we are going to use iterative constraints everywhere. We're used to this now, we have foralls and sums and these kind of things throughout our models. So, let's have a look at this little example here, where I have n objects, and they have a size and a value. So, this is a knapsack problem. And we're basically deciding for each of these objects how many to take. So, we can look at we have this constraint. Well, all of the values that number of times we take every object has to have gotten through zero. So, that's a forall over these objects. And then, we've got the sum, if we sum over all the objects of this size times the number we take, that has to be less than equal to the size limit. And then, we're trying to maximise this sum of the value of each object times a number of times we take it. And we'll start with some simple data here, where we've got four objects with these sizes and these values and this size limit. Alright. So what's going to happen to this in terms of unrolling? Alright, so, iteration in MiniZinc is always actually really one thing. We only build a big array, and then we apply a function to it. So when we write this, we're really just writing a syntactic sugar for this, which says, "Apply the sum function to this array." So, we take this size of i times x of i, we build one of those for each of the i's in object that gives us an array. And then, we take sum of that, and we say that's less than or equal to the limit. So, you can think about this in terms of array comprehension. So we're going to build up an array which has each of these expressions in it. So, I'm going to get the first one which is five, that's the size of the first object times x of one. Then the second one which is eight, the size of the second object times x of two. There's the third and the fourth object, then we build this array, which has all of those four expressions in it. And then, we sum them up, and then we say that's less than or equal to 29. Alright, so that's the naive way of what's happening in this array comprehension. And this is the general case it will work. Of course, in this case, we may want to do better. Because it's just a single linear constraint, we want to know just that and do better. Alright, what about conjunctions and foralls? So, there's a important distinction in MiniZinc between top level conjunctions and conjunctions that occur inside other kinds of logical operators like implication and disjunction. Because the constraint solver just takes a single conjunction of constraints. So top level conjunctions are fine because they just give you more and more constraints, which is just conjoined together, that single top level conjunction. So, if I have constraint forall, like as an example here, so this is a top level constraint. And this forall is just going to make a and, and, and, and. And so, all of them can be broken up and sent separately. So if you think about it naively, we, first of all, build this array of all the constraints. And then, we say forall on that array, which is basically saying, "This is true, and this is true, and this is true, and this is true," and the result is just going to be these four individual constraints, because we're at the top level. So if this was, let's say, b or forall, then we're not going to be able to do that, because the constraints are no longer at the top level. Alright, what about objectives? So, an example here, we have this objective, which is the sum of the value times x of i. We're going to unroll just simply as we did before, for the linear constraint. So, we're going to build up this array of all the possible things that we're summing up. Then, we're going to take the sum and then , we're going to call the solve maximise on this result. And this is one of the restrictions of MiniZinc is that effectively, we always build up a local variable, a newly introduced variable which holds the value of the objective. And then, the constraints that we get will always be something like, solve, maximise and a variable name, will solve minimise and a variable name. So, the objective will be given a name, given a variable that contains it and then, set to the solver in that way. Alright. A bit more about unrolling, if we look at that knapsack problem. After we do the linear constraints simplification which I mentioned before, the forall mapped into these four inequalities, the bounds on the limit mapped into this single inequality. So, basically we've got rid of, we've evaluated the sum, got a linear expression, and we've replaced that into the constraint, which said it was less than or equal to 29. We've introduced an objective variable which takes the values of the objects times the number of times we take them, and then we solve minimize with respect to that objective variable. So, there's our final value. All right and if we look at it in FlatZinc, that's what it's going to look like in FlatZinc, which is a bit harder to read. But, remember this is going to solve only, it's not really designed for human consumption. Alright, what happens to arrays? Alright so, arrays in FlatZinc are only one-dimensional and they always start from index one. Alright, so, in MiniZinc, we have multi-dimensional arrays and the indices can be all over the place. So, basically, we need to translate all of our multi-dimensional arrays into a single flat array. So, if we think about this, if we have this. Let's say two-dimensional array here, which goes from lower bound to upper bound, lower bound outer bound, the two indexes. Then, we are going to convert that into an array, which goes from one to the number of elements in this array. Which is just this expression where you take the differences between those and the differences between those, and multiply them together, adding one to each of them. And that tells you the number of elements in this array, if we just think of it as one flat thing. And notice, this isn't that different than many other kinds of programming languages, for example like C where two-dimensional arrays are really often just laid out. They're really just a one-dimensional array in memory and two dimensions is a way of accessing them. And then we have to expand, we have to convert these expressions. When I'm accessing a two-dimensional array, where I have two indexes, I have to convert that into a one-dimensional axis. So, if I'm going to access this array x of i,j, how do I find which element in this one-dimensional it is? Well basically, this is this counting. I take i minus the lower bound, I multiply it by the size of the second dimension, and then, I add j minus its lower bound plus 1. And that's going to basically tell us which element in this array corresponds to x of i,j in this array. So, let's do an example of that. So, here we have an array whose indices are from 0 to 2, and we're now going to sum up all the diagonal elements of that, and record that they are less than or equal to one. And then, we're going to do a bit trickier thing here. We're going to look up, we're going to find the 1-1 element here, use that as an index into the array, itself and set that element to 2. So, what happens in flattening. So, of course this sum just maps to x of 0,0 plus x of 1,1 plus x of 2,2 are less or equal to one. And we introduce a new local variable to represent the value of x of 1,1 right here INT01. And then, we're going to have this array look up here. Now, we got to convert so that's still two-dimensional arrays. And then, in flattening, we have converted it to a one-dimensional array. So, clearly if we look at this two-dimensional array. It's a three times three, two-dimensional array so it has nine elements. So, we get elements from one to nine. And then, we look at this x of 0,0. Well, that's actually the first element in the flat version of this array. So, that's x of 1. We look at x of 1,1. So, that's in the second row of the array and it's the second element in the second row. So, we had the length of the row which is three, plus the second element two, gives us five. And similarly x of 2,2 is the last element array, that's x of 9. So, that's what the constraint eventually comes in the FlatZinc perspective. Again, we know that x of 1,1 is actually x of 5. So, that's where INT01 is. And then, we have to calculate this index. So, this index is not fixed. So, we have to do index our calculations here. So, here, it's just we take INT01 multiply it by three. This is the calculation we saw on the previous slide. And then, we take one which is this index and add one to it because, we have to basically. The lower bound was zero, so we subtract zero and had one. And that gives us the index, this INT01,1. It means into this one-dimensional version of the array. So, once we've got this index, we can just set that the value of that index is forced to be two, that's the encoding of this constraint here. So, you can see that translating arrays is a little bit complicated. A lot of the time we can do this sort of index translation right away, because we know all these values, they're fixed. But when we have indexes with integers in it, with integer variables in it, when we're going to have to do some constraints to work out the index of the resulting value. Alright, a crucial part of CP modeling languages is in fact the element constraint which allows us to encode this thing. Where we have an array here, we look it up with another variable. And so, this is array INT element constraint takes an index. So in this case, it's INT02, an array, this is x and the results, so in this case the result is going to be two. So, this constraint here that we wrote on the previous slide, actually gets converted to this element constraint. And this is one of the crucial modeling strengths of CP languages where we can directly write array indexes with variable indexes, and use that to build quite concise models. Alright, other parts of MiniZinc which are important; if, then, else, endif. So, we've basically got an expression, if b, then true else, else the else case. So, how do we do this? So, if b is fixed, where we can evaluate it. If it's true then we replace this expression by t. And if it's false, we replace it by e. So, that's the easy case. If b is fixed, if we can work out the value of this to be true or false when we're doing the flattening, then it's easy. We just replace it by this expression, we keep flattening these expressions as usual. Otherwise, if b is not fixed then we're going to actually build a constraint to enforce this relationship. So, basically we're going to build a little array. So, this is the else case and here's the then case, and we're going to look up that array with the value of b. If you think about it here, if b is false, then this evaluates to 0 plus 1. So, we look up the first element this array and we get e. And if b is true, then this evaluates to 1 plus 1, 2. So, we look up the second element of this array and we get to t. So, if we think about our constraint here, if b then x else y endif is greater than or equal to 0, then we end up with this flattening. So, we build a little array y, x. Then, we look it up with this expression and we ask that to greater than or equal to zero. And then, we're going to flatten that a bit more, because we're going to build an expression to hold the value of this bool2int b plus 1 and then, we can convert this. This is now an element constraint and then this constraint is just a linear constraint on the result of looking up this array index. And if we look at FlatZinc, that's what it looks like. So, bool2int is in fact a built in constraint in the solver. We've got our integer plus and there's the element constraint that we talked about and a linear inequality. We also have to think about flattening Boolean expressions, because remember solvers only take a conjunction of constraints. So, what happens when we write down something like this? X greater than zero implies, some other expression with a conjunction in it, some linear constraint. Well basically, in order to write this down, we're going to have to name the constraints which make up the part of this logical expression or Boolean expression. And that's what reification is about. So, we reify constraints c by basically building this constraint b, if we only have c. When you think of b holds the true value of this constraint here. If b is true then the constraint c holds. If b is false then c doesn't hold. And most of the FlatZinc primitives have a reified version. So, our INT linear less than or equal to constraint has sort of an array of constants, and array of variables on the left hand side to build up a linear inequality. Then there's this reified version which has the same array of variables, the same array of constants, array of variables on the left hand side and then, this Boolean variable which is meant to hold, whether the constraint holds or not. Alright, so let's consider an example of reification. So, this is basically flattened in a way, very analogous to other expressions. So, x greater than 0 is not a constraint, that's necessarily true. So, we basically have to give it a name to whether it holds or not. So, that bool01. And similarly for y greater than 0, and z greater or equal to 0, so we get bool02 and bool03. And then this conjunction, we don't know whether it holds or not but we're going to need to reason about it, and that's bool04. This tells us whether that conjunction holds or not. Then, we can do this bool2int which is just converting bool01 into an integer, a 01 integer. And then, we basically have this linear constraint here which we don't know whether it holds or not, and this is its reified linear here. So, basically INT01 which is this plus t is greater than or equal to u. Is that true or not. And then, finally we can add the constraint which says that, if the first constraint holds, if bool01 is true then bool05 has to be true as well. All right. So, if we look at the FlatZinc for that, we can see we have these reified versions of a less than or equal to constraint. So, basically is x greater than or equal to 1. And we have these Boolean functions and so we're anding together two bools to get another bool. And we got bool2int as a normal FlatZinc constraint. We've got a reified version of our linear constraint to express this. And finally, we have implication constraint at the end. So, notice that avoiding negative context can help us get a simple model. So, if we try to push the negation down to the bottom level, we'll hopefully have more positive contexts and that can make things easier. So if we look at this, we know that's really the same as saying not x greater than zero or the linear inequality. And since this negation is easy, we can just write that as x less than equal to zero. And we can build up this model which is essentially the same but has less negation in it. So, we have this x less less equal to zero. We basically replace the implication constraint here by an or. And now, everything is in a positive context. And in fact, that'll give us a chance to do a better job than we do here. But this is a slightly better model in the sense that we only have positive contexts involved. If there's a more complicated thing here, then that would certainly help us. Alright, let's talk about predicates and functions. So, remember that predicate and functions act like macros and MiniZinc. Particularly, when we see an expression including them, we expand it with the arguments and then we flatten. So, they act very much like macros. The only addition is that they've got local variables we have to worry about, and we do common sub-expression elimination with functions. So if I see this f expression with all these arguments here is equated to some expression, and when I see I'm using f of arg1 to argn, I'm just going to evaluate this expression with these values stuck into it. So, let's have a look at an example. So here, we have a far_or_equal predicate, which takes two points, x, y, and says they're far_or_equal if the Manhattan distance between them is greater than equal to four, or they happen to be the same point. And here, we have a Manhattan distance function which returns a Manhattan distance between two points represented as u1, v1 and u2, v2. And of course, that's just the absolute value of the difference in the u of the x coordinates and the absolute difference in the v added up. And here, we're actually using this far_or_equal in a constraint. So, what happens? When we see the far_or_equal here, we basically replace. We look at this definition of the predicate and replace it. So, basically, wherever we saw x1, we put a, wherever we saw y1, we put b, et cetera. And here, we get a copy of this body here. So we get man_distance a, b, c, d is greater than equal to four, or a equals c, or b equals d. So basically, we just replaced this thing with its body. Now again, we've got this function evaluation here and we're going to replace that with its definition of the body. So, we get absolute of a minus c plus absolute of b minus d, replaces that call to man_dist. And now, you can see, we've just got a normal expression with no functions and no predicates in it, and we can just flatten it as usual. So, if we think about flattening this, we're going to work out the value of a minus c, take the absolute value, record value b minus d, take its absolute value, then we'll basically kind of build the reified version of this constraint, because notice, we don't know whether it holds or not, alright? So that's the reified version of that linear constraint. We're also going to work out reified versions of these two constraints in the reified version of the conjunction. So this is the BOOL04 says: Does this conjunction hold or not? And then finally, we're going to force that one of these two Booleans holds. Either this constraint must be true, or this conjunction must be true. Okay, what about predicates with no definition? So remember, if a global constraint is native to the solver, there's only a definition, not a declaration. So, if alldifferent is native in my solver, I just say, "Oh, alldifferent is like this, and that means you can send me directly alldifferent." So, if we have a call to this native predicate, what happens? So, if it's in the root context, then it's fine. We can just send it straight to the solver. If it's in a reified context or if we don't know whether constraint holds or not, so if we send it directly to the solver, we're enforcing the constraint. But if it's in a reified context where we don't know whether it's going to be true or not, we try to look at this whether there's a reified version of this predicate available. And then we basically add in this Boolean variable which is meant to hold the value of whether this constraint is true or not. And this might fail if this reified version doesn't exist. So, let's have a look at an example. So, imagine we have our global's library says, "Okay, we've got a native version of alldifferent, but we'll add in a reified version, is just the usual decomposition of alldifferent." Just saying, the truth b of this rarified alldifferent is just that all of the individual pairs of values are different. So, if we see this example code, alldifferent x, y, z, and alldifferent y, z, t implies x equals zero, then this one is in a root context so we can just send it directly to the solver as it is. This one is not in a root context, so we need to reify. So we reify that thing to get a value b, and then we can replace this by b implies x equals zero, since b is storing whether this constraint holds or not. Alright, and in fact, we would actually expand out that alldifferent, right? So, remember this alldifferent_reif is here, and so, that alldifferent would expand out into this set of inequalities, and then we'd expand out some further. We have to reify each of those individual inequalities and then build the conjunction, et cetera. Alright, one of the most complicated things we can do in a MiniZinc model is Let expressions. So they allow us to introduce new variables, alright? And remember that FlatZinc only consists of variable declarations and primitive constraints. And so, these new variables which are meant to be very local to where they're used have to be floated up to the top level. That means, we need to rename copies of the new variables. And this is actually complex in MiniZinc because of the relational semantics and the interaction of these new variables and the constraints on them with partial functions. We also have the ability to add local constraints, in our Let expressions, which also complicates things. So, if we look at some expression which has a let inside it, remember, so here's a Let. We're introducing a variable. We're introducing another constraint. And that Let is respect to using x, so you can use it here. The first thing we need to do is rename it to be a new variable. So that's easy enough. It's just that we don't want this x to conflict with any other x, particularly if this expression here is a looping one. We're going to get multiple copies. We need to know that they're not the same variable. And then, once we've renamed the variable, we want to basically introduce a new variable to name this constraint, because it's not clear whether this constraint is going to hold or not, depends on what the outlying expression is. So, we're basically saying b is equal to c, so that's the reified version of the constraint. And then we're just saying constraint b. So that's forcing the constraint to hold at least in this local context. Now, we can float out the local variable declarations to the nearest enclosing Boolean context because that's the rule in MiniZinc for the relational semantics. And basically, then we're done. Now that may seem complicated. Let's have a look at an example. So here, we've got some constraint here. So a negation of some sum calling a local function. square-root inside. Okay, so here's our square root function, and inside the square-function, I introduce a local variable y. I said y times y equals x, and y is greater than or equal to zero. And then I return that y. And so, that's a good definition of integer square-root. So, unrolling the sum gives us two copies of this square-root function, and basically, I get two copies of this Let expression. But the first thing I need to notice is those two copies of y are not the same. This is a y which is used for this thing, and this is a y which is used for this thing. We don't want to mix them up. So we have to rename the local variables. Actually, first of all, if we introduce local variables inside a non-positive expression, we have to know that they total. So, we probably have to add a promise_total into our function to allow us to do this. Okay, but once we do that, then the compiler will say, "Okay, you are not introducing local variables which don't have a definition." And then we rename the two ys to be y1 and y2. So they're now different. Okay, next step. Now, we introduce a new Boolean variable which names this constraint. So here's the Boolean variable, b1, which names all of the constraints, in fact, which used to be inside this Let construct. We do the same for the other one. And then, we look where's the nearest enclosing Boolean context. It's actually this eight greater than or equal to the sum, is the nearest enclosing Boolean context. So, we're going to lift out things to that point. So, we get not b1 and b2. These are the constraints which we floated out to that context, is the original constraint which is eight greater than or equal to y1 plus y2, and then these are the definitions. All the variables are being floated out to the top, and the definitions of b1 which is what this constraint means, and the definitions of b2 are now at the top. So you can see, the variables float right to the top where the names of the constraints float to is in the nearest Boolean context. And that gives us the result. Okay, you can see that pushing negations can make this a whole lot better. So if we push the negation through that greater than or equal to, we just get this thing here. And now, the nearest Boolean context is the root. So if we float things out, we just get that eight is less than y1 plus y2, and b1 and b2 which just splits up into these individual constraints. But then, now, we can see that b1 is just true. So we can actually simplify and just force these constraints to hold straight away, and get rid of these Boolean variables because we know they are true. And so, you can see in this case, how pushing negations can end up with a much simpler version of our flattened model. Alright. So, flattening top level conjunctions can also help. So here, we have y1 and y2. Those are our usual variables, and our not here if we did it later on. We can remove these things here which were just functional definitions, y times y equals a1. We can split them out into separate constraints. Alright, so understanding how MiniZinc works in terms of flattening is important because it helps us in debugging models. We can actually look at the FlatZinc and sort of see what's going on there. It also helps us in understanding why some different modeling approaches are preferable to others. Because one model might produce a very small FlatZinc file, another model a very large one, and typically, that means that the first model is better because small FlatZinc file means less constraints going into the solver, less variables, and usually, the solver will have a better job of doing that. So, flattening is this process in MiniZinc to convert a MiniZinc model to a conjunction of primitive constraints and variable declarations, which the solver can handle. And it's a critical part of how MiniZinc works.
