this repo has no description
dekker.one
1% FlatZinc built-in redefinitions for G12/LazyFD.
2
3predicate array_bool_element(var int : idx, array[int] of bool : arr,
4 var bool : v) =
5 let { int : N = length(arr),
6 array[1..N] of var bool : tmp = [idx = I | I in 1..N]
7 }
8 in
9 exists(I in 1..N)(tmp[I])
10 /\ forall(I in 1..N) (tmp[I] -> v = arr[I]);
11
12predicate array_var_bool_element(var int : idx, array[int] of var bool : arr,
13 var bool : v) =
14 let { int : N = length(arr),
15 array[1..N] of var bool : tmp = [idx = I | I in 1..N]
16 }
17 in
18 exists(I in 1..N)(tmp[I])
19 /\ forall(I in 1..N) (tmp[I] -> v = arr[I]);
20
21predicate array_bool_xor(array[int] of var bool: bs) =
22 let { int: bs_lower = min(index_set(bs)),
23 int: bs_upper = max(index_set(bs)),
24 int: n = length(bs)
25 } in
26 if n == 1 then bs[bs_lower] else
27 if n == 2 then bs[bs_lower] xor bs[bs_upper] else
28 if n == 3 then bs[bs_lower] = (bs[bs_lower + 1] = bs[bs_upper])
29 else
30 let { int: cs_lower = bs_lower + 1,
31 int: cs_upper = bs_upper - 1,
32 array [cs_lower..cs_upper] of var bool: cs
33 } in
34 forall(i in cs_lower..cs_upper-1)(
35 cs[i+1] = bs[i+1] xor cs[i]
36 )
37 /\ (cs[cs_lower] = bs[bs_lower] xor bs[bs_lower + 1])
38 /\ (bs[bs_upper] xor cs[cs_upper])
39 endif endif endif;
40
41predicate int_abs(var int: a, var int: b) =
42 b >= 0 /\ b >= a /\ b >= -a /\ (b <= a \/ b <= - a);
43
44predicate int_mod(var int: a, var int: b, var int: c) =
45 let {
46 int : bnd = max([lb(a), ub(a), -lb(a), -ub(a)]),
47 var -bnd .. bnd : z
48 } in
49 ( b >= 0 -> c >= 0 /\ c < b) /\
50 ( b <= 0 -> c <= 0 /\ c > b) /\
51 b * z + c = a;