Welcome to the reference section on predicates. So predicates are basically a way of writing on a macro constraints. But we should be aware that they're not like macros in the sense of they have a local variables and predicates, then you get a new copy of that variable every time. So it's more like a procedure. So the important thing is they allow us to encapsulate and name and re-use important constraints and indeed they are critical to the way MiniZinc implements global constraints for various solvers. So a predicate thats in use has to be declared so this is with the predicate key word and then the name. And then the types of each of its arguments. For example here, we see the old different constant. It takes a single array of var integers and has as its only argument. And notice that array sizes need not be known. Whereas when you're declaring the array usually you need to either give the size explicitly, if it's var or you need to build the array with some declaration, so that MiniZinc can work out the science. But notice that this here, it just has the declaration and fused with a semicolon, it only declares the predicate. Now this is enough to be able to be used in a model and really only makes sense if the solver you're using understands the predicate directly. So predicates can be defined, so this is the same thing as a declaration. So basically, a definition extends a declaration by adding basically this Boolean expression which, Defines what the predicate means. And so here's our alldifferent constraint with the definition of what it means. And here it says, forall(i, j in index_set(x) where i < j), basically for all pairs of elements in the array x(i) != x(j). And if I use this predicate, then basically what MiniZinc is going to do is replace anytime I use alldifferent on an array, it's going to replace it with a copy of the body Boolean expression. But as we said before, predicates don't need to be defined if the software directly understands them. So there's also tests we only rarely use them in MiniZinc, but they can be useful. And a test is basically a predicate, except that it returns a par bool. So it's only working on parameters. This can be useful for building some complicated test that you're using in lots of expressions in your code. So basically it looks exactly like a predicate except it has this test definitions. The tests always have to be defined and they can't involve variables. So basically, we can use this in this example here building a test saying that do these row columns indicate a different position. It obviously indicated a different position. If either the rows are different or the columns are different, it is what that definition says. The test can't involve variables. This is useful if you want to build complex test that you are going to be using multiple paths for your model. So MiniZinc Globals are predicate declarations, declaring that this predicate is understood. And then a definition which is specific to the solver that we are going to use. So we can imagine if we're using a constraint programming solver with a builtin alldifferent, then you'll just have a definition, that's with a declaration like this with no definition. And that means that this all any cause for alldifferent will be sent directly to the solver. If we're using a CP solver without a builtin, then we might define the alldifferent constraint. This way, we're basically saying we're going to replace it with this big injection of disequalities is possible that every pair of variables in array has a different value. Now if we're using a MIP solver we might have very different decomposition. So here we're looking at all the possible values that the variables in the array could take. And saying, well, it's going to sum up over that array how many times that a variable takes that value. And make sure that that's less than or equal to one. So, because this is a linear constraint which is going to be understood easily by the MIP solver, but you can see it's a very different view on the whole thing. So we've seen the examples in the previous slide, but often when we want to use predicates it's useful to know properties of the variables in that model. So remember when we're building loops and different things like this, we typically want them to be fixed by knowledge that we know the beginning in MiniZinc before the solver runs. And so we need to extract things about variables even before they're fixed. So the lower bound of x returns a lower bound on all the possible values of x. And similarly the upper bound of x returns an upper bound. So, for example, in here obviously x is lower bound. The obvious lower bound is -4 and the obvious upper bound is 6 they've declared that. We can also use domain of x, which returns a superset of all possible of values of x. We do dom(x), just looking at this thing here, we'd expect to get back the set from -4 to 6, all the numbers from -4 to 6. And there's versions of this to work on arrays. We can get the lower bound of all the variables in array x, and upper bound of all the values in array x similarly. Now we have to be careful but these things are not guaranteed to be the clear bounds. They can be anything that is actually correct. That MiniZinc can work out at the time. So for example we look at this example here, we would imagine that the lower bound of x would return -4. That would make sense because that's the declared bound. And that's certainly a correct bound. But actually if we know that x is the absolute value of y. Well we know that actually has to be positive. So it means you could say well the lower end of x is 0. Because it might have done some advanced computation and actually refined the bounds of x to be 0. And if you have done some pre-solving or actually run this constraint it might actually be able to work that more because in fact the only solutions for x which is the output value of y from -4, 2, it is basically from 2, to 4. All right, so lb(x) could be returned as 2. So we're guaranteed that the lower bound is correct, but we're not guaranteed that it's what we declared it to be. So we have to be careful when we're using these, to know, to make sure that the code that we produce is correct for whatever value of lower bound we get. Now, on the assumption that that's correct for all x. So let's have a look at using those reflections, very similar to what we saw in the MIP example. So the in variable constraints basically counts the number of different values occur in the array x. So here is the definition for this predicate and so what are we going to do? We're going to look at all the possible values that could appear in this array x. We have the low bound of the array x the upper bound of the array x and we're going to check for each possible value. Does their existent and actual index in the array which takes that value. So we're basically doing this count. Count for each possible value of j occurring in the array if it actually appears. For each part of the array that could be in the array if it appears count up that number and then we know the number of different values that occurred in the array. So you know to use predicate declarations. Once we've declared a predicate we can use the predicate in the model. If we only have a declaration then basically we're assuming that the solver we're using understands it. But predicate definitions replace the use of the predicate by the definition constraints. And test are basically the same but they return bools not var bools. And then the global constraints in MiniZinc are implemented using predicates. And in order to do that we need these reflection functions which allow us to basically find fixed information about variables that appear in the predicate. That brings to the end to this section.