1.. |coerce| replace:: :math:`\stackrel{c}{\rightarrow}` 2 3.. |varify| replace:: :math:`\stackrel{v}{\rightarrow}` 4 5.. |TyOverview| replace:: *Visión general.* 6 7.. |TyInsts| replace:: *Instancias permitidas.* 8 9.. |TySyntax| replace:: *Sintaxis.* 10 11.. |TyFiniteType| replace:: *Finito?* 12 13.. |TyVarifiable| replace:: *Varificable?* 14 15.. |TyOrdering| replace:: *Ordenando.* 16 17.. |TyInit| replace:: *Inicialización.* 18 19.. |TyCoercions| replace:: *Coerciones.* 20 21 22Especificación de MiniZinc 23========================== 24 25Introducción 26------------ 27 28Este documento define a MiniZinc, el cual es un lenguaje para modelar satisfacción de restricciones y problemas de optimización. 29 30 31MiniZinc es un lenguaje de modelado de alto nivel, mecanografiado, sobre todo de primer orden, funcional. 32El lenguaje provee de: 33 34- Sintaxis como una notación matemática (coerciones automáticas, sobrecarga, iteraciones, conjuntos, arreglos); 35- Restricciones expresivas (dominio finito, conjunto, aritmética lineal, entera); 36- Soporte para diferentes tipos de problemas (satisfacción, optimización explicita); 37- Separación del modelo y de los datos; 38- Estructuras de datos de alto-nivel y encapsulamiento de datos (conjuntos, arreglos, tipos de enumeración restriciones de tipo-instanciación); 39- Extensibilidad (usuarios definen funciones y predicados); 40- Confiabilidad (verificación de tipo, comprobación de instancias, aserciones); 41- Modelado independiente del solver; 42- Semántica declarativa y simple; 43 44Minizinc es similar a OPL y más cercano a los lenguajes de CLP como ECLIPSe. 45 46Este documento tiene la siguiente estructura 47:ref:`spec-syntax-notation` introduce la notación de sintaxis utilizado en toda la especificación. 48:ref:`spec-Overview` ofrece una visión general de alto nivel de los modelos MiniZinc. 49:ref:`spec-Syntax-Overview` cubre los fundamentos de la sintaxis. 50:ref:`spec-High-level-Model-Structure` cubre las estructuras de alto nivel: elementos, modelos de archivos múltiples, espacios de nombres y ámbitos. 51:ref:`spec-Types` cubre los tipos y los tipo-instanciación. 52:ref:`spec-Expressions` cubre las expresiones. 53:ref:`spec-Items` describe en detalle los elementos de nivel-superior. 54:ref:`spec-Annotations` describe las anotaciones. 55:ref:`spec-Partiality` describe como se maneja la parcialidad en varios casos. 56:ref:`spec-builtins` describe el lenguaje incorporado. 57:ref:`spec-Grammar` da la gramática de MiniZinc. 58:ref:`spec-Content-types` define los tipos de contenido utilizados en esta especificación. 59 60 61Este documento también proporciona una explicación de por qué se tomaron ciertas decisiones de diseño. Dichas explicaciones están marcadas por la palabra *Justificación* y están escritas en cursiva, y no constituyen parte de la especificación como tal. 62*Justificación: estas explicaciones están presentes porque son útiles tanto para los diseñadores como para los usuarios de MiniZinc.* 63 64 65Autores originales 66~~~~~~~~~~~~~~~~~~ 67 68La versión original de este documento fue preparada por Nicholas Nethercote, Kim Marriott, Reza Rafeh, Mark Wallace y Maria Garcia de la Banda. Sin embargo, MiniZinc está evolucionando, al igual que este documento. 69 70Para ver un documento publicado formalmente sobre el lenguaje MiniZinc y el lenguaje Zinc superconjunto, consulte: 71 72- N. Nethercote, P.J. Stuckey, R. Becket, S. Brand, G.J. Duck, and G. Tack. 73 Minizinc: Towards a standard CP modelling language. 74 In C. Bessiere, editor, *Proceedings of the 13th International 75 Conference on Principles and Practice of Constraint Programming*, volume 4741 76 of *LNCS*, pages 529--543. Springer-Verlag, 2007. 77- K. Marriott, N. Nethercote, R. Rafeh, P.J. Stuckey, 78 M. Garcia de la Banda, and M. Wallace. 79 The Design of the Zinc Modelling Language. 80 *Constraints*, 13(3):229-267, 2008. 81 82.. _spec-syntax-notation: 83 84 85 86Notación 87-------- 88 89Los conceptos básicos del EBNF utilizados en esta especificación son los siguientes. 90 91- Los no terminales se escriben entre corchetes angulares, :mzndef:`<item>`. 92- Las terminales están escritas entre comillas dobles. Por ejemplo, :mzndef:`"constraint"`. Una terminal de doble cita se escribe como una secuencia de tres comillas dobles :mzndef:`"""`. 93- Los elementos opcionales están escritos entre corchetes, por ejemplo, :mzndef:`[ "var" ]`. 94- Las secuencias de cero o más elementos se escriben con paréntesis y una estrella, por ejemplo :mzndef:`( "," <ident> )*`. 95- Las secuencias de uno o más elementos se escriben con paréntesis y un signo más (+), por ejemplo :mzndef:`( <msg> )+`. 96- Las listas no vacías se escriben con un elemento, un terminal separador/terminador, y tres puntos. Por ejemplo: 97 98.. code-block:: minizincdef 99 100 <expr> "," ... 101 102Es la abreviatura de: 103 104.. code-block:: minizincdef 105 106 <expr> ( "," <expr> )* [ "," ] 107 108 109El terminal final siempre es opcional en listas no vacías. 110 111- Las expresiones regulares se usan en algunas producciones. Por ejemplo, :mzndef:`[-+]?[0-9]+`. 112 113La gramática de MiniZinc se presenta pieza por pieza a lo largo de este documento. También está disponible como un todo en :ref:`spec-Grammar`. 114 115La gramática de salida también incluye algunos detalles del uso del espacio en blanco. 116Se usan las siguientes convenciones: 117 118- Un carácter de nueva línea o una secuencia CRLF es escrito ``\n``. 119 120 121.. - A sequence of space characters of length :math:`n` is written ``nSP``, e.g., ``2SP``. 122 123 124.. _spec-Overview: 125 126 127Descripción general de un modelo 128-------------------------------- 129 130Conceptualmente, una especificación de problema MiniZinc tiene dos partes. 131 1321. El *modelo*: la parte principal de la especificación del problema, que describe la estructura de una clase particular de problemas. 1332. Los *datos*: los datos de entrada para el modelo, que especifica un problema particular dentro de esta clase de problemas. 134 135El emparejamiento de un modelo con un conjunto de datos particular es una *instancia de modelo* (a veces abreviado como *instancia*). 136 137El modelo y los datos pueden estar separados, o los datos pueden estar "cableados" en el modelo. 138:ref:`spec-Model-Instance-Files` especifica cómo el modelo y los datos se pueden estructurar dentro de archivos en una instancia modelo. 139 140Hay dos clases amplias de problemas: satisfacción y optimización. 141En los problemas de satisfacción, todas las soluciones se consideran igualmente buenas, mientras que en los problemas de optimización las soluciones se ordenan según un objetivo y el objetivo es encontrar una solución cuyo objetivo sea óptimo. 142:ref:`spec-Solve-Items` especifica cómo se elige la clase de problema. 143 144 145Fases de evaluación 146~~~~~~~~~~~~~~~~~~~ 147 148Una instancia de modelo MiniZinc se evalúa en dos fases distintas. 149 1501. Tiempo de instancia: Comprobación estática de la instancia del modelo. 1512. Tiempo de ejecución: Evaluación de la instancia (ejemplo, resolución de restricciones). 152 153Es posible que la instancia del modelo no se compile debido a un problema con el modelo y/o los datos que se detectaron en el momento de la instancia. 154Esto podría deberse a un error de sintaxis, a un error de 155instanciación de tipo, al uso de una función u operación no admitida, etc. 156En este caso, el resultado de la evaluación es un error estático, esto se debe informar antes del tiempo de ejecución. 157La forma de salida para los errores estáticos depende de la implementación, aunque dicha salida debería ser fácilmente reconocible como un error estático. 158 159Una implementación puede producir advertencias durante todas las fases de evaluación. 160Por ejemplo, una implementación puede ser capaz de determinar que existen restricciones insatisfactorias antes del tiempo de ejecución, y la advertencia resultante dada al usuario puede ser más útil que si se detecta la insatisfacción en el tiempo de ejecución. 161 162Una implementación debe producir una advertencia si el objetivo para un problema de optimización no tiene límites. 163 164 165.. _spec-run-time-outcomes: 166 167Resultados en tiempo de ejecución 168~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 169 170Suponiendo que no hay errores estáticos, el resultado de la fase de tiempo de ejecución tiene la siguiente forma abstracta: 171 172.. literalinclude:: output.mzn 173 :language: minizincdef 174 :start-after: % Output 175 :end-before: % 176 177Si se produce una solución en la salida, entonces debe ser factible. 178Para problemas de optimización, cada solución debe ser estrictamente mejor que cualquier solución anterior. 179 180Si no hay soluciones en el resultado, el resultado debe indicar que no hay soluciones. 181 182Si la búsqueda está completa, la salida puede indicar esto después de las soluciones. 183La ausencia del mensaje de completitud indica que la búsqueda está incompleta. 184 185Cualquier advertencia producida durante el tiempo de ejecución se debe resumir después de la declaración de integridad. 186En particular, si hubo advertencias durante el tiempo de ejecución, entonces el resumen debe indicar este hecho. 187 188La implementación puede producir texto en cualquier formato después de las advertencias. 189Por ejemplo, puede imprimir un resumen de estadísticas de benchmarking o recursos utilizados. 190 191.. _spec-output: 192 193 194 195 196Salida 197~~~~~~ 198 199Las implementaciones deben ser capaces de producir resultados de tipo de contenido ``application/x-zinc-output``, que se describe a continuación y también en :ref:`spec-Content-types`. 200Las implementaciones también pueden producir resultados en formatos alternativos. 201Cualquier salida debe ajustarse al formato abstracto de la sección anterior y debe tener la semántica descrita allí. 202 203Tipo de contenido ``application/x-zinc-output`` extiende la sintaxis de la sección anterior de la siguiente manera: 204 205.. literalinclude:: output.mzn 206 :language: minizincdef 207 :start-after: % Solutions 208 :end-before: % 209 210El texto de la solución para cada solución debe ser como se describe en :ref:`spec-Output-Items`. 211Se debe agregar una nueva línea si el texto de la solución no finaliza con una nueva línea. 212*Justificación: Esto permite que las soluciones se extraigan de la salida sin saber necesariamente cómo se formatean las soluciones.* 213Las soluciones terminan con una secuencia de diez guiones seguidos de una nueva línea. 214 215.. literalinclude:: output.mzn 216 :language: minizincdef 217 :start-after: % Unsatisfiable 218 :end-before: % 219 220El resultado de integridad se imprime en una línea separada. *Justificación: las cadenas están diseñadas para indicar claramente el final de las soluciones.* 221 222.. literalinclude:: output.mzn 223 :language: minizincdef 224 :start-after: % Complete 225 :end-before: % 226 227Si la búsqueda está completa, se imprime una declaración correspondiente al resultado. 228Para un resultado sin soluciones, el enunciado es que la instancia del modelo no es satisfactoria. Para el resultado de no más soluciones, la declaración es que el conjunto de soluciones está completo. Finalmente, para un resultado sin mejores soluciones, la afirmación es que la última solución es óptima . 229*Justificación: estas son las implicaciones lógicas de una búsqueda completa.* 230 231.. literalinclude:: output.mzn 232 :language: minizincdef 233 :start-after: % Messages 234 :end-before: % 235 236Si la búsqueda es incompleta, se pueden imprimir uno o más mensajes que describen los motivos de la falta de cumplimiento. 237Del mismo modo, si se produjeron advertencias durante la búsqueda, se repiten después del mensaje de integridad. 238Ambos tipos de mensajes deben tener líneas que comiencen con ``%`` para que se reconozcan como comentarios por postprocesamiento. 239*Justificación: Esto permite que los mensajes individuales sean fácilmente reconocibles.* 240 241Por ejemplo, se puede generar lo siguiente para un problema de optimización: 242 243.. code-block:: bash 244 245 =====UNSATISFIABLE===== 246 % trentin.fzn:4: warning: model inconsistency detected before search. 247 248Tenga en cuenta que, como en este caso, un objetivo ilimitado no se considera una fuente de incompletud. 249 250.. _spec-syntax-overview: 251 252 253Descripción general de la sintaxis 254---------------------------------- 255 256Conjunto de caracteres 257~~~~~~~~~~~~~~~~~~~~~~ 258 259Los archivos de entrada a MiniZinc deben codificarse como UTF-8. 260 261MiniZinc es sensible a mayúsculas y minúsculas. No hay lugares donde se deben usar letras mayúsculas o minúsculas. 262 263MiniZinc no tiene restricciones de diseño, es decir, cualquier espacio en blanco (que contiene espacios, pestañas y líneas nuevas) es equivalente a cualquier otro. 264 265 266Comentarios 267~~~~~~~~~~~ 268 269Un ``%`` indica que el resto de la línea es un comentario. MiniZinc también tiene comentarios de bloque, usando los símbolos ``/*`` and ``*/`` para marcar el comienzo y el final de un comentario. 270 271 272.. _spec-identifiers: 273 274 275Identificadores 276~~~~~~~~~~~~~~~ 277 278Los identificadores tienen la siguiente sintaxis: 279 280.. code-block:: minizincdef 281 282 <ident> ::= [A-Za-z][A-Za-z0-9_]* % excluyendo las palabras clave 283 | "'" [^'\xa\xd\x0]* "'" 284 285.. code-block:: minizinc 286 287 mi_nombre_2 288 MiNombre2 289 'Un identificador arbitrario' 290 291Se reservan varias palabras clave y no se pueden usar como identificadores. Las palabras clave son: 292:mzn:`ann`, 293:mzn:`annotation`, 294:mzn:`any`, 295:mzn:`array`, 296:mzn:`bool`, 297:mzn:`case`, 298:mzn:`constraint`, 299:mzn:`diff`, 300:mzn:`div`, 301:mzn:`else`, 302:mzn:`elseif`, 303:mzn:`endif`, 304:mzn:`enum`, 305:mzn:`false`, 306:mzn:`float`, 307:mzn:`function`, 308:mzn:`if`, 309:mzn:`in`, 310:mzn:`include`, 311:mzn:`int`, 312:mzn:`intersect`, 313:mzn:`let`, 314:mzn:`list`, 315:mzn:`maximize`, 316:mzn:`minimize`, 317:mzn:`mod`, 318:mzn:`not`, 319:mzn:`of`, 320:mzn:`op`, 321:mzn:`opt`, 322:mzn:`output`, 323:mzn:`par`, 324:mzn:`predicate`, 325:mzn:`record`, 326:mzn:`satisfy`, 327:mzn:`set`, 328:mzn:`solve`, 329:mzn:`string`, 330:mzn:`subset`, 331:mzn:`superset`, 332:mzn:`symdiff`, 333:mzn:`test`, 334:mzn:`then`, 335:mzn:`true`, 336:mzn:`tuple`, 337:mzn:`type`, 338:mzn:`union`, 339:mzn:`var`, 340:mzn:`where`, 341:mzn:`xor`. 342 343Una serie de identificadores se utilizan para integradas; ver :ref:`spec-builtins` para más detalles. 344 345.. _spec-High-level-Model-Structure: 346 347 348Estructura de modelo de alto nivel 349---------------------------------- 350 351Un modelo MiniZinc consta de múltiples *elementos*: 352 353.. literalinclude:: grammar.mzn 354 :language: minizincdef 355 :start-after: % A MiniZinc model 356 :end-before: % 357 358Los elementos pueden disponerse en cualquier orden; los identificadores no necesitan ser declarados antes de ser usados. Los elementos tienen la siguiente sintaxis de nivel superior: 359 360.. literalinclude:: grammar.mzn 361 :language: minizincdef 362 :start-after: % Items 363 :end-before: % 364 365Incluir elementos proporciona una forma de combinar múltiples archivos en una sola instancia. Esto permite que un modelo se divida en varios archivos 366(:ref:`spec-Include-Items`). 367 368Los ítems de declaración variables introducen nuevas variables globales y posiblemente las vinculen a un valor (:ref:`spec-Declarations`). 369 370Los elementos de asignación vinculan valores a variables globales (:ref:`spec-Assignments`). 371 372Los elementos de restricción describen las restricciones del modelo (:ref:`spec-Constraint-Items`). 373 374Los elementos de resolución son el "punto de partida" de un modelo y especifican exactamente qué tipo de solución se está buscando: 375simple satisfacción, o la minimización/maximización de una expresión. Cada modelo debe tener exactamente un elemento de solución (:ref:`spec-Solve-Items`). 376 377Los elementos de salida se utilizan para presentar muy bien el resultado de una ejecución del modelo (:ref:`spec-Output-Items`). 378 379Elementos de predicados, elementos de prueba (que son solo un tipo especial de predicado) y los elementos de función introducen nuevos predicados y funciones definidos por el usuario que pueden invocarse en expresiones (:ref:`spec-preds-and-fns`). 380Los predicados, las funciones y los operadores incorporados se describen colectivamente como *operaciones*. 381 382Los elementos de anotación aumentan el tipo :mzn:`ann`, cuyos valores pueden especificar información no declarativa y/o específica del solucionador en un modelo. 383 384.. _spec-model-instance-files: 385 386 387 388 389Archivos de instancias modelo 390~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 391 392Los modelos en MiniZinc se pueden construir a partir de múltiples archivos utilizando elementos incluidos (ver :ref:`spec-Include-Items`). MiniZinc no tiene un sistema de módulos como tal; todos los archivos incluidos simplemente se concatenan y procesan como un todo, exactamente como si todos hubieran sido parte de un solo archivo. 393*Razón fundamental: No hemos encontrado mucha necesidad de uno hasta el momento. Si los modelos más grandes se vuelven comunes y el espacio de nombres global único se convierte en un problema, esto debería reconsiderarse.* 394 395Cada modelo puede emparejarse con uno o más archivos de datos. Los archivos de datos son más restringidos que los archivos de modelo. Solo pueden contener asignaciones de variables (ver :ref:`spec-Assignments`). 396 397Los archivos de datos pueden no incluir llamadas a operaciones definidas por el usuario. 398 399Los modelos no contienen los nombres de los archivos de datos. Al hacerlo, se corregirá el archivo de datos utilizado por el modelo y se frustrará el propósito de permitir archivos de datos separados. En cambio, una implementación debe permitir que uno o más archivos de datos se combinen con un modelo para su evaluación a través de un mecanismo como la línea de comandos. 400 401Al verificar un modelo con datos, se deben asignar todas las variables globales con inserciones de tipo fijo, a menos que no se utilicen (en cuyo caso pueden eliminarse del modelo sin efecto). 402 403Un archivo de datos solo se puede verificar en busca de errores estáticos junto con un modelo, ya que el modelo contiene las declaraciones que incluyen los tipos de las variables asignadas en el archivo de datos. 404 405Un único archivo de datos puede compartirse entre varios modelos, siempre que las definiciones sean compatibles con todos los modelos. 406 407.. _spec-namespaces: 408 409 410Espacios de nombres (Namespaces) 411~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 412 413Todos los nombres declarados en el nivel superior pertenecen a un solo espacio de nombres. 414Incluye los siguientes nombres. 415 4161. Todos los nombres de variables globales. 4172. Todos los nombres de funciones y predicados, tanto integrados como definidos por el usuario. 4183. Todos los nombres de tipos enumerados y nombres de casos de enumeración. 4194. Todos los nombres de anotación. 420 421Debido a que los modelos MiniZinc de archivos múltiples se componen a través de la concatenación (:ref:`spec-Model-Instance-Files`), todos los archivos comparten este espacio de nombres de nivel superior. Por lo tanto, una variable ``x`` declarado en un archivo de modelo no se pudo declarar con un tipo diferente en un archivo diferente, por ejemplo. 422 423MiniZinc admite la sobrecarga de operaciones integradas y definidas por el usuario. 424 425.. _spec-scopes: 426 427 428 429Alcances 430~~~~~~~~ 431 432Dentro del espacio de nombres de nivel superior, hay varios tipos de ámbito local que 433introducir nombres locales: 434 435- Expresiones de Comprensión (:ref:`spec-Set-Comprehensions`). 436- Expresiones Let (:ref:`spec-Let-Expressions`). 437- Listas de funciones y argumentos de predicados y cuerpos (:ref:`spec-preds-and-fns`). 438 439Las secciones enumeradas especifican estos ámbitos con más detalle. En cada caso, cualquier 440los nombres declarados en el ámbito local eclipsan nombres globales idénticos. 441 442 443.. _spec-types: 444 445 446 447Tipos y Tipos de Instanciación 448------------------------------ 449 450MiniZinc proporciona: 451 452- Cuatro tipos de escalar incorporados: Booleanos (Boolean), enteros (Integer), flotantes (Float) y cadenas (Strings); 453- Tipos enumerados; 454- Dos tipos integrados compuestos: conjuntos y matrices multidimensionales; 455- Y el tipo de anotación extensible del usuario :mzn:`ann`. 456 457Cada tipo tiene uno o más posibles de *instanciación*. La instanciación de una variable o valor indica si se ha fijado a un valor conocido o no. Un emparejamiento de un tipo y creación de instancias se llama *tipo-instanciación*. 458 459Comenzamos discutiendo algunas propiedades que se aplican a todos los tipos. Luego presentamos instancias con más detalle. Luego cubrimos cada tipo individualmente, dando: una visión general del tipo y sus posibles instancias, la sintaxis para su tipo-instanciación, si es un tipo finito (y si es así, su dominio), si es variable, el orden y operaciones de igualdad, si sus variables deben inicializarse en el momento de la instancia y si puede estar involucrado en coacciones automáticas. 460 461 462Propiedades de los tipos 463~~~~~~~~~~~~~~~~~~~~~~~~ 464 465La siguiente lista presenta algunas propiedades generales de los tipos MiniZinc. 466 467- Actualmente, todos los tipos son monotipos. En el futuro, podemos permitir tipos que son polimórficos en otros tipos y también las limitaciones asociadas. 468- Distinguimos tipos que son *tipos finitos*. En MiniZinc, los tipos finitos incluyen booleanos, enumeraciones (enums), tipos definidos via conjunto de expresiones tipo-instanciación como los tipos de rango (ver :ref:`spec-Set-Expression-type-insts`), así como conjuntos y matrices, compuestos de tipos finitos. Los tipos que no son tipos finitos son enteros no restringidos, flotantes no restringidos, cadenas no restringidas y :mzn:`ann`. Los tipos finitos son relevantes para conjuntos (:mzn:`spec-Sets`) y los índices de matriz (:mzn:`spec-Arrays`). Cada tipo finito tiene un *dominio*, que es un valor establecido que contiene todos los valores posibles representados por el tipo. 469- Todos los tipos de primer orden (esto excluye :mzn:`ann`) tiene incorporado un orden total y un sistema incorporado en la igualdad; ``>``, ``<``, ``==``/``=``, ``!=``, ``<=`` and ``>=`` los operadores de comparación se pueden aplicar a cualquier par de valores del mismo tipo. *Razón fundamental: Esto facilita la especificación de ruptura de simetría y de predicados y funciones polimórficos.* Tenga en cuenta que, como en la mayoría de los lenguajes, el uso de igualdad en flotantes o tipos que contienen flotantes generalmente no es confiable debido a su representación inexacta. Una implementación puede optar por advertir sobre el uso de igualdad con flotantes o tipos que contienen flotantes. 470 471.. _spec-instantiations: 472 473 474Instanciaciones 475~~~~~~~~~~~~~~~ 476 477Cuando se evalúa un modelo MiniZinc, el valor de cada variable puede ser inicialmente desconocido. A medida que se ejecuta, el *dominio* de cada variable (el conjunto de valores que puede tomar) puede reducirse, posiblemente hasta un único valor. 478 479Una *instanciación* (a veces abreviado como *inst*) describe cómo fija o no fija una variable en una tiempo-instancia. En el nivel más básico, el sistema de creación de instancias distingue dos tipos de variables: 480 481#. *Parametros*, cuyos valores están fijados a tiempo-instancia, usualmente escrito como "fijo" (fixed). 482#. *Variables de decisión* (a menudo abreviado como *variables*), cuyos valores pueden estar completamente sin fijar en tiempo-instancia, pero puede volverse fijo en tiempo de ejecución (de hecho, la fijación de variables de decisión es el objetivo total de la resolución de restricciones). 483 484En las variables de decisión MiniZinc pueden tener los siguientes tipos: Booleanos, enteros, flotantes y conjuntos de enteros, y enumeración. 485Arreglos y :mzn:`ann` puede contener variables de decisión. 486 487.. _spec-type-inst: 488 489 490Tipo-Instanciación 491~~~~~~~~~~~~~~~~~~ 492 493Como cada variable tiene un tipo y una instancia, a menudo se combinan en un único *tipo-instanciación*. Tipo-instanciación son principalmente lo que tratamos cuando escribimos modelos, en lugar de tipos. 494 495Una variable de tipo-instanciación *nunca cambia*. Esto significa que una variable de decisión cuyo valor se vuelve fijo durante la evaluación del modelo todavía tiene su original tipo-instanciación (ejemplo :mzn:`var int`), porque ese era su tipo-instanciación a un tiempo-instancia. 496 497Algunos tipos-instanciación puede ser coaccionado automáticamente a otro tipo-instanciación. Por ejmplo, si un :mzn:`par int` valor se usa en un contexto donde :mzn:`var int` se espera, que es forzado automáticamente a una :mzn:`var int`. Escribimos esto :mzn:`par int` |coerce| :mzn:`var int`. Además, cualquier tipo-instanciación puede considerarse coercible a sí mismo. 498MiniZinc permite coerciones entre algunos tipos también. 499 500Algunos tipo-instanciación pueden ser *varificado* (varified). Por ejemplo, hecho sin fijar en el nivel superior. 501Por ejemplo, :mzn:`par int` está varificado a :mzn:`var int`. Escribimos esto :mzn:`par int` |varify| :mzn:`var int`. 502 503Tipo-instanciación que son varificables incluyen el tipo-instanciación de los tipos que pueden ser variables de decisión (Booleanos, enteros, flotantes, conjuntos, tipos enumerados). 504La varificación es relevante para tipo-instanciación sinónimos y accesos a la matriz. 505 506 507 508 509 510 511Visión general de expresiones de Tipo-instanciación 512~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 513 514Esta sección describe parcialmente cómo escribir inserciones de tipo en modelos MiniZinc. 515Se proporcionan más detalles para cada tipo tal como se describen en las siguientes secciones. 516 517Una expresión tipo-instanciación especifica un tipo-instanciación. 518Una expresión tipo-instanciación puede incluir un tipo-instanciación constraints. 519Una expresión tipo-instanciación aparece en declaraciones de variables (:ref:`spec-Declarations`) y elementos de operación definidos por el usuario (:ref:`spec-preds-and-fns`). 520 521Una expresión de tipo-instanciación tiene las siguientes sintaxis: 522 523.. literalinclude:: grammar.mzn 524 :language: minizincdef 525 :start-after: % Type-inst expressions 526 :end-before: % 527 528(La alternativa final, para los tipos de rango, usa el numérico específico :mzndef:`<num-expr>` no terminal, definido en :ref:`spec-Expressions-Overview`, en lugar de la :mzndef:`<expr>` no terminal. Si este no fuera el caso, la regla nunca coincidiría porque el operador ``..`` siempre se correspondería con el primero :mzndef:`<expr>`.) 529 530Esto cubre completamente las expresiones tipo-instanciación para tipos escalares. El compuesto de las sintaxis de las expresiones de tipo-instanciación está descrita con más detalle en :ref:`spec-Built-in-Compound-Types`. 531 532Las palabras claves :mzn:`par` y :mzn:`var` (o falta de ellos) determina la instanciación. La anotación :mzn:`par` puede ser emitida; las siguientes dos expresiones de tipo-instanciación son equivalentes: 533 534.. code-block:: minizinc 535 536 par int 537 int 538 539*Razón fundamental: El uso explícito de la palabra clave* :mzn:`var` *permite que una implementación compruebe que todos los parámetros se inicializan en el modelo o la instancia. También documenta claramente qué variables son parámetros y permite una comprobación de tipo-instanciación más precisa.* 540 541A tipo-instanciación es fijo si no contiene :mzn:`var` o :mzn:`any`, con la excepción de :mzn:`ann`. 542 543Tenga en cuenta que varias expresoines de tipo-instanciación que son sintácticamente expresables representan una ilegal tipo-instanciación. Por ejemplo, aunque la gramática permite :mzn:`var` frente a todas estas bases de colas de expresión de tipo-instanciación, es un error de tipo-instanciación que tiene una :mzn:`var` en el frente de una expresión de cadena o matriz. 544 545.. _spec-built-in-scalar-types: 546 547 548 549Tipos escalares incorporados y tipos de instanciación 550~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 551 552Booleanos 553+++++++++ 554 555|TyOverview| 556Los booleanos representan la verdad o la falsedad (verdadero o falso, true o false). *Justificación: los valores booleanos no están representados por números enteros. 557Los booleanos se pueden convertir explícitamente a enteros con la función * :mzn:`bool2int` *, lo que hace que la intención del usuario sea clara.* 558 559|TyInsts| 560Los booleanos pueden ser fijos o no. 561 562|TySyntax| 563Los booleanos fijos son escritos como :mzn:`bool` o :mzn:`par bool`. Los booleanos no fijos se escriben como :mzn:`var bool`. 564 565|TyFiniteType| 566Sí. El dominio de un booleano es :mzn:`false, true`. 567 568|TyVarifiable| 569:mzn:`par bool` |varify| :mzn:`var bool`, :mzn:`var bool` |varify| :mzn:`var bool`. 570 571|TyOrdering| 572El valor :mzn:`false` se considera más pequeño que :mzn:`true`. 573 574|TyInit| 575Una variable booleana fija se debe inicializar en el momento de la instancia; una variable booleana sin fijar no tiene que ser. 576 577|TyCoercions| 578:mzn:`par bool` |coerce| :mzn:`var bool`. 579 580También los booleanos se pueden forzar automáticamente a enteros; ver :ref:`spec-Integers`. 581 582.. _spec-integers: 583 584 585Enteros 586++++++++ 587 588|TyOverview| 589Los números enteros representan números enteros. Las representaciones enteras están definidas por la implementación. Esto significa que el rango representable de enteros está definido por la implementación. Sin embargo, una implementación debe abortar en tiempo de ejecución si una operación entera se desborda. 590 591|TyInsts| 592Los enteros pueden ser fijos o no. 593 594|TySyntax| 595Los enteros fijos están escritos como :mzn:`int` o :mzn:`par int`. Los enteros no fijos se escriben como :mzn:`var int`. 596 597|TyFiniteType| 598No, a menos que esté limitado por una expresión establecida (ver :ref:`spec-Set-Expression-Type-insts`). 599 600|TyVarifiable| 601:mzn:`par int` |varify| :mzn:`var int`, 602:mzn:`var int` |varify| :mzn:`var int`. 603 604|TyOrdering| 605El orden en enteros es el estándar. 606 607|TyInit| 608Una variable entera fija se debe inicializar en el momento de la instancia; una variable entera no fijada no lo necesita. 609 610|TyCoercions| 611:mzn:`par int` |coerce| :mzn:`var int`, 612:mzn:`par bool` |coerce| :mzn:`par int`, 613:mzn:`par bool` |coerce| :mzn:`var int`, 614:mzn:`var bool` |coerce| :mzn:`var int`. 615 616Además, los enteros se pueden forzar automáticamente a flotantes; ver :ref:`spec-Floats`. 617 618.. _spec-floats: 619 620 621 622Punto Flotante (Floats) 623+++++++++++++++++++++++ 624 625|TyOverview| 626Los números de punto flotante representan números reales. Las representaciones de números flotantes están definidas por la implementación. Esto significa que el rango y la precisión representables de los números de punto flotante están definidos por la implementación. Sin embargo, una implementación debe abortar en tiempo de ejecución en operaciones de punto flotante excepcionales 627 628(por ejemplo, aquellos que producen ``NaN``, es decir, Not a Number: No es un número, si usas número de punto flotante IEEE754). 629 630|TyInsts| 631Los números de punto flotante puede ser arreglado o no. 632 633|TySyntax| 634Los números de punto flotante son escritos como :mzn:`float` o :mzn:`par float`. Los números de punto flotante no fijos son escritos como :mzn:`var float`. 635 636|TyFiniteType| 637No, a menos que esté limitado por una expresión establecida (ver :ref:`spec-Set-Expression-Type-insts`). 638 639|TyVarifiable| 640:mzn:`par float` |varify| :mzn:`var float`, 641:mzn:`var float` |varify| :mzn:`var float`. 642 643|TyOrdering| 644El orden en los número de punto flotante es el estándar. 645 646|TyInit| 647Una variable flotante fija se debe inicializar en el momento de la instancia; una variable flotante no fija no lo necesita. 648 649|TyCoercions| 650:mzn:`par int` |coerce| :mzn:`par float`, 651:mzn:`par int` |coerce| :mzn:`var float`, 652:mzn:`var int` |coerce| :mzn:`var float`, 653:mzn:`par float` |coerce| :mzn:`var float`. 654 655.. _spec-enumerated-types: 656 657 658 659 660 661Tipos Enumerados 662++++++++++++++++ 663 664|TyOverview| 665Los tipos enumerados (o *enumerados* para abreviar) proporcionan un conjunto de alternativas nombradas. Cada alternativa se identifica por su *nombre del caso*. 666Los tipos enumerados, como en muchos otros idiomas, se pueden usar en lugar de tipos enteros para lograr una verificación de tipo más estricta. 667 668|TyInsts| 669Las enumeraciones pueden ser fijas o no. 670 671|TySyntax| 672Las variables de un tipo enumerado llamado ``X`` están representados por el término :mzn:`X` o :mzn:`par X` si es fija, y :mzn:`var X` si es no fija. 673 674|TyFiniteType| 675Sí. 676El dominio de una enumeración es el conjunto que contiene todos sus nombres de casos. 677 678|TyVarifiable| 679:mzn:`par X` |varify| :mzn:`var X`, 680:mzn:`var X` |varify| :mzn:`var X`. 681 682|TyOrdering| 683Cuando se comparan dos valores enumerados con diferentes nombres de casos, el valor con el nombre del caso que se declara primero se considera más pequeño que el valor con el nombre del caso que se declara en segundo lugar. 684 685|TyInit| 686Una variable de enumeración fija se debe inicializar en el momento de la instancia; una variable enumeración no fijada no lo necesita. 687 688|TyCoercions| 689:mzn:`par X` |coerce| :mzn:`par int`, 690:mzn:`var X` |coerce| :mzn:`var int`. 691 692.. _spec-strings: 693 694 695 696Cadenas (Strings) 697+++++++++++++++++ 698 699|TyOverview| 700Las cadenas son primitivas, es decir, no son listas de caracteres. 701 702Las expresiones de cadena se utilizan en aserciones, elementos de salida y anotaciones, y los literales de cadena se utilizan en los elementos de inclusión. 703 704|TyInsts| 705Las cadenas deben ser corregidas. 706 707|TySyntax| 708Las cadenas fijas están escritas como :mzn:`string` o :mzn:`par string`. 709 710|TyFiniteType| 711No, a menos que esté limitado por una expresión establecida (ver :ref:`spec-Set-Expression-Type-insts`). 712 713|TyVarifiable| 714No. 715 716|TyOrdering| 717Las cadenas se ordenan lexicográficamente utilizando los códigos de caracteres subyacentes. 718 719|TyInit| 720Una variable de cadena (que solo se puede arreglar) se debe inicializar en el momento de la instancia. 721 722|TyCoercions| 723Ninguno automático. Sin embargo, cualquier valor que no sea de cadena se puede convertir manualmente a una cadena usando la función built-in :mzn:`show` o usando la interpolación de cuerdas (ver :ref:`spec-String-Interpolation-Expressions`). 724 725.. _spec-Built-in-Compound-Types: 726 727 728 729Tipos de compuestos incorporados y Tipo-Instanciación 730~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 731 732.. _spec-sets: 733 734 735Conjuntos 736+++++++++ 737 738|TyOverview| 739Un conjunto es una colección sin duplicados. 740 741|TyInsts| 742Un tipo-instanciación de los elementos de un conjunto debe ser fija. *Justificación: Esto se debe a que los solucionadores actuales no son lo suficientemente potentes como para manejar conjuntos que contienen variables de decisión.* 743 744Los conjuntos pueden contener cualquier tipo, y pueden ser fijos o no. 745Si un conjunto no está fijado, sus elementos deben ser finitos, a menos que ocurra en uno de los siguientes contextos: 746 747- El argumento de un predicado, función o anotación. 748- La declaración de una variable o una variable local ``let`` con un valor asignado. 749 750|TySyntax| 751Una base establecida de una expresión de tipo-instanciación tiene la siguiente sintaxis: 752 753.. literalinclude:: grammar.mzn 754 :language: minizincdef 755 :start-after: % Set type-inst expressions 756 :end-before: % 757 758Algunos ejemplos de expresiones de conjuntos de tipo-instanciación: 759 760.. code-block:: minizinc 761 762 set of int 763 var set of bool 764 765|TyFiniteType| 766Sí, si los elementos establecidos son tipos finitos. De otra manera no. 767 768El dominio de un tipo de conjunto que es un tipo finito es el conjunto de poder del dominio de su tipo de elemento. Por ejemplo, el dominio de :mzn:`set of 1..2` es :mzn:`powerset(1..2)`, cual es :mzn:`{}, {1}, {1,2}, {2}`. 769 770|TyVarifiable| 771:mzn:`par set of TI` |varify| :mzn:`var set of TI`, 772:mzn:`var set of TI` |varify| :mzn:`var set of TI`. 773 774|TyOrdering| 775El orden predefinido en los conjuntos es un ordenamiento lexicográfico del *forma de conjunto ordenado*, donde :mzn:`{1,2}` está en forma de conjunto ordenado, por ejemplo, :mzn:`{2,1}` no es. 776Esto significa, por ejemplo, :mzn:`{} < {1,3} < {2}`. 777 778|TyInit| 779Una variable de conjunto fijo se debe inicializar en el momento de la instancia; una variable set no fijada no necesita ser. 780 781|TyCoercions| 782:mzn:`par set of TI` |coerce| :mzn:`par set of UI` y 783:mzn:`par set of TI` |coerce| :mzn:`var set of UI` y 784:mzn:`var set of TI` |coerce| :mzn:`var set of UI`, si 785:mzn:`TI` |coerce| :mzn:`UI`. 786 787 788 789 790Arreglos 791++++++++ 792 793|TyOverview| 794Los arrays MiniZinc son mapas de enteros fijos a valores. 795Los valores pueden ser de cualquier tipo. 796Los valores solo pueden tener inserciones de base tipo-instanciación. 797Las matrices de matrices no están permitidas. 798Las matrices pueden ser multidimensionales. 799 800Las matrices MiniZinc se pueden declarar de dos maneras diferentes. 801 802- *Las matrices explícitamente indexadas* tienen tipos de índice en la declaración que son tipos finitos. Por ejemplo: 803 804 .. code-block:: minizinc 805 806 array[0..3] of int: a1; 807 array[1..5, 1..10] of var float: a5; 808 809Para tales arrays, el tipo de índice especifica exactamente los índices que estarán en la matriz - el conjunto de índices de la matriz es el *dominio* del tipo de índice - y si los índices del valor asignado no coinciden, entonces es un tiempo de ejecución error. 810 811Por ejemplo, las siguientes asignaciones causan errores en tiempo de ejecución: 812 813 .. code-block:: minizinc 814 815 a1 = [4,6,4,3,2]; % Demasiados elementos. 816 a5 = []; % Muy pocos elementos. 817 818- *Las matrices implícitamente indexadas* tienen tipos de índice en la declaración que no son tipos finitos. Por ejemplo: 819 820 .. code-block:: minizinc 821 822 array[int,int] of int: a6; 823 824 No se verifican los índices cuando estas variables están asignadas. 825 826En MiniZinc, todos los conjuntos de índices de una matriz deben ser rangos contiguos de enteros o tipos enumerados. 827La expresión utilizada para la inicialización de una matriz debe tener conjuntos de índices coincidentes. 828Una expresión de matriz con un conjunto de índices enum se puede asignar a una matriz declarada con un conjunto de índices enteros, pero no al revés. 829La excepción son los literales de matriz, que se pueden asignar a matrices declaradas con conjuntos de índices enumerados. 830 831Por ejemplo: 832 833.. code-block:: minizinc 834 835 enum X = {A,B,C}; 836 enum Y = {D,E,F}; 837 array[X] of int: x = array1d(X, [5,6,7]); % Correcto 838 array[Y] of int: y = x; % Conjunto de índices no 839 % coinciden : Y != X 840 array[int] of int: z = x; % Correcto: asigne el índice X 841 % establecido en int 842 array[X] of int: x2 = [10,11,12]; % Correcto: coerción automática 843 % para literales de matriz 844 845La inicialización de una matriz se puede hacer en una declaración de asignación separada, que puede estar presente en el modelo o en un archivo de datos separado. 846 847Las matrices pueden ser accedidos. Ver :ref:`spec-Array-Access-Expressions` para más detalles. 848 849|TyInsts| 850El tamaño de una matriz debe ser fijo. Sus índices también deben tener inserciones de tipo fijo. Sus elementos pueden ser fijos o no. 851 852|TySyntax| 853Un arreglo base de una expresión de tipo-instanciación tiene la siguiente sintaxis: 854 855.. literalinclude:: grammar.mzn 856 :language: minizincdef 857 :start-after: % Array type-inst expressions 858 :end-before: % 859 860Algunos ejemplos de arreglos de expresiones de tipo-instanciación: 861 862.. code-block:: minizinc 863 864 array[1..10] of int 865 list of var int 866 867Tenga en cuenta que :mzndef:`list of <T>` es solo sintáctico para :mzndef:`array[int] of <T>`. *Justificación: Las matrices con índices enteros de este formulario son muy comunes y merecen un soporte especial para facilitar las cosas a los modeladores. Implementarlo usando azúcar sintáctico evita agregar un tipo extra al lenguaje, lo que simplifica las cosas para los implementadores.* 868 869Como las matrices deben ser de tamaño fijo, es un error tipo-instanciación que precede a una expresión tipo-instanciación de matriz con :mzn:`var`. 870 871|TyFiniteType| 872Sí, si los tipos de índice y el tipo de elemento son todos tipos finitos. 873De otra manera no. 874 875El dominio de un tipo de matriz que es una matriz finita es el conjunto de todas las matrices distintas cuyo conjunto de índices es igual al dominio del tipo de índice y cuyos elementos son del tipo de elemento de matriz. 876 877|TyVarifiable| 878No. 879 880|TyOrdering| 881Las matrices se ordenan lexicográficamente, tomando la ausencia de un valor para una clave dada antes de cualquier valor para esa clave. Por ejemplo, 882:mzn:`[1, 1]` es menor que 883:mzn:`[1, 2]`, que es menor que :mzn:`[1, 2, 3]` y 884:mzn:`array1d(2..4,[0, 0, 0])` que es menor que :mzn:`[1, 2, 3]`. 885 886|TyInit| 887Una variable de matriz indexada explícitamente debe inicializarse en instancia-tiempo solo si sus elementos deben inicializarse en el momento de la instancia. 888Una variable de matriz indexada implícitamente se debe inicializar en el momento de la instancia para que se conozca su longitud y conjunto de índices. 889 890|TyCoercions| 891:mzn:`array[TI0] of TI` |coerce| :mzn:`array[UI0] of UI` si 892:mzn:`TI0` |coerce| :mzn:`UI0` y :mzn:`TI` |coerce| :mzn:`UI`. 893 894.. _spec-option-types: 895 896 897 898 899Tipos de opciones 900+++++++++++++++++ 901 902|TyOverview| 903Los tipos de opciones definidos usando el constructor de tipo :mzn:`opt`, definen tipos que pueden o no estar allí. Son similares a tipos ``Puede`` (``Maybe``) de la implicidad de Haskell agrega un nuevo valor :mzn:`<>` al tipo. 904 905 906|TyInsts| 907El argumento de un tipo de opción debe ser uno de los tipos base :mzn:`bool`, :mzn:`int` o :mzn:`float`. 908 909|TySyntax| 910El tipo de opción está escrito :mzndef:`opt <T>` donde :mzndef:`<T>` si es uno de los tres tipos base, o una de sus instancias restringidas. 911 912|TyFiniteType| 913Sí, si el tipo subyacente es finito, de lo contrario no. 914 915|TyVarifiable| 916Sí. 917 918|TyOrdering| 919:mzn:`<>` siempre es menor que cualquier otro valor en el tipo. 920Pero ten cuidado con la sobrecarga de operadores como :mzn:`<`, que es diferente para los tipos de opciones. 921 922|TyInit| 923Una variable de tipo :mzn:`opt` no necesita ser inicializado en el momento de la instancia. Un tipo de variable sin inicializar :mzn:`opt` se inicializa automáticamente a :mzn:`<>`. 924 925|TyCoercions| 926:mzn:`TI` |coerce| :mzn:`opt UI` si :mzn:`TI` |coerce| :mzn:`UI`.. 927 928.. _spec-the-annotation-type: 929 930 931 932El Tipo de Anotación 933++++++++++++++++++++ 934 935|TyOverview| 936El tipo de anotación, :mzn:`ann`, se puede usar para representar estructuras de términos arbitrarios. Se aumenta con elementos de anotación (:ref:`spec-Annotation-Items`). 937 938|TyInsts| 939:mzn:`ann` siempre se considera no fijado, ya que puede contener elementos no fijadas. No puede ser precedido por :mzn:`var`. 940 941|TySyntax| 942El tipo de anotación está escrito :mzn:`ann`. 943 944|TyFiniteType| 945No. 946 947|TyVarifiable| 948No. 949 950|TyOrdering| 951N/A. Los tipos de anotación no tienen un orden definido en ellos. 952 953|TyInit| 954Una variable :mzn:`ann` debe inicializarse en el momento de la instancia. 955 956|TyCoercions| 957Ninguna. 958 959 960.. _spec-constrained-type-insts: 961 962 963 964 965Restricciones de Tipo-instanciación 966~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 967 968Una poderosa característica de MiniZinc es *restricciones de tipo-instanciación*. Una restricción de tipo-instanciación es una versión restringida de *base* tipo-instanciación, ejemplo, un tipo-instanciación con un menor número de valores en su dominio. 969 970.. _spec-set-expression-type-insts: 971 972 973 974Conjunto de expresiones de Tipo-instanciación 975+++++++++++++++++++++++++++++++++++++++++++++ 976 977Se pueden usar tres tipos de expresiones en tipo-instanciación. 978 979#. Rangos enteros: ejemplos. :mzn:`1..3`. 980#. Conjunto de literales: ejemplos. :mzn:`var {1,3,5}`. 981#. Identifiers: el nombre de un parámetro establecido (que puede ser global, let-local, el argumento de un predicado o función, o un valor de generador) puede servir como tipo-instanciación. 982 983En cada caso, el tipo de base es el de los elementos del conjunto, y los valores dentro del conjunto sirven como el dominio. Por ejemplo, mientras que una variable con tipo-instanciación :mzn:`var int` puede tomar cualquier valor entero, una variable con tipo-instanciación :mzn:`var 1..3` solo puede tomar el valor 1, 2 o 3. 984 985Todas las expresiones establecidas de tipo-instanciación son tipos finitos. Su dominio es igual al conjunto en sí. 986 987 988 989Rango de los números de Tipo-instanciación 990++++++++++++++++++++++++++++++++++++++++++ 991 992Los rangos de los números de punto flotantes se pueden usar como tipo-instanciación. Por ejemplo, :mzn:`1.0 .. 3.0`. 993Estos se tratan de manera similar al rango entero tipo-instanciación, a pesar de que :mzn:`1.0 .. 3.0` no es una expresión válida mientras es :mzn:`1 .. 3`. 994 995Los rangos de números de punto flotante no son tipos finitos. 996 997.. _spec-expressions: 998 999 1000 1001Expresiones 1002----------- 1003 1004.. _spec-expressions-overview: 1005 1006 1007 1008Resumen de expresiones 1009~~~~~~~~~~~~~~~~~~~~~~ 1010 1011Las expresiones representan valores. Ocurren en varios tipos de artículos. Tienen la siguiente sintaxis: 1012 1013.. literalinclude:: grammar.mzn 1014 :language: minizincdef 1015 :start-after: % Expressions 1016 :end-before: % 1017 1018Las expresiones se pueden componer a partir de subexpresiones combinadas con operadores. 1019Todos los operadores (binarios y unarios) se describen en :ref:`spec-Operators`, incluyendo las precedencias de los operadores binarios. Todos los operadores unarios se unen más estrechamente que todos los operadores binarios. 1020 1021Las expresiones pueden tener una o más anotaciones. Las anotaciones se vinculan más estrechamente que las aplicaciones de operador unario y binario, pero menos estrechamente que las operaciones de acceso y las aplicaciones que no son de operador. En algunos casos, este enlace no es intuitivo. Por ejemplo, en las primeras tres de las siguientes líneas, la anotación :mzn:`a` se une a la expresión del identificador :mzn:`x` en lugar de la aplicación del operador. Sin embargo, la cuarta línea presenta una aplicación sin operador (debido a las comillas simples alrededor del :mzn:`not`) y entonces la anotación se une a toda la aplicación. 1022 1023.. code-block:: minizinc 1024 1025 not x::a; 1026 not (x)::a; 1027 not(x)::a; 1028 'not'(x)::a; 1029 1030:ref:`spec-Annotations` tiene más en anotaciones. 1031 1032Las expresiones se pueden contener entre paréntesis. 1033 1034Las operaciones de acceso a la matriz se unen más estrechamente que las anotaciones y operadores unarios y binarios. 1035Se describen con más detalle en :ref:`spec-Array-Access-Expressions`. 1036 1037Los tipos restantes de átomos de expresión (from :mzndef:`<ident>` a 1038:mzndef:`<gen-call-expr>`) están descritos en 1039:ref:`spec-Identifier-Expressions-and-Quoted-Operator-Expressions` a :ref:`spec-Generator-Call-Expressions`. 1040 1041También distinguimos expresiones numéricas sintácticamente válidas. Esto permite que los tipos de rango sean analizados correctamente. 1042 1043.. literalinclude:: grammar.mzn 1044 :language: minizincdef 1045 :start-after: % Numeric expressions 1046 :end-before: % 1047 1048.. _spec-operators: 1049 1050 1051 1052Operadores 1053~~~~~~~~~~ 1054 1055Los operadores son funciones que se distinguen por su sintaxis de una o dos formas. Primero, algunos de ellos contienen caracteres no alfanuméricos que las funciones normales no (por ejemplo, :mzn:`+`). Segundo, su aplicación está escrita de una manera diferente a las funciones normales. 1056 1057Distinguimos entre operadores binarios, que se pueden aplicar de manera infija (por ejemplo, :mzn:`3 + 4`), y operadores unarios, que se pueden aplicar de manera prefija sin paréntesis (por ejemplo, :mzn:`not x`). También distinguimos entre operadores integrados y operadores definidos por el usuario. La sintaxis es la siguiente: 1058 1059.. literalinclude:: grammar.mzn 1060 :language: minizincdef 1061 :start-after: % Built-in operators 1062 :end-before: % 1063 1064Nuevamente, distinguimos sintácticamente operadores numéricos. 1065 1066.. literalinclude:: grammar.mzn 1067 :language: minizincdef 1068 :start-after: % Built-in numeric operators 1069 :end-before: % 1070 1071Algunos operadores se pueden escribir utilizando sus símbolos Unicode, que se enumeran en :numref:`bin-ops-unicode` (recuerde que la entrada de MiniZinc es UTF-8). 1072 1073.. _bin-ops-unicode: 1074 1075.. cssclass:: table-nonfluid table-bordered 1076 1077.. table:: Unicode equivalents of binary operators 1078 1079 1080 ================ ======================= ============ 1081 Operador Símbolo Unicode symbol Código UTF-8 1082 ================ ======================= ============ 1083 :mzn:`<->` :math:`\leftrightarrow` E2 86 94 1084 :mzn:`->` :math:`\rightarrow` E2 86 92 1085 :mzn:`<-` :math:`\leftarrow` E2 86 90 1086 :mzn:`not` :math:`\lnot` C2 AC 1087 ``\/`` :math:`\lor` E2 88 A8 1088 ``/\`` :math:`\land` E2 88 A7 1089 :mzn:`!=` :math:`\neq` E2 89 A0 1090 :mzn:`<=` :math:`\leq` E2 89 A4 1091 :mzn:`>=` :math:`\geq` E2 89 A5 1092 :mzn:`in` :math:`\in` E2 88 88 1093 :mzn:`subset` :math:`\subseteq` E2 8A 86 1094 :mzn:`superset` :math:`\supseteq` E2 8A 87 1095 :mzn:`union` :math:`\cup` E2 88 AA 1096 :mzn:`intersect` :math:`\cap` E2 88 A9 1097 ================ ======================= ============ 1098 1099Los operadores binarios se enumeran en :numref:`bin-ops`. Un número de precedencia más bajo significa un enlace más estricto; por ejemplo, :mzn:`1+2*3` es analizado como :mzn:`1+(2*3)` porque :mzn:`*` se une más fuerte que :mzn:`+`. La asociatividad indica cómo se manejan las cadenas de operadores con igual precedencia; por ejemplo, :mzn:`1+2+3` es analizado como :mzn:`(1+2)+3` porque :mzn:`+` es de izquierda asociativo, :mzn:`a++b++c` es analizado como :mzn:`a++(b++c)` porque :mzn:`++` es asociativo por la derecha, y :mzn:`1<x<2` es un error de sintaxis porque :mzn:`<` no es asociativo. 1100 1101.. _bin-ops: 1102 1103.. cssclass:: table-nonfluid table-bordered 1104 1105.. table:: Binary infix operators 1106 1107 =============================== ========== =========== 1108 Symbolo(s) Asociación Precedencia 1109 =============================== ========== =========== 1110 :mzn:`<->` izquierda 1200 1111 1112 :mzn:`->` izquierda 1100 1113 :mzn:`<-` izquierda 1100 1114 1115 ``\/`` izquierda 1000 1116 :mzn:`xor` izquierda 1000 1117 1118 ``/\`` izquierda 900 1119 1120 :mzn:`<` ninguna 800 1121 :mzn:`>` ninguna 800 1122 :mzn:`<=` ninguna 800 1123 :mzn:`>=` ninguna 800 1124 :mzn:`==`, 1125 :mzn:`=` ninguna 800 1126 :mzn:`!=` ninguna 800 1127 1128 :mzn:`in` ninguna 700 1129 :mzn:`subset` ninguna 700 1130 :mzn:`superset` ninguna 700 1131 1132 :mzn:`union` izquierda 600 1133 :mzn:`diff` izquierda 600 1134 :mzn:`symdiff` izquierda 600 1135 1136 :mzn:`..` ninguna 500 1137 1138 :mzn:`+` izquierda 400 1139 :mzn:`-` izquierda 400 1140 1141 :mzn:`*` izquierda 300 1142 :mzn:`div` izquierda 300 1143 :mzn:`mod` izquierda 300 1144 :mzn:`/` izquierda 300 1145 :mzn:`intersect` izquierda 300 1146 1147 :mzn:`++` derecha 200 1148 1149 ````` :mzndef:`<ident>` ````` izquierda 100 1150 =============================== ========== =========== 1151 1152 1153Un operador binario definido por el usuario se crea mediante el retroceso de un identificador normal, por ejemplo: 1154 1155.. code-block:: minizinc 1156 1157 A `min2` B 1158 1159Este es un error estático si el identificador no es el nombre de una función o predicado binario. 1160 1161Los operadores unarios son: :mzn:`+`, :mzn:`-` y :mzn:`not`. 1162Los operadores unarios definidos por el usuario no son posibles. 1163 1164Como explica:ref:`spec-Identifiers`, cualquier operador incorporado se puede usar como un identificador de función normal citándolo, por ejemplo: :mzn:`'+'(3, 4)` es equivalente a :mzn:`3 + 4`. 1165 1166El significado de cada operador se da en :ref:`spec-builtins`. 1167 1168 1169 1170 1171Expresiones atómicas 1172~~~~~~~~~~~~~~~~~~~~ 1173 1174.. _spec-Identifier-Expressions-and-Quoted-Operator-Expressions: 1175 1176Expresiones de identificador y expresiones de operador entrecomilladas 1177++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1178 1179Las expresiones de identificador y las expresiones de operador entre comillas tienen la siguiente sintaxis: 1180 1181.. literalinclude:: grammar.mzn 1182 :language: minizincdef 1183 :start-after: % Identifiers and quoted operators 1184 :end-before: % 1185 1186Se dieron ejemplos de identificadores en :ref:`spec-Identifiers`. Los siguientes son ejemplos de operadores cotizados: 1187 1188.. code-block:: minizinc 1189 1190 '+' 1191 'union' 1192 1193En los operadores citados, el espacio en blanco no está permitido entre la cotización y el operador. :ref:`spec-Operators` enumera los operadores incorporados de MiniZinc. 1194 1195Sintácticamente, cualquier identificador o operador citado puede servir como una expresión. 1196Sin embargo, en un modelo válido, cualquier identificador o operador citado que sirva como expresión debe ser el nombre de una variable. 1197 1198.. _spec-Anonymous-Decision-Variables: 1199 1200 1201 1202Variables de decisión anónimas 1203++++++++++++++++++++++++++++++ 1204 1205Hay un identificador especial, :mzn:`_`, que representa una variable de decisión anónima no fija. Puede tomar cualquier tipo que pueda ser una variable de decisión. Es particularmente útil para inicializar variables de decisión dentro de tipos compuestos. Por ejemplo, en la siguiente matriz, los elementos primero y tercero se fijan en 1 y 3, respectivamente, y los elementos segundo y cuarto no están fijos: 1206 1207.. code-block:: minizinc 1208 1209 array[1..4] of var int: xs = [1, _, 3, _]; 1210 1211Cualquier expresión que no contenga :mzn:`_` y no involucra variables de decisión, por lo que es fijo. 1212 1213 1214 1215 1216Literales booleanos 1217+++++++++++++++++++ 1218 1219Los literales booleanos tienen esta sintaxis: 1220 1221.. literalinclude:: grammar.mzn 1222 :language: minizincdef 1223 :start-after: % Boolean literals 1224 :end-before: % 1225 1226 1227 1228Entero y Literales de números de punto flotante 1229+++++++++++++++++++++++++++++++++++++++++++++++ 1230 1231Hay tres formas de literales enteros: decimal, hexadecimal y octal, con estas formas respectivas: 1232 1233.. literalinclude:: grammar.mzn 1234 :language: minizincdef 1235 :start-after: % Integer literals 1236 :end-before: % 1237 1238Por ejemplo: :mzn:`0`, :mzn:`005`, :mzn:`123`, :mzn:`0x1b7`, :mzn:`0o777`; pero no :mzn:`-1`. 1239 1240Los literales de punto flotante poseen la siguiente forma: 1241 1242.. literalinclude:: grammar.mzn 1243 :language: minizincdef 1244 :start-after: % Float literals 1245 :end-before: % 1246 1247Por ejemplo: :mzn:`1.05`, :mzn:`1.3e-5`, :mzn:`1.3+e5`; pero no :mzn:`1.`, :mzn:`.5`, :mzn:`1.e5`, :mzn:`.1e5`, :mzn:`-1.0`, :mzn:`-1E05`. 1248 1249Un símbolo :mzn:`-` precede a un entero o literal de número flotante se analiza como unario menos (ndependientemente del espacio en blanco intermedio), no como parte del literal. Esto se debe a que, en general, no es posible distinguir una :mzn:`-` para un entero negativo o literal de número flotante de un binario menos cuando se lee. 1250 1251.. _spec-String-Interpolation-Expressions: 1252 1253 1254 1255 1256Literales de cadenas e interpolación de cadenas 1257+++++++++++++++++++++++++++++++++++++++++++++++ 1258 1259Los literales de cadena se escriben como en C: 1260 1261.. literalinclude:: grammar.mzn 1262 :language: minizincdef 1263 :start-after: % String literals 1264 :end-before: % 1265 1266Esto incluye secuencias de escape estilo C, como :mzn:`\"` para comillas dobles, :mzn:`\\` para la barra invertida, y :mzn:`\n` para nueva línea. 1267 1268Por ejemplo: :mzn:`"Hello, world!\n"`. 1269 1270Los literales de cadena deben caber en una sola línea. 1271 1272Los literales de cadena larga se pueden dividir en varias líneas mediante la concatenación de cadenas. Por ejemplo: 1273 1274.. code-block:: minizinc 1275 1276 string: s = "This is a string literal " 1277 ++ "split across two lines."; 1278 1279Una expresión de cadena puede contener una expresión arbitraria de MiniZinc, que se convertirá en una cadena similar a la función builtin :mzn:`show` y se insertará en la cadena. 1280 1281Por ejemplo: 1282 1283.. code-block:: minizinc 1284 1285 var set of 1..10: q; 1286 solve satisfy; 1287 output [show("The value of q is \(q), and it has \(card(q)) elements.")]; 1288 1289.. _spec-set-literals: 1290 1291 1292 1293Establecer Literales 1294++++++++++++++++++++ 1295 1296Los literales establecidos tienen esta sintaxis: 1297 1298.. literalinclude:: grammar.mzn 1299 :language: minizincdef 1300 :start-after: % Set literals 1301 :end-before: % 1302 1303Por ejemplo: 1304 1305.. code-block:: minizinc 1306 1307 { 1, 3, 5 } 1308 { } 1309 { 1, 2.0 } 1310 1311La instanciación de tipo de todos los elementos en un conjunto literal debe ser la misma, o coercible para la misma instancia de tipo (como en el último ejemplo anterior, donde el entero :mzn:`1` será coaccionado a un :mzn:`float`). 1312 1313 1314.. _spec-set-comprehensions: 1315 1316 1317 1318 1319 1320Establecer comprensiones 1321++++++++++++++++++++++++ 1322 1323Las comprensiones establecidas tienen esta sintaxis: 1324 1325.. literalinclude:: grammar.mzn 1326 :language: minizincdef 1327 :start-after: % Set comprehensions 1328 :end-before: % 1329 1330Por ejemplo (con el equivalente literal a la derecha): 1331 1332.. code-block:: minizinc 1333 1334 { 2*i | i in 1..5 } % { 2, 4, 6, 8, 10 } 1335 { 1 | i in 1..5 } % { 1 } (no duplicates in sets) 1336 1337La expresión antes del :mzn:`|` es la *expresión de la cabeza*. La expresión después del :mzn:`in` es una *expresión del generador*. 1338Los generadores pueden ser restringidos por una expresión mientras (*where-expression*). Por ejemplo: 1339 1340.. code-block:: minizinc 1341 1342 { i | i in 1..10 where (i mod 2 = 0) } % { 2, 4, 6, 8, 10 } 1343 1344Cuando hay múltiples generadores presentes, el generador que está más a la derecha actúa como el más interno. Por ejemplo: 1345 1346.. code-block:: minizinc 1347 1348 { 3*i+j | i in 0..2, j in {0, 1} } % { 0, 1, 3, 4, 6, 7 } 1349 1350El alcance de las variables del generador local viene dado por las siguientes reglas: 1351 1352- Son visibles dentro de la expresión de la cabeza (antes de :mzn:`|`). 1353- Son visibles dentro de la expresión mientras (where-expression). 1354- Son visibles dentro de las expresiones del generador en cualquier generador posterior. 1355 1356La última de estas reglas significa que se permite la siguiente comprensión del conjunto: 1357 1358.. code-block:: minizinc 1359 1360 { i+j | i in 1..3, j in 1..i } % { 1+1, 2+1, 2+2, 3+1, 3+2, 3+3 } 1361 1362Una expresión de generador debe ser una matriz o un conjunto fijo. 1363 1364*Razón fundamental: Para las comprensiones del conjunto, los generadores de conjuntos serían suficientes, pero para las comprensiones de matriz, se requieren generadores de matriz para una expresividad total (ejemplo., para proporcionar control sobre el orden de los elementos en la matriz resultante). Las comprensiones de conjuntos tienen generadores de matriz para coherencia con las comprensiones de matriz, lo que hace que las implementaciones sean más simples.* 1365 1366 1367La expresión mientras (si está presente) debe ser booleano. 1368Puede ser ``var``, en cuyo caso el tipo de comprensión se eleva a un tipo opcional. Solo una donde se permite la expresión por comprensión. 1369 1370*Razón fundamental: 1371Permitir una expresión-donde por generador es otra posibilidad, y una que aparentemente podría dar como resultado una evaluación más eficiente en algunos casos. Por ejemplo, considere la siguiente comprensión:* 1372 1373.. code-block:: minizinc 1374 1375 [f(i, j) | i in A1, j in A2 where p(i) /\ q(i,j)] 1376 1377*Si se permitieran múltiples expresiones-where, esto podría expresarse más eficientemente de la siguiente manera, lo que evita las "iteraciones de bucle interno" infructuosas para cada "iteración de bucle externo" que no satisface* :mzn:`p(i)`: 1378 1379.. code-block:: minizinc 1380 1381 [f(i, j) | i in A1 where p(i), j in A2 where q(i,j)] 1382 1383*Sin embargo, esta eficiencia también se puede lograr con comprensiones anidadas:* 1384 1385.. code-block:: minizinc 1386 1387 [f(i, j) | i in [k | k in A1 where p(k)], j in A2 where q(i,j)] 1388 1389*Por lo tanto, una sola expresión de dónde es todo lo que es compatible.* 1390 1391.. _spec-array-literals: 1392 1393 1394 1395Literales de matrices 1396+++++++++++++++++++++ 1397 1398Los literales de matriz tienen esta sintaxis: 1399 1400.. literalinclude:: grammar.mzn 1401 :language: minizincdef 1402 :start-after: % Array literals 1403 :end-before: % 1404 1405Por ejemplo: 1406 1407.. code-block:: minizinc 1408 1409 [1, 2, 3, 4] 1410 [] 1411 [1, _] 1412 1413 1414En una matriz literal, todos los elementos deben tener la misma instancia de tipo, o ser coercibles para la misma instancia de tipo (como en el último ejemplo anterior, donde el entero fijo :mzn:`1` será coaccionado a un :mzn:`var int`). 1415 1416Los índices de una matriz literal son implícitamente :mzn:`1..n`, donde :mzn:`n` es la longitud del literal. 1417 1418.. _spec-2d-array-literals: 1419 1420 1421 1422Arreglos literales en 2d 1423++++++++++++++++++++++++ 1424 1425Los literales simples de arreglos 2d tienen esta sintaxis: 1426 1427.. literalinclude:: grammar.mzn 1428 :language: minizincdef 1429 :start-after: % 2D Array literals 1430 :end-before: % 1431 1432Por ejemplo: 1433 1434.. code-block:: minizinc 1435 1436 [| 1, 2, 3 1437 | 4, 5, 6 1438 | 7, 8, 9 |] % array[1..3, 1..3] 1439 [| x, y, z |] % array[1..1, 1..3] 1440 [| 1 | _ | _ |] % array[1..3, 1..1] 1441 1442En un 2d array literal, cada sub-array debe tener la misma longitud. 1443 1444En un 2d array literal, todos los elementos deben tener la misma instancia de tipo, o ser coercibles para el mismo tipo de instanciación (como en el último ejemplo anterior, donde el entero fijo :mzn:`1` será coaccionado a un :mzn:`var int`). 1445 1446Los índices de un 2d array literal están implícitamente :mzn:`(1,1)..(m,n)`, donde :mzn:`m` y :mzn:`n` están determinados por la forma del literal. 1447 1448 1449.. _spec-array-comprehensions: 1450 1451 1452 1453 1454Arreglo de Comprensiones 1455++++++++++++++++++++++++ 1456 1457Arreglo de Comprensiones tienen la siguiente sintaxis: 1458 1459.. literalinclude:: grammar.mzn 1460 :language: minizincdef 1461 :start-after: % Array comprehensions 1462 :end-before: % 1463 1464Por ejemplo (con los equivalentes literales a la derecha): 1465 1466.. code-block:: minizinc 1467 1468 [2*i | i in 1..5] % [2, 4, 6, 8, 10] 1469 1470Arreglo de Comprensiones tener requisitos de tipo e instanciación más flexibles que las comprensiones establecidas (see :ref:`spec-Set-Comprehensions`). 1471 1472Arreglo de Comprensiones se permiten sobre un conjunto de variables con tipo finito, el resultado es una matriz de tipo opcional, con una longitud igual a la cardinalidad del límite superior del conjunto de variables. 1473 1474Por ejemplo: 1475 1476.. code-block:: minizinc 1477 1478 var set of 1..5: x; 1479 array[int] of var opt int: y = [ i * i | i in x ]; 1480 1481La longitud de la matriz será 5. 1482 1483Se permiten las comprensiones de matriz donde la expresión mientras es :mzn:`var bool`. 1484De nuevo, la matriz resultante es de tipo opcional, y de longitud igual a la dada por las expresiones del generador. 1485Por ejemplo: 1486 1487.. code-block:: minizinc 1488 1489 var int x; 1490 array[int] of var opt int: y = [ i | i in 1..10 where i != x ]; 1491 1492La longitud de la matriz será 10. 1493 1494Los índices de una comprensión de matriz simple evaluada son implícitamente 1495:mzn:`1..n`, donde :mzn:`n` es la duración de la comprensión evaluada. 1496 1497.. _spec-array-access-expressions: 1498 1499 1500 1501Expresiones de Matriz de Acceso 1502+++++++++++++++++++++++++++++++ 1503 1504Se accede a los elementos de matriz usando corchetes después de una expresión: 1505 1506.. literalinclude:: grammar.mzn 1507 :language: minizincdef 1508 :start-after: % Array access 1509 :end-before: % 1510 1511Por ejemplo: 1512 1513.. code-block:: minizinc 1514 1515 int: x = a1[1]; 1516 1517Si todos los índices utilizados en un arreglo de acceso son fijos, la tipo-instanciación del resultado es la misma que el elemento tipo-instanciación. Sin embargo, si los índices no son fijos, la tipo-instanciación del resultado es el elemento varificado tipo-instanciación. Por ejemplo, si tenemos: 1518 1519.. code-block:: minizinc 1520 1521 array[1..2] of int: a2 = [1, 2]; 1522 var int: i; 1523 1524Entonces el tipo-instanciación de :mzn:`a2[i]` es :mzn:`var int`. Si el elemento tipo-instanciación no es variable, tal acceso causa un error estático. 1525 1526Se accede a matrices multidimensionales usando índices separados por comas. 1527 1528.. code-block:: minizinc 1529 1530 array[1..3,1..3] of int: a3; 1531 int: y = a3[1, 2]; 1532 1533Los índices deben coincidir con el tipo de conjunto de índice de la matriz. Por ejemplo, una matriz declarada con un conjunto de índices enum solo se puede acceder usando índices de esa enumeración. 1534 1535.. code-block:: minizinc 1536 1537 enum X = {A,B,C}; 1538 array[X] of int: a4 = [1,2,3]; 1539 int: y = a4[1]; % tipo de índice incorrecto 1540 int: z = a4[B]; % correcto 1541 1542 1543Literales de Anotación 1544++++++++++++++++++++++ 1545 1546Literales del tipo :mzn:`ann` tiene la siguiente sintaxis: 1547 1548.. literalinclude:: grammar.mzn 1549 :language: minizincdef 1550 :start-after: % Annotation literals 1551 :end-before: % 1552 1553Por ejemplo: 1554 1555.. code-block:: minizinc 1556 1557 foo 1558 cons(1, cons(2, cons(3, nil))) 1559 1560No hay forma de inspeccionar o deconstruir literales de anotación en un modelo MiniZinc; están destinados a ser inspeccionados solo por una implementación, por ejemplo, para dirigir la compilación. 1561 1562 1563 1564 1565 1566 1567Expresiones Si-Entonces-Sino (If-then-else) 1568+++++++++++++++++++++++++++++++++++++++++++ 1569 1570MiniZinc proporciona expresiones if-then-else, que proporcionan una selección de dos alternativas basadas en una condición. Ellos tienen esta sintaxis: 1571 1572.. literalinclude:: grammar.mzn 1573 :language: minizincdef 1574 :start-after: % If-then-else expressions 1575 :end-before: % 1576 1577Por ejemplo: 1578 1579.. code-block:: minizinc 1580 1581 if x <= y then x else y endif 1582 if x < 0 then -1 elseif x > 0 then 1 else 0 endif 1583 1584La presencia del :mzn:`endif` evita la posible ambigüedad cuando una expresión if-then-else es parte de una expresión más grande. 1585 1586La instanciación de tipo de la :mzn:`if` la expresión debe ser :mzn:`par bool` o :mzn:`var bool`. 1587El :mzn:`then` y :mzn:`else` las expresiones deben tener el mismo tipo-instanciación o ser coercibles para el mismo tipo-instanciación, que también es el tipo-instanciación de toda la expresión. 1588 1589Si la expresión :mzn:`if` es :mzn:`var bool` entonces el tipo-instanciación de el :mzn:`then` y la expresión :mzn:`else` debe ser varificable. 1590 1591Si la expresión :mzn:`if` es :mzn:`par bool` entonces la evaluación de las expresiones if-then-else es floja (lazy): la condición es evaluada, y luego solo uno de los :mzn:`then` y :mzn:`else` las ramas se evalúan, dependiendo de si la condición tuvo éxito o falló. 1592Este no es el caso si es :mzn:`var bool`. 1593 1594 1595.. _spec-let-expressions: 1596 1597 1598Expresiones Let 1599+++++++++++++++ 1600 1601Las expresiones Let proporcionan una forma de introducir nombres locales para una o más expresiones y restricciones locales que se pueden usar dentro de otra expresión. Son particularmente útiles en operaciones definidas por el usuario. 1602 1603Las expresions ``let`` tienen la siguiente sintaxis: 1604 1605.. literalinclude:: grammar.mzn 1606 :language: minizincdef 1607 :start-after: % Let expressions 1608 :end-before: % 1609 1610Por ejemplo: 1611 1612.. code-block:: minizinc 1613 1614 let { int: x = 3, int: y = 4; } in x + y; 1615 let { var int: x; 1616 constraint x >= y /\ x >= -y /\ (x = y \/ x = -y); } 1617 in x 1618 1619El alcance de una variable local ``let`` abarca: 1620 1621- Las expresiones de tipo-instanciación e inicialización de cualquier variable posterior dentro de la expresión let (pero no la expresión de inicialización propia de la variable). 1622- La expresión después del :mzn:`in`, que es analizado tan codiciosamente como sea posible. 1623 1624Una variable solo puede declararse una vez en una expresión let. 1625 1626Por lo tanto, en los siguientes ejemplos, el primero es aceptable, pero el resto no: 1627 1628.. code-block:: minizinc 1629 1630 let { int: x = 3; int: y = x; } in x + y; % ok 1631 let { int: y = x; int: x = 3; } in x + y; % x not visible in y's defn. 1632 let { int: x = x; } in x; % x not visible in x's defn. 1633 let { int: x = 3; int: x = 4; } in x; % x declared twice 1634 1635.. 1636 The type-inst expressions can include type-inst variables if the let is 1637 within a function or predicate body in which the same type-inst variables 1638 were present in the function or predicate signature. 1639 TODO: type-inst variables are currently not fully supported 1640 1641El inicializador para una variable local let puede omitirse solo si la variable es una variable de decisión. Por ejemplo: 1642 1643.. code-block:: minizinc 1644 1645 let { var int: x; } in ...; % ok 1646 let { int: x; } in ...; % illegal 1647 1648La tipo-instanciación de toda la expresión let es la tipo-instanciación de la expresión después de la palabra clave :mzn:`in`. 1649 1650Hay una complicación que involucra expresiones de let en contextos negativos. Una expresión ``let`` ocurre en un contexto negativo si ocurre en una expresión de la forma :mzn:`not X`, :mzn:`X <-> Y}` o en la sub-expresión 1651:mzn:`X` en :mzn:`X -> Y` o :mzn:`Y <- X`, o en una subexpresion 1652:mzn:`bool2int(X)`. 1653 1654Las restricciones en las expresiones de let flotan al contexto booleano circundante más cercano. Por ejemplo 1655 1656.. code-block:: minizinc 1657 1658 constraint b -> x + let { var 0..2: y; constraint y != -1;} in y >= 4; 1659 1660Es equivalente a: 1661 1662.. code-block:: minizinc 1663 1664 var 0..2: y; 1665 constraint b -> (x + y >= 4 /\ y != 1); 1666 1667 1668 1669Expresiones de llamada 1670++++++++++++++++++++++ 1671 1672Las expresiones de llamada se usan para llamar predicados y funciones. 1673 1674Las expresiones de llamada tienen esta sintaxis: 1675 1676.. literalinclude:: grammar.mzn 1677 :language: minizincdef 1678 :start-after: % Call expressions 1679 :end-before: % 1680 1681Por ejemplo: 1682 1683.. code-block:: minizinc 1684 1685 x = min(3, 5); 1686 1687 1688El tipo-instanciación de las expresiones pasadas como argumentos debe coincidir con los tipos de argumento de las llamadas predicado/función. El tipo de retorno del predicado/función también debe ser apropiado para el contexto de llamada. 1689 1690Tenga en cuenta que una llamada a una función o predicado sin argumentos es sintácticamente indistinguible del uso de una variable, y así debe determinarse durante la comprobación de tipo-instanciación. 1691 1692La evaluación de los argumentos en las expresiones de llamada es estricta: todos los argumentos se evalúan antes de que se evalúe la llamada. Tenga en cuenta que esto incluye operaciones booleanas como ``/\``, ``\/``, :mzn:`->` y :mzn:`<-` que podría ser flojo (lazy) en un argumento. La única excepción es :mzn:`assert`, que es flojo en su tercer argumento (:ref:`spec-Other-Operations`). 1693 1694*Razón fundamental: Las operaciones booleanas son estrictas porque: 1695(a) esto minimiza casos excepcionales; 1696(b) en una expresión como* :mzn:`A -> B` *donde* :mzn:`A` *no es fijo y* :mzn:`B` *provoca un aborto, el comportamiento apropiado no está claro si la pereza está presente; y 1697(c) si un usuario necesita laziness, un if-then-else puede ser usado.* 1698 1699El orden de evaluación de los argumentos no está especificado. *Justificación: debido a que MiniZinc es declarativo, no existe una necesidad obvia de especificar una orden de evaluación, y dejarla sin especificar da a los implementadores cierta libertad.* 1700 1701.. _spec-generator-call-expressions: 1702 1703 1704 1705Expresiones de Generador de llamadas 1706++++++++++++++++++++++++++++++++++++ 1707 1708MiniZinc tiene una sintaxis especial para ciertos tipos de expresiones de llamada lo que hace que los modelos sean mucho más legibles. 1709 1710Las expresiones de llamada del generador tienen esta sintaxis: 1711 1712.. literalinclude:: grammar.mzn 1713 :language: minizincdef 1714 :start-after: % Generator call expressions 1715 :end-before: % 1716 1717Una expresión de llamada del generador :mzn:`P(Gs)(E)` es equivalente a la expresión de llamada :mzn:`P([E | Gs])`. 1718Por ejemplo, la expresión: 1719 1720.. code-block:: minizinc 1721 1722 forall(i,j in Domain where i<j) 1723 (noattack(i, j, queens[i], queens[j])); 1724 1725(en un modelo que especifica el problema N-Reinas) es equivalente a: 1726 1727.. code-block:: minizinc 1728 1729 forall( [ noattack(i, j, queens[i], queens[j]) 1730 | i,j in Domain where i<j ] ); 1731 1732Los paréntesis alrededor de la última expresión son obligatorios; esto evita una posible confusión cuando la expresión de llamada del generador es parte de una expresión más grande. 1733 1734El identificador debe ser el nombre de un predicado o función unaria que toma un argumento de matriz. 1735 1736Los generadores y expresión-mientras (si está presente) tienen los mismos requisitos que aquellos en las comprensiones de matriz (:ref:`spec-Array-Comprehensions`). 1737 1738.. _spec-items: 1739 1740 1741 1742 1743Elementos 1744--------- 1745 1746Esta sección describe los elementos del programa de nivel superior. 1747 1748.. _spec-include-items: 1749 1750 1751 1752Incluir elementos 1753~~~~~~~~~~~~~~~~~~~~ 1754 1755Incluir elementos permite dividir un modelo en varios archivos. Ellos tienen esta sintaxis: 1756 1757.. literalinclude:: grammar.mzn 1758 :language: minizincdef 1759 :start-after: % Include items 1760 :end-before: % 1761 1762Por ejemplo: 1763 1764.. code-block:: minizinc 1765 1766 include "foo.mzn"; 1767 1768Incluye el archivo ``foo.mzn``. 1769 1770Incluir elementos es particularmente útil para acceder a bibliotecas o dividir modelos grandes en piezas pequeñas. Ellos no son, como :ref:`spec-Model-Instance-Files` explica, utilizado para especificar archivos de datos. 1771 1772Si el nombre de pila no es completo, el archivo se busca en un conjunto de directorios definido por la implementación. Los directorios de búsqueda deben poder modificarse con una opción de línea de comando. 1773 1774.. _spec-declarations: 1775 1776 1777 1778Elementos de declaración variable 1779~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 1780 1781Las declaraciones de variables tienen esta sintaxis: 1782 1783.. literalinclude:: grammar.mzn 1784 :language: minizincdef 1785 :start-after: % Variable declaration items 1786 :end-before: % 1787 1788Por ejemplo: 1789 1790.. code-block:: minizinc 1791 1792 int: A = 10; 1793 1794Es un error de instantación de tipo si una variable se declara y/o define más de una vez en un modelo. 1795 1796Una variable cuya declaración no incluye una asignación se puede inicializar mediante un elemento de asignación por separado (:ref:`spec-Assignments`). Por ejemplo, el artículo anterior se puede separar en los siguientes dos elementos: 1797 1798.. code-block:: minizinc 1799 1800 int: A; 1801 ... 1802 A = 10; 1803 1804Todas las variables que contienen un componente de parámetro deben definirse en instancia-tiempo. 1805 1806Las variables pueden tener una o más anotaciones. :ref:`spec-Annotations` tiene más en las anotaciones. 1807 1808 1809.. _spec-enum_items: 1810 1811 1812 1813 1814 1815 1816Elementos de Enumeración 1817~~~~~~~~~~~~~~~~~~~~~~~~ 1818 1819Los elementos de tipo enumerados tienen esta sintaxis: 1820 1821.. literalinclude:: grammar.mzn 1822 :language: minizincdef 1823 :start-after: % Enum items 1824 :end-before: % 1825 1826Un ejemplo de una enumeración: 1827 1828.. code-block:: minizinc 1829 1830 enum country = {Australia, Canada, China, England, USA}; 1831 1832Cada alternativa se llama *caso de enumeración (enum case)*. El identificador utilizado para nombrar cada caso (por ejemplo, :mzn:`Australia`) se llama el *nombre del caso enum (enum case name)*. 1833 1834Debido a que los nombres de casos de enumeraciones residen en el espacio de nombres de nivel superior (:ref:`spec-Namespaces`), los nombres de los casos en diferentes enumeraciones deben ser distintos. 1835 1836Una enumeración puede declararse pero no definirse, en cuyo caso debe definirse en otra parte dentro del modelo o en un archivo de datos. 1837Por ejemplo, un archivo de modelo podría contener esto: 1838 1839.. code-block:: minizinc 1840 1841 enum Workers; 1842 enum Shifts; 1843 1844Y el archivo de datos podría contener esto: 1845 1846.. code-block:: minizinc 1847 1848 Workers = { welder, driller, stamper }; 1849 Shifts = { idle, day, night }; 1850 1851Algunas veces es útil poder referirse a uno de los nombres de las cajas enum dentro del modelo. Esto se puede lograr usando una variable. El modelo leería: 1852 1853.. code-block:: minizinc 1854 1855 enum Shifts; 1856 Shifts: idle; % Variable representing the idle constant. 1857 1858Y el archivo de datos: 1859 1860.. code-block:: minizinc 1861 1862 enum Shifts = { idle_const, day, night }; 1863 idle = idle_const; % Assignment to the variable. 1864 1865Aunque la constante :mzn:`idle_const` no se puede mencionar en el modelo, la variable :mzn:`idle` puede ser. 1866 1867Todas las enumeraciones se deben definir en el momento de la instancia. 1868 1869Los elementos de enumeraciones se pueden anotar. :ref:`spec-Annotations` tiene más detalles sobre las anotaciones. 1870 1871Cada nombre de caso se puede forzar automáticamente al entero correspondiente a su índice en el tipo. 1872 1873.. code-block:: minizinc 1874 1875 int: oz = Australia; % oz = 1 1876 1877Para cada tipo enumerado :mzn:`T`, las siguientes funciones existen: 1878 1879.. code-block:: minizinc 1880 1881 % Devuelve el siguiente valor de enumeración mayor de x en un tipo de enumeración X 1882 function T: enum_next(set of T: X, T: x); 1883 function var T: enum_next(set of T: X, var T: x); 1884 1885 % Devuelve el siguiente valor enumeración más pequeño de x en un tipo de enumeración X 1886 function T: enum_prev(set of T: X, T: x); 1887 function var T: enum_prev(set of T: X, var T: x); 1888 1889 % Convertir x a un tipo de enumeración X 1890 function T: to_enum(set of T: X, int: x); 1891 function var T: to_enum(set of T: X, var int: x); 1892 1893.. _spec-assignments: 1894 1895 1896 1897 1898Artículos de asignación 1899~~~~~~~~~~~~~~~~~~~~~~~ 1900 1901Las asignaciones tienen esta sintaxis: 1902 1903.. literalinclude:: grammar.mzn 1904 :language: minizincdef 1905 :start-after: % Assign items 1906 :end-before: % 1907 1908Por ejemplo: 1909 1910.. code-block:: minizinc 1911 1912 A = 10; 1913 1914.. % \pjs{Add something about automatic coercion of index sets?} 1915 1916.. _spec-constraint-items: 1917 1918 1919 1920Objetos de restricción 1921~~~~~~~~~~~~~~~~~~~~~~ 1922 1923Los elementos de restricción forman el corazón de un modelo. Cualquier solución encontrada para un modelo satisfará todas sus limitaciones. 1924Los elementos de restricción tienen esta sintaxis: 1925 1926.. literalinclude:: grammar.mzn 1927 :language: minizincdef 1928 :start-after: % Constraint items 1929 :end-before: % 1930 1931Por ejemplo: 1932 1933.. code-block:: minizinc 1934 1935 constraint a*x < b; 1936 1937La expresión en un elemento de restricción debe tener instanciación de tipo :mzn:`par bool` o :mzn:`var bool`; sin embargo, tenga en cuenta que las restricciones con expresiones fijas no son muy útiles. 1938 1939.. _spec-solve-items: 1940 1941 1942 1943Elementos Solve 1944~~~~~~~~~~~~~~~ 1945 1946Cada modelo debe tener exactamente un elemento de solución. Los elementos de resolución tienen la siguiente sintaxis: 1947 1948.. literalinclude:: grammar.mzn 1949 :language: minizincdef 1950 :start-after: % Solve item 1951 :end-before: % 1952 1953Ejemplo de elmentos solve: 1954 1955.. code-block:: minizinc 1956 1957 solve satisfy; 1958 solve maximize a*x + y - 3*z; 1959 1960El elemento solve determina si el modelo representa un problema de satisfacción de restricciones o un problema de optimización. En el último caso, la expresión dada es la que se debe minimizar/maximizar. 1961 1962La expresión en un elemento de solve de minimizar/maximizar puede tener un tipo entero o flotante 1963 1964*Rationale: This is possible because all type-insts have a defined order.* 1965Tenga en cuenta que tener una expresión con una instanciación de tipo fija en un elemento solve no es muy útil, ya que significa que el modelo no requiere optimización. 1966 1967Elementos solve puede ser anotado. :ref:`spec-Annotations` tiene más detalles sobre las anotaciones. 1968 1969.. _spec-output-items: 1970 1971 1972 1973Elementos de salida 1974~~~~~~~~~~~~~~~~~~~ 1975 1976Los elementos de salida se utilizan para presentar las soluciones de una instancia modelo. 1977Tienen la siguiente sintaxis: 1978 1979.. literalinclude:: grammar.mzn 1980 :language: minizincdef 1981 :start-after: % Output items 1982 :end-before: % 1983 1984Por ejemplo: 1985 1986.. code-block:: minizinc 1987 1988 output ["The value of x is ", show(x), "!\n"]; 1989 1990La expresión debe tener un tipo-instanciación de :mzn:`array[int] of par string`. Se puede componer utilizando el operador incorporado :mzn:`++` y las funciones incorporadas :mzn:`show`, :mzn:`show_int`, y :mzn:`show_float` (:ref:`spec-builtins`), así como interpolaciones de cuerdas (:ref:`spec-String-Interpolation-Expressions`). La salida es la concatenación de los elementos de la matriz. Si existen múltiples elementos de salida, la salida es la concatenación de todas sus salidas, en el orden en que aparecen en el modelo. 1991 1992Si no hay ningún elemento de salida presente, la implementación debe imprimir todas las variables globales y sus valores en un formato legible. 1993 1994.. _spec-annotation-items: 1995 1996 1997Artículos de Anotación 1998~~~~~~~~~~~~~~~~~~~~~~ 1999 2000Los elementos de anotación se utilizan para aumentar el tipo :mzn:`ann`. Tienen la siguiente sintaxis: 2001 2002.. literalinclude:: grammar.mzn 2003 :language: minizincdef 2004 :start-after: % Annotation items 2005 :end-before: % 2006 2007Por ejemplo: 2008 2009.. code-block:: minizinc 2010 2011 annotation solver(int: kind); 2012 2013Es un error de instanciación de tipo si una anotación se declara y/o define más de una vez en un modelo. 2014 2015El uso de anotaciones se describe en :ref:`spec-Annotations`. 2016 2017.. _spec-preds-and-fns: 2018 2019 2020 2021 2022 2023 2024Operaciones definidas por el usuario 2025~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2026 2027.. 2028 % XXX: not saying if operations need to be defined. Implementation 2029 % currently requires functions and tests to be defined if used, but 2030 % predicates can be bodyless even if used. Should perhaps require functions 2031 % to be defined even if they're not used (like parameters), and make tests 2032 % like predicates? 2033 2034Los modelos MiniZinc pueden contener operaciones definidas por el usuario. Ellos tienen esta sintaxis: 2035 2036.. literalinclude:: grammar.mzn 2037 :language: minizincdef 2038 :start-after: % Predicate, test and function items 2039 :end-before: % 2040 2041Las expresiones de instanciación de tipos pueden incluir variables type-inst en la función y declaración de predicado. 2042 2043Por ejemplo, el predicado :mzn:`even` verifica que su argumento sea un número par. 2044 2045.. code-block:: minizinc 2046 2047 predicate even(var int: x) = 2048 x mod 2 = 0; 2049 2050Un predicado soportado de forma nativa por el solucionador de destino se puede declarar de la siguiente manera: 2051 2052.. code-block:: minizinc 2053 2054 predicate alldifferent(array [int] of var int: xs); 2055 2056Las declaraciones de predicados que se admiten de forma nativa en MiniZinc están restringidas al uso de tipos de FlatZinc (por ejemplo, las matrices multidimensionales y no basadas en 1 están prohibidas). 2057 2058.. % \pjs{need to fix this if we allow2d arrays in FlatZinc!} 2059 2060Las declaraciones para las operaciones definidas por el usuario se pueden anotar. :ref:`spec-Annotations` tiene más detalles sobre las anotaciones. 2061 2062.. _spec-basic-properties: 2063 2064 2065 2066 2067 2068 2069Propiedades básicas 2070+++++++++++++++++++ 2071 2072El término "predicado" generalmente se usa para referirse tanto a elementos de prueba como a elementos predicados. Cuando se deben distinguir los dos tipos, se pueden usar los términos "elemento de prueba" y "elemento predicado". 2073 2074El retorno tipo-instanciación de un elemento de prueba es implícitamente :mzn:`par bool`. El retorno tipo-instanciación de un elemento predicado es implícitamente :mzn:`var bool`. 2075 2076Los predicados y las funciones pueden ser recursivos. La terminación de una llamada a función recursiva depende únicamente de sus argumentos fijos, es decir, las funciones recursivas y los predicados no se pueden usar para definir variables restringidas recursivamente. 2077 2078.. % \Rationale{This ensures that the satisfiability of models is decidable.} 2079 2080Los predicados y las funciones introducen sus propios nombres locales, siendo los de los argumentos formales. El alcance de estos nombres cubre el predicado/cuerpo de la función. Los nombres de argumento no se pueden repetir dentro de una declaración de predicado/función. 2081 2082 2083Polimorfismo ad-hoc 2084+++++++++++++++++++ 2085 2086MiniZinc admite polimorfismo ad-hoc mediante sobrecarga. Las funciones y los predicados (tanto integrados como definidos por el usuario) pueden sobrecargarse. Un nombre puede estar sobrecargado como una función y un predicado. 2087 2088Es un error tipo-instanciación si una sola versión de una operación sobrecargada con una firma particular tipo-instanciación se define más de una vez en un modelo. Por ejemplo: 2089 2090.. code-block:: minizinc 2091 2092 predicate p(1..5: x); 2093 predicate p(1..5: x) = false; % correcto : primera definición 2094 predicate p(1..5: x) = true; % error : definición repetida 2095 2096La combinación de sobrecarga y coacciones puede causar problemas. 2097Se dice que dos sobrecargas de una operación * se superponen * si pueden coincidir con los mismos argumentos. Por ejemplo, las siguientes sobrecargas de :mzn:`p` se superponen, ya que ambos coinciden con la llamada :mzn:`p(3)`. 2098 2099.. code-block:: minizinc 2100 2101 predicate p(par int: x); 2102 predicate p(var int: x); 2103 2104Sin embargo, los siguientes dos predicados no se superponen porque no pueden coincidir con el mismo argumento: 2105 2106.. code-block:: minizinc 2107 2108 predicate q(int: x); 2109 predicate q(set of int: x); 2110 2111Evitamos dos posibles problemas de sobrecarga al imponer algunas restricciones a la superposición de sobrecargas de operaciones. 2112 2113#. El primer problema es la ambigüedad. La colocación diferente de las coerciones en los argumentos de operación puede permitir diferentes opciones para la función sobrecargada. 2114Por ejemplo, si una función MiniZinc :mzn:`f` está sobrecargado así: 2115 2116 .. code-block:: minizinc 2117 2118 function int: f(int: x, float: y) = 0; 2119 function int: f(float: x, int: y) = 1; 2120 2121 Entonces :mzn:`f(3,3)` podría ser 0 o 1 dependiendo de las opciones de coerción/sobrecarga. 2122 2123 Para evitar este problema, cualquier sobrecarga superpuesta de una operación debe ser semánticamente equivalente con respecto a la coerción. Por ejemplo, las dos sobrecargas del predicado :mzn:`p` anteriormente debe tener cuerpos que son semánticamente equivalentes con respecto a la sobrecarga. 2124 2125 Actualmente, este requisito no se verifica y el modelador debe satisfacerlo manualmente. En el futuro, es posible que solicitemos compartir los cuerpos entre las diferentes versiones de las operaciones sobrecargadas, lo que proporcionaría la satisfacción automática de este requisito. 2126 2127#. El segundo problema es que ciertas combinaciones de sobrecargas podrían requerir una implementación de MiniZinc para realizar una búsqueda combinatoria con el fin de explorar diferentes opciones de coerción y sobrecarga. Por ejemplo, si la función :mzn:`g` está sobrecargado así: 2128 2129 .. code-block:: minizinc 2130 2131 function float: g(int: t1, float: t2) = t2; 2132 function int : g(float: t1, int: t2) = t1; 2133 2134 Entonces, cómo se resuelve la sobrecarga de :mzn:`g(3,4)` depende de su contexto: 2135 2136 .. code-block:: minizinc 2137 2138 float: s = g(3,4); 2139 int: t = g(3,4); 2140 2141 En la definición de :mzn:`s` la primera definición sobrecargada debe ser utilizada mientras que en la definición de :mzn:`t` el segundo debe ser usado. 2142 2143Para evitar este problema, todas las sobrecargas superpuestas de una operación deben cerrarse bajo la intersección de su entrada tipo-instanciación. Es decir, si las versiones sobrecargadas tienen entrada de tipo-instanciación :math:`(S_1,....,S_n)` y :math:`(T_1,...,T_n)` entonces debe haber otra versión sobrecargada con entrada tipo-instanciación :math:`(R_1,...,R_n)` donde cada :math:`R_i` es el límite inferior más grande (*glb*) de :math:`S_i` y :math:`T_i`. 2144 2145Además, todas las sobrecargas superpuestas de una operación deben ser monótonas. Es decir, si hay versiones sobrecargadas con entrada tipo-instanciación :math:`(S_1,....,S_n)` y :math:`(T_1,...,T_n)` y salida tipo-instanciación :math:`S` y :math:`T`, respectivamente, entonces :math:`S_i \preceq T_i` para todos :math:`i`, implica :math:`S \preceq T`. En los sitios de llamadas, siempre se utiliza la sobrecarga de coincidencia que es más baja en el enrejado tipo-instanciación. 2146 2147Para :mzn:`g` posteriormente, el tipo-instanciación intersection (o *glb*) de :mzn:`(int,float)` y :mzn:`(float,int)` es :mzn:`(int,int)`. Por lo tanto, las versiones sobrecargadas no se cierran en intersección y el usuario debe proporcionar otra sobrecarga para :mzn:`g` con entrada de tipo-instanciación :mzn:`(int,int)`. La definición natural es: 2148 2149 .. code-block:: minizinc 2150 2151 function int: g(int: t1, int: t2) = t1; 2152 2153Una vez :mzn:`g` se ha aumentado con la tercera sobrecarga, satisface el requisito de monotonicidad porque la salida tipo-instanciación de la tercera sobrecarga es :mzn:`int` que es menor que la salida tipo-instanciación de las sobrecargas originales. 2154 2155La monotonicidad y el cierre bajo la conjunción tipo-instanciación aseguran que siempre que se alcanza una función o predicado sobrecargado durante la comprobación de tipo-instanciación, siempre hay una versión "mínima" segura y única para elegir, por lo que la complejidad de la comprobación de tipo-instanciación permanece lineal. Por lo tanto, en nuestro ejemplo :mzn:`g(3,4)` siempre se resuelve eligiendo la nueva definición sobrecargada. 2156 2157 2158 2159 2160 2161Variables locales 2162+++++++++++++++++ 2163 2164Las variables locales en los cuerpos de operación se introducen usando expresiones ``let``. 2165Por ejemplo, el predicado :mzn:`have_common_divisor` toma dos valores enteros y comprueba si tienen un divisor común mayor que uno: 2166 2167.. code-block:: minizinc 2168 2169 predicate have_common_divisor(int: A, int: B) = 2170 let { 2171 var 2..min(A,B): C; 2172 } in 2173 A mod C = 0 /\ 2174 B mod C = 0; 2175 2176Sin embargo, como :ref:`spec-Let-Expressions` explicado, porque :mzn:`C` no está definido, este predicado no puede ser llamado en un contexto negativo. La siguiente es una versión que podría llamarse en un contexto negativo: 2177 2178.. code-block:: minizinc 2179 2180 predicate have_common_divisor(int: A, int: B) = 2181 exists(C in 2..min(A,B)) 2182 (A mod C = 0 /\ B mod C = 0); 2183 2184.. _spec-annotations: 2185 2186 2187 2188Anotaciones 2189----------- 2190 2191Anotaciones: valores del tipo :mzn:`ann`, permitir que un modelador especifique información no declarativa y específica del solucionador que está más allá del lenguaje central. Las anotaciones no cambian el significado de un modelo, sin embargo, solo cómo se resuelve. 2192 2193Las anotaciones se pueden adjuntar a variables (en sus declaraciones), expresiones, sinónimos de tipo-instanciación, elementos de enumeraciones, elementos de solución y operaciones definidas por el usuario. 2194Tienen la siguiente sintaxis: 2195 2196.. literalinclude:: grammar.mzn 2197 :language: minizincdef 2198 :start-after: % Annotations 2199.. # :end-before: % 2200 2201Por ejemplo: 2202 2203.. code-block:: minizinc 2204 2205 int: x::foo; 2206 x = (3 + 4)::bar("a", 9)::baz("b"); 2207 solve :: blah(4) 2208 minimize x; 2209 2210Los tipos de expresiones de argumento deben coincidir con los tipos de argumento de la anotación declarada. A diferencia de los predicados y funciones definidos por el usuario, las anotaciones no pueden sobrecargarse. *Justificación: no hay una razón particularmente fuerte para esto, simplemente parecía hacer las cosas más simples.* 2211 2212 2213Las firmas de anotación pueden contener variables de tipo-instanciación. 2214 2215El orden y el anidamiento de las anotaciones no importan. Para el caso de expresión, puede ser útil ver el conector de anotación :mzn:`::` como un operador sobrecargado: 2216 2217.. code-block:: minizinc 2218 2219 ann: '::'(any $T: e, ann: a); % associative 2220 ann: '::'(ann: a, ann: b); % associative + commutative 2221 2222Ambos operadores son asociativos, el segundo es conmutativo. Esto significa que las siguientes expresiones son todas equivalentes: 2223 2224.. code-block:: minizinc 2225 2226 e :: a :: b 2227 e :: b :: a 2228 (e :: a) :: b 2229 (e :: b) :: a 2230 e :: (a :: b) 2231 e :: (b :: a) 2232 2233Esta propiedad también se aplica a las anotaciones sobre elementos de solución y elementos de declaración variable. *Justificación: esta propiedad simplifica las cosas, ya que permite que todas las combinaciones anidadas de anotaciones se traten como si fueran planas, evitando así la necesidad de determinar cuál es el significado de una anotación anotada. También simplifica el árbol de sintaxis abstracta MiniZinc al evitar la necesidad de representar el anidamiento.* 2234 2235.. _spec-partiality: 2236 2237 2238Parcialidad 2239----------- 2240 2241La presencia de tipo-instanciación restringida en MiniZinc significa que varias operaciones son potencialmente *parciales*, es decir, no están claramente definidas para todas las entradas posibles. Por ejemplo, ¿qué sucede si una función que espera un argumento positivo pasa un argumento negativo? ¿Qué sucede si a una variable se le asigna un valor que no satisface sus restricciones tipo-instanciación? ¿Qué sucede si un índice de matriz está fuera de límites? Esta sección describe lo que sucede en todos estos casos. 2242 2243.. % \pjs{This is not what seems to happen in the current MiniZinc!} 2244 2245En general, los casos que implican valores fijos que no satisfacen las restricciones conducen a abortos en tiempo de ejecución. *Justificación: nuestra experiencia muestra que si un valor fijo falla una restricción, es casi seguro que se debe a un error de programación. Además, estos casos son fáciles de verificar para una implementación.* 2246 2247Pero los casos que involucran valores no fijados varían, como veremos. *Justificación: lo mejor que se puede hacer con los valores no fijados varía de un caso a otro. Además, es difícil verificar las restricciones en los valores no fijados, sobre todo porque durante la búsqueda una variable de decisión puede ser fija y, a continuación, retroceder hará que este valor se revierta, en cuyo caso abortar es una mala idea.* 2248 2249 2250 2251 2252 2253Asignaciones parciales 2254~~~~~~~~~~~~~~~~~~~~~~ 2255 2256La primera operación que implica parcialidad es la asignación. Hay cuatro casos distintos para las asignaciones. 2257 2258- Un valor asignado a una variable global fija, limitada se verifica en tiempo de ejecución; si el valor asignado no satisface sus restricciones, es un error en tiempo de ejecución. En otras palabras, esto: 2259 2260 .. code-block:: minizinc 2261 2262 1..5: x = 3; 2263 2264Es equivalente a esto: 2265 2266.. code-block:: minizinc 2267 2268 int: x = 3; 2269 constraint assert(x in 1..5, 2270 "assignment to global parameter 'x' failed") 2271 2272- Un valor asignado a una variable global restringida no fija hace que la asignación actúe como una restricción. Si el valor asignado no satisface las restricciones de la variable, causa un error en el modelo en tiempo de ejecución. 2273 2274En otras palabras, esto: 2275 2276.. code-block:: minizinc 2277 2278 var 1..5: x = 3; 2279 2280Es equivalente a esto: 2281 2282.. code-block:: minizinc 2283 2284 var int: x = 3; 2285 constraint x in 1..5; 2286 2287*Justificación: este comportamiento es fácil de entender y fácil de implementar.* 2288 2289- Un valor asignado a una variable fija, limitada y localizada se verifica en tiempo de ejecución; si el valor asignado no satisface sus restricciones, es un error en tiempo de ejecución. En otras palabras, esto: 2290 2291.. code-block:: minizinc 2292 2293 let { 1..5: x = 3; } in x+1 2294 2295Es equivalente a esto: 2296 2297.. code-block:: minizinc 2298 2299 let { int: x = 3; } in 2300 assert(x in 1..5, 2301 "assignment to let parameter 'x' failed", x+1) 2302 2303- Un valor asignado a una variable localmente limitada y no fijada hace que la asignación actúe como una restricción; si la restricción falla en el tiempo de ejecución, la falla "burbujea" hacia el alcance booleano circundante más cercano, donde se interpreta como :mzn:`false`. 2304 2305*Justificación: este comportamiento es coherente con las asignaciones a variables globales.* 2306 2307Tenga en cuenta que en los casos en que un valor es parcialmente fijo y parcialmente no fijo, por ejemplo, algunas matrices, los diferentes elementos se verifican según los diferentes casos, y los elementos fijos se comprueban antes de los elementos no fijos. Por ejemplo: 2308 2309.. code-block:: minizinc 2310 2311 u = [ let { var 1..5: x = 6} in x, let { par 1..5: y = 6; } in y) ]; 2312 2313Esto provoca un aborto en tiempo de ejecución, porque el segundo elemento fijo se comprueba antes del primer elemento no fijo. Este orden también es cierto para los casos en las siguientes secciones. *Justificación: esto asegura que las fallas no pueden enmascarar interrupciones, lo que parece deseable.* 2314 2315 2316 2317Predicados/Funciones parciales y Argumentos de Anotaciones 2318~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2319 2320El segundo tipo de operación que implica parcialidad es llamadas y anotaciones. 2321 2322.. 2323 % The behaviour for these operations is simple: constraints on arguments are 2324 % ignored. 2325 % 2326 % \Rationale{This is easy to implement and easy to understand. It is also 2327 % justifiable in the sense that predicate/function/annotation arguments are 2328 % values that are passed in from elsewhere; if those values are to be 2329 % constrained, that could be done earlier. (In comparison, when a variable 2330 % with a constrained type-inst is declared, any assigned value must clearly 2331 % respect that constraint.)} 2332 2333La semántica es similar a las asignaciones: los argumentos fijos que fallan sus restricciones provocarán abortos, y los argumentos no fijados que fallan sus restricciones causarán fallas, que se disparan hasta el alcance booleano circundante más cercano. 2334 2335 2336Accesos parciales de matriz 2337~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2338 2339El tercer tipo de operación que implica parcialidad es el acceso a la matriz. Hay dos casos distintos. 2340 2341- Un valor fijo utilizado como un índice de matriz se verifica en tiempo de ejecución; si el valor del índice no está en el conjunto de índice de la matriz, es un error en tiempo de ejecución. 2342 2343- Un valor no fijo utilizado como un índice de matriz hace que el acceso actúe como una restricción; si el acceso falla en el tiempo de ejecución, la falla "burbujea" hacia el alcance booleano circundante más cercano, donde se interpreta como :mzn:`false`. Por ejemplo: 2344 2345 2346 .. code-block:: minizinc 2347 2348 array[1..3] of int: a = [1,2,3]; 2349 var int: i; 2350 constraint (a[i] + 3) > 10 \/ i = 99; 2351 2352Aquí el acceso a la matriz falla, por lo que la falla sube hasta la disyunción, y :mzn:`i` está obligado a ser 99. *Justificación: a diferencia de las llamadas al predicado/función, los modeladores en la práctica a veces usan accesos de matriz que pueden fallar. En tales casos, el comportamiento de "burbujeo" es razonable.* 2353 2354.. _spec-builtins: 2355 2356 2357 2358 2359Operaciones incorporadas 2360------------------------ 2361 2362Este apéndice enumera los operadores integrados, las funciones y los predicados. Pueden implementarse como integradas verdaderas, o en bibliotecas que se importan automáticamente para todos los modelos. Muchos de ellos están sobrecargados. 2363 2364Los nombres de los operadores están escritos dentro de comillas simples cuando se usan en firmas de tipo, por ejemplo :mzn:`bool: '\/'(bool, bool)`. 2365 2366Usamos la sintaxis :mzn:`TI: f(TI1,...,TIn)` para representar una operación llamada :mzn:`f` eso toma argumentos con un tipo-instanciación :mzn:`TI,...,TIn` y devuelve un valor con tipo-instanciación :mzn:`TI`. Esto es un poco más compacto que la sintaxis MiniZinc habitual, ya que omite los nombres de los argumentos. 2367 2368 2369 2370Operaciones de comparación 2371~~~~~~~~~~~~~~~~~~~~~~~~~~ 2372 2373 2374Menos que. Otras comparaciones son similares: 2375mayor que (:mzn:`>`), 2376menor o igual (:mzn:`<=`), 2377mayor que o igual (:mzn:`>=`), 2378igual (:mzn:`==`, :mzn:`=`), 2379y desigualdad (:mzn:`!=`). 2380 2381.. % \pjs{Check use of any here!} 2382 2383.. code-block:: minizinc 2384 2385 bool: '<'( $T, $T) 2386 var bool: '<'(var $T, var $T) 2387 2388 2389 2390 2391 2392Operaciones aritmeticas 2393~~~~~~~~~~~~~~~~~~~~~~~ 2394 2395 2396Adición. Otras operaciones numéricas son similares: resta (:mzn:`-`), y multiplicación (:mzn:`*`). 2397 2398.. code-block:: minizinc 2399 2400 int: '+'( int, int) 2401 var int: '+'(var int, var int) 2402 float: '+'( float, float) 2403 var float: '+'(var float, var float) 2404 2405 2406 2407 2408 2409Menos unaria (:mzn:`-`). Suma unaria (:mzn:`+`) es similar. 2410 2411.. code-block:: minizinc 2412 2413 int: '-'( int) 2414 var int: '-'(var int) 2415 float: '-'( float) 2416 var float: '-'(var float) 2417 2418 2419 2420 2421 2422Entero y división de punto flotante y módulo. 2423 2424.. code-block:: minizinc 2425 2426 int: 'div'( int, int) 2427 var int: 'div'(var int, var int) 2428 int: 'mod'( int, int) 2429 var int: 'mod'(var int, var int) 2430 float: '/' ( float, float) 2431 var float: '/' (var float, var float) 2432 2433 2434 2435El resultado de la operación de módulo, si no es cero, siempre tiene el mismo signo que su primer operando. Las operaciones de división entera y módulo están conectadas por la siguiente identidad: 2436 2437 2438.. code-block:: minizinc 2439 2440 x = (x div y) * y + (x mod y) 2441 2442 2443 2444Algunos ejemplos ilustrativos: 2445 2446.. code-block:: minizinc 2447 2448 7 div 4 = 1 7 mod 4 = 3 2449 -7 div 4 = -1 -7 mod 4 = -3 2450 7 div -4 = -1 7 mod -4 = 3 2451 -7 div -4 = 1 -7 mod -4 = -3 2452 2453 2454 2455 2456 2457Suma de multiples números. 2458Producto (:mzn:`product`) es similar. Tenga en cuenta que la suma de una matriz vacía es 0, y el producto de una matriz vacía es 1. 2459 2460.. code-block:: minizinc 2461 2462 int: sum(array[$T] of int ) 2463 var int: sum(array[$T] of var int ) 2464 float: sum(array[$T] of float) 2465 var float: sum(array[$T] of var float) 2466 2467 2468 2469 2470 2471Mínimo de dos valores; máximo (:mzn:`max`) es similar. 2472 2473.. code-block:: minizinc 2474 2475 any $T: min(any $T, any $T ) 2476 2477 2478 2479 2480 2481Mínimo de una matriz de valores; máximo (:mzn:`max`) es similar. 2482Aborta si el argumento el arreglo esta vacio. 2483 2484.. code-block:: minizinc 2485 2486 any $U: min(array[$T] of any $U) 2487 2488 2489 2490 2491 2492Mínimo de un conjunto fijo; máximo (:mzn:`max`) es similar. 2493Aborta si el argumento el conjunto esta vacio. 2494 2495.. code-block:: minizinc 2496 2497 $T: min(set of $T) 2498 2499 2500 2501 2502 2503Valor absoluto de un número. 2504 2505.. code-block:: minizinc 2506 2507 int: abs( int) 2508 var int: abs(var int) 2509 float: abs( float) 2510 var float: abs(var float) 2511 2512 2513 2514 2515 2516Raíz cuadrada de un número en punto flotante (``float``). Aborta si el argumento es negativo. 2517 2518.. code-block:: minizinc 2519 2520 float: sqrt( float) 2521 var float: sqrt(var float) 2522 2523 2524 2525Operador de energía. Por ejemplo, :mzn:`pow(2, 5)` da como resultado :mzn:`32`. 2526 2527.. code-block:: minizinc 2528 2529 int: pow(int, int) 2530 float: pow(float, float) 2531 2532 2533.. 2534 % We should also have: 2535 % var float: pow(var float, int) 2536 2537 2538Natural exponent. 2539 2540.. code-block:: minizinc 2541 2542 float: exp(float) 2543 var float: exp(var float) 2544 2545 2546 2547 2548 2549Logaritmo natural. Logaritmo en base 10 (:mzn:`log10`) y logaritmo en base 25502 (:mzn:`log2`) son similares. 2551 2552.. code-block:: minizinc 2553 2554 float: ln(float) 2555 var float: ln(var float) 2556 2557 2558 2559Logaritmo general; el primer argumento es la base. 2560 2561.. code-block:: minizinc 2562 2563 float: log(float, float) 2564 2565 2566Seno (:mzn:`sin`), Coseno (:mzn:`cos`), tangente (:mzn:`tan`), seno inverso 2567(:mzn:`asin`), coseno inverso (:mzn:`acos`), tangente inversa 2568(:mzn:`atan`), seno hiperbólico (:mzn:`sinh`), coseno hiperbólico 2569(:mzn:`cosh`), tangente hiperbólica (:mzn:`tanh`), 2570seno hiperbólico inverso (:mzn:`asinh`), coseno hiperbólico inverso 2571(:mzn:`acosh`) y tangente hiperbólica inversa (:mzn:`atanh`) son similares. 2572 2573.. code-block:: minizinc 2574 2575 float: sin(float) 2576 var float: sin(var float) 2577 2578 2579Operaciones Lógicas 2580~~~~~~~~~~~~~~~~~~~ 2581 2582Conjunción. Otras operaciones lógicas son similares: 2583disyunción (``\/``) 2584implicación inversa (:mzn:`<-`), 2585implicación directa (:mzn:`->`), 2586bi-implicación (:mzn:`<->`), 2587exclusive disjunction (:mzn:`xor`), 2588negación lógica (:mzn:`not`). 2589 2590Tenga en cuenta que los operadores de implicación no están escritos usando :mzn:`=>`, :mzn:`<=` y :mzn:`<=>` como es el caso en algunos idiomas. Esto permite :mzn:`<=` para representar en su lugar "menor que o igual". 2591 2592.. code-block:: minizinc 2593 2594 bool: '/\'( bool, bool) 2595 var bool: '/\'(var bool, var bool) 2596 2597 2598 2599Cuantificación universal. 2600Cuantificación existencial (:mzn:`exists`) es similar. Tenga en cuenta que, cuando se aplica a una lista vacía, :mzn:`forall` retorna :mzn:`true`, y :mzn:`exists` retorna :mzn:`false`. 2601 2602 .. code-block:: minizinc 2603 2604 bool: forall(array[$T] of bool) 2605 var bool: forall(array[$T] of var bool) 2606 2607 2608 2609 2610 2611N-aria disyunción exclusiva. 2612N-aria bi-implicación (:mzn:`iffall`) es similar, con :mzn:`true` en lugar de :mzn:`false`. 2613 2614 .. code-block:: minizinc 2615 2616 bool: xorall(array[$T] of bool: bs) = foldl('xor', false, bs) 2617 var bool: xorall(array[$T] of var bool: bs) = foldl('xor', false, bs) 2618 2619 2620Operaciones de Matriz 2621~~~~~~~~~~~~~~~~~~~~~ 2622 2623Longitud de una matriz. 2624 2625.. code-block:: minizinc 2626 2627int: length(array[$T] of any $U) 2628 2629 2630Concatenación de lista Devuelve la lista (matriz indexada entera) que contiene todos los elementos del primer argumento seguidos por todos los elementos del segundo argumento, con elementos que ocurren en el mismo orden que en los argumentos. Los índices resultantes están en el rango :mzn:`1..n`, donde :mzn:`n` es la suma de las longitudes de los argumentos. *Justificación: Esto permite que las matrices en forma de listas se concatenen naturalmente y evita problemas con índices superpuestos. Los índices resultantes son consistentes con los de literales indexados implícitamente.* 2631 2632Tenga en cuenta que :mzn:`'++'` también realiza la concatenación de cadenas. 2633 2634.. code-block:: minizinc 2635 2636 array[int] of any $T: '++'(array[int] of any $T, array[int] of any $T) 2637 2638 2639Conjuntos de índices de matrices. Si el argumento es un literal, retorna :mzn:`1..n` en donde :mzn:`n` es el largo de la sub-matriz. De lo contrario, devuelve el conjunto de índices declarado o inferido. Esta lista es solo parcial, se extiende de manera obvia, para matrices de mayores dimensiones. 2640 2641.. code-block:: minizinc 2642 2643 set of $T: index_set (array[$T] of any $V) 2644 set of $T: index_set_1of2(array[$T, $U] of any $V) 2645 set of $U: index_set_2of2(array[$T, $U] of any $V) 2646 ... 2647 2648Reemplace los índices de la matriz dada por el último argumento con el 2649Producto cartesiano de los conjuntos dados por los argumentos anteriores. Existen versiones similares para matrices de hasta 6 dimensiones. 2650 2651.. code-block:: minizinc 2652 2653 array[$T1] of any $V: array1d(set of $T1, array[$U] of any $V) 2654 array[$T1,$T2] of any $V: 2655 array2d(set of $T1, set of $T2, array[$U] of any $V) 2656 array[$T1,$T2,$T3] of any $V: 2657 array3d(set of $T1, set of $T2, set of $T3, array[$U] of any $V) 2658 2659 2660 2661 2662Operaciones de coerción 2663~~~~~~~~~~~~~~~~~~~~~~~ 2664 2665Redondea un número de punto flotante (``float``) hacia :math:`+\infty`, :math:`-\infty`, y el entero más cercano, respectivamente. 2666 2667.. code-block:: minizinc 2668 2669 int: ceil (float) 2670 int: floor(float) 2671 int: round(float) 2672 2673 2674Conversiones explícitas de una instancia de tipo-instanciación. 2675 2676.. code-block:: minizinc 2677 2678 int: bool2int( bool) 2679 var int: bool2int(var bool) 2680 float: int2float( int) 2681 var float: int2float(var int) 2682 array[int] of $T: set2array(set of $T) 2683 2684 2685 2686 2687Operaciones de cadena 2688~~~~~~~~~~~~~~~~~~~~~ 2689 2690 2691Conversión de cadena. Convierte cualquier valor en una cadena para fines de salida. La forma exacta de la cadena resultante depende de la implementación. 2692 2693.. code-block:: minizinc 2694 2695 string: show(any $T) 2696 2697 2698Conversión de cadena formateada para enteros. 2699Convierte el entero dado por el segundo argumento en una cadena a la derecha justificada por el número de caracteres dados por el primer argumento, o justificado a la izquierda si ese argumento es negativo. 2700Si el segundo argumento no es fijo, la forma de la cadena depende de la implementación. 2701 2702.. code-block:: minizinc 2703 2704 string: show_int(int, var int); 2705 2706 2707Conversión de cadena formateada para flotadores. 2708Convierte la flotación dada por el tercer argumento en una cadena a la derecha justificada por el número de caracteres dados por el primer argumento, o justificada a la izquierda si ese argumento es negativo. 2709La cantidad de dígitos que aparecen después del punto decimal viene dada por el segundo argumento. 2710Es un error en tiempo de ejecución para que el segundo argumento sea negativo. 2711Si el tercer argumento no es fijo, la forma de la cadena depende de la implementación. 2712 2713.. code-block:: minizinc 2714 2715 string: show_float(int, int, var float) 2716 2717 2718Concatenación de cadenas Tenga en cuenta que :mzn:`'++'` también realiza concatenación de matriz. 2719 2720.. code-block:: minizinc 2721 2722 string: '++'(string, string) 2723 2724 2725Concatenar una matriz de cadenas. 2726Equivalente a :mzn:`'++'` sobre la matriz, pero puede implementarse de manera más eficiente. 2727 2728.. code-block:: minizinc 2729 2730 string: concat(array[$T] of string) 2731 2732 2733Concatenar una matriz de cadenas, poniendo un separador entre cadenas adyacentes. 2734Devuelve la cadena vacía si la matriz está vacía. 2735 2736.. code-block:: minizinc 2737 2738 string: join(string, array[$T] of string) 2739 2740 2741 2742 2743Operaciones vinculadas y de dominio 2744~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2745 2746Las operaciones de límite :mzn:`lb` y :mzn:`ub` devuelve los límites fijos inferiores/superiores corregidos a la expresión. 2747 2748Para los tipos numéricos, devuelven un valor límite inferior/superior, por ejemplo, el valor más-bajo/más-alto que la expresión puede tomar. 2749 2750Para los tipos de conjuntos, devuelven un subconjunto/superconjunto, por ejemplo, la intersección/unión de todos los valores posibles de la expresión establecida. 2751 2752Las operaciones enlazadas abortan en expresiones que no tienen un límite finito correspondiente. 2753Por ejemplo, este sería el caso de una variable declarada sin límites en una implementación que no asigna límites predeterminados. Las expresiones set siempre tienen un límite inferior finito de curso, es decir :mzn:`{}`, el conjunto vacío. 2754 2755Numérico de límite inferior/superior: 2756 2757.. code-block:: minizinc 2758 2759 int: lb(var int) 2760 float: lb(var float) 2761 int: ub(var int) 2762 float: ub(var float) 2763 2764 2765Establecer límite inferior/superior: 2766 2767.. code-block:: minizinc 2768 2769 set of int: lb(var set of int) 2770 set of int: ub(var set of int) 2771 2772Las versiones de las operaciones vinculadas que operan en matrices también están disponibles, devuelven un límite inferior seguro o límite superior para todos los miembros de la matriz - abortan si la matriz está vacía: 2773 2774.. code-block:: minizinc 2775 2776 int: lb_array(array[$T] of var int) 2777 float: lb_array(array[$T] of var float) 2778 set of int: lb_array(array[$T] of var set of int) 2779 int: ub_array(array[$T] of var int) 2780 float: ub_array(array[$T] of var float) 2781 set of int: ub_array(array[$T] of var set of int) 2782 2783 2784 2785 2786Dominio Entero: 2787 2788.. code-block:: minizinc 2789 2790 set of int: dom(var int) 2791 2792 2793La operación de dominio :mzn:`dom` devuelve un superconjunto fijo de los posibles valores de la expresión. 2794 2795Entero de dominio de matriz, devuelve un superconjunto de todos los valores posibles que pueden aparecer en la matriz; esto se cancela si la matriz está vacía: 2796 2797.. code-block:: minizinc 2798 2799 set of int: dom_array(array[$T] of var int) 2800 2801Tamaño de dominio para enteros: 2802 2803.. code-block:: minizinc 2804 2805 int: dom_size(var int) 2806 2807La operación de tamaño de dominio :mzn:`dom_size` es equivalente a :mzn:`card(dom(x))`. 2808 2809Tenga en cuenta que estas operaciones pueden producir resultados diferentes dependiendo de cuándo se evalúan y qué forma toma el argumento. Por ejemplo, considere la operación de límite inferior numérico. 2810 2811 2812- Si el argumento es una expresión fija, el resultado es el valor del argumento. 2813 2814- Si el argumento es una variable de decisión, el resultado depende del contexto. 2815 2816- Si la implementación puede determinar un límite inferior para la variable, el resultado es ese límite inferior. El límite inferior puede ser de la declaración de la variable, o más alto que debido al preprocesamiento, o menor que si se aplica un límite inferior definido por la implementación (por ejemplo, si la variable se declaró sin límite inferior, pero la implementación impone un límite mínimo ligado). 2817 2818- Si la implementación no puede determinar un límite inferior para la variable, la operación aborta. 2819 2820- Si el argumento es cualquier otro tipo de expresión no fijada, el límite inferior depende de los límites de las subexpresiones no fijadas y de los operadores de conexión. 2821 2822 2823.. _spec-option-type-operations: 2824 2825 2826 2827Operaciones de Tipo de Opción 2828~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2829 2830El valor del tipo de opción (:math:`\top`) es escrito 2831 2832.. code-block:: minizinc 2833 2834 opt $T: '<>'; 2835 2836 2837Uno puede determinar si una variable de tipo de opción realmente ocurre o no usando :mzn:`occurs` y :mzn:`absent` 2838 2839.. code-block:: minizinc 2840 2841 par bool: occurs(par opt $T); 2842 var bool: occurs(var opt $T); 2843 par bool: absent(par opt $T); 2844 var bool: absent(var opt $T); 2845 2846 2847Uno puede devolver el valor no opcional de una variable de tipo de opción usando la función :mzn:`deopt` 2848 2849.. code-block:: minizinc 2850 2851 par $T: deopt{par opt $T); 2852 var $T: deopt(var opt $T); 2853 2854 2855.. 2856 % Note that this is not really a function only a pseudo function placeholder 2857 % used in the translation of option types to non-option types. 2858 % \pjs{Explain better} 2859 2860.. _spec-other-operations: 2861 2862 2863 2864Otras operaciones 2865~~~~~~~~~~~~~~~~~~~~~~~ 2866 2867Verifique que una expresión booleana sea verdadera, y aborte si no, imprimiendo el segundo argumento como el mensaje de error. El primero devuelve el tercer argumento, y es particularmente útil para los argumentos de comprobación de formalidad para los predicados y las funciones; importante, su tercer argumento es flojo, es decir, solo se evalúa si la condición tiene éxito. El segundo devuelve :mzn:`true` y es útil para verificaciones de cordura globales (por ejemplo, de datos de instancia) en elementos de restricción. 2868 2869 2870.. code-block:: minizinc 2871 2872 any $T: assert(bool, string, any $T) 2873 par bool: assert(bool, string) 2874 2875 2876Cancelar la evaluación, imprimiendo la cadena dada. 2877 2878.. code-block:: minizinc 2879 2880 any $T: abort(string) 2881 2882Devuelve verdadero. Como efecto secundario, una implementación puede imprimir el primer argumento. 2883 2884.. code-block:: minizinc 2885 2886 bool: trace(string) 2887 2888 2889Devuelve el segundo argumento. 2890Como efecto secundario, una implementación puede imprimir el primer argumento. 2891 2892.. code-block:: minizinc 2893 2894 any $T: trace(string, any $T) 2895 2896Verifique si el valor del argumento está fijo en este punto de la evaluación. Si no, aborta; si es así, devuelve su valor. Esto es más útil en los elementos de salida cuando las variables de decisión deben ser corregidas: permite que se utilicen en lugares donde se necesita un valor fijo, como las condiciones if-then-else. 2897 2898 2899.. code-block:: minizinc 2900 2901 $T: fix(any $T) 2902 2903 2904Como arriba, pero retorna :mzn:`false` si el valor del argumento no es fijo. 2905 2906.. code-block:: minizinc 2907 2908 par bool: is_fixed(any $T) 2909 2910 2911.. _spec-content-types: 2912 2913 2914 2915Tipos de Contenido 2916------------------ 2917 2918El tipo de contenido ``application/x-zinc-output`` define un formato de salida de texto para Zinc. 2919El formato amplía la sintaxis abstracta y la semántica dadas en 2920 2921 2922 :ref:`spec-Run-time-Outcomes`, and is discussed in detail in :ref:`spec-Output`. 2923 2924La sintaxis completa es la siguiente: 2925 2926.. literalinclude:: output.mzn 2927 :language: minizincdef 2928 2929El texto de la solución para cada solución debe ser como se describe en :ref:`spec-Output-Items`. 2930Se debe agregar una nueva línea si el texto de la solución no finaliza con una nueva línea. 2931 2932.. _spec-json: 2933 2934 2935 2936Soporte de JSON 2937----------------------------- 2938 2939MiniZinc puede admitir la lectura de parámetros de entrada y proporcionar resultados formateados como objetos JSON. Un archivo de entrada JSON debe tener la siguiente estructura: 2940 2941- Consiste en un solo objeto de nivel superior 2942 2943- Los miembros del objeto (pares clave-valor) representan parámetros del modelo 2944 2945- Cada clave miembro debe ser un identificador MiniZinc válido (y proporciona el valor para el parámetro correspondiente del modelo) 2946 2947- Cada valor de miembro puede ser uno de los siguientes: 2948 2949 - Una cadena (asignado a un parámetro de cadena MiniZinc) 2950 2951 - Un número (asignado a un parámetro MiniZinc int o float) 2952 2953 - Los valores ``true`` o ``false`` (asignado a un parámetro bool MiniZinc) 2954 2955 - Una matriz de valores. Las matrices de matrices solo se admiten si todas las matrices internas tienen la misma longitud, por lo que se pueden asignar a matrices multidimensionales MiniZinc. 2956 2957 - Un conjunto de valores codificados como un objeto con un único miembro con clave ``"set"`` y una lista de valores (los elementos del conjunto). 2958 2959Este es un ejemplo de un archivo de parámetros JSON que utiliza todas las características anteriores: 2960 2961.. code-block:: json 2962 2963 { 2964 "n" : 3, 2965 "distances" : [ [1,2,3], 2966 [4,5,6]], 2967 "patterns" : [ {"set" : [1,3,5]}, {"set" : [2,4,6]} ] 2968 } 2969 2970 2971El primer parámetro declara un entero simple ``n``. El parámetro ``distances`` es una matriz bidimensional; tenga en cuenta que todas las matrices internas deben ser del mismo tamaño para mapearse en una matriz bidimensional (rectangular) MiniZinc. El tercer parámetro es una matriz de conjuntos de enteros. 2972 2973.. _spec-grammar: 2974 2975 2976 2977Gramática completa 2978------------------ 2979 2980Elementos 2981~~~~~~~~~ 2982 2983.. literalinclude:: grammar.mzn 2984 :language: minizincdef 2985 :end-before: % Type-inst expressions 2986 2987Expresiones de Tipo-Instanciación 2988~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 2989 2990.. literalinclude:: grammar.mzn 2991 :language: minizincdef 2992 :start-after: % Type-inst expressions 2993 :end-before: % Expressions 2994 2995Expresiones 2996~~~~~~~~~~~ 2997 2998.. literalinclude:: grammar.mzn 2999 :language: minizincdef 3000 :start-after: % Expressions 3001 :end-before: % Miscellaneous 3002 3003Elementos Misceláneos 3004~~~~~~~~~~~~~~~~~~~~~~~ 3005 3006.. literalinclude:: grammar.mzn 3007 :language: minizincdef 3008 :start-after: % Miscellaneous 3009