minizinc/libminizinc

The MiniZinc compiler

MiniZinc

A high-level constraint modelling language that allows you to easily express and solve discrete optimisation problems.
Visit our website »

View Documentation · Report Bug · Request Feature

Table of Contents

• About the Project
• Getting Started
  • Installation
  • Usage
• Building
  • Prerequisites
  • Compilation
• Testing
• License
• Contact

About The Project

MiniZinc is a free and open-source constraint modeling language.

You can use MiniZinc to model constraint satisfaction and optimisation problems in a high-level, solver-independent way, taking advantage of a large library of pre-defined constraints. Your model is then compiled into FlatZinc, a solver input language that is understood by a wide range of solvers.

MiniZinc is developed at Monash University in collaboration with Data61 Decision Sciences.

Getting Started

To get a MiniZinc up and running follow these simple steps.

Installation

The recommended way to install MiniZinc is by the use of the bundled binary packages. These packages are available for machines running Linux, Mac, and Windows.

The latest release can be found on the MiniZinc website.

Usage

Once the MiniZinc bundle is installed on your machine, you can start expressing and solving discrete optimisation problems. The following code segment shows a MiniZinc model for the well known n-queens problem.

int: n = 8; % The number of queens.

array [1..n] of var 1..n: q;

include "alldifferent.mzn";

constraint alldifferent(q);
constraint alldifferent(i in 1..n)(q[i] + i);
constraint alldifferent(i in 1..n)(q[i] - i);

You have two easy options to solve this model:

• In the MiniZincIDE: Select your preferred solver and press the "Run" button.
• With the minizinc executable available on your path: run minizinc --solver gecode nqueens.mzn.

For more example MiniZinc models and more information about working with MiniZinc, please refer to our Documentation

Building

The following instructions will help you compile the MiniZinc compiler. Note that this repository does not include the IDE, findMUS, or any solvers that are part of the MiniZinc project. These can be found in the following repositories:

• MiniZincIDE
• Gecode
• Chuffed

Prerequisites

• CMake (>=3.4)
• A recent C++ compiler - Compilation is tested with recent versions of Clang, GCC, and Microsoft Visual C++.
• (optional) Bison (>=3.4) and Flex (>=2.5) - To make changes to the MiniZinc lexer or parser.
• (optional) Gecode - To compile the internal Gecode solver interface (included in the MiniZinc bundle)
• (optional) Coin OR's CBC - To compile the internal CBC solver interface (included in the MiniZinc bundle)
• (optional) Proprietary solver headers (CPLEX, Gurobi, SCIP, Xpress) - To load these solvers at runtime (included in the MiniZinc bundle)

Compilation

The MiniZinc compiler is compiled as a CMake project. CMake's User Interaction Guide can provide you with a quick introduction to compiling CMake projects. The following CMake variables can be used in the MiniZinc project to instruct the compilation behaviour:

Variable	Default	Description
CMAKE_BUILD_TYPE	Release	Build type of single-configuration generators.
CMAKE_INSTALL_PREFIX		Install directory used by --target install.
CMAKE_POSITION_INDEPENDENT_CODE	TRUE	Whether to create a position-independent targets
<solver_name>_ROOT		Additional directory to look for <solver_name>
CMAKEDISABLE_FIND_PACKAGE**<solver_name>**	FALSE	Disable compilation of <solver_name>'s solver interface
CPLEX_PLUGIN	TRUE	Load CPLEX at runtime (instead of static compilation)

Possible values for <solver_name> are CPlex, Geas, Gecode, and OsiCBC.

Testing

The correctness of the MiniZinc compiler is tested using a PyTest test suite. Instruction on how to run the test suite and how to add new tests can be found here

License

Distributed under the Mozilla Public License Version 2.0. See LICENSE for more information.

Contact

🏛 MiniZinc Community

• Website: https://www.minizinc.org/
• StackOverflow: https://stackoverflow.com/questions/tagged/minizinc
• Google Groups: https://groups.google.com/g/minizinc

🏛 Monash Optimisation Group

• Website: https://www.monash.edu/it/dsai/optimisation

libminizinc's Issues

link_set_to_booleans bug (Gecode specific?) (MZN 1.6, 2.0)

Model:

include "globals.mzn";

set of int: foo = {2};
array[1..3] of var bool: bar;

constraint
  link_set_to_booleans(foo, bar);

solve satisfy;

output [
  "foo = ", show(foo), "\n",
  "bar = ", show(bar), "\n",
  ];

Output:

solovej>mzn-gecode -a bug.mzn 
foo = 2..2
bar = [false, true, false]
----------
foo = 2..2
bar = [true, true, false]
----------
foo = 2..2
bar = [false, true, true]
----------
foo = 2..2
bar = [true, true, true]
----------
==========

mzn2fzn introduces undeclared variable

