this repo has no description
dekker.one
1.. |coerce| replace:: :math:`\stackrel{c}{\rightarrow}`
2
3.. |varify| replace:: :math:`\stackrel{v}{\rightarrow}`
4
5.. |TyOverview| replace:: *Overview.*
6
7.. |TyInsts| replace:: *Allowed Insts.*
8
9.. |TySyntax| replace:: *Syntax.*
10
11.. |TyFiniteType| replace:: *Finite?*
12
13.. |TyVarifiable| replace:: *Varifiable?*
14
15.. |TyOrdering| replace:: *Ordering.*
16
17.. |TyInit| replace:: *Initialisation.*
18
19.. |TyCoercions| replace:: *Coercions.*
20
21.. _ch-mzn-spec:
22
23Specification of MiniZinc
24=========================
25
26Introduction
27------------
28
29This document defines MiniZinc, a language for modelling constraint
30satisfaction and optimisation problems.
31
32MiniZinc is a high-level, typed, mostly first-order, functional, modelling
33language. It provides:
34
35- mathematical notation-like syntax (automatic coercions, overloading,
36 iteration, sets, arrays);
37- expressive constraints (finite domain, set, linear arithmetic, integer);
38- support for different kinds of problems (satisfaction, explicit
39 optimisation);
40- separation of data from model;
41- high-level data structures and data encapsulation (sets,
42 arrays, enumerated types, constrained type-insts);
43- extensibility (user-defined functions and predicates);
44- reliability (type checking, instantiation checking, assertions);
45- solver-independent modelling;
46- simple, declarative semantics.
47
48MiniZinc is similar to
49OPL and moves closer to CLP languages such as ECLiPSe.
50
51This document has the following structure.
52:ref:`spec-syntax-notation` introduces the syntax notation
53used throughout the specification.
54:ref:`spec-Overview` provides a high-level overview of MiniZinc models.
55:ref:`spec-Syntax-Overview` covers syntax basics.
56:ref:`spec-High-level-Model-Structure` covers high-level structure: items,
57multi-file models, namespaces, and scopes.
58:ref:`spec-Types` introduces types and type-insts.
59:ref:`spec-Expressions` covers expressions.
60:ref:`spec-Items` describes the top-level items in detail.
61:ref:`spec-Annotations` describes annotations.
62:ref:`spec-Partiality` describes how partiality is handled in various
63cases.
64:ref:`spec-builtins` describes the language built-ins.
65:ref:`spec-Grammar` gives the MiniZinc grammar.
66:ref:`spec-Content-types` defines content-types used in this specification.
67
68This document also provides some explanation of why certain design decisions
69were made. Such explanations are marked by the word *Rationale* and
70written in italics, and do not constitute part of the specification as such.
71*Rationale: These explanations are present because they are useful to both
72the designers and the users of MiniZinc.*
73
74Original authors.
75~~~~~~~~~~~~~~~~~
76
77The original version of this document was prepared by
78Nicholas Nethercote, Kim Marriott, Reza Rafeh, Mark Wallace
79and Maria Garcia de la Banda.
80MiniZinc is evolving, however, and so is this document.
81
82For a formally published paper on the MiniZinc language
83and the superset Zinc language, please see:
84
85- N. Nethercote, P.J. Stuckey, R. Becket, S. Brand, G.J. Duck, and G. Tack.
86 Minizinc: Towards a standard CP modelling language.
87 In C. Bessiere, editor, *Proceedings of the 13th International
88 Conference on Principles and Practice of Constraint Programming*, volume 4741
89 of *LNCS*, pages 529--543. Springer-Verlag, 2007.
90- K. Marriott, N. Nethercote, R. Rafeh, P.J. Stuckey,
91 M. Garcia de la Banda, and M. Wallace.
92 The Design of the Zinc Modelling Language.
93 *Constraints*, 13(3):229-267, 2008.
94
95.. _spec-syntax-notation:
96
97Notation
98--------
99
100The basics of the EBNF used in this specification are as follows.
101
102- Non-terminals are written between angle brackets, :mzndef:`<item>`.
103- Terminals are written in double quotes, e.g. :mzndef:`"constraint"`.
104 A double quote terminal is written as a sequence of three double quotes: :mzndef:`"""`.
105- Optional items are written in square brackets,
106 e.g. :mzndef:`[ "var" ]`.
107- Sequences of zero or more items are written with parentheses and a
108 star, e.g. :mzndef:`( "," <ident> )*`.
109- Sequences of one or more items are written with parentheses and a
110 plus, e.g. :mzndef:`( <msg> )+`.
111- Non-empty lists are written with an item, a separator/terminator
112 terminal, and three dots. For example, this:
113
114 .. code-block:: minizincdef
115
116 <expr> "," ...
117
118 is short for this:
119
120 .. code-block:: minizincdef
121
122 <expr> ( "," <expr> )* [ "," ]
123
124 The final terminal is always optional in non-empty lists.
125- Regular expressions are used in some
126 productions, e.g. :mzndef:`[-+]?[0-9]+`.
127
128MiniZinc's grammar is presented piece-by-piece throughout this document. It is
129also available as a whole in :ref:`spec-Grammar`.
130The output grammar also includes some details of the use of whitespace.
131The following conventions are used:
132
133- A newline character or CRLF sequence is written ``\n``.
134
135.. - A sequence of space characters of length :math:`n` is written ``nSP``, e.g., ``2SP``.
136
137.. _spec-Overview:
138
139Overview of a Model
140-------------------
141
142Conceptually, a MiniZinc problem specification has two parts.
143
1441. The *model*: the main part of the problem specification, which
145 describes the structure of a particular class of problems.
1462. The *data*: the input data for the model, which specifies one
147 particular problem within this class of problems.
148
149The pairing of a model with a particular data set is a *model
150instance* (sometimes abbreviated to *instance*).
151
152The model and data may be separated, or the data
153may be "hard-wired" into the model.
154:ref:`spec-Model-Instance-Files` specifies how the model and data can be
155structured within files in a model instance.
156
157There are two broad classes of problems: satisfaction and optimisation.
158In satisfaction problems all solutions are considered equally good,
159whereas in optimisation problems the solutions are
160ordered according to an objective and
161the aim is to find a solution whose objective is optimal.
162:ref:`spec-Solve-Items` specifies how the class of problem is chosen.
163
164Evaluation Phases
165~~~~~~~~~~~~~~~~~
166
167A MiniZinc model instance is evaluated in two distinct phases.
168
1691. Instance-time: static checking of the model instance.
1702. Run-time: evaluation of the instance (i.e., constraint solving).
171
172The model instance may not compile due to a problem with the model and/or data,
173detected at instance-time.
174This could be caused by a syntax error, a type-inst error,
175the use of an unsupported feature or operation, etc.
176In this case the outcome of evaluation is a static error;
177this must be reported prior to run-time.
178The form of output for static errors is implementation-dependent,
179although such output should be easily recognisable as a static error.
180
181An implementation may produce warnings during all evaluation phases.
182For example, an implementation may be able to determine that
183unsatisfiable constraints exist prior to run-time,
184and the resulting warning given to the user may be more helpful than
185if the unsatisfiability is detected at run-time.
186
187An implementation must produce a warning
188if the objective for an optimisation problem is unbounded.
189
190
191.. _spec-run-time-outcomes:
192
193Run-time Outcomes
194~~~~~~~~~~~~~~~~~
195
196Assuming there are no static errors,
197the output from the run-time phase has the following abstract form:
198
199.. literalinclude:: output.mzn
200 :language: minizincdef
201 :start-after: % Output
202 :end-before: %
203
204If a solution occurs in the output
205then it must be feasible.
206For optimisation problems,
207each solution must be strictly better than any preceding solution.
208
209If there are no solutions in the output,
210the outcome must indicate that there are no solutions.
211
212If the search is complete the output may state this after the solutions.
213The absence of the completeness message indicates that the search is incomplete.
214
215Any warnings produced during run-time must be summarised
216after the statement of completeness.
217In particular, if there were any warnings at all during run-time
218then the summary must indicate this fact.
219
220The implementation may produce text in any format after the warnings.
221For example, it may print
222a summary of benchmarking statistics or resources used.
223
224.. _spec-output:
225
226Output
227~~~~~~
228
229Implementations must be capable of producing output of content type
230``application/x-zinc-output``,
231which is described below and also in :ref:`spec-Content-types`.
232Implementations may also produce output in alternative formats.
233Any output should conform to
234the abstract format from the previous section
235and must have the semantics described there.
236
237Content type ``application/x-zinc-output`` extends
238the syntax from the previous section as follows:
239
240.. literalinclude:: output.mzn
241 :language: minizincdef
242 :start-after: % Solutions
243 :end-before: %
244
245The solution text for each solution must be
246as described in :ref:`spec-Output-Items`.
247A newline must be appended if the solution text does not end with a newline.
248*Rationale: This allows solutions to be extracted from output
249without necessarily knowing how the solutions are formatted.*
250Solutions end with a sequence of ten dashes followed by a newline.
251
252.. literalinclude:: output.mzn
253 :language: minizincdef
254 :start-after: % Unsatisfiable
255 :end-before: %
256
257The completness result is printed on a separate line.
258*Rationale: The strings are designed to clearly indicate
259the end of the solutions.*
260
261.. literalinclude:: output.mzn
262 :language: minizincdef
263 :start-after: % Complete
264 :end-before: %
265
266If the search is complete, a statement corresponding to the outcome is printed.
267For an outcome of no solutions
268the statement is that the model instance is unsatisfiable,
269for an outcome of no more solutions
270the statement is that the solution set is complete,
271and for an outcome of no better solutions
272the statement is that the last solution is optimal.
273*Rationale: These are the logical implications of a search being complete.*
274
275.. literalinclude:: output.mzn
276 :language: minizincdef
277 :start-after: % Messages
278 :end-before: %
279
280If the search is incomplete,
281one or more messages describing reasons for incompleteness may be printed.
282Likewise, if any warnings occurred during search
283they are repeated after the completeness message.
284Both kinds of message should have lines that start with ``%``
285so they are recognized as comments by post-processing.
286*Rationale: This allows individual messages to be easily recognised.*
287
288For example, the following may be output for an optimisation problem:
289
290.. code-block:: bash
291
292 =====UNSATISFIABLE=====
293 % trentin.fzn:4: warning: model inconsistency detected before search.
294
295Note that, as in this case,
296an unbounded objective is not regarded as a source of incompleteness.
297
298.. _spec-syntax-overview:
299
300Syntax Overview
301---------------
302
303Character Set
304~~~~~~~~~~~~~
305
306The input files to MiniZinc must be encoded as UTF-8.
307
308MiniZinc is case sensitive. There are no places where upper-case or
309lower-case letters must be used.
310
311MiniZinc has no layout restrictions, i.e., any single piece of whitespace
312(containing spaces, tabs and newlines) is equivalent to any other.
313
314
315Comments
316~~~~~~~~
317
318A ``%`` indicates that the rest of the line is a comment. MiniZinc
319also has block comments, using symbols ``/*`` and ``*/``
320to mark the beginning and end of a comment.
321
322.. _spec-identifiers:
323
324Identifiers
325~~~~~~~~~~~
326
327Identifiers have the following syntax:
328
329.. code-block:: minizincdef
330
331 <ident> ::= [A-Za-z][A-Za-z0-9_]* % excluding keywords
332 | "'" [^'\xa\xd\x0]* "'"
333
334.. code-block:: minizinc
335
336 my_name_2
337 MyName2
338 'An arbitrary identifier'
339
340A number of keywords are reserved and cannot be used as identifiers. The
341keywords are:
342:mzn:`ann`,
343:mzn:`annotation`,
344:mzn:`any`,
345:mzn:`array`,
346:mzn:`bool`,
347:mzn:`case`,
348:mzn:`constraint`,
349:mzn:`diff`,
350:mzn:`div`,
351:mzn:`else`,
352:mzn:`elseif`,
353:mzn:`endif`,
354:mzn:`enum`,
355:mzn:`false`,
356:mzn:`float`,
357:mzn:`function`,
358:mzn:`if`,
359:mzn:`in`,
360:mzn:`include`,
361:mzn:`int`,
362:mzn:`intersect`,
363:mzn:`let`,
364:mzn:`list`,
365:mzn:`maximize`,
366:mzn:`minimize`,
367:mzn:`mod`,
368:mzn:`not`,
369:mzn:`of`,
370:mzn:`op`,
371:mzn:`opt`,
372:mzn:`output`,
373:mzn:`par`,
374:mzn:`predicate`,
375:mzn:`record`,
376:mzn:`satisfy`,
377:mzn:`set`,
378:mzn:`solve`,
379:mzn:`string`,
380:mzn:`subset`,
381:mzn:`superset`,
382:mzn:`symdiff`,
383:mzn:`test`,
384:mzn:`then`,
385:mzn:`true`,
386:mzn:`tuple`,
387:mzn:`type`,
388:mzn:`union`,
389:mzn:`var`,
390:mzn:`where`,
391:mzn:`xor`.
392
393A number of identifiers are used for built-ins; see :ref:`spec-builtins`
394for details.
395
396.. _spec-High-level-Model-Structure:
397
398High-level Model Structure
399--------------------------
400
401A MiniZinc model consists of multiple *items*:
402
403.. literalinclude:: grammar.mzn
404 :language: minizincdef
405 :start-after: % A MiniZinc model
406 :end-before: %
407
408Items can occur in any order; identifiers need not be declared before they are used. Items have the following top-level syntax:
409
410.. literalinclude:: grammar.mzn
411 :language: minizincdef
412 :start-after: % Items
413 :end-before: %
414
415Include items provide a way of combining multiple files into a single
416instance. This allows a model to be split into multiple files
417(:ref:`spec-Include-Items`).
418
419Variable declaration items introduce new global variables and possibly
420bind them to a value (:ref:`spec-Declarations`).
421
422Assignment items bind values to global variables
423(:ref:`spec-Assignments`).
424
425Constraint items describe model constraints (:ref:`spec-Constraint-Items`).
426
427Solve items are the "starting point" of a model, and specify exactly
428what kind of solution is being looked for: plain satisfaction, or the
429minimization/maximization of an expression. Each model must have exactly
430one solve item (:ref:`spec-Solve-Items`).
431
432Output items are used for nicely presenting the result of a model
433execution (:ref:`spec-Output-Items`).
434
435Predicate items, test items (which are just a special type of predicate)
436and function items introduce new user-defined predicates and
437functions which can be called in expressions (:ref:`spec-preds-and-fns`).
438Predicates, functions, and built-in operators are described collectively as
439*operations*.
440
441Annotation items augment the :mzn:`ann` type, values of which can specify
442non-declarative and/or solver-specific information in a model.
443
444.. _spec-model-instance-files:
445
446Model Instance Files
447~~~~~~~~~~~~~~~~~~~~
448
449MiniZinc models can be constructed from multiple files using
450include items (see :ref:`spec-Include-Items`). MiniZinc has no
451module system as such; all the included files are simply concatenated and
452processed as a whole, exactly as if they had all been part of a single file.
453*Rationale: We have not found much need for one so far. If bigger models
454become common and the single global namespace becomes a problem, this should
455be reconsidered.*
456
457Each model may be paired with one or more data files. Data files are more
458restricted than model files. They may only contain variable assignments (see
459:ref:`spec-Assignments`).
460
461Data files may not include calls to user-defined operations.
462
463Models do not contain the names of data files; doing so would fix the data
464file used by the model and defeat the purpose of allowing separate data
465files. Instead, an implementation must allow one or more data files to be
466combined with a model for evaluation via a mechanism such as the
467command-line.
468
469When checking a model with
470data, all global variables with fixed type-insts must be assigned, unless
471they are not used (in which case they can be removed from the model without
472effect).
473
474A data file can only be checked for static errors in conjunction with a
475model, since the model contains the declarations that include the types of
476the variables assigned in the data file.
477
478A single data file may be shared between multiple models, so long as the
479definitions are compatible with all the models.
480
481.. _spec-namespaces:
482
483Namespaces
484~~~~~~~~~~
485
486All names declared at the top-level belong to a single namespace.
487It includes the following names.
488
4891. All global variable names.
4902. All function and predicate names, both built-in and user-defined.
4913. All enumerated type names and enum case names.
4924. All annotation names.
493
494Because multi-file MiniZinc models are composed via
495concatenation (:ref:`spec-Model-Instance-Files`), all files share
496this top-level namespace. Therefore a variable ``x`` declared in one
497model file could not be declared with a different type in a different file,
498for example.
499
500MiniZinc supports overloading of built-in and user-defined operations.
501
502.. _spec-scopes:
503
504Scopes
505~~~~~~
506
507Within the top-level namespace, there are several kinds of local scope that
508introduce local names:
509
510- Comprehension expressions (:ref:`spec-Set-Comprehensions`).
511- Let expressions (:ref:`spec-Let-Expressions`).
512- Function and predicate argument lists and bodies (:ref:`spec-preds-and-fns`).
513
514The listed sections specify these scopes in more detail. In each case, any
515names declared in the local scope overshadow identical global names.
516
517.. _spec-types:
518
519Types and Type-insts
520--------------------
521
522MiniZinc provides four scalar built-in types: Booleans, integers, floats, and
523strings; enumerated types; two compound built-in types: sets and multi-dimensional arrays;
524and the user extensible annotation type :mzn:`ann`.
525
526Each type has one or more possible *instantiations*. The
527instantiation of a variable or value indicates if it is fixed to a known
528value or not. A pairing of a type and instantiation is called a
529*type-inst*.
530
531We begin by discussing some properties that apply to every type. We then
532introduce instantiations in more detail. We then cover each type
533individually, giving: an overview of the type and its possible
534instantiations, the syntax for its type-insts, whether it is a finite
535type (and if so, its domain), whether it is varifiable, the ordering and
536equality operations, whether its variables must be initialised at
537instance-time, and whether it can be involved in automatic coercions.
538
539Properties of Types
540~~~~~~~~~~~~~~~~~~~
541
542The following list introduces some general properties of MiniZinc types.
543
544- Currently all types are monotypes. In the future we may allow types which
545 are polymorphic in other types and also the associated constraints.
546- We distinguish types which are *finite types*. In MiniZinc, finite types
547 include Booleans, enums, types defined via set expression type-insts such
548 as range types (see :ref:`spec-Set-Expression-Type-insts`), as well as
549 sets and arrays, composed of finite types. Types that are not finite types
550 are unconstrained integers, unconstrained floats, unconstrained strings,
551 and :mzn:`ann`. Finite types are relevant to sets (:mzn:`spec-Sets`) and
552 array indices (:mzn:`spec-Arrays`). Every finite type has a *domain*,
553 which is a set value that holds all the possible values represented by the
554 type.
555- Every first-order type (this excludes :mzn:`ann`) has a built-in total
556 order and a built-in equality; ``>``, ``<``, ``==``/``=``, ``!=``, ``<=``
557 and ``>=`` comparison operators can be applied to any pair of values of
558 the same type. *Rationale: This facilitates the specification of symmetry
559 breaking and of polymorphic predicates and functions.* Note that, as in
560 most languages, using equality on floats or types that contain floats is
561 generally not reliable due to their inexact representation. An
562 implementation may choose to warn about the use of equality with floats or
563 types that contain floats.
564
565.. _spec-instantiations:
566
567Instantiations
568~~~~~~~~~~~~~~
569
570When a MiniZinc model is evaluated, the value of each variable may initially
571be unknown. As it runs, each variable's *domain* (the set of
572values it may take) may be reduced, possibly to a single value.
573
574An *instantiation* (sometimes abbreviated to *inst*) describes
575how fixed or unfixed a variable is at instance-time. At the most basic
576level, the instantiation system distinguishes between two kinds of
577variables:
578
579#. *Parameters*, whose values are fixed at instance-time (usually written just as "fixed").
580#. *Decision variables* (often abbreviated to *variables*), whose values may
581 be completely unfixed at instance-time, but may become fixed at run-time
582 (indeed, the fixing of decision variables is the whole aim of constraint
583 solving).
584
585In MiniZinc decision variables can have the following types: Booleans,
586integers, floats, and sets of integers, and enums.
587Arrays and :mzn:`ann` can contain decision variables.
588
589.. _spec-type-inst:
590
591Type-insts
592~~~~~~~~~~
593
594Because each variable has both a type and an inst, they are often
595combined into a single *type-inst*. Type-insts are primarily what
596we deal with when writing models, rather than types.
597
598A variable's type-inst *never changes*. This means a decision
599variable whose value becomes fixed during model evaluation still has its
600original type-inst (e.g. :mzn:`var int`), because that was its
601type-inst at instance-time.
602
603Some type-insts can be automatically coerced to another type-inst. For
604example, if a :mzn:`par int` value is used in a context where a
605:mzn:`var int` is expected, it is automatically coerced to a
606:mzn:`var int`. We write this :mzn:`par int` |coerce| :mzn:`var int`.
607Also, any type-inst can be considered coercible to itself.
608MiniZinc allows coercions between some types as well.
609
610Some type-insts can be *varified*, i.e., made unfixed at the top-level.
611For example, :mzn:`par int` is varified to :mzn:`var int`. We write this
612:mzn:`par int` |varify| :mzn:`var int`.
613
614Type-insts that are varifiable include the type-insts of the types that can
615be decision variables (Booleans, integers, floats, sets, enumerated types).
616Varification is relevant to type-inst synonyms and
617array accesses.
618
619Type-inst expression overview
620~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
621
622This section partly describes how to write type-insts in MiniZinc models.
623Further details are given for each type as they are described in the
624following sections.
625
626A type-inst expression specifies a type-inst.
627Type-inst expressions may include type-inst constraints.
628Type-inst expressions appear in variable declarations
629(:ref:`spec-Declarations`) and user-defined operation items
630(:ref:`spec-preds-and-fns`).
631
632Type-inst expressions have this syntax:
633
634.. literalinclude:: grammar.mzn
635 :language: minizincdef
636 :start-after: % Type-inst expressions
637 :end-before: %
638
639(The final alternative, for range types, uses the numeric-specific
640:mzndef:`<num-expr>` non-terminal, defined in :ref:`spec-Expressions-Overview`,
641rather than the :mzndef:`<expr>` non-terminal. If this were not the case, the rule
642would never match because the ``..`` operator would always be matched
643by the first :mzndef:`<expr>`.)
644
645This fully covers the type-inst expressions for scalar types. The compound
646type-inst expression syntax is covered in more detail in
647:ref:`spec-Built-in-Compound-Types`.
648
649The :mzn:`par` and :mzn:`var` keywords (or lack of them) determine the
650instantiation. The :mzn:`par` annotation can be omitted; the following
651two type-inst expressions are equivalent:
652
653.. code-block:: minizinc
654
655 par int
656 int
657
658*Rationale: The use of the explicit* :mzn:`var` *keyword allows an
659implementation to check that all parameters are initialised in the model or
660the instance. It also clearly documents which variables are parameters, and
661allows more precise type-inst checking.*
662
663A type-inst is fixed if it does not contain :mzn:`var`,
664with the exception of :mzn:`ann`.
665
666Note that several type-inst expressions that are syntactically expressible
667represent illegal type-insts. For example, although the grammar allows
668:mzn:`var` in front of all these base type-inst expression tails, it is a
669type-inst error to have :mzn:`var` in the front of a string or array
670expression.
671
672.. _spec-built-in-scalar-types:
673
674Built-in Scalar Types and Type-insts
675~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
676
677Booleans
678++++++++
679
680|TyOverview|
681Booleans represent truthhood or falsity. *Rationale: Boolean values are
682not represented by integers.
683Booleans can be explicit converted to
684integers with the* :mzn:`bool2int` *function, which makes the user's intent
685clear.*
686
687|TyInsts|
688Booleans can be fixed or unfixed.
689
690|TySyntax|
691Fixed Booleans are written :mzn:`bool` or :mzn:`par bool`. Unfixed
692Booleans are written as :mzn:`var bool`.
693
694|TyFiniteType|
695Yes. The domain of a Boolean is :mzn:`false, true`.
696
697|TyVarifiable|
698:mzn:`par bool` |varify| :mzn:`var bool`, :mzn:`var bool` |varify| :mzn:`var bool`.
699
700|TyOrdering|
701The value :mzn:`false` is considered smaller than :mzn:`true`.
702
703|TyInit|
704A fixed Boolean variable must be initialised at instance-time; an unfixed
705Boolean variable need not be.
706
707|TyCoercions|
708:mzn:`par bool` |coerce| :mzn:`var bool`.
709
710Also Booleans can be automatically coerced to integers; see
711:ref:`spec-Integers`.
712
713.. _spec-integers:
714
715Integers
716++++++++
717
718|TyOverview|
719Integers represent integral numbers. Integer representations are
720implementation-defined. This means that the representable range of
721integers is implementation-defined. However, an implementation should
722abort at run-time if an integer operation overflows.
723
724|TyInsts|
725Integers can be fixed or unfixed.
726
727|TySyntax|
728Fixed integers are written :mzn:`int` or :mzn:`par int`. Unfixed
729integers are written as :mzn:`var int`.
730
731|TyFiniteType|
732Not unless constrained by a set expression (see :ref:`spec-Set-Expression-Type-insts`).
733
734|TyVarifiable|
735:mzn:`par int` |varify| :mzn:`var int`,
736:mzn:`var int` |varify| :mzn:`var int`.
737
738|TyOrdering|
739The ordering on integers is the standard one.
740
741|TyInit|
742A fixed integer variable must be initialised at instance-time; an unfixed
743integer variable need not be.
744
745|TyCoercions|
746:mzn:`par int` |coerce| :mzn:`var int`,
747:mzn:`par bool` |coerce| :mzn:`par int`,
748:mzn:`par bool` |coerce| :mzn:`var int`,
749:mzn:`var bool` |coerce| :mzn:`var int`.
750
751Also, integers can be automatically coerced to floats; see
752:ref:`spec-Floats`.
753
754
755.. _spec-floats:
756
757Floats
758++++++
759
760|TyOverview|
761Floats represent real numbers. Float representations are
762implementation-defined. This means that the representable range and
763precision of floats is implementation-defined. However, an
764implementation should abort at run-time on exceptional float operations
765(e.g., those that produce ``NaN``, if using IEEE754 floats).
766
767|TyInsts|
768Floats can be fixed or unfixed.
769
770|TySyntax|
771Fixed floats are written :mzn:`float` or :mzn:`par float`. Unfixed
772floats are written as :mzn:`var float`.
773
774|TyFiniteType|
775Not unless constrained by a set expression (see :ref:`spec-Set-Expression-Type-insts`).
776
777|TyVarifiable|
778:mzn:`par float` |varify| :mzn:`var float`,
779:mzn:`var float` |varify| :mzn:`var float`.
780
781|TyOrdering|
782The ordering on floats is the standard one.
783
784|TyInit|
785A fixed float variable must be initialised at instance-time; an unfixed
786float variable need not be.
787
788|TyCoercions|
789:mzn:`par int` |coerce| :mzn:`par float`,
790:mzn:`par int` |coerce| :mzn:`var float`,
791:mzn:`var int` |coerce| :mzn:`var float`,
792:mzn:`par float` |coerce| :mzn:`var float`.
793
794.. _spec-enumerated-types:
795
796Enumerated Types
797++++++++++++++++
798
799|TyOverview|
800Enumerated types (or *enums* for short) provide a set of named
801alternatives. Each alternative is identified by its *case name*.
802Enumerated types, like in many other languages, can be used in the place of
803integer types to achieve stricter type checking.
804
805|TyInsts|
806Enums can be fixed or unfixed.
807
808|TySyntax|
809Variables of an enumerated type named ``X`` are represented by the term
810:mzn:`X` or :mzn:`par X` if fixed, and :mzn:`var X`
811if unfixed.
812
813|TyFiniteType|
814Yes.
815
816The domain of an enum is the set containing all of its case names.
817
818|TyVarifiable|
819:mzn:`par X` |varify| :mzn:`var X`,
820:mzn:`var X` |varify| :mzn:`var X`.
821
822|TyOrdering|
823When two enum values with different case names are compared, the value with
824the case name that is declared first is considered smaller than the value
825with the case name that is declared second.
826
827|TyInit|
828A fixed enum variable must be initialised at instance-time; an unfixed
829enum variable need not be.
830
831|TyCoercions|
832:mzn:`par X` |coerce| :mzn:`par int`,
833:mzn:`var X` |coerce| :mzn:`var int`.
834
835.. _spec-strings:
836
837Strings
838+++++++
839
840|TyOverview|
841Strings are primitive, i.e., they are not lists of characters.
842
843String expressions are used in assertions, output items and
844annotations, and string literals are used in include items.
845
846|TyInsts|
847Strings must be fixed.
848
849|TySyntax|
850Fixed strings are written :mzn:`string` or :mzn:`par string`.
851
852|TyFiniteType|
853Not unless constrained by a set expression (see :ref:`spec-Set-Expression-Type-insts`).
854
855|TyVarifiable|
856No.
857
858|TyOrdering|
859Strings are ordered lexicographically using the underlying character codes.
860
861|TyInit|
862A string variable (which can only be fixed) must be initialised at
863instance-time.
864
865|TyCoercions|
866None automatic. However, any non-string value can be manually converted to
867a string using the built-in :mzn:`show` function or using string interpolation
868(see :ref:`spec-String-Interpolation-Expressions`).
869
870.. _spec-Built-in-Compound-Types:
871
872Built-in Compound Types and Type-insts
873~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
874
875.. _spec-sets:
876
877Sets
878++++
879
880|TyOverview|
881A set is a collection with no duplicates.
882
883|TyInsts|
884The type-inst of a set's elements must be fixed. *Rationale: This is because
885current solvers are not powerful enough to handle sets containing decision
886variables.*
887Sets may contain any type, and may be fixed or unfixed.
888If a set is unfixed, its elements must be finite, unless it occurs in one
889of the following contexts:
890
891- the argument of a predicate, function or annotation.
892- the declaration of a variable or let local variable with an
893 assigned value.
894
895|TySyntax|
896A set base type-inst expression is a special case of the base type-inst rule:
897
898.. code-block:: minizincdef
899
900 <base-ti-expr> ::= <var-par> <opt-ti> "set" "of" <base-ti-expr-tail>
901
902Some example set type-inst expressions:
903
904.. code-block:: minizinc
905
906 set of int
907 var set of bool
908
909|TyFiniteType|
910Yes, if the set elements are finite types. Otherwise, no.
911
912The domain of a set type that is a finite type is the powerset of the domain
913of its element type. For example, the domain of :mzn:`set of 1..2` is
914:mzn:`powerset(1..2)`, which is :mzn:`{}, {1}, {1,2}, {2}`.
915
916|TyVarifiable|
917:mzn:`par set of TI` |varify| :mzn:`var set of TI`,
918:mzn:`var set of TI` |varify| :mzn:`var set of TI`.
919
920|TyOrdering|
921The pre-defined ordering on sets is a lexicographic ordering of the
922*sorted set form*, where :mzn:`{1,2}` is in sorted set form, for example,
923but :mzn:`{2,1}` is not.
924This means, for instance, :mzn:`{} < {1,3} < {2}`.
925
926|TyInit|
927A fixed set variable must be initialised at instance-time; an unfixed
928set variable need not be.
929
930|TyCoercions|
931:mzn:`par set of TI` |coerce| :mzn:`par set of UI` and
932:mzn:`par set of TI` |coerce| :mzn:`var set of UI` and
933:mzn:`var set of TI` |coerce| :mzn:`var set of UI`, if
934:mzn:`TI` |coerce| :mzn:`UI`.
935
936Arrays
937++++++
938
939|TyOverview|
940MiniZinc arrays are maps from fixed integers to values.
941Values can be of any type.
942The values can only have base type-insts.
943Arrays-of-arrays are not allowed.
944Arrays can be multi-dimensional.
945
946MiniZinc arrays can be declared in two different ways.
947
948- *Explicitly-indexed* arrays have index types in the declaration
949 that are finite types. For example:
950
951 .. code-block:: minizinc
952
953 array[1..3] of int: a1;
954 array[0..3] of int: a2;
955 array[1..5, 1..10] of var float: a5;
956
957 For such arrays, the index type specifies exactly the indices that will
958 be in the array - the array's index set is the *domain* of the
959 index type - and if the indices of the value assigned do not match then
960 it is a run-time error.
961
962 For example, the following assignments cause run-time errors:
963
964 .. code-block:: minizinc
965
966 a1 = [4,6,4,3,2]; % too many elements
967 a2 = [3,2,6,5]; % index set mismatch
968 a5 = [||]; % too few elements
969
970 For :mzn:`a2` above, the index set of the array literal :mzn:`[3,2,6,5]`
971 is (implicitly) :mzn:`1..4`, so it cannot be assigned to an array declared
972 with index set :mzn:`0..3`, even though the length matches. A correct
973 assignment would use the :mzn:`array1d` function (see :ref:`sec-array-ops`):
974
975 .. code-block:: minizinc
976
977 a2 = array1d(0..3,[3,2,6,5]); % correct
978- *Implicitly-indexed* arrays have index types in the declaration
979 that are not finite types. For example:
980
981 .. code-block:: minizinc
982
983 array[int,int] of int: a6;
984
985 No checking of indices occurs when these variables are assigned.
986
987In MiniZinc all index sets of an array must be contiguous ranges of
988integers, or enumerated types. The expression used for initialisation of an
989array must have matching index sets. An array expression with an enum index
990set can be assigned to an array declared with an integer index set, but not
991the other way around. The exception are array literals, which can be
992assigned to arrays declared with enum index sets.
993
994For example:
995
996.. code-block:: minizinc
997
998 enum X = {A,B,C};
999 enum Y = {D,E,F};
1000 array[X] of int: x = array1d(X, [5,6,7]); % correct
1001 array[Y] of int: y = x; % index set mismatch: Y != X
1002 array[int] of int: z = x; % correct: assign X index set to int
1003 array[X] of int: x2 = [10,11,12]; % correct: automatic coercion for array literals
1004
1005The initialisation of an array can be done in a separate assignment
1006statement, which may be present in the model or a separate data file.
1007
1008Arrays can be accessed. See :ref:`spec-Array-Access-Expressions` for
1009details.
1010
1011|TyInsts|
1012An array's size must be fixed. Its indices must also have
1013fixed type-insts. Its elements may be fixed or unfixed.
1014
1015|TySyntax|
1016An array base type-inst expression tail has this syntax:
1017
1018.. literalinclude:: grammar.mzn
1019 :language: minizincdef
1020 :start-after: % Array type-inst expressions
1021 :end-before: %
1022
1023Some example array type-inst expressions:
1024
1025.. code-block:: minizinc
1026
1027 array[1..10] of int
1028 list of var int
1029
1030Note that :mzndef:`list of <T>` is just syntactic sugar for
1031:mzndef:`array[int] of <T>`. *Rationale: Integer-indexed arrays of this form
1032are very common, and so worthy of special support to make things easier for
1033modellers. Implementing it using syntactic sugar avoids adding an extra
1034type to the language, which keeps things simple for implementers.*
1035
1036Because arrays must be fixed-size it is a type-inst error to precede an
1037array type-inst expression with :mzn:`var`.
1038
1039|TyFiniteType|
1040Yes, if the index types and element type are all finite types.
1041Otherwise, no.
1042
1043The domain of an array type that is a finite array is the set of all
1044distinct arrays whose index set equals the domain of the index type
1045and whose elements are of the array element type.
1046
1047|TyVarifiable|
1048No.
1049
1050|TyOrdering|
1051Arrays are ordered lexicographically, taking absence of a value for a given key
1052to be before any value for that key. For example,
1053:mzn:`[1, 1]` is less than
1054:mzn:`[1, 2]`, which is less than :mzn:`[1, 2, 3]` and
1055:mzn:`array1d(2..4,[0, 0, 0])` is less than :mzn:`[1, 2, 3]`.
1056
1057|TyInit|
1058An explicitly-indexed array variable must be initialised at instance-time
1059only if its elements must be initialised at instance time.
1060An implicitly-indexed array variable must be initialised at instance-time
1061so that its length and index set is known.
1062
1063|TyCoercions|
1064:mzn:`array[TI0] of TI` |coerce| :mzn:`array[UI0] of UI` if
1065:mzn:`TI0` |coerce| :mzn:`UI0` and :mzn:`TI` |coerce| :mzn:`UI`.
1066
1067.. _spec-option-types:
1068
1069Option Types
1070++++++++++++
1071
1072|TyOverview|
1073Option types defined using the :mzn:`opt` type constructor, define types
1074that may or may not be there. They are similar to ``Maybe`` types of
1075Haskell implicitly adding a new value :mzn:`<>` to the type.
1076
1077
1078|TyInsts|
1079The argument of an option type must be one of the base types
1080:mzn:`bool`, :mzn:`int` or :mzn:`float`.
1081
1082|TySyntax|
1083The option type is written :mzndef:`opt <T>` where :mzndef:`<T>` if one of
1084the three base types, or one of their constrained instances.
1085
1086|TyFiniteType|
1087Yes if the underlying type is finite, otherwise no.
1088
1089|TyVarifiable|
1090Yes.
1091
1092|TyOrdering|
1093:mzn:`<>` is always less than any other value in the type.
1094But beware that overloading of operators like :mzn:`<` is different for
1095option types.
1096
1097|TyInit|
1098An :mzn:`opt` type variable does not need to be initialised at
1099instance-time. An uninitialised :mzn:`opt` type variable is automatically
1100initialised to :mzn:`<>`.
1101
1102|TyCoercions|
1103:mzn:`TI` |coerce| :mzn:`opt UI` if :mzn:`TI` |coerce| :mzn:`UI`..
1104
1105.. _spec-the-annotation-type:
1106
1107The Annotation Type
1108+++++++++++++++++++
1109
1110|TyOverview|
1111The annotation type, :mzn:`ann`, can be used to represent arbitrary term
1112structures. It is augmented by annotation items (:ref:`spec-Annotation-Items`).
1113
1114|TyInsts|
1115:mzn:`ann` is always considered unfixed, because it may contain unfixed
1116elements. It cannot be preceded by :mzn:`var`.
1117
1118|TySyntax|
1119The annotation type is written :mzn:`ann`.
1120
1121|TyFiniteType|
1122No.
1123
1124|TyVarifiable|
1125No.
1126
1127|TyOrdering|
1128N/A. Annotation types do not have an ordering defined on them.
1129
1130|TyInit|
1131An :mzn:`ann` variable must be initialised at instance-time.
1132
1133|TyCoercions|
1134None.
1135
1136
1137.. _spec-constrained-type-insts:
1138
1139Constrained Type-insts
1140~~~~~~~~~~~~~~~~~~~~~~
1141
1142One powerful feature of MiniZinc is *constrained type-insts*. A
1143constrained type-inst is a restricted version of a *base* type-inst,
1144i.e., a type-inst with fewer values in its domain.
1145
1146.. _spec-set-expression-type-insts:
1147
1148Set Expression Type-insts
1149+++++++++++++++++++++++++
1150
1151Three kinds of expressions can be used in type-insts.
1152
1153#. Integer ranges: e.g. :mzn:`1..3`.
1154#. Set literals: e.g. :mzn:`var {1,3,5}`.
1155#. Identifiers: the name of a set parameter (which can be global,
1156 let-local, the argument of a predicate or function, or a generator
1157 value) can serve as a type-inst.
1158
1159In each case the base type is that of the set's elements, and the values
1160within the set serve as the domain. For example, whereas a variable with
1161type-inst :mzn:`var int` can take any integer value, a variable with
1162type-inst :mzn:`var 1..3` can only take the value 1, 2 or 3.
1163
1164All set expression type-insts are finite types. Their domain is equal to
1165the set itself.
1166
1167Float Range Type-insts
1168++++++++++++++++++++++
1169
1170Float ranges can be used as type-insts, e.g. :mzn:`1.0 .. 3.0`. These are
1171treated similarly to integer range type-insts, although :mzn:`1.0 .. 3.0` is
1172not a valid expression whereas :mzn:`1 .. 3` is.
1173
1174Float ranges are not finite types.
1175
1176.. _spec-expressions:
1177
1178Expressions
1179-----------
1180
1181.. _spec-expressions-overview:
1182
1183Expressions Overview
1184~~~~~~~~~~~~~~~~~~~~
1185
1186Expressions represent values. They occur in various kinds of items. They
1187have the following syntax:
1188
1189.. literalinclude:: grammar.mzn
1190 :language: minizincdef
1191 :start-after: % Expressions
1192 :end-before: %
1193
1194Expressions can be composed from sub-expressions combined with operators.
1195All operators (binary and unary) are described in :ref:`spec-Operators`,
1196including the precedences of the binary operators. All unary operators bind
1197more tightly than all binary operators.
1198
1199Expressions can have one or more annotations. Annotations bind
1200more tightly than unary and binary operator applications, but less tightly
1201than access operations and non-operator applications. In some cases this
1202binding is non-intuitive. For example, in the first three of the following
1203lines, the annotation :mzn:`a` binds to the identifier expression
1204:mzn:`x` rather than the operator application. However, the fourth
1205line features a non-operator application (due to the single quotes around
1206the :mzn:`not`) and so the annotation binds to the whole application.
1207
1208.. code-block:: minizinc
1209
1210 not x::a;
1211 not (x)::a;
1212 not(x)::a;
1213 'not'(x)::a;
1214
1215:ref:`spec-Annotations` has more on annotations.
1216
1217Expressions can be contained within parentheses.
1218
1219The array access operations
1220all bind more tightly than unary and binary operators and annotations.
1221They are described in more detail in :ref:`spec-Array-Access-Expressions`.
1222
1223The remaining kinds of expression atoms (from :mzndef:`<ident>` to
1224:mzndef:`<gen-call-expr>`) are described in
1225:ref:`spec-Identifier-Expressions-and-Quoted-Operator-Expressions` to :ref:`spec-Generator-Call-Expressions`.
1226
1227We also distinguish syntactically valid numeric expressions. This allows
1228range types to be parsed correctly.
1229
1230.. literalinclude:: grammar.mzn
1231 :language: minizincdef
1232 :start-after: % Numeric expressions
1233 :end-before: %
1234
1235.. _spec-operators:
1236
1237Operators
1238~~~~~~~~~
1239
1240Operators are functions that are distinguished by their syntax in one or two
1241ways. First, some of them contain non-alphanumeric characters that normal
1242functions do not (e.g. :mzn:`+`). Second, their application is written
1243in a manner different to normal functions.
1244
1245We distinguish between binary operators, which can be applied in an infix
1246manner (e.g. :mzn:`3 + 4`), and unary operators, which can be applied in a
1247prefix manner without parentheses (e.g. :mzn:`not x`). We also
1248distinguish between built-in operators and user-defined operators. The
1249syntax is the following:
1250
1251.. literalinclude:: grammar.mzn
1252 :language: minizincdef
1253 :start-after: % Built-in operators
1254 :end-before: %
1255
1256Again, we syntactically distinguish numeric operators.
1257
1258.. literalinclude:: grammar.mzn
1259 :language: minizincdef
1260 :start-after: % Built-in numeric operators
1261 :end-before: %
1262
1263Some operators can be written using their unicode symbols, which are listed
1264in :numref:`bin-ops-unicode` (recall that MiniZinc input is UTF-8).
1265
1266.. _bin-ops-unicode:
1267
1268.. cssclass:: table-nonfluid table-bordered
1269
1270.. table:: Unicode equivalents of binary operators
1271
1272 ================ ======================= ==============
1273 Operator Unicode symbol UTF-8 code
1274 ================ ======================= ==============
1275 :mzn:`<->` :math:`\leftrightarrow` E2 86 94
1276 :mzn:`->` :math:`\rightarrow` E2 86 92
1277 :mzn:`<-` :math:`\leftarrow` E2 86 90
1278 :mzn:`not` :math:`\lnot` C2 AC
1279 ``\/`` :math:`\lor` E2 88 A8
1280 ``/\`` :math:`\land` E2 88 A7
1281 :mzn:`!=` :math:`\neq` E2 89 A0
1282 :mzn:`<=` :math:`\leq` E2 89 A4
1283 :mzn:`>=` :math:`\geq` E2 89 A5
1284 :mzn:`in` :math:`\in` E2 88 88
1285 :mzn:`subset` :math:`\subseteq` E2 8A 86
1286 :mzn:`superset` :math:`\supseteq` E2 8A 87
1287 :mzn:`union` :math:`\cup` E2 88 AA
1288 :mzn:`intersect` :math:`\cap` E2 88 A9
1289 :mzn:`^-1` :math:`^{-1}` E2 81 BB C2 B9
1290 ================ ======================= ==============
1291
1292The binary operators are listed in :numref:`bin-ops`. A lower precedence
1293number means tighter binding; for example, :mzn:`1+2*3` is parsed as
1294:mzn:`1+(2*3)` because :mzn:`*` binds tighter than :mzn:`+`. Associativity
1295indicates how chains of operators with equal precedences are handled; for
1296example, :mzn:`1+2+3` is parsed as :mzn:`(1+2)+3` because :mzn:`+` is
1297left-associative, :mzn:`a++b++c` is parsed as :mzn:`a++(b++c)` because
1298:mzn:`++` is right-associative, and :mzn:`1<x<2` is a syntax error because
1299:mzn:`<` is non-associative.
1300
1301Note that the last entry in the table, :mzn:`^-1`, is a combination of the binary power operator and the constant -1, which effectively turns it into a unary inverse operator. Other special cases (such as power of 2) are currently not supported yet.
1302
1303.. _bin-ops:
1304
1305.. cssclass:: table-nonfluid table-bordered
1306
1307.. table:: Binary infix operators
1308
1309 =============================== ====== ======
1310 Symbol(s) Assoc. Prec.
1311 =============================== ====== ======
1312 :mzn:`<->` left 1200
1313
1314 :mzn:`->` left 1100
1315 :mzn:`<-` left 1100
1316
1317 ``\/`` left 1000
1318 :mzn:`xor` left 1000
1319
1320 ``/\`` left 900
1321
1322 :mzn:`<` none 800
1323 :mzn:`>` none 800
1324 :mzn:`<=` none 800
1325 :mzn:`>=` none 800
1326 :mzn:`==`,
1327 :mzn:`=` none 800
1328 :mzn:`!=` none 800
1329
1330 :mzn:`in` none 700
1331 :mzn:`subset` none 700
1332 :mzn:`superset` none 700
1333
1334 :mzn:`union` left 600
1335 :mzn:`diff` left 600
1336 :mzn:`symdiff` left 600
1337
1338 :mzn:`..` none 500
1339
1340 :mzn:`+` left 400
1341 :mzn:`-` left 400
1342
1343 :mzn:`*` left 300
1344 :mzn:`div` left 300
1345 :mzn:`mod` left 300
1346 :mzn:`/` left 300
1347 :mzn:`intersect` left 300
1348
1349 :mzn:`^` left 200
1350
1351 :mzn:`++` right 100
1352
1353 ````` :mzndef:`<ident>` ````` left 50
1354 =============================== ====== ======
1355
1356
1357A user-defined binary operator is created by backquoting a normal
1358identifier, for example:
1359
1360.. code-block:: minizinc
1361
1362 A `min2` B
1363
1364This is a static error if the identifier is not the name of a binary
1365function or predicate.
1366
1367The unary operators are: :mzn:`+`, :mzn:`-` and :mzn:`not`.
1368User-defined unary operators are not possible.
1369
1370As :ref:`spec-Identifiers` explains, any built-in operator can be used as
1371a normal function identifier by quoting it, e.g: :mzn:`'+'(3, 4)` is
1372equivalent to :mzn:`3 + 4`.
1373
1374The meaning of each operator is given in :ref:`spec-builtins`.
1375
1376Expression Atoms
1377~~~~~~~~~~~~~~~~
1378
1379.. _spec-Identifier-Expressions-and-Quoted-Operator-Expressions:
1380
1381Identifier Expressions and Quoted Operator Expressions
1382++++++++++++++++++++++++++++++++++++++++++++++++++++++
1383
1384Identifier expressions and quoted operator expressions have the following
1385syntax:
1386
1387.. literalinclude:: grammar.mzn
1388 :language: minizincdef
1389 :start-after: % Identifiers and quoted operators
1390 :end-before: %
1391
1392Examples of identifiers were given in :ref:`spec-Identifiers`. The
1393following are examples of quoted operators:
1394
1395.. code-block:: minizinc
1396
1397 '+'
1398 'union'
1399
1400In quoted operators, whitespace is not permitted between either quote
1401and the operator. :ref:`spec-Operators` lists MiniZinc's built-in operators.
1402
1403Syntactically, any identifier or quoted operator can serve as an expression.
1404However, in a valid model any identifier or quoted operator serving as an
1405expression must be the name of a variable.
1406
1407.. _spec-Anonymous-Decision-Variables:
1408
1409Anonymous Decision Variables
1410++++++++++++++++++++++++++++
1411
1412There is a special identifier, :mzn:`_`, that represents an unfixed,
1413anonymous decision variable. It can take on any type that can be a decision
1414variable. It is particularly useful for initialising decision variables
1415within compound types. For example, in the following array the first and
1416third elements are fixed to 1 and 3 respectively and the second and fourth
1417elements are unfixed:
1418
1419.. code-block:: minizinc
1420
1421 array[1..4] of var int: xs = [1, _, 3, _];
1422
1423Any expression that does not contain :mzn:`_` and does not involve
1424decision variables is fixed.
1425
1426Boolean Literals
1427++++++++++++++++
1428
1429Boolean literals have this syntax:
1430
1431.. literalinclude:: grammar.mzn
1432 :language: minizincdef
1433 :start-after: % Boolean literals
1434 :end-before: %
1435
1436Integer and Float Literals
1437++++++++++++++++++++++++++
1438
1439There are three forms of integer literals - decimal, hexadecimal, and
1440octal - with these respective forms:
1441
1442.. literalinclude:: grammar.mzn
1443 :language: minizincdef
1444 :start-after: % Integer literals
1445 :end-before: %
1446
1447For example: :mzn:`0`, :mzn:`005`, :mzn:`123`, :mzn:`0x1b7`,
1448:mzn:`0o777`; but not :mzn:`-1`.
1449
1450Float literals have the following form:
1451
1452.. literalinclude:: grammar.mzn
1453 :language: minizincdef
1454 :start-after: % Float literals
1455 :end-before: %
1456
1457For example: :mzn:`1.05`, :mzn:`1.3e-5`, :mzn:`1.3+e5`; but not
1458:mzn:`1.`, :mzn:`.5`, :mzn:`1.e5`, :mzn:`.1e5`, :mzn:`-1.0`,
1459:mzn:`-1E05`.
1460A :mzn:`-` symbol preceding an integer or float literal is parsed as a
1461unary minus (regardless of intervening whitespace), not as part of the
1462literal. This is because it is not possible in general to distinguish a
1463:mzn:`-` for a negative integer or float literal from a binary minus
1464when lexing.
1465
1466.. _spec-String-Interpolation-Expressions:
1467
1468String Literals and String Interpolation
1469++++++++++++++++++++++++++++++++++++++++
1470
1471String literals are written as in C:
1472
1473.. literalinclude:: grammar.mzn
1474 :language: minizincdef
1475 :start-after: % String literals
1476 :end-before: %
1477
1478This includes C-style escape sequences, such as :mzn:`\"` for
1479double quotes, :mzn:`\\` for backslash, and
1480:mzn:`\n` for newline.
1481
1482For example: :mzn:`"Hello, world!\n"`.
1483
1484String literals must fit on a single line.
1485
1486Long string literals can be split across multiple lines using string
1487concatenation. For example:
1488
1489.. code-block:: minizinc
1490
1491 string: s = "This is a string literal "
1492 ++ "split across two lines.";
1493
1494A string expression can contain an arbitrary MiniZinc expression, which will
1495be converted to a string similar to the builtin :mzn:`show` function and
1496inserted into the string.
1497
1498For example:
1499
1500.. code-block:: minizinc
1501
1502 var set of 1..10: q;
1503 solve satisfy;
1504 output [show("The value of q is \(q), and it has \(card(q)) elements.")];
1505
1506.. _spec-set-literals:
1507
1508Set Literals
1509++++++++++++
1510
1511Set literals have this syntax:
1512
1513.. literalinclude:: grammar.mzn
1514 :language: minizincdef
1515 :start-after: % Set literals
1516 :end-before: %
1517
1518For example:
1519
1520.. code-block:: minizinc
1521
1522 { 1, 3, 5 }
1523 { }
1524 { 1, 2.0 }
1525
1526The type-insts of all elements in a literal set must be the same, or
1527coercible to the same type-inst (as in the last example above, where the
1528integer :mzn:`1` will be coerced to a :mzn:`float`).
1529
1530
1531.. _spec-set-comprehensions:
1532
1533Set Comprehensions
1534++++++++++++++++++
1535
1536Set comprehensions have this syntax:
1537
1538.. literalinclude:: grammar.mzn
1539 :language: minizincdef
1540 :start-after: % Set comprehensions
1541 :end-before: %
1542
1543For example (with the literal equivalent on the right):
1544
1545.. code-block:: minizinc
1546
1547 { 2*i | i in 1..5 } % { 2, 4, 6, 8, 10 }
1548 { 1 | i in 1..5 } % { 1 } (no duplicates in sets)
1549
1550The expression before the :mzn:`|` is the *head expression*. The
1551expression after the :mzn:`in` is a *generator expression*.
1552Generators can be restricted by a *where-expression*. For example:
1553
1554.. code-block:: minizinc
1555
1556 { i | i in 1..10 where (i mod 2 = 0) } % { 2, 4, 6, 8, 10 }
1557
1558When multiple generators are present, the right-most generator acts as the
1559inner-most one. For example:
1560
1561.. code-block:: minizinc
1562
1563 { 3*i+j | i in 0..2, j in {0, 1} } % { 0, 1, 3, 4, 6, 7 }
1564
1565The scope of local generator variables is given by the following rules:
1566
1567- They are visible within the head expression (before the :mzn:`|`).
1568- They are visible within the where-expression of their own generator.
1569- They are visible within generator expressions and where-expressions in any subsequent generators.
1570
1571The last of these rules means that the following set comprehension is allowed:
1572
1573.. code-block:: minizinc
1574
1575 { i+j | i in 1..3, j in 1..i } % { 1+1, 2+1, 2+2, 3+1, 3+2, 3+3 }
1576
1577Multiple where-expressions are allowed, as in the following example:
1578
1579.. code-block:: minizinc
1580
1581 [f(i, j) | i in A1 where p(i), j in A2 where q(i,j)]
1582
1583
1584A generator expression must be an array or a fixed set.
1585
1586*Rationale: For set comprehensions, set generators would suffice, but for
1587array comprehensions, array generators are required for full expressivity
1588(e.g., to provide control over the order of the elements in the resulting
1589array). Set comprehensions have array generators for consistency with array
1590comprehensions, which makes implementations simpler.*
1591
1592The where-expression (if present) must be Boolean.
1593It can be var, in which case the type of the comprehension is lifted to an optional type.
1594
1595.. _spec-array-literals:
1596
1597Array Literals
1598++++++++++++++
1599
1600Array literals have this syntax:
1601
1602.. literalinclude:: grammar.mzn
1603 :language: minizincdef
1604 :start-after: % Array literals
1605 :end-before: %
1606
1607For example:
1608
1609.. code-block:: minizinc
1610
1611 [1, 2, 3, 4]
1612 []
1613 [1, _]
1614
1615
1616In an array literal all elements must have the same type-inst, or
1617be coercible to the same type-inst (as in the last example above, where the
1618fixed integer :mzn:`1` will be coerced to a :mzn:`var int`).
1619
1620The indices of a array literal are implicitly :mzn:`1..n`, where :mzn:`n` is
1621the length of the literal.
1622
1623.. _spec-2d-array-literals:
1624
16252d Array Literals
1626+++++++++++++++++
1627
1628Simple 2d array literals have this syntax:
1629
1630.. literalinclude:: grammar.mzn
1631 :language: minizincdef
1632 :start-after: % 2D Array literals
1633 :end-before: %
1634
1635For example:
1636
1637.. code-block:: minizinc
1638
1639 [| 1, 2, 3
1640 | 4, 5, 6
1641 | 7, 8, 9 |] % array[1..3, 1..3]
1642 [| x, y, z |] % array[1..1, 1..3]
1643 [| 1 | _ | _ |] % array[1..3, 1..1]
1644
1645In a 2d array literal, every sub-array must have the same length.
1646
1647In a 2d array literal all elements must have the same type-inst, or
1648be coercible to the same type-inst (as in the last example above, where the
1649fixed integer :mzn:`1` will be coerced to a :mzn:`var int`).
1650
1651The indices of a 2d array literal are implicitly :mzn:`(1,1)..(m,n)`,
1652where :mzn:`m` and :mzn:`n` are determined by the shape of the literal.
1653
1654
1655.. _spec-array-comprehensions:
1656
1657Array Comprehensions
1658++++++++++++++++++++
1659
1660Array comprehensions have this syntax:
1661
1662.. literalinclude:: grammar.mzn
1663 :language: minizincdef
1664 :start-after: % Array comprehensions
1665 :end-before: %
1666
1667For example (with the literal equivalents on the right):
1668
1669.. code-block:: minizinc
1670
1671 [2*i | i in 1..5] % [2, 4, 6, 8, 10]
1672
1673Array comprehensions have more flexible type and inst requirements than set
1674comprehensions (see :ref:`spec-Set-Comprehensions`).
1675
1676Array comprehensions are allowed over a variable set with finite type, the
1677result is an array of optional type, with length equal to the
1678cardinality of the upper bound of the variable set.
1679For example:
1680
1681.. code-block:: minizinc
1682
1683 var set of 1..5: x;
1684 array[int] of var opt int: y = [ i * i | i in x ];
1685
1686The length of array will be 5.
1687
1688Array comprehensions are allowed where the where-expression is a :mzn:`var bool`.
1689Again the resulting array is of optional type, and of length
1690equal to that given by the generator expressions.
1691For example:
1692
1693.. code-block:: minizinc
1694
1695 var int x;
1696 array[int] of var opt int: y = [ i | i in 1..10 where i != x ];
1697
1698The length of the array will be 10.
1699
1700The indices of an evaluated simple array comprehension are implicitly
1701:mzn:`1..n`, where :mzn:`n` is the length of the evaluated comprehension.
1702
1703.. _spec-array-access-expressions:
1704
1705Array Access Expressions
1706++++++++++++++++++++++++
1707
1708Array elements are accessed using square brackets after an expression:
1709
1710.. literalinclude:: grammar.mzn
1711 :language: minizincdef
1712 :start-after: % Array access
1713 :end-before: %
1714
1715For example:
1716
1717.. code-block:: minizinc
1718
1719 int: x = a1[1];
1720
1721If all the indices used in an array access are fixed, the type-inst of the
1722result is the same as the element type-inst. However, if any
1723indices are not fixed, the type-inst of the result is the varified element
1724type-inst. For example, if we have:
1725
1726.. code-block:: minizinc
1727
1728 array[1..2] of int: a2 = [1, 2];
1729 var int: i;
1730
1731then the type-inst of :mzn:`a2[i]` is :mzn:`var int`. If the element type-inst
1732is not varifiable, such an access causes a static error.
1733
1734Multi dimensional arrays
1735are accessed using comma separated indices.
1736
1737.. code-block:: minizinc
1738
1739 array[1..3,1..3] of int: a3;
1740 int: y = a3[1, 2];
1741
1742Indices must match the index set type of the array. For example, an array
1743declared with an enum index set can only be accessed using indices from that
1744enum.
1745
1746.. code-block:: minizinc
1747
1748 enum X = {A,B,C};
1749 array[X] of int: a4 = [1,2,3];
1750 int: y = a4[1]; % wrong index type
1751 int: z = a4[B]; % correct
1752
1753Array Slice Expressions
1754+++++++++++++++++++++++
1755
1756Arrays can be *sliced* in order to extract individual rows, columns or blocks. The syntax is that of an array access expression (see above), but where one or more of the expressions inside the square brackets are set-valued.
1757
1758For example, the following extracts row 2 from a two-dimensional array:
1759
1760.. code-block:: minizinc
1761
1762 array[1..n,4..8] of int: x;
1763 array[int] of int: row_2_of_x = x[2,4..8];
1764
1765Note that the resulting array ``row_2_of_x`` will have index set ``4..8``.
1766
1767A short-hand for all indices of a particular dimension is to use just dots:
1768
1769.. code-block:: minizinc
1770
1771 array[1..n,4..8] of int: x;
1772 array[int] of int: row_2_of_x = x[2,..];
1773
1774You can also restrict the index set by giving a sub-set of the original index set as the slice:
1775
1776.. code-block:: minizinc
1777
1778 array[1..n,4..8] of int: x;
1779 array[int] of int: row_2_of_x = x[2,5..6];
1780
1781The resulting array ``row_2_of_x`` will now have length 2 and index set ``5..6``.
1782
1783The dots notation also allows for partial bounds, for example:
1784
1785.. code-block:: minizinc
1786
1787 array[1..n,4..8] of int: x;
1788 array[int] of int: row_2_of_x = x[2,..6];
1789
1790The resulting array will have length 3 and index set ``4..6``. Of course ``6..`` would also be allowed and result in an array with index set ``6..8``.
1791
1792Annotation Literals
1793+++++++++++++++++++
1794
1795Literals of the :mzn:`ann` type have this syntax:
1796
1797.. literalinclude:: grammar.mzn
1798 :language: minizincdef
1799 :start-after: % Annotation literals
1800 :end-before: %
1801
1802For example:
1803
1804.. code-block:: minizinc
1805
1806 foo
1807 cons(1, cons(2, cons(3, nil)))
1808
1809There is no way to inspect or deconstruct annotation literals in a MiniZinc
1810model; they are intended to be inspected only by an implementation, e.g., to
1811direct compilation.
1812
1813If-then-else Expressions
1814++++++++++++++++++++++++
1815
1816MiniZinc provides if-then-else expressions, which provide selection from two
1817alternatives based on a condition. They have this syntax:
1818
1819.. literalinclude:: grammar.mzn
1820 :language: minizincdef
1821 :start-after: % If-then-else expressions
1822 :end-before: %
1823
1824For example:
1825
1826.. code-block:: minizinc
1827
1828 if x <= y then x else y endif
1829 if x < 0 then -1 elseif x > 0 then 1 else 0 endif
1830
1831The presence of the :mzn:`endif` avoids possible ambiguity when an
1832if-then-else expression is part of a larger expression.
1833
1834The type-inst of the :mzn:`if` expression must be :mzn:`par bool` or
1835:mzn:`var bool`.
1836The :mzn:`then` and
1837:mzn:`else` expressions must have the same type-inst, or be coercible to the
1838same type-inst, which is also the type-inst of the whole expression.
1839
1840If the :mzn:`if` expression is :mzn:`var bool` then the type-inst of the
1841:mzn:`then` and :mzn:`else` expressions must be varifiable.
1842
1843If the :mzn:`if` expression is :mzn:`par bool` then
1844evaluation of if-then-else expressions is lazy: the condition is evaluated,
1845and then only one of the :mzn:`then` and :mzn:`else` branches are evaluated,
1846depending on whether the condition succeeded or failed.
1847This is not the case if it is :mzn:`var bool`.
1848
1849
1850.. _spec-let-expressions:
1851
1852Let Expressions
1853+++++++++++++++
1854
1855Let expressions provide a way of introducing local names for one or more
1856expressions and local constraints
1857that can be used within another expression. They are
1858particularly useful in user-defined operations.
1859
1860Let expressions have this syntax:
1861
1862.. literalinclude:: grammar.mzn
1863 :language: minizincdef
1864 :start-after: % Let expressions
1865 :end-before: %
1866
1867For example:
1868
1869.. code-block:: minizinc
1870
1871 let { int: x = 3; int: y = 4; } in x + y;
1872 let { var int: x;
1873 constraint x >= y /\ x >= -y /\ (x = y \/ x = -y); }
1874 in x
1875
1876The scope of a let local variable covers:
1877
1878- The type-inst and initialisation expressions of any subsequent variables
1879 within the let expression (but not the variable's own initialisation
1880 expression).
1881- The expression after the :mzn:`in`, which is parsed as greedily as
1882 possible.
1883
1884A variable can only be declared once in a let expression.
1885
1886Thus in the following examples the first is acceptable but the rest are not:
1887
1888.. code-block:: minizinc
1889
1890 let { int: x = 3; int: y = x; } in x + y; % ok
1891 let { int: y = x; int: x = 3; } in x + y; % x not visible in y's defn.
1892 let { int: x = x; } in x; % x not visible in x's defn.
1893 let { int: x = 3; int: x = 4; } in x; % x declared twice
1894
1895..
1896 The type-inst expressions can include type-inst variables if the let is
1897 within a function or predicate body in which the same type-inst variables
1898 were present in the function or predicate signature.
1899 TODO: type-inst variables are currently not fully supported
1900
1901The initialiser for a let local variable can be omitted only if the variable
1902is a decision variable. For example:
1903
1904.. code-block:: minizinc
1905
1906 let { var int: x; } in ...; % ok
1907 let { int: x; } in ...; % illegal
1908
1909The type-inst of the entire let expression is the type-inst of the expression
1910after the :mzn:`in` keyword.
1911
1912There is a complication involving let expressions in negative contexts. A
1913let expression occurs in a negative context if it occurs in an expression
1914of the form :mzn:`not X`, :mzn:`X <-> Y}` or in the sub-expression
1915:mzn:`X` in :mzn:`X -> Y` or :mzn:`Y <- X`, or in a subexpression
1916:mzn:`bool2int(X)`.
1917
1918If a let expression is used in a negative context, then any let-local
1919decision variables must be defined only in terms of non-local variables and
1920parameters. This is because local variables are implicitly existentially
1921quantified, and if the let expression occurred in a negative context then
1922the local variables would be effectively universally quantified which is not
1923supported by MiniZinc.
1924
1925Constraints in let expressions float to the nearest enclosing Boolean
1926context. For example
1927
1928.. code-block:: minizinc
1929
1930 constraint b -> x + let { var 0..2: y; constraint y != -1;} in y >= 4;
1931
1932is equivalent to
1933
1934.. code-block:: minizinc
1935
1936 var 0..2: y;
1937 constraint b -> (x + y >= 4 /\ y != 1);
1938
1939For backwards compatibility with older versions of MiniZinc, items inside the ``let`` can also be separated by commas instead of semicolons.
1940
1941Call Expressions
1942++++++++++++++++
1943
1944Call expressions are used to call predicates and functions.
1945
1946Call expressions have this syntax:
1947
1948.. literalinclude:: grammar.mzn
1949 :language: minizincdef
1950 :start-after: % Call expressions
1951 :end-before: %
1952
1953For example:
1954
1955.. code-block:: minizinc
1956
1957 x = min(3, 5);
1958
1959The type-insts of the expressions passed as arguments must match the
1960argument types of the called predicate/function. The return type of the
1961predicate/function must also be appropriate for the calling context.
1962
1963Note that a call to a function or predicate with no arguments is
1964syntactically indistinguishable from the use of a variable, and so must be
1965determined during type-inst checking.
1966
1967Evaluation of the arguments in call expressions is strict: all arguments
1968are evaluated before the call itself is evaluated. Note that this includes
1969Boolean operations such as ``/\``, ``\/``, :mzn:`->` and :mzn:`<-`
1970which could be lazy in one argument. The one exception is :mzn:`assert`,
1971which is lazy in its third argument (:ref:`spec-Other-Operations`).
1972
1973*Rationale: Boolean operations are strict because: (a) this minimises
1974exceptional cases; (b) in an expression like* :mzn:`A -> B` *where*
1975:mzn:`A` *is not fixed and* :mzn:`B` *causes an abort, the appropriate
1976behaviour is unclear if laziness is present; and (c) if a user needs
1977laziness, an if-then-else can be used.*
1978
1979The order of argument evaluation is not specified. *Rationale: Because MiniZinc
1980is declarative, there is no obvious need to specify an evaluation order, and
1981leaving it unspecified gives implementors some freedom.*
1982
1983.. _spec-generator-call-expressions:
1984
1985Generator Call Expressions
1986++++++++++++++++++++++++++
1987
1988MiniZinc has special syntax for certain kinds of call expressions which makes
1989models much more readable.
1990
1991Generator call expressions have this syntax:
1992
1993.. literalinclude:: grammar.mzn
1994 :language: minizincdef
1995 :start-after: % Generator call expressions
1996 :end-before: %
1997
1998A generator call expression :mzn:`P(Gs)(E)` is equivalent to the call
1999expression :mzn:`P([E | Gs])`.
2000For example, the expression:
2001
2002.. code-block:: minizinc
2003
2004 forall(i,j in Domain where i<j)
2005 (noattack(i, j, queens[i], queens[j]));
2006
2007(in a model specifying the N-queens problem) is equivalent to:
2008
2009.. code-block:: minizinc
2010
2011 forall( [ noattack(i, j, queens[i], queens[j])
2012 | i,j in Domain where i<j ] );
2013
2014The parentheses around the latter expression are mandatory; this avoids
2015possible confusion when the generator call expression is part of a larger
2016expression.
2017
2018The identifier must be the name of a unary predicate or function that takes
2019an array argument.
2020
2021The generators and where-expression (if present) have the same requirements
2022as those in array comprehensions (:ref:`spec-Array-Comprehensions`).
2023
2024.. _spec-items:
2025
2026Items
2027-----
2028
2029This section describes the top-level program items.
2030
2031.. _spec-include-items:
2032
2033Include Items
2034~~~~~~~~~~~~~
2035
2036Include items allow a model to be split across multiple files. They have
2037this syntax:
2038
2039.. literalinclude:: grammar.mzn
2040 :language: minizincdef
2041 :start-after: % Include items
2042 :end-before: %
2043
2044For example:
2045
2046.. code-block:: minizinc
2047
2048 include "foo.mzn";
2049
2050includes the file ``foo.mzn``.
2051
2052Include items are particularly useful for accessing libraries or breaking up
2053large models into small pieces. They are not, as :ref:`spec-Model-Instance-Files`
2054explains, used for specifying data files.
2055
2056If the given name is not a complete path then the file is searched for in an
2057implementation-defined set of directories. The search directories must be
2058able to be altered with a command line option.
2059
2060.. _spec-declarations:
2061
2062Variable Declaration Items
2063~~~~~~~~~~~~~~~~~~~~~~~~~~
2064
2065Variable declarations have this syntax:
2066
2067.. literalinclude:: grammar.mzn
2068 :language: minizincdef
2069 :start-after: % Variable declaration items
2070 :end-before: %
2071
2072For example:
2073
2074.. code-block:: minizinc
2075
2076 int: A = 10;
2077
2078It is a type-inst error if a variable is declared and/or defined more than
2079once in a model.
2080
2081A variable whose declaration does not include an assignment can be
2082initialised by a separate assignment item (:ref:`spec-Assignments`). For
2083example, the above item can be separated into the following two items:
2084
2085.. code-block:: minizinc
2086
2087 int: A;
2088 ...
2089 A = 10;
2090
2091All variables that contain a parameter component must be defined at
2092instance-time.
2093
2094Variables can have one or more annotations.
2095:ref:`spec-Annotations` has more on annotations.
2096
2097
2098.. _spec-enum_items:
2099
2100Enum Items
2101~~~~~~~~~~
2102
2103Enumerated type items have this syntax:
2104
2105.. literalinclude:: grammar.mzn
2106 :language: minizincdef
2107 :start-after: % Enum items
2108 :end-before: %
2109
2110An example of an enum:
2111
2112.. code-block:: minizinc
2113
2114 enum country = {Australia, Canada, China, England, USA};
2115
2116Each alternative is called an *enum case*. The identifier used to name
2117each case (e.g. :mzn:`Australia`) is
2118called the *enum case name*.
2119
2120Because enum case names all reside in the top-level namespace
2121(:ref:`spec-Namespaces`), case names in different enums must be distinct.
2122
2123Enumerated type items can also be defined in terms of other enumerated types by using an *enumerated type constructor* and the :mzn:`++` operator, as in the following example:
2124
2125.. code-block:: minizinc
2126
2127 enum country_or_none = C(country) ++ {None};
2128
2129The :mzn:`country_or_none` type now contains all of the cases of the :mzn:`country` type, plus the new case :mzn:`None`. The two enumerated types are however completely separate: :mzn:`country` is *not* a subtype of :mzn:`country_or_none`. In order to coerce a value of type :mzn:`country` to type :mzn:`country_or_none`, use the constructor. E.g., :mzn:`C(Canada)` is of type :mzn:`country_or_none`. Similarly, you can use the *inverse constructor* to coerce a value back:
2130
2131.. code-block:: minizinc
2132
2133 country_or_none: c_o_n = C(England);
2134 country: c = C⁻¹(c_o_n);
2135
2136The inverse operator can be written using unicode characters (as in the example) or using ASCII syntax, e.g. :mzn:`C^-1(c_o_n)`.
2137
2138An enum can be declared but not defined, in which case it must be defined
2139elsewhere within the model, or in a data file.
2140For example, a model file could contain this:
2141
2142.. code-block:: minizinc
2143
2144 enum Workers;
2145 enum Shifts;
2146
2147and the data file could contain this:
2148
2149.. code-block:: minizinc
2150
2151 Workers = { welder, driller, stamper };
2152 Shifts = { idle, day, night };
2153
2154Sometimes it is useful to be able to refer to one of the enum case names
2155within the model. This can be achieved by using a variable. The model
2156would read:
2157
2158.. code-block:: minizinc
2159
2160 enum Shifts;
2161 Shifts: idle; % Variable representing the idle constant.
2162
2163and the data file:
2164
2165.. code-block:: minizinc
2166
2167 enum Shifts = { idle_const, day, night };
2168 idle = idle_const; % Assignment to the variable.
2169
2170Although the constant :mzn:`idle_const` cannot be mentioned in the
2171model, the variable :mzn:`idle` can be.
2172
2173All enums must be defined at instance-time.
2174
2175Enum items can be annotated.
2176:ref:`spec-Annotations` has more details on annotations.
2177
2178Each case name can be coerced automatically to the integer corresponding to its index in the type.
2179
2180.. code-block:: minizinc
2181
2182 int: oz = Australia; % oz = 1
2183
2184For each enumerated type :mzn:`T`, the following functions exist:
2185
2186.. code-block:: minizinc
2187
2188 % Return next greater enum value of x in enum type X
2189 function T: enum_next(set of T: X, T: x);
2190 function var T: enum_next(set of T: X, var T: x);
2191
2192 % Return next smaller enum value of x in enum type X
2193 function T: enum_prev(set of T: X, T: x);
2194 function var T: enum_prev(set of T: X, var T: x);
2195
2196 % Convert x to enum type X
2197 function T: to_enum(set of T: X, int: x);
2198 function var T: to_enum(set of T: X, var int: x);
2199
2200.. _spec-assignments:
2201
2202Assignment Items
2203~~~~~~~~~~~~~~~~
2204
2205Assignments have this syntax:
2206
2207.. literalinclude:: grammar.mzn
2208 :language: minizincdef
2209 :start-after: % Assign items
2210 :end-before: %
2211
2212For example:
2213
2214.. code-block:: minizinc
2215
2216 A = 10;
2217
2218.. % \pjs{Add something about automatic coercion of index sets?}
2219
2220.. _spec-constraint-items:
2221
2222Constraint Items
2223~~~~~~~~~~~~~~~~
2224
2225Constraint items form the heart of a model. Any solutions found for a model
2226will satisfy all of its constraints.
2227
2228Constraint items have this syntax:
2229
2230.. literalinclude:: grammar.mzn
2231 :language: minizincdef
2232 :start-after: % Constraint items
2233 :end-before: %
2234
2235For example:
2236
2237.. code-block:: minizinc
2238
2239 constraint a*x < b;
2240
2241The expression in a constraint item must have type-inst :mzn:`par bool` or
2242:mzn:`var bool`; note however that constraints with fixed expressions are
2243not very useful.
2244
2245.. _spec-solve-items:
2246
2247Solve Items
2248~~~~~~~~~~~
2249
2250Every model must have exactly one or no solve item. Solve items have the
2251following syntax:
2252
2253.. literalinclude:: grammar.mzn
2254 :language: minizincdef
2255 :start-after: % Solve item
2256 :end-before: %
2257
2258Example solve items:
2259
2260.. code-block:: minizinc
2261
2262 solve satisfy;
2263 solve maximize a*x + y - 3*z;
2264
2265The solve item determines whether the model represents a constraint
2266satisfaction problem or an optimisation problem. If there is no solve item, the model is assumed to be a satisfaction problem.
2267For optimisation problems, the given expression is the one to be minimized/maximized.
2268
2269The expression in a ``minimize``/``maximize`` solve item can have integer or float type.
2270
2271*Rationale: This is possible because all type-insts have a defined order.*
2272Note that having an expression with a fixed type-inst in a solve item is not
2273very useful as it means that the model requires no optimisation.
2274
2275Solve items can be annotated. :ref:`spec-Annotations` has more details on
2276annotations.
2277
2278.. _spec-output-items:
2279
2280Output Items
2281~~~~~~~~~~~~
2282
2283Output items are used to present the solutions of a model instance.
2284They have the following syntax:
2285
2286.. literalinclude:: grammar.mzn
2287 :language: minizincdef
2288 :start-after: % Output items
2289 :end-before: %
2290
2291For example:
2292
2293.. code-block:: minizinc
2294
2295 output ["The value of x is ", show(x), "!\n"];
2296
2297The expression must have type-inst :mzn:`array[int] of par string`. It can
2298be composed using the built-in operator :mzn:`++` and the built-in functions
2299:mzn:`show`, :mzn:`show_int`, and :mzn:`show_float` (:ref:`spec-builtins`),
2300as well as string interpolations
2301(:ref:`spec-String-Interpolation-Expressions`). The output is the
2302concatenation of the elements of the array. If multiple output items exist,
2303the output is the concatenation of all of their outputs, in the order in
2304which they appear in the model.
2305
2306If no output item is present,
2307the implementation should print all the global variables and their values
2308in a readable format.
2309
2310.. _spec-annotation-items:
2311
2312Annotation Items
2313~~~~~~~~~~~~~~~~
2314
2315Annotation items are used to augment the :mzn:`ann` type. They have the
2316following syntax:
2317
2318.. literalinclude:: grammar.mzn
2319 :language: minizincdef
2320 :start-after: % Annotation items
2321 :end-before: %
2322
2323For example:
2324
2325.. code-block:: minizinc
2326
2327 annotation solver(int: kind);
2328
2329It is a type-inst error if an annotation is declared and/or defined more
2330than once in a model.
2331
2332The use of annotations is described in :ref:`spec-Annotations`.
2333
2334.. _spec-preds-and-fns:
2335
2336User-defined Operations
2337~~~~~~~~~~~~~~~~~~~~~~~
2338
2339..
2340 % XXX: not saying if operations need to be defined. Implementation
2341 % currently requires functions and tests to be defined if used, but
2342 % predicates can be bodyless even if used. Should perhaps require functions
2343 % to be defined even if they're not used (like parameters), and make tests
2344 % like predicates?
2345
2346MiniZinc models can contain user-defined operations. They have this syntax:
2347
2348.. literalinclude:: grammar.mzn
2349 :language: minizincdef
2350 :start-after: % Predicate, test and function items
2351 :end-before: %
2352
2353The type-inst expressions can include type-inst variables in
2354the function and predicate declaration.
2355
2356For example, predicate :mzn:`even` checks that its argument is an even
2357number.
2358
2359.. code-block:: minizinc
2360
2361 predicate even(var int: x) =
2362 x mod 2 = 0;
2363
2364A predicate supported natively by the target solver can be declared as
2365follows:
2366
2367.. code-block:: minizinc
2368
2369 predicate alldifferent(array [int] of var int: xs);
2370
2371Predicate declarations that are natively supported
2372in MiniZinc are restricted to using FlatZinc
2373types (for instance, multi-dimensional and non-1-based arrays are
2374forbidden).
2375.. % \pjs{need to fix this if we allow2d arrays in FlatZinc!}
2376
2377Declarations for user-defined operations can be annotated.
2378:ref:`spec-Annotations` has more details on annotations.
2379
2380.. _spec-basic-properties:
2381
2382Basic Properties
2383++++++++++++++++
2384
2385The term "predicate" is generally used to refer to both test items and
2386predicate items. When the two kinds must be distinguished, the terms
2387"test item" and "predicate item" can be used.
2388
2389The return type-inst of a test item is implicitly :mzn:`par bool`. The
2390return type-inst of a predicate item is implicitly :mzn:`var bool`.
2391
2392Predicates and functions are allowed to be recursive. Termination of
2393a recursive function call depends solely on its fixed arguments, i.e.,
2394recursive functions and predicates cannot be used to define recursively
2395constrained variables.
2396.. % \Rationale{This ensures that the satisfiability of models is decidable.}
2397
2398Predicates and functions introduce their own local names, being those of the
2399formal arguments. The scope of these names covers the predicate/function
2400body. Argument names cannot be repeated within a predicate/function
2401declaration.
2402
2403Ad-hoc polymorphism
2404+++++++++++++++++++
2405
2406MiniZinc supports ad-hoc polymorphism via overloading. Functions
2407and predicates (both built-in and user-defined) can be overloaded. A name
2408can be overloaded as both a function and a predicate.
2409
2410It is a type-inst error if a single version of an overloaded operation with
2411a particular type-inst signature is defined more than once
2412in a model. For example:
2413
2414.. code-block:: minizinc
2415
2416 predicate p(1..5: x);
2417 predicate p(1..5: x) = false; % ok: first definition
2418 predicate p(1..5: x) = true; % error: repeated definition
2419
2420The combination of overloading and coercions can cause problems.
2421Two overloadings of an operation are said to *overlap* if they could match
2422the same arguments. For example, the following overloadings of :mzn:`p`
2423overlap, as they both match the call :mzn:`p(3)`.
2424
2425.. code-block:: minizinc
2426
2427 predicate p(par int: x);
2428 predicate p(var int: x);
2429
2430However, the following two predicates do not overlap because they cannot
2431match the same argument:
2432
2433.. code-block:: minizinc
2434
2435 predicate q(int: x);
2436 predicate q(set of int: x);
2437
2438We avoid two potential overloading problems by placing some restrictions on
2439overlapping overloadings of operations.
2440
2441#. The first problem is ambiguity. Different placement of coercions in
2442 operation arguments may allow different choices for the overloaded function.
2443 For instance, if a MiniZinc function :mzn:`f` is overloaded like this:
2444
2445 .. code-block:: minizinc
2446
2447 function int: f(int: x, float: y) = 0;
2448 function int: f(float: x, int: y) = 1;
2449
2450 then :mzn:`f(3,3)` could be either 0 or 1 depending on
2451 coercion/overloading choices.
2452
2453 To avoid this problem, any overlapping overloadings of an operation must
2454 be semantically equivalent with respect to coercion. For example, the
2455 two overloadings of the predicate :mzn:`p` above must have bodies that are
2456 semantically equivalent with respect to overloading.
2457
2458 Currently, this requirement is not checked and the modeller must satisfy it
2459 manually. In the future, we may require the sharing of bodies among
2460 different versions of overloaded operations, which would provide automatic
2461 satisfaction of this requirement.
2462#. The second problem is that certain combinations of overloadings could
2463 require a MiniZinc implementation to perform combinatorial search in
2464 order to explore different choices of coercions and overloading. For
2465 example, if function :mzn:`g` is overloaded like this:
2466
2467 .. code-block:: minizinc
2468
2469 function float: g(int: t1, float: t2) = t2;
2470 function int : g(float: t1, int: t2) = t1;
2471
2472 then how the overloading of :mzn:`g(3,4)` is resolved depends upon its
2473 context:
2474
2475 .. code-block:: minizinc
2476
2477 float: s = g(3,4);
2478 int: t = g(3,4);
2479
2480 In the definition of :mzn:`s` the first overloaded definition must be used
2481 while in the definition of :mzn:`t` the second must be used.
2482
2483 To avoid this problem, all overlapping overloadings of an operation must be
2484 closed under intersection of their input type-insts. That is, if overloaded
2485 versions have input type-inst :math:`(S_1,....,S_n)` and :math:`(T_1,...,T_n)` then
2486 there must be another overloaded version with input type-inst
2487 :math:`(R_1,...,R_n)` where each :math:`R_i` is the greatest lower bound (*glb*) of
2488 :math:`S_i` and :math:`T_i`.
2489
2490 Also, all overlapping overloadings of an operation must be monotonic. That
2491 is, if there are overloaded versions with input type-insts :math:`(S_1,....,S_n)`
2492 and :math:`(T_1,...,T_n)` and output type-inst :math:`S` and :math:`T`, respectively, then
2493 :math:`S_i \preceq T_i` for all :math:`i`, implies :math:`S \preceq T`. At call sites, the
2494 matching overloading that is lowest on the type-inst lattice is always used.
2495
2496 For :mzn:`g` above, the type-inst intersection (or *glb*) of
2497 :mzn:`(int,float)` and :mzn:`(float,int)` is
2498 :mzn:`(int,int)`. Thus, the overloaded versions are not closed under
2499 intersection and the user needs to provide another overloading for
2500 :mzn:`g` with input type-inst :mzn:`(int,int)`. The natural
2501 definition is:
2502
2503 .. code-block:: minizinc
2504
2505 function int: g(int: t1, int: t2) = t1;
2506
2507 Once :mzn:`g` has been augmented with the third overloading, it satisfies
2508 the monotonicity requirement because the output type-inst of the third
2509 overloading is :mzn:`int` which is less than the output
2510 type-inst of the original overloadings.
2511
2512 Monotonicity and closure under type-inst conjunction ensure that whenever an
2513 overloaded function or predicate is reached during type-inst checking, there
2514 is always a unique and safe "minimal" version to choose, and so the
2515 complexity of type-inst checking remains linear. Thus in our example
2516 :mzn:`g(3,4)` is always resolved by choosing the new overloaded
2517 definition.
2518
2519
2520Local Variables
2521+++++++++++++++
2522
2523Local variables in operation bodies are introduced using let expressions.
2524For example, the predicate :mzn:`have_common_divisor` takes two
2525integer values and checks whether they have a common divisor greater than
2526one:
2527
2528.. code-block:: minizinc
2529
2530 predicate have_common_divisor(int: A, int: B) =
2531 let {
2532 var 2..min(A,B): C;
2533 } in
2534 A mod C = 0 /\
2535 B mod C = 0;
2536
2537However, as :ref:`spec-Let-Expressions` explained, because :mzn:`C` is
2538not defined, this predicate cannot be called in a negative context. The
2539following is a version that could be called in a negative context:
2540
2541.. code-block:: minizinc
2542
2543 predicate have_common_divisor(int: A, int: B) =
2544 exists(C in 2..min(A,B))
2545 (A mod C = 0 /\ B mod C = 0);
2546
2547.. _spec-annotations:
2548
2549Annotations
2550-----------
2551
2552Annotations allow a modeller to specify
2553non-declarative and solver-specific information that is beyond the core
2554language. Annotations do not change the meaning of a model, however, only
2555how it is solved.
2556
2557Annotations can be attached to variables (on their declarations), constraints,
2558expressions, type-inst synonyms, enum items, solve items and on user
2559defined operations.
2560They have the following syntax:
2561
2562.. literalinclude:: grammar.mzn
2563 :language: minizincdef
2564 :start-after: % Annotations
2565
2566For example:
2567
2568.. code-block:: minizinc
2569
2570 int: x::foo;
2571 x = (3 + 4)::bar("a", 9)::baz("b");
2572 solve :: blah(4)
2573 minimize x;
2574
2575The types of the argument expressions must match the argument types of the
2576declared annotation. Like user-defined predicates and functions,
2577annotations can be overloaded.
2578
2579Annotation signatures can contain type-inst variables.
2580
2581The order and nesting of annotations do not matter. For the expression case
2582it can be helpful to view the annotation connector :mzn:`::` as an
2583overloaded operator:
2584
2585.. code-block:: minizinc
2586
2587 ann: '::'(var $T: e, ann: a); % associative
2588 ann: '::'(ann: a, ann: b); % associative + commutative
2589
2590Both operators are associative, the second is commutative. This means that
2591the following expressions are all equivalent:
2592
2593.. code-block:: minizinc
2594
2595 e :: a :: b
2596 e :: b :: a
2597 (e :: a) :: b
2598 (e :: b) :: a
2599 e :: (a :: b)
2600 e :: (b :: a)
2601
2602This property also applies to annotations on solve items and variable
2603declaration items. *Rationale: This property make things simple, as it
2604allows all nested combinations of annotations to be treated as if they are
2605flat, thus avoiding the need to determine what is the meaning of an
2606annotated annotation. It also makes the MiniZinc abstract syntax tree simpler
2607by avoiding the need to represent nesting.*
2608
2609Annotations have to be values of the :mzn:`ann` type or string literals. The
2610latter are used for *naming* constraints and expressions, for example
2611
2612.. code-block:: minizinc
2613
2614 constraint ::"first constraint" alldifferent(x);
2615 constraint ::"second constraint" alldifferent(y);
2616 constraint forall (i in 1..n) (my_constraint(x[i],y[i])::"constraint \(i)");
2617
2618Note that constraint items can *only* be annotated with string literals.
2619
2620*Rationale: Allowing arbitrary annotations on constraint items makes the grammar ambiguous, and seems unnecessary since we can just as well annotate the constraint expression.*
2621
2622.. _spec-partiality:
2623
2624Partiality
2625----------
2626
2627The presence of constrained type-insts in MiniZinc means that
2628various operations are potentially *partial*, i.e., not clearly defined
2629for all possible inputs. For example, what happens if a function expecting
2630a positive argument is passed a negative argument? What happens if a
2631variable is assigned a value that does not satisfy its type-inst constraints?
2632What happens if an array index is out of bounds? This section describes
2633what happens in all these cases.
2634
2635.. % \pjs{This is not what seems to happen in the current MiniZinc!}
2636
2637In general, cases involving fixed values that do not satisfy constraints
2638lead to run-time aborts.
2639*Rationale: Our experience shows that if a fixed value fails a constraint, it
2640is almost certainly due to a programming error. Furthermore, these cases
2641are easy for an implementation to check.*
2642
2643But cases involving unfixed values vary, as we will see.
2644*Rationale: The best thing to do for unfixed values varies from case to case.
2645Also, it is difficult to check constraints on unfixed values, particularly
2646because during search a decision variable might become fixed and then
2647backtracking will cause this value to be reverted, in which case aborting is
2648a bad idea.*
2649
2650Partial Assignments
2651~~~~~~~~~~~~~~~~~~~
2652
2653The first operation involving partiality is assignment. There are four
2654distinct cases for assignments.
2655
2656- A value assigned to a fixed, constrained global variable is checked at
2657 run-time; if the assigned value does not satisfy its constraints, it is
2658 a run-time error. In other words, this:
2659
2660 .. code-block:: minizinc
2661
2662 1..5: x = 3;
2663
2664 is equivalent to this:
2665
2666 .. code-block:: minizinc
2667
2668 int: x = 3;
2669 constraint assert(x in 1..5,
2670 "assignment to global parameter 'x' failed")
2671
2672- A value assigned to an unfixed, constrained global variable makes the
2673 assignment act like a constraint; if the assigned value does not
2674 satisfy the variable's constraints, it causes a run-time model failure.
2675 In other words, this:
2676
2677 .. code-block:: minizinc
2678
2679 var 1..5: x = 3;
2680
2681 is equivalent to this:
2682
2683 .. code-block:: minizinc
2684
2685 var int: x = 3;
2686 constraint x in 1..5;
2687
2688 *Rationale: This behaviour is easy to understand and easy to implement.*
2689
2690- A value assigned to a fixed, constrained let-local variable is checked at
2691 run-time; if the assigned value does not satisfy its constraints, it is
2692 a run-time error. In other words, this:
2693
2694 .. code-block:: minizinc
2695
2696 let { 1..5: x = 3; } in x+1
2697
2698 is equivalent to this:
2699
2700 .. code-block:: minizinc
2701
2702 let { int: x = 3; } in
2703 assert(x in 1..5,
2704 "assignment to let parameter 'x' failed", x+1)
2705
2706- A value assigned to an unfixed, constrained let-local variable makes the
2707 assignment act like a constraint; if the constraint fails at run-time, the
2708 failure "bubbles up" to the nearest enclosing Boolean scope, where it
2709 is interpreted as :mzn:`false`.
2710
2711 *Rationale: This behaviour is consistent with assignments to global
2712 variables.*
2713
2714Note that in cases where a value is partly fixed and partly unfixed, e.g., some
2715arrays, the different elements are checked according to the different cases,
2716and fixed elements are checked before unfixed elements. For example:
2717
2718.. code-block:: minizinc
2719
2720 u = [ let { var 1..5: x = 6} in x, let { par 1..5: y = 6; } in y) ];
2721
2722This causes a run-time abort, because the second, fixed element is checked
2723before the first, unfixed element. This ordering is true for the cases in the
2724following sections as well. *Rationale: This ensures that failures cannot
2725mask aborts, which seems desirable.*
2726
2727Partial Predicate/Function and Annotation Arguments
2728~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
2729
2730The second kind of operation involving partiality is calls and annotations.
2731
2732..
2733 % The behaviour for these operations is simple: constraints on arguments are
2734 % ignored.
2735 %
2736 % \Rationale{This is easy to implement and easy to understand. It is also
2737 % justifiable in the sense that predicate/function/annotation arguments are
2738 % values that are passed in from elsewhere; if those values are to be
2739 % constrained, that could be done earlier. (In comparison, when a variable
2740 % with a constrained type-inst is declared, any assigned value must clearly
2741 % respect that constraint.)}
2742
2743The semantics is similar to assignments: fixed arguments that fail their constraints
2744will cause aborts, and unfixed arguments that fail their constraints will
2745cause failure, which bubbles up to the nearest enclosing Boolean scope.
2746
2747
2748Partial Array Accesses
2749~~~~~~~~~~~~~~~~~~~~~~
2750
2751The third kind of operation involving partiality is array access. There
2752are two distinct cases.
2753
2754- A fixed value used as an array index is checked at run-time; if the
2755 index value is not in the index set of the array, it is a run-time
2756 error.
2757
2758- An unfixed value used as an array index makes the access act like a
2759 constraint; if the access fails at run-time, the failure "bubbles up"
2760 to the nearest enclosing Boolean scope, where it is interpreted as
2761 :mzn:`false`. For example:
2762
2763 .. code-block:: minizinc
2764
2765 array[1..3] of int: a = [1,2,3];
2766 var int: i;
2767 constraint (a[i] + 3) > 10 \/ i = 99;
2768
2769 Here the array access fails, so the failure bubbles up to the
2770 disjunction, and :mzn:`i` is constrained to be 99.
2771 *Rationale: Unlike predicate/function calls, modellers in practice
2772 sometimes do use array accesses that can fail. In such cases, the
2773 "bubbling up" behaviour is a reasonable one.*
2774
2775.. _spec-builtins:
2776
2777Built-in Operations
2778-------------------
2779
2780This appendix lists built-in operators, functions and
2781predicates. They may be implemented as true built-ins, or in libraries that
2782are automatically imported for all models. Many of them are overloaded.
2783
2784Operator names are written within single quotes when used in type
2785signatures, e.g. :mzn:`bool: '\/'(bool, bool)`.
2786
2787We use the syntax :mzn:`TI: f(TI1,...,TIn)` to represent an operation
2788named :mzn:`f` that takes arguments with type-insts :mzn:`TI,...,TIn`
2789and returns a value with type-inst :mzn:`TI`. This is slightly more
2790compact than the usual MiniZinc syntax, in that it omits argument names.
2791
2792
2793Comparison Operations
2794~~~~~~~~~~~~~~~~~~~~~
2795
2796
2797Less than. Other comparisons are similar:
2798greater than (:mzn:`>`),
2799less than or equal (:mzn:`<=`),
2800greater than or equal (:mzn:`>=`),
2801equality (:mzn:`==`, :mzn:`=`),
2802and disequality (:mzn:`!=`).
2803
2804.. % \pjs{Check use of any here!}
2805
2806.. code-block:: minizinc
2807
2808 bool: '<'( $T, $T)
2809 var bool: '<'(var $T, var $T)
2810
2811
2812
2813
2814
2815Arithmetic Operations
2816~~~~~~~~~~~~~~~~~~~~~
2817
2818
2819Addition. Other numeric operations are similar:
2820subtraction (:mzn:`-`), and
2821multiplication (:mzn:`*`).
2822
2823.. code-block:: minizinc
2824
2825 int: '+'( int, int)
2826 var int: '+'(var int, var int)
2827 float: '+'( float, float)
2828 var float: '+'(var float, var float)
2829
2830
2831
2832
2833
2834Unary minus. Unary plus (:mzn:`+`) is similar.
2835
2836.. code-block:: minizinc
2837
2838 int: '-'( int)
2839 var int: '-'(var int)
2840 float: '-'( float)
2841 var float: '-'(var float)
2842
2843
2844
2845
2846
2847Integer and floating-point division and modulo.
2848
2849.. code-block:: minizinc
2850
2851 int: 'div'( int, int)
2852 var int: 'div'(var int, var int)
2853 int: 'mod'( int, int)
2854 var int: 'mod'(var int, var int)
2855 float: '/' ( float, float)
2856 var float: '/' (var float, var float)
2857
2858
2859
2860The result of the modulo operation, if non-zero, always has the same sign as
2861its first operand. The integer division and modulo operations are connected
2862by the following identity:
2863
2864.. code-block:: minizinc
2865
2866 x = (x div y) * y + (x mod y)
2867
2868
2869
2870Some illustrative examples:
2871
2872.. code-block:: minizinc
2873
2874 7 div 4 = 1 7 mod 4 = 3
2875 -7 div 4 = -1 -7 mod 4 = -3
2876 7 div -4 = -1 7 mod -4 = 3
2877 -7 div -4 = 1 -7 mod -4 = -3
2878
2879
2880
2881
2882
2883Sum multiple numbers.
2884Product (:mzn:`product`) is similar. Note that the sum of an empty array
2885is 0, and the product of an empty array is 1.
2886
2887.. code-block:: minizinc
2888
2889 int: sum(array[$T] of int )
2890 var int: sum(array[$T] of var int )
2891 float: sum(array[$T] of float)
2892 var float: sum(array[$T] of var float)
2893
2894
2895
2896
2897
2898Minimum of two values; maximum (:mzn:`max`) is
2899similar.
2900
2901.. code-block:: minizinc
2902
2903 $T: min( $T, $T)
2904 var $T: min(var $T, var $T)
2905
2906
2907
2908
2909
2910Minimum of an array of values; maximum (:mzn:`max`) is similar.
2911Aborts if the array is empty.
2912
2913.. code-block:: minizinc
2914
2915 $U: min(array[$T] of $U)
2916 var $U: min(array[$T] of var $U)
2917
2918
2919
2920
2921
2922Minimum of a fixed set; maximum (:mzn:`max`) is similar.
2923Aborts if the set is empty.
2924
2925.. code-block:: minizinc
2926
2927 $T: min(set of $T)
2928
2929
2930
2931
2932
2933Absolute value of a number.
2934
2935.. code-block:: minizinc
2936
2937 int: abs( int)
2938 var int: abs(var int)
2939 float: abs( float)
2940 var float: abs(var float)
2941
2942
2943
2944
2945
2946Square root of a float. Aborts if argument is negative.
2947
2948.. code-block:: minizinc
2949
2950 float: sqrt( float)
2951 var float: sqrt(var float)
2952
2953
2954
2955
2956
2957Power operator. E.g. :mzn:`pow(2, 5)` gives :mzn:`32`.
2958
2959.. code-block:: minizinc
2960
2961 int: pow(int, int)
2962 float: pow(float, float)
2963
2964
2965..
2966 % We should also have:
2967 % var float: pow(var float, int)
2968
2969
2970Natural exponent.
2971
2972.. code-block:: minizinc
2973
2974 float: exp(float)
2975 var float: exp(var float)
2976
2977
2978
2979
2980
2981Natural logarithm. Logarithm to base 10 (:mzn:`log10`) and logarithm to base
29822 (:mzn:`log2`) are similar.
2983
2984.. code-block:: minizinc
2985
2986 float: ln(float)
2987 var float: ln(var float)
2988
2989
2990
2991
2992
2993General logarithm; the first argument is the base.
2994
2995.. code-block:: minizinc
2996
2997 float: log(float, float)
2998
2999
3000
3001
3002
3003Sine. Cosine (:mzn:`cos`), tangent (:mzn:`tan`), inverse sine
3004(:mzn:`asin`), inverse cosine (:mzn:`acos`), inverse tangent
3005(:mzn:`atan`), hyperbolic sine (:mzn:`sinh`), hyperbolic cosine
3006(:mzn:`cosh`), hyperbolic tangent (:mzn:`tanh`),
3007inverse hyperbolic sine (:mzn:`asinh`), inverse hyperbolic cosine
3008(:mzn:`acosh`) and inverse hyperbolic tangent (:mzn:`atanh`) are similar.
3009
3010.. code-block:: minizinc
3011
3012 float: sin(float)
3013 var float: sin(var float)
3014
3015
3016
3017
3018
3019Logical Operations
3020~~~~~~~~~~~~~~~~~~
3021
3022
3023Conjunction. Other logical operations are similar:
3024disjunction (``\/``)
3025reverse implication (:mzn:`<-`),
3026forward implication (:mzn:`->`),
3027bi-implication (:mzn:`<->`),
3028exclusive disjunction (:mzn:`xor`),
3029logical negation (:mzn:`not`).
3030
3031Note that the implication operators are not written
3032using :mzn:`=>`, :mzn:`<=` and :mzn:`<=>` as is the case in some
3033languages. This allows :mzn:`<=` to instead represent "less than or
3034equal".
3035
3036.. code-block:: minizinc
3037
3038 bool: '/\'( bool, bool)
3039 var bool: '/\'(var bool, var bool)
3040
3041
3042
3043
3044
3045Universal quantification.
3046Existential quantification (:mzn:`exists`) is similar. Note that, when
3047applied to an empty list, :mzn:`forall` returns :mzn:`true`, and
3048:mzn:`exists` returns :mzn:`false`.
3049
3050.. code-block:: minizinc
3051
3052 bool: forall(array[$T] of bool)
3053 var bool: forall(array[$T] of var bool)
3054
3055
3056
3057
3058
3059N-ary exclusive disjunction.
3060N-ary bi-implication (:mzn:`iffall`) is similar, with :mzn:`true` instead
3061of :mzn:`false`.
3062
3063.. code-block:: minizinc
3064
3065 bool: xorall(array[$T] of bool: bs) = foldl('xor', false, bs)
3066 var bool: xorall(array[$T] of var bool: bs) = foldl('xor', false, bs)
3067
3068
3069
3070
3071
3072Set Operations
3073~~~~~~~~~~~~~~
3074
3075
3076Set membership.
3077
3078.. code-block:: minizinc
3079
3080 bool: 'in'( $T, set of $T )
3081 var bool: 'in'(var int, var set of int)
3082
3083
3084
3085
3086
3087Non-strict subset. Non-strict superset (:mzn:`superset`) is similar.
3088
3089.. code-block:: minizinc
3090
3091 bool: 'subset'( set of $T , set of $T )
3092 var bool: 'subset'(var set of int, var set of int)
3093
3094
3095
3096
3097
3098Set union. Other set operations are similar:
3099intersection (:mzn:`intersect`),
3100difference (:mzn:`diff`),
3101symmetric difference (:mzn:`symdiff`).
3102
3103.. code-block:: minizinc
3104
3105 set of $T: 'union'( set of $T, set of $T )
3106 var set of int: 'union'(var set of int, var set of int )
3107
3108
3109
3110
3111
3112Set range. If the first argument is larger than the second
3113(e.g. :mzn:`1..0`), it returns the empty set.
3114
3115.. code-block:: minizinc
3116
3117 set of int: '..'(int, int)
3118
3119
3120
3121
3122
3123Cardinality of a set.
3124
3125.. code-block:: minizinc
3126
3127 int: card( set of $T)
3128 var int: card(var set of int)
3129
3130
3131
3132
3133
3134Union of an array of sets.
3135Intersection of multiple sets (:mzn:`array_intersect`) is similar.
3136
3137.. code-block:: minizinc
3138
3139 set of $U: array_union(array[$T] of set of $U)
3140 var set of int: array_union(array[$T] of var set of int)
3141
3142
3143.. _sec-array-ops:
3144
3145Array Operations
3146~~~~~~~~~~~~~~~~
3147
3148
3149Length of an array.
3150
3151.. code-block:: minizinc
3152
3153 int: length(array[$T] of $U)
3154
3155
3156
3157
3158
3159List concatenation. Returns the list (integer-indexed array) containing
3160all elements of the first argument followed by all elements of the
3161second argument, with elements occurring in the same order as
3162in the arguments. The resulting indices are in the range :mzn:`1..n`,
3163where :mzn:`n` is the sum of the lengths of the arguments.
3164*Rationale: This allows list-like arrays to be concatenated naturally
3165and avoids problems with overlapping indices. The resulting indices
3166are consistent with those of implicitly indexed array literals.*
3167Note that :mzn:`'++'` also performs string concatenation.
3168
3169.. code-block:: minizinc
3170
3171 array[int] of $T: '++'(array[int] of $T, array[int] of $T)
3172
3173Index sets of arrays. If the argument is a literal, returns :mzn:`1..n`
3174where :mzn:`n` is the (sub-)array length. Otherwise, returns the declared
3175or inferred index set. This list is only partial, it extends in the obvious
3176way, for arrays of higher dimensions.
3177
3178.. code-block:: minizinc
3179
3180 set of $T: index_set (array[$T] of $V)
3181 set of $T: index_set_1of2(array[$T, $U] of $V)
3182 set of $U: index_set_2of2(array[$T, $U] of $V)
3183 ...
3184
3185Replace the indices of the array given by the last argument with the
3186Cartesian product of the sets given by the previous arguments. Similar
3187versions exist for arrays up to 6 dimensions.
3188
3189.. code-block:: minizinc
3190
3191 array[$T1] of $V: array1d(set of $T1, array[$U] of $V)
3192 array[$T1,$T2] of $V:
3193 array2d(set of $T1, set of $T2, array[$U] of $V)
3194 array[$T1,$T2,$T3] of $V:
3195 array3d(set of $T1, set of $T2, set of $T3, array[$U] of $V)
3196
3197
3198Coercion Operations
3199~~~~~~~~~~~~~~~~~~~
3200
3201
3202Round a float towards :math:`+\infty`, :math:`-\infty`, and the nearest integer,
3203respectively.
3204
3205.. code-block:: minizinc
3206
3207 int: ceil (float)
3208 int: floor(float)
3209 int: round(float)
3210
3211
3212Explicit casts from one type-inst to another.
3213
3214.. code-block:: minizinc
3215
3216 int: bool2int( bool)
3217 var int: bool2int(var bool)
3218 float: int2float( int)
3219 var float: int2float(var int)
3220 array[int] of $T: set2array(set of $T)
3221
3222
3223String Operations
3224~~~~~~~~~~~~~~~~~
3225
3226
3227To-string conversion. Converts any value to a string for output purposes.
3228The exact form of the resulting string is implementation-dependent.
3229
3230.. code-block:: minizinc
3231
3232 string: show($T)
3233
3234
3235Formatted to-string conversion for integers.
3236Converts the integer given by the second argument into a string right justified
3237by the number of characters given by the first argument, or left justified
3238if that argument is negative.
3239If the second argument is not fixed, the form of the string is
3240implementation-dependent.
3241
3242.. code-block:: minizinc
3243
3244 string: show_int(int, var int);
3245
3246
3247Formatted to-string conversion for floats.
3248Converts the float given by the third argument into a string right
3249justified by the number of characters given by the first argument, or left
3250justified if that argument is negative.
3251The number of digits to appear after the decimal point is given by
3252the second argument.
3253It is a run-time error for the second argument to be negative.
3254If the third argument is not fixed, the form of the string is
3255implementation-dependent.
3256
3257.. code-block:: minizinc
3258
3259 string: show_float(int, int, var float)
3260
3261
3262String concatenation. Note that :mzn:`'++'` also performs array
3263concatenation.
3264
3265.. code-block:: minizinc
3266
3267 string: '++'(string, string)
3268
3269
3270Concatenate an array of strings.
3271Equivalent to folding :mzn:`'++'` over the array, but may be implemented more
3272efficiently.
3273
3274.. code-block:: minizinc
3275
3276 string: concat(array[$T] of string)
3277
3278
3279Concatenate an array of strings, putting a separator between adjacent strings.
3280Returns the the empty string if the array is empty.
3281
3282.. code-block:: minizinc
3283
3284 string: join(string, array[$T] of string)
3285
3286
3287Bound and Domain Operations
3288~~~~~~~~~~~~~~~~~~~~~~~~~~~
3289
3290The bound operations :mzn:`lb` and :mzn:`ub` return fixed, correct lower/upper bounds
3291to the expression.
3292For numeric types, they return a lower/upper bound value,
3293e.g. the lowest/highest value the expression can take.
3294For set types, they return a subset/superset,
3295e.g. the intersection/union of all possible values of the set expression.
3296
3297The bound operations abort on expressions that have no corresponding finite bound.
3298For example, this would be the case for a variable declared without bounds
3299in an implementation that does not assign default bounds.
3300(Set expressions always have a finite lower bound of course,
3301namely :mzn:`{}`, the empty set.)
3302
3303Numeric lower/upper bound:
3304
3305.. code-block:: minizinc
3306
3307 int: lb(var int)
3308 float: lb(var float)
3309 int: ub(var int)
3310 float: ub(var float)
3311
3312
3313Set lower/upper bound:
3314
3315.. code-block:: minizinc
3316
3317 set of int: lb(var set of int)
3318 set of int: ub(var set of int)
3319
3320Versions of the bound operations that operate on arrays are also available,
3321they return a safe lower bound or upper bound for all members of the array
3322- they abort if the array is empty:
3323
3324.. code-block:: minizinc
3325
3326 int: lb_array(array[$T] of var int)
3327 float: lb_array(array[$T] of var float)
3328 set of int: lb_array(array[$T] of var set of int)
3329 int: ub_array(array[$T] of var int)
3330 float: ub_array(array[$T] of var float)
3331 set of int: ub_array(array[$T] of var set of int)
3332
3333
3334
3335
3336
3337Integer domain:
3338
3339.. code-block:: minizinc
3340
3341 set of int: dom(var int)
3342
3343
3344
3345The domain operation :mzn:`dom` returns a fixed superset
3346of the possible values of the expression.
3347
3348
3349Integer array domain, returns a superset of all possible values that may
3350appear in the array - this aborts if the array is empty:
3351
3352.. code-block:: minizinc
3353
3354 set of int: dom_array(array[$T] of var int)
3355
3356Domain size for integers:
3357
3358.. code-block:: minizinc
3359
3360 int: dom_size(var int)
3361
3362The domain size operation :mzn:`dom_size` is equivalent
3363to :mzn:`card(dom(x))`.
3364
3365Note that these operations can produce different results depending on when
3366they are evaluated and what form the argument takes. For example, consider
3367the numeric lower bound operation.
3368
3369- If the argument is a fixed expression, the result is the argument's
3370 value.
3371
3372- If the argument is a decision variable, then the result depends on
3373 the context.
3374
3375 - If the implementation can determine a lower bound for the variable,
3376 the result is that lower bound.
3377 The lower bound may be from the variable's declaration,
3378 or higher than that due to preprocessing,
3379 or lower than that if an implementation-defined lower bound is applied
3380 (e.g. if the variable was declared with no lower bound,
3381 but the implementation imposes a lowest possible bound).
3382
3383 - If the implementation cannot determine a lower bound for the variable,
3384 the operation aborts.
3385
3386- If the argument is any other kind of unfixed expression, the
3387 lower bound depends on the bounds of unfixed subexpressions
3388 and the connecting operators.
3389
3390.. _spec-option-type-operations:
3391
3392Option Type Operations
3393~~~~~~~~~~~~~~~~~~~~~~~
3394
3395The option type value (:math:`\top`) is written
3396
3397.. code-block:: minizinc
3398
3399 opt $T: '<>';
3400
3401
3402One can determine if an option type variable actually occurs or not using
3403:mzn:`occurs` and :mzn:`absent`
3404
3405.. code-block:: minizinc
3406
3407 par bool: occurs(par opt $T);
3408 var bool: occurs(var opt $T);
3409 par bool: absent(par opt $T);
3410 var bool: absent(var opt $T);
3411
3412
3413One can return the non-optional value of an option type variable using the
3414function :mzn:`deopt`
3415
3416.. code-block:: minizinc
3417
3418 par $T: deopt{par opt $T);
3419 var $T: deopt(var opt $T);
3420
3421
3422..
3423 % Note that this is not really a function only a pseudo function placeholder
3424 % used in the translation of option types to non-option types.
3425 % \pjs{Explain better}
3426
3427.. _spec-other-operations:
3428
3429Other Operations
3430~~~~~~~~~~~~~~~~~~~~~~~
3431
3432Check a Boolean expression is true, and abort if not, printing the second
3433argument as the error message. The first one returns the third argument, and
3434is particularly useful for sanity-checking arguments to predicates and
3435functions; importantly, its third argument is lazy, i.e. it is only evaluated
3436if the condition succeeds. The second one returns :mzn:`true` and is useful
3437for global sanity-checks (e.g. of instance data) in constraint items.
3438
3439.. code-block:: minizinc
3440
3441 $T: assert(bool, string, s$T)
3442 par bool: assert(bool, string)
3443
3444
3445Abort evaluation, printing the given string.
3446
3447.. code-block:: minizinc
3448
3449 $T: abort(string)
3450
3451Return true. As a side-effect, an implementation may print the first argument.
3452
3453.. code-block:: minizinc
3454
3455 bool: trace(string)
3456
3457
3458Return the second argument.
3459As a side-effect, an implementation may print the first argument.
3460
3461.. code-block:: minizinc
3462
3463 $T: trace(string, $T)
3464
3465
3466Check if the argument's value is fixed at this point in evaluation. If not,
3467abort; if so, return its value. This is most useful in output items when
3468decision variables should be fixed: it allows them to be used in places
3469where a fixed value is needed, such as if-then-else conditions.
3470
3471.. code-block:: minizinc
3472
3473 $T: fix(var $T)
3474
3475
3476As above, but return :mzn:`false` if the argument's value is not fixed.
3477
3478.. code-block:: minizinc
3479
3480 par bool: is_fixed(var $T)
3481
3482
3483.. _spec-content-types:
3484
3485Content-types
3486-------------
3487
3488The content-type ``application/x-zinc-output`` defines
3489a text output format for Zinc.
3490The format extends the abstract syntax and semantics
3491given in :ref:`spec-Run-time-Outcomes`,
3492and is discussed in detail in :ref:`spec-Output`.
3493
3494The full syntax is as follows:
3495
3496.. literalinclude:: output.mzn
3497 :language: minizincdef
3498
3499The solution text for each solution must be
3500as described in :ref:`spec-Output-Items`.
3501A newline must be appended if the solution text does not end with a newline.
3502
3503.. _spec-json:
3504
3505JSON support
3506------------
3507
3508MiniZinc can support reading input parameters and providing output formatted
3509as JSON objects. A JSON input file needs to have the following structure:
3510
3511- Consist of a single top-level object
3512
3513- The members of the object (the key-value pairs) represent model parameters
3514
3515- Each member key must be a valid MiniZinc identifier (and it supplies the value for the corresponding parameter of the model)
3516
3517- Each member value can be one of the following:
3518
3519 - A string (assigned to a MiniZinc string parameter)
3520
3521 - A number (assigned to a MiniZinc int or float parameter)
3522
3523 - The values ``true`` or ``false`` (assigned to a MiniZinc bool parameter)
3524
3525 - An array of values. Arrays of arrays are supported only if all inner arrays are of the same length, so that they can be mapped to multi-dimensional MiniZinc arrays.
3526
3527 - A set of values encoded as an object with a single member with key ``"set"`` and a list of values (the elements of the set).
3528
3529 - A value of an enumerated type encoded as an object with a single member with key ``"e"`` and a string value (the identifier of the enumerated value).
3530
3531Assume a MiniZinc model declaring the following parameters:
3532
3533.. code-block:: minizinc
3534
3535 int: n;
3536 enum Customers;
3537 array[1..n,Customers] of int: distances;
3538 array[1..n] of set of int: patterns;
3539
3540Here is an example of a JSON parameter file using all of the above features:
3541
3542.. code-block:: json
3543
3544 {
3545 "n" : 2,
3546 "Customers" : [ {"e" : "Customer A"}, {"e" : "Customer B"}, {"e" : "Customer C"} ],
3547 "distances" : [ [1,2,3],
3548 [4,5,6]],
3549 "patterns" : [ {"set" : [1,3,5]}, {"set" : [2,4,6]} ]
3550 }
3551
3552
3553The first parameter declares a simple integer ``n``. The ``Customers`` parameter defines the members of an enumerated type. The
3554``distances`` parameter is a two-dimensional array; note that all inner
3555arrays must be of the same size in order to map to a (rectangular) MiniZinc
3556two-dimensional array. The ``patterns`` parameter is an array of sets of integers.
3557
3558.. _spec-grammar:
3559
3560Full grammar
3561------------
3562
3563Items
3564~~~~~
3565
3566.. literalinclude:: grammar.mzn
3567 :language: minizincdef
3568 :end-before: % Type-inst expressions
3569
3570Type-Inst Expressions
3571~~~~~~~~~~~~~~~~~~~~~
3572
3573.. literalinclude:: grammar.mzn
3574 :language: minizincdef
3575 :start-after: % Type-inst expressions
3576 :end-before: % Expressions
3577
3578Expressions
3579~~~~~~~~~~~
3580
3581.. literalinclude:: grammar.mzn
3582 :language: minizincdef
3583 :start-after: % Expressions
3584 :end-before: % Miscellaneous
3585
3586Miscellaneous Elements
3587~~~~~~~~~~~~~~~~~~~~~~
3588
3589.. literalinclude:: grammar.mzn
3590 :language: minizincdef
3591 :start-after: % Miscellaneous
3592