this repo has no description
dekker.one
1% RUNS ON mzn20_fd
2% RUNS ON mzn-fzn_fd
3% RUNS ON mzn20_fd_linear
4% RUNS ON mzn20_mip
5
6% Regression test for bug #380 - the body of the lex_leq_bool_half was being
7% flattened in a reified context. (The reification context was not being
8% correctly reset after the application arguments had been flattened.)
9
10int: n = 4;
11set of int: N = 1..n;
12
13array[N,N] of var bool: a;
14array[N] of var 3..n-1: d;
15
16int: i = 2;
17
18constraint
19 lex_lesseq_bool_half([ a[i,j+1] | j in N where j != i /\ j != i+1 ],
20 [ a[i,j] | j in N where j != i /\ j != i+1 ],
21 d[i] = d[i+1] );
22
23solve satisfy;
24
25output ["d = array1d(1..4, ", show(d), ");\n"];
26
27
28% half reified version of lex_lesseq for Booleans, that is
29% h -> lex_lesseq(x,y)
30predicate lex_lesseq_bool_half(array[int] of var bool: x,
31 array[int] of var bool: y,
32 var bool: h) =
33 let { int: lx = min(index_set(x)),
34 int: ux = max(index_set(x)),
35 int: ly = min(index_set(y)),
36 int: uy = max(index_set(y)),
37 int: size = max(ux - lx, uy - ly),
38 array[0..size] of var bool: b }
39 % b[i] is true if the lexicographical order holds from position i on.
40 in
41 (h -> b[0])
42 /\
43 forall(i in 0..size) (
44 b[i] = ( x[lx + i] <= y[ly + i]
45 /\
46 if i = size then true
47 else x[lx + i] < y[ly + i] \/ b[i+1] endif
48 )
49 );