4.1. Specification of MiniZinc
4.1.1. Introduction
This document defines MiniZinc, a language for modelling constraint satisfaction and optimisation problems.
MiniZinc is a highlevel, typed, mostly firstorder, functional, modelling language. It provides:
mathematical notationlike syntax (automatic coercions, overloading, iteration, sets, arrays);
expressive constraints (finite domain, set, linear arithmetic, integer);
support for different kinds of problems (satisfaction, explicit optimisation);
separation of data from model;
highlevel data structures and data encapsulation (sets, arrays, enumerated types, constrained typeinsts);
extensibility (userdefined functions and predicates);
reliability (type checking, instantiation checking, assertions);
solverindependent modelling;
simple, declarative semantics.
MiniZinc is similar to OPL and moves closer to CLP languages such as ECLiPSe.
This document has the following structure. Notation introduces the syntax notation used throughout the specification. Overview of a Model provides a highlevel overview of MiniZinc models. Syntax Overview covers syntax basics. Highlevel Model Structure covers highlevel structure: items, multifile models, namespaces, and scopes. Types and Typeinsts introduces types and typeinsts. Expressions covers expressions. Items describes the toplevel items in detail. Annotations describes annotations. Partiality describes how partiality is handled in various cases. Builtin Operations describes the language builtins. Full grammar gives the MiniZinc grammar. Contenttypes defines contenttypes used in this specification.
This document also provides some explanation of why certain design decisions were made. Such explanations are marked by the word Rationale and written in italics, and do not constitute part of the specification as such. Rationale: These explanations are present because they are useful to both the designers and the users of MiniZinc.
4.1.2. Notation
The basics of the EBNF used in this specification are as follows.
Nonterminals are written between angle brackets,
<item>
.Terminals are written in double quotes, e.g.
"constraint"
. A double quote terminal is written as a sequence of three double quotes:"""
.Optional items are written in square brackets, e.g.
[ "var" ]
.Sequences of zero or more items are written with parentheses and a star, e.g.
( "," <ident> )*
.Sequences of one or more items are written with parentheses and a plus, e.g.
( <msg> )+
.Nonempty lists are written with an item, a separator/terminator terminal, and three dots. For example, this:
<expr> "," ...
is short for this:
<expr> ( "," <expr> )* [ "," ]
The final terminal is always optional in nonempty lists.
Regular expressions are used in some productions, e.g.
[+]?[09]+
.
MiniZinc’s grammar is presented piecebypiece throughout this document. It is also available as a whole in Full grammar. The output grammar also includes some details of the use of whitespace. The following conventions are used:
A newline character or CRLF sequence is written \n.
4.1.3. Overview of a Model
Conceptually, a MiniZinc problem specification has two parts.
The model: the main part of the problem specification, which describes the structure of a particular class of problems.
The data: the input data for the model, which specifies one particular problem within this class of problems.
The pairing of a model with a particular data set is a model instance (sometimes abbreviated to instance).
The model and data may be separated, or the data may be “hardwired” into the model. Model Instance Files specifies how the model and data can be structured within files in a model instance.
There are two broad classes of problems: satisfaction and optimisation. In satisfaction problems all solutions are considered equally good, whereas in optimisation problems the solutions are ordered according to an objective and the aim is to find a solution whose objective is optimal. Solve Items specifies how the class of problem is chosen.
4.1.3.1. Evaluation Phases
A MiniZinc model instance is evaluated in two distinct phases.
Instancetime: static checking of the model instance.
Runtime: evaluation of the instance (i.e., constraint solving).
The model instance may not compile due to a problem with the model and/or data, detected at instancetime. This could be caused by a syntax error, a typeinst error, the use of an unsupported feature or operation, etc. In this case the outcome of evaluation is a static error; this must be reported prior to runtime. The form of output for static errors is implementationdependent, although such output should be easily recognisable as a static error.
An implementation may produce warnings during all evaluation phases. For example, an implementation may be able to determine that unsatisfiable constraints exist prior to runtime, and the resulting warning given to the user may be more helpful than if the unsatisfiability is detected at runtime.
An implementation must produce a warning if the objective for an optimisation problem is unbounded.
4.1.3.2. Runtime Outcomes
Assuming there are no static errors, the output from the runtime phase has the following abstract form:
<output> ::= <nosolutions> [ <warnings> ] <freetext>
 ( <solution> )* [ <complete> ] [ <warnings> ] <freetext>
If a solution occurs in the output then it must be feasible. For optimisation problems, each solution must be strictly better than any preceding solution.
If there are no solutions in the output, the outcome must indicate that there are no solutions.
If the search is complete the output may state this after the solutions. The absence of the completeness message indicates that the search is incomplete.
Any warnings produced during runtime must be summarised after the statement of completeness. In particular, if there were any warnings at all during runtime then the summary must indicate this fact.
The implementation may produce text in any format after the warnings. For example, it may print a summary of benchmarking statistics or resources used.
4.1.3.3. Output
Implementations must be capable of producing output of content type application/xzincoutput, which is described below and also in Contenttypes. Implementations may also produce output in alternative formats. Any output should conform to the abstract format from the previous section and must have the semantics described there.
Content type application/xzincoutput extends the syntax from the previous section as follows:
<solution> ::= <solutiontext> [ \n ] "" \n
The solution text for each solution must be as described in Output Items. A newline must be appended if the solution text does not end with a newline. Rationale: This allows solutions to be extracted from output without necessarily knowing how the solutions are formatted. Solutions end with a sequence of ten dashes followed by a newline.
<nosolutions> ::= "=====UNSATISFIABLE=====" \n
The completness result is printed on a separate line. Rationale: The strings are designed to clearly indicate the end of the solutions.
<complete> ::= "==========" \n
If the search is complete, a statement corresponding to the outcome is printed. For an outcome of no solutions the statement is that the model instance is unsatisfiable, for an outcome of no more solutions the statement is that the solution set is complete, and for an outcome of no better solutions the statement is that the last solution is optimal. Rationale: These are the logical implications of a search being complete.
<warnings> ::= ( <message> )+
<message> ::= ( <line> )+
If the search is incomplete, one or more messages describing reasons for incompleteness may be printed. Likewise, if any warnings occurred during search they are repeated after the completeness message. Both kinds of message should have lines that start with % so they are recognized as comments by postprocessing. Rationale: This allows individual messages to be easily recognised.
For example, the following may be output for an optimisation problem:
=====UNSATISFIABLE=====
% trentin.fzn:4: warning: model inconsistency detected before search.
Note that, as in this case, an unbounded objective is not regarded as a source of incompleteness.
4.1.4. Syntax Overview
4.1.4.1. Character Set
The input files to MiniZinc must be encoded as UTF8.
MiniZinc is case sensitive. There are no places where uppercase or lowercase letters must be used.
MiniZinc has no layout restrictions, i.e., any single piece of whitespace (containing spaces, tabs and newlines) is equivalent to any other.
4.1.4.3. Identifiers
Identifiers have the following syntax:
<ident> ::= _?[AZaz][AZaz09_]* % excluding keywords
 "'" [^'\xa\xd\x0]+ "'"
my_name_2
MyName2
'An arbitrary identifier'
A number of keywords are reserved and cannot be used as identifiers. The
keywords are:
ann
,
annotation
,
any
,
array
,
bool
,
case
,
constraint
,
diff
,
div
,
else
,
elseif
,
endif
,
enum
,
false
,
float
,
function
,
if
,
in
,
include
,
int
,
intersect
,
let
,
list
,
maximize
,
minimize
,
mod
,
not
,
of
,
op
,
opt
,
output
,
par
,
predicate
,
record
,
satisfy
,
set
,
solve
,
string
,
subset
,
superset
,
symdiff
,
test
,
then
,
true
,
tuple
,
type
,
union
,
var
,
where
,
xor
.
A number of identifiers are used for builtins; see Builtin Operations for details.
4.1.5. Highlevel Model Structure
A MiniZinc model consists of multiple items:
<model> ::= [ <item> ";" ... ]
Items can occur in any order; identifiers need not be declared before they are used. Items have the following toplevel syntax:
<item> ::= <includeitem>
 <vardeclitem>
 <enumitem>
 <typeinstsynitem>
 <assignitem>
 <constraintitem>
 <solveitem>
 <outputitem>
 <predicateitem>
 <testitem>
 <functionitem>
 <annotationitem>
<tiexprandid> ::= <tiexpr> ":" <ident>
Include items provide a way of combining multiple files into a single instance. This allows a model to be split into multiple files (Include Items).
Variable declaration items introduce new global variables and possibly bind them to a value (Variable Declaration Items).
Assignment items bind values to global variables (Assignment Items).
Constraint items describe model constraints (Constraint Items).
Solve items are the “starting point” of a model, and specify exactly what kind of solution is being looked for: plain satisfaction, or the minimization/maximization of an expression. Each model must have exactly one solve item (Solve Items).
Output items are used for nicely presenting the result of a model execution (Output Items).
Predicate items, test items (which are just a special type of predicate) and function items introduce new userdefined predicates and functions which can be called in expressions (Userdefined Operations). Predicates, functions, and builtin operators are described collectively as operations.
Annotation items augment the ann
type, values of which can specify
nondeclarative and/or solverspecific information in a model.
4.1.5.1. Model Instance Files
MiniZinc models can be constructed from multiple files using include items (see Include Items). MiniZinc has no module system as such; all the included files are simply concatenated and processed as a whole, exactly as if they had all been part of a single file. Rationale: We have not found much need for one so far. If bigger models become common and the single global namespace becomes a problem, this should be reconsidered.
Each model may be paired with one or more data files. Data files are more restricted than model files. They may only contain variable assignments (see Assignment Items).
Data files may not include calls to userdefined operations.
Models do not contain the names of data files; doing so would fix the data file used by the model and defeat the purpose of allowing separate data files. Instead, an implementation must allow one or more data files to be combined with a model for evaluation via a mechanism such as the commandline.
When checking a model with data, all global variables with fixed typeinsts must be assigned, unless they are not used (in which case they can be removed from the model without effect).
A data file can only be checked for static errors in conjunction with a model, since the model contains the declarations that include the types of the variables assigned in the data file.
A single data file may be shared between multiple models, so long as the definitions are compatible with all the models.
4.1.5.2. Namespaces
All names declared at the toplevel belong to a single namespace. It includes the following names.
All global variable names.
All function and predicate names, both builtin and userdefined.
All enumerated type names and enum case names.
All annotation names.
Because multifile MiniZinc models are composed via concatenation (Model Instance Files), all files share this toplevel namespace. Therefore a variable x declared in one model file could not be declared with a different type in a different file, for example.
MiniZinc supports overloading of builtin and userdefined operations.
4.1.5.3. Scopes
Within the toplevel namespace, there are several kinds of local scope that introduce local names:
Comprehension expressions (Set Comprehensions).
Let expressions (Let Expressions).
Function and predicate argument lists and bodies (Userdefined Operations).
The listed sections specify these scopes in more detail. In each case, any names declared in the local scope overshadow identical global names.
4.1.6. Types and Typeinsts
MiniZinc provides four scalar builtin types: Booleans, integers, floats, and
strings; enumerated types; two compound builtin types: sets and multidimensional arrays;
and the user extensible annotation type ann
.
Each type has one or more possible instantiations. The instantiation of a variable or value indicates if it is fixed to a known value or not. A pairing of a type and instantiation is called a typeinst.
We begin by discussing some properties that apply to every type. We then introduce instantiations in more detail. We then cover each type individually, giving: an overview of the type and its possible instantiations, the syntax for its typeinsts, whether it is a finite type (and if so, its domain), whether it is varifiable, the ordering and equality operations, whether its variables must be initialised at instancetime, and whether it can be involved in automatic coercions.
4.1.6.1. Properties of Types
The following list introduces some general properties of MiniZinc types.
Currently all types are monotypes. In the future we may allow types which are polymorphic in other types and also the associated constraints.
We distinguish types which are finite types. In MiniZinc, finite types include Booleans, enums, types defined via set expression typeinsts such as range types (see Set Expression Typeinsts), as well as sets and arrays, composed of finite types. Types that are not finite types are unconstrained integers, unconstrained floats, unconstrained strings, and
ann
. Finite types are relevant to sets (specSets
) and array indices (specArrays
). Every finite type has a domain, which is a set value that holds all the possible values represented by the type.Every firstorder type (this excludes
ann
) has a builtin total order and a builtin equality; >, <, ==/=, !=, <= and >= comparison operators can be applied to any pair of values of the same type. Rationale: This facilitates the specification of symmetry breaking and of polymorphic predicates and functions. Note that, as in most languages, using equality on floats or types that contain floats is generally not reliable due to their inexact representation. An implementation may choose to warn about the use of equality with floats or types that contain floats.
4.1.6.2. Instantiations
When a MiniZinc model is evaluated, the value of each variable may initially be unknown. As it runs, each variable’s domain (the set of values it may take) may be reduced, possibly to a single value.
An instantiation (sometimes abbreviated to inst) describes how fixed or unfixed a variable is at instancetime. At the most basic level, the instantiation system distinguishes between two kinds of variables:
Parameters, whose values are fixed at instancetime (usually written just as “fixed”).
Decision variables (often abbreviated to variables), whose values may be completely unfixed at instancetime, but may become fixed at runtime (indeed, the fixing of decision variables is the whole aim of constraint solving).
In MiniZinc decision variables can have the following types: Booleans,
integers, floats, and sets of integers, and enums.
Arrays and ann
can contain decision variables.
4.1.6.3. Typeinsts
Because each variable has both a type and an inst, they are often combined into a single typeinst. Typeinsts are primarily what we deal with when writing models, rather than types.
A variable’s typeinst never changes. This means a decision
variable whose value becomes fixed during model evaluation still has its
original typeinst (e.g. var int
), because that was its
typeinst at instancetime.
Some typeinsts can be automatically coerced to another typeinst. For
example, if a par int
value is used in a context where a
var int
is expected, it is automatically coerced to a
var int
. We write this par int
\(\stackrel{c}{\rightarrow}\) var int
.
Also, any typeinst can be considered coercible to itself.
MiniZinc allows coercions between some types as well.
Some typeinsts can be varified, i.e., made unfixed at the toplevel.
For example, par int
is varified to var int
. We write this
par int
\(\stackrel{v}{\rightarrow}\) var int
.
Typeinsts that are varifiable include the typeinsts of the types that can be decision variables (Booleans, integers, floats, sets, enumerated types). Varification is relevant to typeinst synonyms and array accesses.
4.1.6.4. Typeinst expression overview
This section partly describes how to write typeinsts in MiniZinc models. Further details are given for each type as they are described in the following sections.
A typeinst expression specifies a typeinst. Typeinst expressions may include typeinst constraints. Typeinst expressions appear in variable declarations (Variable Declaration Items) and userdefined operation items (Userdefined Operations).
Typeinst expressions have this syntax:
<tiexpr> ::= <basetiexpr>
 <arraytiexpr>
<basetiexpr> ::= <varpar> <optti> <setti> <basetiexprtail> ["++" <basetiexpr>]
 "any" <tivariableexprtail>
<varpar> ::= "var"  "par"  ε
<optti> ::= "opt"  ε
<setti> ::= "set" "of"  ε
<basetype> ::= "bool"
 "int"
 "float"
 "string"
<basetiexprtail> ::= <ident>
 <basetype>
 <tivariableexprtail>
 <tupletiexprtail>
 <recordtiexprtail>
 "ann"
 "{" <expr> "," ... "}"
 <numexpr> ".." <numexpr>
(The final alternative, for range types, uses the numericspecific
<numexpr>
nonterminal, defined in Expressions Overview,
rather than the <expr>
nonterminal. If this were not the case, the rule
would never match because the .. operator would always be matched
by the first <expr>
.)
This fully covers the typeinst expressions for scalar types. The compound typeinst expression syntax is covered in more detail in Builtin Compound Types and Typeinsts.
The par
and var
keywords (or lack of them) determine the
instantiation. The par
annotation can be omitted; the following
two typeinst expressions are equivalent:
par int
int
Rationale: The use of the explicit var
keyword allows an
implementation to check that all parameters are initialised in the model or
the instance. It also clearly documents which variables are parameters, and
allows more precise typeinst checking.
A typeinst is fixed if it does not contain var
,
with the exception of ann
.
Note that several typeinst expressions that are syntactically expressible
represent illegal typeinsts. For example, although the grammar allows
var
in front of all these base typeinst expression tails, it is a
typeinst error to have var
in the front of a string or array
expression.
4.1.6.5. Builtin Scalar Types and Typeinsts
Booleans
Overview.
Booleans represent truthhood or falsity. Rationale: Boolean values are
not represented by integers.
Booleans can be explicit converted to
integers with the bool2int
function, which makes the user’s intent
clear.
Allowed Insts. Booleans can be fixed or unfixed.
Syntax.
Fixed Booleans are written bool
or par bool
. Unfixed
Booleans are written as var bool
.
Finite?
Yes. The domain of a Boolean is false, true
.
Varifiable?
par bool
\(\stackrel{v}{\rightarrow}\) var bool
, var bool
\(\stackrel{v}{\rightarrow}\) var bool
.
Ordering.
The value false
is considered smaller than true
.
Initialisation. A fixed Boolean variable must be initialised at instancetime; an unfixed Boolean variable need not be.
Coercions.
par bool
\(\stackrel{c}{\rightarrow}\) var bool
.
Also Booleans can be automatically coerced to integers; see Integers.
Integers
Overview. Integers represent integral numbers. Integer representations are implementationdefined. This means that the representable range of integers is implementationdefined. However, an implementation should abort at runtime if an integer operation overflows.
Allowed Insts. Integers can be fixed or unfixed.
Syntax.
Fixed integers are written int
or par int
. Unfixed
integers are written as var int
.
Finite? Not unless constrained by a set expression (see Set Expression Typeinsts).
Varifiable?
par int
\(\stackrel{v}{\rightarrow}\) var int
,
var int
\(\stackrel{v}{\rightarrow}\) var int
.
Ordering. The ordering on integers is the standard one.
Initialisation. A fixed integer variable must be initialised at instancetime; an unfixed integer variable need not be.
Coercions.
par int
\(\stackrel{c}{\rightarrow}\) var int
,
par bool
\(\stackrel{c}{\rightarrow}\) par int
,
par bool
\(\stackrel{c}{\rightarrow}\) var int
,
var bool
\(\stackrel{c}{\rightarrow}\) var int
.
Also, integers can be automatically coerced to floats; see Floats.
Floats
Overview. Floats represent real numbers. Float representations are implementationdefined. This means that the representable range and precision of floats is implementationdefined. However, an implementation should abort at runtime on exceptional float operations (e.g., those that produce NaN, if using IEEE754 floats).
Allowed Insts. Floats can be fixed or unfixed.
Syntax.
Fixed floats are written float
or par float
. Unfixed
floats are written as var float
.
Finite? Not unless constrained by a set expression (see Set Expression Typeinsts).
Varifiable?
par float
\(\stackrel{v}{\rightarrow}\) var float
,
var float
\(\stackrel{v}{\rightarrow}\) var float
.
Ordering. The ordering on floats is the standard one.
Initialisation. A fixed float variable must be initialised at instancetime; an unfixed float variable need not be.
Coercions.
par int
\(\stackrel{c}{\rightarrow}\) par float
,
par int
\(\stackrel{c}{\rightarrow}\) var float
,
var int
\(\stackrel{c}{\rightarrow}\) var float
,
par float
\(\stackrel{c}{\rightarrow}\) var float
.
Strings
Overview. Strings are primitive, i.e., they are not lists of characters.
String expressions are used in assertions, output items and annotations, and string literals are used in include items.
Allowed Insts. Strings must be fixed.
Syntax.
Fixed strings are written string
or par string
.
Finite? Not unless constrained by a set expression (see Set Expression Typeinsts).
Varifiable? No.
Ordering. Strings are ordered lexicographically using the underlying character codes.
Initialisation. A string variable (which can only be fixed) must be initialised at instancetime.
Coercions.
None automatic. However, any nonstring value can be manually converted to
a string using the builtin show
function or using string interpolation
(see String Literals and String Interpolation).
4.1.6.6. Builtin Compound Types and Typeinsts
Sets
Overview. A set is a collection with no duplicates.
Allowed Insts. The typeinst of a set’s elements must be fixed. Rationale: This is because current solvers are not powerful enough to handle sets containing decision variables. Sets may contain any type, and may be fixed or unfixed. If a set is unfixed, its elements must be finite, unless it occurs in one of the following contexts:
the argument of a predicate, function or annotation.
the declaration of a variable or let local variable with an assigned value.
Syntax. A set base typeinst expression is a special case of the base typeinst rule:
<basetiexpr> ::= <varpar> <optti> "set" "of" <basetiexprtail>
Some example set typeinst expressions:
set of int
var set of bool
Finite? Yes, if the set elements are finite types. Otherwise, no.
The domain of a set type that is a finite type is the powerset of the domain
of its element type. For example, the domain of set of 1..2
is
powerset(1..2)
, which is {}, {1}, {1,2}, {2}
.
Varifiable?
par set of TI
\(\stackrel{v}{\rightarrow}\) var set of TI
,
var set of TI
\(\stackrel{v}{\rightarrow}\) var set of TI
.
Ordering.
The predefined ordering on sets is a lexicographic ordering of the
sorted set form, where {1,2}
is in sorted set form, for example,
but {2,1}
is not.
This means, for instance, {} < {1,3} < {2}
.
Initialisation. A fixed set variable must be initialised at instancetime; an unfixed set variable need not be.
Coercions.
par set of TI
\(\stackrel{c}{\rightarrow}\) par set of UI
and
par set of TI
\(\stackrel{c}{\rightarrow}\) var set of UI
and
var set of TI
\(\stackrel{c}{\rightarrow}\) var set of UI
, if
TI
\(\stackrel{c}{\rightarrow}\) UI
.
Arrays
Overview. MiniZinc arrays are maps from fixed integers to values. Values can be of any type. The values can only have base typeinsts. Arraysofarrays are not allowed. Arrays can be multidimensional.
MiniZinc arrays can be declared in two different ways.
Explicitlyindexed arrays have index types in the declaration that are finite types. For example:
array[1..3] of int: a1; array[0..3] of int: a2; array[1..5, 1..10] of var float: a5;
For such arrays, the index type specifies exactly the indices that will be in the array  the array’s index set is the domain of the index type  and if the indices of the value assigned do not match then it is a runtime error.
For example, the following assignments cause runtime errors:
a1 = [4,6,4,3,2]; % too many elements a2 = [3,2,6,5]; % index set mismatch a5 = []; % too few elements
For
a2
above, the index set of the array literal[3,2,6,5]
is (implicitly)1..4
, so it cannot be assigned to an array declared with index set0..3
, even though the length matches. A correct assignment would use thearray1d
function (see Array Operations):a2 = array1d(0..3,[3,2,6,5]); % correct
Implicitlyindexed arrays have index types in the declaration that are not finite types. For example:
array[int,int] of int: a6;
No checking of indices occurs when these variables are assigned.
In MiniZinc all index sets of an array must be contiguous ranges of integers, or enumerated types. The expression used for initialisation of an array must have matching index sets. An array expression with an enum index set can be assigned to an array declared with an integer index set, but not the other way around. The exception are array literals, which can be assigned to arrays declared with enum index sets.
For example:
enum X = {A,B,C};
enum Y = {D,E,F};
array[X] of int: x = array1d(X, [5,6,7]); % correct
array[Y] of int: y = x; % index set mismatch: Y != X
array[int] of int: z = x; % correct: assign X index set to int
array[X] of int: x2 = [10,11,12]; % correct: automatic coercion for array literals
The initialisation of an array can be done in a separate assignment statement, which may be present in the model or a separate data file.
Arrays can be accessed. See Indexed Array Comprehensions for details.
Allowed Insts. An array’s size must be fixed. Its indices must also have fixed typeinsts. Its elements may be fixed or unfixed.
Syntax. An array base typeinst expression tail has this syntax:
<arraytiexpr> ::= "array" [ <tiexpr> "," ... ] "of" <basetiexpr>
 "list" "of" <basetiexpr>
Some example array typeinst expressions:
array[1..10] of int
list of var int
Note that list of <T>
is just syntactic sugar for
array[int] of <T>
. Rationale: Integerindexed arrays of this form
are very common, and so worthy of special support to make things easier for
modellers. Implementing it using syntactic sugar avoids adding an extra
type to the language, which keeps things simple for implementers.
Because arrays must be fixedsize it is a typeinst error to precede an
array typeinst expression with var
.
Finite? Yes, if the index types and element type are all finite types. Otherwise, no.
The domain of an array type that is a finite array is the set of all distinct arrays whose index set equals the domain of the index type and whose elements are of the array element type.
Varifiable? No.
Ordering.
Arrays are ordered lexicographically, taking absence of a value for a given key
to be before any value for that key. For example,
[1, 1]
is less than
[1, 2]
, which is less than [1, 2, 3]
and
array1d(2..4,[0, 0, 0])
is less than [1, 2, 3]
.
Initialisation. An explicitlyindexed array variable must be initialised at instancetime only if its elements must be initialised at instance time. An implicitlyindexed array variable must be initialised at instancetime so that its length and index set is known.
Coercions.
array[TI0] of TI
\(\stackrel{c}{\rightarrow}\) array[UI0] of UI
if
TI0
\(\stackrel{c}{\rightarrow}\) UI0
and TI
\(\stackrel{c}{\rightarrow}\) UI
.
Option Types
Overview.
Option types defined using the opt
type constructor, define types
that may or may not be there. They are similar to Maybe types of
Haskell implicitly adding a new value <>
to the type.
Allowed Insts.
The argument of an option type must be one of the base types
bool
, int
or float
.
Syntax.
The option type is written opt <T>
where <T>
if one of
the three base types, or one of their constrained instances.
Finite? Yes if the underlying type is finite, otherwise no.
Varifiable? Yes.
Ordering.
<>
is always less than any other value in the type.
But beware that overloading of operators like <
is different for
option types.
Initialisation.
An opt
type variable does not need to be initialised at
instancetime. An uninitialised opt
type variable is automatically
initialised to <>
.
Coercions.
TI
\(\stackrel{c}{\rightarrow}\) opt UI
if TI
\(\stackrel{c}{\rightarrow}\) UI
..
Tuple Types
Overview. Tuples are fixedsize, heterogeneous collections. They must contain at least two elements; unary tuples are not allowed.
Allowed Insts. Tuples may contain unfixed elements.
Syntax. A tuple base typeinst expression tail has this syntax:
<tupletiexprtail> ::= "tuple" ( <tiexpr> "," ... )
An example tuple typeinst expression:
tuple(int, var float)
Finite?
Yes, if all its constituent elements are finite types. Otherwise, no. The domain
of a tuple type that is a finite type is the Cartesian product of the domains of
the element types. For example, the domain of tuple(1..2, {3,5})
is
{(1,3), (1,5), (2,3), (2,5)}
.
Varifiable? Yes, if all its constituent elements are varifiable.
Ordering. Tuples are ordered lexicographically.
Initialisation. A tuple variable must be initialised at instancetime if any of its constituent elements must be initialised at instancetime.
Coercions.
tuple(TI1, ..., TIn)
\(\stackrel{c}{\rightarrow}\) tuple(UI1, ..., UIn)
if TI1
\(\stackrel{c}{\rightarrow}\) UI1
, …, TIn
\(\stackrel{c}{\rightarrow}\) UIn
.
Record Types
Overview. Records are fixedsize, heterogeneous collections. They are similar to tuples, but have named fields. Field names in different records can be identical, because each record’s field names belong to a different namespace.
The order in which a record’s field are specified is irrelevant; the following two record typeinsts are equivalent:
record(var int: x, var int: y)
record(var int: y, var int: x)
Allowed Insts. Records may contain unfixed elements.
Syntax. A record base typeinst expression tail has this syntax:
<recordtiexprtail> ::= "record" ( <tiexprandid> "," ... )
An example record typeinst expression:
record(int: x, int: y)
Finite?
Yes, if all its constituent elements are finite types. Otherwise, no. The domain
of a record type that is a finite type is the same as that of a tuple type, but
with the fields included. For example, the domain of record(1..2: x, {3,5}: y)
is {(x: 1,y: 3), (x: 1,y: 5), (x: 2,y: 3), (x: 2,y: 5)}
.
Varifiable? Yes, if all its constituent elements are varifiable.
Ordering. Records are ordered lexicographically according to the values of the fields, where the fields are sorted in alphabetical order.
Initialisation. A record variable must be initialised at instancetime if any of its constituent elements must be initialised at instancetime.
Coercions.
record(TI1: x1, ..., TIn: xn)
\(\stackrel{c}{\rightarrow}\) record(UI1: x1, ..., UIn: xn)
if TI1
\(\stackrel{c}{\rightarrow}\) UI1
, …, TIn
\(\stackrel{c}{\rightarrow}\) UIn
.
The Annotation Type
Overview.
The annotation type, ann
, can be used to represent arbitrary term
structures. It is augmented by annotation items (Annotation Items).
Allowed Insts.
ann
is always considered unfixed, because it may contain unfixed
elements. It cannot be preceded by var
.
Syntax.
The annotation type is written ann
.
Finite? No.
Varifiable? No.
Ordering. N/A. Annotation types do not have an ordering defined on them.
Initialisation.
An ann
variable must be initialised at instancetime.
Coercions. None.
4.1.6.7. Userdefined Types and Typeinsts
Enumerated Types
Overview. Enumerated types (or enums for short) provide a set of named alternatives. Each alternative is identified by its case name. Enumerated types, like in many other languages, can be used in the place of integer types to achieve stricter type checking.
Allowed Insts. Enums can be fixed or unfixed.
Syntax.
Variables of an enumerated type named X are represented by the term
X
or par X
if fixed, and var X
if unfixed.
Finite? Yes.
The domain of an enum is the set containing all of its case names.
Varifiable?
par X
\(\stackrel{v}{\rightarrow}\) var X
,
var X
\(\stackrel{v}{\rightarrow}\) var X
.
Ordering. When two enum values with different case names are compared, the value with the case name that is declared first is considered smaller than the value with the case name that is declared second.
Initialisation. A fixed enum variable must be initialised at instancetime; an unfixed enum variable need not be.
Coercions.
par X
\(\stackrel{c}{\rightarrow}\) par int
,
var X
\(\stackrel{c}{\rightarrow}\) var int
.
Typeinst Synonyms
Overview.
A typeinst synonym is an alternative name for a preexisting typeinst which
can be used interchangeably with the preexisting typeinst. For example, if
MyFixedInt
is a synonym for par int
then MyFixedInt
can be
used anywhere par int
can, and vice versa.
Allowed Insts.
Preceding a typeinst synonym with var
varifies it, unless the typeinst
is not varifiable, in which case it is a typeinst error. Preceding a typeinst
synonym with par
has the reverse effect, and the type is explicitly made
par
.
Syntax. A typeinst synonym named “X” is represented by the term X.
Finite? As for the preexisting typeinst.
Varifiable? Yes, if the preexisting typeinst is varifiable.
Ordering. As for the preexisting typeinst.
Initialisation. As for the preexisting typeinst.
Coercions. As for the preexisting typeinst.
4.1.6.8. Constrained Typeinsts
One powerful feature of MiniZinc is constrained typeinsts. A constrained typeinst is a restricted version of a base typeinst, i.e., a typeinst with fewer values in its domain.
Set Expression Typeinsts
Three kinds of expressions can be used in typeinsts.
Integer ranges: e.g.
1..3
.Set literals: e.g.
var {1,3,5}
.Identifiers: the name of a set parameter (which can be global, letlocal, the argument of a predicate or function, or a generator value) can serve as a typeinst.
In each case the base type is that of the set’s elements, and the values
within the set serve as the domain. For example, whereas a variable with
typeinst var int
can take any integer value, a variable with
typeinst var 1..3
can only take the value 1, 2 or 3.
All set expression typeinsts are finite types. Their domain is equal to the set itself.
Float Range Typeinsts
Float ranges can be used as typeinsts, e.g. 1.0 .. 3.0
. These are
treated similarly to integer range typeinsts, although 1.0 .. 3.0
is
not a valid expression whereas 1 .. 3
is.
Float ranges are not finite types.
4.1.7. Expressions
4.1.7.1. Expressions Overview
Expressions represent values. They occur in various kinds of items. They have the following syntax:
<expr> ::= <expratom> <exprbinoptail>
<expratom> ::= <expratomhead> <expratomtail> <annotations>
<exprbinoptail> ::= [ <binop> <expr> ]
<expratomhead> ::= <builtinunop> <expratom>
 "(" <expr> ")"
 <identorquotedop>
 "_"
 <boolliteral>
 <intliteral>
 <floatliteral>
 <stringliteral>
 <setliteral>
 <setcomp>
 <arrayliteral>
 <arrayliteral2d>
 <indexedarrayliteral>
 <indexedarrayliteral2d>
 <tupleliteral>
 <recordliteral>
 <arraycomp>
 <indexedarraycomp>
 <annliteral>
 <ifthenelseexpr>
 <letexpr>
 <callexpr>
 <gencallexpr>
<expratomtail> ::= ε
 <arrayaccesstail> <expratomtail>
Expressions can be composed from subexpressions combined with operators. All operators (binary and unary) are described in Operators, including the precedences of the binary operators. All unary operators bind more tightly than all binary operators.
Expressions can have one or more annotations. Annotations bind
more tightly than unary and binary operator applications, but less tightly
than access operations and nonoperator applications. In some cases this
binding is nonintuitive. For example, in the first three of the following
lines, the annotation a
binds to the identifier expression
x
rather than the operator application. However, the fourth
line features a nonoperator application (due to the single quotes around
the not
) and so the annotation binds to the whole application.
not x::a;
not (x)::a;
not(x)::a;
'not'(x)::a;
Annotations has more on annotations.
Expressions can be contained within parentheses.
The array access operations all bind more tightly than unary and binary operators and annotations. They are described in more detail in Indexed Array Comprehensions.
The remaining kinds of expression atoms (from <ident>
to
<gencallexpr>
) are described in
Identifier Expressions and Quoted Operator Expressions to Generator Call Expressions.
We also distinguish syntactically valid numeric expressions. This allows range types to be parsed correctly.
<numexpr> ::= <numexpratom> <numexprbinoptail>
<numexpratom> ::= <numexpratomhead> <expratomtail> <annotations>
<numexprbinoptail> ::= [ <numbinop> <numexpr> ]
<numexpratomhead> ::= <builtinnumunop> <numexpratom>
 "(" <numexpr> ")"
 <identorquotedop>
 <intliteral>
 <floatliteral>
 <ifthenelseexpr>
 <letexpr>
 <callexpr>
 <gencallexpr>
4.1.7.2. Operators
Operators are functions that are distinguished by their syntax in one or two
ways. First, some of them contain nonalphanumeric characters that normal
functions do not (e.g. +
). Second, their application is written
in a manner different to normal functions.
We distinguish between binary operators, which can be applied in an infix
manner (e.g. 3 + 4
), and unary operators, which can be applied in a
prefix manner without parentheses (e.g. not x
). We also
distinguish between builtin operators and userdefined operators. The
syntax is the following:
<builtinop> ::= <builtinbinop>  <builtinunop>
<binop> ::= <builtinbinop>  ‘<ident>‘
<builtinbinop> ::= "<>"  ">"  "<"  "\/"  "xor"  "/\"
 "<"  ">"  "<="  ">="  "=="  "="  "!="
 "~="  "~!="
 "in"  "subset"  "superset"  "union"  "diff"  "symdiff"
 ".."  "intersect"  "++"  "default"  <builtinnumbinop>
<builtinunop> ::= "not"  <builtinnumunop>
Again, we syntactically distinguish numeric operators.
<numbinop> ::= <builtinnumbinop>  ‘<ident>‘
<builtinnumbinop> ::= "+"  ""  "*"  "/"  "div"  "mod"  "^"
 "~+"  "~"  "~*"  "~/"  "~div"
<builtinnumunop> ::= "+"  ""
Some operators can be written using their unicode symbols, which are listed in Table 4.1.1 (recall that MiniZinc input is UTF8).
Operator 
Unicode symbol 
UTF8 code 


\(\leftrightarrow\) 
E2 86 94 

\(\rightarrow\) 
E2 86 92 

\(\leftarrow\) 
E2 86 90 

\(\lnot\) 
C2 AC 
\/ 
\(\lor\) 
E2 88 A8 
/\ 
\(\land\) 
E2 88 A7 

\(\neq\) 
E2 89 A0 

\(\leq\) 
E2 89 A4 

\(\geq\) 
E2 89 A5 

\(\in\) 
E2 88 88 

\(\subseteq\) 
E2 8A 86 

\(\supseteq\) 
E2 8A 87 

\(\cup\) 
E2 88 AA 

\(\cap\) 
E2 88 A9 

\(^{1}\) 
E2 81 BB C2 B9 
The binary operators are listed in Table 4.1.2. A lower precedence
number means tighter binding; for example, 1+2*3
is parsed as
1+(2*3)
because *
binds tighter than +
. Associativity
indicates how chains of operators with equal precedences are handled; for
example, 1+2+3
is parsed as (1+2)+3
because +
is
leftassociative, a++b++c
is parsed as a++(b++c)
because
++
is rightassociative, and 1<x<2
is a syntax error because
<
is nonassociative.
Note that the last entry in the table, ^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.
Symbol(s) 
Assoc. 
Prec. 


left 
1200 

left 
1100 

left 
1100 
\/ 
left 
1000 

left 
1000 
/\ 
left 
900 

none 
800 

none 
800 

none 
800 

none 
800 



none 
800 

none 
800 

none 
700 

none 
700 

none 
700 

left 
600 

left 
600 

left 
600 

none 
500 

none 
500 

none 
500 

none 
500 

left 
400 

left 
400 

left 
300 

left 
300 

left 
300 

left 
300 

left 
300 

left 
200 

right 
100 

left 
70 
` 
left 
50 
A userdefined binary operator is created by backquoting a normal identifier, for example:
A `min2` B
This is a static error if the identifier is not the name of a binary function or predicate.
The unary operators are: +
, 
and not
.
Userdefined unary operators are not possible.
As Identifiers explains, any builtin operator can be used as
a normal function identifier by quoting it, e.g: '+'(3, 4)
is
equivalent to 3 + 4
.
The meaning of each operator is given in Builtin Operations.
4.1.7.3. Expression Atoms
Identifier Expressions and Quoted Operator Expressions
Identifier expressions and quoted operator expressions have the following syntax:
<identorquotedop> ::= <ident>
 ’<builtinop>’
Examples of identifiers were given in Identifiers. The following are examples of quoted operators:
'+'
'union'
In quoted operators, whitespace is not permitted between either quote and the operator. Operators lists MiniZinc’s builtin operators.
Syntactically, any identifier or quoted operator can serve as an expression. However, in a valid model any identifier or quoted operator serving as an expression must be the name of a variable.
Anonymous Decision Variables
There is a special identifier, _
, that represents an unfixed,
anonymous decision variable. It can take on any type that can be a decision
variable. It is particularly useful for initialising decision variables
within compound types. For example, in the following array the first and
third elements are fixed to 1 and 3 respectively and the second and fourth
elements are unfixed:
array[1..4] of var int: xs = [1, _, 3, _];
Any expression that does not contain _
and does not involve
decision variables is fixed.
Boolean Literals
Boolean literals have this syntax:
<boolliteral> ::= "false"  "true"
Integer and Float Literals
There are three forms of integer literals  decimal, hexadecimal, and octal  with these respective forms:
<intliteral> ::= [09]+
 0x[09AFaf]+
 0o[07]+
For example: 0
, 005
, 123
, 0x1b7
,
0o777
; but not 1
.
Float literals have the following form:
<floatliteral> ::= [09]+"."[09]+
 [09]+"."[09]+[Ee][+]?[09]+
 [09]+[Ee][+]?[09]+
 0[xX]([09afAF]*"."[09afAF]+[09afAF]+".")([pP][+]?[09]+)
 (0[xX][09afAF]+[pP][+]?[09]+)
For example: 1.05
, 1.3e5
, 1.3+e5
; but not
1.
, .5
, 1.e5
, .1e5
, 1.0
,
1E05
.
A 
symbol preceding an integer or float literal is parsed as a
unary minus (regardless of intervening whitespace), not as part of the
literal. This is because it is not possible in general to distinguish a

for a negative integer or float literal from a binary minus
when lexing.
String Literals and String Interpolation
String literals are written as in C:
<stringcontents> ::= ([^"\n\]  \[07][07?][07]?  \x[09afAF][09afAF]?  \n  \t  \"  \\)*
<stringliteral> ::= """ <stringcontents> """
 """ <stringcontents> "\(" <stringinterpolatetail>