solovej>minizinc -a -k -s bug.mzn bug.dzn
bug.fzn:1395:
  symbol error: `X_INTRODUCED_1264' undeclared
solovej>which minizinc
/opt/minizinc-2.0.1/bin/minizinc

It works in 1.6. Here is the input:

:bug.mzn:

include "globals.mzn";

%-----------------------------------------------------------------------------%
% Parameters

int: no_machines;   % Number of machines
int: no_tests;   % Number of tests
int: no_resources;   % Number of total resources

set of int: Mach  = 1..no_machines;
set of int: Test  = 1..no_tests;
set of int: Resource  = 1..no_resources;

array[Test] of int: duration;
array[Test] of int: order;
array[Test] of set of Mach: machine;
array[Resource] of int: resource_capacity;
array[Test,Resource] of int: resource_usage;

int: maxtime = sum(i in Test)(duration[i]);
int: maxdur = max(i in Test)(duration[i]);

% VARIABLES

array[Test] of var 0..maxtime: start;
array[Test] of var Mach: mach;
array[Test] of var 0..maxtime: start_part;

var 0..maxtime: makespan;

% CONSTRAINTS

constraint
  forall(t in Test)(
    mach[t] in machine[t] /\
    start[t] + duration[t] <= makespan
  );

constraint
  forall(t in Test)(
    start_part[t] = start[t] div duration[t]
  );

constraint
  diffn(start, mach, duration, [1 | t in Test]);

constraint
  forall(r in Resource where card({t | t in Test where resource_usage[t,r]>0})>1)(
    cumulative([start[t] | t in Test where resource_usage[t,r]>0], 
           [duration[t] | t in Test where resource_usage[t,r]>0], 
           [resource_usage[t,r] | t in Test where resource_usage[t,r]>0], 
           resource_capacity[r])
  );

constraint
  forall(m in Mach, n in Mach
        where m<n /\ forall(t in Test)(m in machine[t] <-> n in machine[t]))(
    value_precede(m, n, [mach[order[t]] | t in Test])
  );

% search & output

solve :: seq_search([   if k=1 then 
                           int_search([start_part[order[t]]], input_order, indomain_split, complete)
                        else
                           int_search([mach[order[t]]], input_order, indomain_random, complete)
            endif
            |   t in Test, k in 1..2
            ] ++ [
                           int_search([start[order[t]] | t in Test], input_order, indomain_split, complete)
            ])
minimize makespan;

output 
[   "makespan = ", show(makespan), ";\n",
    "start = ", show(start), ";\n",
    "mach = ", show(mach), ";\n"
];

:bug.dzn:

no_tests = 10;
no_machines = 3;
no_resources = 3;

%Duration of each test case
duration = [2,4,3,4,3,2,1,2,3,5];

%Each test case can be executed on one of the following machines:
machine = [{1,2,3}, {1,2,3}, {1,2,3}, {1,2,3}, {1,2,3}, {1,2,3}, {1}, {2}, {3}, {1,3}] ;

%Capacity of each resource (r1,r2,r3)
resource_capacity = [1,1,1];

%Each test case require the following amount of resources from each resource (r1,r2,r3):
resource_usage = [|0,1,0,
                  |0,1,0,
          |1,1,0,
          |0,1,1,
          |0,0,0,
          |0,0,0,
          |0,0,0,
          |0,0,0,
          |0,0,0,
          |0,0,0,
          |];

order = [4,3,2,1,10,9,5,6,8,7];

minizinc-2.0: geost extreme cases

Currently, a shape can be defined as an empty set of rectangles. Such a shape is arguably not too useful, and we certainly didn't mean to allow it when we came up with geost.

Another fine point: in SICStus, geost can take the option bounding_box(Lower,Upper), which almost corresponds to the two extra arguments of geost_bb, but not quite. SICStus requires that some objects actually reach Lower and Upper, whereas geost_bb provides a bounding box that allows a margin to the closest objects.

show2d is slow

The function "show2d" is very very slow, even for relatively small arrays (3*100). I found that the largest bottleneck was in

int: max_length = max([string_length(s[i]) | i in index_set(s)])

So I believe the builtin function string_length is in turn quite slow. I didn't check the c++ code for that function but if this is unavoidable, one might one to explore an alternative definition of show2d, for instance, taking an argument for the max_length to be set by the user.

Long sequence of ++ exhausts memory

An output item like this:

output [ "X" ++ "X" ++ "X" ++ "X" ++ ... ++ "X" ++ "X" ];

causes the compiler to give up with this error message:

Error: memory exhausted

A workaround in this case is to use concat instead, but the sequence of ++ should also work.

MiniZinc: type error: identifier `friend' already defined groupphoto.ozn:8

Command $ minizinc groupphoto.mzn data/groupphoto1.dzn.

Code:

 include "alldifferent.mzn";
 array[Person] of var 0..4: obj =
    [left(position[i]) +
     right(position[i]) +
     front(position[i]) +
     rear(position[i])
     | i in Person];

output [show(obj),
    show(position)];

solve maximize sum(obj);
int: n;
array[Person, Person] of bool: friend;

set of int: Person = 1..n;
array[Person] of var Person: position;
constraint alldifferent(position);
int: m = n div 2;
constraint assert(n mod 2 = 0, "n must be even");

function var 0..1: left(var Person: i) =
  if i > 1 /\ i != m + 1
  then bool2int(friend[position[i], position[i-1]])
  else 0 endif;

function var 0..1: right(var Person: i) =
  if i < n /\ i != m
  then bool2int(friend[position[i], position[i+1]])
  else 0 endif;

function var 0..1: front(var Person: i) =
  if i > m
  then bool2int(friend[position[i], position[i-m]])
  else 0 endif;

function var 0..1: rear(var Person: i) =
  if i < m
  then bool2int(friend[position[i], position[i+m]])
  else 0 endif;

Out-of-bounds error in "then" branch goes undetected

int: M = 2;
int: N = 3;
array[1..M] of var 1..N: length; % We consider M tours of maximum length N
array[1..M, 1..N] of var int: places; % Only places[i, j] with j <= length[i] are valid

% In the valid part of places[i], adjacent places must be different
constraint
forall(i in 1..M, j in 1..N-1) (
if j < length[i] then places[i, j] != places[i, j + 1] else true endif
);

% Same constraint as above except for undetected out-of-bounds error ("j - 1" instead of "j + 1")
constraint
forall(i in 1..M, j in 1..N-1) (
if j < length[i] then places[i, j] != places[i, j - 1] else true endif
);

% Now without if/then/endif: Out-of-bounds error is detected properly
constraint
forall(i in 1..M, j in 1..N-1) (
places[i, j] != places[i, j - 1]
);

