this repo has no description
dekker.one
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 0..1: 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 % Array of variables: x[i] = d <-> x_eq_d[i,d]
16predicate equality_encoding(array[int] of var int: x,
17 array[int, int] of var 0..1: x_eq_d) =
18 forall(i in index_set(x))(
19 x[i] in index_set_2of2(x_eq_d)
20 /\
21 sum(d in index_set_2of2(x_eq_d))( x_eq_d[i,d] ) = 1
22 /\
23 sum(d in index_set_2of2(x_eq_d))( d * x_eq_d[i,d] ) = x[i]
24 );
25
26function var int: eq_new_var(var int: x, int: i) =
27 if i in dom(x) then
28 let {
29 var 0..1: xi;
30 } in xi
31 else 0 endif;
32
33function array[int] of var 0..1: eq_encode(var int: x) ::promise_total =
34 let {
35 array[int] of var 0..1: y = array1d(lb(x)..ub(x),[eq_new_var(x,i) | i in lb(x)..ub(x)]);
36 constraint equality_encoding(x,y);
37 } in y;
38
39function array[int] of int: eq_encode(int: x) ::promise_total =
40 array1d(lb(x)..ub(x),[ if i=x then 1 else 0 endif | i in lb(x)..ub(x)]);
41
42function array[int,int] of var int: eq_encode(array[int] of var int: x) ::promise_total =
43 let {
44 array[index_set(x),lb_array(x)..ub_array(x)] of var 0..1: y =
45 array2d(index_set(x),lb_array(x)..ub_array(x),
46 [ let {
47 array[int] of var int: xi = eq_encode(x[i])
48 } in if j in index_set(xi) then xi[j] else 0 endif
49 | i in index_set(x), j in lb_array(x)..ub_array(x)]
50 )
51 } in y;
52
53function array[int,int] of int: eq_encode(array[int] of int: x) ::promise_total =
54 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)]);
55
56%-----------------------------------------------------------------------------%
57%-----------------------------------------------------------------------------%