<stringinterpolatetail> ::= <expr> ")"<stringcontents>"""
 <expr> ")"<stringcontents>"\(" <stringinterpolatetail>
This includes the following Cstyle escape sequences:
\"
for double quotes\\
for backslash\n
for newline\t
for tab\x[09afAF][09afAF]?
for an arbitrary 8bit character specified by the given hexadecimal number\x[07][07]?[07]?
for an arbitrary 8bit character specified by the given octal number
For example: "Hello, world!\n"
.
String literals must fit on a single line.
All string literals are represented and interpreted as UTF8 strings.
This means that you can either include UTF8 characters directly in the strings,
or you can use the hexadecimal or octal notation to insert the UTF8 byte sequences,
for example: "\xe4\xbd\xa0\xe5\xa5\xbd means hello"
is a valid string.
Long string literals can be split across multiple lines using string concatenation. For example:
string: s = "This is a string literal "
++ "split across two lines.";
A string expression can contain an arbitrary MiniZinc expression, which will
be converted to a string similar to the builtin show
function and
inserted into the string.
For example:
var set of 1..10: q;
solve satisfy;
output [show("The value of q is \(q), and it has \(card(q)) elements.")];
Set Literals
Set literals have this syntax:
<setliteral> ::= "{" [ <expr> "," ... ] "}"
For example:
{ 1, 3, 5 }
{ }
{ 1, 2.0 }
The typeinsts of all elements in a literal set must be the same, or
coercible to the same typeinst (as in the last example above, where the
integer 1
will be coerced to a float
).
Set Comprehensions
Set comprehensions have this syntax:
<setcomp> ::= "{" <expr> "" <comptail> "}"
<comptail> ::= <generator> [ "where" <expr> ] "," ...
<generator> ::= ( <ident>  "_" ) "," ... "in" <expr>
For example (with the literal equivalent on the right):
{ 2*i  i in 1..5 } % { 2, 4, 6, 8, 10 }
{ 1  i in 1..5 } % { 1 } (no duplicates in sets)
The expression before the 
is the head expression. The
expression after the in
is a generator expression.
Generators can be restricted by a whereexpression. For example:
{ i  i in 1..10 where (i mod 2 = 0) } % { 2, 4, 6, 8, 10 }
When multiple generators are present, the rightmost generator acts as the innermost one. For example:
{ 3*i+j  i in 0..2, j in {0, 1} } % { 0, 1, 3, 4, 6, 7 }
The scope of local generator variables is given by the following rules:
They are visible within the head expression (before the

).They are visible within the whereexpression of their own generator.
They are visible within generator expressions and whereexpressions in any subsequent generators.
The last of these rules means that the following set comprehension is allowed:
{ i+j  i in 1..3, j in 1..i } % { 1+1, 2+1, 2+2, 3+1, 3+2, 3+3 }
Multiple whereexpressions are allowed, as in the following example:
[f(i, j)  i in A1 where p(i), j in A2 where q(i,j)]
A generator expression must be an array or a fixed set.
Rationale: For set comprehensions, set generators would suffice, but for array comprehensions, array generators are required for full expressivity (e.g., to provide control over the order of the elements in the resulting array). Set comprehensions have array generators for consistency with array comprehensions, which makes implementations simpler.
The whereexpression (if present) must be Boolean. It can be var, in which case the type of the comprehension is lifted to an optional type.
Simple Array Literals
Simple array literals have this syntax:
<arrayliteral> ::= "[" [ <expr> "," ... ] "]"
For example:
[1, 2, 3, 4]
[]
[1, _]
In an array literal all elements must have the same typeinst, or
be coercible to the same typeinst (as in the last example above, where the
fixed integer 1
will be coerced to a var int
).
The indices of an array literal are implicitly 1..n
, where n
is
the length of the literal.
Indexed Array Literals
Indexed array literals have this syntax:
<indexedarrayliteral> ::= "[" [ ( <indextuple> ":" <expr> ) "," ... ] "]"
 "[" [ <indextuple> ":" <expr> "," <expr> "," ... ] "]"
<indextuple> ::= <expr>
 "(" [ <expr> "," ... ] ")"
For example:
[ 1: 1, 2: 2, 3: 3, 4: 4, 5: 5]
[ A: 0, B: 3, C: 5]
[ (1,2): 1, (1,3): 2, (2,2): 3, (2,3): 4]
[ 1: 1, 4: 2, 5: 3, 3: 4, 2: 5]
[ 0: A, B, C ]
The expressions before the colons are the indexes (or keys), those after are the values.
The indexes must be of integer or enumerated type.
The index set of the resulting array is, for each dimension, the union of the indexes of that dimension.
For example, the index set of the first and fourth arrays above is 1..5
,
the index set of the second array is {A,B,C}
, and the index sets of the third array are 1..2
and 2..3
.
For onedimensional arrays, it is possible to give only the starting index of the first element, as in the last example above. All following elements are indexed consecutively.
The index sets of indexed array literals must be contiguous and, for multidimensional arrays, “rectangular”. For example, the following literals are not allowed:
% not contiguous, index 2 missing:
[ 1: 1, 3:2, 4:, 3]
% not contiguous, index 2 missing in dimension 2:
[ (1,1): 0, (1,3): 1, (2,1): 0, (2,3): 2]
% not rectangular, second row has fewer entries than first row:
[ (1,1): 0, (1,2): 0, (1,3): 0, (2,1): 1, (2,2): 2]
The indexes need not be specified in order (e.g. the last example above denotes the same array as the first one).
2d Array Literals
Simple 2d array literals have this syntax:
<arrayliteral2d> ::= "[" [ [ <expr> "," ... ] "" ... ] "]"
For example:
[ 1, 2, 3
 4, 5, 6
 7, 8, 9 ] % array[1..3, 1..3]
[ x, y, z ] % array[1..1, 1..3]
[ 1  _  _ ] % array[1..3, 1..1]
In a 2d array literal, every subarray must have the same length.
In a 2d array literal all elements must have the same typeinst, or
be coercible to the same typeinst (as in the last example above, where the
fixed integer 1
will be coerced to a var int
).
The indices of a 2d array literal are implicitly (1,1)..(m,n)
,
where m
and n
are determined by the shape of the literal.
Indexed 2d Array Literals
Indexed 2d array literals have this syntax:
<indexedarrayliteral2d> ::= "[" [ <expr> ":" ... ] [ [ <expr> ":" ] <expr> "," ... ] "]"
For example:
% only column index:
[ A: B: C:
 0, 0, 0
 1, 1, 1
 2, 2, 2 ];
% only row index:
[ A: 0, 0, 0
 B: 1, 1, 1
 C: 2, 2, 2 ];
% row and column index:
[ A: B: C:
 A: 0, 0, 0
 B: 1, 1, 1
 C: 2, 2, 2 ];
The index sets are either 1..n
for n
rows/columns if no index is given, or the union
of the given indexes. As for general indexed array literals, the union of the given indexes must be
a contiguous set.
Simple Array Comprehensions
Simple array comprehensions have this syntax:
<arraycomp> ::= "[" <expr> "" <comptail> "]"
A generator expression (the part following the in
) can be either a
set or an array (multidimensional arrays are iterated over in rowmajor
order).
For example (with the literal equivalents on the right):
[2*i  i in 1..5] % [2, 4, 6, 8, 10]
[2*i  i in [3,5,7] ] % [6, 10, 14]
[i  i in [1,23,4] ] % [1, 2, 3, 4]
A generator variable in an array comprehension can also be the anonymous variable _
.
For instance, the following generates an array of n*n
ones:
[ 1  _, _ in 1..n ]
Array comprehensions have more flexible type and inst requirements than set comprehensions (see Set Comprehensions).
Array comprehensions are allowed over a variable set with finite type, the result is an array of optional type, with length equal to the cardinality of the upper bound of the variable set. For example:
var set of 1..5: x;
array[int] of var opt int: y = [ i * i  i in x ];
The length of array will be 5.
Array comprehensions are allowed where the whereexpression is a var bool
.
Again the resulting array is of optional type, and of length
equal to that given by the generator expressions.
For example:
var int x;
array[int] of var opt int: y = [ i  i in 1..10 where i != x ];
The length of the array will be 10.
The indices of an evaluated simple array comprehension are implicitly
1..n
, where n
is the length of the evaluated comprehension.
Indexed Array Comprehensions
Indexed array comprehensions have this syntax:
<indexedarraycomp> ::= "[" <indextuple> ":" <expr> "" <comptail> "]"
For example:
% This equals [ 3:9, 4:12, 5:15 ]:
[ i: 3*i  i in 3..5 ]
% This generates a 2d array
% [ 1: 2: 3:
%  2: 7, 8, 9
%  3: 10, 11, 12
%  4: 13, 14, 15
% ]:
[ (i,j): i*3+j  i in 2..4, j in 1..3]
The keys for indexed array comprehensions have the same requirements as for indexed array literals (see Indexed Array Literals).
Array Access Expressions
Array elements are accessed using square brackets after an expression:
<arrayaccesstail> ::= "[" <expr> "," ... "]"
For example:
int: x = a1[1];
If all the indices used in an array access are fixed, the typeinst of the result is the same as the element typeinst. However, if any indices are not fixed, the typeinst of the result is the varified element typeinst. For example, if we have:
array[1..2] of int: a2 = [1, 2];
var int: i;
then the typeinst of a2[i]
is var int
. If the element typeinst
is not varifiable, such an access causes a static error.
Multi dimensional arrays are accessed using comma separated indices.
array[1..3,1..3] of int: a3;
int: y = a3[1, 2];
Indices must match the index set type of the array. For example, an array declared with an enum index set can only be accessed using indices from that enum.
enum X = {A,B,C};
array[X] of int: a4 = [1,2,3];
int: y = a4[1]; % wrong index type
int: z = a4[B]; % correct
Array Slice Expressions
Arrays 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 setvalued.
For example, the following extracts row 2 from a twodimensional array:
array[1..n,4..8] of int: x;
array[int] of int: row_2_of_x = x[2,4..8];
Note that the resulting array row_2_of_x will have index set 4..8.
A shorthand for all indices of a particular dimension is to use just dots:
array[1..n,4..8] of int: x;
array[int] of int: row_2_of_x = x[2,..];
You can also restrict the index set by giving a subset of the original index set as the slice:
array[1..n,4..8] of int: x;
array[int] of int: row_2_of_x = x[2,5..6];
The resulting array row_2_of_x will now have length 2 and index set 5..6.
The dots notation also allows for partial bounds, for example:
array[1..n,4..8] of int: x;
array[int] of int: row_2_of_x = x[2,..6];
The 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.
In addition to the ..
operator, you can also use the <..
, ..<
and <..<
operators (Section 4.1.11.4) to exclude the first, last or both elements from the slice. This also works if you leave one or both of the bounds:
enum X = {A, B, C, D};
array[X, 1..3] of var int: x;
% x1 = x[A..C, 2..3]
array[_, _] of var int: x1 = x[A..<, <..];
% x2 = x[B..C, 3..3]
array[_, _] of var int: x2 = x[<..<, 2<..];
Annotation Literals
Literals of the ann
type have this syntax:
<annliteral> ::= <ident> [ "(" <expr> "," ... ")" ]
For example:
foo
cons(1, cons(2, cons(3, nil)))
There is no way to inspect or deconstruct annotation literals in a MiniZinc model; they are intended to be inspected only by an implementation, e.g., to direct compilation.
Ifthenelse Expressions
MiniZinc provides ifthenelse expressions, which provide selection from two alternatives based on a condition. They have this syntax:
<ifthenelseexpr> ::= "if" <expr> "then" <expr> [ "elseif" <expr> "then" <expr> ]* "else" <expr> "endif"
For example:
if x <= y then x else y endif
if x < 0 then 1 elseif x > 0 then 1 else 0 endif
The presence of the endif
avoids possible ambiguity when an
ifthenelse expression is part of a larger expression.
The typeinst of the if
expression must be par bool
or
var bool
.
The then
and
else
expressions must have the same typeinst, or be coercible to the
same typeinst, which is also the typeinst of the whole expression.
If the if
expression is var bool
then the typeinst of the
then
and else
expressions must be varifiable.
If the if
expression is par bool
then
evaluation of ifthenelse expressions is lazy: the condition is evaluated,
and then only one of the then
and else
branches are evaluated,
depending on whether the condition succeeded or failed.
This is not the case if it is var bool
.
Let Expressions
Let expressions provide a way of introducing local names for one or more expressions and local constraints that can be used within another expression. They are particularly useful in userdefined operations.
Let expressions have this syntax:
<letexpr> ::= "let" "{" <letitem> ";" ... "}" "in" <expr>
<letitem> ::= <vardeclitem>
 <constraintitem>
For example:
let { int: x = 3; int: y = 4; } in x + y;
let { var int: x;
constraint x >= y /\ x >= y /\ (x = y \/ x = y); }
in x
The scope of a let local variable covers:
The typeinst and initialisation expressions of any subsequent variables within the let expression (but not the variable’s own initialisation expression).
The expression after the
in
, which is parsed as greedily as possible.
A variable can only be declared once in a let expression.
Thus in the following examples the first is acceptable but the rest are not:
let { int: x = 3; int: y = x; } in x + y; % ok
let { int: y = x; int: x = 3; } in x + y; % x not visible in y's defn.
let { int: x = x; } in x; % x not visible in x's defn.
let { int: x = 3; int: x = 4; } in x; % x declared twice
The initialiser for a let local variable can be omitted only if the variable is a decision variable. For example:
let { var int: x; } in ...; % ok
let { int: x; } in ...; % illegal
For let local variables with initialisers, the typeinst can be ommitted by using
the any
keyword, in which case the typeinst is inferred from the initialiser:
let { any: x = [5,6,7]; } in ...; % x has type array[1..3] of int
The typeinst of the entire let expression is the typeinst of the expression
after the in
keyword.
There is a complication involving let expressions in negative contexts. A
let expression occurs in a negative context if it occurs in an expression
of the form not X
, X <> Y}
or in the subexpression
X
in X > Y
or Y < X
, or in a subexpression
bool2int(X)
.
If a let expression is used in a negative context, then any letlocal decision variables must be defined only in terms of nonlocal variables and parameters. This is because local variables are implicitly existentially quantified, and if the let expression occurred in a negative context then the local variables would be effectively universally quantified which is not supported by MiniZinc.
Constraints in let expressions float to the nearest enclosing Boolean context. For example
constraint b > x + let { var 0..2: y; constraint y != 1;} in y >= 4;
is equivalent to
var 0..2: y;
constraint b > (x + y >= 4 /\ y != 1);
For backwards compatibility with older versions of MiniZinc, items inside the let can also be separated by commas instead of semicolons.
Call Expressions
Call expressions are used to call predicates and functions.
Call expressions have this syntax:
<callexpr> ::= <identorquotedop> [ "(" <expr> "," ... ")" ]
For example:
x = min(3, 5);
The typeinsts of the expressions passed as arguments must match the argument types of the called predicate/function. The return type of the predicate/function must also be appropriate for the calling context.
Note that a call to a function or predicate with no arguments is syntactically indistinguishable from the use of a variable, and so must be determined during typeinst checking.
Evaluation of the arguments in call expressions is strict: all arguments
are evaluated before the call itself is evaluated. Note that this includes
Boolean operations such as /\, \/, >
and <
which could be lazy in one argument. The one exception is assert
,
which is lazy in its third argument (Other Operations).
Rationale: Boolean operations are strict because: (a) this minimises
exceptional cases; (b) in an expression like A > B
where
A
is not fixed and B
causes an abort, the appropriate
behaviour is unclear if laziness is present; and (c) if a user needs
laziness, an ifthenelse can be used.
The order of argument evaluation is not specified. Rationale: Because MiniZinc is declarative, there is no obvious need to specify an evaluation order, and leaving it unspecified gives implementors some freedom.
Generator Call Expressions
MiniZinc has special syntax for certain kinds of call expressions which makes models much more readable.
Generator call expressions have this syntax:
<gencallexpr> ::= <identorquotedop> "(" <comptail> ")" "(" <expr> ")"
A generator call expression P(Gs)(E)
is equivalent to the call
expression P([E  Gs])
.
For example, the expression:
forall(i,j in Domain where i<j)
(noattack(i, j, queens[i], queens[j]));
(in a model specifying the Nqueens problem) is equivalent to:
forall( [ noattack(i, j, queens[i], queens[j])
 i,j in Domain where i<j ] );
The parentheses around the latter expression are mandatory; this avoids possible confusion when the generator call expression is part of a larger expression.
The identifier must be the name of a unary predicate or function that takes an array argument.
The generators and whereexpression (if present) have the same requirements as those in array comprehensions (Simple Array Comprehensions).
4.1.8. Items
This section describes the toplevel program items.
4.1.8.1. Include Items
Include items allow a model to be split across multiple files. They have this syntax:
<includeitem> ::= "include" <stringliteral>
For example:
include "foo.mzn";
includes the file foo.mzn.
Include items are particularly useful for accessing libraries or breaking up large models into small pieces. They are not, as Model Instance Files explains, used for specifying data files.
If the given name is not a complete path then the file is searched for in an implementationdefined set of directories. The search directories must be able to be altered with a command line option.
4.1.8.2. Variable Declaration Items
Variable declarations have this syntax:
<vardeclitem> ::= <tiexprandid> <annotations> [ "=" <expr> ]
 "any" ":" <ident> <annotations> [ "=" <expr> ]
For example:
int: A = 10;
It is a typeinst error if a variable is declared and/or defined more than once in a model.
A variable whose declaration does not include an assignment can be initialised by a separate assignment item (Assignment Items). For example, the above item can be separated into the following two items:
int: A;
...
A = 10;
All variables that contain a parameter component must be defined at instancetime.
Variable declarations with a definition can omit the typeinst by using the any
keyword:
any: x = [1, 2, 3];
any: y = x[2];
The typeinst of these variables is inferred by MiniZinc to be that of the definition.
In the example above, x
would have type array[1..3] of int, and y
would have type int.
Note that variables with typeinst any
can only be defined inplace, not using separate assignment items.
Variables can have one or more annotations. Annotations has more on annotations.
4.1.8.3. Enum Items
Enumerated type items have this syntax:
<enumitem> ::= "enum" <ident> <annotations> [ "=" <enumcaseslist> ]
<enumcaseslist> ::= <enumcases>
 <enumcaseslist> "++" <enumcases>
<enumcases> ::= "{" <ident> "," ... "}"
 "_" "(" <expr> ")"
 <ident> "(" <ident> ")"
 "anon_enum" "(" <expr> ")"
An example of an enum:
enum country = {Australia, Canada, China, England, USA};
Each alternative is called an enum case. The identifier used to name
each case (e.g. Australia
) is
called the enum case name.
Because enum case names all reside in the toplevel namespace (Namespaces), case names in different enums must be distinct.
Instead of defining explicit, named enum cases, it is also possible to define an anonymous enum.
The special enum constructor _
takes an integer set argument. For example,
enum Slot = _(1..n);
defines an enumerated type Slot
with n
cases. An alternative syntax for
anonymous enums is enum Slot = anon_enum(n);
, which defines the same enum as the code above.
Enumerated type items can also be defined in terms of other sets and enumerated types by using an enumerated type constructor and the ++
operator, as in the following example:
enum country_or_none = C(country) ++ {None};
The country_or_none
type now contains all of the cases of the country
type, plus the new case None
. The two enumerated types are however completely separate: country
is not a subtype of country_or_none
. In order to coerce a value of type country
to type country_or_none
, use the constructor. E.g., C(Canada)
is of type country_or_none
. Similarly, you can use the inverse constructor to coerce a value back:
country_or_none: c_o_n = C(England);
country: c = C⁻¹(c_o_n);
The inverse operator can be written using unicode characters (as in the example) or using ASCII syntax, e.g. C^1(c_o_n)
.
The same enum constructor syntax also works with integer sets, for example
enum Node = Left(1..n) ++ Right(1..n);
declares an enum for nodes in a bipartite graph with n
left nodes and n
right nodes.
Enum constructors can be used to map noncontiguous sets to (contiguous) enumerated types. Consider the following example:
enum Person = { Amy, Bert, Celeste, Doug, Emely };
enum Staff = S({Amy, Doug});
enum Customers = S(Person setminus S⁻¹(Staff));
An enum can be declared but not defined, in which case it must be defined elsewhere within the model, or in a data file. For example, a model file could contain this:
enum Workers;
enum Shifts;
and the data file could contain this:
Workers = { welder, driller, stamper };
Shifts = { idle, day, night };
Sometimes it is useful to be able to refer to one of the enum case names within the model. This can be achieved by using a variable. The model would read:
enum Shifts;
Shifts: idle; % Variable representing the idle constant.
and the data file:
enum Shifts = { idle_const, day, night };
idle = idle_const; % Assignment to the variable.
Although the constant idle_const
cannot be mentioned in the
model, the variable idle
can be.
All enums must be defined at instancetime.
Enum items can be annotated. Annotations has more details on annotations.
Each case name can be coerced automatically to the integer corresponding to its index in the type.
int: oz = Australia; % oz = 1
For each enumerated type T
, the following functions exist:
% Return next greater enum value of x in enum type X
function T: enum_next(T: x);
function var T: enum_next(var T: x);
% Return next smaller enum value of x in enum type X
function T: enum_prev(T: x);
function var T: enum_prev(var T: x);
% Return enum base set for value x in enum type x
function set of T: enum_of(T: x);
function set of T: enum_of(var T: x);
function set of T: enum_of(set of T: x);
function set of T: enum_of(var set of T: x);
% Convert x to enum type X
function T: to_enum(set of T: X, int: x);
function var T: to_enum(set of T: X, var int: x);
4.1.8.4. Typeinst Synonym Items
Typeinst synonym items have this syntax:
<typeinstsynitem> ::= "type" <ident> <annotations> "=" <tiexpr>
For example:
type MyInt = int;
type Person = record(string: name, int: height);
type Domain = 1..n;
It is a typeinst error if a typeinst synonym is declared and/or defined more than once in a model. Typeinst synonym items can be annotated. Section (Annotation Items) has more details on annotations. All typeinst synonyms must be defined at modeltime.
4.1.8.5. Assignment Items
Assignments have this syntax:
<assignitem> ::= <ident> "=" <expr>
For example:
A = 10;
4.1.8.6. Constraint Items
Constraint items form the heart of a model. Any solutions found for a model will satisfy all of its constraints.
Constraint items have this syntax:
<constraintitem> ::= "constraint" [ <stringannotation> ] <expr>
For example:
constraint a*x < b;
The expression in a constraint item must have typeinst par bool
or
var bool
; note however that constraints with fixed expressions are
not very useful.
4.1.8.7. Solve Items
Every model must have exactly one or no solve item. Solve items have the following syntax:
<solveitem> ::= "solve" <annotations> "satisfy"
 "solve" <annotations> "minimize" <expr>
 "solve" <annotations> "maximize" <expr>
Example solve items:
solve satisfy;
solve maximize a*x + y  3*z;
The solve item determines whether the model represents a constraint satisfaction problem or an optimisation problem. If there is no solve item, the model is assumed to be a satisfaction problem. For optimisation problems, the given expression is the one to be minimized/maximized.
The expression in a minimize/maximize solve item can have integer or float type.
Rationale: This is possible because all typeinsts have a defined order. Note that having an expression with a fixed typeinst in a solve item is not very useful as it means that the model requires no optimisation.
Solve items can be annotated. Annotations has more details on annotations.
4.1.8.8. Output Items
Output items are used to present the solutions of a model instance. They have the following syntax:
<outputitem> ::= "output" [ <stringannotation> ] <expr>
For example:
output ["The value of x is ", show(x), "!\n"];
The expression must have typeinst array[int] of par string
. It can
be composed using the builtin operator ++
and the builtin functions
show
, show_int
, and show_float
(Builtin Operations),
as well as string interpolations
(String Literals and String Interpolation). The output is the
concatenation of the elements of the array. If multiple output items exist,
the output is the concatenation of all of their outputs, in the order in
which they appear in the model.
If no output item is present, the implementation should print all the global variables and their values in a readable format.
Output items can optionally given a string annotation denoting a section name which the output is associated with. Sections can be turned on or off using the onlysections and notsections command line arguments (The MiniZinc Command Line Tool).
4.1.8.9. Annotation Items
Annotation items are used to augment the ann
type. They have the
following syntax:
<annotationitem> ::= "annotation" <ident> <params>
For example:
annotation solver(int: kind);
It is a typeinst error if an annotation is declared and/or defined more than once in a model.
The use of annotations is described in Annotations.
4.1.8.10. Userdefined Operations
MiniZinc models can contain userdefined operations. They have this syntax:
<predicateitem> ::= "predicate" <operationitemtail>
<testitem> ::= "test" <operationitemtail>
<functionitem> ::= "function" <tiexpr> ":" <operationitemtail>
<operationitemtail> ::= <ident> <params> <annotations> [ "=" <expr> ]
<params> ::= [ ( <tiexprandid> "," ... ) ]
The typeinst expressions can include typeinst variables in the function and predicate declaration.
For example, predicate even
checks that its argument is an even
number.
predicate even(var int: x) =
x mod 2 = 0;
A predicate supported natively by the target solver can be declared as follows:
predicate alldifferent(array [int] of var int: xs);
Predicate declarations that are natively supported in MiniZinc are restricted to using FlatZinc types (for instance, multidimensional and non1based arrays are forbidden).
Declarations for userdefined operations can be annotated. Annotations has more details on annotations.
Basic Properties
The term “predicate” is generally used to refer to both test items and predicate items. When the two kinds must be distinguished, the terms “test item” and “predicate item” can be used.
The return typeinst of a test item is implicitly par bool
. The
return typeinst of a predicate item is implicitly var bool
.
Predicates and functions are allowed to be recursive. Termination of a recursive function call depends solely on its fixed arguments, i.e., recursive functions and predicates cannot be used to define recursively constrained variables.
Predicates and functions introduce their own local names, being those of the formal arguments. The scope of these names covers the predicate/function body. Argument names cannot be repeated within a predicate/function declaration.
Adhoc polymorphism
MiniZinc supports adhoc polymorphism via overloading. Functions and predicates (both builtin and userdefined) can be overloaded. A name can be overloaded as both a function and a predicate.
It is a typeinst error if a single version of an overloaded operation with a particular typeinst signature is defined more than once in a model. For example:
predicate p(1..5: x);
predicate p(1..5: x) = false; % ok: first definition
predicate p(1..5: x) = true; % error: repeated definition
The combination of overloading and coercions can cause problems.
Two overloadings of an operation are said to overlap if they could match
the same arguments. For example, the following overloadings of p
overlap, as they both match the call p(3)
.
predicate p(par int: x);
predicate p(var int: x);
However, the following two predicates do not overlap because they cannot match the same argument:
predicate q(int: x);
predicate q(set of int: x);
We avoid two potential overloading problems by placing some restrictions on overlapping overloadings of operations.
The first problem is ambiguity. Different placement of coercions in operation arguments may allow different choices for the overloaded function. For instance, if a MiniZinc function
f
is overloaded like this:function int: f(int: x, float: y) = 0; function int: f(float: x, int: y) = 1;
then
f(3,3)
could be either 0 or 1 depending on coercion/overloading choices.To avoid this problem, any overlapping overloadings of an operation must be semantically equivalent with respect to coercion. For example, the two overloadings of the predicate
p
above must have bodies that are semantically equivalent with respect to overloading.Currently, this requirement is not checked and the modeller must satisfy it manually. In the future, we may require the sharing of bodies among different versions of overloaded operations, which would provide automatic satisfaction of this requirement.
The second problem is that certain combinations of overloadings could require a MiniZinc implementation to perform combinatorial search in order to explore different choices of coercions and overloading. For example, if function
g
is overloaded like this:function float: g(int: t1, float: t2) = t2; function int : g(float: t1, int: t2) = t1;
then how the overloading of
g(3,4)
is resolved depends upon its context:float: s = g(3,4); int: t = g(3,4);
In the definition of
s
the first overloaded definition must be used while in the definition oft
the second must be used.To avoid this problem, all overlapping overloadings of an operation must be closed under intersection of their input typeinsts. That is, if overloaded versions have input typeinst \((S_1,....,S_n)\) and \((T_1,...,T_n)\) then there must be another overloaded version with input typeinst \((R_1,...,R_n)\) where each \(R_i\) is the greatest lower bound (glb) of \(S_i\) and \(T_i\).
Also, all overlapping overloadings of an operation must be monotonic. That is, if there are overloaded versions with input typeinsts \((S_1,....,S_n)\) and \((T_1,...,T_n)\) and output typeinst \(S\) and \(T\), respectively, then \(S_i \preceq T_i\) for all \(i\), implies \(S \preceq T\). At call sites, the matching overloading that is lowest on the typeinst lattice is always used.
For
g
above, the typeinst intersection (or glb) of(int,float)
and(float,int)
is(int,int)
. Thus, the overloaded versions are not closed under intersection and the user needs to provide another overloading forg
with input typeinst(int,int)
. The natural definition is:function int: g(int: t1, int: t2) = t1;
Once
g
has been augmented with the third overloading, it satisfies the monotonicity requirement because the output typeinst of the third overloading isint
which is less than the output typeinst of the original overloadings.Monotonicity and closure under typeinst conjunction ensure that whenever an overloaded function or predicate is reached during typeinst checking, there is always a unique and safe “minimal” version to choose, and so the complexity of typeinst checking remains linear. Thus in our example
g(3,4)
is always resolved by choosing the new overloaded definition.
Local Variables
Local variables in operation bodies are introduced using let expressions.
For example, the predicate have_common_divisor
takes two
integer values and checks whether they have a common divisor greater than
one:
predicate have_common_divisor(int: A, int: B) =
let {
var 2..min(A,B): C;
} in
A mod C = 0 /\
B mod C = 0;
However, as Let Expressions explained, because C
is
not defined, this predicate cannot be called in a negative context. The
following is a version that could be called in a negative context:
predicate have_common_divisor(int: A, int: B) =
exists(C in 2..min(A,B))
(A mod C = 0 /\ B mod C = 0);
4.1.9. Annotations
Annotations allow a modeller to specify nondeclarative and solverspecific information that is beyond the core language. Annotations do not change the meaning of a model, however, only how it is solved.
Annotations can be attached to variables (on their declarations), constraints, expressions, typeinst synonyms, enum items, solve items and on user defined operations. They have the following syntax:
<annotations> ::= [ "::" <annotation> ]*
<annotation> ::= <expratomhead> <expratomtail>
<stringannotation> ::= "::" <stringliteral>
For example:
int: x::foo;
x = (3 + 4)::bar("a", 9)::baz("b");
solve :: blah(4)
minimize x;
The types of the argument expressions must match the argument types of the declared annotation. Like userdefined predicates and functions, annotations can be overloaded.
Annotation signatures can contain typeinst variables.
The order and nesting of annotations do not matter. For the expression case
it can be helpful to view the annotation connector ::
as an
overloaded operator:
ann: '::'(var $T: e, ann: a); % associative
ann: '::'(ann: a, ann: b); % associative + commutative
Both operators are associative, the second is commutative. This means that the following expressions are all equivalent:
e :: a :: b
e :: b :: a
(e :: a) :: b
(e :: b) :: a
e :: (a :: b)
e :: (b :: a)
This property also applies to annotations on solve items and variable declaration items. Rationale: This property make things simple, as it allows all nested combinations of annotations to be treated as if they are flat, thus avoiding the need to determine what is the meaning of an annotated annotation. It also makes the MiniZinc abstract syntax tree simpler by avoiding the need to represent nesting.
Annotations have to be values of the ann
type or string literals. The
latter are used for naming constraints and expressions, for example
constraint ::"first constraint" alldifferent(x);
constraint ::"second constraint" alldifferent(y);
constraint forall (i in 1..n) (my_constraint(x[i],y[i])::"constraint \(i)");
Note that constraint items can only be annotated with string literals.
Rationale: Allowing arbitrary annotations on constraint items makes the grammar ambiguous, and seems unnecessary since we can just as well annotate the constraint expression.
4.1.10. Partiality
The presence of constrained typeinsts in MiniZinc means that various operations are potentially partial, i.e., not clearly defined for all possible inputs. For example, what happens if a function expecting a positive argument is passed a negative argument? What happens if a variable is assigned a value that does not satisfy its typeinst constraints? What happens if an array index is out of bounds? This section describes what happens in all these cases.
In general, cases involving fixed values that do not satisfy constraints lead to runtime aborts. Rationale: Our experience shows that if a fixed value fails a constraint, it is almost certainly due to a programming error. Furthermore, these cases are easy for an implementation to check.
But cases involving unfixed values vary, as we will see. Rationale: The best thing to do for unfixed values varies from case to case. Also, it is difficult to check constraints on unfixed values, particularly because during search a decision variable might become fixed and then backtracking will cause this value to be reverted, in which case aborting is a bad idea.
4.1.10.1. Partial Assignments
The first operation involving partiality is assignment. There are four distinct cases for assignments.
A value assigned to a fixed, constrained global variable is checked at runtime; if the assigned value does not satisfy its constraints, it is a runtime error. In other words, this:
1..5: x = 3;
is equivalent to this:
int: x = 3; constraint assert(x in 1..5, "assignment to global parameter 'x' failed")
A value assigned to an unfixed, constrained global variable makes the assignment act like a constraint; if the assigned value does not satisfy the variable’s constraints, it causes a runtime model failure. In other words, this:
var 1..5: x = 3;
is equivalent to this:
var int: x = 3; constraint x in 1..5;
Rationale: This behaviour is easy to understand and easy to implement.
A value assigned to a fixed, constrained letlocal variable is checked at runtime; if the assigned value does not satisfy its constraints, it is a runtime error. In other words, this:
let { 1..5: x = 3; } in x+1
is equivalent to this:
let { int: x = 3; } in assert(x in 1..5, "assignment to let parameter 'x' failed", x+1)
A value assigned to an unfixed, constrained letlocal variable makes the assignment act like a constraint; if the constraint fails at runtime, the failure “bubbles up” to the nearest enclosing Boolean scope, where it is interpreted as
false
.Rationale: This behaviour is consistent with assignments to global variables.
Note that in cases where a value is partly fixed and partly unfixed, e.g., some arrays, the different elements are checked according to the different cases, and fixed elements are checked before unfixed elements. For example:
u = [ let { var 1..5: x = 6} in x, let { par 1..5: y = 6; } in y) ];
This causes a runtime abort, because the second, fixed element is checked before the first, unfixed element. This ordering is true for the cases in the following sections as well. Rationale: This ensures that failures cannot mask aborts, which seems desirable.
4.1.10.2. Partial Predicate/Function and Annotation Arguments
The second kind of operation involving partiality is calls and annotations.
The semantics is similar to assignments: fixed arguments that fail their constraints will cause aborts, and unfixed arguments that fail their constraints will cause failure, which bubbles up to the nearest enclosing Boolean scope.
4.1.10.3. Partial Array Accesses
The third kind of operation involving partiality is array access. There are two distinct cases.
A fixed value used as an array index is checked at runtime; if the index value is not in the index set of the array, it is a runtime error.
An unfixed value used as an array index makes the access act like a constraint; if the access fails at runtime, the failure “bubbles up” to the nearest enclosing Boolean scope, where it is interpreted as
false
. For example:array[1..3] of int: a = [1,2,3]; var int: i; constraint (a[i] + 3) > 10 \/ i = 99;
Here the array access fails, so the failure bubbles up to the disjunction, and
i
is constrained to be 99. Rationale: Unlike predicate/function calls, modellers in practice sometimes do use array accesses that can fail. In such cases, the “bubbling up” behaviour is a reasonable one.
4.1.11. Builtin Operations
This appendix lists builtin operators, functions and predicates. They may be implemented as true builtins, or in libraries that are automatically imported for all models. Many of them are overloaded.
Operator names are written within single quotes when used in type
signatures, e.g. bool: '\/'(bool, bool)
.
We use the syntax TI: f(TI1,...,TIn)
to represent an operation
named f
that takes arguments with typeinsts TI,...,TIn
and returns a value with typeinst TI
. This is slightly more
compact than the usual MiniZinc syntax, in that it omits argument names.
4.1.11.1. Comparison Operations
Less than. Other comparisons are similar:
greater than (>
),
less than or equal (<=
),
greater than or equal (>=
),
equality (==
, =
),
and disequality (!=
).
bool: '<'( $T, $T)
var bool: '<'(var $T, var $T)
4.1.11.2. Arithmetic Operations
Addition. Other numeric operations are similar:
subtraction (
), and
multiplication (*
).
int: '+'( int, int)
var int: '+'(var int, var int)
float: '+'( float, float)
var float: '+'(var float, var float)
Unary minus. Unary plus (+
) is similar.
int: ''( int)
var int: ''(var int)
float: ''( float)
var float: ''(var float)
Integer and floatingpoint division and modulo.
int: 'div'( int, int)
var int: 'div'(var int, var int)
int: 'mod'( int, int)
var int: 'mod'(var int, var int)
float: '/' ( float, float)
var float: '/' (var float, var float)
The result of the modulo operation, if nonzero, always has the same sign as its first operand. The integer division and modulo operations are connected by the following identity:
x = (x div y) * y + (x mod y)
Some illustrative examples:
7 div 4 = 1 7 mod 4 = 3
7 div 4 = 1 7 mod 4 = 3
7 div 4 = 1 7 mod 4 = 3
7 div 4 = 1 7 mod 4 = 3
Sum multiple numbers.
Product (product
) is similar. Note that the sum of an empty array
is 0, and the product of an empty array is 1.
int: sum(array[$T] of int )
var int: sum(array[$T] of var int )
float: sum(array[$T] of float)
var float: sum(array[$T] of var float)
Minimum of two values; maximum (max
) is
similar.
$T: min( $T, $T)
var $T: min(var $T, var $T)
Minimum of an array of values; maximum (max
) is similar.
Aborts if the array is empty.
$U: min(array[$T] of $U)
var $U: min(array[$T] of var $U)
Minimum of a fixed set; maximum (max
) is similar.
Aborts if the set is empty.
$T: min(set of $T)
Absolute value of a number.
int: abs( int)
var int: abs(var int)
float: abs( float)
var float: abs(var float)
Square root of a float. Aborts if argument is negative.
float: sqrt( float)
var float: sqrt(var float)
Power operator. E.g. pow(2, 5)
gives 32
.
int: pow(int, int)
float: pow(float, float)
Natural exponent.
float: exp(float)
var float: exp(var float)
Natural logarithm. Logarithm to base 10 (log10
) and logarithm to base
2 (log2
) are similar.
float: ln(float)
var float: ln(var float)
General logarithm; the first argument is the base.
float: log(float, float)
Sine. Cosine (cos
), tangent (tan
), inverse sine
(asin
), inverse cosine (acos
), inverse tangent
(atan
), hyperbolic sine (sinh
), hyperbolic cosine
(cosh
), hyperbolic tangent (tanh
),
inverse hyperbolic sine (asinh
), inverse hyperbolic cosine
(acosh
) and inverse hyperbolic tangent (atanh
) are similar.
float: sin(float)
var float: sin(var float)
4.1.11.3. Logical Operations
Conjunction. Other logical operations are similar:
disjunction (\/)
reverse implication (<
),
forward implication (>
),
biimplication (<>
),
exclusive disjunction (xor
),
logical negation (not
).
Note that the implication operators are not written
using =>
, <=
and <=>
as is the case in some
languages. This allows <=
to instead represent “less than or
equal”.
bool: '/\'( bool, bool)
var bool: '/\'(var bool, var bool)
Universal quantification.
Existential quantification (exists
) is similar. Note that, when
applied to an empty list, forall
returns true
, and
exists
returns false
.
bool: forall(array[$T] of bool)
var bool: forall(array[$T] of var bool)
Nary exclusive disjunction.
Nary biimplication (iffall
) is similar, with true
instead
of false
.
bool: xorall(array[$T] of bool: bs) = foldl('xor', false, bs)
var bool: xorall(array[$T] of var bool: bs) = foldl('xor', false, bs)
4.1.11.4. Set Operations
Set membership.
bool: 'in'( $T, set of $T )
var bool: 'in'(var $$E, var set of $$E)
Nonstrict subset. Nonstrict superset (superset
) is similar.
bool: 'subset'( set of $T , set of $T )
var bool: 'subset'(var set of $$E, var set of $$E)
Set union. Other set operations are similar:
intersection (intersect
),
difference (diff
),
symmetric difference (symdiff
).
set of $T: 'union'( set of $T, set of $T )
var set of $$E: 'union'(var set of $$E, var set of $$E )
Set ranges. Constructs a set given a lower and an upper bound.
Whether the operator constructs a set that includes or excludes the bounds depends
on the placement of the < symbol in the operator.
If the first argument is larger than the second
(e.g. 1..0
), it returns the empty set.
The arguments to the operators can be either integers or values of
enumerated types (l+1
and u1
in the comments mean enum_next(l)
and enum_prev(l)
in that case).
% Return set {l, ..., u}
set of $$E: '..'($$E: l, $$E: u)
% Return set {l+1, ..., u}
set of $$E: '<..'($$E: l, $$E: u)
% Return set {l, ..., u1}
set of $$E: '..<'($$E: l, $$E: u)
% Return set {l+1, ..., u1}
set of $$E: '<..<'($$E: l, $$E: u)
Note that set range operators can be used with only one of the bounds given. The minimum or maximum of the type of the bound is then used for the other bound:
% x = {l, ..., max(enum_of(l))}
set of X: x = l..;
% x = {min(enum_of(u)), ..., u}
set of X: x = ..u;
Cardinality of a set.
int: card( set of $T)
var int: card(var set of $$E)
Union of an array of sets.
Intersection of multiple sets (array_intersect
) is similar.
set of $U: array_union(array[$T] of set of $U)
var set of $$E: array_union(array[$T] of var set of $$E)
4.1.11.5. Array Operations
Length of an array.
int: length(array[$T] of $U)
List concatenation. Returns the list (integerindexed array) containing
all elements of the first argument followed by all elements of the
second argument, with elements occurring in the same order as
in the arguments. The resulting indices are in the range 1..n
,
where n
is the sum of the lengths of the arguments.
Rationale: This allows listlike arrays to be concatenated naturally
and avoids problems with overlapping indices. The resulting indices
are consistent with those of implicitly indexed array literals.
Note that '++'
also performs string concatenation.
array[int] of $T: '++'(array[int] of $T, array[int] of $T)
Index sets of arrays. If the argument is a literal, returns 1..n
where n
is the (sub)array length. Otherwise, returns the declared
or inferred index set. This list is only partial, it extends in the obvious
way, for arrays of higher dimensions.
set of $T: index_set (array[$T] of $V)
set of $T: index_set_1of2(array[$T, $U] of $V)
set of $U: index_set_2of2(array[$T, $U] of $V)
...
Replace the indices of the array given by the last argument with the Cartesian product of the sets given by the previous arguments. Similar versions exist for arrays up to 6 dimensions.
array[$T1] of $V: array1d(set of $T1, array[$U] of $V)
array[$T1,$T2] of $V:
array2d(set of $T1, set of $T2, array[$U] of $V)
array[$T1,$T2,$T3] of $V:
array3d(set of $T1, set of $T2, set of $T3, array[$U] of $V)
4.1.11.6. Coercion Operations
Round a float towards \(+\infty\), \(\infty\), and the nearest integer, respectively.
int: ceil (float)
int: floor(float)
int: round(float)
Explicit casts from one typeinst to another.
int: bool2int( bool)
var int: bool2int(var bool)
float: int2float( int)
var float: int2float(var int)
array[int] of $T: set2array(set of $T)
Capturing of undefinedness and optionality. These binary infix operators return x
if it is
both defined and not absent, and y
otherwise.
$T: 'default'(opt $T:x, $T: y);
opt $T: 'default'(opt $T:x, opt $T: y);
var $T: 'default'(var opt $T:x, var $T: y);
var opt $T: 'default'(var opt $T:x, var opt $T: y);
array[$U] of $T: 'default'(array[$U] of $T:x, array[$U] of $T: y);
array[$U] of opt $T: 'default'(array[$U] of opt $T:x, array[$U] of opt $T: y);
array[$U] of var $T: 'default'(array[$U] of var $T:x, array[$U] of var $T: y);
array[$U] of var opt $T: 'default'(array[$U] of var opt $T:x, array[$U] of var opt $T: y);
4.1.11.7. String Operations
Tostring conversion. Converts any value to a string for output purposes. The exact form of the resulting string is implementationdependent.
string: show($T)
Formatted tostring conversion for integers. Converts the integer given by the second argument into a string right justified by the number of characters given by the first argument, or left justified if that argument is negative. If the second argument is not fixed, the form of the string is implementationdependent.
string: show_int(int, var int);
Formatted tostring conversion for floats. Converts the float given by the third argument into a string right justified by the number of characters given by the first argument, or left justified if that argument is negative. The number of digits to appear after the decimal point is given by the second argument. It is a runtime error for the second argument to be negative. If the third argument is not fixed, the form of the string is implementationdependent.
string: show_float(int, int, var float)
String concatenation. Note that '++'
also performs array
concatenation.
string: '++'(string, string)
Concatenate an array of strings.
Equivalent to folding '++'
over the array, but may be implemented more
efficiently.
string: concat(array[$T] of string)
Concatenate an array of strings, putting a separator between adjacent strings. Returns the the empty string if the array is empty.
string: join(string, array[$T] of string)
4.1.11.8. Bound and Domain Operations
The bound operations lb
and ub
return fixed, correct lower/upper bounds
to the expression.
For numeric types, they return a lower/upper bound value,
e.g. the lowest/highest value the expression can take.
For set types, they return a subset/superset,
e.g. the intersection/union of all possible values of the set expression.
The bound operations abort on expressions that have no corresponding finite bound.
For example, this would be the case for a variable declared without bounds
in an implementation that does not assign default bounds.
(Set expressions always have a finite lower bound of course,
namely {}
, the empty set.)
Numeric lower/upper bound:
int: lb(var int)
float: lb(var float)
int: ub(var int)
float: ub(var float)
Set lower/upper bound:
set of int: lb(var set of int)
set of int: ub(var set of int)
Versions of the bound operations that operate on arrays are also available, they return a safe lower bound or upper bound for all members of the array  they abort if the array is empty:
int: lb_array(array[$T] of var int)
float: lb_array(array[$T] of var float)
set of int: lb_array(array[$T] of var set of int)
int: ub_array(array[$T] of var int)
float: ub_array(array[$T] of var float)
set of int: ub_array(array[$T] of var set of int)
Integer domain:
set of int: dom(var int)
The domain operation dom
returns a fixed superset
of the possible values of the expression.
Integer array domain, returns a superset of all possible values that may appear in the array  this aborts if the array is empty:
set of int: dom_array(array[$T] of var int)
Domain size for integers:
int: dom_size(var int)
The domain size operation dom_size
is equivalent
to card(dom(x))
.
Note that these operations can produce different results depending on when they are evaluated and what form the argument takes. For example, consider the numeric lower bound operation.
If the argument is a fixed expression, the result is the argument’s value.
If the argument is a decision variable, then the result depends on the context.
If the implementation can determine a lower bound for the variable, the result is that lower bound. The lower bound may be from the variable’s declaration, or higher than that due to preprocessing, or lower than that if an implementationdefined lower bound is applied (e.g. if the variable was declared with no lower bound, but the implementation imposes a lowest possible bound).
If the implementation cannot determine a lower bound for the variable, the operation aborts.
If the argument is any other kind of unfixed expression, the lower bound depends on the bounds of unfixed subexpressions and the connecting operators.
4.1.11.9. Option Type Operations
The option type value (\(\top\)) is written
opt $T: '<>';
One can determine if an option type variable actually occurs or not using
occurs
and absent
par bool: occurs(par opt $T);
var bool: occurs(var opt $T);
par bool: absent(par opt $T);
var bool: absent(var opt $T);
One can return the nonoptional value of an option type variable using the
function deopt
par $T: deopt{par opt $T);
var $T: deopt(var opt $T);
4.1.11.10. Other Operations
Check a Boolean expression is true, and abort if not, printing the second
argument as the error message. The first one returns the third argument, and
is particularly useful for sanitychecking arguments to predicates and
functions; importantly, its third argument is lazy, i.e. it is only evaluated
if the condition succeeds. The second one returns true
and is useful
for global sanitychecks (e.g. of instance data) in constraint items.
$T: assert(bool, string, s$T)
par bool: assert(bool, string)
Abort evaluation, printing the given string.
$T: abort(string)
Return true. As a sideeffect, an implementation may print the first argument.
bool: trace(string)
Return the second argument. As a sideeffect, an implementation may print the first argument.
$T: trace(string, $T)
Check if the argument’s value is fixed at this point in evaluation. If not, abort; if so, return its value. This is most useful in output items when decision variables should be fixed: it allows them to be used in places where a fixed value is needed, such as ifthenelse conditions.
$T: fix(var $T)
As above, but return false
if the argument’s value is not fixed.
par bool: is_fixed(var $T)
4.1.12. Contenttypes
The contenttype application/xzincoutput defines a text output format for Zinc. The format extends the abstract syntax and semantics given in Runtime Outcomes, and is discussed in detail in Output.
The full syntax is as follows:
% Output
<output> ::= <nosolutions> [ <warnings> ] <freetext>
 ( <solution> )* [ <complete> ] [ <warnings> ] <freetext>
% Solutions
<solution> ::= <solutiontext> [ \n ] "" \n
% Unsatisfiable
<nosolutions> ::= "=====UNSATISFIABLE=====" \n
% Complete
<complete> ::= "==========" \n
% Messages
<warnings> ::= ( <message> )+
<message> ::= ( <line> )+
<line> ::= "%" [^\n]* \n
The solution text for each solution must be as described in Output Items. A newline must be appended if the solution text does not end with a newline.
4.1.13. JSON support
MiniZinc can support reading input parameters and providing output formatted as JSON objects. A JSON input file needs to have the following structure:
Consist of a single toplevel object
The members of the object (the keyvalue pairs) represent model parameters
Each member key must be a valid MiniZinc identifier (and it supplies the value for the corresponding parameter of the model)
Each member value can be one of the following:
A string (assigned to a MiniZinc string parameter)
A number (assigned to a MiniZinc int or float parameter)
The values true or false (assigned to a MiniZinc bool parameter)
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 multidimensional MiniZinc arrays.
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). The list may additionally contain an element which is a sublist comprising a pair of values representing a minimum and maximum of a range in the set.
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).
The value of an enumerated type constructor call encoded as an object with a member with key "c" and a string value (the identifier of the constructor call), and a member with key "e" and a enumerated type (or constructor) object value (the argument to the call).
MiniZinc supports coercion of some JSON input types for more convenient input:
A list of values can be coerced to a set
A string value can be coerced to an enumerated type value (but not a constructor call)
Assume a MiniZinc model declaring the following parameters:
int: n;
enum Customers;
array[1..n,Customers] of int: distances;
array[1..n] of set of int: patterns;
Here is an example of a JSON parameter file using all of the above features:
{
"n" : 2,
"Customers" : [ {"e" : "Customer A"}, {"e" : "Customer B"}, {"e" : "Customer C"} ],
"distances" : [ [1,2,3],
[4,5,6]],
"patterns" : [ {"set" : [1,3,5]}, {"set" : [2,4,6]} ]
}
The first parameter declares a simple integer n. The Customers parameter defines the members of an enumerated type. The distances parameter is a twodimensional array; note that all inner arrays must be of the same size in order to map to a (rectangular) MiniZinc twodimensional array. The patterns parameter is an array of sets of integers.
4.1.14. Full grammar
4.1.14.1. Items
% A MiniZinc model
<model> ::= [ <item> ";" ... ]
% Items
<item> ::= <includeitem>
 <vardeclitem>
 <enumitem>
 <typeinstsynitem>
 <assignitem>
 <constraintitem>
 <solveitem>
 <outputitem>
 <predicateitem>
 <testitem>
 <functionitem>
 <annotationitem>
<tiexprandid> ::= <tiexpr> ":" <ident>
% Include items
<includeitem> ::= "include" <stringliteral>
% Variable declaration items
<vardeclitem> ::= <tiexprandid> <annotations> [ "=" <expr> ]
 "any" ":" <ident> <annotations> [ "=" <expr> ]
% Enum items
<enumitem> ::= "enum" <ident> <annotations> [ "=" <enumcaseslist> ]
<enumcaseslist> ::= <enumcases>
 <enumcaseslist> "++" <enumcases>
<enumcases> ::= "{" <ident> "," ... "}"
 "_" "(" <expr> ")"
 <ident> "(" <ident> ")"
 "anon_enum" "(" <expr> ")"
% Typeinst synonym items
<typeinstsynitem> ::= "type" <ident> <annotations> "=" <tiexpr>
% Assign items
<assignitem> ::= <ident> "=" <expr>
% Constraint items
<constraintitem> ::= "constraint" [ <stringannotation> ] <expr>
% Solve item
<solveitem> ::= "solve" <annotations> "satisfy"
 "solve" <annotations> "minimize" <expr>
 "solve" <annotations> "maximize" <expr>
% Output items
<outputitem> ::= "output" [ <stringannotation> ] <expr>
% Annotation items
<annotationitem> ::= "annotation" <ident> <params>
% Predicate, test and function items
<predicateitem> ::= "predicate" <operationitemtail>
<testitem> ::= "test" <operationitemtail>
<functionitem> ::= "function" <tiexpr> ":" <operationitemtail>
<operationitemtail> ::= <ident> <params> <annotations> [ "=" <expr> ]
<params> ::= [ ( <tiexprandid> "," ... ) ]
4.1.14.2. TypeInst Expressions
<tiexpr> ::= <basetiexpr>
 <arraytiexpr>
<basetiexpr> ::= <varpar> <optti> <setti> <basetiexprtail> ["++" <basetiexpr>]
 "any" <tivariableexprtail>
<varpar> ::= "var"  "par"  ε
<optti> ::= "opt"  ε
<setti> ::= "set" "of"  ε
<basetype> ::= "bool"
 "int"
 "float"
 "string"
<basetiexprtail> ::= <ident>
 <basetype>
 <tivariableexprtail>
 <tupletiexprtail>
 <recordtiexprtail>
 "ann"
 "{" <expr> "," ... "}"
 <numexpr> ".." <numexpr>
% Typeinst variables
<tivariableexprtail> ::= $[AZaz$][AZaz09_]*
% Array typeinst expressions
<arraytiexpr> ::= "array" [ <tiexpr> "," ... ] "of" <basetiexpr>
 "list" "of" <basetiexpr>
% Tuple typeinst expressions
<tupletiexprtail> ::= "tuple" ( <tiexpr> "," ... )
% Record typeinst expressions
<recordtiexprtail> ::= "record" ( <tiexprandid> "," ... )
4.1.14.3. Expressions
<expr> ::= <expratom> <exprbinoptail>
<expratom> ::= <expratomhead> <expratomtail> <annotations>
<exprbinoptail> ::= [ <binop> <expr> ]
<expratomhead> ::= <builtinunop> <expratom>
 "(" <expr> ")"
 <identorquotedop>
 "_"
 <boolliteral>
 <intliteral>
 <floatliteral>
 <stringliteral>
 <setliteral>
 <setcomp>
 <arrayliteral>
 <arrayliteral2d>
 <indexedarrayliteral>
 <indexedarrayliteral2d>
 <tupleliteral>
 <recordliteral>
 <arraycomp>
 <indexedarraycomp>
 <annliteral>
 <ifthenelseexpr>
 <letexpr>
 <callexpr>
 <gencallexpr>
<expratomtail> ::= ε
 <arrayaccesstail> <expratomtail>
% Numeric expressions
<numexpr> ::= <numexpratom> <numexprbinoptail>
<numexpratom> ::= <numexpratomhead> <expratomtail> <annotations>
<numexprbinoptail> ::= [ <numbinop> <numexpr> ]
<numexpratomhead> ::= <builtinnumunop> <numexpratom>
 "(" <numexpr> ")"
 <identorquotedop>
 <intliteral>
 <floatliteral>
 <ifthenelseexpr>
 <letexpr>
 <callexpr>
 <gencallexpr>
% Builtin operators
<builtinop> ::= <builtinbinop>  <builtinunop>
<binop> ::= <builtinbinop>  ‘<ident>‘
<builtinbinop> ::= "<>"  ">"  "<"  "\/"  "xor"  "/\"
 "<"  ">"  "<="  ">="  "=="  "="  "!="
 "~="  "~!="
 "in"  "subset"  "superset"  "union"  "diff"  "symdiff"
 ".."  "intersect"  "++"  "default"  <builtinnumbinop>
<builtinunop> ::= "not"  <builtinnumunop>
% Builtin numeric operators
<numbinop> ::= <builtinnumbinop>  ‘<ident>‘
<builtinnumbinop> ::= "+"  ""  "*"  "/"  "div"  "mod"  "^"
 "~+"  "~"  "~*"  "~/"  "~div"
<builtinnumunop> ::= "+"  ""
% Boolean literals
<boolliteral> ::= "false"  "true"
% Integer literals
<intliteral> ::= [09]+
 0x[09AFaf]+
 0o[07]+
% Float literals
<floatliteral> ::= [09]+"."[09]+
 [09]+"."[09]+[Ee][+]?[09]+
 [09]+[Ee][+]?[09]+
 0[xX]([09afAF]*"."[09afAF]+[09afAF]+".")([pP][+]?[09]+)
 (0[xX][09afAF]+[pP][+]?[09]+)
% String literals
<stringcontents> ::= ([^"\n\]  \[07][07?][07]?  \x[09afAF][09afAF]?  \n  \t  \"  \\)*
<stringliteral> ::= """ <stringcontents> """
 """ <stringcontents> "\(" <stringinterpolatetail>