solve satisfy;

Wrong version numbers in 2.04 and 2.06?

After downloading and installing the 2.04 and 2.06 distributions for OSX from
http://www.minizinc.org/
and
http://www.minizinc.org/2.0/install-mac.html
and running
$ minizinc --version
the output is
G12 MiniZinc evaluation driver, version 2.0.3

Sugiyama (minizinc challenge 2010) not working in 2.0

The sugiyama2.mzn model from the 2010 competition is not accepted by mzn2fzn 2.0.1. The reported error is:

constraint forall(l in Layers, i in 1..card(unconnected[l]))(positions[unconnected[l][i]] = partial_widths[l] + i);
                                                                                     ^
Error: syntax error, unexpected [, expecting ]

Note that unconnected is defined to be an array[Layers] of set of int. So it seems that indexing over the elements of a set was allowed in MiniZinc 1.6 but not anymore in MiniZinc 2.0. Although the new behaviour might be the normal one, I could not find this change in the changelog of MiniZinc 2.0. I did not search in the documentation to see whether this was expected behaviour in 1.6 or not, but it was accepted in any case.

Disappearing constraints

Some constraints are lost when flattening the following model:

include "globals.mzn";

array[1..2] of var 0..1: orientation;
array[1..3] of var 1..3: order;

constraint orientation[1] == bool2int(order[1] < order[2]);
constraint orientation[2] == bool2int(order[2] < order[3]);
constraint orientation[1] == 1;

solve satisfy;

The constraints do some channelling between order and orientation but when an orientation variable is fixed (last constraint), the corresponding inequality constraint is not added to the flatzinc model. Here is the output with mzn2fzn 2.0.2:

array [1..2] of int: X_INTRODUCED_5 = [1,-1];
var 1..3: X_INTRODUCED_2;
var 1..3: X_INTRODUCED_3;
var 1..3: X_INTRODUCED_4;
var bool: X_INTRODUCED_8 ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_9 ::var_is_introduced :: is_defined_var;
array [1..2] of var 0..1: orientation:: output_array([1..2]) = [1,X_INTRODUCED_9];
array [1..3] of var 1..3: order:: output_array([1..3]) = [X_INTRODUCED_2,X_INTRODUCED_3,X_INTRODUCED_4];
constraint int_lin_le_reif(X_INTRODUCED_5,[X_INTRODUCED_3,X_INTRODUCED_4],-1,X_INTRODUCED_8):: defines_var(X_INTRODUCED_8);
constraint bool2int(X_INTRODUCED_8,X_INTRODUCED_9):: defines_var(X_INTRODUCED_9);
solve  satisfy;

The problem disappears if orientation is replaced by an array of Boolean variables (and the model is adapted accordingly).

Use of lb() function produces incorrect error message

Using openSUSE Linux 13.2 and Minizinc 0.9.9/2.0.6, in the (bad) code:

array[int] of set of 1..10: thesets = [{1,2},{3,5},{4,6}];
set of 1..10: sett = {5,6,9};

var 1..10: y;
var set of 1..10: z;
constraint y == min(thesets[3]);
constraint z == lb(thesets[3]);

solve satisfy;

minizinc responds with a message indicating that the lb() builtin is missing.
I think this is incorrect, the lb() function is there, but the code referring to it is bad.
A colleague in Prof. Stuckey's online course points out that if the lb() is used correctly to refer to a non-parameterized set then it works, and I confirm this is correct.
A second colleague points out that there are issues with the ub() function as well.
Please see original comments in thread:
https://class.coursera.org/modelingoptimization-001/forum/thread?thread_id=306

fails when range is used

Hello,

I have a simple testcase. The expected answer to the "floors" variable is 205.
Perhaps I am doing something wrong. Thanks for your help.

% ----------------------------

include "globals.mzn";

int: target = 20500 ;

% this works:
var int: floors ;

% But if I replace the above with a range,
% it fails and outputs floors = 1
% but works in minizinc 1.6
% var 1..1000: floors ;

var int: actual = (floors * 10 * 10) ;
constraint actual >= target ;
solve minimize floors ;

output [
"target: ", show(target), "\n",
"actual: ", show(actual), "\n",
"floors: ", show(floors), "\n",
"\n"
] ;

mzn2fzn-2.0.1 generates undocumented count_eq_reif constraints

When I launch mzn2fzn on amaze problems from the 2014 challenge with a redefined count_eq predicate, mzn2fzn generates count_eq_reif constraints which are undocumented in the FlatZinc specification. Is it a new constraint that should be implemented?

Suggestion: add pseudo-boolean (bool_lin_*) constraints

A lot of models make use of pseudo-boolean constraints, which are currently implemented with int_lin_* constraints on boolean variables coerced to Int using bool2int function. This generate many useless variables (one 0/1 and one boolean for each actual decision variable), and potentially many constraints (or other specific solver feature) to enforce the coercion.

Maybe this could be improved if native pseudo-boolean constraints were available.

subset constraint lost when using nosets redefinitions

When I compile the following using mzn2fzn 2.0.1 and the 'nosets' redefinitions.mzn file provided with this version, the subset constraint is lost (if I run it I get an answer of 10).

var set of 1..10: s1;
constraint s1 subset {1,4,10};
var bool: fourin = 4 in s1;
solve :: set_search([s1],input_order,indomain_min,complete)
 maximize card(s1);

Note that if I remove the third line, where fourin is declared, then it works (gives answer 3).

Constraint array_float_element not found

With the following simple traveling salesman model:
https://gist.github.com/kim0/ba480a0f918c41e1a2e9

I get this error when I run it
$ mzn-gecode -a solver-sa.mzn
Error: Registry: Constraint array_float_element not found

