this repo has no description
dekker.one
1.. _ch-fzn-interfacing:
2
3Interfacing Solvers to Flatzinc
4===============================
5
6This document describes the interface between the MiniZinc system and FlatZinc solvers.
7
8.. _ch-fzn-spec:
9
10Specification of FlatZinc
11-------------------------
12
13This document is the specification of the FlatZinc modelling language.
14It also includes a definition of the standard command line options a FlatZinc solver should support
15in order to work with the ``minizinc`` driver program (and the MiniZinc IDE).
16
17FlatZinc is the target constraint modelling language into which MiniZinc
18models are translated.
19It is a very simple solver independent problem specification language,
20requiring minimal implementation effort to support.
21
22Throughout this document: :math:`r_1`, :math:`r_2` denote float literals; :math:`x_1, x_2, \dots, x_k, i, j, k` denote int literals; :math:`y_1, y_2, \dots, y_k, y_i` denote literal array elements.
23
24Comments
25~~~~~~~~
26
27Comments start with a percent sign ``%`` and extend to the end of the line. Comments can appear anywhere in a model.
28
29Types
30~~~~~
31
32There are three varieties of types in FlatZinc.
33
34- *Parameter* types apply to fixed values that are specified directly in the model.
35- *Variable* types apply to values computed by the solver during search. Every parameter type has a corresponding variable type; the variable type being distinguished by a ``var`` keyword.
36- *Annotations* and *strings*: annotations can appear on variable declarations, constraints, and on the solve goal. They provide information about how a variable or constraint should be treated by the solver (e.g., whether a variable should be output as part of the result or whether a particular constraint should implemented using domain consistency). Strings may appear as arguments to annotations, but nowhere else.
37
38Parameter types
39+++++++++++++++
40
41Parameters are fixed quantities explicitly specified in the model
42(see rule :mzndef:`<par-type>` in :numref:`ch-fzn-syntax`).
43
44============================================ ===========================
45Type Values
46============================================ ===========================
47``bool`` ``true`` or ``false``
48``float`` float
49``int`` int
50``set of int`` subset of int
51``array [1..`` :math:`n` ``] of bool`` array of bools
52``array [1..`` :math:`n` ``] of float`` array of floats
53``array [1..`` :math:`n` ``] of int`` array of ints
54``array [1..`` :math:`n` ``] of set of int`` array of sets of ints
55============================================ ===========================
56
57A parameter may be used where a variable is expected, but not vice versa.
58
59In predicate declarations the following additional parameter types are allowed.
60
61=================================================================================== ===========================
62Type Values
63=================================================================================== ===========================
64:math:`r_a` ``..`` :math:`r_b` bounded float
65:math:`x_a` ``..`` :math:`x_b` int in range
66``{`` :math:`x_a, x_b, \ldots, x_k` ``}`` int in set
67``set of`` :math:`x_a` ``..`` :math:`x_b` subset of int range
68``set of`` ``{`` :math:`x_a, x_b, \ldots, x_k` ``}`` subset of int set
69``array [1..`` :math:`n` ``] of`` :math:`r_a` ``..`` :math:`r_b` array of floats in range
70``array [1..`` :math:`n` ``] of`` :math:`x_a` ``..`` :math:`x_b` array of ints in range
71``array [1..`` :math:`n` ``] of set of`` :math:`x_a` ``..`` :math:`x_b` array of sets of ints in range
72``array [1..`` :math:`n` ``] of set of`` ``{`` :math:`x_a, x_b, \ldots, x_k` ``}`` array of subsets of set
73=================================================================================== ===========================
74
75A range :math:`x_a` ``..`` :math:`x_b` denotes a closed interval
76:math:`\{x | x_a \leq x \leq x_b\}` (same for float ranges).
77
78An array type appearing in a predicate declaration may use just
79``int`` instead of ``1..`` :math:`n` for the array index range
80in cases where the array argument can be of any length.
81
82Variable types
83++++++++++++++
84
85Variables are quantities decided by the solver
86(see rules :mzndef:`<basic-var-type>` and :mzndef:`<array-var-type>` in :numref:`ch-fzn-syntax`).
87
88+-----------------------------------------------------------------------------------+
89| Variable type |
90+===================================================================================+
91|``var bool`` |
92+-----------------------------------------------------------------------------------+
93|``var float`` |
94+-----------------------------------------------------------------------------------+
95|``var`` :math:`r_a` ``..`` :math:`r_b` |
96+-----------------------------------------------------------------------------------+
97|``var int`` |
98+-----------------------------------------------------------------------------------+
99|``var`` :math:`x_a` ``..`` :math:`x_b` |
100+-----------------------------------------------------------------------------------+
101|``var`` ``{`` :math:`x_a, x_b, \ldots, x_k` ``}`` |
102+-----------------------------------------------------------------------------------+
103|``var set of`` :math:`x_a` ``..`` :math:`x_b` |
104+-----------------------------------------------------------------------------------+
105|``var set of {`` :math:`x_a, x_b, \ldots, x_k` ``}`` |
106+-----------------------------------------------------------------------------------+
107|``array [1..`` :math:`n` ``] of var bool`` |
108+-----------------------------------------------------------------------------------+
109|``array [1..`` :math:`n` ``] of var float`` |
110+-----------------------------------------------------------------------------------+
111|``array [1..`` :math:`n` ``] of var`` :math:`r_a` ``..`` :math:`r_b` |
112+-----------------------------------------------------------------------------------+
113|``array [1..`` :math:`n` ``] of var int`` |
114+-----------------------------------------------------------------------------------+
115|``array [1..`` :math:`n` ``] of var`` :math:`x_a` ``..`` :math:`x_b` |
116+-----------------------------------------------------------------------------------+
117|``array [1..`` :math:`n` ``] of var set of`` :math:`x_a` ``..`` :math:`x_b` |
118+-----------------------------------------------------------------------------------+
119|``array [1..`` :math:`n` ``] of var set of {`` :math:`x_a, x_b, \ldots, x_k` ``}`` |
120+-----------------------------------------------------------------------------------+
121
122In predicate declarations the following additional variable types are allowed.
123
124+-----------------------------------------------------------------------------------+
125| Variable type |
126+===================================================================================+
127|``var set of int`` |
128+-----------------------------------------------------------------------------------+
129|``array [1..`` :math:`n` ``] of var set of int`` |
130+-----------------------------------------------------------------------------------+
131
132An array type appearing in a predicate declaration may use just
133``int`` instead of ``1..`` :math:`n` for the array index range
134in cases where the array argument can be of any length.
135
136The string type
137+++++++++++++++
138
139String literals and literal arrays of string literals can appear as
140annotation arguments, but not elsewhere.
141Strings have the same syntax as in C programs (namely, they are
142delimited by double quotes and the backslash character is used for
143escape sequences).
144
145Examples:
146
147.. code-block:: minizinc
148
149 "" % The empty string.
150 "Hello."
151 "Hello,\nWorld\t\"quoted!\"" % A string with an embedded newline, tab and quotes.
152
153Values and expressions
154~~~~~~~~~~~~~~~~~~~~~~
155
156(See rule :mzndef:`<expr>` in :numref:`ch-fzn-syntax`)
157
158Examples of literal values:
159
160
161Type Literals
162``bool`` ``true``, ``false``
163``float`` ``2.718``, ``-1.0``, ``3.0e8``
164``int`` ``-42``, ``0``, ``69``
165``set of int`` ``{}``, ``{2, 3, 5}``, ``1..10``
166``arrays`` ``[]``, ``[`` :math:`y_a, \ldots, y_k` ``]``
167
168where each array element :math:`y_i` is either: a non-array literal, or the
169name of a non-array parameter or variable, ``v``. For example:
170
171
172.. code-block:: minizinc
173
174 [1, 2, 3] % Just literals
175 [x, y, z] % x, y, and z are variables or parameters.
176 [x, 3] % Mix of identifiers and literals
177
178:numref:`ch-fzn-syntax` gives the regular expressions specifying the
179syntax for float and int literals.
180
181FlatZinc models
182~~~~~~~~~~~~~~~
183
184A FlatZinc model consists of:
185
186#. zero or more external predicate declarations (i.e., a non-standard predicate that is supported directly by the target solver);
187#. zero or more parameter declarations;
188#. zero or more variable declarations;
189#. zero or more constraints;
190#. a solve goal
191
192in that order.
193
194FlatZinc uses the UTF-8 character set. Non-ASCII characters can only appear in string literals.
195
196FlatZinc syntax is case sensitive (``foo`` and ``Foo`` are different
197names).
198Identifiers start with a letter (``[A-Za-z]``) and are followed by
199any sequence of letters, digits, or underscores (``[A-Za-z0-9_]``).
200Additionally, identifiers of variable or parameter names may start with an underscore.
201Identifiers that correspond to the names of predicates, predicate parameters
202and annotations cannot have leading underscores.
203
204The following keywords are reserved and cannot be used as identifiers:
205``annotation``,
206``any``,
207``array``,
208``bool``,
209``case``,
210``constraint``,
211``diff``,
212``div``,
213``else``,
214``elseif``,
215``endif``,
216``enum``,
217``false``,
218``float``,
219``function``,
220``if``,
221``in``,
222``include``,
223``int``,
224``intersect``,
225``let``,
226``list``,
227``maximize``,
228``minimize``,
229``mod``,
230``not``,
231``of``,
232``satisfy``,
233``subset``,
234``superset``,
235``output``,
236``par``,
237``predicate``,
238``record``,
239``set``,
240``solve``,
241``string``,
242``symdiff``,
243``test``,
244``then``,
245``true``,
246``tuple``,
247``union``,
248``type``,
249``var``,
250``where``,
251``xor``.
252Note that some of these keywords are not used in FlatZinc.
253They are reserved because they are keywords in Zinc and MiniZinc.
254
255FlatZinc syntax is insensitive to whitespace.
256
257Predicate declarations
258~~~~~~~~~~~~~~~~~~~~~~
259
260(See rule :mzndef:`<predicate-item>` in :numref:`ch-fzn-syntax`)
261
262Predicates used in the model that are not standard FlatZinc must be
263declared at the top of a FlatZinc model, before any other lexical items.
264Predicate declarations take the form
265
266.. literalinclude:: fzn-grammar.mzn
267 :language: minizincdef
268 :start-after: % Predicate items
269 :end-before: %
270
271Annotations are not permitted anywhere in predicate declarations.
272
273It is illegal to supply more than one predicate declaration for a given
274:mzndef:`<identifier>`.
275
276Examples:
277
278.. code-block:: minizinc
279
280 % m is the median value of {x, y, z}.
281 %
282 predicate median_of_3(var int: x, var int: y, var int: z, var int: m);
283
284 % all_different([x1, .., xn]) iff
285 % for all i, j in 1..n: xi != xj.
286 %
287 predicate all_different(array [int] of var int: xs);
288
289 % exactly_one([x1, .., xn]) iff
290 % there exists an i in 1..n: xi = true
291 % and for all j in 1..n: j != i -> xj = false.
292 %
293 predicate exactly_one(array [int] of var bool: xs);
294
295
296Parameter declarations
297~~~~~~~~~~~~~~~~~~~~~~
298
299(See rule ``param_decl`` in :numref:`ch-fzn-syntax`)
300
301Parameters have fixed values and must be assigned values:
302
303.. literalinclude:: fzn-grammar.mzn
304 :language: minizincdef
305 :start-after: % Parameter declarations
306 :end-before: %
307
308where :mzndef:`<par-type>` is a parameter type, :mzndef:`<var-par-identifier>` is an identifier,
309and :mzndef:`<par-expr>` is a literal value (either a basic integer, float or bool literal, or a set or array of such literals).
310
311Annotations are not permitted anywhere in parameter declarations.
312
313Examples:
314
315.. code-block:: minizinc
316
317 float: pi = 3.141;
318 array [1..7] of int: fib = [1, 1, 2, 3, 5, 8, 13];
319 bool: beer_is_good = true;
320
321Variable declarations
322~~~~~~~~~~~~~~~~~~~~~
323
324(See rule ``var_decl`` in :numref:`ch-fzn-syntax`)
325
326Variables have variable types and can be declared with optional assignments.
327The assignment can fix a variable to a literal value, or create an alias to another
328variable. Arrays of variables always have an assignment, defining them in terms of an array literal
329that can contain identifiers of variables or constant literals.
330Variables may be declared with zero or more annotations.
331
332.. literalinclude:: fzn-grammar.mzn
333 :language: minizincdef
334 :start-after: % Variable declarations
335 :end-before: %
336
337where :mzndef:`<basic-var-type>` and :mzndef:`<array-var-type>` are variable types, :mzndef:`<var-par-identifier>` is an identifier,
338:mzndef:`<annotations>` is a (possibly empty) set of annotations, :mzndef:`<basic-expr>` is an identifier or a literal, and :mzndef:`<array-literal>` is a literal array
339value.
340
341Examples:
342
343.. code-block:: minizinc
344
345 var 0..9: digit;
346 var bool: b;
347 var set of 1..3: s;
348 var 0.0..1.0: x;
349 var int: y :: mip; % 'mip' annotation: y should be a MIP variable.
350 array [1..3] of var 1..10: b = [y, 3, digit];
351
352
353Constraints
354~~~~~~~~~~~
355
356(See rule :mzndef:`<constraint-item>` in :numref:`ch-fzn-syntax`)
357
358Constraints take the following form and may include zero or more annotations:
359
360
361.. literalinclude:: fzn-grammar.mzn
362 :language: minizincdef
363 :start-after: % Constraint items
364 :end-before: %
365
366The arguments expressions (:mzndef:`<expr>`) can be literal values or identifiers.
367
368Examples:
369
370.. code-block:: minizinc
371
372 constraint int_le(0, x); % 0 <= x
373 constraint int_lt(x, y); % x < y
374 constraint int_le(y, 10); % y <= 10
375 % 'domain': use domain consistency for this constraint:
376 % 2x + 3y = 10
377 constraint int_lin_eq([2, 3], [x, y], 10) :: domain;
378
379Solve item
380~~~~~~~~~~
381
382(See rule :mzndef:`<solve-item>` in :numref:`ch-fzn-syntax`)
383
384A model finishes with a solve item, taking one of the following forms:
385
386.. literalinclude:: fzn-grammar.mzn
387 :language: minizincdef
388 :start-after: % Solve item
389 :end-before: %
390
391The first alternative searches for any satisfying assignment, the second one searches for an assignment minimizing the given expression, and the third one for an assignment maximizing the expression. The :mzndef:`<basic-expr>` can be either a variable identifier or a literal value (if the objective function is constant).
392
393A solution consists of a complete assignment where all variables in the
394model have been given a fixed value.
395
396Examples:
397
398
399.. code-block:: minizinc
400
401 solve satisfy; % Find any solution using the default strategy.
402
403 solve minimize w; % Find a solution minimizing w, using the default strategy.
404
405 % First label the variables in xs in the order x[1], x[2], ...
406 % trying values in ascending order.
407 solve :: int_search(xs, input_order, indomain_min, complete)
408 satisfy; % Find any solution.
409
410 % First use first-fail on these variables, splitting domains
411 % at each choice point.
412 solve :: int_search([x, y, z], first_fail, indomain_split, complete)
413 maximize x; % Find a solution maximizing x.
414
415Annotations
416~~~~~~~~~~~
417
418Annotations are optional suggestions to the solver concerning how
419individual variables and constraints should be handled (e.g., a
420particular solver may have multiple representations for int variables)
421and how search should proceed.
422An implementation is free to ignore any annotations it does not
423recognise, although it should print a warning on the standard error
424stream if it does so.
425Annotations are unordered and idempotent: annotations can be reordered
426and duplicates can be removed without changing the meaning of the
427annotations.
428
429
430An annotation is prefixed by ``::``, and either just an identifier or an expression that looks like a predicate call:
431
432.. literalinclude:: fzn-grammar.mzn
433 :language: minizincdef
434 :start-after: % Annotations
435 :end-before: %
436
437The arguments of the second alternative can be any expression or other annotations (without the leading ``::``).
438
439Search annotations
440++++++++++++++++++
441
442While an implementation is free to ignore any or all annotations in a
443model, it is recommended that implementations at least recognise the
444following standard annotations for solve items.
445
446.. code-block:: minizincdef
447
448 seq_search([<searchannotation>, ...])
449
450allows more than one search annotation to be specified in a particular
451order (otherwise annotations can be handled in any order).
452
453A :mzndef:`<searchannotation>` is one of the following:
454
455.. code-block:: minizincdef
456
457 int_search(<vars>, <varchoiceannotation>, <assignmentannotation>, <strategyannotation>)
458
459 bool_search(<vars>, <varchoiceannotation>, <assignmentannotation>, <strategyannotation>)
460
461 set_search(<vars>, <varchoiceannotation>, <assignmentannotation>, <strategyannotation>)
462
463where :mzndef:`<vars>` is the identifier of an array variable or an array literal specifying
464the variables to be assigned (ints, bools, or sets respectively). Note that these arrays may contain literal values.
465
466:mzndef:`<varchoiceannotation>` specifies how the next variable to be assigned is
467chosen at each choice point.
468Possible choices are as follows (it is recommended that implementations
469support the starred options):
470
471+-----------------------+---------------+------------------------------------------------------------------------------------------------------+
472| ``input_order`` | :math:`\star` | Choose variables in the order they appear in :mzndef:`vars`. |
473+-----------------------+---------------+------------------------------------------------------------------------------------------------------+
474| ``first_fail`` | :math:`\star` | Choose the variable with the smallest domain. |
475+-----------------------+---------------+------------------------------------------------------------------------------------------------------+
476| ``anti_first_fail`` | | Choose the variable with the largest domain. |
477+-----------------------+---------------+------------------------------------------------------------------------------------------------------+
478| ``smallest`` | | Choose the variable with the smallest value in its domain. |
479+-----------------------+---------------+------------------------------------------------------------------------------------------------------+
480| ``largest`` | | Choose the variable with the largest value in its domain. |
481+-----------------------+---------------+------------------------------------------------------------------------------------------------------+
482| ``occurrence`` | | Choose the variable with the largest number of attached constraints. |
483+-----------------------+---------------+------------------------------------------------------------------------------------------------------+
484| ``most_constrained`` | | Choose the variable with the smallest domain, breaking ties using the number of constraints. |
485+-----------------------+---------------+------------------------------------------------------------------------------------------------------+
486| ``max_regret`` | | Choose the variable with the largest difference between the two smallest values in its domain. |
487+-----------------------+---------------+------------------------------------------------------------------------------------------------------+
488| ``dom_w_deg`` | | Choose the variable with the smallest value of domain size divided by weighted degree, |
489| | | where the weighted degree is the number of times the variables been in a constraint which failed |
490+-----------------------+---------------+------------------------------------------------------------------------------------------------------+
491
492:mzndef:`<assignmentannotation>` specifies how the chosen variable should be
493constrained.
494Possible choices are as follows (it is recommended that implementations
495support at least the starred options):
496
497+---------------------------+---------------+------------------------------------------------------------------------------------------------------+
498| ``indomain_min`` | :math:`\star` | Assign the smallest value in the variable's domain. |
499+---------------------------+---------------+------------------------------------------------------------------------------------------------------+
500| ``indomain_max`` | :math:`\star` | Assign the largest value in the variable's domain. |
501+---------------------------+---------------+------------------------------------------------------------------------------------------------------+
502| ``indomain_middle`` | | Assign the value in the variable's domain closest to the mean of its current bounds. |
503+---------------------------+---------------+------------------------------------------------------------------------------------------------------+
504| ``indomain_median`` | | Assign the middle value in the variable's domain. |
505+---------------------------+---------------+------------------------------------------------------------------------------------------------------+
506| ``indomain`` | | Nondeterministically assign values to the variable in ascending order. |
507+---------------------------+---------------+------------------------------------------------------------------------------------------------------+
508| ``indomain_random`` | | Assign a random value from the variable's domain. |
509+---------------------------+---------------+------------------------------------------------------------------------------------------------------+
510| ``indomain_split`` | | Bisect the variable's domain, excluding the upper half first. |
511+---------------------------+---------------+------------------------------------------------------------------------------------------------------+
512| ``indomain_reverse_split``| | Bisect the variable's domain, excluding the lower half first. |
513+---------------------------+---------------+------------------------------------------------------------------------------------------------------+
514| ``indomain_interval`` | | If the variable's domain consists of several contiguous intervals, |
515| | | reduce the domain to the first interval. Otherwise just split the variable's domain. |
516+---------------------------+---------------+------------------------------------------------------------------------------------------------------+
517
518Of course, not all assignment strategies make sense for all search
519annotations (e.g., ``bool_search`` and ``indomain_split``).
520
521Finally, :mzndef:`<strategyannotation>` specifies a search strategy;
522implementations should at least support ``complete`` (i.e., exhaustive
523search).
524
525Output annotations
526++++++++++++++++++
527
528Model output is specified through variable annotations.
529Non-array output variables are annotated with
530``output_var``.
531Array output variables are annotated with
532``output_array([`` :math:`x_1` ``..`` :math:`x_2` ``, ... ])``
533where :math:`x_1` ``..`` :math:`x_2` ``, ...`` are the index set ranges of the
534original MiniZinc array (which
535may have had multiple dimensions and/or index sets that do not start at
5361). See :numref:`ch-fzn-output` for details on the output format.
537
538Variable definition annotations
539+++++++++++++++++++++++++++++++
540
541To support solvers capable of exploiting functional relationships, a
542variable defined as a function of other variables may be annotated thus:
543
544.. code-block:: minizinc
545
546 var int: x :: is_defined_var;
547
548 ...
549
550 constraint int_plus(y, z, x) :: defines_var(x);
551
552(The ``defines_var`` annotation should appear on exactly one
553constraint.)
554This allows a solver to represent ``x`` internally as a representation
555of ``y+z`` rather than as a separate constrained variable.
556The ``is_defined_var`` annotation on the declaration of ``x``
557provides "early warning" to the solver that such an option is
558available.
559
560Intermediate variables
561++++++++++++++++++++++
562
563Intermediate variables introduced during conversion of a MiniZinc
564model to FlatZinc may be annotated thus:
565
566.. code-block:: minizinc
567
568 var int: X_INTRODUCED_3 :: var_is_introduced;
569
570This information is potentially useful to the solver's search strategy.
571
572Constraint annotations
573++++++++++++++++++++++
574
575Annotations can be placed on constraints advising the solver how the
576constraint should be implemented.
577Here are some constraint annotations supported by some solvers:
578
579
580+---------------------------+----------------------------------------------------------------------------+
581| ``bounds`` or ``boundsZ`` | Use integer bounds propagation. |
582+---------------------------+----------------------------------------------------------------------------+
583| ``boundsR`` | Use real bounds propagation. |
584+---------------------------+----------------------------------------------------------------------------+
585| ``boundsD`` | A tighter version of ``boundsZ`` where support for the bounds must exist. |
586+---------------------------+----------------------------------------------------------------------------+
587| ``domain`` | Use domain propagation. |
588+---------------------------+----------------------------------------------------------------------------+
589|``priority(k)`` | where ``k`` is an integer constant indicating propagator priority. |
590+---------------------------+----------------------------------------------------------------------------+
591
592.. _ch-fzn-output:
593
594Output
595------
596
597An implementation can produce three types of output: solutions, statistics, and errors.
598
599Solution output
600~~~~~~~~~~~~~~~
601
602An implementation must output values for all and only the variables
603annotated with ``output_var`` or ``output_array`` (output
604annotations must not appear on parameters). Output must be printed to
605the standard output stream.
606
607For example:
608
609.. code-block:: minizinc
610
611 var 1..10: x :: output_var;
612 var 1..10: y; % y is not output.
613 % Output zs as a "flat" representation of a 2D array:
614 array [1..4] of var int: zs :: output_array([1..2, 1..2]);
615
616All non-error output must be sent to the standard output stream.
617
618Output must take the following form:
619
620.. code-block:: minizincdef
621
622 <var-par-identifier> = <basic-literal-expr> ;
623
624or, for array variables,
625
626.. code-block:: minizincdef
627
628 <var-par-identifier> = array<N>d(<a>..<b>, ..., [<y1>, <y2>, ... <yk>]);
629
630where :mzndef:`<N>` is the number of index sets specified in the
631corresponding :mzndef:`output_array` annotation,
632:mzndef:`<a>..<b>, ...` are the index set ranges,
633and :mzndef:`<y1>, <y2>, ... <yk>` are literals of the element type.
634
635Using this format, the output of a FlatZinc model solution is
636suitable for input to a MiniZinc model as a data file (this is why
637parameters are not included in the output).
638
639Implementations must ensure that *all* model variables (not
640just the output variables) have satisfying assignments before printing a
641solution.
642
643The output for a solution must be terminated with ten consecutive
644minus signs on a separate line: ``----------``.
645
646Multiple solutions may be output, one after the other, as search
647proceeds. How many solutions should be output depends on the mode the solver is run in as controlled by the ``-a`` command line flag (see :numref:`fzn-cmdline-options`).
648
649If at least one solution has been found and search then terminates
650having explored the whole search space, then ten
651consecutive equals signs should be printed on a separate line:
652``==========``.
653
654If no solutions have been found and search terminates having explored
655the whole search space, then ``=====UNSATISFIABLE=====`` should be
656printed on a separate line.
657
658If the objective of an optimization problem is unbounded, then
659``=====UNBOUNDED=====`` should be printed on a separate line.
660
661If no solutions have been found and search terminates having
662*not* explored the whole search space, then
663``=====UNKNOWN=====`` should be printed on a separate line.
664
665Implementations may output further information about the solution(s),
666or lack thereof, in the form of FlatZinc comments.
667
668Examples:
669
670Asking for a single solution to this model:
671
672.. code-block:: minizinc
673
674 var 1..3: x :: output_var;
675 solve satisfy
676
677might produce this output:
678
679.. code-block:: minizinc
680
681 x = 1;
682 ----------
683
684Asking for all solutions to this model:
685
686.. code-block:: minizinc
687
688 array [1..2] of var 1..3: xs :: output_array([1..2]);
689 constraint int_lt(xs[1], xs[2]); % x[1] < x[2].
690 solve satisfy
691
692might produce this output:
693
694.. code-block:: minizinc
695
696 xs = array1d(1..2, [1, 2]);
697 ----------
698 xs = array1d(1..2, [1, 3]);
699 ----------
700 xs = array1d(1..2, [2, 3]);
701 ----------
702 ==========
703
704
705Asking for a single solution to this model:
706
707.. code-block:: minizinc
708
709 var 1..10: x :: output_var;
710 solve maximize x;
711
712should produce this output:
713
714.. code-block:: minizinc
715
716 x = 10;
717 ----------
718 ==========
719
720The row of equals signs indicates that a complete search was performed
721and that the last result printed is the optimal solution.
722
723Running a solver on this model with some termination condition (such as a very short time-out):
724
725.. code-block:: minizinc
726
727 var 1..10: x :: output_var;
728 solve maximize x;
729
730might produce this output:
731
732.. code-block:: minizinc
733
734 x = 1;
735 ----------
736 x = 2;
737 ----------
738 x = 3;
739 ----------
740
741Because the output does not finish with ``==========``, search did not
742finish, hence these results must be interpreted as approximate solutions
743to the optimization problem.
744
745Asking for a solution to this model:
746
747.. code-block:: minizinc
748
749 var 1..3: x :: output_var;
750 var 4..6: y :: output_var;
751 constraint int_lt(y, x); % y < x.
752 solve satisfy;
753
754should produce this output:
755
756.. code-block:: minizinc
757
758 =====UNSATISFIABLE=====
759
760indicating that a complete search was performed and no solutions were
761found (i.e., the problem is unsatisfiable).
762
763Statistics output
764~~~~~~~~~~~~~~~~~
765
766FlatZinc solvers can output statistics in a standard format so that it can be read by scripts,
767for example, in order to run experiments and automatically aggregate the results.
768Statistics should be printed to the standard output stream in the form of FlatZinc comments that follow a specific format.
769Statistics can be output at any time during the solving, i.e., before the first solution, between solutions,
770and after the search has finished. Statistics output corresponding to a solution should be the last one
771before its '----------' separator.
772
773Each value should be output on a line of its own in the following format:
774
775.. code-block:: minizincdef
776
777 %%%mzn-stat: <name>=<value>
778
779Each block of statistics is terminated by a line of its own with the following format:
780
781.. code-block:: minizincdef
782
783 %%%mzn-stat-end
784
785**Example**
786
787.. code-block:: minizincdef
788
789 %%%mzn-stat: objective=1e+308
790 %%%mzn-stat: objectiveBound=0
791 %%%mzn-stat: nodes=0
792 %%%mzn-stat: solveTime=2.3567
793 %%%mzn-stat-end
794
795 (no feasible solution found yet but something can be printed...)
796
797 %%%mzn-stat: objective=12345
798 %%%mzn-stat: objectiveBound=122
799 %%%mzn-stat: nodes=35
800 %%%mzn-stat: solveTime=78.5799
801 %%%mzn-stat-end
802
803 (the corresponding feasible solution with value 12345 goes here
804 or before its statistics but above the separator)
805 ---------- (<- the solution separator)
806
807 %%%mzn-stat: objective=379
808 %%%mzn-stat: objectiveBound=379
809 %%%mzn-stat: nodes=4725
810 %%%mzn-stat: solveTime=178.5799
811 %%%mzn-stat-end
812
813 (the corr. optimal solution with value 379 goes here)
814 ----------
815 ========== (<- the 'search complete' marker)
816
817 %%%mzn-stat: objective=379 (<- this is the concluding output)
818 %%%mzn-stat: objectiveBound=379
819 %%%mzn-stat: nodes=13456
820 %%%mzn-stat: solveTime=2378.5799
821 %%%mzn-stat-end
822
823
824The :mzndef:`<name>` describes the kind of statistics gathered, and the :mzndef:`<value>` can be any value of a MiniZinc type.
825The following names are considered standard statistics:
826
827======================== ====== ================================================
828Name Type Explanation
829======================== ====== ================================================
830``nodes`` int Number of search nodes
831``openNodes`` int Number of open search nodes
832``objective`` float Current objective value
833``objectiveBound`` float Dual bound on the objective value
834``failures`` int Number of leaf nodes that were failed
835``restarts`` int Number of times the solver restarted the search
836``variables`` int Number of variables
837``intVariables`` int Number of integer variables created
838``boolVariables`` int Number of bool variables created
839``floatVariables`` int Number of float variables created
840``setVariables`` int Number of set variables created
841``propagators`` int Number of propagators created
842``propagations`` int Number of propagator invocations
843``peakDepth`` int Peak depth of search tree
844``nogoods`` int Number of nogoods created
845``backjumps`` int Number of backjumps
846``peakMem`` float Peak memory (in Mbytes)
847``initTime`` float Initialisation time (in seconds)
848``solveTime`` float Solving time (in seconds)
849======================== ====== ================================================
850
851Error and warning output
852~~~~~~~~~~~~~~~~~~~~~~~~
853
854Errors and warnings must be output to the standard error stream. When an error occurs, the implementation should exit with a non-zero exit code, signaling failure.
855
856
857.. _ch-solver-specific-libraries:
858
859Solver-specific Libraries
860-------------------------
861
862Constraints in FlatZinc can call standard predicates as well as solver-specific predicates. Standard predicates are the ones that the MiniZinc compiler assumes to be present in all solvers. Without further customisation, the compiler will try to compile the entire model into a set of these standard predicates.
863
864Solvers can use custom predicates and *redefine* standard predicates by supplying a *solver specific library* of predicate declarations. Examples of such libraries can be found in the binary distribution of MiniZinc, inside the ``share/minizinc/gecode`` and ``share/minizinc/chuffed`` directories.
865
866The solver-specific library needs to be made available to the MiniZinc compiler by specifying its location in the solver's configuration file, see :numref:`sec-cmdline-conffiles`.
867
868Standard predicates
869~~~~~~~~~~~~~~~~~~~
870
871FlatZinc solvers need to support the predicates listed as ``FlatZinc builtins`` in the library reference documentation, see :numref:`ch-lib-flatzinc`.
872
873Any standard predicate that is not supported by a solver needs to be *redefined*. This can be achieved by placing a file called ``redefinitions.mzn`` in the solver's MiniZinc library, which can contain alternative definitions of predicates, or define them as unsupported using the ``abort`` predicate.
874
875Example for a ``redefinitions.mzn``:
876
877.. code-block:: minizinc
878
879 % Redefine float_sinh function in terms of exp
880 predicate float_sinh(var float: a, var float: b) =
881 b == (exp(a)-exp(-a))/2.0;
882
883 % Mark float_tanh as unsupported
884 predicate float_tanh(var float: a, var float: b) =
885 abort("The builtin float_tanh is not supported by this solver.");
886
887The redefinition can use the full MiniZinc language. Note, however, that redefining builtin predicates in terms of MiniZinc expressions can lead to problems if the MiniZinc compiler translates the high-level expression back to the redefined builtin.
888
889The reference documentation (:numref:`ch-lib-flatzinc`) also contains sections on builtins that were added in later versions of MiniZinc. In order to maintain backwards compatibility with solvers that don't support these, they are organised in redefinition files with a version number attached, such as ``redefinitions-2.0.mzn``. In order to declare support for these builtins, the solver-specific library must contain the corresponding redefinitions file, with the predicates either redefined in terms of other predicates, or declared as supported natively by the solver by providing a predicate declaration without a body.
890
891Example for a ``redefinitions-2.0.mzn`` that declares native support for the predicates added in MiniZinc 2.0:
892
893.. code-block:: minizinc
894
895 predicate bool_clause_reif(array[int] of var bool: as,
896 array[int] of var bool: bs,
897 var bool: b);
898 predicate array_int_maximum(var int: m, array[int] of var int: x);
899 predicate array_float_maximum(var float: m, array[int] of var float: x);
900 predicate array_int_minimum(var int: m, array[int] of var int: x);
901 predicate array_float_minimum(var float: m, array[int] of var float: x);
902
903
904Solver-specific predicates
905~~~~~~~~~~~~~~~~~~~~~~~~~~
906
907Many solvers have built-in support for some of the constraints in the MiniZinc standard library. But without declaring which constraints they support, MiniZinc will assume that they don't support any except for the standard FlatZinc builtins mentioned in the section above.
908
909A solver can declare that it supports a non-standard constraint by overriding one of the files of the standard library in its own solver-specific library. For example, assume that a solver supports the ``all_different`` constraint on integer variables. In the standard library, this constraint is defined in the file ``fzn_all_different_int.mzn``, with the following implementation:
910
911.. code-block:: minizinc
912
913 predicate fzn_all_different_int(array[int] of var int: x) =
914 forall(i,j in index_set(x) where i < j) ( x[i] != x[j] );
915
916A solver, let's call it *OptiSolve*, that supports this constraint natively can place a file with the same name, ``fzn_all_different_int.mzn``, in its library, and redefine it as follows:
917
918.. code-block:: minizinc
919
920 predicate optisolve_alldifferent(array[int] of var int: x);
921
922 predicate fzn_all_different_int(array[int] of var int: x) =
923 optisolve_alldifferent(x);
924
925When a MiniZinc model that contains the ``all_different`` constraint is now compiled with the *OptiSolve* library, the generated FlatZinc will contain calls to the newly defined predicate ``optisolve_alldifferent``.
926
927**Note:** The solver-specific library has been reorganised for MiniZinc version 2.3.0. Previously, a solver library would contain e.g. the file ``bin_packing.mzn`` in order to override the :mzn:`bin_packing` constraint. With version 2.3.0, this is still possible (in order to maintain backwards compatibility). However, the predicate :mzn:`bin_packing` from file ``bin_packing.mzn`` now delegates to the predicate :mzn:`fzn_bin_packing` in ``fzn_bin_packing.mzn``. This enables the :mzn:`bin_packing` predicate to check that the arguments are correct using assertions, before delegating to the solver-specific predicate. If your solver still uses the old library layout (i.e., overriding ``bin_packing.mzn`` instead of ``fzn_bin_packing.mzn``), you should consider updating it to the new standard.
928
929.. _fzn-half-reif:
930
931Reified and half-reified predicates
932~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
933
934A reified constraint is a constraint that is not simply enforced, but whose truth value is bound to a Boolean variable. For example, a MiniZinc expression :mzn:`var bool: b = all_different(x);` would constrain :mzn:`b` to be true if and only if the variables :mzn:`x` take pairwise different values.
935
936If a predicate is called in such a reified context, the MiniZinc compiler will try to find a version of the predicate with :mzn:`_reif` added to its identifier and an additional :mzn:`var bool` argument. For the above example, the compiler will try to generate the following FlatZinc code:
937
938.. code-block:: minizinc
939
940 var bool: b;
941 constraint all_different_reif(x, b);
942
943If the :mzn:`_reif` predicate does not exist, the compiler will try to use the definition of the original predicate. However, this may not be ideal: the original definition may make use of free variables in a :mzn:`let` expression (which is not allowed in reified contexts), or it may lead to inefficient solving.
944
945Solver libraries should therefore provide reified versions of constraints whenever possible. The library contains files ``fzn_<constraintname>_reif.mzn`` for this purpose.
946
947When a reified constraint is used in a *positive context* (see :numref:`pred-context`), the MiniZinc compiler can use a special version, called a half-reified predicate and identified by an :mzn:`_imp` suffix, instead of the :mzn:`_reif` predicate. Half-reified predicates essentially represent constraints that are *implied* by a Boolean variable rather than being equivalent to one. This typically leads to simpler translations or more efficient propagation (e.g., a half-reified :mzn:`all_different` only needs to *check* whether it is false, but it never has to implement the negation of the actual constraint).
948
949For example, :mzn:`constraint y=0 \/ all_different(x)` might be translated as follows:
950
951.. code-block:: minizinc
952
953 var bool: X_INTRODUCED_1;
954 var bool: X_INTRODUCED_2;
955 constraint int_eq_imp(y,0,X_INTRODUCED_1);
956 constraint all_different_imp(x, X_INTRODUCED_2);
957 constraint array_bool_or([X_INTRODUCED_1,X_INTRODUCED_2]);
958
959MiniZinc will decide whether to use half-reification case by case based on the availability of the :mzn:`_imp` predicate. As for reified constraints, it may be benefitial to provide specialised half-reified versions if the solver supports them.
960
961.. _fzn-cmdline-options:
962
963Command-Line Interface and Standard Options
964-------------------------------------------
965
966In order to work with the ``minizinc`` command line driver, a FlatZinc solver must be an executable (which can include e.g. shell scripts) that can be invoked as follows:
967
968.. code-block:: bash
969
970 $ <executable-name> [options] model.fzn
971
972where ``<executable-name>`` is the name of the executable. Solvers may support the following standard options:
973
974.. option:: -a
975
976 Instructs the solver to report *all* solutions in the case of satisfaction
977 problems, or print *intermediate* solutions of increasing quality in the case
978 of optimisation problems.
979
980.. option:: -n <i>
981
982 Instructs the solver to stop after reporting ``i`` solutions (only used with
983 satisfaction problems).
984
985.. option:: -i
986
987 Instructs the solver to print *intermediate* solutions of increasing quality
988 (only used with optimisation problems). This option should be supported rather
989 than ``-a`` for solvers which only support printing of intermediate solutions
990 for optimisation problems but no reporting of all solutions for satisfaction
991 problems.
992
993.. option:: -f
994
995 Instructs the solver to conduct a "free search", i.e., ignore any search
996 annotations. The solver is not *required* to ignore the annotations, but it
997 is *allowed* to do so.
998
999.. option:: -s
1000
1001 Print statistics during and/or after the search for solutions. Statistics
1002 should be printed as FlatZinc comments to the standard output stream.
1003 See below for a standard format for statistics.
1004
1005.. option:: -v
1006
1007 Print log messages (verbose solving) to the standard error stream. If solvers
1008 choose to print to standard output instead, all messages must be valid
1009 comments (i.e., start with a ``%`` character).
1010
1011.. option:: -p <i>
1012
1013 Run with ``i`` parallel threads (for multi-threaded solvers).
1014
1015.. option:: -r <i>
1016
1017 Use ``i`` as the random seed (for any random number generators the solver
1018 may be using).
1019
1020.. option:: -t <ms>
1021
1022 Wall time limit ``ms`` milliseconds.
1023
1024.. _sec-cmdline-conffiles:
1025
1026Solver Configuration Files
1027--------------------------
1028
1029In order for a solver to be available to MiniZinc, it has to be described in a *solver configuration file*. This is a simple file, in JSON or ``.dzn`` format, that contains some basic information such as the solver's name, version, where its library of global constraints can be found, and a path to its executable.
1030Examples are given in section Solver Backends in User Manual.
1031
1032A solver configuration file must have file extension ``.msc`` (for MiniZinc Solver Configuration), and can be placed in any of the following locations:
1033
1034- In the ``minizinc/solvers/`` directory of the MiniZinc installation. If you install MiniZinc from the binary distribution, this directory can be found at ``/usr/share/minizinc/solvers`` on Linux systems, inside the MiniZincIDE application on macOS system, and in the ``Program Files\MiniZinc IDE (bundled)`` folder on Windows.
1035- In the directory ``$HOME/.minizinc/solvers`` on Linux and macOS systems, and the Application Data directory on Windows systems.
1036- In any directory listed on the ``MZN_SOLVER_PATH`` environment variable (directories are separated by ``:`` on Linux and macOS, and by ``;`` on Windows systems).
1037- In any directory listed in the ``mzn_solver_path`` option of the global or user-specific configuration file (see :numref:`ch-user-config`)
1038- Alternatively, you can use the MiniZinc IDE to create solver configuration files, see :numref:`sec-ide-add-solvers` for details.
1039
1040Solver configuration files must be valid JSON or ``.dzn`` files. As a JSON file, it must be an object with certain fields. As a ``.dzn`` file, it must consist of assignment items.
1041
1042For example, a simple solver configuration in JSON format could look like this:
1043
1044.. code-block:: json
1045
1046 {
1047 "name" : "My Solver",
1048 "version": "1.0",
1049 "id": "org.myorg.my_solver",
1050 "executable": "fzn-mysolver"
1051 }
1052
1053
1054The same configuration in ``.dzn`` format would look like this:
1055
1056.. code-block:: minizinc
1057
1058 name = "My Solver";
1059 version = "1.0";
1060 id = "org.myorg.my_solver";
1061 executable = "fzn-mysolver";
1062
1063Here is a list of all configuration options recognised by the configuration file parser. Any valid configuration file must at least contain the fields ``name``, ``version``, ``id``, and ``executable``.
1064
1065- ``name`` (string, required): The name of the solver (displayed, together with the version, when you call ``minizinc --solvers``, and in the MiniZinc IDE).
1066- ``version`` (string, required): The version of the solver.
1067- ``id`` (string, required): A unique identifier for the solver, "reverse domain name" notation.
1068- ``executable`` (string, required): The executable for this solver that can run FlatZinc files. This can be just a file name (in which case the solver has to be on the current PATH), or an absolute path to the executable, or a relative path (which is interpreted relative to the location of the configuration file).
1069- ``mznlib`` (string, default ``""``): The solver-specific library of global constraints and redefinitions. This should be the name of a directory (either an absolute path or a relative path, interpreted relative to the location of the configuration file). For solvers whose libraries are installed in the same location as the MiniZinc standard library, this can also take the form ``-G<solverlib>``, e.g., ``-Ggecode`` (this is mostly the case for solvers that ship with the MiniZinc binary distribution).
1070- ``tags`` (list of strings, default empty): Each solver can have one or more tags that describe its features in an abstract way. Tags can be used for selecting a solver using the ``--solver`` option. There is no fixed list of tags, however we recommend using the following tags if they match the solver's behaviour:
1071
1072 - ``"cp"``: for Constraint Programming solvers
1073 - ``"mip"``: for Mixed Integer Programming solvers
1074 - ``"float"``: for solvers that support float variables
1075 - ``"api"``: for solvers that use the internal C++ API
1076
1077- ``stdFlags`` (list of strings, default empty): Which of the standard solver command line flags are supported by this solver. The standard flags are ``-a``, ``-n``, ``-i``, ``-s``, ``-v``, ``-p``, ``-r``, ``-f``, ``-t``.
1078- ``extraFlags`` (list of list of strings, default empty): Extra command line flags supported by the solver. Each entry must be a list of four strings. The first string is the name of the option (e.g. ``"--special-algorithm"``). The second string is a description that can be used to generate help output (e.g. ``"which special algorithm to use"``). The third string specifies the type of the argument (``"int"``, ``"bool"``, ``"float"``, ``"string"`` or ``"opt"``). The fourth string is the default value. The following types have an additional extended syntax:
1079
1080 - ``"int:n:m"`` where ``n`` and ``m`` are integers, gives lower and upper bounds for the supported values
1081 - ``"float:n:m"`` where ``n`` and ``m`` are floating point numbers, gives lower and upper bounds for the supported values
1082 - ``"bool:onstring:offstring"`` specifies strings to add to the command line flag to turn it on (``onstring``) and off (``offstring``). E.g., ``["-interrupt","whether to catch Ctrl-C","bool:false:true","true"]`` specifies a command line option that can be called as ``-interrupt true`` or ``-interrupt false``. The standard behaviour (just ``"bool"``) means that the option is either added to the command line or not.
1083 - ``"opt:first option:second option:...:last option"`` specifies a list of possible values for the option
1084
1085- ``supportsMzn`` (bool, default ``false``): Whether the solver can run MiniZinc directly (i.e., it implements its own compilation or interpretation of the model).
1086- ``supportsFzn`` (bool, default ``true``): Whether the solver can run FlatZinc. This should be the case for most solvers
1087- ``needsSolns2Out`` (bool, default ``true``): Whether the output of the solver needs to be passed through the MiniZinc output processor.
1088- ``needsMznExecutable`` (bool, default ``false``): Whether the solver needs to know the location of the MiniZinc executable. If true, it will be passed to the solver using the ``mzn-executable`` option.
1089- ``needsStdlibDir`` (bool, default ``false``): Whether the solver needs to know the location of the MiniZinc standard library directory. If true, it will be passed to the solver using the ``stdlib-dir`` option.
1090- ``isGUIApplication`` (bool, default ``false``): Whether the solver has its own graphical user interface, which means that MiniZinc will detach from the process and not wait for it to finish or to produce any output.
1091
1092.. _ch-fzn-syntax:
1093
1094Grammar
1095-------
1096
1097This is the full grammar for FlatZinc. It is a proper subset of the MiniZinc grammar (see :numref:`spec-grammar`). However, instead of specifying all the cases in the MiniZinc grammar that do *not* apply to FlatZinc, the BNF syntax below contains only the relevant syntactic constructs. It uses the same notation as in :numref:`spec-syntax-notation`.
1098
1099.. literalinclude:: fzn-grammar.mzn
1100 :language: minizincdef