1/* 2% FlatZinc built-in redefinitions for linear solvers. 3% 4% AUTHORS 5% Sebastian Brand 6% Gleb Belov 7*/ 8 9%-----------------------------------------------------------------------------% 10% 11% Logic operations 12% Use indicators for reifs (CPLEX)? Seems weak. 13% 14%-----------------------------------------------------------------------------% 15 16predicate bool_not(var bool: p) = bool2int(p)=0; 17 18predicate bool_not(var bool: p, var bool: q) = 19 bool2int(p) + bool2int(q) = 1; 20 21predicate bool_and(var bool: p, var bool: q, var bool: r) = 22% my_trace(" bool_and: \(p) /\\ \(q) <-> \(r) \n") /\ 23 if false then 24 int_lin_le_reif__IND( [-1, -1], [p, q], -2, r) 25 else 26 array_bool_and( [p, q], r ) 27% bool_and__INT(bool2int(p), bool2int(q), bool2int(r)) 28 endif; 29 30predicate bool_and__INT(var int: x, var int: y, var int: z) = 31 x + y <= z + 1 /\ 32 %% x + y >= z * 2; % weak 33 x >= z /\ y >= z; % strong 34 35 36predicate bool_or(var bool: p, var bool: q, var bool: r) = 37 if false then 38 int_lin_le_reif__IND( [-1, -1], [p, q], -1, r) 39 elseif true then 40 array_bool_or( [p, q], r ) 41 else 42 let { var int: x = bool2int(p), 43 var int: y = bool2int(q), 44 var int: z = bool2int(r) } 45 in 46 x + y >= z /\ 47 % x + y <= z * 2; % weak 48 x <= z /\ y <= z % strong 49 endif; 50 51predicate bool_xor(var bool: p, var bool: q) = 52 1==p+q; 53 54predicate bool_xor(var bool: p, var bool: q, var bool: r) = 55 if false then 56% int_lin_eq_reif__IND( [1, 1], [p, q], 1, r) /\ 57 true 58 else 59 let { var int: x = bool2int(p), 60 var int: y = bool2int(q), 61 var int: z = bool2int(r) } 62 in 63 x <= y + z /\ 64 y <= x + z /\ 65 z <= x + y /\ 66 x + y + z <= 2 67 endif; 68 69 70predicate bool_eq_reif(var bool: p, var bool: q, var bool: r) = 71%% trace(" bool_eq_reif: \(p), \(q), \(r) \n") /\ 72 if is_fixed(r) then % frequent case 73 if fix(r) = true then p = q else bool_not(p,q) endif 74 elseif is_fixed(q) then 75 if fix(q) = true then p = r 76 else bool_not(p,r) endif 77 elseif is_fixed(p) then 78 if fix(p) = true then q = r 79 else bool_not(q,r) endif 80 elseif false then 81% int_lin_eq_reif__IND( [1, -1], [p, q], 0, r) /\ 82 true 83 else 84 let { var int: x = bool2int(p), 85 var int: y = bool2int(q), 86 var int: z = bool2int(r) } 87 in 88 x + y <= z + 1 /\ 89 x + z <= y + 1 /\ 90 y + z <= x + 1 /\ 91 x + y + z >= 1 92 endif; 93 94 95predicate bool_ne_reif(var bool: p, var bool: q, var bool: r) = 96 bool_xor(p, q, r); 97 98 99predicate bool_le(var bool: p, var bool: q) = 100 let { var int: x = bool2int(p), 101 var int: y = bool2int(q) } 102 in 103 x <= y; 104 105 106predicate bool_le_reif(var bool: p, var bool: q, var bool: r) = 107 if false then 108% int_lin_le_reif__IND( [1, -1], [p, q], 0, r) /\ 109 true 110 else 111 let { var int: x = bool2int(p), 112 var int: y = bool2int(q), 113 var int: z = bool2int(r) } 114 in 115 1 - x + y >= z /\ 116 %% /\ 1 - x + y <= z * 2 not needed 117 1 - x <= z /\ y <= z % strong 118 endif; 119 120 121predicate bool_lt(var bool: p, var bool: q) = 122 not p /\ q; 123 124 125predicate bool_lt_reif(var bool: p, var bool: q, var bool: r) = 126 (not p /\ q) <-> r; 127 128%-----------------------------------------------------------------------------% 129 130%% Reified disjunction 131predicate array_bool_or(array[int] of var bool: a, var bool: b) = 132 if exists( i in index_set( a ) )( is_fixed(a[i]) /\ fix(a[i]) ) then 133 b 134 elseif is_fixed(b) then % frequent case 135 if fix(b) = true then 136 sum(i in index_set(a))( bool2int(a[i]) ) >= 1 %% >=1 seems better for MIPDomains... 5.4.19 137 else 138 forall(i in index_set(a))( not a[i] ) 139 endif 140 else 141 let { var int: x = bool2int(b), 142 array[1..length(a)] of var int: c = 143 [ bool2int(a[i]) | i in index_set(a) ] } 144 in 145 sum(c) >= x /\ 146 % sum(c) <= x * length(a) % weak 147 forall (i in index_set(a)) (x >= c[i]) % strong 148 endif; 149 150%% Reified conjunction 151predicate array_bool_and(array[int] of var bool: a, var bool: b) = 152 if exists( i in index_set( a ) )( is_fixed(a[i]) /\ not fix(a[i]) ) then 153 not b 154 elseif is_fixed(b) then % frequent case 155 if fix(b) = false then 156 sum(i in index_set(a))( bool2int(a[i]) ) <= length(a)-1 157 else 158 forall(i in index_set(a))( a[i] ) 159 endif 160 else 161 let { var int: x = bool2int(b), 162 array[1..length(a)] of var int: c = 163 [ bool2int(a[i]) | i in index_set(a) ] } 164 in 165 length(a) - sum(c) >= 1 - x /\ 166 % length(a) - sum(c) <= (1 - x) * length(a); % weak 167 forall (i in index_set(a)) (x <= c[i]) % strong 168 endif; 169 170% predicate array_bool_xor(array[int] of var bool: a) = .. sum(a) is odd .. 171predicate array_bool_xor(array[int] of var bool: a) = 172 let { var 0..(length(a)-1) div 2: m, 173 var 1..((length(a)-1) div 2)*2+1: ss = sum(i in index_set(a))( bool2int(a[i]) ) } 174 in 175 ss == 1 + 2 * m; 176 177predicate bool_clause(array[int] of var bool: p, array[int] of var bool: n) = 178 sum(i in index_set(p))( bool2int(p[i]) ) 179 - sum(i in index_set(n))( bool2int(n[i]) ) 180 + length(n) 181 >= 1; 182 183predicate bool_lin_eq(array[int] of int: c, array[int] of var bool: x, var int: d) :: promise_total = 184 sum(i in index_set(x))( c[i]*bool2int(x[i]) ) == d; 185 186predicate bool_lin_eq_reif(array[int] of int: c, array[int] of var bool: x, 187 int: d, var bool: b) = %% No var int d, sorry 188 aux_int_eq_iff_1(sum(i in index_set(x))( c[i]*bool2int(x[i]) ), d, bool2int(b)); 189 190 191