minizinc-2.0: how many solutions: 1, 3 or 6?

The attached model has three distinct solutions, but each solution is reported twice.
fzn-gecode -mode gist ...fzn (Gecode-4.3.2) finds the three solutions, no duplicates.
fzn-gecode -a ...fzn reports only the first solution, with no ========.
So, what's the correct number of solutions of this model: 1, 3 or 6?

% minizinc -k -a my_regular_nfa.mzn 
x = [1, 1, 2]
----------
x = [1, 1, 2]
----------
x = [1, 2, 2]
----------
x = [1, 2, 2]
----------
x = [2, 1, 2]
----------
x = [2, 1, 2]
----------
==========

% fzn-gecode -a my_regular_nfa.fzn
x = array1d(1..3, [1, 1, 2]);
----------

my_regular_nfa.mzn:
include "globals.mzn";

int: r = 1;
int: b = 2;

array [1..3] of var r..b: x;
array [int,int] of set of int: d = 
  [|{2,4     }, {5        },
   |{4,6     }, {1,3,5    },
   |{2,6     }, {5        },
   |{2,8     }, {1,5,7    },
   |{2,4,6,8 }, {1,3,7,9  },
   |{2,8     }, {3,5,9    },
   |{4,8     }, {5        },
   |{4,6     }, {5,7,9    },
   |{6,8     }, {5        },
   |];

constraint
  regular_nfa(x, 9, b, d, 1, {9});

solve :: int_search(x, input_order, indomain_min, complete)
  satisfy;

output ["x = \(x)\n"];

my_regular_nfa.fzn:
array [1..18] of set of int: X_INTRODUCED_3 = [{2,4},5..5,{4,6},{1,3,5},{2,6},5..5,{2,8},{1,5,7},{2,4,6,8},{1,3,7,9},{2,8},{3,5,9},{4,8},5..5,{4,6},{5,7,9},{6,8},5..5];
array [1..18] of set of int: X_INTRODUCED_13 = [{2,4},5..5,{4,6},{1,3,5},{2,6},5..5,{2,8},{1,5,7},{2,4,6,8},{1,3,7,9},{2,8},{3,5,9},{4,8},5..5,{4,6},{5,7,9},{6,8},5..5];
array [1..18] of set of int: X_INTRODUCED_17 = [{2,4},5..5,{4,6},{1,3,5},{2,6},5..5,{2,8},{1,5,7},{2,4,6,8},{1,3,7,9},{2,8},{3,5,9},{4,8},5..5,{4,6},{5,7,9},{6,8},5..5];
array [1..18] of set of int: X_INTRODUCED_21 = [{2,4},5..5,{4,6},{1,3,5},{2,6},5..5,{2,8},{1,5,7},{2,4,6,8},{1,3,7,9},{2,8},{3,5,9},{4,8},5..5,{4,6},{5,7,9},{6,8},5..5];
var 1..2: X_INTRODUCED_0;
var 1..2: X_INTRODUCED_1;
var 1..2: X_INTRODUCED_2;
var 1..9: X_INTRODUCED_6 ::var_is_introduced ;
var 1..9: X_INTRODUCED_7 ::var_is_introduced ;
var 1..2: X_INTRODUCED_11 ::var_is_introduced :: is_defined_var;
var set of 1..9: X_INTRODUCED_12 ::var_is_introduced :: is_defined_var;
var 1..18: X_INTRODUCED_15 ::var_is_introduced :: is_defined_var;
var set of 1..9: X_INTRODUCED_16 ::var_is_introduced :: is_defined_var;
var 1..18: X_INTRODUCED_19 ::var_is_introduced :: is_defined_var;
var set of 1..9: X_INTRODUCED_20 ::var_is_introduced :: is_defined_var;
array [1..3] of var 1..2: x:: output_array([1..3]) = [X_INTRODUCED_0,X_INTRODUCED_1,X_INTRODUCED_2];
constraint array_set_element(X_INTRODUCED_11,X_INTRODUCED_13,X_INTRODUCED_12);
constraint set_in(X_INTRODUCED_6,X_INTRODUCED_12);
constraint array_set_element(X_INTRODUCED_15,X_INTRODUCED_17,X_INTRODUCED_16);
constraint set_in(X_INTRODUCED_7,X_INTRODUCED_16);
constraint array_set_element(X_INTRODUCED_19,X_INTRODUCED_21,X_INTRODUCED_20);
constraint set_in(9,X_INTRODUCED_20);
constraint int_lin_eq([1,-1],[X_INTRODUCED_0,X_INTRODUCED_11],0):: defines_var(X_INTRODUCED_11);
constraint int_lin_eq([1,2,-1],[X_INTRODUCED_1,X_INTRODUCED_6,X_INTRODUCED_15],2):: defines_var(X_INTRODUCED_15);
constraint int_lin_eq([1,2,-1],[X_INTRODUCED_2,X_INTRODUCED_7,X_INTRODUCED_19],2):: defines_var(X_INTRODUCED_19);
solve :: int_search(x,input_order,indomain_min,complete) satisfy;

mzn2fzn duplicates non-empty array and loses type of empty array

Hi,
When I compile the following minizinc model, the flatzinc has an extra copy of the non-empty array and type array [1..0] of bot for the empty one.

MiniZinc:

predicate fakepred(array[int] of int: a1, array[int] of int: a2, var int: result);
var 1..5: x;
array[int] of int: a1 = [2, 3];
array[int] of int: a2 = [];
constraint fakepred(a1, a2, x);
solve minimize x;

Flatzinc produced by mzn2fzn 2.0.1:

