Skip to content

Commit

Permalink
Release MiniZinc 2.8.2
Browse files Browse the repository at this point in the history
  • Loading branch information
cyderize committed Dec 15, 2023
1 parent 24d4a71 commit 3a5924b
Show file tree
Hide file tree
Showing 1,147 changed files with 168,396 additions and 371 deletions.
8 changes: 4 additions & 4 deletions _data/version.yaml
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
mznversion: 2.8.1
mzndate: "27 November 2023"
ideversion: 2.8.1
idedate: "27 November 2023"
mznversion: 2.8.2
mzndate: "15 December 2023"
ideversion: 2.8.2
idedate: "15 December 2023"
minisearchversion: 0.1.0b1
minisearchdate: "28 August 2015"

Expand Down
Binary file added doc-2.8.2/chi/MiniZinc Handbook.pdf
Binary file not shown.
245 changes: 245 additions & 0 deletions doc-2.8.2/chi/basic_steps.html

Large diffs are not rendered by default.

3,298 changes: 3,298 additions & 0 deletions doc-2.8.2/chi/changelog.html

Large diffs are not rendered by default.

554 changes: 554 additions & 0 deletions doc-2.8.2/chi/checkers.html

Large diffs are not rendered by default.

912 changes: 912 additions & 0 deletions doc-2.8.2/chi/command_line.html

Large diffs are not rendered by default.

615 changes: 615 additions & 0 deletions doc-2.8.2/chi/cpprofiler.html

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
include "alldifferent.mzn";

int: S;
int: N = S * S;
int: digs = ceil(log(10.0,int2float(N))); % 输出的数字

set of int: PuzzleRange = 1..N;
set of int: SubSquareRange = 1..S;

array[1..N,1..N] of 0..N: start; %% 板初始0 = 空
array[1..N,1..N] of var PuzzleRange: puzzle;

% 填充初始板
constraint forall(i,j in PuzzleRange)(
if start[i,j] > 0 then puzzle[i,j] = start[i,j] else true endif );

% 每行中取值各不相同
constraint forall (i in PuzzleRange) (
alldifferent( [ puzzle[i,j] | j in PuzzleRange ]) );

% 每列中取值各不相同
constraint forall (j in PuzzleRange) (
alldifferent( [ puzzle[i,j] | i in PuzzleRange ]) );

% 每个子方格块中取值各不相同
constraint
forall (a, o in SubSquareRange)(
alldifferent( [ puzzle[(a-1) *S + a1, (o-1)*S + o1] |
a1, o1 in SubSquareRange ] ) );

solve satisfy;

output [ show_int(digs,puzzle[i,j]) ++ " " ++
if j mod S == 0 then " " else "" endif ++
if j == N then
if i != N then
if i mod S == 0 then "\n\n" else "\n" endif
else "" endif else "" endif
| i,j in PuzzleRange ] ++ ["\n"];
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
int: wa;
int: nt;
int: sa;
int: q;
int: nsw;
int: v;
int: t;

test check(bool: b,string: s) =
if b then true else trace_stdout("ERROR: "++s++"\n",false) endif;

array[int] of bool: checks = [
check(wa!=nt, "wa and nt have the same colour"),
check(wa!=sa, "wa and sa have the same colour"),
check(nt!=sa, "nt and sa have the same colour"),
check(nt!=q, "nt and q have the same colour"),
check(sa!=q, "sa and q have the same colour"),
check(sa!=nsw, "sa and nsw have the same colour"),
check(sa!=v, "sa and v have the same colour"),
check(q!=nsw, "q and nsw have the same colour"),
check(nsw!=v, "nsw and v have the same colour")
];

output [
if forall(checks)
then "CORRECT: all constraints hold.\n"
else "INCORRECT\n"
endif
];
Original file line number Diff line number Diff line change
@@ -0,0 +1,43 @@
include "ide/vis.mzn";

int: n_colors;

enum PALETTE = { red, lime, blue, cyan, magenta, yellow, orange };
set of PALETTE: COLOR = to_enum(PALETTE, 1..n_colors);

% Color for each region
var COLOR: wa;
var COLOR: nt;
var COLOR: sa;
var COLOR: q;
var COLOR: nsw;
var COLOR: v;
var COLOR: t;

% Neighboring regions have different colours
constraint wa != nt;
constraint wa != sa;
constraint nt != sa;
constraint nt != q;
constraint sa != q;
constraint sa != nsw;
constraint sa != v;
constraint q != nsw;
constraint nsw != v;

% Data to send during initialisation of the visualisation
any: initial_data = (n: n_colors);

