1/*%-----------------------------------------------------------------------------%
2% Domain encodings
3%-----------------------------------------------------------------------------%
4*/
5% Linear equality encoding
6
7    % Single variable:  x = d  <->  x_eq_d[d]
8predicate equality_encoding(var int: x, array[int] of var int: x_eq_d) =
9    x in index_set(x_eq_d)
10    /\
11    sum(d in dom(x))(     x_eq_d[d] ) = 1
12    /\
13    sum(d in dom(x))( d * x_eq_d[d] ) = x
14    /\
15%    my_trace( "eq_enc: \(x), index_set(pp)=" ++ show(index_set( x_eq_d )) ++ "\n" ) /\
16    if fPostprocessDomains then
17      equality_encoding__POST(x, x_eq_d)
18    else true endif
19    ;
20
21    % Two variables:  x = d /\ y = e  <->  x_eq_d[d] /\ y_eq_e[e] /\ xy_eq_de[d, e]
22predicate equality_encoding(var int: x, var int: y,
23      array[int] of var int: x_eq_d,
24      array[int] of var int: y_eq_e,
25      array[int, int] of var int: xy_eq_de
26      ) =
27    x in index_set(x_eq_d) /\
28    y in index_set(y_eq_e) /\
29    index_set(x_eq_d) == index_set_1of2(xy_eq_de) /\
30    index_set(y_eq_e) == index_set_2of2(xy_eq_de) /\
31    sum(d in dom(x), e in dom(y))( xy_eq_de[d, e] ) = 1
32    /\
33    forall(d in dom(x)) (sum(e in dom(y))( xy_eq_de[d, e] ) = x_eq_d[d])
34    /\
35    forall(e in dom(y)) (sum(d in dom(x))( xy_eq_de[d, e] ) = y_eq_e[e])
36    ;
37
38    % Array of variables:  x[i] = d  <->  x_eq_d[i,d]
39predicate equality_encoding(array[int] of var int: x,
40                            array[int, int] of var int: x_eq_d) =
41    forall(i in index_set(x))(
42        x[i] in index_set_2of2(x_eq_d)
43        /\
44        sum(d in index_set_2of2(x_eq_d))(     x_eq_d[i,d] ) = 1
45        /\
46        sum(d in index_set_2of2(x_eq_d))( d * x_eq_d[i,d] ) = x[i]
47    );
48
49function var int: eq_new_var(var int: x, int: i) ::promise_total =
50  if i in dom(x) then
51  let {
52    var 0..1: xi;
53  } in xi
54  else 0 endif;
55
56function array[int] of var int: eq_encode(var int: x) ::promise_total =
57  let {
58    array[int] of var int: y = array1d(lb(x)..ub(x),[eq_new_var(x,i) | i in lb(x)..ub(x)]);
59    constraint equality_encoding(x,y);
60%    constraint
61%      if card(dom(x))>0 then
62%        my_trace("  eq_encode: dom(\(x)) = " ++ show(dom(x)) ++ ",  card( dom(\(x)) ) = " ++ show(card(dom(x))) ++ "\n")
63%      else true endif;
64 %%   constraint assert(card(dom(x))>1, "  eq_encode: card(dom(\(x))) == " ++ show(card(dom(x))));
65  } in  y;
66
67function array[int] of int: eq_encode(int: x) ::promise_total =
68  array1d(lb(x)..ub(x),[ if i=x then 1 else 0 endif | i in lb(x)..ub(x)]);
69
70%%% The same for 2 variables:
71function var int: eq_new_var(var int: x, int: i, var int: y, int: j) ::promise_total =
72  if i in dom(x) /\ j in dom(y) then
73  let {
74    var 0..1: xi;
75  } in xi
76  else 0 endif;
77
78function array[int, int] of var int: eq_encode(var int: x, var int: y) ::promise_total =
79  let {
80    array[int] of var int: pX = eq_encode(x),
81    array[int] of var int: pY = eq_encode(y),
82    array[int, int] of var int: pp = array2d(index_set(pX), index_set(pY),
83      [eq_new_var(x,i,y,j) | i in index_set(pX), j in index_set(pY)]);
84    constraint equality_encoding(x, y, pX, pY, pp);
85  } in pp;
86
87function array[int, int] of int: eq_encode(int: x, int: y) ::promise_total =
88%  let {
89%    constraint       if card(dom(x))*card(dom(y))>200 then
90%      my_trace("  eq_encode: dom(\(x)) = " ++ show(dom(x)) ++ ", dom(\(y)) = " ++ show(dom(y)) ++ "\n")
91%      else true endif;
92%  } in
93    array2d(lb(x)..ub(x), lb(y)..ub(y),
94      [if i==x /\ j==y then 1 else 0 endif | i in lb(x)..ub(x), j in lb(y)..ub(y)]);
95
96function array[int,int] of var int: eq_encode(array[int] of var int: x) ::promise_total =
97  let {
98    array[index_set(x),lb_array(x)..ub_array(x)] of var int: y =
99      array2d(index_set(x),lb_array(x)..ub_array(x),
100      [ let {
101          array[int] of var int: xi = eq_encode(x[i])
102        } in if j in index_set(xi) then xi[j] else 0 endif
103        | i in index_set(x), j in lb_array(x)..ub_array(x)]
104      )
105  } in y;
106
107function array[int,int] of int: eq_encode(array[int] of int: x) ::promise_total =
108  array2d(index_set(x),lb_array(x)..ub_array(x),[ if j=x[i] then 1 else 0 endif | i in index_set(x), j in lb_array(x)..ub_array(x)]);
109
110%-----------------------------------------------------------------------------%
111%-----------------------------------------------------------------------------%
112