MiniZinc Change Log
- Add warning for MIP solvers that do not support -a option for satisfaction
- Print introduced variable names with additional underscore to make
debugging FlatZinc easier. Fixes 147.
- Add support for pow function in linearisation library.
- Add support for parallel solving with CBC.
- Flatten top-level conjunctions in the order defined in the model.
- Fix major race condition that would crash the IDE when it didn't detect
that a solver process had finished.
- Improve HTML output in the IDE by making sure every line is terminated by a newline.
- Fix a garbage collection bug that could cause dangling pointers when
expressions were copied.
- Fix type checker to allow empty arrays to be assigned to variables
declared as arrays of enums.
- Fix infeasibility check in MIP translation for some inequality constraints.
- Improved defines_var annotations for reified xor constraints. Fixes 146.
- Fix output of empty integer sets and deal with empty arrays in output models.
- Fix MIP translation when boolean variables were removed due to aliasing.
- Improve corner cases for linearisation of cumulative constraint.
- Properly report undefinedness in par bool expressions.
- Enable some additional constant folding during flattening. Fixes 149.
- Remove more internal annotations from the generated FlatZinc.
- Detect failure earlier if optimisation pass leads to fixing of variables
outside their domains.
- Fix CBC backend to correctly print UNSAT message for models where the
compiler already detected unsatisfiability, and print solution separators
even where there is no other output.
- Add missing var_dom function for arrays of optional integer variables.
- Fix aliasing for optional integer variables. Fixes 132.
- Remove all annotations from output model.
- Fix computation of return type for functions that return arrays of enums.
- Don't output newline if user-defined solution separator or status message is empty
- Fix return type computation for functions where return type contains
- Check finiteness of float literals and bounds. Fixes 138.
- More checks for function return values. Fixes 136.
- Fix var int comprehensions (now triggers error message instead of crash
for var set of int comprehensions). Fixes 135.
- Fix output of variables with quoted identifiers.
- Fix flattening of let expressions that contain variables with undefined
(i.e., partial) right hand side.
- Make printing of error messages to stdout or stderr more consistent
- Fix type checking of initialisation of enum types.
- Improve error messages for array access and index set errors. Fixes 131.
- Fix definition of multi-dimensional element constraints to impose
correct bounds on index variables.
- Fix binding analysis during type checking, which did not handle the
shadowing of top-level declarations by comprehension generators correctly.
- Fix a bug in the type checking for generators that iterate over
arrays of enums.
- Fix a bug in the output handling of arrays of enums.
- Fix handling of multiple output items (only the last item was
compiled, now the concatenation is used for output as defined
in the specification).
- Add missing min/max functions for set variables. Can be redefined to solver
builtins using the new redefinitions-2.1.1.mzn library file.
- Add support for option type expressions as objective functions.
- Automatically coerce arrays constructed using ++ to any enum index set
(in addition to array literals and comprehensions).
- Include cmath header to fix compilation issues with some compilers. Fixes 125.
- Fix a garbage collection bug in the type checking for enumerated types that would
sometimes lead to crashes or incorrect error messages.
- Fix type checking of comprehensions that involve enumerated types.
- Fix bounds computation for var sets of enumerated types.
- Support anon_enum function as documented.
- MiniZinc now supports enumerated types.
- Solvers can be interfaced directly to the MiniZinc library, and MiniZinc
comes with direct support for the CBC, Gurobi and CPLEX MIP solvers.
- The linearisation library has been updated, resulting in much better FlatZinc
being generated for MIP solvers.
- Data files can be in JSON format, and MiniZinc can produce JSON output
(using the --output-mode command line option).
- Variables can be annotated as ::add_to_output instead of writing an output
- The compiler can output information about the parameters and output variables
of a model (using the --model-interface-only option).
- Floats are handled better (detecting infinities and handling sets of floats).
- Bounds can be computed for more expressions (instead of failing with an error
- Fix a bug in optimization that could remove variables even if they are used.
- Fix float variable declarations with sets of floats as domains.
Fixes 117 and 98.
- Fix type checking and evaluation of asserts with array arguments. Fixes 109.
- Fix abs(var float) declaration to work on floats without declared bounds.
- Fix a bug in the computation of int and float bounds that could result in
incorrect bounds in some cases. Fixes 94.
- Fix garbage collection when creating output models. Fixes 77.
- Fix binary operators on optional variables (in some cases comparison
operators were reversed).
- Fix optimization of unconstrained variables (could sometimes lead to
constraints being removed although they were not subsumed).
- Less aggressive aggregation of linear expressions in cases where it
leads to much less efficient FlatZinc.
- Don't create temporary variable for an array literal if it is discarded
- Only create new partiality variable for if-then-else expression if there's
at least one var condition.
- Replace recursive definitions of array_intersect and array_union with
- Don't report warnings about partiality when using extended generator
- Include cmath to enable building with some versions of gcc.
- Constrain result of function call based on function return type if necessary.
- Make sure linear expressions generated during binding of variables are
properly flattened (including simplification of the linear expression)
- Fix a bug in the Common Subexpression Elimination table of the compiler,
which could lead to some constraints being dropped (especially when using
- The output model sometimes did not include all required definitions,
in particular when array declarations used identifiers to specify the
- The generated FlatZinc sometimes still contained bool variables that were
not connected to the rest of the model, which could produce incorrect
solutions being printed.
- Fix a bug where warnings (e.g. about partial functions) could lead to
- Fix the bounds computation for integer and float variables, which could
produce incorrect bounds for linear expressions. Fixes 94.
- Fix a bug in the IDE that caused solver output to be shown incompletely
in some cases.
- Partial functions are now always evaluated in their Boolean context,
independent of whether they are par or var. If the result of a partial
function is statically known to be undefined (such as division by zero or
array access out of bounds), and it is used in a constraint expression,
this now results in a warning instead of an
error. Warnings can be turned off using the ::maybe_partial annotation.
Fixes 43 and 74.
- Fix a bug in the optimisation phase related to unification of aliased
- Fix short-circuit evaluation of Boolean expressions.
- Fix a bug in the optimisation phase related to repeated simplification of
some Boolean expressions.
- Handle errors in output produced by solver without solns2out crashing.
- Fix a bug in the integer bounds computation that caused bool2int with an
embedded conditional to crash.
- Fix a problem with short-circuit compilation of == expressions when one
side was a var opt bool.
- Stop compilation when model is failed. Fixes a bug where mzn2fzn would
sometimes not clean up the FlatZinc enough for the solver.
- Fix parsing of hex and octal literals. Fixes 71.
- Fix compilation of extended comprehensions. Fixes 72.
- Fix computation of float array access bounds.
- Fix aggregation of clauses (could sometimes ignore the negative literals).
- Fix a bug in the optimiser that could lead to undefined variables in the
generated FlatZinc. Fixes 70.
- Need to take return type into account when copying functions to output
model. Fixes 55.
- Evaluate calls that result in arrays using eval_arraylit. Fixes 57.
- Move inverse function to its own library file, so that it remains available
when a solver provides an alternative for the inverse predicate.
- Optimisation phase now recursively checks constraints when elements in an
array become fixed.
- Fix CMakeLists file to work for paths that contain spaces.
- Distinguish between infix operators and regular functions in the generated
html documentation. Fixes 61.
- Made parser more robust against incorrect code.
- Fix increment/decrement operators for IntVals and make all operations throw
correct overflow exceptions.
- Fix automatic type coercion for variables declared in let expressions.
- Fix a crash when printing some error messages.
- Fix compute_div_bounds builtin to return correct result for a division by
- Fix optimisation of Boolean constraints to use pointer equality instead of
structural equality (same expression can occur multiple times in the
- Only optimise constraints that have not been removed yet.
- Fix declaration of functional version of bin_packing_load. Fixes 64.
- Set type of arrays returned from polymorphic functions. Fixes 65.
- Fix parsing of quoted unary operator calls.
- Only compute set functions when bounds are valid. Fixes 66.
- Compute proper bounds for if-then-else expressions.
- Report error when no reified version of a constraint is available. Fixes 67.
- Fix type checking of annotations on binary operators.
- Keep annotations when rewriting linear constraints and remove is_defined_var
annotations from fixed variables. Fixes 69.
Integer, Boolean and float literals are now cached to achieve better memory
performance for some models.
Improve performance of parsing integer literals.
Improve handling of clause constraints.
Add source files of MiniZinc specification to the repository.
Limit maximum array size to enable better error messages.
Add implied_constraint predicate as a synonym for redundant_constraint.
- Fix incorrect negation of some reified comparisons.
- Make lb/ub functions work in more cases.
- Fix several bugs in the optimisation phase (could lead to incorrect
FlatZinc and crashes).
- Fix a problem with reverse mapper functions when the result of the reverse
mapper can be fixed to a constant.
- Improved propagation of Boolean constants in the optimisation phase. This
should result in far fewer aliases and improves simplification of
conjunctions, disjunctions and clauses.
- Add special case handling for integer division by 1.
- Fix FlatZinc generator phase, need to turn all array literal arguments into
1-based single dimensional arrays.
- Fix compilation of if-then-else expressions with var conditions (which didn't
implement proper partiality/totality semantics). Fixes 42.
- Provide correct bounds for weak opt var arithmetic. Fixes 51.
- Need to be able to handle unflattened annotations. Fixes 53.
- Fix generation of output model (needs to ignore items that have been removed
- Add missing lb(var set of int) builtin. Fixes 47.
- Check that var set declarations have a finite element type. Fixes 46.
- Fix translation context for binary operators on arrays.
- Need to access IntVal::infinity as a function, otherwise depending on linker
etc it may become 0 in some cases. Fixes 40.
- Change pretty printer to use one less digit when printing float literals.
This fixes 41 (or at least provides a workaround), but some double
constants may still be rounded incorrectly when pretty printing and reading
them back in. The real fix will be to output hex float literals (coming
- Distinguish between generalised comprehensions (iterating over sets) and
iterating over arrays. Fixes compilation of comprehensions where iteration
over an array is combined with var where clauses. Fixes 45.
- Fix bug in creation of output model where sometimes chains of variable
definitions could lead to crashes.
- Avoi creating mutually recursive definitions in some corner cases, which
could cause the compiler to run into infinite loops.
- Don't copy vardecl items to output model that are already there. Fixes 44.
- Remove domain from array declarations in FlatZinc (avoids problems with
domains where holes need to be removed and when there are infinities in the
- Fix flattening of equality operator between non-opt and opt vars.
- Check that model contains a single solve and output item during type
checking (previously, multiple output items were not detected and resulted
in incorrect .ozn files).
- Fix flattening of xor (arguments need to be in mixed context).
- Use is_fixed in cumulative definition.
- Fix bug where a par right hand side of a variable mentioned in the output
would cause a crash.
- Fix variable dependency tracking during rewriting in the optimisation phase.
Could previously lead to variables being removed that are still required.
- Add parser support for hexadecimal floating point constants.
- Fix bounds computation for some calls (abs, int_times).
- Fix flattening of some array declarations (when right hand side is
- Add four missing GC locks (could lead to incorrect garbage collection).
- Compact output model only after optimisation phase (could lead to
incorrect items being removed from output model).
- Improve the standard decomposition for the cumulative constraint.
- Better handling of binary operators during type checking and flattening,
can sometimes avoid stack overflows (e.g. for large conjunctions).
- Make ++ operator left associative (avoid stack overflows in the parser).
- Add ::domain annotations to linear constraints generated from
multi-dimensional element constraints.
- Greatly improved linearisation library.
- Fix recursive function calls that contain let expressions.
- Fix compilation of comprehensions inside parametric functions.
- Fix a memory leak in solns2out.
- Fix a problem in the evaluation of binary operators.
- Fix a bug in the flattening of array literals.
- Fix a bug that would crash the parser on certain syntax errors in let
- Models can now be read from standard input (using the "-" or
"--input-from-stdin" command line options). Thanks to Sebastian Kosch.
- Improved handling of bool2int during FlatZinc generation.
- Fix unification of aliased variables which could sometimes result in
variables being removed although had a constraining right hand side.
- Fix evaluation of set comprehensions.
- Fix command line flag --no-output-ozn
- Fix performance problem when evaluating array expressions inside lets.
- Fix flattening of bool_xor redefinitions.
- Fix partial evaluation of some array access expressions with var indexes.
- Fix definition of geost constraint.
- User-defined functions are now copied correctly into the output model
if they are referenced in the output item.
- Set comprehensions are fully evaluated.
(Internal release that did not contain some essential fixes)
- The optimiser now removes simple domain constraints from the FlatZinc
- The compiler now checks for integer overflows in all built-in operations
- Report an error when the FlatZinc or ozn file cannot be opened for writing
- Add support for 3d array literals (e.g. [| |1,2|3,4|,|5,6|7,8| |] )
- Add show2d and show3d functions for formatting array output
- Add row/col functions for variable arrays (fixes 2)
- Introduce builtins for creating random distributions
- Add reverse library function
- Postpone flattening of some reified constraints
- Slightly improved compilation of partial function calls when it can be
inferred at compile time that their result is undefined
- Allow functions with empty argument lists to be declared as
function int: foo(); instead of just function int: foo;
- Improve error reporting, in particular for errors in comprehensions
- Enable expressions a..b where a and b are integer variables
- Add redundant_constraint and symmetry_breaking_constraint builtins, these
can be rewritten by solver libraries to allow e.g. local search solvers to
ignore redundant constraints.
- Improve flattening of predicates that simply return their arguments (makes
the redundant_constraint and symmetry_breaking_constraint predicates work
in more situations).
- Replace command line option --only-range-domains by optional boolean value
so that solver libraries can set the flag directly in their redefinitions
- Stop flattening immediately when a model has been found to contain an
- Improve flattening of array access expressions, in particular for nested
array accesses that can be combined into a single element constraint
- Add command line option -s or --statistics to print statistics about the
- Improve bounds computation for if-then-else expressions
- Clause arguments are compiled in positive and negative contexts instead of
mixed. That means that predicates that introduce free variables can now
be used in the positive part of a clause.
- Fix simplification of linear expressions, negative coefficients could
sometimes result in incorrect bounds
- Fix bounds computation for unary minus operator
- Add missing par set comparison builtins
- Fix bounds computation for extended comprehension syntax
- Fix a bug in the garbage collector that could sometimes lead to premature
deletion of expressions
- Fix bounds computation for set difference
- Fix duplication of some arrays in the FlatZinc (fixes 3)
- Fix bounds inference for variables bound to empty sets (fixes 3)
- Fix bug in error reporting function, which would sometimes not report the
entire call stack
- Fix the generation of fresh variable names for generator expressions
- Fix subtype check to allow empty arrays as subtype of arrays of sets
- Fix crash when using assert/2
- Fix bug when function used in output referred to par variable
- Fix bug in type checker, the detection of cyclic definitions was not
correct and could lead to stack overflows
- Fix parser to accept expressions with two consecutive array accesses
(like x, which are valid MiniZinc if x is an array of sets)
- Fix error reporting when an evaluation error occurs within a comprehension
- Report type error on some ambiguous function calls
- Report type error on var sets with element type other than int
- Report type error when trying to coerce a var set into an array
- Report error when calling function with a value that is outside the
declared parameter bounds
- Fix arg_sort builtin to implement the correct semantics
- Fix sort_by builtin to sort in non-decreasing order, and work with floats
- Fix bug in type checker, now automatic coercions in functions defined with
type variables (like the comparison operators) work correctly
- Check that index sets match for arrays assigned in let expressions
- Fix bug in bounds inference for integer expressions with annotations
- Fix propagation of defines_var annotation to be pushed through calls
- Fix parser to accept empty 2d and 3d array literals
- Fix flattening to remove defines_var annotations with par argument, e.g.
defines_var(2), which could be introduced by the optimisation pass
- Fix output model creation for variables that have been redefined, and
remove more unused variables from the FlatZinc.
- Fix bug in the garbage collector that could result in function items not
being kept alive in rare cases.
Major bugs and changes:
- Fix optimisation phase, which was previously incorrectly removing variables
- Add support for trigonometric functions (built-ins were missing in 2.0.0)
and pow (var versions were missing)
- Fix equality operator on par arrays
- All expressions in output model are now made par
- Improve bounds computation for float variables
- Fix translation of functions that need automatic coercion of their return
- Fix the array_lb and array_ub builtins, which would return incorrect bounds
in some cases
Minor bugs and changes:
- Add space between "array" and "[" in the pretty printer, to be compatible
with 1.6 output
- Output all par declarations before the var declarations in FlatZinc
- Fix parser, which could sometimes crash on invalid input
- Improve efficiency of bounds computation on some float expressions
- Add special case handling for division by 1
- Add missing float_times definition to the flatzinc builtins
- Use correct version of var_dom for float variables
- Output information about which files are included in verbose mode
- Only compute bounds for "then" expressions if the "if" is not fixed to false
MiniZinc 2.0 contains many new features and is based on a complete rewrite of
the MiniZinc-to-FlatZinc compiler. If you are currently using the previous
version 1.6, the new tools can be used as drop-in replacements. The generated
FlatZinc is compatible with version 1.6, so all FlatZinc solvers should work
MiniZinc language changes
- MiniZinc now supports user-defined functions. Details have been published
in the paper "MiniZinc with Functions". Both functions and predicates can
- MiniZinc now supports option types. Details have been published in the
paper "Modelling with Option Types in MiniZinc".
- Let expressions have been generalised. They can now contain constraint
items in addition to variable declarations.
- Array index sets can be declared using arbitrary set expressions as long as
they evaluate to contiguous ranges.
- The if-then-else expression has been generalised to allow the condition to
be a var bool expression (instead of only par bool).
- Array and set comprehensions as well as generator calls can now iterate
over variables and use var bool where conditions.
- Any bool expression can now automatically coerce to an int expression,
likewise for int and float. This means that you don't have to write
bool2int or int2float in you models any more.
- Equality constraints can now be posted between array expressions.
- Arbitrary expressions can now be included ("interpolated") into strings,
using the syntax "some text \(e) some more text", where e is any
expression. It is the same as writing "some text "++show(e)++" some more
New built-in functions
- Array functions: array1d, arrayXd, row, col, has_index, has_element, sort_by,
sort, arg_sort, arg_min, arg_max
New global constraints
- arg_max, arg_min
- k-dimensional diffn
- regular with NFAs
- symmetric all different
- optional scheduling constraints: alternative, span, disjunctive, cumulative
- functional versions of many global constraints
New tool chain
- There are a few new builtins that solvers can reimplement, these are listed
in the redefinitions-2.0 file.
- Include items use a different method for finding included files. Paths are
now interpreted as relative to the file that has the include item. That
way, the mzn2fzn compiler can be called from a different working directory.
- A new tool, mzn2doc, can produce html output from the documentation
comments. The MiniZinc distribution contains the documentation for global
constraints and builtins generated directly from the library source code.