1% ---------------------------------------------------------------------- 2% BEGIN LICENSE BLOCK 3% Version: CMPL 1.1 4% 5% The contents of this file are subject to the Cisco-style Mozilla Public 6% License Version 1.1 (the "License"); you may not use this file except 7% in compliance with the License. You may obtain a copy of the License 8% at www.eclipse-clp.org/license. 9% 10% Software distributed under the License is distributed on an "AS IS" 11% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied. See 12% the License for the specific language governing rights and limitations 13% under the License. 14% 15% The Original Code is The ECLiPSe Constraint Logic Programming System. 16% The Initial Developer of the Original Code is Cisco Systems, Inc. 17% Portions created by the Initial Developer are 18% Copyright (C) 1989-2006 Cisco Systems, Inc. All Rights Reserved. 19% 20% Contributor(s): ECRC GmbH 21% Contributor(s): IC-Parc, Imperal College London 22% 23% END LICENSE BLOCK 24% 25% System: ECLiPSe Constraint Logic Programming System 26% Version: $Id: fd_arith.pl,v 1.3 2009/07/16 09:11:24 jschimpf Exp $ 27% ---------------------------------------------------------------------- 28 29/* 30 * SEPIA PROLOG SOURCE MODULE 31 */ 32 33/* 34 * FINITE DOMAINS 35 * 36 * IDENTIFICATION: fd_arith.pl 37 * 38 * AUTHOR: Micha Meier 39 * 40 * DESCRIPTION: Arithmetic constraints over linear or polynomial 41 terms and structures. 42 */ 43 44 45:- module(fd_arith). 46 47:- reexport fd_domain. 48 49:- export op(700, xfx, ##). 50:- export op(750, fy, #\+). 51:- export op(760, yfx, #/\). 52:- export op(770, yfx, #\/). 53:- export op(780, yfx, #=>). 54:- export op(790, yfx, #<=>). 55:- export op(800, xfx, isd). 56:- export op(400, yfx, *`). % to print qeqsquarecheck 57 58% Export transformation routines. 59:- export 60 check_dom/1, 61 fd_eq/1, 62 fd_eq/2, 63 fd_ge/1, 64 fd_ge/2, 65 fd_gec/5, 66 fd_gec_ent/6, 67 fd_ineq/1, 68 fd_ineq/2, 69 fd_qeq/3, 70 fd_re/2, 71 fd_eval/1, 72 tr_fd_arith_bool/2, 73 tr_fd_arith_in/2, 74 tr_fd_arith_out/2. 75 76% Output Macros 77 78:- export macro(fd_eq/1, tr_fd_arith_out/2, [write, goal]). 79:- export macro(fd_eq/2, tr_fd_arith_out/2, [write, goal]). 80:- export macro(fd_abs/3, tr_fd_arith_out/2, [write, goal]). 81:- export macro(fd_min/4, tr_fd_arith_out/2, [write, goal]). 82:- export macro(fd_max/4, tr_fd_arith_out/2, [write, goal]). 83:- export macro(fd_ge/1, tr_fd_arith_out/2, [write, goal]). 84:- export macro(fd_ge/2, tr_fd_arith_out/2, [write, goal]). 85:- export macro(fd_gec/5, tr_fd_arith_out/2, [write, goal]). 86:- export macro(fd_gec_ent/6, tr_fd_arith_out/2, [write, goal]). 87:- export macro(fd_ineq/1, tr_fd_arith_out/2, [write, goal]). 88:- export macro(fd_ineq/2, tr_fd_arith_out/2, [write, goal]). 89:- export macro(fd_re/2, tr_fd_arith_out/2, [write, goal]). 90:- export macro(fd_qeq/3, tr_fd_arith_out/2, [write, goal]). 91:- export macro(ge/3, tr_fd_arith_out/2, [write, goal]). 92:- export macro(gec/4, tr_fd_arith_out/2, [write, goal]). 93:- export macro(gec_ent/6, tr_fd_arith_out/2, [write, goal]). 94:- export macro(qeq/3, tr_fd_arith_out/2, [write, goal]). 95:- export macro(qeqsquare/3, tr_fd_arith_out/2, [write, goal]). 96:- export macro(eq_ent/3, tr_fd_arith_out/2, [write, goal]). 97:- export macro(eq/2, tr_fd_arith_out/2, [write, goal]). 98 99 100 101% Goal Macros 102:- inline((#>=)/2, tr_fd_arith_in/2). 103:- inline((#>)/2, tr_fd_arith_in/2). 104:- inline((#<=)/2, tr_fd_arith_in/2). 105:- inline((#=<)/2, tr_fd_arith_in/2). 106:- inline((#<)/2, tr_fd_arith_in/2). 107:- inline((#>=)/3, tr_fd_arith_in/2). 108:- inline((#>)/3, tr_fd_arith_in/2). 109:- inline((#<=)/3, tr_fd_arith_in/2). 110:- inline((#=<)/3, tr_fd_arith_in/2). 111:- inline((#<)/3, tr_fd_arith_in/2). 112:- inline((#=)/2, tr_fd_arith_in/2). 113:- inline((#=)/3, tr_fd_arith_in/2). 114:- inline((#\=)/2, tr_fd_arith_in/2). 115:- inline((#\=)/3, tr_fd_arith_in/2). 116:- inline((##)/2, tr_fd_arith_in/2). 117:- inline((##)/3, tr_fd_arith_in/2). 118:- inline((#/\)/2, tr_fd_arith_in/2). 119:- inline((#\/)/2, tr_fd_arith_in/2). 120:- inline((#\+)/1, tr_fd_arith_in/2). 121:- inline((#=>)/2, tr_fd_arith_in/2). 122:- inline((#<=>)/2, tr_fd_arith_in/2). 123:- inline((#/\)/3, tr_fd_arith_in/2). 124:- inline((#\/)/3, tr_fd_arith_in/2). 125:- inline((#\+)/2, tr_fd_arith_in/2). 126:- inline((#=>)/3, tr_fd_arith_in/2). 127:- inline((#<=>)/3, tr_fd_arith_in/2). 128:- inline(fd_eval/1, tr_fd_arith_in/2). 129:- inline((isd)/2, tr_fd_arith_in/2). 130 131 132:- export 133 % not skipped because might suspend & wake 134 #= /2, 135 #> /2, 136 #< /2, 137 #>= /2, 138 #<= /2, 139 #=< /2, 140 #= /3, 141 #> /3, 142 #< /3, 143 #>= /3, 144 #<= /3, 145 #=< /3, 146 ## /2, 147 ## /3, 148 #/\ /2, 149 #\/ /2, 150 #=> /2, 151 #<=> /2, 152 (#\+) /1, 153 #/\ /3, 154 #\/ /3, 155 #=> /3, 156 #<=> /3, 157 (#\+) /2, 158 #\= /2, 159 #\= /3, 160 (isd)/2, 161 default_domain/1. 162 163:- export 164 term_to_linear/2, 165 linear_term_range/3. 166 167:- import 168 % general-purpose predicates 169 get_bip_error/1, 170 setarg/3, 171 set_bip_error/1, 172 suspensions_to_goals/3, 173 trprotect/2, 174 175 % FD-specific predicates 176 attr_instantiate/2, 177 lt_test/3, 178 make_extreme/2, 179 linear_term_range_eq/6, 180 linear_term_range_ge/6, 181 linear_term_range_only/6, 182 ex_insert_suspension/3, 183 gec_insert_suspension/4, 184 gec_comp/5, 185 gec_start/7, 186 gec_ent_start/7, 187 gec_test/5, 188 ineq_test/4, 189 peval/4, 190 remove_element/3 191 from sepia_kernel. 192 193:- pragma(nodebug). 194:- pragma(system). 195 196 197fderror(N, G) :- 198 error(N, G, _). 199 200% 201% Transformation routines 202% 203 204%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 205% 206% Input goal transformation 207% 208%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 209 210% This should work, but i don't want to risk hitting compiler bugs now... 211%:- local 'C'/3. 212%:- inline('C'/3, tr_c/2). 213%tr_c('C'(S, Token, Rest), S = [Token|Rest]). 214%'C'(S, Token, Rest) :- S = [Token|Rest]. 215 216tr_fd_arith_in(fd_eval(Goal), G) :- 217 -?-> 218 !, 219 Goal = G. 220tr_fd_arith_in(isd(Bool, Expr), G) :- 221 -?-> 222 !, 223 conv_bool_expr(Expr, Bool, compile, List, []), 224 list_goals(List, G). 225tr_fd_arith_in(Pred, Goals) :- 226 conv_pred(Pred, compile, List, []), 227 list_goals(List, Goals). 228 229tr_fd_arith_bool(Var, Val) :- 230 conv_bool_expr(Var, Val, run, Goals, []), 231 call_list(Goals). 232 233:- mode conv_pred(+, ?, +, ?). 234:- mode conv_expr(+, ?, ?, +, ?). 235% 236% transform a predicate into its compiled/executable form 237% 238 % tell arithmetic constraints 239conv_pred(A #= B, Mode) --> 240 {(compound(A) -> true; compound(B)), % don't transform simple args 241 !}, 242 conv_expr(A - B, Expr, Mode), 243 {linearize(Expr, List)}, 244 [fd_arith:fd_eq(List)]. 245conv_pred(A #\= B, Mode) --> 246 conv_ne(A, B, Mode). 247conv_pred(A ## B, Mode) --> 248 (conv_ne(A, B, Mode) -> 249 {true} 250 ; 251 [fd_arith:(A #\= B)] 252 ). 253conv_pred(A #>= B, Mode) --> 254 conv_expr(A - B, Expr, Mode), 255 {linearize(Expr, List)}, 256 conv_ge(List, Mode). 257conv_pred(A #> B, Mode) --> 258 conv_pred(A - 1 #>= B, Mode). 259conv_pred(A #=< B, Mode) --> 260 conv_pred(B #>= A, Mode). 261conv_pred(A #<= B, Mode) --> 262 conv_pred(B #>= A, Mode). 263conv_pred(A #< B, Mode) --> 264 conv_pred(B - 1 #>= A, Mode). 265 % ask arithmetic constraints 266conv_pred(#=(A, B, Bool), Mode) --> 267 {(compound(A) -> true; compound(B)), % don't transform simple args 268 !}, 269 conv_expr(A - B, Expr, Mode), 270 {linearize(Expr, List)}, 271 [fd_arith:fd_eq(List, Bool)]. 272conv_pred(#\=(A, B, Bool), Mode) --> 273 conv_ne(A, B, Bool, Mode). 274conv_pred(##(A, B, Bool), Mode) --> 275 conv_ne(A, B, Bool, Mode). 276conv_pred(#>=(A, B, Bool), Mode) --> 277 conv_expr(A - B, Expr, Mode), 278 {linearize(Expr, List)}, 279 conv_ge(List, Bool, Mode). 280conv_pred(#>(A, B, Bool), Mode) --> 281 conv_pred(#>=(A - 1, B, Bool), Mode). 282conv_pred(#=<(A, B, Bool), Mode) --> 283 conv_pred(#>=(B, A, Bool), Mode). 284conv_pred(#<=(A, B, Bool), Mode) --> 285 conv_pred(#>=(B, A, Bool), Mode). 286conv_pred(#<(A, B, Bool), Mode) --> 287 conv_pred(#>=(B - 1, A, Bool), Mode). 288 % tell boolean constraints 289conv_pred(A #\/ B, Mode) --> 290 conv_bool_expr(A, AC, Mode), 291 conv_bool_expr(B, BC, Mode), 292 conv_sub_pred(AC + BC #>= 1, Mode). 293conv_pred(A #/\ B, Mode) --> 294 conv_sub_pred(A, Mode), % make a normal conjunction out of it 295 conv_sub_pred(B, Mode). 296conv_pred(#\+ A, Mode) --> 297 conv_bool_expr(A, 0, Mode). 298conv_pred(A #=> B, Mode) --> 299 conv_bool_expr(A, AC, Mode), 300 conv_bool_expr(B, BC, Mode), 301 conv_sub_pred(AC #<= BC, Mode). 302conv_pred(A #<=> B, Mode) --> 303 conv_bool_expr(A, AC, Mode), 304 conv_bool_expr(B, AC, Mode). 305 % ask boolean constraints 306conv_pred(#\/(A, B, Bool), Mode) --> 307 conv_bool_expr(A, AC, Mode), 308 conv_bool_expr(B, BC, Mode), 309 conv_sub_pred(#>=(AC + BC, 1, Bool), Mode). 310conv_pred(#/\(A, B, Bool), Mode) --> 311 conv_bool_expr(A, AC, Mode), 312 conv_bool_expr(B, BC, Mode), 313 conv_sub_pred(#=(AC + BC, 2, Bool), Mode). 314conv_pred(#=>(A, B, Bool), Mode) --> 315 conv_bool_expr(A, AC, Mode), 316 conv_bool_expr(B, BC, Mode), 317 conv_sub_pred(#<=(AC, BC, Bool), Mode). 318conv_pred(#<=>(A, B, Bool), Mode) --> 319 conv_bool_expr(A, AC, Mode), 320 conv_bool_expr(B, BC, Mode), 321 {linearize(1*AC+(-1)*BC, List)}, % conv_pred(#=(AC, BC, Bool), Mode). 322 [fd_arith:fd_eq(List, Bool)]. 323conv_pred(#\+(A, Bool), Mode) --> 324 conv_bool_expr(A, AC, Mode), 325 {linearize(1*AC, List)}, % conv_pred(#=(AC, 0, Bool), Mode). 326 [fd_arith:fd_eq(List, Bool)]. 327 328 329% like conv_pred, but don't fail 330 331conv_sub_pred(Goal, Mode) --> 332 conv_pred(Goal, Mode), !. 333conv_sub_pred(Goal, _Mode) --> 334 [Goal]. 335 336% 337% transform a boolean expression into its compiled/executable form 338% 339conv_bool_expr(Var, Val, Mode) --> 340 {var(Var), 341 !}, 342 conv_bool_var(Var, Val, Mode, 1). 343conv_bool_expr(Expr, Bool, Mode) --> 344 {bool_functor(Expr), 345 !, % by default, add one argument and evaluate as 346 Expr =.. [F|Args], % a predicate (similar to is/2) 347 (Mode == run -> 348 Bool :: 0..1 349 ; 350 true 351 ), 352 append(Args, [Bool], NewArgs), 353 BoolExpr =.. [F|NewArgs]}, 354 conv_sub_pred(BoolExpr, Mode). 355conv_bool_expr(Expr, Val, Mode) --> 356 conv_expr(Expr, Val, Mode). 357 358conv_bool_var(Var, Var, run, _) --> 359 {Var :: 0..1}. 360% {fderror(4, bool_expr(Var))}. 361conv_bool_var(Var, Val, compile, _) --> 362 [fd_arith:tr_fd_arith_bool(Var, Val)]. 363 364% 365% transform an arithmetic expression into its compiled/executable form 366% conv_expr(+Expr, -LinExpr, +RunCompile) 367conv_expr(Expr, Val, Mode) --> 368 conv_expr(Expr, Val, Mode, 1). 369 370conv_expr(Var, Val, Mode, K) --> 371 {var(Var), 372 !}, 373 conv_expr_var(Var, Val, Mode, K). 374conv_expr(A + B, AC + BC, Mode, K) --> 375 !, 376 conv_expr(A, AC, Mode, K), 377 conv_expr(B, BC, Mode, K). 378conv_expr(A - B, AC + BC, Mode, K) --> 379 !, 380 conv_expr(A, AC, Mode, K), 381 {K1 is -K}, 382 conv_expr(B, BC, Mode, K1). 383conv_expr(-A, AC, Mode, K) --> 384 !, 385 {K1 is -K}, 386 conv_expr(A, AC, Mode, K1). 387conv_expr(A * B, Val, Mode, K) --> 388 !, 389 conv_mult(A, B, Val, Mode, K). 390conv_expr(A / B, K*X, Mode, K) --> 391 !, 392 conv_sub_pred(X * B #= A, Mode). 393conv_expr(abs(A), K*B, Mode, K) --> 394 !, 395 conv_sub_expr(A, AC, Mode), 396 [fd_arith:fd_abs(AC, B)]. 397conv_expr(min(A,B), K*C, Mode, K) --> 398 !, 399 conv_sub_expr(A, AC, Mode), 400 conv_sub_expr(B, BC, Mode), 401 conv_sub_expr(C, CC, Mode), 402 [fd_arith:fd_min(AC, BC, CC, _Susp)]. 403conv_expr(max(A,B), K*C, Mode, K) --> 404 !, 405 conv_sub_expr(A, AC, Mode), 406 conv_sub_expr(B, BC, Mode), 407 conv_sub_expr(C, CC, Mode), 408 [fd_arith:fd_max(AC, BC, CC, _Susp)]. 409conv_expr(sum(List), Val, Mode, K) --> 410 !, 411 conv_sum(List, Val, Mode, K). 412conv_expr(Expr, Val, Mode, K) --> 413 {compound(Expr), arith_functor(Expr)}, !, 414 conv_arith(Expr, Elem, Mode), 415 conv_expr(Elem, Val, Mode, K). 416conv_expr(N, Val, _, K) --> 417 {integer(N), 418 Val is N * K}. 419 420 conv_arith(Expr, Val, run) --> 421 { Val is Expr }. 422 conv_arith(Expr, Val, compile) --> 423 peval(Val, Expr). 424 425conv_sub_expr(Var, Var, Mode) --> 426 {var(Var)}, !, 427 ( {Mode == run} -> 428 {check_dom(Var)} 429 ; 430 [fd_arith:check_dom(Var)] 431 ). 432conv_sub_expr(Expr, Result, Mode) --> 433 conv_pred(Result #= Expr, Mode). 434 435conv_mult(A, B, K*Val, Mode, K) --> 436 {var(A), 437 var(B), 438 !, 439 Mode == run}, % it might not be a good idea to expand * 440 register_var(A, Mode), % as qeq, because one might become an integer 441 register_var(B, Mode), 442 [fd_arith:fd_qeq(A, B, Val)]. 443conv_mult(A, B*C, Val, Mode, K) --> 444 -?-> 445 {integer(B)}, 446 !, 447 ({B = 0} -> 448 {Val = 0} 449 ; 450 {K1 is B * K}, 451 conv_mult(A, C, Val, Mode, K1) 452 ). 453conv_mult(A, B+C, Val, Mode, K) --> 454 -?-> 455 !, 456 {Val = E1 + E2}, 457 conv_mult(A, B, E1, Mode, K), 458 conv_mult(A, C, E2, Mode, K). 459conv_mult(A, B-C, Val, Mode, K) --> 460 -?-> 461 !, 462 {Val = E1 + E2}, 463 conv_mult(A, B, E1, Mode, K), 464 {K1 is -K}, 465 conv_mult(A, C, E2, Mode, K1). 466conv_mult(A, B, Val, Mode, K) --> 467 {integer(B)}, 468 !, 469 ({B = 0} -> 470 {Val = 0} 471 ; 472 {K1 is B * K}, 473 conv_expr(A, Val, Mode, K1) 474 ). 475conv_mult([A|As], [B|Bs], Val, Mode, K) --> 476 -?-> 477 !, 478 {make_prod_sum(As, Bs, ABs)}, 479 conv_sum([A*B|ABs], Val, Mode, K). 480conv_mult(A, B, Val, Mode, K) --> 481 {compound(B)}, 482 !, 483 conv_expr(B, E1, Mode, 1), 484 conv_mult(A, E1, Val, Mode, K). 485conv_mult(_A, B, _Val, _Mode, _K) --> 486 {atomic(B), 487 !, 488 error(5, fd_arith(B)), 489 fail}. 490conv_mult(A, B, Val, Mode, K) --> 491 conv_mult(B, A, Val, Mode, K). 492 493conv_sum([], Sum, _Mode, _K) --> -?-> !, { Sum=0 }. 494conv_sum([A|As], Sum, Mode, K) --> 495 -?-> 496 { Sum = AC+AsC }, 497 conv_expr(A, AC, Mode, K), 498 conv_sum(As, AsC, Mode, K). 499conv_sum(subscript(Array,Index), Sum, Mode, K) --> 500 -?-> 501 { Mode==run, subscript(Array,Index,Elem) }, 502 ( { number(Elem) } -> conv_expr(Elem, Sum, Mode, K) 503 ; { var(Elem) } -> conv_expr(Elem, Sum, Mode, K) 504 ; conv_sum(Elem, Sum, Mode, K) 505 ). 506 507make_prod_sum([], [], Sum) :- -?-> Sum=[]. 508make_prod_sum([X|Xs], [Y|Ys], Sum) :- -?-> 509 Sum = [X*Y|XYs], 510 make_prod_sum(Xs, Ys, XYs). 511 512 513conv_expr_var(Var{fd:(fd with [])}, Val, _, K) --> 514 -?-> 515 !, 516 {Val = K*Var}. 517conv_expr_var(Var, K*Var, compile, K) --> 518 !. 519conv_expr_var(Var, K*Var, _, K) --> 520 {default_domain(Var)}. 521 522register_var(Var, Mode) --> 523 conv_expr_var(Var, _, Mode, 1). 524 525list_goals([], true). 526list_goals([G|L], Goals) :- 527 list_goals(G, L, Goals). 528 529list_goals(G, [], G). 530list_goals(G, [Next|L], (G, Goals)) :- 531 list_goals(Next, L, Goals). 532 533% 534% Convert a linear expression to a list 535% 536linearize(Expr, [C|L2]) :- 537 linearize(Expr, L, [], 0, C), 538 sort(2, =<, L, L1), 539 var_sort(L1, L2). 540 541linearize(A + B, L, LC, C0, C1) :- 542 !, 543 linearize(A, L, L1, C0, C2), 544 linearize(B, L1, LC, C2, C1). 545linearize(C, L, L, C0, C1) :- 546 integer(C), 547 !, 548 C1 is C + C0. 549linearize(Prod, [Prod|LC], LC, C, C). 550 551 552var_sort([], []). 553var_sort([K*V|T], LT) :- 554 var_sort(K, V, T, LT). 555 556var_sort(K, V, [], L) :- 557 (K = 0 -> 558 L = [] 559 ; 560 L = [K*V] 561 ). 562var_sort(K, V, [M*V1|T], LT) :- 563 (V == V1 -> 564 K1 is K + M, 565 var_sort(K1, V, T, LT) 566 ; 567 (K \== 0 -> 568 LT = [K*V|LT1], 569 var_sort(M, V1, T, LT1) 570 ; 571 var_sort(M, V1, T, LT) 572 ) 573 ). 574 575unlinearize([K], K) :- !. 576unlinearize([H|L], H+T) :- 577 unlinearize(L, T). 578 579:- mode conv_ge(+, ?, ?, ?). 580conv_ge([C], _) --> 581 !, 582 ({C >= 0} -> {true}; [fail]). 583conv_ge([C, K*X], _) --> 584 !, 585 [fd_arith:fd_gec(0, K, X, C, 0)]. 586conv_ge([C, 1*X, K*Y], _) --> 587 !, 588 [fd_arith:fd_gec(X, K, Y, C, 0)]. 589conv_ge([C, K*X, 1*Y], _) --> 590 !, 591 [fd_arith:fd_gec(Y, K, X, C, 0)]. 592conv_ge([0|L], _) --> 593 {L = [_, _, _], 594 find_coefs(L, Goal)}, 595 !, 596 [Goal]. 597conv_ge(List, _) --> 598 [fd_arith:fd_ge(List)]. 599 600find_coefs([-1*Y, 1*X, 1*C], fd_arith:fd_gec(X, -1, Y, C, 0)) :- !. 601find_coefs([1*C, -1*Y, 1*X], fd_arith:fd_gec(X, -1, Y, C, 0)) :- !. 602find_coefs([1*X, 1*C, -1*Y], fd_arith:fd_gec(X, -1, Y, C, 0)) :- !. 603find_coefs([-1*Y, -1*D, 1*X], fd_arith:fd_gec(X, -1, Y, 0, D)) :- !. 604find_coefs([1*X, -1*Y, -1*D], fd_arith:fd_gec(X, -1, Y, 0, D)) :- !. 605find_coefs([-1*D, 1*X, -1*Y], fd_arith:fd_gec(X, -1, Y, 0, D)) :- !. 606 607:- mode conv_ge(+, -, ?, ?, ?). 608conv_ge([C], Bool, _) --> 609 !, 610 ({C >= 0} -> [Bool = 1]; [Bool = 0]). 611conv_ge([C, K*X], Bool, _) --> 612 !, 613 [fd_arith:fd_gec_ent(0, K, X, C, 0, Bool)]. 614conv_ge([C, 1*X, K*Y], Bool, _) --> 615 !, 616 [fd_arith:fd_gec_ent(X, K, Y, C, 0, Bool)]. 617conv_ge([C, K*X, 1*Y], Bool, _) --> 618 !, 619 [fd_arith:fd_gec_ent(Y, K, X, C, 0, Bool)]. 620conv_ge([0|L], Bool, _) --> 621 {L = [_, _, _], 622 find_coefs(L, Bool, Goal)}, 623 !, 624 [Goal]. 625conv_ge(List, Bool, _) --> 626 [fd_arith:fd_ge(List, Bool)]. 627 628find_coefs([-1*Y, 1*X, 1*C], Bool, fd_arith:fd_gec_ent(X, -1, Y, C, 0, Bool)) :- !. 629find_coefs([1*C, -1*Y, 1*X], Bool, fd_arith:fd_gec_ent(X, -1, Y, C, 0, Bool)) :- !. 630find_coefs([1*X, 1*C, -1*Y], Bool, fd_arith:fd_gec_ent(X, -1, Y, C, 0, Bool)) :- !. 631find_coefs([-1*Y, -1*D, 1*X], Bool, fd_arith:fd_gec_ent(X, -1, Y, 0, D, Bool)) :- !. 632find_coefs([1*X, -1*Y, -1*D], Bool, fd_arith:fd_gec_ent(X, -1, Y, 0, D, Bool)) :- !. 633find_coefs([-1*D, 1*X, -1*Y], Bool, fd_arith:fd_gec_ent(X, -1, Y, 0, D, Bool)) :- !. 634 635conv_ne(A, B, _) --> 636 {var(A), 637 nonvar(B), 638 is_element(B)}, 639 !, 640 [fd_arith:fd_re(A, B)]. 641conv_ne(A, B, _) --> 642 {nonvar(A), 643 is_element(A), 644 var(B)}, 645 !, 646 [fd_arith:fd_re(B, A)]. 647conv_ne(A, B, Mode) --> 648 {(compound(A) -> true; compound(B))}, 649 conv_expr(A - B, Expr, Mode), 650 {linearize(Expr, List)}, 651 [fd_arith:fd_ineq(List)]. 652 653conv_ne(A, B, Bool, Mode) --> 654 {(compound(A) -> true; compound(B))}, 655 conv_expr(A - B, Expr, Mode), 656 {linearize(Expr, List)}, 657 [fd_arith:fd_ineq(List, Bool)]. 658 659is_element(Var) :- 660 var(Var). 661is_element(A) :- 662 atomic(A). 663is_element(C) :- 664 compound(C), 665 ground(C), 666 not arith_functor(C). 667 668arith_functor(+_). 669arith_functor(-_). 670arith_functor(_+_). 671arith_functor(_-_). 672arith_functor(_*_). 673arith_functor(_/_). 674arith_functor(sum(_)). 675arith_functor(subscript(_,_)). 676 677bool_functor(_::_). 678bool_functor(_#=_). 679bool_functor(_#<=_). 680bool_functor(_#=<_). 681bool_functor(_#>=_). 682bool_functor(_#<_). 683bool_functor(_#>_). 684bool_functor(_##_). 685bool_functor(_#\=_). 686bool_functor(#\+_). 687bool_functor(_#/\_). 688bool_functor(_#\/_). 689bool_functor(_#=>_). 690bool_functor(_#<=>_). 691 692%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 693% 694% Output goal transformation 695% 696%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 697 698:- mode tr_fd_arith_out(+, -). 699tr_fd_arith_out(In, Out) :- 700 arg(1, In, Arg), 701 ( Arg == ... -> 702 tr_fd_arith_out_dummy(In, Out) % debugger dummy goal with ... args 703 ; 704 tr_fd_arith_out_(In, Out) 705 ). 706 707:- mode tr_fd_arith_out_(+, -). 708tr_fd_arith_out_(fd_eq(List), Expr #= 0) :- 709 !, 710 list_to_expr(List, Expr). 711tr_fd_arith_out_(fd_eq(List, B), #=(Expr, 0, B)) :- 712 !, 713 list_to_expr(List, Expr). 714tr_fd_arith_out_(fd_ge(List), Expr #>= 0) :- 715 !, 716 list_to_expr(List, Expr). 717tr_fd_arith_out_(fd_ge(List, B), #>=(Expr, 0, B)) :- 718 !, 719 list_to_expr(List, Expr). 720tr_fd_arith_out_(fd_gec(X, K, Y, C, D), Expr #>= D) :- 721 !, 722 next_elem(K*Y, X, Expr1), 723 (C == 0 -> Expr = Expr1; Expr = Expr1 + C). 724tr_fd_arith_out_(fd_gec_ent(X, K, Y, C, D, Bo), #>=(Expr + C, D, Bo)) :- 725 !, 726 next_elem(K*Y, X, Expr). 727tr_fd_arith_out_(fd_ineq(List), Expr #\= 0) :- 728 !, 729 list_to_expr(List, Expr). 730tr_fd_arith_out_(fd_ineq(List, B), #\=(Expr, 0, B)) :- 731 !, 732 list_to_expr(List, Expr). 733tr_fd_arith_out_(fd_re(X, Y), X #\= Y) :- 734 !. 735tr_fd_arith_out_(fd_qeq(X, Y, Z), X * Y #= Z) :- 736 !. 737tr_fd_arith_out_(ge(List, B, _), #>=(Expr, 0, B)) :- 738 !, 739 list_to_expr(List, Expr). 740tr_fd_arith_out_(gec(X, K, Y, C), Expr #>= NC) :- 741 !, 742 next_elem(K*Y, X, Expr), 743 NC is -C. 744tr_fd_arith_out_(gec_ent(X, K, Y, C, B, _), #>=(E, N, B)) :- 745 !, 746 tr_fd_arith_out_(gec(X, K, Y, C), G), 747 G = (E #>= N). 748tr_fd_arith_out_(qeq(X, Y, Z), X * Y #= Z) :- 749 !. 750tr_fd_arith_out_(qeqsquare(X, Y,_Susp), X^2 #= Y) :- 751 !. 752tr_fd_arith_out_(eq_ent(X, Y, B), #=(X, Y, B)) :- 753 !. 754tr_fd_arith_out_(eq(List, B), #=(Expr, 0, B)) :- 755 !, 756 list_to_expr(List, Expr). 757tr_fd_arith_out_(fd_abs(A, B, _Susp), B#=abs(A)) :- !. 758tr_fd_arith_out_(fd_min(A, B, C, _Susp), C#=min(A,B)) :- !. 759tr_fd_arith_out_(fd_max(A, B, C, _Susp), C#=max(A,B)) :- !. 760 761:- mode tr_fd_arith_out_dummy(+, -). 762tr_fd_arith_out_dummy(fd_eq(_List), ... #= 0). 763tr_fd_arith_out_dummy(fd_eq(_List, _B), #=(..., 0, ...)). 764tr_fd_arith_out_dummy(fd_ge(_List), ... #>= 0). 765tr_fd_arith_out_dummy(fd_ge(_List, _B), #>=(..., 0, ...)). 766tr_fd_arith_out_dummy(fd_gec(_X, _K, _Y, _C, _D), ... #>= ...). 767tr_fd_arith_out_dummy(fd_gec_ent(_X, _K, _Y, _C, _D, _Bo), #>=(... + ..., ..., ...)). 768tr_fd_arith_out_dummy(fd_ineq(_List), ... #\= 0). 769tr_fd_arith_out_dummy(fd_ineq(_List, _B), #\=(..., 0, ...)). 770tr_fd_arith_out_dummy(fd_re(_X, _Y), ... #\= ...). 771tr_fd_arith_out_dummy(fd_qeq(_X, _Y, _Z), ... * ... #= ...). 772tr_fd_arith_out_dummy(ge(_List, _B, _), #>=(..., 0, ...)). 773tr_fd_arith_out_dummy(gec(_X, _K, _Y, _C), ... #>= ...). 774tr_fd_arith_out_dummy(gec_ent(_X, _K, _Y, _C, _B, _), #>=(..., ..., ...)). 775tr_fd_arith_out_dummy(qeq(_X, _Y, _Z), ... * ... #= ...). 776tr_fd_arith_out_dummy(qeqsquare(_X, _Y,_Susp), ... ^2 #= ...). 777tr_fd_arith_out_dummy(eq_ent(_X, _Y, _B), #=(..., ..., ...)). 778tr_fd_arith_out_dummy(eq(_List, _B), #=(..., 0, ...)). 779tr_fd_arith_out_dummy(fd_abs(_A,_B,_), ... #= abs(...)). 780tr_fd_arith_out_dummy(fd_min(_A,_B,_C,_), ... #= min(...,...)). 781tr_fd_arith_out_dummy(fd_max(_A,_B,_C,_), ... #= max(...,...)). 782 783list_to_expr([F], Expr) :- 784 !, 785 first_elem(F, Expr). 786list_to_expr([F|T], Expr) :- 787 first_elem(F, E0), 788 next_to_expr(T, E0, Expr). 789 790next_to_expr([H], E0, Expr) :- 791 !, 792 next_elem(H, E0, Expr). 793next_to_expr([H|T], E0, Expr) :- 794 next_elem(H, E0, E1), 795 next_to_expr(T, E1, Expr). 796 797:- mode first_elem(?, -). 798first_elem(1*X, Y) :- -?-> !, Y = X. 799first_elem(-1*X, Y) :- -?-> !, Y = -X. 800first_elem(V, V). 801 802:- mode next_elem(+, ?, -). 803next_elem(1*X, Prev, Prev + X) :- !. 804next_elem(-1*X, Prev, Prev - X) :- !. 805next_elem(K*X, Prev, Prev + K*X) :- 806 K > 0, 807 !. 808next_elem(K*X, Prev, Prev - K1*X) :- 809 K < 0, 810 !, 811 K1 is -K. 812next_elem(K, Prev, G) :- 813 nonvar(K), 814 !, 815 (K > 0 -> 816 G = Prev + K 817 ; 818 K1 is -K, 819 G = Prev - K1 820 ). 821next_elem(V, Prev, Prev + V). 822 823 824call_list([]). 825call_list([Goal|List]) :- 826 call(Goal), 827 call_list(List). 828 829%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 830% 831% Auxiliary Visible Predicates 832% 833%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 834 835linear_term_range(Term, Min, Max) :- 836 linear_term_range_only(Term, Res, TMin, TMax, _, _), 837 Res = 5, 838 TMin = Min, 839 TMax = Max. 840 841term_to_linear(Term, List) :- 842 conv_expr(Term, Val, linear, _, _), 843 linearize(Val, List). 844 845%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 846% 847% Arithmetic Constraints 848% 849%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 850 851A #= B :- 852 is_element(A), 853 !, 854 eq_en(A, B). 855A #= B :- 856 conv_pred(A #= B, run, List, []), 857 !, 858 call_list(List). 859A #= B :- 860 arith_functor(A), 861 !, 862 fderror(5, A #= B). 863A #= B :- 864 arith_functor(B), 865 !, 866 fderror(5, A #= B). 867A #= B :- 868 fderror(4, A #= B). 869 870eq_en(A, B) :- 871 is_element(B), 872 !, 873 A = B. 874eq_en(A, B) :- 875 conv_pred(A #= B, run, List, []), 876 !, 877 call_list(List). 878eq_en(A, B) :- 879 arith_functor(B), 880 !, 881 fderror(5, A #= B). 882eq_en(A, B) :- 883 fderror(4, A #= B). 884 885A ## B :- 886 A #\= B. 887 888A #\= B :- 889 var(A), 890 !, 891 ne_vn(A, B). 892A #\= B :- 893 atomic(A), 894 !, 895 ne_en(A, B). 896A #\= B :- 897 compound(A), 898 ground(A), 899 not arith_functor(A), 900 !, 901 ne_en(A, B). 902A #\= B :- 903 conv_pred(A #\= B, run, List, []), 904 !, 905 A \== B, 906 call_list(List). 907A #\= B :- 908 arith_functor(A), 909 !, 910 fderror(5, A #\= B). 911A #\= B :- 912 arith_functor(B), 913 !, 914 fderror(5, A #\= B). 915A #\= B :- 916 fderror(4, A #\= B). 917 918ne_vn(A, B) :- 919 var(B), 920 !, 921 A \== B, 922 make_suspension(A #\= B, 2, Susp), 923 insert_suspension([A|B], Susp, inst of suspend, suspend). 924ne_vn(A, B) :- 925 atomic(B), 926 !, 927 fd_re(A, B). 928ne_vn(A, B) :- 929 compound(B), 930 ground(B), 931 not arith_functor(B), 932 !, 933 fd_re(A, B). 934ne_vn(A, B) :- 935 conv_pred(A #\= B, run, List, []), 936 !, 937 A \== B, 938 call_list(List). 939ne_vn(A, B) :- 940 arith_functor(B), 941 !, 942 fderror(5, A #\= B). 943ne_vn(A, B) :- 944 fderror(4, A #\= B). 945 946ne_en(A, B) :- 947 var(B), 948 !, 949 fd_re(B, A). 950ne_en(A, B) :- 951 atomic(B), 952 !, 953 A \== B. 954ne_en(A, B) :- 955 compound(B), 956 ground(B), 957 not arith_functor(B), 958 !, 959 A \== B. 960ne_en(A, B) :- 961 conv_pred(A #\= B, run, List, []), 962 !, 963 A \== B, 964 call_list(List). 965ne_en(A, B) :- 966 arith_functor(B), 967 !, 968 fderror(5, A #\= B). 969ne_en(A, B) :- 970 fderror(4, A #\= B). 971 972A #>= B :- 973 conv_pred(A #>= B, run, List, []), 974 call_list(List). 975 976A #> B :- 977 conv_pred(A #> B, run, List, []), 978 call_list(List). 979 980A #< B :- 981 conv_pred(A #< B, run, List, []), 982 call_list(List). 983 984A #=< B :- 985 conv_pred(B #>= A, run, List, []), 986 call_list(List). 987 988A #<= B :- 989 conv_pred(B #>= A, run, List, []), 990 call_list(List). 991 992%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 993% 994% Entailment Arithmetic Constraints 995% 996%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 997 998#=(A, B, Bool) :- 999 is_element(A), 1000 !, 1001 eq_en(A, B, Bool). 1002#=(A, B, Bool) :- 1003 conv_pred(#=(A, B, Bool), run, List, []), 1004 !, 1005 call_list(List). 1006#=(A, B, Bool) :- 1007 arith_functor(A), 1008 !, 1009 fderror(5, #=(A, B, Bool)). 1010#=(A, B, Bool) :- 1011 arith_functor(B), 1012 !, 1013 fderror(5, #=(A, B, Bool)). 1014#=(A, B, Bool) :- 1015 fderror(4, #=(A, B, Bool)). 1016 1017eq_en(A, B, Bool) :- 1018 is_element(B), 1019 !, 1020 fd_eqe(A, B, Bool). 1021eq_en(A, B, Bool) :- 1022 conv_pred(#=(A, B, Bool), run, List, []), 1023 !, 1024 call_list(List). 1025eq_en(A, B, Bool) :- 1026 arith_functor(B), 1027 !, 1028 fderror(5, #=(A, B, Bool)). 1029eq_en(A, B, Bool) :- 1030 fderror(4, #=(A, B, Bool)). 1031 1032##(A, B, Bool) :- 1033 #\=(A, B, Bool). 1034 1035#\=(A, B, Bool) :- 1036 Bool :: 0..1, 1037 BoolN #= 1 - Bool, 1038 #=(A, B, BoolN). 1039 1040#>=(A, B, Bool) :- 1041 #>=(A, B, Bool). 1042 1043#>(A, B, Bool) :- 1044 #>(A, B, Bool). 1045 1046#=<(A, B, Bool) :- 1047 #=<(A, B, Bool). 1048 1049#<=(A, B, Bool) :- 1050 #<=(A, B, Bool). 1051 1052#<(A, B, Bool) :- 1053 #<(A, B, Bool). 1054 1055%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1056% 1057% Boolean Constraints 1058% 1059%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1060 1061A #/\ B :- 1062 conv_pred(A #/\ B, run, List, []), 1063 call_list(List). 1064 1065A #\/ B :- 1066 A #\/ B. 1067 1068A #=> B :- 1069 A #=> B. 1070 1071A #<=> B :- 1072 A #<=> B. 1073 1074#\+ A :- 1075 #\+ A. 1076 1077%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1078% 1079% Boolean Entailment Constraints 1080% 1081%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1082 1083#/\(A, B, Bool) :- 1084 #/\(A, B, Bool). 1085 1086#\/(A, B, Bool) :- 1087 #\/(A, B, Bool). 1088 1089#=>(A, B, Bool) :- 1090 #=>(A, B, Bool). 1091 1092#<=>(A, B, Bool) :- 1093 #<=>(A, B, Bool). 1094 1095#\+(A, Bool) :- 1096 #\+(A, Bool). 1097 1098%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1099% 1100% Low Level Implementation of Arithmetic Constraints 1101% 1102%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1103 1104fd_eval(Goal) :- 1105 call(Goal). 1106 1107isd(Bool, Expr) :- 1108 conv_bool_expr(Expr, Bool, run, List, []), 1109 call_list(List). 1110 1111% 1112% equality 1113% 1114fd_eq(Term) :- 1115 linear_term_range_eq(Term, Res, Min, Max, NewTerm, _), 1116 handle_eq(NewTerm, Res, Min, Max). 1117 1118:- mode handle_eq(+, ++, ++, ++). 1119handle_eq(Term, 0, _, _) :- % take maximum 1120 make_extreme(Term, max). 1121handle_eq(_, 1, _, _). % solved 1122handle_eq(Term, 2, _, _) :- 1123 make_extreme(Term, min). 1124handle_eq(_, 3, _, _) :- 1125 fail. 1126handle_eq(Term, 4, Min, Max) :- % only one variable left 1127 lt_maxmin(Term, Min, Max), 1128 fd_eq(Term), 1129 wake. 1130handle_eq(Term, 5, _, _) :- % no updates 1131 make_suspension(fd_eq(Term), 3, Susp), 1132 ex_insert_suspension(Term, Susp, 1). 1133handle_eq(Term, 6, _, _) :- % type error 1134 tr_fd_arith_out_(fd_eq(Term), G), 1135 fderror(5, G). 1136handle_eq(Term, 7, Min, Max) :- % update 1137 lt_maxmin(Term, Min, Max), 1138 wake, 1139 fd_eq(Term). 1140handle_eq(Term, 8, Min, Max) :- % update 1141 lt_maxmin(Term, Min, Max), 1142 wake, 1143 fd_eq(Term). 1144handle_eq(Term, 9, _, _) :- % not linearized 1145 unlinearize(Term, T), 1146 T #= 0. 1147handle_eq(_, 10, X, X). % X #= Y 1148 1149lt_maxmin([], _, _). 1150lt_maxmin([H|T], Min, Max) :- 1151 lt_test(H, Min, Max), 1152 lt_maxmin(T, Min, Max). 1153 1154% 1155% inequality 1156% 1157fd_ge(Term) :- 1158 linear_term_range_ge(Term, Res, K, Max, NewTerm, Offset), 1159 handle_ge(NewTerm, Res, Max, Offset, K). 1160 1161:- mode handle_ge(+, ++, ++, ++, ++). 1162handle_ge(Term, 0, _, _, _) :- % take maximum 1163 make_extreme(Term, max). 1164handle_ge(_, 1, _, _, _). % solved 1165handle_ge(_, 2, _, _, _). % solved 1166handle_ge(_, 3, _, _, _). % solved 1167handle_ge(Term, 4, Max, _, _) :- % only one variable left 1168 lt_min(Term, Max), 1169 wake. 1170handle_ge(Term, 5, _, _, _) :- % no updates 1171 make_suspension(fd_ge(Term), 3, Susp), 1172 ex_insert_suspension(Term, Susp, 0). 1173handle_ge(Term, 6, _, _, _) :- % type error 1174 tr_fd_arith_out_(fd_ge(Term), G), 1175 fderror(5, G). 1176handle_ge(Term, 7, _, _, _) :- % no updates 1177 make_suspension(fd_ge(Term), 3, Susp), 1178 ex_insert_suspension(Term, Susp, 0). 1179handle_ge(Term, 8, Max, _, _) :- % update 1180 lt_min(Term, Max), 1181 fd_ge(Term). 1182handle_ge(Term, 9, _, _, _) :- % not linearized 1183 unlinearize(Term, T), 1184 fd_eval(T #>= 0). 1185handle_ge(X, 10, Y, C, K) :- % simple relation 1186 gec(X, K, Y, C). 1187 1188lt_min([], _). 1189lt_min([H|T], Max) :- 1190 lt_test(H, Max, Max), 1191 lt_min(T, Max). 1192 1193/* X + K*Y + C >= D */ 1194fd_gec(X, K, Y, C, D) :- 1195 gec_start(X, K, Y, C, D, E, Res), 1196 gec_res(X, K, Y, E, Res). 1197 1198gec(X, K, Y, C) :- 1199 gec_comp(X, K, Y, C, Res), 1200 gec_res(X, K, Y, C, Res). 1201 1202:- mode gec_res(?, ++, ?, ++, ++). 1203gec_res(X, K, Y, C, 0) :- % no change 1204 gec_delay(X, K, Y, C). 1205gec_res(X, K, Y, C, 1) :- % change 1206 gec_delay(X, K, Y, C), 1207 wake. 1208gec_res(_, _, _, _, 2) :- % solved with modifs 1209 wake. 1210gec_res(_, _, _, _, 5). % solved 1211gec_res(X, K, Y, C, 6) :- % not simplified 1212 (var(X), var(Y), var(C) -> % otherwise it would loop 1213 fd_ge([1*X, K*Y, 1*C]) 1214 ; 1215 conv_pred(X+K*Y+C #>= 0, run, List, []) -> 1216 call_list(List) 1217 ; 1218 tr_fd_arith_out_(gec(X, K, Y, C), G), 1219 fderror(5, G) 1220 ). 1221gec_res(X, K, Y, C, 7) :- % not simplified 1222 (var(X), var(Y), var(C) -> 1223 fd_ge([1*X, K*Y, -1*C]) 1224 ; 1225 conv_pred(X+K*Y-C #>= 0, run, List, []) -> 1226 call_list(List) 1227 ; 1228 tr_fd_arith_out_(gec(X, K, Y, -C), G), 1229 fderror(5, G) 1230 ). 1231 1232gec_delay(X, K, Y, C) :- 1233 make_suspension(gec(X, K, Y, C), 2, Susp), 1234 gec_insert_suspension(X, K, Y, Susp). 1235 1236 1237fd_re(Var{fd:(fd with [])}, Value) :- 1238 -?-> 1239 !, 1240 remove_element(Var, Value, Res), 1241 del_res(Var, Value, Res). 1242fd_re(Var, Value) :- 1243 var(Var), 1244 !, 1245 make_suspension(Var #\= Value, 3, Susp), 1246 insert_suspension(Var, Susp, constrained of suspend, suspend). 1247fd_re(A, B) :- % may be when expanded 1248 fd_eval(A #\= B). 1249 1250:- mode del_res(?, ?, ++). 1251del_res(_, _, 2) :- % update 1252 wake. 1253del_res(_, _, 5). % not in the domain or inst 1254del_res(A, B, 6) :- 1255 fderror(5, A #\= B). 1256 1257 1258% The real inequality predicate. It is woken when there is at most 1259% one variable in its arguments. 1260fd_ineq(L) :- 1261 ineq_test(L, Res, Var, Val), 1262 ineq_res(L, Res, Var, Val). 1263 1264:- mode ineq_res(+, ++, ?, ++). 1265ineq_res(L, 0, Var1, Var2) :- % redelay 1266 make_suspension(fd_ineq(L), 2, Susp), 1267 insert_suspension([Var1|Var2], Susp, inst of suspend, suspend). 1268ineq_res(_, 2, _, _) :- % update 1269 wake. 1270ineq_res(_, 5, _, _). % not in the domain or inst 1271ineq_res(L, 6, _, _) :- % bound later 1272 tr_fd_arith_out_(ineq(L), G), 1273 fderror(5, G). 1274ineq_res(L, 9, _, _) :- % not linearized 1275 unlinearize(L, Expr), 1276 fd_eval(Expr #\= 0). 1277 1278%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1279% 1280% Low Level Implementation of Entailment Arithmetic Constraints 1281% 1282%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1283 1284% 1285% entailment of #= 1286% 1287% variables and simple elements 1288fd_eqe(A{fd:(fd with domain:dom([0, 1], 2))}, B, 1) :- 1289 -?-> 1290 !, 1291 A = B. 1292fd_eqe(A, B, Bool) :- 1293 Bool :: 0..1, 1294 eq_ent(A, B, Bool). 1295 1296eq_ent(A, B, 0) :- 1297 -?-> 1298 !, 1299 A #\= B. 1300eq_ent(A, B, 1) :- 1301 -?-> 1302 !, 1303 A #= B. 1304eq_ent(A, B, Bool) :- 1305 (A == B -> 1306 Bool = 1 1307 ; 1308 eq_ent_test(A, B, Bool) 1309 ). 1310 1311eq_ent_test(A{fd:(fd with domain:D)}, B, Bool) :- 1312 -?-> 1313 !, 1314 eq_ent_dom(A, B, Bool, D). 1315eq_ent_test(A, B, Bool) :- 1316 var(A), 1317 !, 1318 make_suspension(eq_ent(A, B, Bool), 3, Susp), 1319 insert_suspension(A, Susp, constrained of suspend, suspend). 1320eq_ent_test(A, B, Bool) :- 1321 eq_ent_el(A, B, Bool). 1322 1323eq_ent_dom(A, B{fd:(fd with domain:DB)}, Bool, DA) :- 1324 -?-> 1325 !, 1326 (dom_intersection(DA, DB, _, _) -> 1327 make_suspension(eq_ent(A, B, Bool), 3, Susp), 1328 insert_suspension([A,B|Bool], Susp, any of fd, fd), 1329 insert_suspension([A|B], Susp, bound of suspend, suspend) 1330 ; 1331 Bool = 0 1332 ). 1333eq_ent_dom(A, B, Bool, _) :- 1334 var(B), 1335 !, 1336 make_suspension(eq_ent(A, B, Bool), 3, Susp), 1337 insert_suspension([A|B], Susp, constrained of suspend, suspend). 1338eq_ent_dom(A, B, Bool, DA) :- 1339 (dom_check_in(B, DA) -> 1340 make_suspension(eq_ent(A, B, Bool), 3, Susp), 1341 insert_suspension([A|Bool], Susp, any of fd, fd) 1342 ; 1343 Bool = 0 1344 ). 1345 1346eq_ent_el(A, B{fd:(fd with domain:DB)}, Bool) :- 1347 -?-> 1348 !, 1349 (dom_check_in(A, DB) -> 1350 make_suspension(eq_ent(A, B, Bool), 3, Susp), 1351 insert_suspension([B|Bool], Susp, any of fd, fd) 1352 ; 1353 Bool = 0 1354 ). 1355eq_ent_el(A, B, Bool) :- 1356 var(B), 1357 !, 1358 make_suspension(eq_ent(A, B, Bool), 3, Susp), 1359 insert_suspension(B, Susp, constrained of suspend, suspend). 1360eq_ent_el(A, B, Bool) :- 1361 (A == B -> 1362 Bool = 1 1363 ; 1364 Bool = 0 1365 ). 1366 1367fd_eq(Term, Bool) :- 1368 Bool :: 0..1, 1369 eq(Term, Bool). 1370 1371eq(Term, 1) :- 1372 -?-> 1373 fd_eq(Term). 1374eq(Term, 0) :- 1375 -?-> 1376 fd_ineq(Term). 1377eq(Term, Bool) :- 1378 var(Bool), 1379 (linear_term_range_eq(Term, Res, Min, Max, NewTerm, _) -> 1380 handle_eq_ent(NewTerm, Res, Min, Max, Bool) 1381 ; 1382 Bool = 0 1383 ). 1384 1385:- mode handle_eq_ent(+, ++, ++, ++, ?). 1386handle_eq_ent(_, 1, _, _, 1) :- !. % solved 1387handle_eq_ent(_, 3, _, _, 0) :- !. 1388handle_eq_ent(Term, 6, _, _, Bool) :- % type error 1389 !, 1390 tr_fd_arith_out_(fd_eq(Term, Bool), G), 1391 fderror(5, G). 1392handle_eq_ent(Term, 9, _, _, Bool) :- % not linearized 1393 !, 1394 unlinearize(Term, T), 1395 #=(T, 0, Bool). 1396handle_eq_ent(_, 10, X, Y, Bool) :- 1397 !, 1398 NewTerm = [1*X,-1*Y], 1399 handle_eq_ent(NewTerm, 5, 0, 0, Bool). 1400handle_eq_ent(Term, _, _, _, Bool) :- 1401 make_suspension(eq(Term, Bool), 3, Susp), 1402 ex_insert_suspension(Term, Susp, 1), 1403 insert_suspension(Bool, Susp, inst of suspend, suspend). 1404 1405% entailment of inequality; just use equality and reverse boolean 1406fd_ineq(Term, Bool) :- 1407 Bool :: [0..1], 1408 Bool + Rev #= 1, 1409 fd_eq(Term, Rev). 1410 1411% 1412% entailment of #>= 1413% 1414fd_ge(Term, B) :- 1415 B :: 0..1, 1416 ge(Term, B, _Susp). 1417 1418:- demon ge/3. 1419ge(Term, 1, Susp) :- 1420 -?-> 1421 kill_suspension(Susp), 1422 fd_ge(Term). 1423ge(Term, 0, Susp) :- 1424 -?-> 1425 kill_suspension(Susp), 1426 negate(Term, NewTerm), 1427 fd_ge([-1|NewTerm]). 1428ge(Term, B, Susp) :- 1429 var(B), 1430 (linear_term_range_ge(Term, Res, K, Max, NewTerm, Offset) -> 1431 handle_ge_ent(NewTerm, Term, Res, Max, Offset, K, B, Susp) 1432 ; 1433 kill_suspension(Susp), 1434 B = 0 1435 ). 1436 1437negate([], []). 1438negate([K*V|L1], T) :- 1439 -?-> 1440 !, 1441 K1 is -K, 1442 T = [K1*V|T1], 1443 negate(L1, T1). 1444negate([C|L], [C1|T]) :- 1445 C1 is -C, 1446 negate(L, T). 1447 1448:- mode handle_ge_ent(+, +, ++, ++, ++, ++, ?, ?). 1449handle_ge_ent(_, _, 1, _, _, _, 1, Susp) :- !, % solved 1450 kill_suspension(Susp). 1451handle_ge_ent(_, _, 2, _, _, _, 1, Susp) :- !, % solved 1452 kill_suspension(Susp). 1453handle_ge_ent(_, _, 3, _, _, _, 1, Susp) :- !, % solved 1454 kill_suspension(Susp). 1455handle_ge_ent(Term, _, 6, _, _, _, _, Susp) :- % type error 1456 !, 1457 kill_suspension(Susp), 1458 tr_fd_arith_out_(fd_ge(Term), G), 1459 fderror(5, G). 1460handle_ge_ent(Term, _, 9, _, _, _, B, Susp) :- % not linearized 1461 !, 1462 kill_suspension(Susp), 1463 unlinearize(Term, T), 1464 fd_eval(#>=(T, 0, B)). 1465handle_ge_ent(X, _, 10, Y, C, K, B, Susp) :- % simple relation 1466 !, 1467 kill_suspension(Susp), 1468 gec_ent(X, K, Y, C, B, _Susp). 1469handle_ge_ent(Term, OldTerm, _, _, _, _, B, Susp) :- % no updates 1470 ( var(Susp) -> 1471 suspend(ge(Term, B, Susp), 3, [Term->min, Term->max, B->inst], Susp) 1472 ; 1473 (Term \== OldTerm -> % Term has changed, suspension needs update 1474 get_suspension_data(Susp, goal, Goal), 1475 setarg(1, Goal, Term) 1476 ; true 1477 ) 1478 ). 1479 1480 1481fd_gec_ent(X, K, Y, C, D, 0) :- 1482 -?-> 1483 X + K*Y + C #< D. 1484fd_gec_ent(X, K, Y, C, D, 1) :- 1485 -?-> 1486 fd_gec(X, K, Y, C, D). 1487fd_gec_ent(X, K, Y, C, D, Bool) :- 1488 var(Bool), 1489 Bool :: 0..1, 1490 gec_ent_start(X, K, Y, C, D, E, Res), 1491 gec_ent_res(X, K, Y, E, Bool, Res, _Susp). 1492 1493:- demon gec_ent/6. 1494gec_ent(X, K, Y, C, 1, Susp) :- 1495 -?-> 1496 kill_suspension(Susp), 1497 gec(X, K, Y, C). 1498gec_ent(X, K, Y, C, 0, Susp) :- 1499 -?-> 1500 kill_suspension(Susp), 1501 C1 is -(C + 1), 1502 K1 is -K, 1503 fd_ge([C1, -1*X, K1*Y]). 1504gec_ent(X, K, Y, C, B, Susp) :- 1505 var(B), 1506 gec_test(X, K, Y, C, Res), 1507 gec_ent_res(X, K, Y, C, B, Res, Susp). 1508 1509:- mode gec_ent_res(?, ++, ?, ++, ?, ++, ?). 1510gec_ent_res(X, K, Y, C, B, 0, Susp) :- % delay 1511 ( var(Susp) -> 1512 suspend(gec_ent(X, K, Y, C, B, Susp), 2, 1513 [X-Y->min, X-Y->max, B->inst], Susp) %%% what about C? 1514 ; 1515 true 1516 ). 1517gec_ent_res(_, _, _, _, B, 5, Susp) :- % true 1518 kill_suspension(Susp), 1519 B = 1. 1520gec_ent_res(_, _, _, _, B, 11, Susp) :- % false 1521 kill_suspension(Susp), 1522 B = 0. 1523gec_ent_res(X, K, Y, C, B, 6, Susp) :- % error 1524 kill_suspension(Susp), 1525 (var(X), var(Y), var(C) -> 1526 fd_ge([1*X, K*Y, 1*C], B) 1527 ; 1528 conv_pred(#>=(X+K*Y+C, 0, B), run, List, []) -> 1529 call_list(List) 1530 ; 1531 tr_fd_arith_out_(gec(X, K, Y, C, B), G), 1532 fderror(5, G) 1533 ). 1534gec_ent_res(X, K, Y, C, B, 7, Susp) :- % error 1535 kill_suspension(Susp), 1536 (var(X), var(Y), var(C) -> 1537 fd_ge([1*X, K*Y, -1*C], B) 1538 ; 1539 conv_pred(#>=(X+K*Y-C, 0, B), run, List, []) -> 1540 call_list(List) 1541 ; 1542 tr_fd_arith_out_(gec(X, K, Y, -C, B), G), 1543 fderror(5, G) 1544 ). 1545 1546 1547%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1548% 1549% Y * Z = X 1550% 1551%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1552 1553fd_qeq(Y, Z, X) :- 1554 check_dom(X), 1555 check_dom(Y), 1556 check_dom(Z), 1557 qeq(Y, Z, X). 1558 1559qeq(Y, Z, X) :- 1560 dvar_domain(X, DomX), 1561 dvar_domain(Y, DomY), 1562 dvar_domain(Z, DomZ), 1563 dom_range(DomX, MinX, MaxX), 1564 dom_range(DomY, MinY, MaxY), 1565 dom_range(DomZ, MinZ, MaxZ), 1566 % propagate to X 1567 % update the maximum 1568 (MinY >= 0 -> 1569 (MinZ >= 0 -> 1570 qequpmax(MaxY, MaxZ, MaxX, X, Upd), 1571 qequpmin(MinY, MinZ, MinX, X, Upd) 1572 ; 1573 MaxZ >= 0 -> 1574 qequpmax(MaxY, MaxZ, MaxX, X, Upd), 1575 qequpmin(MaxY, MinZ, MinX, X, Upd) 1576 ; 1577 qequpmax(MinY, MaxZ, MaxX, X, Upd), 1578 qequpmin(MaxY, MinZ, MinX, X, Upd) 1579 ) 1580 ; 1581 MaxY >= 0 -> 1582 (MinZ >= 0 -> 1583 qequpmax(MaxY, MaxZ, MaxX, X, Upd), 1584 qequpmin(MinY, MaxZ, MinX, X, Upd) 1585 ; 1586 MaxZ >= 0 -> 1587 (MaxY*MaxZ > MinY*MinZ -> 1588 qequpmax(MaxY, MaxZ, MaxX, X, Upd) 1589 ; 1590 qequpmax(MinY, MinZ, MaxX, X, Upd) 1591 ), 1592 (MaxY*MinZ < MinY*MaxZ -> 1593 qequpmin(MaxY, MinZ, MinX, X, Upd) 1594 ; 1595 qequpmin(MinY, MaxZ, MinX, X, Upd) 1596 ) 1597 ; 1598 qequpmax(MinY, MinZ, MaxX, X, Upd), 1599 qequpmin(MaxY, MinZ, MinX, X, Upd) 1600 ) 1601 ; 1602 (MinZ >= 0 -> 1603 qequpmax(MaxY, MinZ, MaxX, X, Upd), 1604 qequpmin(MinY, MaxZ, MinX, X, Upd) 1605 ; 1606 MaxZ >= 0 -> 1607 qequpmax(MinY, MinZ, MaxX, X, Upd), 1608 qequpmin(MinY, MaxZ, MinX, X, Upd) 1609 ; 1610 qequpmax(MinY, MinZ, MaxX, X, Upd), 1611 qequpmin(MaxY, MaxZ, MinX, X, Upd) 1612 ) 1613 ), 1614 % propagate from X 1615 qeqdownmin(MinX, MaxX, MinZ, MaxZ, MinY, Y, Upd), 1616 qeqdownmin(MinX, MaxX, MinY, MaxY, MinZ, Z, Upd), 1617 qeqdownmax(MinX, MaxX, MinZ, MaxZ, MaxY, Y, Upd), 1618 qeqdownmax(MinX, MaxX, MinY, MaxY, MaxZ, Z, Upd), 1619 (nonvar(Upd) -> 1620 qeq(Y, Z, X) 1621 ; 1622 Vars = p(X, Y, Z), 1623 term_variables(Vars, VL), 1624 length(VL, N), 1625 (N = 3 -> 1626 make_suspension(qeq(Y, Z, X), 4, Susp), 1627 insert_suspension(Vars, Susp, bound of suspend, suspend), 1628 insert_suspension(Vars, Susp, min of fd, fd), 1629 insert_suspension(Vars, Susp, max of fd, fd) 1630 ; 1631 N = 2 -> 1632 ntimes2(Y, Z, X) 1633 ; 1634 ntimes1(Y, Z, X) 1635 ), 1636 wake 1637 ). 1638 1639qequpmin(M1, M2, MinX, X, Upd) :- 1640 MiX is min(100000,M1*M2), 1641 (MiX > MinX -> 1642 dvar_remove_smaller(X, MiX), 1643 Upd = 1 1644 ; 1645 true 1646 ). 1647 1648qequpmax(M1, M2, MaxX, X, Upd) :- 1649 MaX is max(-100000,M1*M2), 1650 (MaX < MaxX -> 1651 dvar_remove_greater(X, MaX), 1652 true, 1653 Upd = 1 1654 ; 1655 true 1656 ). 1657 1658qeqdownmax(MinX, MaxX, MinZ, MaxZ, MaxY, Y, Upd) :- 1659 (MinZ >= 0 -> 1660 (MaxX >= 0 -> 1661 qeqdownmax(MaxX, MinZ, MaxY, Y, Upd) 1662 ; 1663 qeqdownmax(MaxX, MaxZ, MaxY, Y, Upd) 1664 ) 1665 ; 1666 MaxZ >= 0 -> 1667 (MinX >= 0 -> 1668 qeqdownmax(MaxX, 1, MaxY, Y, Upd) 1669 ; 1670 MaxX >= 0 -> 1671 Mx1 is max(MaxX, -MinX), 1672 qeqdownmax(Mx1, 1, MaxY, Y, Upd) 1673 ; 1674 qeqdownmax(MinX, -1, MaxY, Y, Upd) 1675 ) 1676 ; 1677 MinX >= 0 -> 1678 qeqdownmax(MinX, MinZ, MaxY, Y, Upd) 1679 ; 1680 qeqdownmax(MinX, MaxZ, MaxY, Y, Upd) 1681 ). 1682 1683qeqdownmin(MinX, MaxX, MinZ, MaxZ, MinY, Y, Upd) :- 1684 (MinZ >= 0 -> 1685 (MinX >= 0 -> 1686 qeqdownmin(MinX, MaxZ, MinY, Y, Upd) 1687 ; 1688 qeqdownmin(MinX, MinZ, MinY, Y, Upd) 1689 ) 1690 ; 1691 MaxZ >= 0 -> 1692 (MinX >= 0 -> 1693 qeqdownmin(MaxX, -1, MinY, Y, Upd) 1694 ; 1695 MaxX >= 0 -> 1696 Mx1 is min(-MaxX, MinX), 1697 qeqdownmin(Mx1, -1, MinY, Y, Upd) 1698 ; 1699 qeqdownmin(MinX, 1, MinY, Y, Upd) 1700 ) 1701 ; 1702 MaxX >= 0 -> 1703 qeqdownmin(MaxX, MaxZ, MinY, Y, Upd) 1704 ; 1705 qeqdownmin(MaxX, MinZ, MinY, Y, Upd) 1706 ). 1707 1708qeqdownmax(MaxX, MinY, MaxZ, Z, Upd) :- 1709 (MaxX < MinY*MaxZ -> 1710 (sgn(MaxX) =:= sgn(MinY) -> 1711 NM is MaxX//MinY 1712 ; 1713 NM is (MaxX + MinY - 1)//MinY 1714 ), 1715 (NM < MaxZ -> 1716 dvar_remove_greater(Z, NM), 1717 Upd = 1 1718 ; 1719 true 1720 ) 1721 ; 1722 true 1723 ). 1724 1725qeqdownmin(MinX, MaxY, MinZ, Z, Upd) :- 1726 (MinX > MaxY*MinZ -> 1727 (sgn(MinX) =:= sgn(MaxY) -> 1728 NM is (MinX + MaxY - 1)//MaxY 1729 ; 1730 NM is MinX//MaxY 1731 ), 1732 (NM > MinZ -> 1733 dvar_remove_smaller(Z, NM), 1734 Upd = 1 1735 ; 1736 true 1737 ) 1738 ; 1739 true 1740 ). 1741 1742% Y*Y = X 1743qeqsquare(Y, X ) :- 1744 fd_abs(Y,AY), 1745 suspend(qeqsquare(AY,X,Susp),4,[[AY|X]->min,[AY|X]->max],Susp), 1746 qeqsquare(AY,X,Susp). 1747 1748 % Y is positive 1749:- demon qeqsquare/3. 1750qeqsquare(Y, X ,Susp) :- 1751 ( X==Y -> 1752 X::0..1, 1753 kill_suspension(Susp) 1754 ; integer(X) -> 1755 PY is fix(sqrt(X)), 1756 X is PY*PY, 1757 NY is -PY, 1758 Y:: [NY,PY], 1759 kill_suspension(Susp) 1760 ; integer(Y) -> 1761 X is Y*Y, 1762 kill_suspension(Susp) 1763 ; 1764 % propagate to X 1765 fd_util:dvar_range(Y, MinY, MaxY), 1766 fd_util:dvar_range(X, MinX, MaxX), 1767 NewMinX is MinY*MinY, % may have created a bignum 1768 (NewMinX > MinX -> 1769 dvar_remove_smaller(X, NewMinX), 1770 Min = NewMinX 1771 ; 1772 Min = MinX 1773 ), 1774 NewMaxX is MaxY*MaxY, 1775 (NewMaxX < MaxX -> % may have created a bignum 1776 dvar_remove_greater(X, NewMaxX), 1777 Max = NewMaxX 1778 ; 1779 Max = MaxX 1780 ), 1781 % propagate to Y 1782 MinS is fix(ceiling(sqrt(Min))), % round up 1783 MaxS is fix(sqrt(Max)), % round down 1784 dvar_remove_smaller(Y, MinS), 1785 dvar_remove_greater(Y, MaxS) 1786 ). 1787 1788 1789 1790ntimes2(0, _, C) :- 1791 -?-> 1792 !, 1793 C = 0. 1794ntimes2(_, 0, C) :- 1795 -?-> 1796 !, 1797 C = 0. 1798ntimes2(1, B, C) :- 1799 -?-> 1800 !, 1801 C = B. 1802ntimes2(A, 1, C) :- 1803 -?-> 1804 !, 1805 C = A. 1806ntimes2(X, X, Y) :- 1807 -?-> 1808 !, 1809 qeqsquare(X,Y). 1810ntimes2(X, Y, X) :- 1811 -?-> 1812 !, 1813 ( X #= 0 #\/ Y #= 1). 1814ntimes2(Y, Z, X) :- 1815 integer(Y), 1816 !, 1817 Y*Z #= X. 1818ntimes2(Y, Z, X) :- 1819 integer(Z), 1820 !, 1821 Y*Z #= X. 1822ntimes2(Y, X, X) :- 1823 -?-> 1824 !, 1825 ( X #= 0 #\/ Y #= 1). 1826ntimes2(Y, Z, X) :- 1827 Goal = qeq(Y, Z, X), 1828 make_suspension(Goal, 4, Susp), 1829 insert_suspension(Goal, Susp, bound of suspend, suspend), 1830 insert_suspension(Goal, Susp, min of fd, fd), 1831 insert_suspension(Goal, Susp, max of fd, fd). 1832 1833% we know there is only one variable 1834% but some of A,B,C may be the same variable 1835ntimes1(A, B, C) :- 1836 ( var(A) -> 1837 ( var(B) -> 1838 ( var(C) -> 1839 A::0..1 1840 ; % C is ground 1841 S is sqrt(C), 1842 FS is fix(S), 1843 C is FS * FS, 1844 MFS is - FS, 1845 A::[MFS,FS] 1846 ) 1847 ; % B is ground 1848 ( var(C) -> 1849 ( B=1 -> 1850 true 1851 ; 1852 A=0 1853 ) 1854 ; 1855 times(A,B,C) 1856 ) 1857 ) 1858 ; 1859 ( var(B) -> 1860 ( var(C) -> 1861 ( A=1 -> 1862 true 1863 ; 1864 B=0 1865 ) 1866 ; 1867 times(A,B,C) 1868 ) 1869 ; 1870 times(A,B,C) 1871 ) 1872 ). 1873 1874 1875 1876check_dom(_{fd:(fd with [])}) :- -?-> !. 1877check_dom(Var) :- var(Var), !, 1878 default_domain(Var). 1879check_dom(_). 1880 1881default_domain(V) :- 1882 V :: -10000000..10000000. 1883 1884 1885%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1886% 1887% abs(X) 1888% 1889%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1890 1891:- export fd_abs/2. 1892fd_abs(X,A) :- 1893 A #>= 0, 1894 suspend(fd_abs(X,A,Susp),3,[X->any,A->min,A->max],Susp), 1895 fd_abs(X,A,Susp). 1896 1897:- demon fd_abs/3. 1898fd_abs(X,A,Susp):- 1899 fd_util:dvar_range(A,AMin,AMax), 1900 MAMax is -AMax, 1901 MAMin is -AMin, 1902 X::[MAMax..MAMin,AMin..AMax], 1903 fd_util:dvar_range(X,Xmin,Xmax), 1904 ( Xmin >=0 -> 1905 kill_suspension(Susp), 1906 X=A 1907 ; Xmax =< 0 -> 1908 kill_suspension(Susp), 1909 A #= -X 1910 ; 1911 dvar_domain(X,XDom), 1912 dom_min_abs(XDom,XMinAbs), 1913 XMaxAbs is max(-Xmin,Xmax), 1914 dvar_remove_smaller(A,XMinAbs), 1915 dvar_remove_greater(A,XMaxAbs), 1916 (var(A),var(X) -> 1917 true 1918 ; 1919 kill_suspension(Susp) 1920 ), 1921 wake 1922 ). 1923 1924% Find the smallest absolute value in the domain of X 1925dom_min_abs(dom(List,_), MinAbs) :- 1926 dom_min_abs(List, -10000000, MaxNeg, MinPos), 1927 MinAbs is min(-MaxNeg, MinPos). 1928 1929 dom_min_abs([], MaxNeg, MaxNeg, MaxNeg). 1930 dom_min_abs([I|Is], MaxNeg0, MaxNeg, MinPos) :- 1931 ( I = From..To -> 1932 ( From >= 0 -> 1933 MaxNeg = MaxNeg0, MinPos = From 1934 ; To < 0 -> 1935 dom_min_abs(Is, To, MaxNeg, MinPos) 1936 ; 1937 MaxNeg = 0, MinPos = 0 1938 ) 1939 ; I >= 0 -> 1940 MaxNeg = MaxNeg0, MinPos = I 1941 ; 1942 dom_min_abs(Is, I, MaxNeg, MinPos) 1943 ). 1944 1945 1946%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1947% 1948% min(X,Y) and max(X,Y) 1949% 1950%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 1951 1952:- export fd_min/4. 1953:- demon(fd_min/4). 1954fd_min(A, B, M, Susp):- 1955 call_priority(( 1956 fd_util:dvar_range(A, MinA, MaxA), 1957 fd_util:dvar_range(B, MinB, MaxB), 1958 fd_util:dvar_range(M, MinM, MaxM), 1959 Max is min(MaxA, MaxB), 1960 Min is min(MinA, MinB), 1961 dvar_remove_smaller(M, Min), % M :: Min..Max 1962 dvar_remove_greater(M, Max), 1963 1964 dvar_remove_smaller(A, MinM), % A #>= MinM 1965 dvar_remove_smaller(B, MinM), % B #>= MinM 1966 1967 ( MaxA =< MinB -> 1968 kill_suspension(Susp), 1969 A = M 1970 ; MaxB =< MinA -> 1971 kill_suspension(Susp), 1972 B = M 1973 ; MaxM < MinB -> 1974 kill_suspension(Susp), 1975 A = M 1976 ; MaxM < MinA -> 1977 kill_suspension(Susp), 1978 B = M 1979 ; Vars=v(A,B,M), nonground(2,Vars,_) -> 1980 ( nonvar(Susp) -> 1981 true % re-suspend 1982 ; 1983 suspend(fd_min(A, B, M, Susp), 3, [Vars->min,Vars->max], Susp) 1984 ) 1985 ; 1986 kill_suspension(Susp) 1987 ) 1988 ), 2). 1989 1990 1991:- export fd_max/4. 1992:- demon(fd_max/4). 1993fd_max(A, B, M, Susp):- 1994 call_priority(( 1995 fd_util:dvar_range(A, MinA, MaxA), 1996 fd_util:dvar_range(B, MinB, MaxB), 1997 fd_util:dvar_range(M, MinM, MaxM), 1998 Max is max(MaxA, MaxB), 1999 Min is max(MinA, MinB), 2000 dvar_remove_smaller(M, Min), % M :: Min..Max 2001 dvar_remove_greater(M, Max), 2002 2003 dvar_remove_greater(A, MaxM), % A #=< MaxM 2004 dvar_remove_greater(B, MaxM), % B #=< MaxM 2005 2006 ( MinA >= MaxB -> 2007 kill_suspension(Susp), 2008 A = M 2009 ; MinB >= MaxA -> 2010 kill_suspension(Susp), 2011 B = M 2012 ; MinM > MaxB -> 2013 kill_suspension(Susp), 2014 A = M 2015 ; MinM > MaxA -> 2016 kill_suspension(Susp), 2017 B = M 2018 ; Vars=v(A,B,M), nonground(2,Vars,_) -> 2019 ( nonvar(Susp) -> 2020 true % re-suspend 2021 ; 2022 suspend(fd_max(A, B, M, Susp), 3, [Vars->min,Vars->max], Susp) 2023 ) 2024 ; 2025 kill_suspension(Susp) 2026 ) 2027 ), 2). 2028 2029