predicate fakepred(array [int] of int: a1,array [int] of int: a2,var int: result);
array [1..0] of bot: a2 = [];
array [1..2] of int: a1 = [2,3];
array [1..2] of int: X_INTRODUCED_0 = [2,3];
var 1..5: x:: output_var;
constraint fakepred(a1,a2,x);
solve  minimize x;

Failed type inference of anonymous decision variables

Tested in MiniZinc 2.0.2.

Anonymous decision variables don't seem to be coerced to the correct type within array assignments. This would be useful for conditionalizing the size of an array, for example.

Input file:

array [int] of var bool: x = [_ | i in 1..3];
solve satisfy;

Output of mzn2fzn:

input.mzn:1:
MiniZinc: type error: initialisation value for `x' has invalid type-inst: expected `array[int] of var bool', actual `array[int] of ??? '

Two running processes in IDE, one uncontrolled

It is possible to run one model and then a second. Stopping one process is easy, but the other is uncontrolled. Steps to reproduce:

1. open a model in the editor and run it; run button is greyed out and stop button activated
2. make an edit to the model and save it; run button is now activated along with stop button
3. click run; run button is now greyed out, stop is active, two runs now running
4. click stop; stop is now greyed, one process stops, but the other keeps running
5. close IDE to stop the run and reset the IDE.

`minizinc -c` results in `sh: 1: solns2dzn: not found`

For testing, I want to solve some MiniZinc problem, ignoring the "output" section (so that I can reinject the solution into the MiniZinc file to verify it using another solver). It seems that there is no much documentation about the "minizinc" and "flatzinc" commands themselves, I thought the "-c" parameter would do the job, but it seems that it is broken.

Set literal 1..0

The program generates set_eq_reif with one set literal 1..0. Possibly it should be an empty file. I cannot attach the file but can send it on request.

mzn2fzn v2.0 drops output variables

Output variables aren't included in the FlatZinc generated by mzn2fzn (v2.0) if they can be reduced to an equivalent variable.

Example MiniZinc:

var 0..1: x;
var int: y = x;
solve maximize x;
output [show(x), show(y)];

Resulting FlatZinc using mzn2fzn v1.6:

var 0..1: x :: output_var;
var 0..1: y :: output_var = x;
solve maximize x;

Resulting FlatZinc using mzn2fzn v2.0:

var 0..1: x:: output_var;
solve  maximize x;

This becomes more of an issue when y reduces to x through a more complex expression, or when the MiniZinc model is itself the result of a generation tool. I.e., when the relationship between equivalent variables is unclear, and one of them is not included in the FlatZinc, deciphering the output of the FlatZinc solver can become difficult.

Arithmetic Operation on Infinite Value Error - Option Types

The following code from the paper "Modelling with Option Types in MiniZinc" throws the error:
MiniZinc: arithmetic error: arithmetic operation on infinite value

NOTE: Hopefully I haven't made a silly mistake with the allowable input parameter values.

Side note: It might also be a good time to point out that the arguments to a number of the scheduling global constraints are miss-specified. Several constrains list "var int" when it should only be "int". It would be worth giving the global constraints a review because I have encountered other mistakes as well.

include "globals.mzn";

% Example 11. A MINIZINC model for flexible job shop scheduling as discussed in Example
% 1 is shown below. Note that the optional variables are used to give start times for
% the version of the tasks starting on each machine. The disjunctive constraint is the
% version lifted for option types. The alternative constraints are directly defined on
% option types; they enforce the span constraint (see Example 10) as well as ensuring at
% most one optional task actually occurs. The redundant cumulative constraint ensures
% no more than k tasks run at one time. The aim is to minimize the latest end time.

int: horizon = 300; % time horizon
set of int: Time = 0..horizon;
int: n = 10; % number of tasks
set of int: Task = 1..n;
int: k = 10; % number of machines
set of int: Machine = 1..k;
array[Task,Machine] of int: d = [| 
1,2,3,4,5,6,7,8,9,10,|
1,2,3,4,5,6,7,8,9,10,|
1,2,3,4,5,6,7,8,9,10,|
1,2,3,4,5,6,7,8,9,10,|
1,2,3,4,5,6,7,8,9,10,|
1,2,3,4,5,6,7,8,9,10,|
1,2,3,4,5,6,7,8,9,10,|
1,2,3,4,5,6,7,8,9,10,|
1,2,3,4,5,6,7,8,9,10,|
1,2,3,4,5,6,7,8,9,10 |];
int: maxd = max([ d[t,m] | t in Task, m in Machine ]);
int: mind = min([ d[t,m] | t in Task, m in Machine ]);
array[Task] of var Time: S;
array[Task] of var mind..maxd: D;
array[Task,Machine] of var opt Time: O;

constraint 
forall(m in Machine)
(
  disjunctive([O[t,m] | t in Task], [d[t,m] | t in Task])
);

constraint 
forall(t in Task)(
    alternative(S[t], 
                D[t], 
                [O[t,m] | m in Machine], 
                [d[t,m] | m in Machine])
);

constraint cumulative(S, D, [1 | i in Task], k);

solve minimize max(t in Task)(S[t] + D[t]);

Variable defined by wrong constraint

Flattening parity-learning.mzn with 44_22_5.2.dzn (from the minizinc-benchmark), leads to a flatzinc file containing the following lines:

array [1..23] of var bool: X_INTRODUCED_207 ::var_is_introduced  = [X_INTRODUCED_206,X_INTRODUCED_0,X_INTRODUCED_1,X_INTRODUCED_2,X_INTRODUCED_3,X_INTRODUCED_4,false,false,false,X_INTRODUCED_8,X_INTRODUCED_9,X_INTRODUCED_10,false,X_INTRODUCED_12,X_INTRODUCED_13,X_INTRODUCED_14,X_INTRODUCED_15,false,false,false,false,X_INTRODUCED_20,false];
constraint array_bool_xor(X_INTRODUCED_207):: defines_var(X_INTRODUCED_25);

