This appendix defines the exact bytes rendered from the data of
chapter 3. The rules apply independently of the
implementation language, locale, and host stream settings. In byte
spellings below, LF is 0a, space is 20, and punctuation is ASCII.
B.1 Rendering data and operation boundaries
Rendering MUST preserve entry order
and render each entry once, using its final value at its existing position.
It MUST NOT sort entries, expose record names as extra entries, include
format metadata, or add a filename or header. It MUST render stored values
without rereading input, reevaluating expressions, checks, or defaults, or
reinterpreting original token spellings.
The dznexample operation
MUST perform the same parsing, parameter admission, UTF-8 validation,
instance selection, execution, and trailing-input checks as read, then
render its successful data. An earlier failure MUST retain its existing
code and locations. Failed reading produces no successful dzn document.
Rendering successful catalog data
MUST use these same rendering rules; §B.7 defines its example notation.
Rendering MUST add zero idle-work and expression-effort units under
chapter 10, regardless of depth, leaf count, output
size, or the work used to choose numeric text. Successful execution exactly
at either limit MUST remain renderable. Rendering introduces no language
error code; §B.8 covers output failures.
B.2 Entry names and integers
An entry name MUST be emitted unchanged if its first byte is an ASCII
letter and it is not exactly one of these case-sensitive names:
ann annotation any array bool case constraint default 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
Every other entry name MUST be enclosed in single ASCII quotes. Thus _
and every underscore-leading name are quoted, var is quoted, and Var
and annotation_2 are plain. Implementations MUST use this frozen set,
independently of any host MiniZinc package. Entry names remain subject to
§5.4; these output rules introduce neither
arbitrary identifiers nor a name-escape syntax.
An int leaf MUST use its exact signed base-10 spelling: a minus sign only
for negative values, no plus sign or leading zeros, and no decimal point
or exponent. Zero MUST be 0. Implementations MUST preserve the entire
signed 64-bit range without narrowing to a
host int or converting through floating point.
For every finite binary64 float leaf f, implementations MUST use the
algorithm below. All rounding in this algorithm MUST be mathematical
round to nearest, ties to even, independently of the caller's locale or
floating point rounding mode. This spelling differs from
canonical JSON. A host default
conversion, fixed 17-digit format, or unconstrained shortest-output
algorithm MUST NOT replace these rules.
If f is zero, emit 0.0 for positive zero or -0.0 for negative zero
and stop. Rendering MUST preserve the stored sign. Reading declarations
already apply default offset addition;
let, captures, and supplied float parameters can retain negative zero.
Let m be the exact magnitude of f. If 1 ≤ m < 100000000000000000,
let the initial precision p0 be the number of decimal digits in the
integer part of m. Otherwise let p0 = 1. This digit count MUST use exact
comparisons, without a log10 approximation.
For p = p0 through 17 in increasing order, round the exact m to p
significant decimal digits. On an exact tie, choose the decimal with
an even last retained digit. Convert that decimal to binary64 using
round to nearest, ties to even. Select the first p whose conversion
equals m; at p = 17 select its rounded decimal in any event. Subsequent
steps use that p and that rounded decimal.
Let e be the rounded decimal's normalized base-10 exponent, after any
rounding carry: its magnitude is at least 10^e and less than 10^(e+1).
Use scientific notation exactly when e < -4 or e ≥ p. It MUST have one
leading digit, a decimal point only when fractional digits remain,
lowercase e, an explicit + or - exponent sign, and at least two
exponent digits, padding with leading zeros only to reach two digits.
Examples are 1e-05, 1e+17, and 1e+100.
Otherwise use fixed decimal notation with all necessary integer digits,
a leading 0 before a fractional decimal point, and no exponent.
In either notation, remove insignificant fractional trailing zeros and
an unnecessary decimal point. Significant integer zeros MUST remain.
Prepend - exactly when f is negative. If the text contains neither
. nor e, append .0. Thus 20.0, 1000.0, and
10000000000000000.0 retain fixed integral-float spelling; 1e+17
receives no .0.
This is an increasing-precision round-trip search beginning at p0, rather
than a global search for the shortest text. Even when an integral float
has a shorter scientific spelling, its integer-digit starting precision
can require fixed notation.
Iris-only correction; the pinned Gecode reference emits empty text for
float leaves with 99999999999999600 ≤ |f| < 100000000000000000, as recorded
in appendix C.4.
The algorithm above renders every one of those 25 positive values and
its negative with p = 17 in fixed notation plus .0. The following
expected bytes follow that algorithm, independently checked with exact
decimal arithmetic; they are not the pinned reference's output.
id: dzn-float-precision-gap
operation: dzn
--- spec
let below=99999999999999584.0
let edge=99999999999999600.0
let negative=-99999999999999984.0
let above=1e17
values[2]:float
--- input
99999999999999984.01
--- expected dzn
below =99999999999999584.0;
edge =99999999999999600.0;
negative =-99999999999999984.0;
above =1e+17;
values = [99999999999999984.0, 1.0];
B.4 String quoting and UTF-8 bytes
Every string leaf, including an empty string, MUST be enclosed in ASCII
double quotes. Implementations MUST process its UTF-8 encoding bytes in
order, without normalization, using this table. Byte values are hexadecimal.
Byte
Output bytes
22 (double quote)
Backslash followed by double quote: \"
5c (backslash)
Two backslashes: \\
0a (LF)
Backslash followed by n: \n
09 (tab)
Backslash followed by t: \t
Every other byte 00 through 1f
\xhh, with exactly two lowercase hexadecimal digits for the byte
All remaining bytes
The byte itself
Consequently CR is \x0d, backspace \x08, form feed \x0c, NUL
\x00, and ESC \x1b. Implementations MUST NOT substitute JSON \u
escapes or named \r, \b, or \f escapes. DEL (7f), slash,
apostrophe, and every non-ASCII UTF-8 byte remain literal. This includes
U+0085 and combining sequences. String validity continues to follow
§3.6 and
appendix C.
id: dzn-string-bytes
operation: dzn
--- spec
let empty=""let escaped="a\nb\tc\\d\"e" payload:rest
An array MUST be treated as rectangular exactly when, separately at each
array level, all existing arrays at that level have the same length.
The comparison MUST include arrays under different parents, not just
siblings. A level with no existing arrays satisfies this condition.
Rectangular entries of depth 1 through 6 MUST use this section's
representation, regardless of which statements created them.
For each level, its extent MUST be the length of its first existing array,
or 0 when no array exists there. Extents MUST come from the resulting
data, not saved reader-spec dimensions. Thus [0][3] has output extents
0,0; [2][0][9] has 2,0,0. Implementations MUST NOT invent dimensions
below an empty array.
A depth-1 array MUST use [ followed by its scalar leaves separated by
exactly comma-space, then ], without a trailing comma. Empty int, float,
and string vectors MUST all render [].
A depth-2 array with positive row and column extents MUST use matrix
syntax: start with [| , separate leaves within a row with , , start
each subsequent row with LF followed by two spaces and | , then end with
|]. There MUST NOT be a leading newline or an extra row separator.
One-row and one-column matrices MUST use the same rule.
Empty depth-2 arrays and all rectangular arrays at depths 3 through 6
MUST use arrayNd(1..s1, 1..s2, ..., [LEAVES]), replacing N with the
entry's decimal depth and each si with its level's extent, using §B.2's
integer spelling. There MUST be comma-space after each index set. LEAVES MUST be the row-major
flattened leaves, with the last level varying fastest, separated by
comma-space without a trailing comma. Empty index sets MUST be 1..0;
an empty leaf list MUST be []. No B.5 array receives a type comment.
id: dzn-rectangular-arrays
operation: dzn
--- spec
words[2]:word matrix[2][2]:float
three[2][1][2]:int four[1][1][1][2]:int
five[1][1][1][1][2]:int six[1][1][1][1][1][2]:int
--- input no-final-newline
hi there 12.53412345678910
--- expected dzn
words = ["hi", "there"];
matrix = [|1.0, 2.5
|3.0, 4.0|];
three =array3d(1..2, 1..1, 1..2, [1, 2, 3, 4]);
four =array4d(1..1, 1..1, 1..1, 1..2, [5, 6]);
five =array5d(1..1, 1..1, 1..1, 1..1, 1..2, [7, 8]);
six =array6d(1..1, 1..1, 1..1, 1..1, 1..1, 1..2, [9, 10]);
The last entry below uses the depth-greater-than-6 rule in §B.6.
six =array6d(1..1, 1..0, 1..0, 1..0, 1..0, 1..0, []);
% seven: array[int] of tuple(array[int] of tuple(array[int] of tuple(array[int] of tuple(array[int] of tuple(array[int] of tuple(array[int] of int))))))
seven = [];
B.6 Ragged and deeper arrays
Every nonrectangular array entry and every array entry of depth greater than 6
MUST use the nested one-tuple representation below, even when a deep array
is rectangular or empty. This choice MUST apply to the entire entry;
a rectangular subarray within a ragged entry MUST NOT independently use
matrix syntax.
Define the type string T1 as array[int] of TYPE, where TYPE is exactly
int, float, or string according to the entry's value type. Define
T(k+1) as array[int] of tuple( followed by Tk and ). A depth-d entry
MUST emit % NAME: Td followed by LF immediately before its assignment,
substituting its original unquoted name for NAME and its type string for
Td. A quoted assignment name MUST still be unquoted in the comment.
Each actual array MUST render as [ followed by comma-space-separated
items and ], without a trailing comma. At the last array level, items
MUST be scalar leaves rendered under §§B.2–B.4. At every higher level,
each child array MUST render recursively, wrapped as ( followed by
CHILD and ,). Thus a child [5] becomes ([5],) and an empty child
becomes ([],). Higher levels repeat the wrapping. Implementations MUST
NOT insert line breaks or indentation inside this value. Every existing
empty array remains []; nonexistent descendants MUST NOT be created.
For a completely empty deep entry, only the comment retains its type and
depth.
% nested: array[int] of tuple(array[int] of tuple(array[int] of int))
nested = [([([7],)],), ([([8, 9],), ([],)],)];
% deep: array[int] of tuple(array[int] of tuple(array[int] of tuple(array[int] of tuple(array[int] of tuple(array[int] of tuple(array[int] of int))))))
deep = [([([([([([([5],)],)],)],)],)],)];
B.7 Catalog data and executable examples
Successful catalog data MUST render using the same entry, scalar, and
array rules as read data. §9.6
continues to define its entries and their order: scalar instances,
optional string vector name, then optional string vector failed.
Each failed element MUST retain the entire exact summary required there,
including the four summary templates and reader-spec line number.
Implementations MUST apply §B.4 to these data strings, including embedded
quotes, backslashes, LF, tabs, and controls; they MUST NOT localize or
reword them or convert them into error documents. A valid instance's
empty summary MUST remain "".
Under §2.3, a catalog
example with expected dzn MUST catalog the input, then render the
returned data. A catalog example with expected data retains its
canonical JSON result. The expected part chooses the representation;
it does not change which operation constructs the data. The dzn
operation continues to mean read-then-render under §B.1. This notation
defines no command-line option combination.
id: dzn-catalog-summaries
operation: catalog
--- spec
instances {
sections {
"NAME {name}"optional
"X {x:int}"
"END"last
}
check!defined(x)||x>0"positive"
check!defined(x)||(x!=0&& x!=2)
}
--- input
NAME a
X 0
END
NAME b
NAME c
X 1
END
NAME d
END
NAME e
X 2
END
NAME f
X 3
END
--- expected dzn
instances=5;
name = ["a", "c", "d", "e", "f"];
failed = ["positive", "a second line matching \"NAME {name}\"", "no line matching \"X {x:int}\"", "check on line 8 of the spec", ""];
B.8 Separators, line endings, and errors
Each assignment MUST consist of its rendered name, exactly =, its
rendered value, exactly ;, then one LF. A B.6 type comment MUST immediately
precede its assignment; a B.5 matrix MUST contain the internal LFs defined
there. Output MUST NOT contain blank lines between entries, a BOM, CR LF
conversion, tab indentation, or an additional final newline. Nonempty data
ends in exactly the LF terminating its last assignment. Zero entries MUST
produce zero bytes, with no final LF.
In executable examples,
a literal expected dzn part includes its final LF. An empty expected
part represents zero bytes. hex makes controls, CR, DEL, and other
visually ambiguous bytes explicit; no-final-newline on an input part
removes that input's final LF. It MUST NOT remove the required LF from a
nonempty expected dzn result.
The following read succeeds exactly at the idle-work limit and renders
zero bytes.
id: dzn-empty-data
operation: dzn
--- spec
repeat1048576 {}
--- input
--- expected dzn
Rendering introduces no new language error code. Failures
of the preceding read or catalog MUST follow §11.2
and prevent a successful dzn document. Catalog rejection summaries remain
data under §B.7. Host output-stream or I/O failures and allocation failures
remain outside language errors under §11.7.
You are visitor 01402520 — GeezerVison does not store the pages you look up. Best viewed with Netscape Navigator 4.7 or Internet Explorer 6 at 800×600. No cookies required.