% Data to send on each solution
% Note the use of :: output_only
any: solution_data :: output_only = (
wa: show(wa), % Get colors as strings
nt: show(nt),
sa: show(sa),
q: show(q),
nsw: show(nsw),
v: show(v),
t: show(t)
);
% Launch the visualisation
output :: vis_server("vis_aust.html", initial_data) solution_data;
36 changes: 36 additions & 0 deletions doc-2.8.2/chi/downloads/0c6bf095aa185af296b6e6e6c9908455/meal.mzn
Original file line number Diff line number Diff line change
@@ -0,0 +1,36 @@
% 规划均衡的膳食
include "table.mzn";
int: min_energy;
int: min_protein;
int: max_salt;
int: max_fat;
set of FOOD: desserts;
set of FOOD: mains;
set of FOOD: sides;
enum FEATURE = { name, energy, protein, salt, fat, cost};
enum FOOD;
array[FOOD,FEATURE] of int: dd; % 食物数据库

array[FEATURE] of var int: main;
array[FEATURE] of var int: side;
array[FEATURE] of var int: dessert;
var int: budget;

constraint main[name] in mains;
constraint side[name] in sides;
constraint dessert[name] in desserts;
constraint table(main, dd);
constraint table(side, dd);
constraint table(dessert, dd);
constraint main[energy] + side[energy] + dessert[energy] >=min_energy;
constraint main[protein]+side[protein]+dessert[protein] >=min_protein;
constraint main[salt] + side[salt] + dessert[salt] <= max_salt;
constraint main[fat] + side[fat] + dessert[fat] <= max_fat;
constraint budget = main[cost] + side[cost] + dessert[cost];

solve minimize budget;

output ["main = ",show(to_enum(FOOD,main[name])),
", side = ",show(to_enum(FOOD,side[name])),
", dessert = ",show(to_enum(FOOD,dessert[name])),
", cost = ",show(budget), "\n"];
Original file line number Diff line number Diff line change
@@ -0,0 +1,38 @@
% 为校园游乐会做蛋糕(和数据文件一起)

int: flour; %拥有的面粉克数
int: banana; %拥有的香蕉个数
int: sugar; %拥有的糖克数
int: butter; %拥有的黄油克数
int: cocoa; %拥有的可可粉克数

constraint assert(flour >= 0,"Invalid datafile: " ++
"Amount of flour should be non-negative");
constraint assert(banana >= 0,"Invalid datafile: " ++
"Amount of banana should be non-negative");
constraint assert(sugar >= 0,"Invalid datafile: " ++
"Amount of sugar should be non-negative");
constraint assert(butter >= 0,"Invalid datafile: " ++
"Amount of butter should be non-negative");
constraint assert(cocoa >= 0,"Invalid datafile: " ++
"Amount of cocoa should be non-negative");

var 0..100: b; % 香蕉蛋糕的个数
var 0..100: c; % 巧克力蛋糕的个数

% 面粉
constraint 250*b + 200*c <= flour;
% 香蕉
constraint 2*b <= banana;
% 糖
constraint 75*b + 150*c <= sugar;
% 黄油
constraint 100*b + 150*c <= butter;
% 可可粉
constraint 75*c <= cocoa;

% 最大化我们的利润
solve maximize 400*b + 450*c;

output ["no. of banana cakes = \(b)\n",
"no. of chocolate cakes = \(c)\n"];
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
int: x = 3;
int: y = 4;
predicate smallx(var int:y) = -x <= y /\ y <= x;
predicate p(int: u, var bool: y) =
exists(x in 1..u)(y \/ smallx(x));
constraint p(x,false);
solve satisfy;
21 changes: 21 additions & 0 deletions doc-2.8.2/chi/downloads/1011d5e79df40aa13b0423339f3ca014/cakes.mzn
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
% 为校园游乐会做蛋糕

var 0..100: b; % 香蕉蛋糕的个数
var 0..100: c; % 巧克力蛋糕的个数

% 面粉
constraint 250*b + 200*c <= 4000;
% 香蕉
constraint 2*b <= 6;
% 糖
constraint 75*b + 150*c <= 2000;
% 黄油
constraint 100*b + 150*c <= 500;
% 可可粉
constraint 75*c <= 500;

% 最大化我们的利润
solve maximize 400*b + 450*c;

output ["no. of banana cakes = \(b)\n",
"no. of chocolate cakes = \(c)\n"];
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
I = 0.04;
P = 1000.0;
B4 = 0.0;
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
include "cumulative.mzn";