The second line tells that X_INTRODUCED_25 is defined by the constraint, but the array X_INTRODUCED_207 does not contain that variable. The other lines containing variable "_25" are:

var bool: X_INTRODUCED_25:: is_defined_var;
array [1..44] of var bool: computed_parities:: output_array([1..44]) = [X_INTRODUCED_22,X_INTRODUCED_23,X_INTRODUCED_24,X_INTRODUCED_25,X_INTRODUCED_26, .... ];
constraint bool_xor(false,X_INTRODUCED_25,X_INTRODUCED_72):: defines_var(X_INTRODUCED_72);
constraint bool_eq_reif(X_INTRODUCED_25,false,X_INTRODUCED_206):: defines_var(X_INTRODUCED_206);

Variable "_206" in the last line appears in the array "_207", so there is indeed a link but a step is missing.

Allow creation of arrays of unknown length

Hi,
there was some ambition in 2011 to allow the declaration of arrays without a length, if they are initialized with constant data (see page 8 of http://www.minizinc.org/workshop2011/report.pdf). To my knowledge this still isn't possible—if that's so, are there efforts underway to allow this?

Cheers :)

intersect set operator type error (MiniZinc 2)

MiniZinc 2 currently raises the following type error when I use the intersect set operator and then compile using mzn2fzn.exe on Windows 7:

MiniZinc: type error: type error in operator application for 'intersect'. No matching operator found with left-hand side type 'int' and right-hand side type 'set of int'.

Changing the operator from intersect to union results in the minizinc to flatzinc conversion executing without error.

Also, note that the minizinc tutorial at:
http://www.minizinc.org/downloads/doc-latest/minizinc-tute.pdf
lists the intersection operator as "inter" instead of "intersect".

mzn2fzn --no-output-ozn generates an output file

An invocation of
mzn2fzn --no-out-ozn <model>.mzn [<data>.dzn ...]
or
mzn2fzn -O- <model>.mzn [<data>.dzn ...]
should not produce the ozn-output file, but it does for MiniZinc 2.0.2.

solns2out memory leak

There is a bug (in 2.0.4 and HEAD) where solns2out does not garbage collect the literals that it creates, which means that it uses a lot of memory when all solutions are being printed for a problem with a lot of solutions. I didn't fully debugged it, so I'm not exactly sure where the issue is.

I am running on Linux 4.1.2, gcc 4.9.3, I haven't tried reproducing on other operating systems.

It can be reproduced by running minizinc with all solutions turned on for a very simple example (see below). Using "MINIZINC_GC_STATS" showed a rapid increase in memory use. Using another solver (eg. gecode) which spits out solutions faster helps. Testing using cgroups to limit it to 16GB results in it being killed (or alternately 32GB for some cases where I forgot to limit it with cgroups).

minizinc -a example.mzn > /dev/null

% memory leak is more obvious for a higher value of n
int: n = 1000;
array[1..n] of var 1..n: x;
solve satisfy;

Value change of par floats during flattening using MiniZinc 2.0.x

Given the following MiniZinc model, the par float 12.8 becomes 12.800000000000001, which will cut, e.g., the solution f = 12.8;

float: a = 12.8;
float: b = 40.0;
var float: f;
constraint a <= f /\ f <= b;
solve satisfy;

The generated FlatZinc model using MiniZinc 2.0.x:

var float: f:: output_var;
constraint float_le(f,40.0);
constraint float_le(12.800000000000001,f);
solve  satisfy;

Interestingly, MiniZinc 1.6 not only generates an equivalent FlatZinc model, but also simplifies the model:

var 12.8..40.0: f;
solve satisfy;

Bug in the Linux version of MiniZinc 2.0.6

I have downloaded the MiniZinc IDE 0.9.9/2.0.6 bundle for a Mac and a Linux machine. The following model is solved correctly on the Mac OS version but not on the Linux one:

set of int: range = 1..4;

array [range] of var bool: run;
array [range] of var int: acc;

constraint not(run[1]) /\ run[2] /\ not(run[3]) /\ run[4];

function array [range] of var int: conf(
        array [range] of var bool: run
    ) = let {
        array [range] of var int: acc;
        constraint acc[1] = bool2int(run[1]);
        constraint forall (i in 2..4) (
            (acc[i] = acc[i-1] + bool2int(run[i]))
        )
    } in acc
;

constraint let {
    int: period = 2;
    array[range] of var int: acc1 = conf(run);
  } in
    forall (i in range) (
      acc[i] = (acc1[i]) div period
    );

solve satisfy;

output ["acc: \(acc)\n"];

In Linux, for the Gecode solver it simply says unsatisfiable while the g12 solver reports model inconsistency.
However, when I copy the .fzn file produced on the Mac machine to the Linux machine, it runs correctly with fzn-gecode.

Variable defined by more than one constraint

Not sure this is a bug or a feature ;-), but it is new to release 2.0.2: some variables appear in more than one "defines_var" annotation. This is the case for several variables in the model "javarouting/trip_6_3.mzn" from the minizinc-benchmark and MiniZinc Challenge 2013.

JN

CMAKE_OSX_DEPLOYMENT_TARGET pinned at 10.7

Is MiniZinc unsupported on newer versions of OSX, or can this be changed to detect the SDK version?

minizinc-2.0: 2 or 4 solutions?

model:

include "globals.mzn";

var set of 1..2: x;
array[1..2] of var bool: y;

constraint
  x = {1} /\
  forall(i in x)(y[i]);

solve satisfy;

output [
  "x = ", show(x), "\n",
  "y = ", show(y), "\n",
  ];

run:

