程序代写代做代考 Haskell chain flex data structure Specification of MiniZinc

Specification of MiniZinc

The MiniZinc Team

Data61/CSIRO
Monash University

The University of Melbourne
Melbourne, Australia

November 2016
(MiniZinc version 2.1.0)

Contents

1. Introduction 4

2. Notation 4

3. Overview of a Model 5
3.1. Evaluation Phases . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
3.2. Run-time Outcomes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
3.3. Output . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

4. Syntax Overview 6
4.1. Character Set . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
4.2. Comments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
4.3. Identifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6

5. High-level Model Structure 6
5.1. Items . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6
5.2. Model Instance Files . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
5.3. Namespaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7
5.4. Scopes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

6. Types and Type-insts 8
6.1. Properties of Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
6.2. Instantiations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
6.3. Type-insts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
6.4. Type-inst Expressions Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8
6.5. Built-in Scalar Types and Type-insts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
6.6. Built-in Compound Types and Type-insts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10
6.7. Constrained Type-insts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

7. Expressions 13
7.1. Expressions Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13
7.2. Operators . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
7.3. Expression Atoms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

8. Items 20
8.1. Include Items . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
8.2. Variable Declaration Items . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
8.3. Enum Items . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
8.4. Assignment Items . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
8.5. Constraint Items . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
8.6. Solve Items . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
8.7. Output Items . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
8.8. Annotation Items . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
8.9. User-defined Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23

9. Annotations 25

10.Partiality 25
10.1. Partial Assignments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
10.2. Partial Predicate/Function and Annotation Arguments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26
10.3. Partial Array Accesses . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27

A. Built-in Operations 28
A.1. Comparison Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
A.2. Arithmetic Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
A.3. Logical Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
A.4. Set Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
A.5. Array Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
A.6. Coercion Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
A.7. String Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
A.8. Bound and Domain Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
A.9. Option Type Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
A.10.Other Operations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32

B. MiniZinc Grammar 33
B.1. Items . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
B.2. Type-Inst Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
B.3. Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34
B.4. Miscellaneous Elements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35

C. Content-types 36
C.1. ‘application/x-zinc-output’ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36

D. JSON support 37

1. Introduction

This document defines MiniZinc, a language for modelling constraint satisfaction and optimisation problems.
MiniZinc is a high-level, typed, mostly first-order, functional, modelling language. It provides:

• mathematical notation-like 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;

• high-level data structures and data encapsulation (sets, arrays, enumerated types, constrained type-insts);

• extensibility (user-defined functions and predicates);

• reliability (type checking, instantiation checking, assertions);

• solver-independent modelling;

• simple, declarative semantics.

MiniZinc is similar to OPL and moves closer to CLP languages such as ECLiPSe.
This document has the following structure. Section 2 introduces the syntax notation used throughout the specification.

Section 3 provides a high-level overview of MiniZinc models. Section 4 covers syntax basics. Section 5 covers high-level
structure: items, multi-file models, namespaces, and scopes. Section 6 introduces types and type-insts. Section 7 covers
expressions. Section 8 describes the top-level items in detail. Section 9 describes annotations. Section 10 describes how
partiality is handled in various cases. Appendix A describes the language built-ins. Appendix B gives the MiniZinc
grammar. Appendix C defines content-types 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.

Original authors. The original version of this document was prepared by Nicholas Nethercote, Kim Marriott, Reza Rafeh,
Mark Wallace and Maŕıa Garćıa de la Banda. MiniZinc is evolving, however, and so is this document.

For a formally published paper on the MiniZinc language and the superset Zinc language , please see:
N. Nethercote, P.J. Stuckey, R. Becket, S. Brand, G.J. Duck, and G. Tack. Minizinc: Towards a standard CP modelling

language. In C. Bessiere, editor, Proceedings of the 13th International Conference on Principles and Practice of Constraint
Programming, volume 4741 of LNCS, pages 529–543. Springer-Verlag, 2007.

K. Marriott, N. Nethercote, R. Rafeh, P.J. Stuckey, M. Garćıa de la Banda, and M. Wallace. The Design of the Zinc
Modelling Language. Constraints, 13(3):229-267, 2008.

2. Notation

The basics of the EBNF used in this specification are as follows.

• Non-terminals are written between angle brackets, e.g. 〈item〉.

• Terminals are written in fixed-width font. They are usually underlined for emphasis, e.g. constraint, although this
is not always done if the meaning is clear.

• 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〉 )+.

• Non-empty lists are written with an item, a separator/terminator terminal, and “. . . ”. For example, this:
〈expr〉 , . . .

is short for this:

〈expr〉 ( , 〈expr〉 )* [ , ]
The final terminal is always optional in non-empty lists.

• Regular expressions, written in fixed-width font, are used in some productions, e.g. [-+]?[0-9]+.

