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