solovej>minizinc -a bug.mzn
x = 1..1
y = [true, false]
----------
x = 1..1
y = [true, false]
----------
x = 1..1
y = [true, true]
----------
x = 1..1
y = [true, true]
----------
==========
solovej>mzn-gecode -a bug.mzn
x = 1..1
y = [true, false]
----------
x = 1..1
y = [true, true]
----------
==========

Why are there multiple copies of solutions in the first query?

v.2.0.4: "internal error: undeclared function or predicate var_dom"

The following model cause mzn2fzn to panic with error:
"MiniZinc: internal error: undeclared function or predicate var_dom"

set of int: smallset = 0..10;
array[1..2, 1..4] of var smallset: X;
constraint forall( i in 1..2 ) (
let {
  array[int] of var smallset: Y = row(X, i);
} in
  Y[1] == 3 % Any use of Y triggers the issue.
);
solve satisfy;

There was an old issue with the same symptom: http://www.minizinc.org/trac/ticket/91 .

I have reproduced the issue on mzn2fzn v2.0.2 and v2.0.4.

Emptied domain

The following model (trimmed down from the bacp model of the 2010 challenge) is incorrectly flattened by MiniZinc 2.0.1. In particular, the domain of neg_obj is wrongly computed.

var 2..100: objective;
var -100..-2 : neg_obj = -objective;
solve minimize neg_obj;

result:

var 2..100: objective:: output_var;
var 1..0: neg_obj:: is_defined_var;
constraint int_lin_eq([-1,-1],[objective,neg_obj],0):: defines_var(neg_obj);
solve  minimize neg_obj;

Cheers,
JN

Inconsistency in results between MiniZinc 1.6 and 2.0.4

Results from the MiniZinc challenge 2013 show that all solvers find an optimal solution of 1046 for the Radiation i8-7 problem.

Ran with MiniZinc 2.0.4, both my solver and the G12-fd solver find an optimal solution of 118. One of the two versions of MiniZinc are thus probably bugged.

xor problem (minizinc-2.0 + opturion-cpx)

If I do:

FLATZINC_CMD=fzn-cpx minizinc -G opturion-cpx foo.mzn

on foo.mzn:

var bool: x;
var bool: y;

constraint x xor y;

solve satisfy;

output [ "x=", show(x), "\n"
   , "y=", show(y), "\n"
   ];

I get foo.fzn:

predicate bool_xor(var bool: a,var bool: b,var bool: r) = array_bool_even([a,b,r]);
var bool: x:: output_var;
var bool: y:: output_var;
constraint bool_xor(x,y,true);
solve  satisfy;

which doesn't run:

Opturion CPX(tm) Optimizer version 1.0.2.
Academic license, issued to [email protected]. 
Error: syntax error, unexpected '=', expecting ';' in line no. 1

Evidently, the definition of bool_xor/3 was copied into foo.fzn from the redefinitions.mzn that comes with the Opturion CPX distribution.

How come bool_xor(x,y,true) wasn't unfolded to array_bool_even(x,y,true), and is the definition of bool_xor/3 legal FlatZinc at all? This worked with MiniZinc 1.6. Is there a work-around?

annotation functions

Hi,

I am trying to use annotation functions but I ran accross some problem. Here is my code:

annotation simpleann;
annotation composeann(ann: s);
function ann: annfunc(ann: s) = composeann(s);
solve :: annfunc(composeann(simpleann)) satisfy;

The annotation function works fine if the passed annotation does not take any argument but it crashes if the passed annotation takes an argument as in the example above. The error message is:

mzn2fzn: /home/janho/programs/libminizinc/include/minizinc/ast.hh:198: T* MiniZinc::Expression::cast() [with T = MiniZinc::VarDecl]: Assertion `isa<T>()' failed.
Aborted

Is this a bug or am I simply hitting the limits of mzn2fzn?

Includes are not equivalent to concatenation (Arrays seem to differ).

An array defined in an included file will lead to:

T* MiniZinc::Expression::cast() [with T = MiniZinc::ArrayLit]:Assertion`isa<T>()` failed.
Aborted (core dumped)

While if the include is replaced by the contents of the included file, no such assertion is thrown.

Trivial example (tested in 2.0.4):
If you have two files:
main.mzn:

include "array.mzn"

var 0..0 index;

constraint(inner_array[index] == 1);

solve::int_search([index], first_fail, indomain_random, complete) satisfy;

And array.mzn:

array[0..0] of int: inner_array = array1d(0..0, [1]);

That will fail.

However:

array[0..0] of int: inner_array = array1d(0..0, [1]);

var 0..0 index;

constraint(inner_array[index] == 1);

solve::int_search([index], first_fail, indomain_random, complete) satisfy;

In a single file works. From what I can see in the MiniZinc specification, includes should behave much like in C (i.e. simple concatenation), so this seems like a bug.

Issue with optimized compilation for partially defined mydiv function

When trying the user-defined partial function example mydiv from the Coursera class, I noticed some problems with compiler optimizations (also here Gist) :

function var int:mydiv(var int: x, var int: y) = 
  assert(lb(x) >= 0 /\ lb(y) >= 0,
         "Mydiv got wrong arguments",
         let {constraint y != 0 } in 
         safediv(x, y)
);

function var int: safediv(var int: x, var int: y)   :: promise_total = 
  let {
    var 0..ub(x): q;
    var 0..ub(y)-1: r;
    constraint q*y + r = x;
    constraint r < y;
  }  in q;

var int: x;
var int: y; 
var int: z;

constraint x = 7;
constraint y = 1;
constraint z = mydiv(x,y);

% should return z = 7
solve satisfy;

which returns { (7,1,i) | i in 0..7} as solution set when producing optimized FlatZinc.

*. When declaring var 0..ub(y)-1: r; as var int: r;' with optimized FlatZinc, the correct (only) solution(7,1,7)` is returned. Then, the constraints

