this repo has no description
dekker.one
1.. _ch-cmdline:
2
3The MiniZinc Command Line Tool
4==============================
5
6The core of the MiniZinc constraint modelling system is the ``minizinc`` tool. You can use it directly from the command line, through the MiniZinc IDE, or through a programmatic interface (API). This chapter summarises the options accepted by the tool, and explains how it interacts with target solvers.
7
8Basic Usage
9-----------
10
11The ``minizinc`` tool performs three basic functions: it *compiles* a MiniZinc model (plus instance data), it *runs* an external solver, and it *translates solver output* into the form specified in the model. Most users would use all three functions at the same time. For example, let us assume that we want to solve the following simple problem, given as two files (:download:`model.mzn <examples/command_line/model.mzn>` and :download:`data.dzn <examples/command_line/data.dzn>`):
12
13.. literalinclude:: examples/command_line/model.mzn
14 :language: minizinc
15
16.. literalinclude:: examples/command_line/data.dzn
17 :language: minizinc
18
19To run the model file ``model.mzn`` with data file ``data.dzn`` using the Gecode solver, you can use the following command line:
20
21.. code-block:: bash
22
23 $ minizinc --solver Gecode model.mzn data.dzn
24
25This would result in the output
26
27.. code-block:: none
28
29 The resulting values are [10, 9, 8, 7, 6].
30 ----------
31 ==========
32
33However, each of the three functions can also be accessed individually. For example, to compile the same model and data, use the ``-c`` option:
34
35.. code-block:: bash
36
37 $ minizinc -c --solver Gecode model.mzn data.dzn
38
39This will result in two new files, ``model.fzn`` and ``model.ozn``, being output in the same directory as ``model.mzn``. You could then run a target solver directly on the ``model.fzn`` file, or use ``minizinc``:
40
41.. code-block:: bash
42
43 $ minizinc --solver Gecode model.fzn
44
45You will see that the solver produces output in a standardised form, but not the output prescribed by the output item in the model:
46
47.. code-block:: none
48
49 x = array1d(1..5 ,[10, 9, 8, 7, 6]);
50 ----------
51 ==========
52
53The translation from this output to the form specified in the model is encoded in the ``model.ozn`` file. You can use ``minizinc`` to execute the ``.ozn`` file. In this mode, it reads a stream of solutions from standard input, so we need to pipe the solver output into ``minizinc``:
54
55.. code-block:: bash
56
57 $ minizinc --solver Gecode model.fzn | minizinc --ozn-file model.ozn
58
59These are the most basic command line options that you need in order to compile and run models and translate their output. The next section lists all available command line options in detail. :numref:`sec-cmdline-conffiles` explains how new solvers can be added to the system.
60
61Adding Solvers
62--------------
63
64Solvers that support MiniZinc typically consist of two parts: a solver *executable*, which can be run on the FlatZinc output of the MiniZinc compiler, and a *solver library*, which consists of a set of MiniZinc files that define the constraints that the solver supports natively. This section deals with making existing solvers available to the MiniZinc tool chain. For information on how to add FlatZinc support to a solver, refer to :numref:`ch-fzn-interfacing`.
65
66Configuration files
67~~~~~~~~~~~~~~~~~~~
68
69In order for MiniZinc to be able to find both the solver library and the executable, the solver needs to be described in a *solver configuration file* (see :numref:`sec-cmdline-conffiles` for details). If the solver you want to install comes with a configuration file (which has the file extension ``.msc`` for MiniZinc Solver Configuration), it has to be in one of the following locations:
70
71- 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.
72- In the directory ``$HOME/.minizinc/solvers`` on Linux and macOS systems, and the Application Data directory on Windows systems.
73- In any directory listed on the ``MZN_SOLVER_PATH`` environment variable (directories are separated by ``:`` on Linux and macOS, and by ``;`` on Windows systems).
74- In any directory listed in the ``mzn_solver_path`` option of the global or user-specific configuration file (see :numref:`ch-user-config`)
75- Alternatively, you can use the MiniZinc IDE to create solver configuration files, see :numref:`sec-ide-add-solvers` for details.
76
77After adding a solver, it will be listed in the output of the ``minizinc --solvers`` command.
78
79Configuration for MIP solvers
80~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
81
82Some solvers require additional configuration flags before they can be used. For example, the binary bundle of MiniZinc comes with interfaces to the CPLEX and Gurobi Mixed Integer Programming solvers. However, due to licensing restrictions, the solvers themselves are not part of the bundled release. Depending on where CPLEX or Gurobi is installed on your system, MiniZinc may be able to find the solvers automatically, or it may require an additional option to point it to the shared library.
83
84In case the libraries cannot be found automatically, you can use one of the following:
85
86- CPLEX: Specify the location of the shared library using the ``--cplex-dll`` command line option. On Windows, the library is called ``cplexXXXX.dll`` and typically found in same directory as the ``cplex`` executable. On Linux it is ``libcplexXXX.so``, and on macOS ``libcplexXXXX.jnilib``, where ``XXX`` and ``XXXX`` stand for the version number.
87- Gurobi: The command line option for Gurobi is ``--gurobi-dll``. On Windows, the library is called ``gurobiXX.dll`` (in the same directory as the ``gurobi`` executable), and on Linux and macOS is it ``libgurobiXX.so`` (in the ``lib`` directory of your Gurobi installation).
88- You can define these paths as defaults in your user configuration file, see :numref:`ch-user-config`.
89
90.. _ch-cmdline-options:
91
92Options
93-------
94
95You can get a list of all the options supported by the ``minizinc`` tool using the ``--help`` flag.
96
97General options
98~~~~~~~~~~~~~~~
99
100These options control the general behaviour of the ``minizinc`` tool.
101
102.. option:: --help, -h
103
104 Print a help message.
105
106.. option:: --version
107
108 Print version information.
109
110.. option:: --solvers
111
112 Print list of available solvers.
113
114.. option:: --solver <id>, --solver <solver configuration file>.msc
115
116 Select solver to use. The first form of the command selects one of the
117 solvers known to MiniZinc (that appear in the list of the ``--solvers``
118 command). You can select a solver by name, id, or tag, and add a specific
119 version. For example, to select a mixed-integer programming solver,
120 identified by the ``mip`` tag, you can use ``--solver mip``. To select
121 a specific version of Gurobi (in case you have two versions installed),
122 use ``--solver Gurobi@7.5.2``. Instead of the name you can also use
123 the solver's identifier, e.g. ``--solver org.gecode.gecode``.
124
125 The second form of the command selects the solver from the given
126 configuration file (see :numref:`sec-cmdline-conffiles`).
127
128.. option:: --help <id>
129
130 Print help for a particular solver. The scheme for selecting a solver
131 is the same as for the ``--solver`` option.
132
133.. option:: -v, -l, --verbose
134
135 Print progress/log statements (for both compilation and solver).
136 Note that some solvers may log to stdout.
137
138.. option:: --verbose-compilation
139
140 Print progress/log statements for compilation only.
141
142.. option:: -s, --statistics
143
144 Print statistics (for both compilation and solving).
145
146.. option:: --compiler-statistics
147
148 Print statistics for compilation.
149
150.. option:: -c, --compile
151
152 Compile only (do not run solver).
153
154.. option:: --config-dirs
155
156 Output configuration directories.
157
158.. option:: --solvers-json
159
160 Print configurations of available solvers as a JSON array.
161
162.. option:: --param-file <file>
163
164 Read command line options from the given JSON file. See :numref:`ch-param-files`.
165
166Solving options
167~~~~~~~~~~~~~~~
168
169Each solver may support specific command line options for controlling its behaviour. These can be queried using the ``--help <id>`` flag, where ``<id>`` is the name or identifier of a particular solver. Most solvers will support some or all of the following options.
170
171
172.. option:: -a, --all-solutions
173
174 Report *all* solutions in the case of satisfaction
175 problems, or print *intermediate* solutions of increasing quality in the case
176 of optimisation problems.
177
178.. option:: -n <i>, --num-solutions <i>
179
180 Stop after reporting ``i`` solutions (only used with satisfaction problems).
181
182.. option:: -i, --intermediate
183
184 Turns on printing of intermediate solutions for optimisation problems. Has no effect for satisfaction problems.
185
186.. option:: -n-i, --no-intermediate
187
188 Turns off printing of intermediate solutions for optimisation problems. Has no effect for satisfaction problems.
189
190.. option:: --all-satisfaction
191
192 Turns on printing of all solutions for satisfaction problems. Has no effect for optimisation problems.
193
194.. option:: --disable-all-satisfaction
195
196 Turns off printing of all solutions for satisfaction problems. Has no effect for optimisation problems.
197
198.. option:: -f, --free-search
199
200 Instructs the solver to conduct a "free search", i.e., ignore any search
201 annotations. The solver is not *required* to ignore the annotations, but it
202 is *allowed* to do so.
203
204.. option:: --solver-statistics
205
206 Print statistics during and/or after the search for solutions.
207
208.. option:: --verbose-solving
209
210 Print log messages (verbose solving) to the standard error stream.
211
212.. option:: -p <i>, --parallel <i>
213
214 Run with ``i`` parallel threads (for multi-threaded solvers).
215
216.. option:: -r <i>, --random-seed <i>
217
218 Use ``i`` as the random seed (for any random number generators the solver
219 may be using).
220
221Flattener input options
222~~~~~~~~~~~~~~~~~~~~~~~
223
224These options control aspects of the MiniZinc compiler.
225
226.. option:: --ignore-stdlib
227
228 Ignore the standard libraries stdlib.mzn and builtins.mzn
229
230.. option:: --instance-check-only
231
232 Check the model instance (including data) for errors, but do not
233 convert to FlatZinc.
234
235.. option:: -e, --model-check-only
236
237 Check the model (without requiring data) for errors, but do not
238 convert to FlatZinc.
239
240.. option:: --model-interface-only
241
242 Only extract parameters and output variables.
243
244.. option:: --model-types-only
245
246 Only output variable (enum) type information.
247
248.. option:: --no-optimize
249
250 Do not optimize the FlatZinc
251
252.. option:: -m <file>, --model <file>
253
254 File named <file> contains the model.
255
256.. option:: -d <file>, --data <file>
257
258 File named <file> contains data used by the model.
259
260.. option:: -D <data>, --cmdline-data <data>
261
262 Include the given data assignment in the model.
263
264.. option:: --stdlib-dir <dir>
265
266 Path to MiniZinc standard library directory
267
268.. option:: -G --globals-dir --mzn-globals-dir <dir>
269
270 Search for included globals in <stdlib>/<dir>.
271
272.. option:: - --input-from-stdin
273
274 Read problem from standard input
275
276.. option:: -I --search-dir
277
278 Additionally search for included files in <dir>.
279
280.. option:: -D "fMIPdomains=false"
281
282 No domain unification for MIP
283
284.. option:: --MIPDMaxIntvEE <n>
285
286 Max integer domain subinterval length to enforce equality encoding, default 0
287
288.. option:: --MIPDMaxDensEE <n>
289
290 Max domain cardinality to N subintervals ratio
291 to enforce equality encoding, default 0, either condition triggers
292
293.. option:: --only-range-domains
294
295 When no MIPdomains: all domains contiguous, holes replaced by inequalities
296
297.. option:: --allow-multiple-assignments
298
299 Allow multiple assignments to the same variable (e.g. in dzn)
300
301.. option:: --compile-solution-checker <file>.mzc.mzn
302
303 Compile solution checker model.
304
305Flattener two-pass options
306++++++++++++++++++++++++++
307
308Two-pass compilation means that the MiniZinc compiler will first compile the model in order to collect some global information about it, which it can then use in a second pass to improve the resulting FlatZinc. For some combinations of model and target solver, this can lead to substantial improvements in solving time. However, the additional time spent on the first compilation pass does not always pay off.
309
310.. option:: --two-pass
311
312 Flatten twice to make better flattening decisions for the target
313
314.. option:: --use-gecode
315
316 Perform root-node-propagation with Gecode (adds --two-pass)
317
318.. option:: --shave
319
320 Probe bounds of all variables at the root node (adds --use-gecode)
321
322.. option:: --sac
323
324 Probe values of all variables at the root node (adds --use-gecode)
325
326.. option:: --pre-passes <n>
327
328 Number of times to apply shave/sac pass (0 = fixed-point, 1 = default)
329
330.. option:: -O<n>
331
332 Two-pass optimisation levels:
333
334 -O0: Disable optimize (--no-optimize)
335 -O1: Single pass (default)
336 -O2: Same as: --two-pass
337 -O3: Same as: --use-gecode
338 -O4: Same as: --shave
339 -O5: Same as: --sac
340
341Flattener output options
342++++++++++++++++++++++++
343
344These options control how the MiniZinc compiler produces the resulting FlatZinc output. If you run the solver directly through the ``minizinc`` command or the MiniZinc IDE, you do not need to use any of these options.
345
346.. option:: --no-output-ozn, -O-
347
348 Do not output ozn file
349
350.. option:: --output-base <name>
351
352 Base name for output files
353
354.. option:: --fzn <file>, --output-fzn-to-file <file>
355
356 Filename for generated FlatZinc output
357
358.. option:: -O, --ozn, --output-ozn-to-file <file>
359
360 Filename for model output specification (-O- for none)
361
362.. option:: --keep-paths
363
364 Don't remove path annotations from FlatZinc
365
366.. option:: --output-paths
367
368 Output a symbol table (.paths file)
369
370.. option:: --output-paths-to-file <file>
371
372 Output a symbol table (.paths file) to <file>
373
374.. option:: --output-to-stdout, --output-fzn-to-stdout
375
376 Print generated FlatZinc to standard output
377
378.. option:: --output-ozn-to-stdout
379
380 Print model output specification to standard output
381
382.. option:: --output-paths-to-stdout
383
384 Output symbol table to standard output
385
386.. option:: --output-mode <item|dzn|json>
387
388 Create output according to output item (default), or output compatible
389 with dzn or json format
390
391.. option:: --output-objective
392
393 Print value of objective function in dzn or json output
394
395.. option:: -Werror
396
397 Turn warnings into errors
398
399Solution output options
400~~~~~~~~~~~~~~~~~~~~~~~
401
402These options control how solutions are output. Some of these options only apply if ``minizinc`` is used to translate a stream of solutions coming from a solver into readable output (using a .ozn file generated by the compiler).
403
404.. option:: --ozn-file <file>
405
406 Read output specification from ozn file.
407
408.. option:: -o <file>, --output-to-file <file>
409
410 Filename for generated output.
411
412.. option:: -i <n>, --ignore-lines <n>, --ignore-leading-lines <n>
413
414 Ignore the first <n> lines in the FlatZinc solution stream.
415
416.. option:: --soln-sep <s>, --soln-separator <s>, --solution-separator <s>
417
418 Specify the string printed after each solution (as a separate line).
419 The default is to use the same as FlatZinc, "----------".
420
421.. option:: --soln-comma <s>, --solution-comma <s>
422
423 Specify the string used to separate solutions.
424 The default is the empty string.
425
426.. option:: --unsat-msg (--unsatisfiable-msg)
427
428 Specify status message for unsatisfiable problems
429 (default: ``"=====UNSATISFIABLE====="``)
430
431.. option:: --unbounded-msg
432
433 Specify status message for unbounded problems
434 (default: ``"=====UNBOUNDED====="``)
435
436.. option:: --unsatorunbnd-msg
437
438 Specify status message for unsatisfiable or unbounded problems
439 (default: ``"=====UNSATorUNBOUNDED====="``)
440
441.. option:: --unknown-msg
442
443 Specify status message if search finished before determining status
444 (default: ``"=====UNKNOWN====="``)
445
446.. option:: --error-msg
447
448 Specify status message if search resulted in an error
449 (default: ``"=====ERROR====="``)
450
451.. option:: --search-complete-msg <msg>
452
453 Specify status message if when search exhausted the entire search space
454 (default: ``"=========="``)
455
456.. option:: --non-unique
457
458 Allow duplicate solutions.
459
460.. option:: -c, --canonicalize
461
462 Canonicalize the output solution stream (i.e., buffer and sort).
463
464.. option:: --output-non-canonical <file>
465
466 Non-buffered solution output file in case of canonicalization.
467
468.. option:: --output-raw <file>
469
470 File to dump the solver's raw output (not for hard-linked solvers)
471
472.. option:: --no-output-comments
473
474 Do not print comments in the FlatZinc solution stream.
475
476.. option:: --output-time
477
478 Print timing information in the FlatZinc solution stream.
479
480.. option:: --no-flush-output
481
482 Don't flush output stream after every line.
483
484.. _ch-user-config:
485
486User Configuration Files
487------------------------
488
489The ``minizinc`` tool reads a system-wide and a user-specific configuration file to determine default paths, solvers and solver options. The files are called ``Preferences.json``, and you can find out the locations for your platform using the option ``--config-dirs``:
490
491.. code-block:: bash
492
493 $ minizinc --config-dirs
494 {
495 "globalConfigFile" : "/Applications/MiniZincIDE.app/Contents/Resources/share/minizinc/Preferences.json",
496 "userConfigFile" : "/Users/Joe/.minizinc/Preferences.json",
497 "userSolverConfigDir" : "/Users/Joe/.minizinc/solvers",
498 "mznStdlibDir" : "/Applications/MiniZincIDE.app/Contents/Resources/share/minizinc"
499 }
500
501The configuration files are simple JSON files that can contain the following configuration options:
502
503- ``mzn_solver_path`` (list of strings): Additional directories to scan for solver configuration files.
504- ``mzn_lib_dir`` (string): Location of the MiniZinc standard library.
505- ``tagDefaults`` (list of lists of strings): Each entry maps a tag to the default solver for that tag. For example, ``[["cp","org.chuffed.chuffed"],["mip","org.minizinc.gurobi"]]`` would declare that whenever a solver with tag ``"cp"`` is requested, Chuffed should be used, and for the ``"mip"`` tag, Gurobi is the default. The empty tag (``""``) can be used to define the system-wide default solver (i.e., the solver that is chosen when running ``minizinc`` without the ``--solver`` argument).
506- ``solverDefaults`` (list of lists of strings): Each entry consists of a list of three strings: a solver identifier, a command line option, and a value for that command line option.For example, ``[["org.minizinc.gurobi","--gurobi-dll", "/Library/gurobi752/mac64/lib/libgurobi75.so"]]`` would specify the Gurobi shared library to use (on a macOS system with Gurobi 7.5.2). For command line options that don't take a value, you have to specify an empty string, e.g. ``[["org.minizinc.gurobi","--uniform-search",""]]``.
507
508Here is a sample configuration file:
509
510.. code-block:: json
511
512 {
513 "mzn_solver_path": ["/usr/share/choco"],
514 "tagDefaults": [["cp","org.choco-solver.choco"],["mip","org.minizinc.cplex"],["","org.gecode.gecode"]],
515 "solverDefaults": [["org.minizinc.cplex","--cplex-dll","/opt/CPLEX_Studio128/cplex/bin/x86-64_sles10_4.1/libcplex128.so"]]
516 }
517
518Configuration values in the user-specific configuration file override the global values, except for solver default arguments, which are only overridden if the name of the option is the same, and otherwise get added to the command line.
519
520Note: Due to current limitations in MiniZinc's JSON parser, we use lists of strings rather than objects for the default mappings. This may change in a future release, but the current syntax will remain valid. The location of the global configuration is currently the ``share/minizinc`` directory of the MiniZinc installation. This may change in future versions to be more consistent with file system standards (e.g., to use ``/etc`` on Linux and ``/Library/Preferences`` on macOS).
521
522.. _ch-param-files:
523
524Command-line Parameter Files
525----------------------------
526
527The ``minizinc`` tool is able to read command line options from one or more JSON files through use of the ``--param-file`` option.
528This option may be specified multiple times, and substitutes the options given in the JSON file in its place, meaning it can be combined with normal command-line options, as well as other ``--param-file`` configurations.
529MiniZinc also recognises the ``.mpc`` file extension for command line parameter files without requiring the ``--param-file`` option.
530
531As most ``minizinc`` options which take a single value are given the final one they are assigned, later specifications of command-line parameter files will generally override options contained in previous ones, and later command-line options will override previous options.
532
533The given file must be in JSON format and contain a root object whose keys and values correspond to command line options and their values respectively.
534For long-form options which start with two dashes, the leading dashes may be omitted from the JSON object key name.
535For short-form options which start with a single dash, the leading dash is required.
536Command line options which take multiple values through being specified multiple times can be represented using a JSON array.
537Options which take the JSON boolean value ``true`` are treated as flags without associated parameters (``false`` omits the flag).
538
539Consider the configuration file ``config.mpc``:
540
541.. code-block:: json
542
543 {
544 "solver": "gecode",
545 "cmdline-data": ["x = 1", "y = 2", "z = 3"],
546 "-p": 2,
547 "output-paths": true
548 }
549
550Running ``minizinc --verbose config.mpc -p 4 model.mzn`` (or ``minizinc --verbose --param-file config.mpc -p 4 model.mzn``) is equivalent to running
551
552.. code-block:: bash
553
554 $ minizinc --verbose \
555 --solver gecode \
556 --cmdline-data "x = 1" \
557 --cmdline-data "y = 2" \
558 --cmdline-data "z = 3" \
559 -p 2 \
560 --output-paths \
561 -p 4 \
562 model.mzn
563
564Note that since ``-p 4`` comes after ``-p 2``, its value overrides the previous one and so ``-p 4`` is used. However, the multiple ``--cmdline-data`` options do not override each other as ``--cmdline-data`` allows for specification of multiple strings of data.
565
566Configuration files may also be used as a convenient way to specify instances.
567
568For a configuration file ``instance.mpc``
569
570.. code-block:: json
571
572 {
573 "model": "model.mzn",
574 "data": "data.dzn"
575 }
576
577And another configuration file ``gecode.mpc``
578
579.. code-block:: json
580
581 {
582 "solver": "gecode",
583 "intermediate-solutions": true
584 }
585
586We can run the instance with ``minizinc gecode.mpc instance.mpc``. Note that the files ``model.dzn`` and ``data.dzn`` will be resolved relative to the location of the configuration file which specified them.
587
588In this way, multiple configuration files can be set up for different instances and solver configurations, then combined as required.