this repo has no description
dekker.one
1.. index::
2 single: predicate
3 single: function
4
5.. _sec-predicates:
6
7Predicados y Funciones
8======================
9
10Los predicados en MiniZinc nos permiten capturar restricciones complejas de nuestro modelo de manera sucinta. Los predicados en MiniZinc se utilizan para modelar con restricciones globales predefinidas y para capturar y definir nuevas restricciones complejas por el modelador.
11
12Las funciones son usadas en MiniZinc para capturar estructuras comunes de modelos. De hecho, un predicado es solo una función con tipo de salida :mzn:`var bool`.
13
14
15.. _sec-globals:
16
17Restricciones Globales
18----------------------
19
20.. index::
21 single: global constraint
22
23Hay muchas restricciones globales definidas en MiniZinc para su uso en el modelado.
24La lista definitiva se encuentra en la documentación de la versión de liberación (release), ya que la lista está creciendo lentamente.
25A continuación discutimos algunas de las restricciones globales más importantes.
26
27
28
29Alldifferent
30~~~~~~~~~~~~
31
32.. index::
33 single: alldifferent
34 single: global constraint; alldifferent
35
36La restricción :mzn:`alldifferent` toma una matriz de variables y las restringe para tomar valores diferentes.
37Un uso de :mzn:`alldifferent` tiene la forma
38
39.. code-block:: minizinc
40
41 alldifferent(array[int] of var int: x)
42
43El argumento es una matriz de variables enteras.
44
45La restricción :mzn:`alldifferent` es una de las restricciones globales más estudiadas y utilizadas en la programación de restricciones. Se usa para definir subproblemas de asignación y existen propagadores globales eficientes para :mzn:`alldifferent`.
46Los modelos :download:`send-more-money_es.mzn <examples/send-more-money_es.mzn>` (:numref:`ex-smm`) y :download:`sudoku_es.mzn <examples/sudoku_es.mzn>` (:numref:`ex-sudoku`) son ejemplos de modelos que usan :mzn:`alldifferent`.
47
48
49
50Cumulative
51~~~~~~~~~~
52
53.. index::
54 single: cumulative
55 single: global constraint; cumulative
56
57La restricción :mzn:`cumulative` se usa para describir el uso acumulado de recursos.
58
59.. code-block:: minizinc
60
61 cumulative(array[int] of var int: s, array[int] of var int: d,
62 array[int] of var int: r, var int: b)
63
64Requiere que un conjunto de tareas proporcionadas por las horas de inicio :mzn:`s`, duraciones :mzn:`d` y requisitos de recursos :mzn:`r`, nunca requiera más que un límite global de recursos :mzn:`b` en cualquier momento.
65
66.. literalinclude:: examples/moving_es.mzn
67 :language: minizinc
68 :name: ex-moving
69 :caption: Modelo para mover muebles usando ``cumulative`` (:download:`moving_es.mzn <examples/moving_es.mzn>`).
70
71.. literalinclude:: examples/moving_es.dzn
72 :language: minizinc
73 :name: ex-movingd
74 :caption: Datos para mover muebles usando ``cumulative`` (:download:`moving_es.dzn <examples/moving_es.dzn>`).
75
76El modelo en :numref:`ex-moving` encuentra un cronograma para mover los muebles de modo que cada mueble tenga suficientes manipuladores (personas) y suficientes carritos disponibles durante el movimiento. Se proporciona el tiempo disponible, los manipuladores y los carros, y los datos proporcionan para cada objeto la duración del movimiento, el número de manipuladores y la cantidad de carros requeridos.
77
78Usando los datos mostrados en :mzn:`ex-movingd`, el comando
79
80.. code-block:: bash
81
82 $ mzn-gecode moving_es.mzn moving_es.dzn
83
84Puede dar como resultado la salida
85
86.. code-block:: none
87
88 start = [0, 60, 60, 90, 120, 0, 15, 105]
89 end = 140
90 ----------
91 ==========
92
93:numref:`fig-histogram-a` y :numref:`fig-histogram-b` muestra los requisitos para manipuladores y carros en cada momento del movimiento para esta solución.
94
95.. _fig-histogram-a:
96
97.. figure:: figures/handlers_es.*
98
99 Histograma de uso de los manipuladores en movimiento.
100
101.. _fig-histogram-b:
102
103.. figure:: figures/trolleys_es.*
104
105 Histograma de uso de carritos en el movimiento.
106
107Table
108~~~~~
109
110.. index::
111 single: table
112 single: global constraint; table
113
114La restricción :mzn:`table` impone que una tupla de variables tome un valor de un conjunto de tuplas. Como no hay tuplas en MiniZinc, esto se codifica utilizando matrices.
115
116El uso de :mzn:`table` tiene una de las formas
117
118.. code-block:: minizinc
119
120 table(array[int] of var bool: x, array[int, int] of bool: t)
121 table(array[int] of var int: x, array[int, int] of int: t)
122
123Dependiendo de si las tuplas son booleanas o enteras.
124
125La restricción impone :math:`x \in t` donde consideramos :math:`x` y cada fila en :math:`t` para ser una tupla, y :math:`t` para ser un conjunto de tuplas.
126
127.. literalinclude:: examples/meal_es.mzn
128 :language: minizinc
129 :name: ex-meal
130 :caption: Modelo para la planificación de comidas usando la restricción ``table`` (:download:`meal_es.mzn <examples/meal_es.mzn>`).
131
132.. literalinclude:: examples/meal_es.dzn
133 :language: minizinc
134 :name: ex-meald
135 :caption: Datos para la planificación de comidas que definen la tabla ``table`` usada (:download:`meal_es.dzn <examples/meal_es.dzn>`).
136
137El modelo en :numref:`ex-meal` busca comidas balanceadas.
138Cada elemento de comida tiene un nombre (codificado como un entero), un kilojulio, proteínas en gramos, sal en miligramos y grasa en gramos, así como un costo en centavos. La relación entre estos elementos se codifica utilizando una restricción :mzn:`table`.
139El modelo busca una comida de costo mínimo que tenga un recuento mínimo de kilojulios :mzn:`min_energy`, una cantidad mínima de proteína :mzn:`min_protein`, cantidad máxima de sal :mzn:`max_salt` y grasa :mzn:`max_fat`.
140
141
142Regular
143~~~~~~~
144
145.. index::
146 single: regular
147 single: global constraint; regular
148
149La restricción :mzn:`regular` se usa para exigir que una secuencia de variables tome un valor definido por un autómata finito.
150El uso de :mzn:`regular` tiene la forma
151
152
153.. code-block:: minizinc
154
155 regular(array[int] of var int: x, int: Q, int: S,
156 array[int,int] of int: d, int: q0, set of int: F)
157
158Restringe que la secuencia de valores en array :mzn:`x` (que debe estar en el :index:`range` :mzn:`1..S`) es aceptado por el :index:`DFA` de :mzn:`Q` estados con entrada :mzn:`1..S` y función de transición :mzn:`d` (que asigna :mzn:`<1..Q, 1..S>` a :mzn:`0..Q`) y el estado inicial :mzn:`q0` (que debe estar en :mzn:`1..Q`) y estados de aceptación :mzn:`F` (que deben estar todos en :mzn:`1..Q`).
159
160El estado 0 está reservado para ser un estado siempre fallido.
161
162.. _fig-dfa:
163
164.. figure:: figures/dfa.*
165
166 Un DFA determina las listas correctas.
167
168Considere un problema de lista de enfermeras. Cada enfermera está programada para cada día como:
169(d) en el turno de día,
170(n) en el turno de noche, o
171(o) para ninguno.
172En cada período de cuatro días, una enfermera debe tener al menos un día libre y ninguna enfermera puede programar 3 turnos nocturnos seguidos.
173Esto se puede codificar utilizando el DFA incompleto que se muestra en :numref:`fig-dfa`.
174Podemos codificar este DFA teniendo como estado de inicial :mzn:`1`, los estados finales :mzn:`1..6`, y la función de transición.
175
176.. cssclass:: table-nonfluid table-bordered
177
178+---+---+---+---+
179| | d | n | o |
180+===+===+===+===+
181| 1 | 2 | 3 | 1 |
182+---+---+---+---+
183| 2 | 4 | 4 | 1 |
184+---+---+---+---+
185| 3 | 4 | 5 | 1 |
186+---+---+---+---+
187| 4 | 6 | 6 | 1 |
188+---+---+---+---+
189| 5 | 6 | 0 | 1 |
190+---+---+---+---+
191| 6 | 0 | 0 | 1 |
192+---+---+---+---+
193
194Tenga en cuenta que el estado 0 en la tabla indica un estado de error.
195El modelo que se muestra en :numref:`ex-nurse` encuentra un cronograma para :mzn:`num_nurses` enfermeras sobre el :mzn:`num_days` días, donde requerimos :mzn:`req_day` enfermeras en el turno de día cada día, y enfermeras :mzn:`req_night` en el turno de noche. Cada cada enfermera toma al menos :mzn:`min_night` turnos nocturnos.
196
197.. literalinclude:: examples/nurse_es.mzn
198 :language: minizinc
199 :name: ex-nurse
200 :caption: Modelo para la formación de la enfermera usando la restricción ``regular`` (:download:`nurse_es.mzn <examples/nurse_es.mzn>`)
201
202Ejecutando el comando
203
204.. code-block:: bash
205
206 $ mzn-gecode nurse_es.mzn nurse_es.dzn
207
208Encuentra un horario de 10 días para 7 enfermeras, que requiere 3 en cada turno de día y 2 en cada turno de noche, con un mínimo de 2 turnos de noche por enfermera.
209Un posible resultado es:
210
211.. code-block:: none
212
213 o d n n o n n d o o
214 d o n d o d n n o n
215 o d d o d o d n n o
216 d d d o n n d o n n
217 d o d n n o d o d d
218 n n o d d d o d d d
219 n n o d d d o d d d
220 ----------
221
222Hay una forma alternativa de la restricción regular :mzn:`regular_nfa` que especifica la expresión regular usando un NFA (sin arcos :mzn:`\epsilon` arcs).
223
224Esta restricción tiene la forma:
225
226.. code-block:: minizinc
227
228 regular_nfa(array[int] of var int: x, int: Q, int: S,
229 array[int,int] of set of int: d, int: q0, set of int: F)
230
231Se restringe que la secuencia de valores en la matriz :mzn:`x` (que debe estar en el rango :mzn:`1..S`) sea aceptada por el :index:`NFA` de :mzn:`Q` estados con entrada :mzn:`1..S` y una función de transición :mzn:`d` (que mapea :mzn:`<1..Q, 1..S>` a subconjuntos de :mzn:`1..Q`) y un estado inicial :mzn:`q0` (que debe estar en :mzn:`1..Q`) y estados de aceptación :mzn:`F` (todos deben estar en :mzn:`1..Q`).
232
233No es necesario un estado de falla 0, ya que la función de transición se puede asignar a un conjunto vacío de estados.
234
235
236
237Definición de Predicados
238------------------------
239
240.. index::
241 single: predicate; definition
242
243Una de las características de modelado más potentes de MiniZinc, es la capacidad del modelador para definir sus propias restricciones de alto nivel. Esto les permite abstraer y modularizar su modelo. También permite la reutilización de restricciones en diferentes modelos y permite el desarrollo de bibliotecas específicas de aplicaciones que definen los tipos y restricciones estándar.
244
245.. literalinclude:: examples/jobshop2_es.mzn
246 :language: minizinc
247 :name: ex-jobshop2
248 :caption: Modelo para la programación de taller de trabajo usando predicados (:download:`jobshop2_es.mzn <examples/jobshop2_es.mzn>`)
249
250Comenzamos con un ejemplo simple, revisando el problema de programación de la tienda de trabajo de la sección anterior. El modelo se muestra en :numref:`ex-jobshop2`. El elemento de interés es el elemento :mzn:`predicate`:
251
252.. literalinclude:: examples/jobshop2_es.mzn
253 :language: minizinc
254 :lines: 12-13
255
256Esto define una nueva restricción que impone que una tarea con hora de inicio :mzn:`s1` y duración :mzn:`d1` no se superpone con una tarea con hora de inicio :mzn:`s2` y duración :mzn:`d2`. Esto ahora se puede usar dentro del modelo en cualquier otro lugar :index:`Expresión booleana <expresión; Booleana>` (que involucra variables de decisión) donde se pueda usar.
257
258Además de los predicados, el modelador puede definir nuevas restricciones que solo involucran parámetros. Estos son útiles para escribir pruebas fijas para una expresión condicional. Estos se definen con la palabra clave :mzn:`test`.
259
260Por ejemplo:
261
262.. code-block:: minizinc
263
264 test even(int:x) = x mod 2 = 0;
265
266.. \ignore{ % for capture for testing!
267.. $ mzn-g12fd jobshop2_es.mzn jobshop_es.dzn
268.. } % $
269
270.. defblock:: Definiciones de Predicado
271
272 .. index::
273 single: predicate; definition
274
275 Los predicados se definen mediante una declaración con la forma
276
277 .. code-block:: minizincdef
278
279 predicate <pred-name> ( <arg-def>, ..., <arg-def> ) = <bool-exp>
280
281 El :mzndef:`<pred-name>` debe ser un identificador de MiniZinc válido, y cada uno de las :mzndef:`<arg-def>` es una válida declaración del :index:`type` en MiniZinc.
282
283
284 .. \ignore{The type-insts\index{type-inst}
285 .. of arguments may include type-inst variables\index{type-inst!variable}
286 .. which are of the
287 .. form \texttt{\$T} or \texttt{any \$T} with \texttt{T} an identifier. A type-inst
288 .. variable \texttt{\$T}\ttindexdef{\$T}
289 .. can match any fixed type-inst, whereas a type-inst
290 .. variable \texttt{any \$T} can
291 .. also match non-fixed type-insts\index{type-index!non-fixed}
292 .. (such as \texttt{var int}).
293 .. Because predicate arguments\index{argument}
294 .. receive an assignment when calling the predicate, the
295 .. argument type-insts may include
296 .. implicitly indexed arrays\index{array!index set!implicit},
297 .. as well as set variables with a
298 .. non-finite element type.}
299
300 Una relajación de las definiciones :index:`argument` es que los tipos de índice para matrices pueden ser :index:`unbounded <array; conjunto de índices; sin límites> `, escrito en :mzn:`int`.
301
302 .. code-block:: minizincdef
303
304 test <pred-name> ( <arg-def>, ..., <arg-def> ) = <bool-exp>
305
306 El :mzndef:`<bool-expo>` del cuerpo debe ser reparado.
307
308 También presentamos una nueva forma del comando :mzn:`assert` para usarlo en predicados.
309
310 .. code-block:: minizincdef
311
312 assert ( <bool-exp>, <string-exp>, <exp> )
313
314El tipo de :mzn:`assert` :index:`expression <expression; assert>` es el mismo que el tipo del último argumento.
315La expresión :mzn:`assert` verifica si el primer argumento es falso, y de ser así, imprime la segunda cadena de argumento. Si el primer argumento es verdadero, devuelve el tercer argumento.
316
317
318Tenga en cuenta que :index:`assert expressions <expression; assert>` son flojos (lazy) en el tercer argumento, es decir, si el primer argumento es falso, no serán evaluados.
319Por lo tanto, se pueden usar para verificar:
320
321.. code-block:: minizinc
322
323 predicate lookup(array[int] of var int:x, int: i, var int: y) =
324 assert(i in index_set(x), "index out of range in lookup"
325 y = x[i]
326 );
327
328This code will not evaluate :mzn:`x[i]` if :mzn:`i` is out of the range of the array :mzn:`x`.
329
330Este código no evaluará :mzn:`x[i]` si :mzn:`i` está fuera del rango de la matriz :mzn:`x`.
331
332
333
334Definiendo Funciones
335--------------------
336
337.. index::
338 single: function; definition
339
340Las funciones se definen en MiniZinc de manera similar a los predicados, pero con un tipo de retorno más general.
341
342La función siguiente define la fila en una matriz de Sudoku de la fila :math:`a1^{th}` de subcuadrados :math:`a^{th}`.
343
344.. code-block:: minizinc
345
346 function int: posn(int: a, int: a1) = (a-1) * S + a1;
347
348Con esta definición podemos reemplazar la última restricción en el problema de Sudoku que se muestra en :numref:`ex-sudoku` por:
349
350.. code-block:: minizinc
351
352 constraint forall(a, o in SubSquareRange)(
353 alldifferent([ puzzle [ posn(a,a0), posn(o,o1) ] |
354 a1,o1 in SubSquareRange ] ) );
355
356Las funciones son útiles para codificar expresiones complejas que se utilizan con frecuencia en el modelo. Por ejemplo, imagina colocando los números 1 en :math:`n` en diferentes posiciones en una grilla :math:`n \times n`, como la distancia de Manhattan entre dos números cualquiera :math:`i` y :math:`j` es mayor que el máximo de los dos números menos 1.
357
358El objetivo es minimizar el total de las distancias de Manhattan entre los pares. La función de distancia de Manhattan se puede expresar como:
359
360.. literalinclude:: examples/manhattan_es.mzn
361 :language: minizinc
362 :lines: 12-14
363
364El modelo completo se muestra en :numref:`ex-manhattan`.
365
366
367.. literalinclude:: examples/manhattan_es.mzn
368 :language: minizinc
369 :name: ex-manhattan
370 :caption: Modelo para un problema de ubicación numérica que ilustra el uso de funciones (:download:`manhattan_es.mzn <examples/manhattan_es.mzn>`).
371
372.. defblock:: Function definitions
373
374 .. index::
375 single: function; definition
376
377 Las funciones se definen mediante una declaración de la forma
378
379 .. code-block:: minizincdef
380
381 function <ret-type> : <func-name> ( <arg-def>, ..., <arg-def> ) = <exp>
382
383 El :mzndef:`<func-name>` debe ser un identificador MiniZinc válido, y cada uno de los :mzndef:`<arg-def>` es una declaración de tipo MiniZinc válida.
384 El :mzndef:`<ret-type>` es el tipo de retorno de la función que debe ser el tipo :mzndef:`<exp>`. Los argumentos tienen las mismas restricciones que en las definiciones de predicados.
385
386Funciones en MiniZinc pueden tener cualquier tipo de retorno, no solo tipos de retorno fijos.
387
388Las funciones son útiles para definir y documentar expresiones complejas que se usan varias veces en un modelo.
389
390
391Funciones de Reflexión
392----------------------
393
394
395Para ayudar a escribir pruebas genéricas y predicados, varias funciones de reflexión devuelven información sobre conjuntos de índices de matriz, dominios de conjuntos de variables y rangos de variables de decisión. Los de los conjuntos de índices son :mzndef:`index_set(<1-D array>)`, :mzndef:`index_set_1of2(<2-D array>)`, :mzndef:`index_set_2of2(<2-D array>)`, y así sucesivamente para matrices de mayor dimensión.
396
397Un mejor modelo de tienda de trabajo combina todas las restricciones no superpuestas para una sola máquina en una única restricción disyuntiva.
398Una ventaja de este enfoque es que si bien inicialmente podemos modelar esto simplemente como una conjunción de: restricciones :mzn:`non-overlap`, si el solucionador subyacente tiene un mejor enfoque para resolver las restricciones disyuntivas, podemos usar eso en su lugar, con cambios mínimos en nuestro modelo. El modelo se muestra en :numref:`ex-jobshop3`.
399
400.. literalinclude:: examples/jobshop3_es.mzn
401 :language: minizinc
402 :name: ex-jobshop3
403 :caption: Modelo para la programación de la tienda de trabajo usando un predicado ``disjunctive`` (:download:`jobshop3_es.mzn <examples/jobshop3_es.mzn>`).
404
405.. index::
406 single: global constraint; disjunctive
407
408La restricción :mzn:`disjunctive` toma una matriz de tiempos de inicio para cada tarea y una matriz de sus duraciones y se asegura de que solo una tarea esté activa en un momento dado. Definimos la restricción disyuntiva como un :index:`predicate <predicate; definition>` con firma
409
410.. code-block:: minizinc
411
412 predicate disjunctive(array[int] of var int:s, array[int] of int:d);
413
414Podemos usar la restricción disyuntiva para definir la no superposición de tareas como se muestra en :numref:`ex-jobshop3`.
415Suponemos una definición para el predicado :mzn:`disjunctive` está dada por el archivo :download:`disjunctive_es.mzn <examples/disjunctive_es.mzn>` que se incluye en el modelo.
416
417Si el sistema subyacente admite :mzn:`disjunctive` directamente, incluirá un archivo :download:`disjunctive_es.mzn <examples/disjunctive_es.mzn>` en su directorio global (con contenido solo la definición de firma anterior).
418
419
420Si el sistema que estamos utilizando no es compatible directamente con disyuntivo, podemos dar nuestra propia definición creando el archivo :download:`disjunctive_es.mzn <examples/disjunctive_es.mzn>`.
421
422La implementación más simple simplemente hace uso del predicado :mzn:`no_overlap` definido anteriormente.
423Una mejor implementación es hacer uso de una restricción global :mzn:`cumulative` asumiendo que sea compatible con el solucionador subyacente. :numref:`ex-disj` muestra una implementación de :mzn:`disjunctive`.
424
425Observe cómo usamos la función de reflexión :mzn:`index_set` para
426(a) verificar que los argumentos para :mzn:`disjunctive` tengan sentido, y
427(b) construir la matriz de utilizaciones de recursos del tamaño apropiado para :mzn:`cumulative`.
428Tenga en cuenta también que utilizamos una versión ternaria :mzn:`assert` aquí.
429
430.. literalinclude:: examples/disjunctive_es.mzn
431 :language: minizinc
432 :name: ex-disj
433 :caption: Definir un predicado ``disjunctive`` utilizando ``cumulative`` (:download:`disjunctive_es.mzn <examples/disjunctive_es.mzn>`).
434
435.. \ignore{ % for capture for testing!
436.. $ mzn-g12fd jobshop3_es.mzn jobshop_es.dzn
437.. } % $
438
439
440
441Variables Locales
442-----------------
443
444.. index::
445 single: variable; local
446 single: let
447
448
449A menudo es útil introducir *variables locales* en un predicado, función o prueba.
450La expresión :mzn:`let` te permite hacerlo.
451Se puede usar para introducir ambas decisiones :index:`variables <variable>` y :index:`parameters <parameter>`, pero los parámetros deben inicializarse. Por ejemplo:
452
453.. code-block:: minizinc
454
455 var s..e: x;
456 let {int: l = s div 2; int: u = e div 2; var l .. u: y;} in x = 2*y
457
458Introduce parámetros :mzn:`l`, :mzn:`u` y variable :mzn:`y`.
459
460Si bien es más útil en :index:`predicate`, :index:`function` y en las definiciones de prueba, las expresiones :mzn:`let` también se pueden usar en otras expresiones, por ejemplo para eliminar subexpresiones comunes:
461
462.. code-block:: minizinc
463
464 constraint let { var int: s = x1 + x2 + x3 + x4 } in
465 l <= s /\ s <= u;
466
467Las variables locales se pueden usar en cualquier lugar y pueden ser bastante útiles para simplificar expresiones complejas.
468:numref:`ex-wedding2` da una versión revisada del modelo de boda, usando variables locales para definir la función :index:`objective`, en lugar de agregar muchas variables al modelo explícitamente.
469
470.. literalinclude:: examples/wedding2_es.mzn
471 :language: minizinc
472 :name: ex-wedding2
473 :caption: Usar variables locales para definir una función objetivo compleja (:download:`wedding2_es.mzn <examples/wedding2_es.mzn>`).
474
475
476Contexto
477--------
478
479.. index::
480 single: context
481 single: context; negative
482 single: predicate
483 single: function
484
485Una limitación es que los predicados y las funciones que contienen variables de decisión que no se inicializan en la declaración no se pueden usar dentro de un contexto negativo.
486Lo siguiente es ilegal:
487
488.. code-block:: minizinc
489
490 predicate even(var int:x) =
491 let { var int: y } in x = 2 * y;
492
493 constraint not even(z);
494
495
496La razón de esto es que los solucionadores solo resuelven problemas existencialmente restringidos, y si introducimos una variable local en un contexto negativo, entonces la variable es *universalmente cuantificada*. Por lo tanto, fuera del alcance de los solucionadores subyacentes. Por ejemplo, :math:`\neg \mathit{even}(z)` es equivalente a :math:`\neg \exists y. z = 2y`, que es equivalente a :math:`\forall y. z \neq 2y`.
497
498Si las variables locales reciben valores, entonces pueden usarse en contextos negativos. Lo siguiente es legal:
499
500
501.. code-block:: minizinc
502
503 predicate even(var int:x) =
504 let { var int: y = x div 2; } in x = 2 * y;
505
506 constraint not even(z);
507
508
509Tenga en cuenta que el significado de :mzn:`even` es correcto, ya que si :mzn:`x` es par :math:`x = 2 * (x ~\mbox{div}~ 2)`.
510Tenga en cuenta que para esta definición :math:`\neg \mathit{even}(z)` es equivalente a :math:`\neg \exists y. y = z ~\mbox{div}~ 2 \wedge z = 2y` que es equivalente a :math:`\exists y. y = z ~\mbox{div}~ 2 \wedge \neg z \neq 2y`, porque :math:`y` se define funcionalmente por :math:`z`.
511
512Cada expresión en MiniZinc aparece en uno de los cuatro *contextos* :index:`root <context; !root>`, :index:`positive <context; !positive>`, :index:`negative <context; !negative>`, o :index:`mixed <context; !mixed>`.
513El contexto de una expresión no booleana es simplemente el contexto de su expresión booleana más cercana. La única excepción es que la expresión objetivo aparece en un contexto raíz (ya que no tiene una expresión booleana adjunta).
514
515Para los propósitos de definir contextos asumimos expresiones de implicación :mzn:`e1 -> e2` se reescriben de forma equivalente como :mzn:`not e1 \/ e2`, y de manera similar :mzn:`e1 <- e2` se reescribe como :mzn:`e1 \/ no e2`.
516
517El contexto para una expresión booleana viene dado por:
518
519Raíz:
520El contexto raíz es el contexto para cualquier expresión $e$ que aparece como el argumento de :mzn:`constraint` o como un elemento :index:`assignment`, o que aparece como una subexpresión :mzn:`e1` o :mzn:`e2` en una expresión :mzn:`e1 /\ e2` que ocurre en un contexto raíz.
521
522Las expresiones booleanas de contexto raíz deben mantenerse en cualquier modelo del problema.
523
524Positivo:
525Un contexto positivo es el contexto para cualquier expresión que aparece como una expresión secundaria :mzn:`e1` o :mzn:`e2` en una expresión :mzn:`e1 \/ e2` que ocurre en un contexto raíz o positivo, el cual aparece como una subexpresión :mzn:`e1` o :mzn:`e2` en una expresión :mzn:`e1 /\ e2` que aparece en un contexto positivo, o que aparece como una subexpresión :mzn:`e` en una expresión:mzn:`not e` que aparece en un contexto negativo.
526
527Las expresiones booleanas de contexto positivo no necesitan mantenerse en un modelo, pero hacer que se sostengan solo aumentará la posibilidad de que se mantenga la restricción adjunta. Una expresión de contexto positiva tiene un número par de negaciones en la ruta desde el contexto raíz adjunto a la expresión.
528
529Negativo:
530El contexto negativo es el contexto para cualquier expresión que aparece como una subexpresión :mzn:`e1` o :mzn:`e2` en una expresión :mzn:`e1 \/ e2` o :mzn:`e1 /\ e2` que ocurre en un negativo contexto, o que aparece como una subexpresión :mzn:`e` en una expresión :mzn:`not e` que aparece en un contexto positivo.
531
532Un contexto negativo es el contexto para cualquier expresión que aparezca como una expresión secundaria :mzn:`e1` o :mzn:`e2` en una expresión :mzn:`e1 \/ e2` o :mzn:`e1 /\ e2` que aparece en un contexto negativo, o que aparece como una subexpresión :mzn:`e` en una expresión :mzn:`not e` que aparece en un contexto positivo.
533
534Las expresiones booleanas de contexto negativo no necesitan mantenerse en un modelo, pero al hacerlas falsas aumentará la posibilidad de que se mantenga la restricción de inclusión. Una expresión de contexto negativa tiene un número impar de negaciones en la ruta desde el contexto raíz adjunto a la expresión.
535
536Mixto:
537Un contexto mixto es el contexto para cualquier expresión booleana que aparece como una subexpresión :mzn:`e1` o :mzn:`e2` en :mzn:`e1 <-> e2`, :mzn:`e1 = e2`, o :mzn:`bool2int(e)`.
538
539La expresión de contexto mixto es tanto positiva como negativa. Esto se puede ver por el hecho de que :mzn:`e1 <-> e2` es equivalente a :mzn:`(e1 /\ e2) \/ (not e1 /\ not e2)` y :mzn:`x = bool2int(e)` es equivalente a :mzn:`(e /\ x=1) \/ (not e /\ x=0)`.
540
541Considera el fragmento de código
542
543.. code-block:: minizinc
544
545 constraint x > 0 /\ (i <= 4 -> x + bool2int(x > i) = 5);
546
547
548Entonces :mzn:`x > 0` está en el contexto raíz, :mzn:`i <= 4}` está en un contexto negativo, :mzn:`x + bool2int(x > i) = 5` está en una posición positiva contexto, y :mzn:`x > i` está en un contexto mixto.
549
550
551Restricciones locales
552---------------------
553
554.. index::
555 single: constraint; local
556
557Let expressions can also be used to include local constraints, usually to constrain the behaviour of local variables.
558For example, consider defining a square root function making use of only multiplication:
559
560Las expresiones ``let`` también se pueden usar para incluir restricciones locales, generalmente para restringir el comportamiento de las variables locales.
561Por ejemplo, considere la definición de una función de raíz cuadrada haciendo uso de solo la multiplicación:
562
563.. code-block:: minizinc
564
565 function var float: mysqrt(var float:x) =
566 let { var float: y;
567 constraint y >= 0;
568 constraint x = y * y; } in y;
569
570Las restricciones locales aseguran que :mzn:`y` toma el valor correcto; que luego es devuelto por la función.
571
572Las restricciones locales se pueden usar en cualquier expresión de let, aunque el uso más común es en la definición de funciones.
573
574
575.. defblock:: Expresiones Let
576
577 .. index::
578 single: expression; let
579
580 :index:`Local variables <variable;local>`
581
582 Se puede introducir en cualquier expresión con *let expression* de la forma:
583
584 .. code-block:: minizincdef
585
586 let { <dec>; ... <dec> ; } in <exp>
587
588 Las declaraciones :mzndef:`<dec>` pueden ser declaraciones de variables y parámetros de decisión (que deben inicializarse) o elementos de restricción.
589 Ninguna declaración puede hacer uso de una variable recientemente declarada antes de ser presentada.
590
591 Tenga en cuenta que las variables locales y las restricciones no pueden ocurrir en las pruebas.
592 Las variables locales no pueden ocurrir en predicados o funciones que aparecen en un :index:`negative <context; negative>` o en un contexto :index:`mixed <context; mixed>`, a menos que la variable esté definida por una expresión.
593
594
595Funciones de Reflexión del Dominio
596----------------------------------
597
598.. index::
599 single: domain; reflection
600
601Otras funciones de reflexión importantes son aquellas que nos permiten acceder a los dominios de las variables. La expresión :mzn:`lb(x)` devuelve un valor que es menor o igual a cualquier valor :mzn `x` que pueda tomar en una solución del problema. Por lo general, será el más bajo declarado :index:`bound <variable; bound>` de :mzn:`x`
602
603Si :mzn:`x` se declara como un tipo no finito, por ejemplo, :mzn:`var int`, entonces es un error.
604
605Similarly the expression :mzn:`dom(x)` returns a (non-strict) superset of the possible values of :mzn:`x` in any solution of the problem.
606
607De nuevo, generalmente son los valores declarados, y de nuevo si no se declara como finito, entonces hay un error.
608
609.. \ignore{ % for capture for testing!
610.. $ mzn-g12fd reflection_es.mzn
611.. } % $
612
613
614.. literalinclude:: examples/reflection_es.mzn
615 :language: minizinc
616 :name: ex-reflect
617 :caption: Usar predicados de reflexión (:download:`reflection_es.mzn <examples/reflection_es.mzn>`).
618
619
620Por ejemplo, el modelo descrito en :numref:`ex-reflect` puede mostrar:
621
622.. code-block:: none
623
624 y = -10
625 D = -10..10
626 ----------
627
628O
629
630.. code-block:: none
631
632 y = 0
633 D = {0, 1, 2, 3, 4}
634 ----------
635
636O cualquier respuesta con :math:`-10 \leq y \leq 0` y :math:`\{0, \ldots, 4\} \subseteq D \subseteq \{-10, \ldots, 10\}`.
637
638Las expresiones de reflexión de dominio variable deben usarse de manera tal que sean correctas para cualquier aproximación segura, ¡pero tenga en cuenta que esto no está verificado!
639
640
641Por ejemplo, el código adicional
642
643.. code-block:: minizinc
644
645 var -10..10: z;
646 constraint z <= y;
647
648No es un uso seguro de la información de dominio.
649Dado que el uso de la aproximación más ajustada (correcta) conduce a más soluciones que la aproximación inicial más débil.
650
651.. TODO: this sounds wrong!
652
653.. defblock:: Domain reflection
654
655 .. index::
656 single: domain; reflection
657
658 Hay funciones de reflexión para interrogar los posibles valores de las expresiones que contienen variables:
659
660 - :mzndef:`dom(<exp>)` devuelve una aproximación segura a los posibles valores de la expresión.
661 - :mzndef:`lb(<exp>)` devuelve una aproximación segura al valor límite inferior de la expresión.
662 - :mzndef:`ub(<exp>)` devuelve una aproximación segura al valor límite superior de la expresión.
663
664 Las expresiones para :mzn:`lb` y :mzn:`ub` solo puede ser de tipos :mzn:`int`, :mzn:`bool`, :mzn:`float` o :mzn:`set of int`.
665 Para :mzn:`dom` el tipo no puede ser :mzn:`float`.
666 Si una de las variables que aparecen en :mzndef:`<exp>` tiene un :index:`non-finite declared type <type; non-finite>` (por ejemplo, :mzn:`var int` o :mzn:`var float`) entonces un error puede ocurrir.
667
668 También hay versiones que funcionan directamente en matrices de expresiones (con restricciones similares):
669
670 - :mzndef:`dom_array(<array-exp>)`: Devuelve una aproximación segura a la unión de todos los valores posibles de las expresiones que aparecen en la matriz.
671 - :mzndef:`lb_array(<array-exp>)`: Devuelve una aproximación segura al límite inferior de todas las expresiones que aparecen en la matriz.
672 - :mzndef:`ub_array(<array-exp>)`: Devuelve una aproximación segura al límite superior de todas las expresiones que aparecen en la matriz.
673
674Las combinaciones de predicados, variables locales y reflexión de dominio permiten la definición de restricciones globales complejas por descomposición.
675Podemos definir la descomposición basada en el tiempo de la restricción :mzn:`cumulative` utilizando el código que se muestra en :numref:`ex-cumul`.
676
677.. literalinclude:: examples/cumulative_es.mzn
678 :language: minizinc
679 :name: ex-cumul
680 :caption: Definiendo un predicado ``cumulative`` por descomposición (:download:`cumulative_es.mzn <examples/cumulative_es.mzn>`).
681
682La descomposición usa :mzn:`lb` y :mzn:`ub` para determinar el conjunto de veces :mzn:`times` sobre las cuales las tareas podrían estar en rango.
683A continuación, afirma para cada momento :mzn:`t` en :mzn:`times` que la suma de recursos para las tareas activas en el momento :mzn:`t` es menor que la límite :mzn:`b`.
684
685Alcance
686-------
687
688.. index::
689 single: scope
690
691Vale la pena mencionar brevemente el alcance de las declaraciones en MiniZinc.
692MiniZinc tiene un único espacio de nombre, por lo que todas las variables que aparecen en las declaraciones son visibles en cada expresión del modelo.
693
694MiniZinc presenta variables con ámbito local de varias maneras:
695
696- Como :index:`iterator <variable; iterator>` variables en expresiones :index:`comprehension`.
697- Usando las expresiones :mzn:`let`.
698- Como predicado y función :index:`arguments <argument>`
699
700Cualquier variable de ámbito local eclipsa las variables de ámbito externo del mismo nombre.
701
702.. literalinclude:: examples/scope_es.mzn
703 :language: minizinc
704 :name: ex-scope
705 :caption: Un modelo para ilustrar alcances de variables (:download:`scope_es.mzn <examples/scope_es.mzn>`).
706
707Por ejemplo, en el modelo que se muestra en :numref:`ex-scope` the :mzn:`x` en :mzn:`-x <= y` es el global :mzn:`x`, el :mzn:`x` en :mzn:`smallx (x)` es el iterador :mzn:`x in 1..u`, mientras que :mzn:`y` en la disyunción es el segundo argumento del predicado.