<stringinterpolatetail> ::= <expr> ")"<stringcontents>"""
 <expr> ")"<stringcontents>"\(" <stringinterpolatetail>
% Set literals
<setliteral> ::= "{" [ <expr> "," ... ] "}"
% Set comprehensions
<setcomp> ::= "{" <expr> "" <comptail> "}"
<comptail> ::= <generator> [ "where" <expr> ] "," ...
<generator> ::= ( <ident>  "_" ) "," ... "in" <expr>
% Array literals
<arrayliteral> ::= "[" [ <expr> "," ... ] "]"
% 2D Array literals
<arrayliteral2d> ::= "[" [ [ <expr> "," ... ] "" ... ] "]"
% Indexed 2D Array literals
<indexedarrayliteral2d> ::= "[" [ <expr> ":" ... ] [ [ <expr> ":" ] <expr> "," ... ] "]"
% Indexed array literals
<indexedarrayliteral> ::= "[" [ ( <indextuple> ":" <expr> ) "," ... ] "]"
 "[" [ <indextuple> ":" <expr> "," <expr> "," ... ] "]"
<indextuple> ::= <expr>
 "(" [ <expr> "," ... ] ")"
% Tuple literals
<tupleliteral> ::= "(" <expr> "," [ <expr> "," ... ] ")"
% Record literals
<recordliteral> ::= "(" <ident> ":" <expr> "," [ <ident> ":" <expr> "," ... ] ")"
% Array comprehensions
<arraycomp> ::= "[" <expr> "" <comptail> "]"
% Indexed array comprehensions
<indexedarraycomp> ::= "[" <indextuple> ":" <expr> "" <comptail> "]"
% Array access
<arrayaccesstail> ::= "[" <expr> "," ... "]"
% Annotation literals
<annliteral> ::= <ident> [ "(" <expr> "," ... ")" ]
% Ifthenelse expressions
<ifthenelseexpr> ::= "if" <expr> "then" <expr> [ "elseif" <expr> "then" <expr> ]* "else" <expr> "endif"
% Call expressions
<callexpr> ::= <identorquotedop> [ "(" <expr> "," ... ")" ]
% Let expressions
<letexpr> ::= "let" "{" <letitem> ";" ... "}" "in" <expr>
<letitem> ::= <vardeclitem>
 <constraintitem>
% Generator call expressions
<gencallexpr> ::= <identorquotedop> "(" <comptail> ")" "(" <expr> ")"
4.1.14.4. Miscellaneous Elements
% Identifiers
<ident> ::= _?[AZaz][AZaz09_]*  ’[^’\xa\xd\x0]+’
% Identifiers and quoted operators
<identorquotedop> ::= <ident>
 ’<builtinop>’
% Annotations
<annotations> ::= [ "::" <annotation> ]*
<annotation> ::= <expratomhead> <expratomtail>
<stringannotation> ::= "::" <stringliteral>
4.1.4.2. Comments
A % indicates that the rest of the line is a comment. MiniZinc also has block comments, using symbols /* and */ to mark the beginning and end of a comment.