array [1..3] of int: X_INTRODUCED_5 = [1,-1,-1];
array [1..2] of int: X_INTRODUCED_6 = [1,-1];

are present, whereas they weren't in the original version. The original FlatZinc is obscurely small:

var 0..7: z:: output_var;
solve  satisfy;

• When compiling the model without the flag for optimized FlatZinc, I get the correct solution set.

I'm using the bundled MiniZinc IDE, Version 0.9.9.

Easy displaying of 2d tables?

Why does MiniZinc not provides an easy way to display 2d tables? They are systematically flattened and always require to check for end of row… Maybe an extra show2d construct could be provided?

System crash on attempt stop compile of large fzn

On openSUSE 13.2 minizinc 0.9.9, attempting to stop the compile generation using the stop button in the IDE of a large fzn results in a system crash. Might be advisable to deactivate the Stop button during compile process unless there is a trap to ensure a clean stop. In many cases the compile happens really fast, so not a problem.

segfault with conditional in var comprehension

The following code

var 1..1: i;
predicate losseq(array[int] of var int: a) = sum([1 | e in a where e >= 1]) = 1;
constraint losseq([0]);
solve satisfy;

results in a segfault when run from the terminal with command

$ /Applications/MiniZincIDE.app/Contents/Resources/mzn2fzn debug.mzn  -Ggecode
[1]    26370 segmentation fault  /Applications/MiniZincIDE.app/Contents/Resources/mzn2fzn debug.mzn -Ggecode

I'm using The MiniZinc IDE Version 0.9.9.

g12-lazy backend generates wrong solution (set_in_reif )

g12-lazy backend generates wrong solution.

test.fzn

var -10..10 : X1 :: output_var;
var bool : B1;

constraint set_in_reif(2, -3..3, B1);
constraint int_eq_reif(X1, 3, B1);

solve maximize X1;

flatzinc -b lazy test.fzn

X1 = 10;
----------
==========

flatzinc -b fd test.fzn

X1 = 3;
----------
==========

Similar problem will be happen with carpet-cutting benchmark included in MiniZinc 1.6 distribution.

Bug: Constraint disregarded in very peculiar cases.

Hi, I have encountered an interesting bug. In the following model, the constraint is completely disregarded, unless I use the function elsewhere.

set of int: idx_set = 1..2;

array[idx_set] of int: t1 = [0, 2];
array[idx_set] of int: t2 = [0, -2];

var 0..1: negative;

function var int:
select_negative(var int: idx) = t2[idx];

function var int:
select_positive(var int: idx) = t1[idx];


function var int:
select(var int: idx) =
    if negative == 0 then
        select_positive(idx)
    else
        select_negative(idx)
    endif
    ;

var idx_set: idx;
var -2..2: result;

constraint ( ( select(idx) != 0) -> (result == select(idx)) );

% Uncommenting any of these blocks makes the issue disappear.
% Block 1
% var int: result2;
% constraint ( result2 == select(idx));

% Block 2
%constraint ( ( select_positive(idx) != 0) -> (result == select(idx)) );

% Block 3
% Replacing the constraint above with this also works.
%constraint (
%    let { var int: x = select(idx) } in
%    ( x != 0) -> (result == x)
%);


solve satisfy;

When solved with fzn-gecode -a I expect there to be exactly two solutions for idx == 2, i.e. one for negative == 1 and one for negative == 0. Uncommenting any of the listed blocks produces the expected output.

Jump to error from error message

Hi,
On linux clicking on an error message in the lower screen links to the line with the error in it in the upper screen
This doesn't work in Windows

not a bool expression '='

Tested in MiniZinc 2.0.2.

Input file:

constraint has_element(2, [1,2,3]);
solve maximize 0;

Output of mzn2fzn:

MiniZinc: evaluation error: 
  input.mzn:1:
  in call 'has_element'
  /opt/minizinc-2.0.4/bin/../share/minizinc/std/builtins.mzn:918:
  in call 'exists'
    with i = 1
  in binary '=' operator expression
  not a bool expression '='

However, the following two input files run without error.

constraint exists (i in index_set([1,2,3])) ([1,2,3][i]=2);
solve maximize 0;

test has_element_int(int: e, array[int] of int: x) = exists (i in index_set(x)) (x[i]=e);
constraint has_element_int(2, [1,2,3]);
solve maximize 0;

Uncontrolled allocation of memory with var set in function let statement

FWIW I have a crash in Minizinc under the following circumstances using openSUSE Linux fully updated:
With configuration set to 1 cpu and print all solutions, I focus on a let{} inside a function where I have a "var set of int" statement.
If I assign a set to this token with a "x = y" plain assignment, all is well and Minizinc produces a solution.
However if I convert the plain assignment to a "var set of int: x, constraint x == blah" then all memory on machine is consumed, system becomes sluggish, eventually I can kill the process and system returns to normal.
Using the more restrictive "var set of [defined set in here]: x" produces a solution correctly with the constraint version.
So there appears to be uncontrolled allocation of memory with the "var set of int" version.
I won't post the code here since it relates to a Coursera course assignment.

row() and col() functions for variable matrices

There are MiniZinc builtins for row() and col() projection of matrices of parameters. I recently modelled timetabling problems where I required such projections for matrices of variables, which do not seem to be provided. I could implement them easily, maybe they could be added to builtins:

function array [int] of var int: col(array [int, int] of var int: tab, par int: c) = 
  [tab[i, c] | i in index_set_1of2(tab)];
function array [int] of var int: row(array [int, int] of var int: tab, par int: r) = 
  [tab[r, i] | i in index_set_2of2(tab)];