MiniZinc’s grammar is presented piece-by-piece throughout this document. It is also available as a whole in Appendix B.
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
.

• A sequence of space characters of length n is written nSP, e.g., 2SP.

3. Overview of a Model

Conceptually, a MiniZinc problem specification has two parts.

1. The model : the main part of the problem specification, which describes the structure of a particular class of problems.

2. 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 an model instance (sometimes abbreviated to instance).
The model and data may be separated, or the data may be “hard-wired” into the model. Section 5.2 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. Section 8.6 specifies how the class of problem is chosen.

3.1. Evaluation Phases

A MiniZinc model instance is evaluated in two distinct phases.

1. Instance-time: static checking of the model instance.

2. Run-time: 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 instance-time. This
could be caused by a syntax error, a type-inst 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 run-time. The form of output for static errors is
implementation-dependent, 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 run-time, and the resulting warning given to the user may be
more helpful than if the unsatisfiability is detected at run-time.

An implementation must produce a warning if the objective for an optimisation problem is unbounded.

3.2. Run-time Outcomes

Assuming there are no static errors, the output from the run-time phase has the following abstract form:

〈output〉 ::= 〈no-solutions〉 [ 〈warnings〉 ] 〈free-text〉
| ( 〈solution〉 )* [ 〈complete〉 ] [ 〈warnings〉 ] 〈free-text〉

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 completness message indicates

that the search is incomplete.
Any warnings produced during run-time must be summarised after the statement of completeness. In particular, if

there were any warnings at all during run-time 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.

3.3. Output

Implementations must be capable of producing output of content type ‘application/x-zinc-output’, which is described
below and also in Appendix C. 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/x-zinc-output’ extends the syntax from the previous section as follows:

〈solution〉 ::= 〈solution-text〉 [
] ———-

The solution text for each solution must be as described in Section 8.7. 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.

〈no-solutions〉 ::= =====UNSATISFIABLE=====

The completness result is printed on a separate line. Rationale. The strings are designed to clearly indicate the end of
the solutions.

〈complete〉 ::= ==========

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〉 )+
〈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 post-processing. 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. Syntax Overview

4.1. Character Set

The input files to MiniZinc must be encoded as UTF-8.
MiniZinc is case sensitive. There are no places where upper-case or lower-case 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.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.

4.3. Identifiers

Identifiers have the following syntax:

〈ident〉 ::= [A-Za-z][A-Za-z0-9_]* % excluding keywords
| ’[^’xaxdx0]*’

For example:

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, 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 built-ins; see Section A for details.

5. High-level Model Structure

5.1. Items

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 top-level syntax:

Include items provide a way of combining multiple files into a single instance. This allows a model to be split into
multiple files (Section 8.1).

Variable declaration items introduce new global variables and possibly bind them to a value (Section 8.2).
Assignment items bind values to global variables (Section 8.4).
Constraint items describe model constraints (Section 8.5).
Solve items are the “starting point” of a model, and specify exactly what kind of solution is being looked for: plain sat-

isfaction, or the minimization/maximization of an expression. Each model must have exactly one solve item (Section 8.6).
Output items are used for nicely presenting the result of a model execution (Section 8.7).
Predicate items, test items (which are just a special type of predicate) and function items introduce new user-defined

predicates and functions which can be called in expressions (Section 8.9). Predicates, functions, and built-in operators are
described collectively as operations.

Annotation items augment the ann type, values of which can specify non-declarative and/or solver-specific information
in a model.

5.2. Model Instance Files

MiniZinc models can be constructed from multiple files using include items (see Section 8.1). 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 Section 8.4).

Data files may not include calls to user-defined 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 command-line.

When checking a model with data, all global variables with fixed type-insts 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.

5.3. Namespaces

All names declared at the top-level belong to a single namespace. It includes the following names.

1. All global variable names.

2. All function and predicate names, both built-in and user-defined.

3. All enumerated type names and enum case names.

4. All annotation names.

Because multi-file MiniZinc models are composed via concatenation (Section 5.2), all files share this top-level namespace.
Therefore a variable v declared in one model file could not be declared with a different type in a different file, for example.

MiniZinc supports overloading of built-in and user-defined operations.

5.4. Scopes

Within the top-level namespace, there are several kinds of local scope that introduce local names:

• Comprehension expressions (Section 7.3.7).

• Let expressions (Section 7.3.14).

• Function and predicate argument lists and bodies (Section 8.9).
The listed sections specify these scopes in more detail. In each case, any names declared in the local scope overshadow
identical global names.

6. Types and Type-insts

MiniZinc provides four scalar built-in types: Booleans, integers, floats, and strings; enumerated types; two compound
built-in types: sets and multi-dimensional 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 type-inst.

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
type-insts, 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 instance-time, and whether it can be involved in automatic coercions.

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, types defined via set expression type-insts such as range types (see
Section 6.7.1), 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 (Section 6.6.1) and
array indices (Section 6.6.2).