enum OBJECTS;
array[OBJECTS] of int: duration; % duration to move
array[OBJECTS] of int: handlers; % number of handlers required
array[OBJECTS] of int: trolleys; % number of trolleys required

int: available_handlers;
int: available_trolleys;
int: available_time;

array[OBJECTS] of var 0..available_time: start;
var 0..available_time: end;

constraint cumulative(start, duration, handlers, available_handlers);
constraint cumulative(start, duration, trolleys, available_trolleys);

constraint forall(o in OBJECTS)(start[o] +duration[o] <= end);

solve minimize end;

output [ "start = \(start)\nend = \(end)\n"];
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
n = 5;
rankWomen =
[| 1, 2, 4, 3, 5,
| 3, 5, 1, 2, 4,
| 5, 4, 2, 1, 3,
| 1, 3, 5, 4, 2,
| 4, 2, 3, 5, 1 |];

rankMen =
[| 5, 1, 2, 4, 3,
| 4, 1, 3, 2, 5,
| 5, 3, 2, 4, 1,
| 1, 5, 4, 3, 2,
| 4, 3, 2, 1, 5 |];
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
% 位 x 的的总和 = 二元表示的 s。
% s[0], s[1], ..., s[k] 其中 2^k >= length(x) > 2^(k-1)
predicate binary_sum(array[int] of var bool:x,
array[int] of var bool:s)=
let { int: l = length(x) } in
if l == 1 then s[0] = x[1]
elseif l == 2 then
s[0] = (x[1] xor x[2]) /\ s[1] = (x[1] /\ x[2])
else let { int: ll = (l div 2),
array[1..ll] of var bool: f = [ x[i] | i in 1..ll ],
array[1..ll] of var bool: t = [x[i]| i in ll+1..2*ll],
var bool: b = if ll*2 == l then false else x[l] endif,
int: cp = floor(log2(int2float(ll))),
array[0..cp] of var bool: fs,
array[0..cp] of var bool: ts } in
binary_sum(f, fs) /\ binary_sum(t, ts) /\
binary_add(fs, ts, b, s)
endif;

% 把两个二元数值 x 和 y 加起来,位 ci 用来表示进位,来得到二元 s
predicate binary_add(array[int] of var bool: x,
array[int] of var bool: y,
var bool: ci,
array[int] of var bool: s) =
let { int:l = length(x),
int:n = length(s), } in
assert(l == length(y),
"length of binary_add input args must be same",
assert(n == l \/ n == l+1, "length of binary_add output " ++
"must be equal or one more than inputs",
let { array[0..l] of var bool: c } in
full_adder(x[0], y[0], ci, s[0], c[0]) /\
forall(i in 1..l)(full_adder(x[i], y[i], c[i-1], s[i], c[i])) /\
if n > l then s[n] = c[l] else c[l] == false endif ));

predicate full_adder(var bool: x, var bool: y, var bool: ci,
var bool: s, var bool: co) =
let { var bool: xy = x xor y } in
s = (xy xor ci) /\ co = ((x /\ y) \/ (ci /\ xy));
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
include "alldifferent.mzn";

int: n;

array[1..n] of var 1..n: x; % sequence of numbers
array[1..n-1] of var 1..n-1: u; % sequence of differences

constraint alldifferent(x);
constraint alldifferent(u);
constraint forall(i in 1..n-1)(u[i] = abs(x[i+1] - x[i]));

solve :: int_search(x, first_fail, indomain_min)
satisfy;
output ["x = \(x);\n"];
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
% latin_squares.mzn
include "globals.mzn";

int: n = 3;
set of int: N = 1..n;
array[N, N] of var N: X;

constraint :: "ADRows"
forall (i in N)
(alldifferent(X[i,..]) :: "AD(row \(i))"
);
constraint :: "ADCols"
forall (j in N)
(alldifferent(X[..,j]) :: "AD(col \(j))"
);

constraint :: "LLRows"
forall (i in 1..n-1)
(lex_less(X[i,..], X[i+1,..]) :: "LL(rows \(i) \(i+1))"
);
constraint :: "LGCols"
forall (j in 1..n-1)
(lex_greater(X[..,j], X[..,j+1]) :: "LG(cols \(j) \(j+1))"
);

solve satisfy;

output [ show2d(X) ];
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
JOB = _(1..5);
TASK = _(1..5);
d = [| 1, 4, 5, 3, 6
| 3, 2, 7, 1, 2
| 4, 4, 4, 4, 4
| 1, 1, 1, 6, 8
| 7, 3, 2, 2, 1 |];
Loading

0 comments on commit 3a5924b

Please sign in to comment.