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. 946