Welcome to the reference section on User Defined Functions.

So, we've seen how user-defined predicates

in MiniZinc provide us macro facilities for constraints.

Basically, you can write down a predicate as a shorthand for a constraint,

and we can reuse that constraint throughout our model.

So, user-defined functions refine effectively macro facilities for expressions.

But there are restrictions on user-defined functions,

particularly because they can introduce complexities arising from partialness

of the functions, so we have to be worried about the function not being able to evaluate.

So, functions is defined in MiniZinc.

There is straightforwardly the function keyword,

then the type of the result of the function, the function name,

and then a set of arguments just like in the predicate withtype,

and then the argument name.

And the new part is the expression here,

and the expression must be of the same as the type of the function.

And basically, you can think of functions.

Basically when you use a function, you replace it by copies of its body expression.

And functions have to be defined.

They can't be undefined like we can with some predicates

and leave them to the solver to understand.

So user-defined functions are always defined in the model.

It's something that loads into the model.

So, functions are most useful when they can define these variable expressions

that can be reused.

So, an example would be, let's say, the Manhattan distance function here,

which returns the Manhattan distance between two points x1 and y1, and x2, y2.

And so, you can see we can work out the Manhattan distance,

it's just the absolute difference for x2 and x1,

and the absolute difference between y2 and y1.

And we can use this to model constraints involving Manhattan distance.

So, in our model for dangerous prisoners, putting prisoners in cellblocks,

we need a constraint to make sure that nooone is adjacent to dangerous prisoners.

And we could have written this in this way saying, 'for every prisoner

and for every dangerous prisoner,

then we want to make sure that the Manhattan distance between the positions

of those two prisoners is greater than one.

So, another thing that functions introduce is the ability to use local constraints.

So, we can do this elsewhere, but it's most useful inside functions.

So, here's a function for returning the absolute value of an integer.

And what we're doing here is, we're saying,

well, we're introducing a new local variable y,

and then we constrain the factor using this constraint

which says that y is the absolute value of x.

And then we're returning the value y.

We can see we've got this local constraint here.

This constraint here inside this let.

So, typically, local constraints are required

because when we add local variables inside functions,

we want to be able to constrain them.

And if we're building expressions, we can't do that,

but we can add these local constraints to constraint for the y.

And indeed, most of the MiniZinc built-in functions are defined this way

because constraints always only have relations.

What happens is, when we write an absolute value expression,

it's actually translated into an absolute value constraint by this definition.

So, we have to understand what happens with these local constraints.

And just as we saw with the undefined result,

local constraints float up to the nearest enclosing Boolean expression.

So, if I write this a is not equal to zero, or my absolute value

of a times bconstraint is > c

then this my absolute value is going to be replaced by the result t,

this local variable equal y in the definition of myabs.

We get a new variable.

And then we add a constraint saying that the absolute value of a,

for x is a and t is y, this is the constraint.

And then, since it starts here in this position t,

it floats up to the nearest enclosing Boolean context which is t times b > c.

And then we conjoin it with that.

So, the overall thing is that this constraint here occurs in this disjunction,

which is where the function float happened.

So, these local constraints are very powerful in fact.

They allow us to introduce new constraints in any point of the model,

but we're not really because, of course, any constraints you introduce here

are floating up to the nearest enclosing Boolean context.

So, this allows us to add local variables

and local constraints in any position we ever want.

Sometimes this is very useful but it's most useful in defining user-defined functions

where inside the function I want to define some constraints.

So, we have to be aware,

remember that when a let constructs introduce new variables without any definition

on the right-hand side, then it can only be used in positive context.

So, this is a restriction of let introducing new variables.

And one of the things that happens when we

introduce functions with local variables is,

we often did not give them a definition because we're gonna add constraints

to give it the definition.

And effectively, this means that,

without any further ado, we can't use user-defined functions in negative or mixed context.

So, if I'll think of my example here, the absolute value example,

then it defines a new variable y which is not assigned to a value.

And so, this my-absolute-value function could not be used in a negative or mixed context.

But we would like to because, in fact, we know that if you fix x,

then this absolute value constraint will force a unique value for y.

So, we know that this really is a function, that we're talking about here,

and there is no problem of it actually giving me an undefined result.

So, we can annotate a function as total,

and that means it's safe to use in non-positive context,

and it means we're going to actually change how it behaves.

We're going to float the body of the function up to the root context

because we know it can't float.

So, here is now example here.

We've got the same exact definition, but we've added this promise_total.

And now, in this example, we can use the absolute,

my-absolute-value function in a negative context in this side of the implication.

And what will happen is, this will float up,

we'll introduce the new variable y, we'll introduce the absolute value of a is y,

and then we'll just rewrite this as y>4 implies b<4.

And this is safe because we're basically promising with this promise_total

that this can never fail to give you an answer, that the constraints always hold.

So, but what happens if we do want it to find partial functions?

Well, the way we do this is, so, splitting it into two parts.

We build a partial function with no local variables.

So, it's got no local variables.

It could be used in any context that calls a total function with local variables.

So, we're going to push the local variables inside the total function.

So, here's an example of this.

We're going to build a division function.

And obviously, division is a partial function because we've got to divide by zero.

We'll just do it for y non-negative numbers, that's the value divided by zero.

So, here's our division user-defined function.

So, x div y.

This is meant to give the result of x div y.

Now, we're gonna add an assertion to make sure that x and y are nonnegative,

otherwise we know this code is wrong, better be checked at and flatten the model.

So, if the lower bounds of x and y,

so x or y could technically very easily just this allows to happen.

The key thing is here.

This function knows has no local variable, has one local constraint which says:

y is not equal to zero.

So, this has no local variables, can be used in any context,

and the safe division here has got a promise_total.

And of course, we know that a promise_total can be used in any context.

So, if we pass this test, the y equal to zero, then we know that we can safely do division

and we're not going to get an undefined result.

And here, we defined a remainder and the result of the division,

z, and the constraints that relate them.

And so, we know that x is y times z plus this remainder,

and the remainder has to be less than y.

And then the result of this div is the zed,

basically how many times does y go to x with a remainder with both.

So, this constraint makes the safediv total because we know by the time it gets here,

that y cannot be equal to zero.

And what happens in this flattening is that this constraint

will float to the nearest Boolean context of mydiv,

and that will force that when it's used, y cannot be equal zero.

Then this body will float to the root level, and these constraints will be this.

So, basically these introduced variables are the root level

and we've overcome problems with negative context.

So, in summary, functions give us macros for complex expressions.

And they certainly improve common sub-expression elimination in MiniZinc.

So, if you used user-defined functions for things that appear multiple times,

you'll possibly get a better model because MiniZinc

will have an easier approach to noticing that these things are the same.

You can include constraints in the let constructs,

and basically this is a very powerful feature but it's really most useful

for defining user-defined functions.

And then, we can use promise_total to make sure

that we can use functions with let in non-positive context.

There is a pause for total functions.

And if we need to build user-defined non-total functions,

then we can do this trick of splitting them into two,

where the topmost one has no local variables and the underneath one is total,

but these are local variables.

That brings the end of the section.