Every finite type has a domain, which is a set value that holds all the possible values represented by the type.

• Every first-order type (this excludes ann) has a built-in total order and a built-in 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.

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 instance-time. At the
most basic level, the instantiation system distinguishes between two kinds of variables:

1. Parameters, whose values are fixed at instance-time (usually written just as “fixed”).

2. Decision variables (often abbreviated to variables), whose values may be completely unfixed at instance-time, but
may become fixed at run-time (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. Arrays and
ann can contain decision variables.

6.3. Type-insts

Because each variable has both a type and an inst, they are often combined into a single type-inst. Type-insts are primarily
what we deal with when writing models, rather than types.

A variable’s type-inst never changes. This means a decision variable whose value becomes fixed during model evaluation
still has its original type-inst (e.g. var int), because that was its type-inst at instance-time.

Some type-insts can be automatically coerced to another type-inst. 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

c→ var int. Also, any
type-inst can be considered coercible to itself. MiniZinc allows coercions between some types as well.

Some type-insts can be varified, i.e. made unfixed at the top-level. For example, par int is varified to var int. We
write this par int

v→ var int.
Type-insts that are varifiable include the type-insts of the types that can be decision variables (Booleans, integers,

floats, sets, enumerated types). Varification is relevant to array accesses.

6.4. Type-inst Expressions Overview

This section partly describes how to write type-insts in MiniZinc models. Further details are given for each type as they
are described in the following sections.

A type-inst expression specifies a type-inst.
Type-inst expressions may include type-inst constraints.
Type-inst expressions appear in variable declarations (Section 8.2), user-defined operation items (Section 8.9).
Type-inst expressions have this syntax:

〈ti-expr〉 ::= 〈base-ti-expr〉
〈base-ti-expr〉 ::= 〈var-par〉〈base-ti-expr-tail〉
〈var-par〉 ::= var | par | �
〈base-ti-expr-tail〉 ::= 〈ident〉

| bool
| int
| float
| string
| 〈set-ti-expr-tail〉
| 〈array-ti-expr-tail〉
| ann
| opt 〈base-ti-expr-tail〉
| { 〈expr〉 , . . . }
| 〈num-expr〉 .. 〈num-expr〉

(The final alternative, for range types, uses the numeric-specific 〈num-expr〉 non-terminal, defined in Section 7.1, rather
than the 〈expr〉 non-terminal. 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 type-inst expressions for scalar types. The compound type-inst expression syntax is covered in
more detail in Section 6.6.

The par and var keywords (or lack of them) determine the instantiation. The par annotation can be omitted; the
following two type-inst 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 type-inst
checking.

A type-inst is fixed if it does not contain var or any, with the exception of ann.
Note that several type-inst expressions that are syntactically expressible represent illegal type-insts. For example,

although the grammar allows var in front of all these base type-inst expression tails, it is a type-inst error to have var in
the front of a string or array expression.

6.5. Built-in Scalar Types and Type-insts

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

v→ var bool, var bool v→ var bool.
Ordering. The value false is considered smaller than true.

Initialisation. A fixed Boolean variable must be initialised at instance-time; an unfixed Boolean variable need not be.

Coercions. par bool
c→ var bool.

Also Booleans can be automatically coerced to integers; see Section 6.5.2.

6.5.2. Integers

Overview. Integers represent integral numbers. Integer representations are implementation-defined. This means that
the representable range of integers is implementation-defined. However, an implementation should abort at run-time 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 Section 6.7.1).

Varifiable? par int
v→ var int, var int v→ var int.

Ordering. The ordering on integers is the standard one.

Initialisation. A fixed integer variable must be initialised at instance-time; an unfixed integer variable need not be.

Coercions. par int
c→ var int, par bool c→ par int, par bool c→ var int, var bool c→ var int.

Also, integers can be automatically coerced to floats; see Section 6.5.3.

6.5.3. Floats

Overview. Floats represent real numbers. Float representations are implementation-defined. This means that the
representable range and precision of floats is implementation-defined. However, an implementation should abort at run-
time on exceptional float operations (e.g. those that produce NaNs, 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 Section 6.7.1).

Varifiable? par float
v→ var float, var float v→ var float.

Ordering. The ordering on floats is the standard one.

Initialisation. A fixed float variable must be initialised at instance-time; an unfixed float variable need not be.

Coercions. par int
c→ par float, par int c→ var float, var int c→ var float, par float c→ var float.

6.5.4. Enumerated Types

Overview. Enumerated types (or enums for short) provide a set of named alternatives. Each alternative is identified by its
case name. Enumerated type

Published by admin

Leave a Reply Cancel reply