0:00

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.

Â