1%-----------------------------------------------------------------------------% 2% FlatZinc built-in redefinitions for linear solvers. 3% 4% Sebastian Brand 5% Gleb Belov Corrected array_var_float_element and float_lin_lt_reif 6%-----------------------------------------------------------------------------% 7 8function var bool: reverse_map(var int: x) = (x==1); 9function bool: reverse_map(int: x) = (x==1); 10 11function var int: bool2int(var bool: x) :: promise_total = 12 let { var 0..1: b2i; 13 constraint (x = reverse_map(b2i)) ::is_reverse_map ; 14 } in b2i; 15 16predicate bool_eq(var bool: x, var bool: y) = 17 bool2int(x)==bool2int(y); 18 19%-----------------------------------------------------------------------------% 20% Strict inequality 21% 22% Uncomment the following redefinition for FlatZinc MIP solver interfaces that 23% do not support strict inequality. Note that it does not preserve equivalence 24% (some solutions of the original problem may become invalid). 25 26% predicate float_lt(var float: x, var float: y) = x + 1e-06 <= y; 27 28%-----------------------------------------------------------------------------% 29% 30% Logic operations 31% 32%-----------------------------------------------------------------------------% 33 34predicate bool_not(var bool: p, var bool: q) = 35 let { var 0..1: x = bool2int(p), 36 var 0..1: y = bool2int(q) } 37 in 38 x + y = 1; 39 40 41predicate bool_and(var bool: p, var bool: q, var bool: r) = 42 let { var 0..1: x = bool2int(p), 43 var 0..1: y = bool2int(q), 44 var 0..1: z = bool2int(r) } 45 in 46 x + y <= z + 1 /\ 47 x + y >= z * 2; 48 % x >= z /\ y >= z; % alternative 49 50 51predicate bool_or(var bool: p, var bool: q, var bool: r) = 52 let { var 0..1: x = bool2int(p), 53 var 0..1: y = bool2int(q), 54 var 0..1: z = bool2int(r) } 55 in 56 x + y >= z /\ 57 x + y <= z * 2; 58 % x <= z /\ y <= z; % alternative 59 60 61predicate bool_xor(var bool: p, var bool: q, var bool: r) = 62 let { var 0..1: x = bool2int(p), 63 var 0..1: y = bool2int(q), 64 var 0..1: z = bool2int(r) } 65 in 66 x <= y + z /\ 67 y <= x + z /\ 68 z <= x + y /\ 69 x + y + z <= 2; 70 71 72predicate bool_eq_reif(var bool: p, var bool: q, var bool: r) = 73 if is_fixed(q) then % frequent case 74 if fix(q) = true then p = r else bool_not(p,r) endif 75 else 76 let { var 0..1: x = bool2int(p), 77 var 0..1: y = bool2int(q), 78 var 0..1: z = bool2int(r) } 79 in 80 x + y <= z + 1 /\ 81 x + z <= y + 1 /\ 82 y + z <= x + 1 /\ 83 x + y + z >= 1 84 endif; 85 86 87predicate bool_ne_reif(var bool: p, var bool: q, var bool: r) = 88 bool_xor(p, q, r); 89 90 91predicate bool_le(var bool: p, var bool: q) = 92 let { var 0..1: x = bool2int(p), 93 var 0..1: y = bool2int(q) } 94 in 95 x <= y; 96 97 98predicate bool_le_reif(var bool: p, var bool: q, var bool: r) = 99 let { var 0..1: x = bool2int(p), 100 var 0..1: y = bool2int(q), 101 var 0..1: z = bool2int(r) } 102 in 103 1 - x + y >= z /\ 104 1 - x + y <= z * 2; 105 % 1 - x <= z /\ y <= z; % alternative 106 107 108predicate bool_lt(var bool: p, var bool: q) = 109 not p /\ q; 110 111 112predicate bool_lt_reif(var bool: p, var bool: q, var bool: r) = 113 (not p /\ q) <-> r; 114 115%-----------------------------------------------------------------------------% 116 117predicate array_bool_or(array[int] of var bool: a, var bool: b) = 118 if is_fixed(b) then % frequent case 119 if fix(b) = true then 120 sum(i in index_set(a))( bool2int(a[i]) ) >= 1 121 else 122 forall(i in index_set(a))( not a[i] ) 123 endif 124 else 125 let { var 0..1: x = bool2int(b), 126 array[1..length(a)] of var 0..1: c = 127 [ bool2int(a[i]) | i in index_set(a) ] } 128 in 129 sum(c) >= x /\ 130 sum(c) <= x * length(a) 131 endif; 132 133predicate array_bool_and(array[int] of var bool: a, var bool: b) = 134 let { var 0..1: x = bool2int(b), 135 array[1..length(a)] of var 0..1: c = 136 [ bool2int(a[i]) | i in index_set(a) ] } 137 in 138 length(a) - sum(c) >= 1 - x /\ 139 length(a) - sum(c) <= (1 - x) * length(a); 140 141predicate array_bool_xor(array[int] of var bool: a) = 142 let { var 0..length(a): m } 143 in 144 sum(i in 1..length(a))( bool2int(a[i]) ) = 1 + 2 * m; 145 146predicate bool_clause(array[int] of var bool: p, array[int] of var bool: n) = 147 sum(i in index_set(p))( bool2int(p[i]) ) 148 - sum(i in index_set(n))( bool2int(n[i]) ) 149 + length(n) 150 >= 1; 151 152% predicate array_bool_xor(array[int] of var bool: a) = .. sum(a) is odd .. 153 154%-----------------------------------------------------------------------------% 155% 156% Linear equations and inequations 157% 158%-----------------------------------------------------------------------------% 159 160predicate int_le_reif(var int: x, var int: y, var bool: b) = 161 let { var 0..1: p = bool2int(b) } 162 in 163 aux_int_le_if_1(x, y, p) /\ 164 aux_int_gt_if_0(x, y, p); 165 166 167predicate int_lt_reif(var int: x, var int: y, var bool: b) = 168 int_le_reif(x, y - 1, b); 169 170 171predicate int_ne(var int: x, var int: y) = 172 let { var 0..1: p } 173 in 174 aux_int_lt_if_1(x, y, p) /\ 175 aux_int_gt_if_0(x, y, p); 176 177predicate int_lin_ne(array[int] of int: c, array[int] of var int: x, int: d) = 178 int_ne(sum(i in index_set(x))( c[i]*x[i] ),d); 179 180predicate int_eq_reif(var int: x, var int: y, var bool: b) = 181 aux_int_eq_iff_1(x, y, bool2int(b)); 182 183 184predicate int_ne_reif(var int: x, var int: y, var bool: b) = 185 aux_int_eq_iff_1(x, y, 1 - bool2int(b)); 186 187%-----------------------------------------------------------------------------% 188 189predicate int_lin_eq_reif(array[int] of int: c, array[int] of var int: x, 190 int: d, var bool: b) = 191 aux_int_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, bool2int(b)); 192 193 194predicate int_lin_ne_reif(array[int] of int: c, array[int] of var int: x, 195 int: d, var bool: b) = 196 aux_int_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, 1 - bool2int(b)); 197 198 199predicate int_lin_le_reif(array[int] of int: c, array[int] of var int: x, 200 int: d, var bool: b) = 201 let { var 0..1: p = bool2int(b) } 202 in 203 aux_int_le_if_1(sum(i in index_set(x))( c[i] * x[i] ), d, p) /\ 204 aux_int_gt_if_0(sum(i in index_set(x))( c[i] * x[i] ), d, p); 205 206 207predicate int_lin_lt_reif(array[int] of int: c, array[int] of var int: x, 208 int: d, var bool: b) = 209 int_lin_le_reif(c, x, d - 1, b); 210 211%-----------------------------------------------------------------------------% 212 213predicate float_le_reif(var float: x, var float: y, var bool: b) = 214 let { var 0..1: p = bool2int(b) } 215 in 216 aux_float_le_if_1(x, y, int2float(p)) /\ 217 aux_float_gt_if_0(x, y, int2float(p)); 218 219 220predicate float_lt_reif(var float: x, var float: y, var bool: b) = 221 let { var 0..1: p = bool2int(b) } 222 in 223 aux_float_lt_if_1(x, y, int2float(p)) /\ 224 aux_float_ge_if_0(x, y, int2float(p)); 225 226 227predicate float_ne(var float: x, var float: y) = 228 let { var 0..1: p } 229 in 230 aux_float_lt_if_1(x, y, int2float(p)) /\ 231 aux_float_gt_if_0(x, y, int2float(p)); 232 233 234predicate float_eq_reif(var float: x, var float: y, var bool: b) = 235 aux_float_eq_iff_1(x, y, int2float(bool2int(b))); 236 237 238predicate float_ne_reif(var float: x, var float: y, var bool: b) = 239 aux_float_eq_iff_1(x, y, 1.0 - int2float(bool2int(b))); 240 241%-----------------------------------------------------------------------------% 242 243predicate float_lin_eq_reif(array[int] of float: c, array[int] of var float: x, 244 float: d, var bool: b) = 245 aux_float_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, 246 int2float(bool2int(b))); 247 248 249predicate float_lin_ne_reif(array[int] of float: c, array[int] of var float: x, 250 float: d, var bool: b) = 251 aux_float_eq_iff_1(sum(i in index_set(x))( c[i]*x[i] ), d, 252 1.0 - int2float(bool2int(b))); 253 254 255predicate float_lin_le_reif(array[int] of float: c, array[int] of var float: x, 256 float: d, var bool: b) = 257 let { var 0.0..1.0: p = int2float(bool2int(b)) } 258 in 259 aux_float_le_if_1(sum(i in index_set(x))( c[i] * x[i] ), d, p) /\ 260 aux_float_gt_if_0(sum(i in index_set(x))( c[i] * x[i] ), d, p); 261 262 263predicate float_lin_lt_reif(array[int] of float: c, array[int] of var float: x, 264 float: d, var bool: b) = 265 let { var 0.0..1.0: p = int2float(bool2int(b)) } 266 in 267 aux_float_lt_if_1(sum(i in index_set(x))( c[i] * x[i] ), d, p) /\ 268 aux_float_ge_if_0(sum(i in index_set(x))( c[i] * x[i] ), d, p); 269 270%-----------------------------------------------------------------------------% 271% Minimum, maximum, absolute value 272 273predicate int_abs(var int: x, var int: z) = 274 let { var 0..1: p } 275 in 276 % z <= x \/ z <= -x 277 aux_int_le_if_1(z, x, p) /\ 278 aux_int_le_if_0(z, -x, p) /\ 279 z >= x /\ 280 z >= -x /\ 281 z >= 0; 282 283 284predicate int_min(var int: x, var int: y, var int: z) = 285 let { var 0..1: p } 286 in 287 % z >= x \/ z >= y 288 aux_int_ge_if_1(z, x, p) /\ 289 aux_int_ge_if_0(z, y, p) /\ 290 z <= x /\ 291 z <= y; 292 293 294predicate int_max(var int: x, var int: y, var int: z) = 295 let { var 0..1: p } 296 in 297 % z <= x \/ z <= y 298 aux_int_le_if_1(z, x, p) /\ 299 aux_int_le_if_0(z, y, p) /\ 300 z >= x /\ 301 z >= y; 302 303 304predicate float_abs(var float: x, var float: z) = 305 let { var 0..1: p } 306 in 307 % z <= x \/ z <= -x 308 aux_float_le_if_1(z, x, int2float(p)) /\ 309 aux_float_le_if_0(z, -x, int2float(p)) /\ 310 z >= x /\ 311 z >= -x /\ 312 z >= 0.0; 313 314 315predicate float_min(var float: x, var float: y, var float: z) = 316 let { var 0..1: p } 317 in 318 % z >= x \/ z >= y 319 aux_float_ge_if_1(z, x, int2float(p)) /\ 320 aux_float_ge_if_0(z, y, int2float(p)) /\ 321 z <= x /\ 322 z <= y; 323 324 325predicate float_max(var float: x, var float: y, var float: z) = 326 let { var 0..1: p } 327 in 328 % z <= x \/ z <= y 329 aux_float_le_if_1(z, x, int2float(p)) /\ 330 aux_float_le_if_0(z, y, int2float(p)) /\ 331 z >= x /\ 332 z >= y; 333 334%-----------------------------------------------------------------------------% 335% Multiplication and division 336 337predicate int_div(var int: x, var int: y, var int: q) = 338 let { var 0..max(abs(lb(y)), abs(ub(y))) - 1: r } 339 in 340 aux_int_division_modulo(x,y,q,r); 341 342 343predicate int_mod(var int: x, var int: y, var int: r) = 344 let { 345 int: bx = max(abs(lb(x)), abs(ub(x))); 346 var -bx..bx: q; 347 int: by = max(abs(lb(y)), abs(ub(y))); 348 constraint r in -by..by; 349 } 350 in 351 aux_int_division_modulo(x,y,q,r); 352 353 354predicate aux_int_division_modulo(var int: x, var int: y, var int: q, 355 var int: r) = 356 x = y * q + r /\ 357 let { array[1..2] of var 0..1: p } 358 in 359 % 0 < x -> 0 <= r which is 0 >= x \/ 0 <= r 360 aux_int_le_if_1(x, 0, p[1]) /\ 361 aux_int_ge_if_0(r, 0, p[1]) /\ 362 % x < 0 -> r <= 0 which is x >= 0 \/ r <= 0 363 aux_int_ge_if_1(x, 0, p[2]) /\ 364 aux_int_le_if_0(r, 0, p[2]) /\ 365 % abs(r) < abs(y) 366 let { var 1.. max(abs(lb(y)), abs(ub(y))): w = abs(y) } 367 in 368 w > r /\ 369 w > -r; 370 371 372predicate int_times(var int: x, var int: y, var int: z) = 373 if card(dom(x)) > card(dom(y)) then int_times(y,x,z) 374 else 375 let { set of int: s = lb(x)..ub(x), 376 set of int: r = {lb(x)*lb(y), lb(x)*ub(y), ub(x)*lb(y), ub(x)*ub(y)}, 377 array[s] of var min(r)..max(r): ady = array1d(s, [ d*y | d in s ]) } 378 in 379 ady[x] = z 380 endif; 381 382%-----------------------------------------------------------------------------% 383% Array 'element' constraints 384 385predicate array_bool_element(var int: x, array[int] of bool: a, var bool: z) = 386 x in index_set(a) /\ 387 forall(d in index_set(a))( x = d -> a[d] = z ); 388 389 390predicate array_var_bool_element(var int: x, array[int] of var bool: a, 391 var bool: z) = 392 x in index_set(a) /\ 393 forall(d in index_set(a))( x = d -> a[d] = z ); 394 395 396predicate array_int_element(var int: x, array[int] of int: a, var int: z) = 397 x in index_set(a) /\ 398 forall(d in index_set(a))( x = d -> a[d] = z ); 399 400predicate array_var_int_element(var int: x, array[int] of var int: a, 401 var int: z) = 402 x in index_set(a) /\ 403 forall(d in index_set(a))( x = d -> a[d] = z ); 404 405 406predicate array_float_element(var int: x, array[int] of float: a, 407 var float: z) = 408 let { set of int: ix = index_set(a), 409 array[ix] of var 0..1: x_eq_d } 410 in 411 sum(i in ix)( x_eq_d[i] ) = 1 412 /\ 413 sum(i in ix)( i * x_eq_d[i] ) = x 414 /\ 415 sum(i in ix)( a[i] * int2float(x_eq_d[i]) ) = z; 416 417 418predicate array_var_float_element(var int: x, array[int] of var float: a, 419 var float: z) = 420 let { set of int: ix = index_set(a), 421 array[ix] of var 0..1: x_eq_d } 422 in 423 sum(i in ix)( x_eq_d[i] ) = 1 424 /\ 425 sum(i in ix)( i * x_eq_d[i] ) = x 426 /\ 427 forall(i in ix)( 428 % x_eq_d[i] -> a[i] = a2[i] 429 a[i] - z >= (lb(a[i])-ub(z))*int2float(1-x_eq_d[i]) 430 /\ 431 z - a[i] >= (lb(z)-ub(a[i]))*int2float(1-x_eq_d[i]) 432 ); 433 434%-----------------------------------------------------------------------------% 435% Domain constraints 436 437% XXX only for a fixed set 438 439predicate set_in(var int: x, set of int: s) = 440 if s = min(s)..max(s) then 441 min(s) <= x /\ x <= max(s) 442 else 443 exists(e in s)( x = e ) 444 endif; 445 446% XXX only for a fixed set 447predicate set_in_reif(var int: x, set of int: s, var bool: b) = 448 b <-> 449 exists(i in 1..length([ 0 | e in s where not (e - 1 in s) ]))( 450 let { int: l = [ e | e in s where not (e - 1 in s) ][i], 451 int: r = [ e | e in s where not (e + 1 in s) ][i] } 452 in 453 l <= x /\ x <= r 454 ); 455 456 % Alternative 457predicate alt_set_in_reif(var int: x, set of int: s, var bool: b) = 458 b <-> 459 if s = min(s)..max(s) then 460 min(s) <= x /\ x <= max(s) 461 else 462 exists(e in s)( x = e ) 463 endif; 464 465%-----------------------------------------------------------------------------% 466% Auxiliary: equality reified onto a 0/1 variable 467 468predicate aux_int_eq_iff_1(var int: x, var int: y, var int: p) = 469 let { array[1..2] of var 0..1: q_458 } 470 in 471 aux_int_lt_if_0(x - p, y, q_458[1]) /\ 472 aux_int_gt_if_0(x + p, y, q_458[2]) /\ 473 sum(q_458) <= 2 - 2*p /\ 474 sum(q_458) <= 1 + p; 475 476 % Alternative 1 477predicate alt_1_aux_int_eq_iff_1(var int: x, var int: y, var int: p) = 478 let { array[1..2] of var 0..1: q } 479 in 480 aux_int_lt_if_0(x - p, y, q[1]) /\ 481 aux_int_gt_if_0(x + p, y, q[2]) /\ 482 q[1] <= 1 - p /\ 483 q[2] <= 1 - p /\ 484 sum(q) <= 1 + p; 485 486 % Alternative 2 487predicate alt_2_aux_int_eq_iff_1(var int: x, var int: y, var int: p) = 488 let { array[1..2] of var 0..1: q } 489 in 490 aux_int_le_if_1(x, y, p) /\ 491 aux_int_ge_if_1(x, y, p) /\ 492 aux_int_lt_if_0(x, y, q[1]) /\ 493 aux_int_gt_if_0(x, y, q[2]) /\ 494 sum(q) <= p + 1; 495 496 497predicate aux_float_eq_iff_1(var float: x, var float: y, var float: p) = 498 let { array[1..2] of var 0..1: q } 499 in 500 aux_float_le_if_1(x, y, p) /\ 501 aux_float_ge_if_1(x, y, p) /\ 502 aux_float_lt_if_0(x, y, int2float(q[1])) /\ 503 aux_float_gt_if_0(x, y, int2float(q[2])) /\ 504 int2float(sum(q)) <= 1.0 + p; 505 506%-----------------------------------------------------------------------------% 507% Auxiliary: indicator constraints 508% p -> x # 0 where p is a 0/1 variable and # is a comparison 509 510% Base cases 511 512predicate aux_int_le_zero_if_0(var int: x, var int: p) = 513 x <= ub(x) * p; 514 515predicate aux_float_le_zero_if_0(var float: x, var float: p) = 516 x <= ub(x) * p; 517 518predicate aux_float_lt_zero_if_0(var float: x, var float: p) = 519 let { float: rho = 1e-02 * abs(ub(x)) } % same order of magnitude as ub(x) 520 in 521 x < (ub(x) + rho) * p; 522 523 524% Derived cases 525 526predicate aux_int_le_if_0(var int: x, var int: y, var int: p) = 527 aux_int_le_zero_if_0(x - y, p); 528 529predicate aux_int_ge_if_0(var int: x, var int: y, var int: p) = 530 aux_int_le_zero_if_0(y - x, p); 531 532predicate aux_int_le_if_1(var int: x, var int: y, var int: p) = 533 aux_int_le_zero_if_0(x - y, 1 - p); 534 535predicate aux_int_ge_if_1(var int: x, var int: y, var int: p) = 536 aux_int_le_zero_if_0(y - x, 1 - p); 537 538predicate aux_int_lt_if_0(var int: x, var int: y, var int: p) = 539 aux_int_le_zero_if_0(x - y + 1, p); 540 541predicate aux_int_gt_if_0(var int: x, var int: y, var int: p) = 542 aux_int_le_zero_if_0(y - x + 1, p); 543 544predicate aux_int_lt_if_1(var int: x, var int: y, var int: p) = 545 aux_int_le_zero_if_0(x - y + 1, 1 - p); 546 547 548predicate aux_float_le_if_0(var float: x, var float: y, var float: p) = 549 aux_float_le_zero_if_0(x - y, p); 550 551predicate aux_float_ge_if_0(var float: x, var float: y, var float: p) = 552 aux_float_le_zero_if_0(y - x, p); 553 554predicate aux_float_le_if_1(var float: x, var float: y, var float: p) = 555 aux_float_le_zero_if_0(x - y, 1.0 - p); 556 557predicate aux_float_ge_if_1(var float: x, var float: y, var float: p) = 558 aux_float_le_zero_if_0(y - x, 1.0 - p); 559 560predicate aux_float_lt_if_0(var float: x, var float: y, var float: p) = 561 aux_float_lt_zero_if_0(x - y, p); 562 563predicate aux_float_gt_if_0(var float: x, var float: y, var float: p) = 564 aux_float_lt_zero_if_0(y - x, p); 565 566predicate aux_float_lt_if_1(var float: x, var float: y, var float: p) = 567 aux_float_lt_zero_if_0(x - y, 1.0 - p); 568 569%-----------------------------------------------------------------------------% 570%-----------------------------------------------------------------------------% 571 572annotation bool_search(array[int] of var bool: x, ann:a1, ann:a2, ann:a3) = 573 int_search([bool2int(x[i]) | i in index_set(x)],a1,a2,a3); 574 575predicate array_int_maximum(var int: m, array[int] of var int: x) = 576 let { int: l = min(index_set(x)), 577 int: u = max(index_set(x)), 578 int: ly = lb_array(x), 579 int: uy = ub_array(x), 580 array[l..u] of var ly..uy: y } in 581 y[l] = x[l] /\ 582 m = y[u] /\ 583 forall (i in l+1 .. u) ( y[i] == max(x[i],y[i-1]) ); 584 585predicate array_float_maximum(var float: m, array[int] of var float: x) = 586 let { int: l = min(index_set(x)), 587 int: u = max(index_set(x)), 588 float: ly = lb_array(x), 589 float: uy = ub_array(x), 590 array[l..u] of var ly..uy: y } in 591 y[l] = x[l] /\ 592 m = y[u] /\ 593 forall (i in l+1 .. u) ( y[i] == max(x[i],y[i-1]) ); 594 595predicate array_int_minimum(var int: m, array[int] of var int: x) = 596 let { int: l = min(index_set(x)), 597 int: u = max(index_set(x)), 598 int: ly = lb_array(x), 599 int: uy = ub_array(x), 600 array[l..u] of var ly..uy: y } in 601 y[l] = x[l] /\ 602 m = y[u] /\ 603 forall (i in l+1 .. u) ( y[i] == min(x[i],y[i-1]) ); 604 605predicate array_float_minimum(var float: m, array[int] of var float: x) = 606 let { int: l = min(index_set(x)), 607 int: u = max(index_set(x)), 608 float: ly = lb_array(x), 609 float: uy = ub_array(x), 610 array[l..u] of var ly..uy: y } in 611 y[l] = x[l] /\ 612 m = y[u] /\ 613 forall (i in l+1 .. u) ( y[i] == min(x[i],y[i-1]) ); 614 615mzn_opt_only_range_domains = true; 616