this repo has no description
dekker.one
1include "redefs_lin_halfreifs.mzn";
2
3% SIMPLE BOOLEAN LOGIC
4% TODO: why not check "is_fixed(r)" everywhere??
5
6predicate bool_eq_imp(var bool: p, var bool: q, var bool: r) =
7 if is_fixed(r) then
8 if fix(r) then p = q else true endif
9 else
10 let {
11 var int: x = bool2int(p),
12 var int: y = bool2int(q),
13 var int: z = bool2int(r)
14 } in x + z <= y + 1 /\ y + z <= x + 1
15 endif;
16
17predicate bool_ne_imp(var bool: p, var bool: q, var bool: r) =
18 bool_xor_imp(p, q, r);
19
20predicate bool_le_imp(var bool: p, var bool: q, var bool: r) =
21 let {
22 var int: x = bool2int(p),
23 var int: y = bool2int(q),
24 var int: z = bool2int(r),
25 } in 1 - x + y >= z;
26
27predicate bool_lt_imp(var bool: p, var bool: q, var bool: r) =
28 bool_and_imp(not p, q, r);
29
30predicate bool_or_imp(var bool: p, var bool: q, var bool: r) =
31 array_bool_or_imp([p,q], r);
32
33predicate bool_and_imp(var bool: p, var bool: q, var bool: r) =
34 array_bool_and_imp([p,q],r);
35
36predicate bool_xor_imp(var bool: p, var bool: q, var bool: r) =
37 let {
38 var int: x = bool2int(p),
39 var int: y = bool2int(q),
40 var int: z = bool2int(r),
41 } in x + y >= z /\ x + y + z <= 2;
42
43% BOOLEAN ARRAY OPERATIONS
44predicate array_bool_or_imp(array[int] of var bool: a, var bool: b) =
45 if forall( i in index_set( a ) )( is_fixed(a[i]) /\ not fix(a[i]) ) then
46 not b
47 elseif exists( i in index_set( a ) )( is_fixed(a[i]) /\ fix(a[i]) ) then
48 true
49 else
50 let {
51 array[index_set(a)] of var bool: a1;
52 var int: x = bool2int(b),
53 } in forall(i in index_set(a)) (a1[i] -> a[i]) /\ sum(a1) = x
54 endif;
55
56predicate array_bool_and_imp(array[int] of var bool: a, var bool: b) =
57 if is_fixed(b) then
58 if fix(b) then
59 forall(i in index_set(a))( a[i] )
60 else
61 true
62 endif
63 elseif forall( i in index_set( a ) )( is_fixed(a[i]) /\ fix(a[i]) ) then
64 true
65 else
66 let {
67 var int: x = bool2int(b),
68 array[index_set(a)] of var int: c =
69 array1d(index_set(a), [ bool2int(a[i] ) | i in index_set(a) ])
70 } in forall(i in index_set(c)) ( c[i] >= x )
71 endif;
72
73%% No var int d, sorry TODO: why not???
74predicate bool_lin_eq_imp(array[int] of int: c, array[int] of var bool: x,
75 int: d, var bool: b) =
76 aux_int_eq_if_1(sum(i in index_set(x))( c[i]*bool2int(x[i]) ), d, bool2int(b));