1/* Part of SWI-Prolog 2 3 Author: Tom Schrijvers 4 E-mail: tom.schrijvers@cs.kuleuven.ac.be 5 WWW: http://www.swi-prolog.org 6 Copyright (c) 2004-2013, K.U.Leuven 7 All rights reserved. 8 9 Redistribution and use in source and binary forms, with or without 10 modification, are permitted provided that the following conditions 11 are met: 12 13 1. Redistributions of source code must retain the above copyright 14 notice, this list of conditions and the following disclaimer. 15 16 2. Redistributions in binary form must reproduce the above copyright 17 notice, this list of conditions and the following disclaimer in 18 the documentation and/or other materials provided with the 19 distribution. 20 21 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 22 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 23 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS 24 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE 25 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, 26 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, 27 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; 28 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER 29 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT 30 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN 31 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 32 POSSIBILITY OF SUCH DAMAGE. 33*/ 34 35%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 36% 37% Simple integer solver that keeps track of upper and lower bounds 38% 39% Author: Tom Schrijvers 40% E-mail: tom.schrijvers@cs.kuleuven.ac.be 41% Copyright: 2004, K.U.Leuven 42% 43%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 44% 45% Todo: 46% - reduce redundant propagation work 47% - other labelling functions 48% - abs, mod, ... 49% 50%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 51 52:- module(bounds, 53 [ 54 op(760,yfx,(#<=>)), 55 op(750,xfy,(#=>)), 56 op(750,yfx,(#<=)), 57 op(740,yfx,(#\/)), 58 op(730,yfx,(#\)), 59 op(720,yfx,(#/\)), 60 op(710, fy,(#\)), 61 op(700,xfx,(#>)), 62 op(700,xfx,(#<)), 63 op(700,xfx,(#>=)), 64 op(700,xfx,(#=<)), 65 op(700,xfx,(#=)), 66 op(700,xfx,(#\=)), 67 op(700,xfx,(in)), 68 op(550,xfx,(..)), 69 (#>)/2, 70 (#<)/2, 71 (#>=)/2, 72 (#=<)/2, 73 (#=)/2, 74 (#\=)/2, 75 (#<=>)/2, 76 (#=>)/2, 77 (#<=)/2, 78 (#/\)/2, 79 (#\/)/2, 80 (#\)/2, 81 (#\)/1, 82 (in)/2, 83 label/1, 84 labeling/2, 85 all_different/1, 86 sum/3, 87 lex_chain/1, 88 indomain/1, 89 check/1, 90 tuples_in/2, 91 serialized/2 92 ]). 93 94:- use_module(library('clp/clp_events')). 95 96/** <module> Simple integer solver that keeps track of upper and lower bounds 97 98@deprecated No longer maintained. Please use clpfd.pl 99@author Tom Schrijvers 100*/ 101 102%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 103% exported predicates 104X #>= Y :- 105 parse_expression(X,RX), 106 parse_expression(Y,RY), 107 geq(RX,RY,yes). 108X #=< Y :- 109 parse_expression(X,RX), 110 parse_expression(Y,RY), 111 leq(RX,RY,yes). 112X #= Y :- 113 parse_expression(X,RX), 114 parse_expression(Y,RX). 115X #\= Y :- 116 parse_expression(X,RX), 117 parse_expression(Y,RY), 118 neq(RX,RY,yes). 119X #> Y :- 120 Z #= Y + 1, 121 X #>= Z. 122X #< Y :- 123 Y #> X. 124X in L .. U :- 125 ( is_list(X) -> 126 domains(X,L,U) 127 ; 128 domain(X,L,U) 129 ). 130 131L #<=> R :- 132 reify(L,B), 133 reify(R,B). 134L #=> R :- 135 reify(L,BL), 136 reify(R,BR), 137 myimpl(BL,BR). 138R #<= L :- 139 reify(L,BL), 140 reify(R,BR), 141 myimpl(BL,BR). 142L #/\ R :- 143 call(L), 144 call(R). 145L #\/ R :- 146 reify(L,BL), 147 reify(R,BR), 148 myor(BL,BR,1). 149L #\ R :- 150 reify(L,BL), 151 reify(R,BR), 152 myxor(BL,BR,1). 153 154#\ C :- 155 reify(C,B), 156 mynot(B,1). 157%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 158reify(B,R) :- 159 var(B), !, 160 R = B. 161reify(B,R) :- 162 number(B), !, 163 R = B. 164reify(X #>= Y,B) :- 165 parse_expression(X,XR), 166 parse_expression(Y,YR), 167 reified_geq(XR,YR,B). 168reify(X #> Y,B) :- 169 parse_expression(X,XR), 170 Z #= Y + 1, 171 reified_geq(XR,Z,B). 172reify(X #=< Y,B) :- 173 parse_expression(X,XR), 174 parse_expression(Y,YR), 175 reified_geq(YR,XR,B). 176reify(X #< Y,B) :- 177 reify(Y #> X,B). 178reify(X #= Y,B) :- 179 parse_expression(X,XR), 180 parse_expression(Y,YR), 181 reified_eq(XR,YR,B). 182reify(X #\= Y,B) :- 183 parse_expression(X,XR), 184 parse_expression(Y,YR), 185 reified_neq(XR,YR,B). 186reify((X #/\ Y),B) :- 187 reify(X,BX), 188 reify(Y,BY), 189 myand(BX,BY,B). 190reify((X #\/ Y),B) :- 191 reify(X,BX), 192 reify(Y,BY), 193 myor(BX,BY,B). 194reify((X #\ Y),B) :- 195 reify(X,BX), 196 reify(Y,BY), 197 myxor(BX,BY,B). 198reify(#\ C, B) :- 199 reify(C,BC), 200 mynot(BC,B). 201 202%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 203check(X #= Y) :- 204 parse_expression(X,XR), 205 parse_expression(Y,YR), 206 check_eq(XR,YR). 207 208check(X #=< Y) :- 209 parse_expression(X,XR), 210 parse_expression(Y,YR), 211 check_leq(XR,YR). 212 213check(X #>= Y) :- 214 parse_expression(X,XR), 215 parse_expression(Y,YR), 216 check_leq(YR,XR). 217 218check(X #< Y) :- 219 parse_expression(X,XR), 220 parse_expression(Y,YR), 221 check_lt(XR,YR). 222 223check(X #> Y) :- 224 parse_expression(X,XR), 225 parse_expression(Y,YR), 226 check_lt(YR,XR). 227 228 229%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 230parse_expression(Expr,Result) :- 231 ( var(Expr) -> 232 Result = Expr 233 ; number(Expr) -> 234 Result = Expr 235 ; Expr = (L + R) -> 236 parse_expression(L,RL), 237 parse_expression(R,RR), 238 myplus(RL,RR,Result,yes) 239 ; Expr = (L * R) -> 240 parse_expression(L,RL), 241 parse_expression(R,RR), 242 mytimes(RL,RR,Result,yes) 243 ; Expr = (L - R) -> 244 parse_expression(L,RL), 245 parse_expression(R,RR), 246 mytimes(-1,RR,RRR,yes), 247 myplus(RL,RRR,Result,yes) 248 ; Expr = (- E) -> 249 parse_expression(E,RE), 250 mytimes(-1,RE,Result,yes) 251 ; Expr = max(L,R) -> 252 parse_expression(L,RL), 253 parse_expression(R,RR), 254 mymax(RL,RR,Result,yes) 255 ; Expr = min(L,R) -> 256 parse_expression(L,RL), 257 parse_expression(R,RR), 258 mymin(RL,RR,Result,yes) 259 ; Expr = L mod R -> 260 parse_expression(L,RL), 261 parse_expression(R,RR), 262 mymod(RL,RR,Result,yes) 263 ; Expr = abs(E) -> 264 parse_expression(E,RE), 265 myabs(RE,Result,yes) 266 ; Expr = (L / R) -> 267 parse_expression(L,RL), 268 parse_expression(R,RR), 269 mydiv(RL,RR,Result,yes) 270 ). 271 272%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 273indomain(Var) :- 274 ( var(Var) -> 275 bounds(Var,L,U), 276 between(L,U,Var) 277 ; 278 true 279 ). 280 281label(Vs) :- labeling([], Vs). 282 283labeling(Options, Vars) :- 284 label(Options, leftmost, none, Vars). 285 286label([Option|Options], Selection, Optimisation, Vars) :- 287 ( selection(Option) -> 288 label(Options, Option, Optimisation, Vars) 289 ; optimization(Option) -> 290 label(Options, Selection, Option, Vars) 291 ; 292 label(Options, Selection, Optimisation, Vars) 293 ). 294label([], Selection, Optimisation, Vars) :- 295 ( Optimisation == none -> 296 label(Vars, Selection) 297 ; 298 optimize(Vars, Selection, Optimisation) 299 ). 300 301 302label([],_) :- !. 303label(Vars,Selection) :- 304 select_var(Selection,Vars,Var,RVars), 305 indomain(Var), 306 label(RVars,Selection). 307 308selection(ff). 309selection(min). 310selection(max). 311selection(leftmost). 312 313optimization(min(_)). 314optimization(max(_)). 315 316select_var(leftmost,[Var|Vars],Var,Vars). 317select_var(min,[V|Vs],Var,RVars) :- 318 find_min(Vs,V,Var), 319 delete_eq([V|Vs],Var,RVars). 320select_var(max,[V|Vs],Var,RVars) :- 321 find_max(Vs,V,Var), 322 delete_eq([V|Vs],Var,RVars). 323select_var(ff,[V|Vs],Var,RVars) :- 324 find_ff(Vs,V,Var), 325 delete_eq([V|Vs],Var,RVars). 326 327find_min([],Var,Var). 328find_min([V|Vs],CM,Min) :- 329 ( min_lt(V,CM) -> 330 find_min(Vs,V,Min) 331 ; 332 find_min(Vs,CM,Min) 333 ). 334 335find_max([],Var,Var). 336find_max([V|Vs],CM,Max) :- 337 ( max_gt(V,CM) -> 338 find_max(Vs,V,Max) 339 ; 340 find_max(Vs,CM,Max) 341 ). 342 343find_ff([],Var,Var). 344find_ff([V|Vs],CM,FF) :- 345 ( ff_lt(V,CM) -> 346 find_ff(Vs,V,FF) 347 ; 348 find_ff(Vs,CM,FF) 349 ). 350 351ff_lt(X,Y) :- 352 bounds(X,LX,UX), 353 bounds(Y,LY,UY), 354 UX - LX < UY - LY. 355 356min_lt(X,Y) :- 357 bounds(X,LX,_), 358 bounds(Y,LY,_), 359 LX < LY. 360 361max_gt(X,Y) :- 362 bounds(X,_,UX), 363 bounds(Y,_,UY), 364 UX > UY. 365 366bounds(X,L,U) :- 367 ( var(X) -> 368 get(X,L,U,_) 369 ; 370 X = L, 371 X = U 372 ). 373 374delete_eq([],_,[]). 375delete_eq([X|Xs],Y,List) :- 376 ( X == Y -> 377 List = Xs 378 ; 379 List = [X|Tail], 380 delete_eq(Xs,Y,Tail) 381 ). 382 383optimize(Vars, Selection, Opt) :- 384 copy_term(Vars-Opt, Vars1-Opt1), 385 once(label(Vars1, Selection)), 386 functor(Opt1, Direction, _), 387 maplist(arg(1), [Opt,Opt1], [Expr,Expr1]), 388 optimize(Direction, Selection, Vars1, Vars, Expr1, Expr). 389 390optimize(Direction, Selection, Vars0, Vars, Expr0, Expr) :- 391 Val0 is Expr0, 392 copy_term(Vars-Expr, Vars1-Expr1), 393 ( Direction == min -> 394 Tighten = (Expr1 #< Val0) 395 ; % max 396 Tighten = (Expr1 #> Val0) 397 ), 398 ( Tighten, label(Vars1, Selection) -> 399 optimize(Direction, Selection, Vars1, Vars, Expr1, Expr) 400 ; 401 Vars = Vars0, 402 Expr = Expr0 403 ). 404 405%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 406all_different([]). 407all_different([X|Xs]) :- 408 different(Xs,X), 409 all_different(Xs). 410 411different([],_). 412different([Y|Ys],X) :- 413 neq(X,Y,yes), 414 different(Ys,X). 415%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 416sum(Xs,Op,Value) :- 417 sum1(Xs,0,Op,Value). 418 419sum1([],Sum,Op,Value) :- 420 call(Op,Sum,Value). 421sum1([X|Xs],Acc,Op,Value) :- 422 NAcc #= Acc + X, 423 sum1(Xs,NAcc,Op,Value). 424 425%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 426% contributed by Markus Triska 427 428lex_le([],[]). 429lex_le([V1|V1s], [V2|V2s]) :- 430 V1 #=< V2, 431 ( integer(V1) -> 432 ( integer(V2) -> 433 (V1 == V2 -> 434 lex_le(V1s,V2s) 435 ; 436 true 437 ) 438 ; 439 freeze(V2,lex_le([V1|V1s],[V2|V2s])) 440 ) 441 ; 442 freeze(V1,lex_le([V1|V1s],[V2|V2s])) 443 ). 444 445lex_chain([]). 446lex_chain([L|Ls]) :- 447 lex_chain_lag(Ls, L). 448 449lex_chain_lag([], _). 450lex_chain_lag([L|Ls], Prev) :- 451 lex_le(Prev, L), 452 lex_chain_lag(Ls, L). 453 454%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 455domain(X,L,U) :- 456 ( var(X) -> 457 get(X,XL,XU,Exp), 458 NL is max(L,XL), 459 NU is min(U,XU), 460 put(X,NL,NU,Exp) 461 ; % nonvar(X) -> 462 X >= L, 463 X =< U 464 ). 465 466domains([],_,_). 467domains([V|Vs],L,U) :- 468 domain(V,L,U), 469 domains(Vs,L,U). 470 471%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 472leq(X,Y,New) :- 473 geq(Y,X,New). 474 475%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 476geq(X,Y,New) :- 477 ( X == Y -> 478 true 479 ; nonvar(X) -> 480 ( nonvar(Y) -> 481 X >= Y 482 ; 483 get(Y,YL,YU,Exp) -> 484 NYU is min(X,YU), 485 put(Y,YL,NYU,Exp) 486 ) 487 ; nonvar(Y) -> 488 get(X,XL,XU,Exp) -> 489 NXL is max(Y,XL), 490 put(X,NXL,XU,Exp) 491 ; 492 get(X,XL,XU,ExpX), 493 get(Y,YL,YU,ExpY), 494 XU >= YL, 495 ( XL > YU -> 496 true 497 ; XU == YL -> 498 X = Y 499 ; member(leq(Z,State),ExpX), 500 Y == Z -> 501 set_passive(State), 502 X = Y 503 ; 504 ( New == yes -> 505 active_state(State), 506 put(Y,YL,YU,[leq(X,State)|ExpY]), 507 ExpX1 = [geq(Y,State)|ExpX] 508 ; 509 ExpX1 = ExpX 510 ), 511 NXL is max(XL,YL), 512 put(X,NXL,XU,ExpX1), 513 ( get(Y,YL2,YU2,ExpY2) -> 514 NYU is min(YU2,XU), 515 put(Y,YL2,NYU,ExpY2) 516 ; 517 true 518 ) 519 ) 520 ). 521 522%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 523neq(X,Y,New) :- 524 X \== Y, 525 ( nonvar(X) -> 526 ( nonvar(Y) -> 527 true 528 ; 529 get(Y,L,U,Exp), 530 ( L == X -> 531 NL is L + 1, 532 put(Y,NL,U,Exp) 533 ; U == X -> 534 NU is U - 1, 535 put(Y,L,NU,Exp) 536 ; L > X -> 537 true 538 ; U < X -> 539 true 540 ; 541 ( New == yes -> 542 active_state(State), 543 put(Y,L,U,[neq(X,State)|Exp]) 544 ; 545 true 546 ) 547 ) 548 ) 549 ; nonvar(Y) -> 550 neq(Y,X,New) 551 ; 552 get(X,XL,XU,XExp), 553 get(Y,YL,YU,YExp), 554 ( XL > YU -> 555 true 556 ; YL > XU -> 557 true 558 ; 559 ( New == yes -> 560 active_state(State), 561 put(X,XL,XU,[neq(Y,State)|XExp]), 562 put(Y,YL,YU,[neq(X,State)|YExp]) 563 ; 564 true 565 ) 566 ) 567 ). 568 569%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 570myplus(X,Y,Z,New) :- 571 ( nonvar(X) -> 572 ( nonvar(Y) -> 573 Z is X + Y 574 ; nonvar(Z) -> 575 Y is Z - X 576 ; 577 get(Z,ZL,ZU,ZExp), 578 get(Y,YL,YU,YExp), 579 ( New == yes -> 580 ZExp1 = [myplus2(Y,X)|ZExp], 581 YExp1 = [myplus(X,Z)|YExp], 582 put(Y,YL,YU,YExp1) 583 ; 584 ZExp1 = ZExp 585 ), 586 NZL is max(ZL,X+YL), 587 NZU is min(ZU,X+YU), 588 put(Z,NZL,NZU,ZExp1), 589 ( get(Y,YL2,YU2,YExp2) -> % JW: YL2 and YU2? 590 NYL is max(YL2,NZL-X), 591 NYU is min(YU2,NZU-X), 592 put(Y,NYL,NYU,YExp2) 593 ; 594 Z is X + Y 595 ) 596 ) 597 ; nonvar(Y) -> 598 myplus(Y,X,Z,New) 599 ; nonvar(Z) -> 600 get(X,XL,XU,XExp), 601 get(Y,YL,YU,YExp), 602 ( New == yes -> 603 XExp1 = [myplus(Y,Z)|XExp], 604 YExp1 = [myplus(X,Z)|YExp], 605 put(Y,YL,YU,YExp1) 606 ; 607 XExp1 = XExp 608 ), 609 NXL is max(XL,Z-YU), 610 NXU is min(XU,Z-YL), 611 put(X,NXL,NXU,XExp1), 612 ( get(Y,YL2,YU2,YExp2) -> 613 NYL is max(YL2,Z-NXU), 614 NYU is min(YU2,Z-NXL), 615 put(Y,NYL,NYU,YExp2) 616 ; 617 X is Z - Y 618 ) 619 ; 620 get(X,XL,XU,XExp), 621 get(Y,YL,YU,YExp), 622 get(Z,ZL,ZU,ZExp), 623 ( New == yes -> 624 XExp1 = [myplus(Y,Z)|XExp], 625 YExp1 = [myplus(X,Z)|YExp], 626 ZExp1 = [myplus2(X,Y)|ZExp], 627 put(Y,YL,YU,YExp1), 628 put(Z,ZL,ZU,ZExp1) 629 ; 630 XExp1 = XExp 631 ), 632 NXL is max(XL,ZL-YU), 633 NXU is min(XU,ZU-YL), 634 put(X,NXL,NXU,XExp1), 635 ( get(Y,YL2,YU2,YExp2) -> 636 NYL is max(YL2,ZL-NXU), 637 NYU is min(YU2,ZU-NXL), 638 put(Y,NYL,NYU,YExp2) 639 ; 640 NYL = Y, 641 NYU = Y 642 ), 643 ( get(Z,ZL2,ZU2,ZExp2) -> 644 NZL is max(ZL2,NXL+NYL), 645 NZU is min(ZU2,NXU+NYU), 646 put(Z,NZL,NZU,ZExp2) 647 ; 648 true 649 ) 650 ). 651 652%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 653% X * Y = Z 654 655div(X,Y,Z) :- 656 ( max_inf(X) -> 657 ( Y >= 0 -> 658 Z = X 659 ; 660 min_inf(Z) 661 ) 662 ; min_inf(X) -> 663 ( Y >= 0 -> 664 Z = X 665 ; 666 max_inf(Z) 667 ) 668 ; Y \== 0 -> 669 Z is X / Y 670 ; X >= 0 -> 671 max_inf(Z) 672 ; X < 0 -> 673 min_inf(Z) 674 ). 675 676mytimes(X,Y,Z,New) :- 677 ( nonvar(X) -> 678 (nonvar(Y) -> 679 Z is X * Y 680 ; X == 0 -> 681 Z = 0 682 ; nonvar(Z) -> 683 0 is Z mod X, 684 Y is Z / X 685 ; 686 get(Y,YL,YU,YExp), 687 get(Z,ZL,ZU,ZExp), 688 NZL is max(ZL,min(X * YL,X*YU)), 689 NZU is min(ZU,max(X * YU,X*YL)), 690 ( New == yes -> 691 YExp1 = [mytimes(X,Z)|YExp], 692 put(Y,YL,YU,YExp1), 693 put(Z,NZL,NZU,[mytimes2(X,Y)|ZExp]) 694 ; 695 put(Z,NZL,NZU,ZExp) 696 ), 697 ( get(Y,YL2,YU2,YExp2) -> 698 min_divide(ZL,ZU,X,X,NYLT), 699 max_divide(ZL,ZU,X,X,NYUT), 700 NYL is max(YL2,ceiling(NYLT)), 701 NYU is min(YU2,floor(NYUT)), 702 put(Y,NYL,NYU,YExp2) 703 ; 704 Z is X * Y 705 ) 706 ) 707 ; nonvar(Y) -> 708 mytimes(Y,X,Z,New) 709 ; nonvar(Z) -> 710 get(X,XL,XU,XExp), 711 get(Y,YL,YU,YExp), 712 min_divide(Z,Z,YL,YU,TNXL), 713 max_divide(Z,Z,YL,YU,TNXU), 714 NXL is max(XL,ceiling(TNXL)), 715 NXU is min(XU,floor(TNXU)), 716 ( New == yes -> 717 YExp1 = [mytimes(X,Z)|YExp], 718 put(Y,YL,YU,YExp1), 719 put(X,NXL,NXU,[mytimes(Y,Z)|XExp]) 720 ; 721 put(X,NXL,NXU,XExp) 722 ), 723 ( get(Y,YL2,YU2,YExp2) -> 724 min_divide(Z,Z,NXL,NXU,NYLT), 725 max_divide(Z,Z,NXL,NXU,NYUT), 726 NYL is max(YL2,ceiling(NYLT)), 727 NYU is min(YU2,floor(NYUT)), 728 put(Y,NYL,NYU,YExp2) 729 ; 730 ( Y \== 0 -> 731 0 is Z mod Y, 732 X is Z / Y 733 ; 734 Z = 0 735 ) 736 ) 737 ; 738 get(X,XL,XU,XExp), 739 get(Y,YL,YU,YExp), 740 get(Z,ZL,ZU,ZExp), 741 min_divide(ZL,ZU,YL,YU,TXL), 742 NXL is max(XL,ceiling(TXL)), 743 max_divide(ZL,ZU,YL,YU,TXU), 744 NXU is min(XU,floor(TXU)), 745 ( New == yes -> 746 put(Y,YL,YU,[mytimes(X,Z)|YExp]), 747 put(Z,ZL,ZU,[mytimes2(X,Y)|ZExp]), 748 put(X,NXL,NXU,[mytimes(Y,Z)|XExp]) 749 ; 750 put(X,NXL,NXU,XExp) 751 ), 752 ( get(Y,YL2,YU2,YExp2) -> 753 min_divide(ZL,ZU,XL,XU,TYL), 754 NYL is max(YL2,ceiling(TYL)), 755 max_divide(ZL,ZU,XL,XU,TYU), 756 NYU is min(YU2,floor(TYU)), 757 put(Y,NYL,NYU,YExp2) 758 ; 759 NYL = Y, 760 NYU = Y 761 ), 762 ( get(Z,ZL2,ZU2,ZExp2) -> 763 min_times(NXL,NXU,NYL,NYU,TZL), 764 NZL is max(ZL2,TZL), 765 max_times(NXL,NXU,NYL,NYU,TZU), 766 NZU is min(ZU2,TZU), 767 put(Z,NZL,NZU,ZExp2) 768 ; 769 770 true 771 ) 772 ). 773 774max_times(L1,U1,L2,U2,Max) :- 775 Max is max(max(L1*L2,L1*U2),max(U1*L2,U1*U2)). 776min_times(L1,U1,L2,U2,Min) :- 777 Min is min(min(L1*L2,L1*U2),min(U1*L2,U1*U2)). 778max_divide(L1,U1,L2,U2,Max) :- 779 ( L2 =< 0 , U2 >= 0 -> 780 max_inf(Max) 781 ; div(L1,L2,DLL), 782 div(L1,U2,DLU), 783 div(U1,L2,DUL), 784 div(U1,U2,DUU), 785 Max is max(max(DLL,DLU),max(DUL,DUU)) 786 ). 787min_divide(L1,U1,L2,U2,Min) :- 788 ( L2 =< 0 , U2 >= 0 -> 789 min_inf(Min) 790 ; div(L1,L2,DLL), 791 div(L1,U2,DLU), 792 div(U1,L2,DUL), 793 div(U1,U2,DUU), 794 Min is min(min(DLL,DLU),min(DUL,DUU)) 795 ). 796 797 798mydiv(X,Y,Z,New) :- 799 ( Y == 0 -> fail ; true ), 800 ( nonvar(X) -> 801 ( nonvar(Y) -> 802 Z is X // Y 803 ; 804 get(Y,YL,YU,YExp), 805 ( New == yes -> 806 put(Y,YL,YU,[mydiv3(X,Z)|YExp]) 807 ; 808 true 809 ), 810 ( nonvar(Z) -> 811 % TODO: cover this 812 true 813 ; 814 get(Z,ZL,ZU,ZExp), 815 ( YL =< 0, YU >= 0 -> 816 NZL is max(-abs(X),ZL), 817 NZU is min(abs(X),ZU) 818 ; X >= 0, YL > 0 -> 819 NZL is max(X // YU, ZL), 820 NZU is min(X // YL, ZU) 821 ; % TODO: cover more cases 822 NZL = ZL, 823 NZU = ZU 824 ), 825 ( New == yes -> 826 put(Z,NZL,NZU,[mydiv2(X,Y)|ZExp]) 827 ; 828 put(Z,NZL,NZU,ZExp) 829 ) 830 ) 831 ) 832 ; nonvar(Y) -> 833 get(X,XL,XU,XExp), 834 ( nonvar(Z) -> 835 (Z >= 0, Y >= 0 -> 836 NXL is max(Z*Y,XL), 837 NXU is min((Z+1)*Y - 1,XU) 838 ; 839 % TODO: cover more cases 840 NXL = XL, 841 NXU = XU 842 ), 843 ( New == yes -> 844 put(X,NXL,NXU,[mydiv(Y,Z)|XExp]) 845 ; 846 put(X,NXL,NXU,XExp) 847 ) 848 ; 849 get(Z,ZL,ZU,ZExp), 850 ( XL >= 0, Y >= 0 -> 851 NZL is max(XL // Y,ZL), 852 NZU is min(XU // Y,ZU), 853 NXL is max(Y*NZL, XL), 854 NXU is min((NZU+1)*Y - 1, XU) 855 ; % TODO: cover more cases 856 NZL is max(-max(abs(XL),abs(XU)),ZL), 857 NZU is min(max(abs(XL),abs(XU)),ZU), 858 NXL = XL, 859 NXU = XU 860 ), 861 ( New == yes -> 862 put(X,NXL,NXU,[mydiv(Y,Z)|XExp]), 863 put(Z,NZL,NZU,[mydiv2(X,Y)|ZExp]) 864 ; 865 put(X,NXL,NXU,XExp), 866 ( nonvar(Z) -> true ; put(Z,NZL,NZU,ZExp) ) 867 ) 868 ) 869 ; nonvar(Z) -> 870 get(X,XL,XU,XExp), 871 get(Y,YL,YU,YExp), 872 (YL >= 0, XL >= 0 -> 873 NXL is max(YL*Z,XL), 874 NXU is min(YU*(Z + 1) - 1,XU) 875 ; % TODO: cover more cases 876 NXL = XL, 877 NXU = XU 878 ), 879 ( New == yes -> 880 put(X,NXL,NXU,[mydiv(Y,Z)|XExp]), 881 put(Y,YL,YU,[mydiv3(X,Z)|YExp]) 882 ; 883 put(X,NXL,NXU,XExp) 884 ) 885 ; 886 get(X,XL,XU,XExp), 887 get(Y,YL,YU,YExp), 888 get(Z,ZL,ZU,ZExp), 889 ( New == yes -> 890 put(Y,YL,YU,[mydiv3(X,Z)|YExp]), 891 put(Z,ZL,ZU,[mydiv2(X,Y)|ZExp]), 892 put(X,XL,XU,[mydiv(Y,Z)|XExp]) 893 ; 894 true 895 ) 896 ). 897 898 899%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 900mymax(X,Y,Z,New) :- 901 ( nonvar(X) -> 902 ( nonvar(Y) -> 903 Z is max(X,Y) 904 ; nonvar(Z) -> 905 ( Z == X -> 906 geq(X,Y,yes) 907 ; Z > X -> 908 Y = Z 909 %; Z < X 910 % fail 911 ) 912 ; 913 get(Y,YL,YU,YExp), 914 get(Z,ZL,ZU,ZExp), 915 ( YL >= X -> 916 Z = Y 917 ; X >= YU -> 918 Z = X 919 ; X < ZL -> 920 Y = Z 921 ; 922 ( New == yes -> 923 put(Y,YL,YU,[mymax(X,Z)|YExp]) 924 ; 925 true 926 ), 927 NZL is max(ZL,X), 928 NZU is min(ZU,YU), 929 ( New == yes -> 930 put(Z,NZL,NZU,[mymax2(X,Y)|ZExp]) 931 ; 932 put(Z,NZL,NZU,ZExp) 933 ), 934 ( get(Y,YL2,YU2,YExp2) -> 935 NYU is min(YU2,NZU), 936 put(Y,YL2,NYU,YExp2) 937 ; 938 true 939 ) 940 ) 941 ) 942 ; nonvar(Y) -> 943 mymax(Y,X,Z,New) 944 ; nonvar(Z) -> 945 get(X,XL,XU,XExp), 946 get(Y,YL,YU,YExp), 947 ( XU < Z -> 948 Y = Z 949 ; % XU >= Z -> 950 YU < Z -> 951 X = Z 952 ; % YU >= Z 953 XL > YU -> 954 Z = X 955 ; YL > XU -> 956 Z = Y 957 ; 958 ( New == yes -> 959 put(Y,YL,YU,[mymax(X,Z)|YExp]), 960 put(X,XL,Z,[mymax(Y,Z)|XExp]) 961 ; 962 put(X,XL,Z,XExp) 963 ), 964 ( get(Y,YL2,YU2,YExp2) -> 965 NYU is min(YU2,Z), 966 put(Y,YL2,NYU,YExp2) 967 ; 968 true 969 ) 970 ) 971 ; X == Y -> 972 Z = X 973 ; Z == X -> 974 geq(X,Y,yes) 975 ; Z == Y -> 976 geq(Y,X,yes) 977 ; 978 get(X,XL,XU,XExp), 979 get(Y,YL,YU,YExp), 980 get(Z,ZL,ZU,ZExp), 981 NZL is max(ZL,max(XL,YL)), 982 NZU is min(ZU,max(XU,YU)), 983 ( New == yes -> 984 put(X,XL,XU,[mymax(Y,Z)|XExp]), 985 put(Y,YL,YU,[mymax(X,Z)|YExp]), 986 put(Z,NZL,NZU,[mymax2(X,Y)|ZExp]) 987 ; 988 put(Z,NZL,NZU,ZExp) 989 ), 990 ( get(X,XL2,XU2,XExp2) -> 991 ( XU2 < NZL -> 992 Y = Z 993 ; YU < NZL -> 994 X = Z 995 ; YU < XL2 -> 996 X = Z 997 ; XU2 < YL -> 998 Y = Z 999 ; 1000 NXU is min(XU2,NZU), 1001 put(X,XL2,NXU,XExp2), 1002 ( get(Y,YL2,YU2,YExp2) -> 1003 NYU is min(YU2,NZU), 1004 put(Y,YL2,NYU,YExp2) 1005 ; 1006 mymax(Y,X,Z,no) 1007 ) 1008 ) 1009 ; 1010 mymax(X,Y,Z,no) 1011 ) 1012 ). 1013 1014mymin(X,Y,Z,New) :- 1015 ( nonvar(X) -> 1016 ( nonvar(Y) -> 1017 Z is min(X,Y) 1018 ; nonvar(Z) -> 1019 ( Z == X -> 1020 leq(X,Y,yes) 1021 ; Z < X -> 1022 Y = Z 1023 %; Z > X 1024 % fail 1025 ) 1026 ; 1027 get(Y,YL,YU,YExp), 1028 get(Z,ZL,ZU,ZExp), 1029 ( YL >= X -> 1030 Z = X 1031 ; X >= YU -> 1032 Z = Y 1033 ; X > ZU -> 1034 Y = Z 1035 ; 1036 ( New == yes -> 1037 put(Y,YL,YU,[mymin(X,Z)|YExp]) 1038 ; 1039 true 1040 ), 1041 NZL is max(ZL,YL), 1042 NZU is min(ZU,X), 1043 ( New == yes -> 1044 put(Z,NZL,NZU,[mymin2(X,Y)|ZExp]) 1045 ; 1046 put(Z,NZL,NZU,ZExp) 1047 ), 1048 ( get(Y,YL2,YU2,YExp2) -> 1049 NYL is max(YL2,NZL), 1050 put(Y,NYL,YU2,YExp2) 1051 ; 1052 true 1053 ) 1054 ) 1055 ) 1056 ; nonvar(Y) -> 1057 mymin(Y,X,Z,New) 1058 ; nonvar(Z) -> 1059 get(X,XL,XU,XExp), 1060 get(Y,YL,YU,YExp), 1061 ( XL > Z -> 1062 Y = Z 1063 ; % XL =< Z -> 1064 YL > Z -> 1065 X = Z 1066 ; % YL =< Z 1067 XU =< YL -> 1068 Z = X 1069 ; YU =< XL -> 1070 Z = Y 1071 ; 1072 ( New == yes -> 1073 put(Y,YL,YU,[mymin(X,Z)|YExp]), 1074 put(X,Z,XU,[mymin(Y,Z)|XExp]) 1075 ; 1076 put(X,Z,XU,XExp) 1077 ), 1078 ( get(Y,YL2,YU2,YExp2) -> 1079 NYL is max(YL2,Z), 1080 put(Y,NYL,YU2,YExp2) 1081 ; 1082 true 1083 ) 1084 ) 1085 ; X == Y -> 1086 Z = X 1087 ; Z == X -> 1088 leq(X,Y,yes) 1089 ; Z == Y -> 1090 leq(Y,X,yes) 1091 ; 1092 get(X,XL,XU,XExp), 1093 get(Y,YL,YU,YExp), 1094 get(Z,ZL,ZU,ZExp), 1095 NZL is max(ZL,min(XL,YL)), 1096 NZU is min(ZU,min(XU,YU)), 1097 ( New == yes -> 1098 put(X,XL,XU,[mymin(Y,Z)|XExp]), 1099 put(Y,YL,YU,[mymin(X,Z)|YExp]), 1100 put(Z,NZL,NZU,[mymin2(X,Y)|ZExp]) 1101 ; 1102 put(Z,NZL,NZU,ZExp) 1103 ), 1104 ( get(X,XL2,XU2,XExp2) -> 1105 ( XL2 > NZU -> 1106 Y = Z 1107 ; YL > NZU -> 1108 X = Z 1109 ; YU < XL2 -> 1110 Y = Z 1111 ; XU2 < YL -> 1112 X = Z 1113 ; 1114 NXL is max(XL2,NZL), 1115 put(X,NXL,XU2,XExp2), 1116 ( get(Y,YL2,YU2,YExp2) -> 1117 NYL is max(YL2,NZL), 1118 put(Y,NYL,YU2,YExp2) 1119 ; 1120 mymin(Y,X,Z,no) 1121 ) 1122 ) 1123 ; 1124 mymin(X,Y,Z,no) 1125 ) 1126 ). 1127 1128myabs(X,Y,New) :- 1129 ( nonvar(X) -> 1130 Y is abs(X) 1131 ; nonvar(Y) -> 1132 Y >= 0, 1133 get(X,LX,UX,ExpX), 1134 ( UX < Y -> 1135 X is (-Y) 1136 ; LX > (-Y) -> 1137 X = Y 1138 ; 1139 NLX is (-Y), 1140 ( New == yes -> 1141 put(X,NLX,Y,[myabs(Y)|ExpX]) 1142 ; 1143 put(X,NLX,Y,ExpX) 1144 ) 1145 ) 1146 ; 1147 get(X,LX,UX,ExpX), 1148 get(Y,LY,UY,ExpY), 1149 UY > 0, 1150 ( New == yes -> 1151 put(X,LX,UX,[myabs(Y)|ExpX]) 1152 ; 1153 true 1154 ), 1155 ( LX =< 0, UX >= 0 -> 1156 NLY is max(0,LY) 1157 ; 1158 NLY is max(min(abs(LX),abs(UX)),max(LY,0)) 1159 ), 1160 NUY is min(UY,max(abs(LX),abs(UX))), 1161 ( New == yes -> 1162 put(Y,NLY,NUY,[myabs2(X)|ExpY]) 1163 ; 1164 put(Y,NLY,NUY,ExpY) 1165 ), 1166 ( var(X) -> 1167 get(X,LX2,UX2,ExpX2), 1168 ( LX2 == LX, UX2 == UX -> 1169 ( NLY == 0 -> 1170 NLX is max(LX,(-NUY)), 1171 NUX is min(UX,NUY) 1172 ; LX > (-NLY) -> 1173 NLX is max(LX,NLY), 1174 NUX is min(UX,NUY) 1175 ; 1176 NLX is max((-NUY),LX), 1177 ( UX < NLY -> 1178 NUX is min((-NLY),UX) 1179 ; 1180 NUX is min(NUY,UX) 1181 ) 1182 ), 1183 put(X,NLX,NUX,ExpX2) 1184 ; 1185 true 1186 ) 1187 ; 1188 true 1189 ) 1190 ). 1191 1192mymod(X,Y,Z,New) :- % Z is X mod Y 1193 ( nonvar(X) -> 1194 ( nonvar(Y) -> 1195 Z is X mod Y 1196 ; nonvar(Z) -> 1197 get(Y,YL,YU,YExp), 1198 ( Z > 0 -> 1199 ( X == Z -> 1200 no_overlap(-X,X,YL,YU,NYL,NYU), 1201 ( New == yes -> 1202 put(Y,NYL,NYU,[mymod2(X,Z)|YExp]) 1203 ; 1204 put(Y,NYL,NYU,YExp) 1205 ) 1206 ; % Z < X 1207 no_overlap(-Z,Z,YL,YU,YL1,YU1), 1208 in_between(-X,X,YL1,YU1,NYL,NYU), 1209 ( New == yes -> 1210 put(Y,NYL,NYU,[mymod2(X,Z)|YExp]) 1211 ; 1212 put(Y,NYL,NYU,YExp) 1213 ) 1214 ) 1215 ; Z < 0 -> 1216 ( X == Z -> 1217 no_overlap(X,-X,YL,YU,NYL,NYU), 1218 ( New == yes -> 1219 put(Y,NYL,NYU,[mymod2(X,Z)|YExp]) 1220 ; 1221 put(Y,NYL,NYU,YExp) 1222 ) 1223 ; % Z < X 1224 no_overlap(Z,-Z,YL,YU,YL1,YU1), 1225 in_between(X,-X,YL1,YU1,NYL,NYU), 1226 ( New == yes -> 1227 put(Y,NYL,NYU,[mymod2(X,Z)|YExp]) 1228 ; 1229 put(Y,NYL,NYU,YExp) 1230 ) 1231 ) 1232 ; % Z == 0 1233 ( X == 0 -> 1234 no_overlap(0,0,YL,YU,NYL,NYU),% Y \== 0 1235 ( New == yes -> 1236 put(Y,NYL,NYU,[mymod2(X,Z)|YExp]) 1237 ; 1238 put(Y,NYL,NYU,YExp) 1239 ) 1240 ; % X \== 0 1241 PX is abs(X), 1242 in_between(-PX,PX,YL,YU,NYL,NYU),% |Y| < |X| 1243 ( New == yes -> 1244 put(Y,NYL,NYU,[mymod2(X,Z)|YExp]) 1245 ; 1246 put(Y,NYL,NYU,YExp) 1247 ) 1248 ) 1249 ) 1250 ; % var(Y), var(Z) 1251 ( New == yes -> 1252 get(Y,YL,YU,YExp), 1253 get(Z,ZL,ZU,ZExp), 1254 put(Y,YL,YU,[mymod2(X,Z)|YExp]), 1255 put(Z,ZL,ZU,[mymod3(X,Y)|ZExp]) 1256 ; 1257 true 1258 ) 1259 ) 1260 ; nonvar(Y) -> 1261 Y \== 0, 1262 ( nonvar(Z) -> 1263 get(X,XL,XU,XExp), 1264 ( Z > 0 -> 1265 NXL is max(XL,1), 1266 ( New == yes -> 1267 put(X,NXL,XU,[mymod1(Y,Z)|XExp]) 1268 ; 1269 put(X,NXL,XU,XExp) 1270 ) 1271 ; Z < 0 -> 1272 NXU is min(XU,-1), 1273 ( New == yes -> 1274 put(X,XL,NXU,[mymod1(Y,Z)|XExp]) 1275 ; 1276 put(X,XL,NXU,XExp) 1277 ) 1278 ; 1279 ( New == yes -> 1280 put(X,XL,XU,[mymod1(Y,Z)|XExp]) 1281 ; 1282 put(X,XL,XU,XExp) 1283 ) 1284 ) 1285 ; 1286 ( New == yes -> 1287 get(X,XL,XU,XExp), 1288 get(Z,ZL,ZU,ZExp), 1289 put(X,XL,XU,[mymod1(Y,Z)|XExp]), 1290 put(Z,ZL,ZU,[mymod3(X,Y)|ZExp]) 1291 ; 1292 true 1293 ) 1294 ) 1295 ; nonvar(Z) -> 1296 ( New == yes -> 1297 get(X,XL,XU,XExp), 1298 get(Y,YL,YU,YExp), 1299 put(X,XL,XU,[mymod1(Y,Z)|XExp]), 1300 put(Y,YL,YU,[mymod2(X,Z)|YExp]) 1301 ; 1302 true 1303 ) 1304 ; 1305 ( New == yes -> 1306 get(X,XL,XU,XExp), 1307 get(Y,YL,YU,YExp), 1308 get(Z,ZL,ZU,ZExp), 1309 put(X,XL,XU,[mymod1(Y,Z)|XExp]), 1310 put(Y,YL,YU,[mymod2(X,Z)|YExp]), 1311 put(Z,ZL,ZU,[mymod3(X,Y)|ZExp]) 1312 ; 1313 true 1314 ) 1315 ). 1316 1317no_overlap(XL,XU,YL,YU,NYL,NYU) :- 1318 ( XL =< YL -> 1319 NYL is XU + 1, 1320 NYU = YU 1321 ; YU =< XU -> 1322 NYU is XL - 1, 1323 NYL is YL 1324 ; 1325 NYL = YL, 1326 NYU = YU 1327 ). 1328in_between(XL,XU,YL,YU,NYL,NYU) :- 1329 ( XL >= YL -> 1330 NYL is XL + 1 1331 ; 1332 NYL = YL 1333 ), 1334 ( XU =< YU -> 1335 NYU is XU -1 1336 ; 1337 NYU = YU 1338 ). 1339 1340%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1341% TODO 1342% trigger reified constraints when geq is added 1343reified_geq(X,Y,B) :- 1344 ( var(B) -> 1345 ( nonvar(X) -> 1346 ( nonvar(Y) -> 1347 ( X >= Y -> 1348 B = 1 1349 ; 1350 B = 0 1351 ) 1352 ; 1353 get(Y,L,U,Expr), 1354 ( X >= U -> 1355 B = 1 1356 ; X < L -> 1357 B = 0 1358 ; 1359 put(Y,L,U,[reified_leq(X,B)|Expr]), 1360 get(B,BL,BU,BExpr), 1361 put(B,BL,BU,[reified_geq2(X,Y)|BExpr]), 1362 B in 0..1 1363 ) 1364 ) 1365 ; nonvar(Y) -> 1366 get(X,L,U,Expr), 1367 ( L >= Y -> 1368 B = 1 1369 ; U < Y -> 1370 B = 0 1371 ; 1372 put(X,L,U,[reified_geq(Y,B)|Expr]), 1373 get(B,BL,BU,BExpr), 1374 put(B,BL,BU,[reified_geq2(X,Y)|BExpr]), 1375 B in 0..1 1376 ) 1377 ; 1378 get(X,XL,XU,XExpr), 1379 get(Y,YL,YU,YExpr), 1380 ( XL >= YU -> 1381 B = 1 1382 ; XU < YL -> 1383 B = 0 1384 ; member(geq(Z,_State),XExpr), 1385 Z == Y -> 1386 B = 1 1387 ; 1388 put(X,XL,XU,[reified_geq(Y,B)|XExpr]), 1389 put(Y,YL,YU,[reified_leq(X,B)|YExpr]), 1390 get(B,BL,BU,BExpr), 1391 put(B,BL,BU,[reified_geq2(X,Y)|BExpr]), 1392 B in 0..1 1393 ) 1394 ) 1395 ; B == 1 -> 1396 X #>= Y 1397 ; B == 0 -> 1398 X #< Y 1399 ). 1400 1401check_leq(X,Y) :- 1402 ( nonvar(X) -> 1403 ( nonvar(Y) -> 1404 X =< Y 1405 ; 1406 bounds(Y,L,_), 1407 X =< L 1408 ) 1409 ; 1410 ( nonvar(Y) -> 1411 bounds(X,_,U), 1412 U =< Y 1413 ; 1414 bounds(X,_,UX), 1415 bounds(Y,LY,_), 1416 UX =< LY 1417 ) 1418 ). 1419 1420check_lt(X,Y) :- 1421 ( nonvar(X) -> 1422 ( nonvar(Y) -> 1423 X < Y 1424 ; 1425 bounds(Y,L,_), 1426 X < L 1427 ) 1428 ; 1429 ( nonvar(Y) -> 1430 bounds(X,_,U), 1431 U < Y 1432 ; 1433 bounds(X,_,UX), 1434 bounds(Y,LY,_), 1435 UX < LY 1436 ) 1437 ). 1438 1439%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1440reified_eq(X,Y,B) :- 1441 ( var(B) -> 1442 ( nonvar(X) -> 1443 ( nonvar(Y) -> 1444 ( X == Y -> 1445 B = 1 1446 ; 1447 B = 0 1448 ) 1449 ; 1450 get(Y,L,U,Expr), 1451 ( L > X -> 1452 B = 0 1453 ; U < X -> 1454 B = 0 1455 ; 1456 put(Y,L,U,[reified_eq(X,B)|Expr]), 1457 get(B,BL,BU,BExpr), 1458 put(B,BL,BU,[reified_eq2(X,Y)|BExpr]), 1459 B in 0..1 1460 ) 1461 ) 1462 ; nonvar(Y) -> 1463 reified_eq(Y,X,B) 1464 ; X == Y -> 1465 B = 1 1466 ; 1467 get(X,XL,XU,XExpr), 1468 get(Y,YL,YU,YExpr), 1469 ( XL > YU -> 1470 B = 0 1471 ; YL > XU -> 1472 B = 0 1473 ; member(neq(Z,_),XExpr), 1474 Z == Y -> 1475 B = 0 1476 ; 1477 put(X,XL,XU,[reified_eq(Y,B)|XExpr]), 1478 put(Y,YL,YU,[reified_eq(X,B)|YExpr]), 1479 get(B,BL,BU,BExpr), 1480 put(B,BL,BU,[reified_eq2(X,Y)|BExpr]), 1481 B in 0..1 1482 ) 1483 ) 1484 ; B == 1 -> 1485 X #= Y 1486 ; B == 0 -> 1487 X #\= Y 1488 ). 1489 1490 1491check_eq(X,Y) :- 1492 X == Y. 1493%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1494reified_neq(X,Y,B) :- 1495 mynot(B,B1), 1496 reified_eq(X,Y,B1). 1497 1498%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1499mynot(B1,B2) :- 1500 ( nonvar(B1) -> 1501 ( B1 == 1 -> 1502 B2 = 0 1503 ; B1 == 0 -> 1504 B2 = 1 1505 ) 1506 ; nonvar(B2) -> 1507 mynot(B2,B1) 1508 ; 1509 get(B1,L1,U1,Expr1), 1510 get(B2,L2,U2,Expr2), 1511 put(B2,L2,U2,[mynot(B1)|Expr2]), 1512 put(B1,L1,U1,[mynot(B2)|Expr1]), 1513 B1 in 0..1, 1514 B2 in 0..1 1515 ). 1516%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1517myimpl(B1,B2) :- 1518 ( nonvar(B1) -> 1519 ( B1 == 1 -> 1520 B2 = 1 1521 ; B1 == 0 -> 1522 B2 in 0..1 1523 ) 1524 ; nonvar(B2) -> 1525 ( B2 == 0 -> 1526 B1 = 0 1527 ; B2 == 1 -> 1528 B1 in 0..1 1529 ) 1530 ; 1531 get(B1,L1,U1,Expr1), 1532 get(B2,L2,U2,Expr2), 1533 put(B1,L1,U1,[myimpl(B2)|Expr1]), 1534 put(B2,L2,U2,[myimpl2(B1)|Expr2]), 1535 B1 in 0..1, 1536 B2 in 0..1 1537 ). 1538%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1539myand(X,Y,Z) :- 1540 ( nonvar(X) -> 1541 ( X == 1 -> 1542 Y in 0..1, 1543 Y = Z 1544 ; X == 0 -> 1545 Y in 0..1, 1546 Z = 0 1547 ) 1548 ; nonvar(Y) -> 1549 myand(Y,X,Z) 1550 ; nonvar(Z) -> 1551 ( Z == 1 -> 1552 X = 1, 1553 Y = 1 1554 ; Z == 0 -> 1555 X in 0..1, 1556 Y in 0..1, 1557 X + Y #=< 1 1558 ) 1559 ; 1560 get(X,LX,UX,ExpX), 1561 get(Y,LY,UY,ExpY), 1562 get(Z,LZ,UZ,ExpZ), 1563 put(X,LX,UX,[myand(Y,Z)|ExpX]), 1564 put(Y,LY,UY,[myand(X,Z)|ExpY]), 1565 put(Z,LZ,UZ,[myand2(X,Y)|ExpZ]), 1566 [X,Y,Z] in 0..1 1567 ). 1568 1569%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1570myor(X,Y,Z) :- 1571 ( nonvar(X) -> 1572 ( X == 0 -> 1573 Y in 0..1, 1574 Y = Z 1575 ; X == 1 -> 1576 Y in 0..1, 1577 Z = 1 1578 ) 1579 ; nonvar(Y) -> 1580 myor(Y,X,Z) 1581 ; nonvar(Z) -> 1582 ( Z == 0 -> 1583 X = 0, 1584 Y = 0 1585 ; Z == 1 -> 1586 X in 0..1, 1587 Y in 0..1, 1588 X + Y #>= 1 1589 ) 1590 ; 1591 get(X,LX,UX,ExpX), 1592 get(Y,LY,UY,ExpY), 1593 get(Z,LZ,UZ,ExpZ), 1594 put(X,LX,UX,[myor(Y,Z)|ExpX]), 1595 put(Y,LY,UY,[myor(X,Z)|ExpY]), 1596 put(Z,LZ,UZ,[myor2(X,Y)|ExpZ]), 1597 [X,Y,Z] in 0..1 1598 ). 1599 1600%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1601myxor(X,Y,Z) :- 1602 ( nonvar(X) -> 1603 ( X == 0 -> 1604 Y in 0..1, 1605 Y = Z 1606 ; X == 1 -> 1607 mynot(Y,Z) 1608 ) 1609 ; nonvar(Y) -> 1610 myxor(Y,X,Z) 1611 ; nonvar(Z) -> 1612 ( Z == 0 -> 1613 X = Y, 1614 [X,Y] in 0..1 1615 ; Z == 1 -> 1616 X in 0..1, 1617 Y in 0..1, 1618 X + Y #= 1 1619 ) 1620 ; 1621 get(X,LX,UX,ExpX), 1622 get(Y,LY,UY,ExpY), 1623 get(Z,LZ,UZ,ExpZ), 1624 put(X,LX,UX,[myxor(Y,Z)|ExpX]), 1625 put(Y,LY,UY,[myxor(X,Z)|ExpY]), 1626 put(Z,LZ,UZ,[myxor2(X,Y)|ExpZ]), 1627 [X,Y,Z] in 0..1 1628 ). 1629 1630 1631%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1632get(X,L,U,Exp) :- 1633 ( get_attr(X,bounds,Attr) -> 1634 Attr = bounds(L,U,Exp) 1635 ; var(X) -> 1636 min_inf(L), 1637 max_inf(U), 1638 Exp = [] 1639 ). 1640 1641put(X,L,U,Exp) :- 1642 L =< U, 1643 ( L == U -> 1644 X = L, 1645 trigger_exps(Exp,X) 1646 ; 1647 ( get_attr(X,bounds,Attr) -> 1648 put_attr(X,bounds,bounds(L,U,Exp)), 1649 Attr = bounds(OldL,OldU,_), 1650 ( OldL == L, OldU == U -> 1651 true 1652 ; 1653 %format('\t~w in ~w .. ~w\n',[X,L,U]), 1654 trigger_exps(Exp,X), 1655 notify(X,bounds) 1656 ) 1657 ; 1658 %format('\t~w in ~w .. ~w\n',[X,L,U]), 1659 put_attr(X,bounds,bounds(L,U,Exp)), 1660 notify(X,bounds) 1661 ) 1662 ). 1663 1664%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1665 1666% SWI-Prolog 5.7.x has unbounded arithmetic. What to do? 1667 1668min_inf(Inf) :- 1669 ( current_prolog_flag(min_integer,MInf) 1670 -> Inf is MInf + 1 1671 ; Inf = -9223372036854775807 1672 ). 1673 1674max_inf(Inf) :- 1675 ( current_prolog_flag(max_integer,Inf) 1676 -> true 1677 ; Inf = 9223372036854775807 1678 ). 1679 1680%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1681attr_unify_hook(bounds(L,U,Exp),Other) :- 1682 ( get(Other,OL,OU,OExp) -> 1683 NL is max(L,OL), 1684 NU is min(U,OU), 1685 append(Exp,OExp,NExp), 1686 check_neqs(NExp,Other), 1687 put(Other,NL,NU,NExp) 1688 ; % nonvar(Other) -> 1689 Other >= L, 1690 Other =< U, 1691 trigger_exps(Exp,Other) 1692 ). 1693 1694check_neqs([],_). 1695check_neqs([E|Es],X) :- 1696 ( E = neq(Y,_), 1697 X == Y -> 1698 fail 1699 ; 1700 check_neqs(Es,X) 1701 ). 1702 1703 1704trigger_exps([],_). 1705trigger_exps([E|Es],X) :- 1706 trigger_exp(E,X), 1707 trigger_exps(Es,X). 1708 1709trigger_exp(geq(Y,State),X) :- 1710 ( is_active(State) -> 1711 geq(X,Y,no) 1712 ; 1713 true 1714 ). 1715trigger_exp(leq(Y,State),X) :- 1716 ( is_active(State) -> 1717 leq(X,Y,no) 1718 ; 1719 true 1720 ). 1721trigger_exp(neq(Y,State),X) :- 1722 ( is_active(State) -> 1723 neq(X,Y,no) 1724 ; 1725 true 1726 ). 1727trigger_exp(myplus(Y,Z),X) :- 1728 myplus(X,Y,Z,no). 1729trigger_exp(myplus2(A,B),X) :- 1730 myplus(A,B,X,no). 1731 1732trigger_exp(mytimes(Y,Z),X) :- 1733 mytimes(X,Y,Z,no). 1734trigger_exp(mytimes2(A,B),X) :- 1735 mytimes(A,B,X,no). 1736 1737trigger_exp(mymax(Y,Z),X) :- 1738 mymax(X,Y,Z,no). 1739trigger_exp(mymax2(X,Y),Z) :- 1740 mymax(X,Y,Z,no). 1741 1742trigger_exp(mymin(Y,Z),X) :- 1743 mymin(X,Y,Z,no). 1744trigger_exp(mymin2(X,Y),Z) :- 1745 mymin(X,Y,Z,no). 1746 1747trigger_exp(reified_leq(X,B),Y) :- 1748 reified_geq(X,Y,B). 1749trigger_exp(reified_geq(Y,B),X) :- 1750 reified_geq(X,Y,B). 1751trigger_exp(reified_geq2(X,Y),B) :- 1752 reified_geq(X,Y,B). 1753 1754trigger_exp(reified_eq(Y,B),X) :- 1755 reified_eq(X,Y,B). 1756trigger_exp(reified_eq2(X,Y),B) :- 1757 reified_eq(X,Y,B). 1758 1759trigger_exp(mynot(Y),X) :- 1760 mynot(X,Y). 1761 1762trigger_exp(myimpl(Y),X) :- 1763 myimpl(X,Y). 1764trigger_exp(myimpl2(X),Y) :- 1765 myimpl(X,Y). 1766 1767trigger_exp(myand(Y,Z),X) :- 1768 myand(X,Y,Z). 1769trigger_exp(myand2(X,Y),Z) :- 1770 myand(X,Y,Z). 1771 1772trigger_exp(myor(Y,Z),X) :- 1773 myor(X,Y,Z). 1774trigger_exp(myor2(X,Y),Z) :- 1775 myor(X,Y,Z). 1776 1777trigger_exp(myxor(Y,Z),X) :- 1778 myxor(X,Y,Z). 1779trigger_exp(myxor2(X,Y),Z) :- 1780 myxor(X,Y,Z). 1781 1782trigger_exp(myabs(Y),X) :- 1783 myabs(X,Y,no). 1784trigger_exp(myabs2(X),Y) :- 1785 myabs(X,Y,no). 1786 1787trigger_exp(mymod1(Y,Z),X) :- 1788 mymod(X,Y,Z,no). 1789trigger_exp(mymod2(X,Z),Y) :- 1790 mymod(X,Y,Z,no). 1791trigger_exp(mymod3(X,Y),Z) :- 1792 mymod(X,Y,Z,no). 1793 1794trigger_exp(mydiv(Y,Z),X) :- 1795 mydiv(X,Y,Z,no). 1796trigger_exp(mydiv2(A,B),X) :- 1797 mydiv(A,B,X,no). 1798trigger_exp(mydiv3(A,B),X) :- 1799 mydiv(A,X,B,no). 1800 1801trigger_exp(rel_tuple(Relation,Tuple), _) :- 1802 ( ground(Tuple) -> 1803 memberchk(Tuple, Relation) 1804 ; 1805 relation_unifiable(Relation, Tuple, Us), 1806 Us \= [], 1807 ( Us = [Single] -> 1808 Single = Tuple 1809 ; 1810 ( Us == Relation -> 1811 true 1812 ; 1813 tuple_domain(Tuple, Us) 1814 ) 1815 ) 1816 ). 1817 1818trigger_exp(serialized(Duration,Left,Right), X) :- 1819 myserialized(Duration, Left, Right, X). 1820 1821 1822memberchk_eq(X,[Y|Ys],Z) :- 1823 ( X == Y -> 1824 Z = Y 1825 ; memberchk_eq(X,Ys,Z) 1826 ). 1827 1828 1829%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1830 1831tuples_in(Tuples, Relation) :- 1832 ground(Relation), 1833 bind_unique(Tuples, Relation), 1834 approx_tuples_domain(Tuples, Relation), 1835 tuples_freeze(Tuples, Relation). 1836 1837bind_unique([], _). 1838bind_unique([Tuple|Ts], Relation) :- 1839 relation_unifiable(Relation, Tuple, Us), 1840 Us \= [], 1841 ( Us = [Single] -> 1842 Single = Tuple 1843 ; 1844 true 1845 ), 1846 bind_unique(Ts, Relation). 1847 1848 1849 % The following predicates find component-wise extrema in the relation. 1850 1851relation_mins_maxs(Relation, Mins, Maxs) :- 1852 Relation = [R|_], 1853 relation_mins_maxs(Relation, R, Mins, R, Maxs). 1854 1855relation_mins_maxs([], Mins, Mins, Maxs, Maxs). 1856relation_mins_maxs([R|Rs], Mins0, Mins, Maxs0, Maxs) :- 1857 components_mins_maxs(R, Mins0, Mins1, Maxs0, Maxs1), 1858 relation_mins_maxs(Rs, Mins1, Mins, Maxs1, Maxs). 1859 1860components_mins_maxs([], [], [], [], []). 1861components_mins_maxs([C|Cs], [Min0|Mins0], [Min|Mins], [Max0|Maxs0], [Max|Maxs]) :- 1862 Min is min(Min0, C), 1863 Max is max(Max0, C), 1864 components_mins_maxs(Cs, Mins0, Mins, Maxs0, Maxs). 1865 1866 1867 % Approximate the domains of each tuple variable for all tuples. 1868 % Heuristics: Take component-wise mins/maxs of the relation. 1869 1870approx_tuples_domain(Tuples, Relation) :- 1871 relation_mins_maxs(Relation, Mins, Maxs), 1872 constrain_domains(Tuples, Mins, Maxs). 1873 1874constrain_domains([], _, _). 1875constrain_domains([Tuple|Tuples], Mins, Maxs) :- 1876 constrain_domain(Tuple, Mins, Maxs), 1877 constrain_domains(Tuples, Mins, Maxs). 1878 1879constrain_domain([], [], []). 1880constrain_domain([T|Ts], [Min|Mins], [Max|Maxs]) :- 1881 T in Min..Max, 1882 constrain_domain(Ts, Mins, Maxs). 1883 1884tuple_domain(Tuple, Relation) :- 1885 relation_mins_maxs(Relation, Mins, Maxs), 1886 constrain_domain(Tuple, Mins, Maxs). 1887 1888 % Set up the attributes for each tuple variable. 1889 % Attributes are rel_tuple(Rel, Tuple) terms: 1890 % Rel: the relation of which Tuple must be an element 1891 % Tuple: the tuple to which this variable belongs 1892 % Note that the variable is itself part of the Tuple of its attribute. 1893 1894tuple_freeze([], _, _). 1895tuple_freeze([T|Ts], Tuple, Relation) :- 1896 ( var(T) -> 1897 get(T, L, U, Exp), 1898 put(T, L, U, [rel_tuple(Relation,Tuple)|Exp]) 1899 ; 1900 true 1901 ), 1902 tuple_freeze(Ts, Tuple, Relation). 1903 1904tuples_freeze([], _). 1905tuples_freeze([Tuple|Tuples], Relation) :- 1906 tuple_freeze(Tuple, Tuple, Relation), 1907 tuples_freeze(Tuples, Relation). 1908 1909 % Find all tuples in the relation that can unify with Tuple, not 1910 % taking into account attributes (like constraints), as that would 1911 % trigger attr_unify_hook recursively. 1912 1913relation_unifiable([], _, []). 1914relation_unifiable([R|Rs], Tuple, Us) :- 1915 ( unifiable(R, Tuple, _) -> 1916 Us = [R|Rest] 1917 ; 1918 Rest = Us 1919 ), 1920 relation_unifiable(Rs, Tuple, Rest). 1921 1922%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1923 1924 % serialized/2; see Dorndorf et al. 2000, "Constraint Propagation 1925 % Techniques for the Disjunctive Scheduling Problem" 1926 1927 % attribute: serialized(Duration, Left, Right) 1928 % Left and Right are lists of Start-Duration pairs representing 1929 % other tasks occupying the same resource 1930 1931 % Currently implements 2-b-consistency 1932 1933serialized(Starts, Durations) :- 1934 pair_up(Starts, Durations, SDs), 1935 serialize(SDs, []). 1936 1937 1938pair_up([], [], []). 1939pair_up([A|As], [B|Bs], [A-B|ABs]) :- pair_up(As, Bs, ABs). 1940 1941 1942 % store attributes for serialized/2 constraint 1943 1944serialize([], _). 1945serialize([Start-Duration|SDs], Left) :- 1946 ( var(Start) -> 1947 get(Start, L, U, Exp), 1948 put(Start, L, U, [serialized(Duration,Left,SDs)|Exp]) 1949 ; 1950 true 1951 ), 1952 myserialized(Duration, Left, SDs, Start), 1953 serialize(SDs, [Start-Duration|Left]). 1954 1955 % consistency check / propagation 1956 1957myserialized(Duration, Left, Right, Start) :- 1958 myserialized(Left, Start, Duration), 1959 myserialized(Right, Start, Duration). 1960 1961 1962earliest_start_time(Start, EST) :- 1963 ( var(Start) -> 1964 get(Start, EST, _, _) 1965 ; 1966 EST = Start 1967 ). 1968 1969latest_start_time(Start, LST) :- 1970 ( var(Start) -> 1971 get(Start, _, LST, _) 1972 ; 1973 LST = Start 1974 ). 1975 1976 1977myserialized([], _, _). 1978myserialized([S_I-D_I|SDs], S_J, D_J) :- 1979 ( var(S_I) -> 1980 serialize_lower_bound(S_I, D_I, Start, D_J), 1981 ( var(S_I) -> % STILL variable? 1982 serialize_upper_bound(S_I, D_I, Start, D_J) 1983 ; 1984 true 1985 ) 1986 ; var(S_J) -> 1987 serialize_lower_bound(S_J, D_J, S, D_I), 1988 ( var(S_J) -> 1989 serialize_upper_bound(S_J, D_J, S, D_I) 1990 ; 1991 true 1992 ) 1993 ; 1994 ( S_I + D_I =< S_J -> 1995 true 1996 ; S_J + D_J =< S_I -> 1997 true 1998 ; 1999 fail 2000 ) 2001 ), 2002 myserialized(SDs, S_J, D_J). 2003 2004serialize_lower_bound(I, D_I, J, D_J) :- 2005 get(I, EST_I, U, Exp), 2006 latest_start_time(J, LST_J), 2007 ( EST_I + D_I > LST_J -> 2008 earliest_start_time(J, EST_J), 2009 EST is max(EST_I, EST_J+D_J), 2010 put(I, EST, U, Exp) 2011 ; 2012 true 2013 ). 2014 2015serialize_upper_bound(I, D_I, J, D_J) :- 2016 get(I, L, LST_I, Exp), 2017 earliest_start_time(J, EST_J), 2018 ( EST_J + D_J > LST_I -> 2019 latest_start_time(J, LST_J), 2020 LST is min(LST_I, LST_J-D_I), 2021 put(I, L, LST, Exp) 2022 ; 2023 true 2024 ). 2025 2026 2027%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2028active_state(state(active)). 2029is_active(state(active)). 2030set_passive(State) :- 2031 setarg(1,State,passive). 2032 2033%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2034attr_portray_hook(bounds(L,U,_),_) :- 2035 write(L..U). 2036 2037