this repo has no description
dekker.one
1.. index::
2 single: predicate
3 single: function
4
5.. _sec-predicates:
6
7Predicates and Functions
8========================
9
10Predicates in MiniZinc
11allow us to capture complex constraints of our model
12in a succinct way. Predicates in MiniZinc
13are used to model with both predefined global
14constraints, and to capture and define new complex constraints by the
15modeller.
16Functions are used in MiniZinc to capture common structures of models.
17Indeed a predicate is just a function with output type :mzn:`var bool`.
18
19.. _sec-globals:
20
21Global Constraints
22------------------
23
24.. index::
25 single: global constraint
26
27There are many global constraints defined in MiniZinc for use in modelling.
28The definitive list is to be found in the documentation for the release, as
29the list is slowly growing.
30Below we discuss some of the most important global constraints.
31
32
33Alldifferent
34~~~~~~~~~~~~
35
36.. index::
37 single: alldifferent
38 single: global constraint; alldifferent
39
40The :mzn:`alldifferent` constraint takes an array of variables and constrains them
41to take different values.
42A use of the :mzn:`alldifferent` has the form
43
44.. code-block:: minizinc
45
46 alldifferent(array[int] of var int: x)
47
48The argument is an array of integer variables.
49
50The :mzn:`alldifferent` constraint is one of the most studied and used global constraints in
51constraint programming. It is used to define assignment subproblems, and
52efficient global propagators for :mzn:`alldifferent` exist.
53The models :download:`send-more-money.mzn <examples/send-more-money.mzn>` (:numref:`ex-smm`)
54and :download:`sudoku.mzn <examples/sudoku.mzn>` (:numref:`ex-sudoku`)
55are examples of models using :mzn:`alldifferent`.
56
57Cumulative
58~~~~~~~~~~
59
60.. index::
61 single: cumulative
62 single: global constraint; cumulative
63
64The :mzn:`cumulative` constraint is used for describing cumulative resource
65usage.
66
67.. code-block:: minizinc
68
69 cumulative(array[int] of var int: s, array[int] of var int: d,
70 array[int] of var int: r, var int: b)
71
72It requires that a set of tasks given by start times :mzn:`s`, durations :mzn:`d`,
73and resource requirements :mzn:`r`, never require more
74than a global resource bound :mzn:`b` at any one time.
75
76.. literalinclude:: examples/moving.mzn
77 :language: minizinc
78 :name: ex-moving
79 :caption: Model for moving furniture using ``cumulative`` (:download:`moving.mzn <examples/moving.mzn>`).
80
81.. literalinclude:: examples/moving.dzn
82 :language: minizinc
83 :name: ex-movingd
84 :caption: Data for moving furniture using ``cumulative`` (:download:`moving.dzn <examples/moving.dzn>`).
85
86The model in :numref:`ex-moving` finds a schedule for moving furniture
87so that each piece of furniture has enough handlers (people) and enough trolleys
88available during the move. The available time, handlers
89and trolleys are given, and the data gives for each object the move
90duration,
91the number of handlers and the number of trolleys required.
92Using the data shown in :mzn:`ex-movingd`, the command
93
94.. code-block:: bash
95
96 $ minizinc moving.mzn moving.dzn
97
98may result in the output
99
100.. code-block:: none
101
102 start = [0, 60, 60, 90, 120, 0, 15, 105]
103 end = 140
104 ----------
105 ==========
106
107:numref:`fig-histogram-a` and :numref:`fig-histogram-b`
108show the requirements for handlers and
109trolleys at each time in the move for this solution.
110
111.. _fig-histogram-a:
112
113.. figure:: figures/handlers.*
114
115 Histogram of usage of handlers in the move.
116
117.. _fig-histogram-b:
118
119.. figure:: figures/trolleys.*
120
121 Histogram of usage of trolleys in the move.
122
123Table
124~~~~~
125
126.. index::
127 single: table
128 single: global constraint; table
129
130The :mzn:`table` constraint enforces that a tuple of variables
131takes a value from a set of tuples. Since there are no tuples in MiniZinc
132this is encoded using arrays. The usage of :mzn:`table`
133has one of the forms
134
135.. code-block:: minizinc
136
137 table(array[int] of var bool: x, array[int, int] of bool: t)
138 table(array[int] of var int: x, array[int, int] of int: t)
139
140depending on whether the tuples are Boolean or integer.
141The constraint enforces :math:`x \in t` where we consider :math:`x`
142and each row in :math:`t` to be a tuple,
143and :math:`t` to be a set of tuples.
144
145.. literalinclude:: examples/meal.mzn
146 :language: minizinc
147 :name: ex-meal
148 :caption: Model for meal planning using ``table`` constraint (:download:`meal.mzn <examples/meal.mzn>`).
149
150.. literalinclude:: examples/meal.dzn
151 :language: minizinc
152 :name: ex-meald
153 :caption: Data for meal planning defining the ``table`` used (:download:`meal.dzn <examples/meal.dzn>`).
154
155The model in :numref:`ex-meal` searches for balanced meals.
156Each meal item has a name (encoded as an integer), a kilojoule count,
157protein in grams, salt in milligrams, and fat in grams, as well as cost
158in cents. The relationship between these items is encoded using
159a :mzn:`table` constraint.
160The model searches for a minimal cost meal
161which has a minimum kilojoule count
162:mzn:`min_energy`, a minimum amount of protein :mzn:`min_protein`,
163maximum amount of salt :mzn:`max_salt` and fat :mzn:`max_fat`.
164
165Regular
166~~~~~~~
167
168.. index::
169 single: regular
170 single: global constraint; regular
171
172
173The :mzn:`regular` constraint is used to enforce that a sequence of
174variables takes a value defined by a finite automaton.
175The usage of :mzn:`regular` has the form
176
177.. code-block:: minizinc
178
179 regular(array[int] of var int: x, int: Q, int: S,
180 array[int,int] of int: d, int: q0, set of int: F)
181
182It constrains that
183the sequence of values in array :mzn:`x` (which must all be in the :index:`range`
184:mzn:`1..S`)
185is accepted by the :index:`DFA` of :mzn:`Q` states with input :mzn:`1..S`
186and transition function :mzn:`d` (which maps :mzn:`<1..Q, 1..S>` to
187:mzn:`0..Q`) and initial state
188:mzn:`q0` (which must be in :mzn:`1..Q`) and accepting states :mzn:`F`
189(which all must be in :mzn:`1..Q`).
190State 0 is reserved to be an always failing state.
191
192.. _fig-dfa:
193
194.. figure:: figures/dfa.*
195
196 A DFA determining correct rosters.
197
198Consider a nurse rostering problem. Each nurse is scheduled for each day as
199either: (d) on day shift, (n) on night shift, or (o) off.
200In each four day period a nurse must have at least one day off, and
201no nurse can be scheduled for 3 night shifts in a row.
202This can be encoded using the incomplete DFA shown in :numref:`fig-dfa`.
203We can encode this DFA as having start state :mzn:`1`, final states :mzn:`1..6`,
204and transition function
205
206.. cssclass:: table-nonfluid table-bordered
207
208+---+---+---+---+
209| | d | n | o |
210+===+===+===+===+
211| 1 | 2 | 3 | 1 |
212+---+---+---+---+
213| 2 | 4 | 4 | 1 |
214+---+---+---+---+
215| 3 | 4 | 5 | 1 |
216+---+---+---+---+
217| 4 | 6 | 6 | 1 |
218+---+---+---+---+
219| 5 | 6 | 0 | 1 |
220+---+---+---+---+
221| 6 | 0 | 0 | 1 |
222+---+---+---+---+
223
224Note that state 0 in the table indicates an error state.
225The model shown in :numref:`ex-nurse` finds a schedule for
226:mzn:`num_nurses` nurses over :mzn:`num_days` days, where we
227require :mzn:`req_day` nurses on day shift each day, and
228:mzn:`req_night` nurses on night shift, and that each nurse
229takes at least :mzn:`min_night` night shifts.
230
231.. literalinclude:: examples/nurse.mzn
232 :language: minizinc
233 :name: ex-nurse
234 :caption: Model for nurse rostering using ``regular`` constraint (:download:`nurse.mzn <examples/nurse.mzn>`)
235
236Running the command
237
238.. code-block:: bash
239
240 $ minizinc nurse.mzn nurse.dzn
241
242finds a 10 day schedule for 7 nurses, requiring 3 on each day shift
243and 2 on each night shift, with a minimum 2 night shifts per nurse.
244A possible output is
245
246.. code-block:: none
247
248 d o n o n o d n o o
249 d o d n n o d d n o
250 o d d n o n d n o n
251 o d d d o n n o n n
252 d d n o d d n o d d
253 n n o d d d o d d d
254 n n o d d d o d d d
255 ----------
256
257There is an alternate form of the regular constraint
258:mzn:`regular_nfa` which specifies the regular
259expression using an NFA (without :math:`\epsilon` arcs).
260This constraint has the form
261
262.. code-block:: minizinc
263
264 regular_nfa(array[int] of var int: x, int: Q, int: S,
265 array[int,int] of set of int: d, int: q0, set of int: F)
266
267It constrains that
268the sequence of values in array :mzn:`x` (which must all be in the range
269:mzn:`1..S`)
270is accepted by the :index:`NFA` of :mzn:`Q` states with input :mzn:`1..S`
271and transition function :mzn:`d` (which maps :mzn:`<1..Q, 1..S>` to
272subsets of :mzn:`1..Q`) and initial state
273:mzn:`q0` (which must be in :mzn:`1..Q`) and accepting states :mzn:`F`
274(which all must be in :mzn:`1..Q`).
275There is no need for a failing state 0, since the transition function can
276map to an empty set of states.
277
278
279Defining Predicates
280-------------------
281
282.. index::
283 single: predicate; definition
284
285One of the most powerful modelling features
286of MiniZinc is the ability for
287the modeller to define their own high-level constraints. This allows them to
288abstract and modularise their model. It also allows re-use of constraints in
289different models and allows the development of application specific
290libraries defining the standard constraints and types.
291
292
293.. literalinclude:: examples/jobshop2.mzn
294 :language: minizinc
295 :name: ex-jobshop2
296 :caption: Model for job shop scheduling using predicates (:download:`jobshop2.mzn <examples/jobshop2.mzn>`)
297
298We start with a simple example, revisiting the job shop scheduling problem
299from the previous section. The model is shown in
300:numref:`ex-jobshop2`. The item of interest is the
301:mzn:`predicate`
302item:
303
304.. literalinclude:: examples/jobshop2.mzn
305 :language: minizinc
306 :lines: 12-13
307
308This defines a new constraint that enforces that a task with start time
309:mzn:`s1` and duration :mzn:`d1` does not overlap with a task with start
310time :mzn:`s2` and duration :mzn:`d2`. This can now be used inside the
311model anywhere any other :index:`Boolean expression <expression; Boolean>`
312(involving decision variables)
313can be used.
314
315As well as predicates the modeller can define new constraints that only
316involve parameters. These are useful to write fixed tests for a
317conditional expression. These are defined using the keyword :mzn:`test`.
318For example
319
320.. code-block:: minizinc
321
322 test even(int:x) = x mod 2 = 0;
323
324.. \ignore{ % for capture for testing!
325.. $ mzn-g12fd jobshop2.mzn jobshop.dzn
326.. } % $
327
328.. defblock:: Predicate definitions
329
330 .. index::
331 single: predicate; definition
332
333 Predicates are defined by a statement of the form
334
335 .. code-block:: minizincdef
336
337 predicate <pred-name> ( <arg-def>, ..., <arg-def> ) = <bool-exp>
338
339 The :mzndef:`<pred-name>` must be a valid MiniZinc identifier, and
340 each :mzndef:`<arg-def>` is a valid MiniZinc :index:`type` declaration.
341
342 .. \ignore{The type-insts\index{type-inst}
343 .. of arguments may include type-inst variables\index{type-inst!variable}
344 .. which are of the
345 .. form \texttt{\$T} or \texttt{any \$T} with \texttt{T} an identifier. A type-inst
346 .. variable \texttt{\$T}\ttindexdef{\$T}
347 .. can match any fixed type-inst, whereas a type-inst
348 .. variable \texttt{any \$T} can
349 .. also match non-fixed type-insts\index{type-index!non-fixed}
350 .. (such as \texttt{var int}).
351 .. Because predicate arguments\index{argument}
352 .. receive an assignment when calling the predicate, the
353 .. argument type-insts may include
354 .. implicitly indexed arrays\index{array!index set!implicit},
355 .. as well as set variables with a
356 .. non-finite element type.}
357
358 One relaxation of :index:`argument`
359 definitions is that the index types for arrays
360 can be :index:`unbounded <array; index set; unbounded>`, written :mzn:`int`.
361
362 .. code-block:: minizincdef
363
364 test <pred-name> ( <arg-def>, ..., <arg-def> ) = <bool-exp>
365
366 The :mzndef:`<bool-exp>` of the body must be fixed.
367
368 We also introduce a new form of the :mzn:`assert` command for use in
369 predicates.
370
371 .. code-block:: minizincdef
372
373 assert ( <bool-exp>, <string-exp>, <exp> )
374
375 The type of the :mzn:`assert`
376 :index:`expression <expression; assert>`
377 is the same as the type of the
378 last argument.
379 The :mzn:`assert` expression checks whether the first argument is false,
380 and if so prints the second argument string. If the first argument is true
381 it returns the third argument.
382
383Note that :index:`assert expressions <expression; assert>`
384are lazy in the third argument, that is if the
385first argument is false they will not be evaluated.
386Hence, they can be used for checking:
387
388.. code-block:: minizinc
389
390 predicate lookup(array[int] of var int:x, int: i, var int: y) =
391 assert(i in index_set(x), "index out of range in lookup",
392 y = x[i]
393 );
394
395This code will not evaluate :mzn:`x[i]` if :mzn:`i` is out of the range of the array
396:mzn:`x`.
397
398Defining Functions
399------------------
400
401.. index::
402 single: function; definition
403
404Functions are defined in MiniZinc
405similarly to predicates, but with a more
406general return type.
407
408The function below defines the index in a Sudoku matrix
409of the :math:`a1^{th}` row (or column) of the :math:`a^{th}` subsquare.
410
411.. code-block:: minizinc
412
413 function int: posn(int: a, int: a1) = (a-1) * S + a1;
414
415With this definition we can replace the last constraint in the
416Sudoku problem shown in :numref:`ex-sudoku` by
417
418.. code-block:: minizinc
419
420 constraint forall(a, o in SubSquareRange)(
421 alldifferent([ puzzle [ posn(a,a1), posn(o,o1) ] |
422 a1, o1 in SubSquareRange ] ) );
423
424Functions are useful for encoding complex expressions that
425are used frequently in the model. For example, imagine
426placing the numbers 1 to :math:`n` in different positions
427in an :math:`n \times n` grid such that
428the Manhattan distance between any two numbers :math:`i` and :math:`j`
429is greater than the maximum of the two numbers minus 1.
430The aim is to minimize the total of the Manhattan distances
431between the pairs. The Manhattan distance function
432can be expressed as:
433
434.. literalinclude:: examples/manhattan.mzn
435 :language: minizinc
436 :lines: 12-14
437
438The complete model is shown in :numref:`ex-manhattan`.
439
440
441.. literalinclude:: examples/manhattan.mzn
442 :language: minizinc
443 :name: ex-manhattan
444 :caption: Model for a number placement problem illustrating the use of functions (:download:`manhattan.mzn <examples/manhattan.mzn>`).
445
446.. defblock:: Function definitions
447
448 .. index::
449 single: function; definition
450
451 Functions are defined by a statement of the form
452
453 .. code-block:: minizincdef
454
455 function <ret-type> : <func-name> ( <arg-def>, ..., <arg-def> ) = <exp>
456
457 The :mzndef:`<func-name>` must be a valid MiniZinc identifier, and
458 each :mzndef:`<arg-def>` is a valid MiniZinc type declaration.
459 The :mzndef:`<ret-type>` is the return type of the function which must be
460 the type of :mzndef:`<exp>`. Arguments have the same restrictions as in
461 predicate definitions.
462
463Functions in MiniZinc can have any return type, not just fixed
464return types.
465Functions are useful for defining and documenting complex expressions that
466are used multiple times in a model.
467
468
469Reflection Functions
470--------------------
471
472To help write generic tests and predicates, various reflection functions
473return information about array index sets, var set domains and decision
474variable ranges. Those for index sets are
475:mzndef:`index_set(<1-D array>)`,
476:mzndef:`index_set_1of2(<2-D array>)`,
477:mzndef:`index_set_2of2(<2-D array>)`,
478and so on for higher
479dimensional arrays.
480
481A better model of the job shop conjoins all the non-overlap constraints for a
482single machine into a single disjunctive constraint.
483An advantage of this approach is that while we may initially model this
484simply as a conjunction of :mzn:`non-overlap` constraints, if the underlying solver has a
485better approach to solving disjunctive constraints we can use that instead,
486with minimal changes to our model. The model is shown in
487:numref:`ex-jobshop3`.
488
489
490.. literalinclude:: examples/jobshop3.mzn
491 :language: minizinc
492 :name: ex-jobshop3
493 :caption: Model for job shop scheduling using ``disjunctive`` predicate (:download:`jobshop3.mzn <examples/jobshop3.mzn>`).
494
495.. index::
496 single: global constraint; disjunctive
497
498The :mzn:`disjunctive`
499constraint takes an array of start times for each
500task and an array of their durations and makes sure that only one task is
501active at any one
502time. We define the disjunctive constraint as a :index:`predicate <predicate; definition>` with
503signature
504
505.. code-block:: minizinc
506
507 predicate disjunctive(array[int] of var int:s, array[int] of int:d);
508
509We can use the disjunctive constraint to define the non-overlap of tasks as
510shown in :numref:`ex-jobshop3`.
511We assume a definition for the :mzn:`disjunctive` predicate is given
512by the file :download:`disjunctive.mzn <examples/disjunctive.mzn>` which is included in the model.
513If the underlying system
514supports :mzn:`disjunctive` directly, it will include a file
515:download:`disjunctive.mzn <examples/disjunctive.mzn>` in its globals directory (with contents
516just the signature definition above).
517If the system we are using does not support disjunctive directly
518we can give our own definition by creating the file
519:download:`disjunctive.mzn <examples/disjunctive.mzn>`.
520The simplest implementation simply makes use of the :mzn:`no_overlap`
521predicate defined above.
522A better implementation is to make use of a global :mzn:`cumulative`
523constraint assuming it is supported by the underlying solver.
524:numref:`ex-disj` shows an implementation of :mzn:`disjunctive`.
525Note how we use the :mzn:`index_set` reflection function to
526(a) check that the arguments to :mzn:`disjunctive` make sense,
527and (b) construct the array of resource utilisations of the appropriate
528size for :mzn:`cumulative`.
529Note also that we use a ternary version of :mzn:`assert` here.
530
531.. literalinclude:: examples/disjunctive.mzn
532 :language: minizinc
533 :name: ex-disj
534 :caption: Defining a ``disjunctive`` predicate using ``cumulative`` (:download:`disjunctive.mzn <examples/disjunctive.mzn>`).
535
536.. \ignore{ % for capture for testing!
537.. $ mzn-g12fd jobshop3.mzn jobshop.dzn
538.. } % $
539
540
541
542Local Variables
543---------------
544
545.. index::
546 single: variable; local
547 single: let
548
549It is often useful to introduce *local variables* in a predicate,
550function
551or test.
552The :mzn:`let` expression allows you to do so.
553It can be used to introduce
554both decision :index:`variables <variable>`
555and
556:index:`parameters <parameter>`,
557but parameters must be initialised. For example:
558
559.. code-block:: minizinc
560
561 var s..e: x;
562 let {int: l = s div 2; int: u = e div 2; var l .. u: y;} in x = 2*y
563
564introduces parameters :mzn:`l` and :mzn:`u` and variable :mzn:`y`.
565While most useful in :index:`predicate`, :index:`function`
566and test definitions,
567:mzn:`let` expressions can also be used in other expressions, for example
568for eliminating common subexpressions:
569
570.. code-block:: minizinc
571
572 constraint let { var int: s = x1 + x2 + x3 + x4 } in
573 l <= s /\ s <= u;
574
575Local variables can be used anywhere and can be quite useful
576for simplifying complex expressions.
577:numref:`ex-wedding2`
578gives a revised version of the wedding model, using local variables to
579define the :index:`objective` function,
580rather than adding lots of variables
581to the model explicitly.
582
583.. literalinclude:: examples/wedding2.mzn
584 :language: minizinc
585 :name: ex-wedding2
586 :caption: Using local variables to define a complex objective function (:download:`wedding2.mzn <examples/wedding2.mzn>`).
587
588Using :mzn:`let` expressions, it is possible to define a function whose result is not well-defined. For example, we could write the following:
589
590.. code-block:: minizinc
591
592 function var int: x_or_x_plus_1(var int: x) = let {
593 var 0..1: y;
594 } in x+y; % result is not well-defined!
595
596The result, :mzn:`x+y`, is indeed not functionally defined by the argument of the function, :mzn:`x`. The MiniZinc compiler does not detect this, and **the behaviour of the resulting model is undefined**. In particular, calling this function twice with the same argument may or may not return the same result. It is therefore important to make sure that any function you define is indeed a function! **If you need non-deterministic behaviour, use a predicate:**
597
598.. code-block:: minizinc
599
600 predicate x_or_x_plus_1(var int: x, var int: z) = let {
601 var 0..1: y;
602 } in z=x+y;
603
604.. _pred-context:
605
606Context
607-------
608
609.. index::
610 single: context
611 single: context; negative
612 single: predicate
613 single: function
614
615One limitation is that predicates and functions
616containing decision variables that are not
617initialised in the declaration cannot be used inside a negative
618context.
619The following is illegal:
620
621.. code-block:: minizinc
622
623 predicate even(var int:x) =
624 let { var int: y } in x = 2 * y;
625
626 constraint not even(z);
627
628The reason for this is that solvers only solve existentially constrained
629problems, and if we introduce a local variable in a negative context, then
630the variable is *universally quantified* and hence out of scope of the
631underlying solvers. For example the :math:`\neg \mathit{even}(z)` is equivalent to
632:math:`\neg \exists y. z = 2y` which is equivalent to
633:math:`\forall y. z \neq 2y`.
634
635If local variables are given values, then they can be used in negative
636contexts. The following is legal
637
638.. code-block:: minizinc
639
640 predicate even(var int:x) =
641 let { var int: y = x div 2; } in x = 2 * y;
642
643 constraint not even(z);
644
645Note that the meaning of :mzn:`even` is correct, since if :mzn:`x` is even
646then :math:`x = 2 * (x ~\mbox{div}~ 2)`. Note that for this definition
647:math:`\neg \mathit{even}(z)` is equivalent to
648:math:`\neg \exists y. y = z ~\mbox{div}~ 2 \wedge z = 2y` which is equivalent to
649:math:`\exists y. y = z ~\mbox{div}~ 2 \wedge \neg z \neq 2y`, because :math:`y` is
650functionally defined by :math:`z`.
651
652
653Every expression in MiniZinc appears in one of the four
654*contexts*: :index:`root <context; !root>`, :index:`positive <context; !positive>`,
655:index:`negative <context; !negative>`,
656or :index:`mixed <context; !mixed>`.
657The context of a non-Boolean expression is simply the context of its nearest
658enclosing Boolean expression. The one exception is that the objective
659expression appears in a root context (since it has no enclosing Boolean expression).
660
661For the purposes of defining contexts we assume implication expressions
662:mzn:`e1 -> e2` are rewritten equivalently as :mzn:`not e1 \/ e2`,
663and similarly :mzn:`e1 <- e2` is rewritten as :mzn:`e1 \/ not e2`.
664
665The context for a Boolean expression is given by:
666
667root
668 root context is the context for any expression :mzn:`e` appearing as
669 the argument of :mzn:`constraint` or as an
670 :index:`assignment` item, or appearing as a sub expression :mzn:`e1`
671 or :mzn:`e2` in an expression :mzn:`e1 /\ e2` occurring in a root context.
672
673 Root context Boolean expressions must hold in any model of the problem.
674
675positive
676 positive context is the context for any expression
677 appearing as a sub expression :mzn:`e1`
678 or :mzn:`e2` in an expression :mzn:`e1 \/ e2` occurring in a root
679 or positive context,
680 appearing as a sub expression :mzn:`e1`
681 or :mzn:`e2` in an expression :mzn:`e1 /\ e2` occurring in a positive context,
682 or appearing as a sub expression :mzn:`e` in an expression
683 :mzn:`not e` appearing in a negative context.
684
685 Positive context Boolean expressions need not hold in a model, but
686 making them hold will only increase the possibility that the enclosing
687 constraint holds. A positive context expression has an even number of
688 negations in the path from the enclosing root context to the expression.
689
690negative
691 negative context is the context for any expression appearing as a sub expression :mzn:`e1`
692 or :mzn:`e2` in an expression :mzn:`e1 \/ e2` or :mzn:`e1 /\ e2` occurring in a negative context,
693 or appearing as a sub expression :mzn:`e` in an expression
694 :mzn:`not e` appearing in a positive context.
695
696 Negative context Boolean expressions need not hold in a model, but
697 making them false will increase the possibility that the enclosing
698 constraint holds. A negative context expression has an odd number of
699 negations in the path from the enclosing root context to the expression.
700
701mixed
702 mixed context is the context for any Boolean expression appearing
703 as a subexpression :mzn:`e1` or :mzn:`e2` in :mzn:`e1 <-> e2`, :mzn:`e1 = e2`, or :mzn:`bool2int(e)`.
704
705 Mixed context expression are effectively both positive and
706 negative. This can be seen from the fact that :mzn:`e1 <-> e2` is equivalent
707 to :mzn:`(e1 /\ e2) \/ (not e1 /\ not e2)` and
708 :mzn:`x = bool2int(e)` is equivalent to :mzn:`(e /\ x=1) \/ (not e /\ x=0)`.
709
710Consider the code fragment
711
712.. code-block:: minizinc
713
714 constraint x > 0 /\ (i <= 4 -> x + bool2int(x > i) = 5);
715
716then :mzn:`x > 0` is in the root context, :mzn:`i <= 4}` is in a negative
717context,
718:mzn:`x + bool2int(x > i) = 5`
719is in a positive context, and :mzn:`x > i` is in a mixed context.
720
721
722
723Local Constraints
724-----------------
725
726.. index::
727 single: constraint; local
728
729Let expressions can also be used to include local constraints,
730usually to constrain the behaviour of local variables.
731For example, consider defining an integer square root function making use
732of only multiplication:
733
734.. code-block:: minizinc
735
736 function var int: mysqrt(var int:x) =
737 let { var 0..infinity: y;
738 constraint x = y * y; } in y;
739
740The local constraints ensure
741:mzn:`y` takes the correct value; which is then returned
742by the function.
743
744Local constraints can be used in any let expression,
745though the most common
746usage is in defining functions.
747A function with local constraints is often *partial*, which means that it is not defined for all possible inputs. For example, the :mzn:`mysqrt` function above constrains its argument :mzn:`x` to take a value that is in fact the square of an integer. The MiniZinc compiler handles these cases according to the *relational semantics*, which means that the result of applying a partial function may become false in its enclosing Boolean context. For example, consider the following model:
748
749.. code-block:: minizinc
750
751 var 1..9: x;
752 var 0..9: y;
753 constraint (x=3 /\ y=0) \/ y = mysqrt(x);
754
755Clearly, the intention of the modeller is that :mzn:`x=3, y=0` should be a solution. This requires the compiler to take care not to "lift" the constraint :mzn:`x=y*y` out of the context of the function, because that would prevent it from finding any solution with :mzn:`x=3`. You can verify that the set of solutions contains :mzn:`x=3, y=0` as well as the expected :mzn:`x=1, y=1`, :mzn:`x=4, y=2` and :mzn:`x=9, y=3`.
756
757If you define a *total* function using local constraints, you can give the compiler a hint that allows it to produce more efficient code. For example, you could write the square function (not square root, note the subtle difference) as follows:
758
759.. code-block:: minizinc
760
761 function var int: mysqr(var int:x) ::promise_total =
762 let { var 0..infinity: y;
763 constraint y = x * x; } in y;
764
765This function is indeed defined for any input value :mzn:`x`. The :mzn:`::promise_total` annotation tells the compiler that it can safely lift all local constraints out of the context of the function call.
766
767.. defblock:: Let expressions
768
769 .. index::
770 single: expression; let
771
772 :index:`Local variables <variable;local>`
773 can be introduced in any expression with a *let expression*
774 of the form:
775
776 .. code-block:: minizincdef
777
778 let { <dec>; ... <dec> ; } in <exp>
779
780 The declarations :mzndef:`<dec>`
781 can be declarations of decision variables and
782 parameters (which must be initialised) or constraint items.
783 No declaration can make use of a newly declared variable
784 before it is introduced.
785
786 Note that local variables and constraints
787 cannot occur in tests.
788 Local variables cannot occur in predicates
789 or functions that appear in a
790 :index:`negative <context; negative>` or :index:`mixed <context; mixed>` context,
791 unless the variable is defined by an expression.
792
793
794Domain Reflection Functions
795---------------------------
796
797.. index::
798 single: domain; reflection
799
800Other important reflection functions are those that allow us to access
801the domains of variables. The expression :mzn:`lb(x)`
802returns
803a value that is lower than or equal to any value that :mzn:`x` may take in
804a solution of the problem. Usually it will just be the
805declared lower :index:`bound <variable; bound>` of :mzn:`x`.
806If :mzn:`x` is declared as a non-finite type, e.g.
807simply :mzn:`var int`
808then it is an error.
809Similarly the expression :mzn:`dom(x)`
810returns a (non-strict)
811superset of the possible values of :mzn:`x` in any solution of the problem.
812Again it is usually the declared values, and again if it is not
813declared as finite then there is an error.
814
815.. \ignore{ % for capture for testing!
816.. $ mzn-g12fd reflection.mzn
817.. } % $
818
819
820.. literalinclude:: examples/reflection.mzn
821 :language: minizinc
822 :name: ex-reflect
823 :caption: Using reflection predicates (:download:`reflection.mzn <examples/reflection.mzn>`).
824
825For example, the model show in :numref:`ex-reflect`
826may output
827
828.. code-block:: none
829
830 y = -10
831 D = -10..10
832 ----------
833
834or
835
836.. code-block:: none
837
838 y = 0
839 D = {0, 1, 2, 3, 4}
840 ----------
841
842or any answer with
843:math:`-10 \leq y \leq 0` and
844:math:`\{0, \ldots, 4\} \subseteq D \subseteq \{-10, \ldots, 10\}`.
845
846Variable domain reflection expressions should be used in a manner where they are
847correct for any safe approximations, but note this is not checked!
848For example the additional code
849
850.. code-block:: minizinc
851
852 var -10..10: z;
853 constraint z <= y;
854
855is not a safe usage of the domain information.
856Since using the tighter (correct) approximation leads to
857more solutions than the weaker initial approximation.
858
859.. TODO: this sounds wrong!
860
861.. defblock:: Domain reflection
862
863 .. index::
864 single: domain; reflection
865
866 There are reflection functions to interrogate
867 the possible values of expressions containing variables:
868
869 - :mzndef:`dom(<exp>)`
870 returns a safe approximation to the possible values of the expression.
871 - :mzndef:`lb(<exp>)`
872 returns a safe approximation to the lower bound value of the expression.
873 - :mzndef:`ub(<exp>)`
874 returns a safe approximation to the upper bound value of the expression.
875
876 The expressions for :mzn:`lb` and :mzn:`ub`
877 can only be of types :mzn:`int`, :mzn:`bool`,
878 :mzn:`float` or :mzn:`set of int`.
879 For :mzn:`dom` the type cannot be :mzn:`float`.
880 If one of the variables appearing in :mzndef:`<exp>` has a
881 :index:`non-finite declared type <type; non-finite>`
882 (e.g. :mzn:`var int` or :mzn:`var float`)
883 then an error can occur.
884
885 There are also versions that work directly on arrays of expressions (with
886 similar restrictions):
887
888 - :mzndef:`dom_array(<array-exp>)`:
889 returns a safe approximation to the union of all
890 possible values of the expressions appearing in the array.
891 - :mzndef:`lb_array(<array-exp>)`
892 returns a safe approximation to the lower bound of all expressions appearing
893 in the array.
894 - :mzndef:`ub_array(<array-exp>)`
895 returns a safe approximation to the upper bound of all expressions appearing
896 in the array.
897
898The combinations of predicates, local variables and domain reflection
899allows the definition of complex global constraints by decomposition.
900We can define the time based decomposition
901of the :mzn:`cumulative`
902constraint using the code shown in :numref:`ex-cumul`.
903
904.. literalinclude:: examples/cumulative.mzn
905 :language: minizinc
906 :name: ex-cumul
907 :caption: Defining a ``cumulative`` predicate by decomposition (:download:`cumulative.mzn <examples/cumulative.mzn>`).
908
909The decomposition uses :mzn:`lb` and :mzn:`ub` to determine
910the set of times :mzn:`times` over which tasks could range.
911It then asserts for each time :mzn:`t` in :mzn:`times` that the
912sum of resources for the active tasks at time :mzn:`t` is less than
913the bound :mzn:`b`.
914
915Scope
916-----
917
918.. index::
919 single: scope
920
921It is worth briefly mentioning the scope of declarations in MiniZinc.
922MiniZinc has a single namespace, so all variables appearing
923in declarations are visible in every expression in the model.
924MiniZinc introduces locally scoped
925variables in a number of ways:
926
927- as :index:`iterator <variable; iterator>`
928 variables in :index:`comprehension` expressions
929- using :mzn:`let` expressions
930- as predicate and function :index:`arguments <argument>`
931
932Any local scoped variable overshadows the outer scoped variables
933of the same name.
934
935.. literalinclude:: examples/scope.mzn
936 :language: minizinc
937 :name: ex-scope
938 :caption: A model for illustrating scopes of variables (:download:`scope.mzn <examples/scope.mzn>`).
939
940For example, in the model shown in :numref:`ex-scope`
941the :mzn:`x` in :mzn:`-x <= y` is the global :mzn:`x`,
942the :mzn:`x` in
943:mzn:`smallx(x)` is the iterator :mzn:`x in 1..u`,
944while the :mzn:`y` in the disjunction is the second
945argument of the predicate.