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