1/* $Id$ 2 3 Part of CLP(Q) (Constraint Logic Programming over Rationals) 4 5 Author: Leslie De Koninck 6 E-mail: Leslie.DeKoninck@cs.kuleuven.be 7 WWW: http://www.swi-prolog.org 8 http://www.ai.univie.ac.at/cgi-bin/tr-online?number+95-09 9 Copyright (C): 2006, K.U. Leuven and 10 1992-1995, Austrian Research Institute for 11 Artificial Intelligence (OFAI), 12 Vienna, Austria 13 14 This software is based on CLP(Q,R) by Christian Holzbaur for SICStus 15 Prolog and distributed under the license details below with permission from 16 all mentioned authors. 17 18 This program is free software; you can redistribute it and/or 19 modify it under the terms of the GNU General Public License 20 as published by the Free Software Foundation; either version 2 21 of the License, or (at your option) any later version. 22 23 This program is distributed in the hope that it will be useful, 24 but WITHOUT ANY WARRANTY; without even the implied warranty of 25 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the 26 GNU General Public License for more details. 27 28 You should have received a copy of the GNU Lesser General Public 29 License along with this library; if not, write to the Free Software 30 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA 31 32 As a special exception, if you link this library with other files, 33 compiled with a Free Software compiler, to produce an executable, this 34 library does not by itself cause the resulting executable to be covered 35 by the GNU General Public License. This exception does not however 36 invalidate any other reasons why the executable file might be covered by 37 the GNU General Public License. 38*/ 39 40 41:- module(ineq_q, 42 [ 43 ineq/4, 44 ineq_one/4, 45 ineq_one_n_n_0/1, 46 ineq_one_n_p_0/1, 47 ineq_one_s_n_0/1, 48 ineq_one_s_p_0/1 49 ]). 50:- use_module(bv_q, 51 [ 52 backsubst/3, 53 backsubst_delta/4, 54 basis_add/2, 55 dec_step/2, 56 deref/2, 57 determine_active_dec/1, 58 determine_active_inc/1, 59 export_binding/1, 60 get_or_add_class/2, 61 inc_step/2, 62 lb/3, 63 pivot_a/4, 64 rcbl_status/6, 65 reconsider/1, 66 same_class/2, 67 solve/1, 68 ub/3, 69 unconstrained/4, 70 var_intern/3, 71 var_with_def_intern/4 72 ]). 73:- use_module(store_q, 74 [ 75 add_linear_11/3, 76 add_linear_ff/5, 77 normalize_scalar/2 78 ]). 79 80% ineq(H,I,Nf,Strictness) 81% 82% Solves the inequality Nf < 0 or Nf =< 0 where Nf is in normal form 83% and H and I are the homogene and inhomogene parts of Nf. 84 85ineq([],I,_,Strictness) :- ineq_ground(Strictness,I). 86ineq([v(K,[X^1])|Tail],I,Lin,Strictness) :- 87 ineq_cases(Tail,I,Lin,Strictness,X,K). 88 89ineq_cases([],I,_,Strictness,X,K) :- % K*X + I < 0 or K*X + I =< 0 90 ineq_one(Strictness,X,K,I). 91ineq_cases([_|_],_,Lin,Strictness,_,_) :- 92 deref(Lin,Lind), % Id+Hd =< 0 93 Lind = [Inhom,_|Hom], 94 ineq_more(Hom,Inhom,Lind,Strictness). 95 96% ineq_ground(Strictness,I) 97% 98% Checks whether a grounded inequality I < 0 or I =< 0 is satisfied. 99 100ineq_ground(strict,I) :- I < 0. 101ineq_ground(nonstrict,I) :- I =< 0. 102 103% ineq_one(Strictness,X,K,I) 104% 105% Solves the inequality K*X + I < 0 or K*X + I =< 0 106 107ineq_one(strict,X,K,I) :- 108 ( K > 0 109 -> ( I =:= 0 110 -> ineq_one_s_p_0(X) % K*X < 0, K > 0 => X < 0 111 ; Inhom is I rdiv K, 112 ineq_one_s_p_i(X,Inhom) % K*X + I < 0, K > 0 => X + I/K < 0 113 ) 114 ; ( I =:= 0 115 -> ineq_one_s_n_0(X) % K*X < 0, K < 0 => -X < 0 116 ; Inhom is -I rdiv K, 117 ineq_one_s_n_i(X,Inhom) % K*X + I < 0, K < 0 => -X - I/K < 0 118 ) 119 ). 120ineq_one(nonstrict,X,K,I) :- 121 ( K > 0 122 -> ( I =:= 0 123 -> ineq_one_n_p_0(X) % K*X =< 0, K > 0 => X =< 0 124 ; Inhom is I rdiv K, 125 ineq_one_n_p_i(X,Inhom) % K*X + I =< 0, K > 0 => X + I/K =< 0 126 ) 127 ; ( I =:= 0 128 -> ineq_one_n_n_0(X) % K*X =< 0, K < 0 => -X =< 0 129 ; Inhom is -I rdiv K, 130 ineq_one_n_n_i(X,Inhom) % K*X + I =< 0, K < 0 => -X - I/K =< 0 131 ) 132 ). 133 134% --------------------------- strict ---------------------------- 135 136% ineq_one_s_p_0(X) 137% 138% Solves the inequality X < 0 139 140ineq_one_s_p_0(X) :- 141 get_attr(X,itf,Att), 142 arg(4,Att,lin([Ix,_|OrdX])), 143 !, % old variable, this is deref 144 ( \+ arg(1,Att,clpq) 145 -> throw(error(permission_error('mix CLP(Q) variables with', 146 'CLP(R) variables:',X),context(_))) 147 ; ineq_one_old_s_p_0(OrdX,X,Ix) 148 ). 149ineq_one_s_p_0(X) :- % new variable, nothing depends on it 150 var_intern(t_u(0),X,1). % put a strict inactive upperbound on the variable 151 152% ineq_one_s_n_0(X) 153% 154% Solves the inequality X > 0 155 156ineq_one_s_n_0(X) :- 157 get_attr(X,itf,Att), 158 arg(4,Att,lin([Ix,_|OrdX])), 159 !, 160 ( \+ arg(1,Att,clpq) 161 -> throw(error(permission_error('mix CLP(Q) variables with', 162 'CLP(R) variables:',X),context(_))) 163 ; ineq_one_old_s_n_0(OrdX,X,Ix) 164 ). 165ineq_one_s_n_0(X) :- 166 var_intern(t_l(0),X,2). % puts a strict inactive lowerbound on the variable 167 168% ineq_one_s_p_i(X,I) 169% 170% Solves the inequality X < -I 171 172ineq_one_s_p_i(X,I) :- 173 get_attr(X,itf,Att), 174 arg(4,Att,lin([Ix,_|OrdX])), 175 !, 176 ( \+ arg(1,Att,clpq) 177 -> throw(error(permission_error('mix CLP(Q) variables with', 178 'CLP(R) variables:',X),context(_))) 179 ; ineq_one_old_s_p_i(OrdX,I,X,Ix) 180 ). 181ineq_one_s_p_i(X,I) :- 182 Bound is -I, 183 var_intern(t_u(Bound),X,1). % puts a strict inactive upperbound on the variable 184 185% ineq_one_s_n_i(X,I) 186% 187% Solves the inequality X > I 188 189ineq_one_s_n_i(X,I) :- 190 get_attr(X,itf,Att), 191 arg(4,Att,lin([Ix,_|OrdX])), 192 !, 193 ( \+ arg(1,Att,clpq) 194 -> throw(error(permission_error('mix CLP(Q) variables with', 195 'CLP(R) variables:',X),context(_))) 196 ; ineq_one_old_s_n_i(OrdX,I,X,Ix) 197 ). 198ineq_one_s_n_i(X,I) :- var_intern(t_l(I),X,2). % puts a strict inactive lowerbound on the variable 199 200% ineq_one_old_s_p_0(Hom,X,Inhom) 201% 202% Solves the inequality X < 0 where X has linear equation Hom + Inhom 203 204ineq_one_old_s_p_0([],_,Ix) :- Ix < 0. % X = I: Ix < 0 205ineq_one_old_s_p_0([l(Y*Ky,_)|Tail],X,Ix) :- 206 ( Tail = [] % X = K*Y + I 207 -> Bound is -Ix rdiv Ky, 208 update_indep(strict,Y,Ky,Bound) % X < 0, X = K*Y + I => Y < -I/K or Y > -I/K (depending on K) 209 ; Tail = [_|_] 210 -> get_attr(X,itf,Att), 211 arg(2,Att,type(Type)), 212 arg(3,Att,strictness(Old)), 213 arg(4,Att,lin(Lin)), 214 udus(Type,X,Lin,0,Old) % update strict upperbound 215 ). 216 217% ineq_one_old_s_p_0(Hom,X,Inhom) 218% 219% Solves the inequality X > 0 where X has linear equation Hom + Inhom 220 221ineq_one_old_s_n_0([],_,Ix) :- Ix > 0. % X = I: Ix > 0 222ineq_one_old_s_n_0([l(Y*Ky,_)|Tail], X, Ix) :- 223 ( Tail = [] % X = K*Y + I 224 -> Coeff is -Ky, 225 Bound is Ix rdiv Coeff, 226 update_indep(strict,Y,Coeff,Bound) 227 ; Tail = [_|_] 228 -> get_attr(X,itf,Att), 229 arg(2,Att,type(Type)), 230 arg(3,Att,strictness(Old)), 231 arg(4,Att,lin(Lin)), 232 udls(Type,X,Lin,0,Old) % update strict lowerbound 233 ). 234 235% ineq_one_old_s_p_i(Hom,C,X,Inhom) 236% 237% Solves the inequality X + C < 0 where X has linear equation Hom + Inhom 238 239ineq_one_old_s_p_i([],I,_,Ix) :- I + Ix < 0. % X = I 240ineq_one_old_s_p_i([l(Y*Ky,_)|Tail],I,X,Ix) :- 241 ( Tail = [] % X = K*Y + I 242 -> Bound is -(Ix + I) rdiv Ky, 243 update_indep(strict,Y,Ky,Bound) 244 ; Tail = [_|_] 245 -> Bound is -I, 246 get_attr(X,itf,Att), 247 arg(2,Att,type(Type)), 248 arg(3,Att,strictness(Old)), 249 arg(4,Att,lin(Lin)), 250 udus(Type,X,Lin,Bound,Old) % update strict upperbound 251 ). 252 253% ineq_one_old_s_n_i(Hom,C,X,Inhom) 254% 255% Solves the inequality X - C > 0 where X has linear equation Hom + Inhom 256 257ineq_one_old_s_n_i([],I,_,Ix) :- I - Ix < 0. % X = I 258ineq_one_old_s_n_i([l(Y*Ky,_)|Tail],I,X,Ix) :- 259 ( Tail = [] % X = K*Y + I 260 -> Coeff is -Ky, 261 Bound is (Ix - I) rdiv Coeff, 262 update_indep(strict,Y,Coeff,Bound) 263 ; Tail = [_|_] 264 -> get_attr(X,itf,Att), 265 arg(2,Att,type(Type)), 266 arg(3,Att,strictness(Old)), 267 arg(4,Att,lin(Lin)), 268 udls(Type,X,Lin,I,Old) % update strict lowerbound 269 ). 270 271% -------------------------- nonstrict -------------------------- 272 273% ineq_one_n_p_0(X) 274% 275% Solves the inequality X =< 0 276 277ineq_one_n_p_0(X) :- 278 get_attr(X,itf,Att), 279 arg(4,Att,lin([Ix,_|OrdX])), 280 !, % old variable, this is deref 281 ( \+ arg(1,Att,clpq) 282 -> throw(error(permission_error('mix CLP(Q) variables with', 283 'CLP(R) variables:',X),context(_))) 284 ; ineq_one_old_n_p_0(OrdX,X,Ix) 285 ). 286ineq_one_n_p_0(X) :- % new variable, nothing depends on it 287 var_intern(t_u(0),X,0). % nonstrict upperbound 288 289% ineq_one_n_n_0(X) 290% 291% Solves the inequality X >= 0 292 293ineq_one_n_n_0(X) :- 294 get_attr(X,itf,Att), 295 arg(4,Att,lin([Ix,_|OrdX])), 296 !, 297 ( \+ arg(1,Att,clpq) 298 -> throw(error(permission_error('mix CLP(Q) variables with', 299 'CLP(R) variables:',X),context(_))) 300 ; ineq_one_old_n_n_0(OrdX,X,Ix) 301 ). 302ineq_one_n_n_0(X) :- 303 var_intern(t_l(0),X,0). % nonstrict lowerbound 304 305% ineq_one_n_p_i(X,I) 306% 307% Solves the inequality X =< -I 308 309ineq_one_n_p_i(X,I) :- 310 get_attr(X,itf,Att), 311 arg(4,Att,lin([Ix,_|OrdX])), 312 !, 313 ( \+ arg(1,Att,clpq) 314 -> throw(error(permission_error('mix CLP(Q) variables with', 315 'CLP(R) variables:',X),context(_))) 316 ; ineq_one_old_n_p_i(OrdX,I,X,Ix) 317 ). 318ineq_one_n_p_i(X,I) :- 319 Bound is -I, 320 var_intern(t_u(Bound),X,0). % nonstrict upperbound 321 322% ineq_one_n_n_i(X,I) 323% 324% Solves the inequality X >= I 325 326ineq_one_n_n_i(X,I) :- 327 get_attr(X,itf,Att), 328 arg(4,Att,lin([Ix,_|OrdX])), 329 !, 330 ( \+ arg(1,Att,clpq) 331 -> throw(error(permission_error('mix CLP(Q) variables with', 332 'CLP(R) variables:',X),context(_))) 333 ; ineq_one_old_n_n_i(OrdX,I,X,Ix) 334 ). 335ineq_one_n_n_i(X,I) :- 336 var_intern(t_l(I),X,0). % nonstrict lowerbound 337 338% ineq_one_old_n_p_0(Hom,X,Inhom) 339% 340% Solves the inequality X =< 0 where X has linear equation Hom + Inhom 341 342ineq_one_old_n_p_0([],_,Ix) :- Ix =< 0. % X =I 343ineq_one_old_n_p_0([l(Y*Ky,_)|Tail],X,Ix) :- 344 ( Tail = [] % X = K*Y + I 345 -> Bound is -Ix rdiv Ky, 346 update_indep(nonstrict,Y,Ky,Bound) 347 ; Tail = [_|_] 348 -> get_attr(X,itf,Att), 349 arg(2,Att,type(Type)), 350 arg(3,Att,strictness(Old)), 351 arg(4,Att,lin(Lin)), 352 udu(Type,X,Lin,0,Old) % update nonstrict upperbound 353 ). 354 355% ineq_one_old_n_n_0(Hom,X,Inhom) 356% 357% Solves the inequality X >= 0 where X has linear equation Hom + Inhom 358 359ineq_one_old_n_n_0([],_,Ix) :- Ix >= 0. % X = I 360ineq_one_old_n_n_0([l(Y*Ky,_)|Tail], X, Ix) :- 361 ( Tail = [] % X = K*Y + I 362 -> Coeff is -Ky, 363 Bound is Ix rdiv Coeff, 364 update_indep(nonstrict,Y,Coeff,Bound) 365 ; Tail = [_|_] 366 -> get_attr(X,itf,Att), 367 arg(2,Att,type(Type)), 368 arg(3,Att,strictness(Old)), 369 arg(4,Att,lin(Lin)), 370 udl(Type,X,Lin,0,Old) % update nonstrict lowerbound 371 ). 372 373% ineq_one_old_n_p_i(Hom,C,X,Inhom) 374% 375% Solves the inequality X + C =< 0 where X has linear equation Hom + Inhom 376 377ineq_one_old_n_p_i([],I,_,Ix) :- I + Ix =< 0. % X = I 378ineq_one_old_n_p_i([l(Y*Ky,_)|Tail],I,X,Ix) :- 379 ( Tail = [] % X = K*Y + I 380 -> Bound is -(Ix + I) rdiv Ky, 381 update_indep(nonstrict,Y,Ky,Bound) 382 ; Tail = [_|_] 383 -> Bound is -I, 384 get_attr(X,itf,Att), 385 arg(2,Att,type(Type)), 386 arg(3,Att,strictness(Old)), 387 arg(4,Att,lin(Lin)), 388 udu(Type,X,Lin,Bound,Old) % update nonstrict upperbound 389 ). 390 391% ineq_one_old_n_n_i(Hom,C,X,Inhom) 392% 393% Solves the inequality X - C >= 0 where X has linear equation Hom + Inhom 394 395ineq_one_old_n_n_i([],I,_,Ix) :- I - Ix =< 0. % X = I 396ineq_one_old_n_n_i([l(Y*Ky,_)|Tail],I,X,Ix) :- 397 ( Tail = [] 398 -> Coeff is -Ky, 399 Bound is (Ix - I) rdiv Coeff, 400 update_indep(nonstrict,Y,Coeff,Bound) 401 ; Tail = [_|_] 402 -> get_attr(X,itf,Att), 403 arg(2,Att,type(Type)), 404 arg(3,Att,strictness(Old)), 405 arg(4,Att,lin(Lin)), 406 udl(Type,X,Lin,I,Old) 407 ). 408 409% --------------------------------------------------------------- 410 411% ineq_more(Hom,Inhom,Lin,Strictness) 412% 413% Solves the inequality Lin < 0 or Lin =< 0 with Lin = Hom + Inhom 414 415ineq_more([],I,_,Strictness) :- ineq_ground(Strictness,I). % I < 0 or I =< 0 416ineq_more([l(X*K,_)|Tail],Id,Lind,Strictness) :- 417 ( Tail = [] 418 -> % X*K < Id or X*K =< Id 419 % one var: update bound instead of slack introduction 420 get_or_add_class(X,_), % makes sure X belongs to a class 421 Bound is -Id rdiv K, 422 update_indep(Strictness,X,K,Bound) % new bound 423 ; Tail = [_|_] 424 -> ineq_more(Strictness,Lind) 425 ). 426 427% ineq_more(Strictness,Lin) 428% 429% Solves the inequality Lin < 0 or Lin =< 0 430 431ineq_more(strict,Lind) :- 432 ( unconstrained(Lind,U,K,Rest) 433 -> % never fails, no implied value 434 % Lind < 0 => Rest < -K*U where U has no bounds 435 var_intern(t_l(0),S,2), % create slack variable S 436 get_attr(S,itf,AttS), 437 arg(5,AttS,order(OrdS)), 438 Ki is -1 rdiv K, 439 add_linear_ff(Rest,Ki,[0,0,l(S*1,OrdS)],Ki,LinU), % U = (-1/K)*Rest + (-1/K)*S 440 LinU = [_,_|Hu], 441 get_or_add_class(U,Class), 442 same_class(Hu,Class), % put all variables of new lin. eq. of U in the same class 443 get_attr(U,itf,AttU), 444 arg(5,AttU,order(OrdU)), 445 arg(6,AttU,class(ClassU)), 446 backsubst(ClassU,OrdU,LinU) % substitute U by new lin. eq. everywhere in the class 447 ; var_with_def_intern(t_u(0),S,Lind,1), % Lind < 0 => Lind = S with S < 0 448 basis_add(S,_), % adds S to the basis 449 determine_active_dec(Lind), % activate bounds 450 reconsider(S) % reconsider basis 451 ). 452ineq_more(nonstrict,Lind) :- 453 ( unconstrained(Lind,U,K,Rest) 454 -> % never fails, no implied value 455 % Lind =< 0 => Rest =< -K*U where U has no bounds 456 var_intern(t_l(0),S,0), % create slack variable S 457 Ki is -1 rdiv K, 458 get_attr(S,itf,AttS), 459 arg(5,AttS,order(OrdS)), 460 add_linear_ff(Rest,Ki,[0,0,l(S*1,OrdS)],Ki,LinU), % U = (-1K)*Rest + (-1/K)*S 461 LinU = [_,_|Hu], 462 get_or_add_class(U,Class), 463 same_class(Hu,Class), % put all variables of new lin. eq of U in the same class 464 get_attr(U,itf,AttU), 465 arg(5,AttU,order(OrdU)), 466 arg(6,AttU,class(ClassU)), 467 backsubst(ClassU,OrdU,LinU) % substitute U by new lin. eq. everywhere in the class 468 ; % all variables are constrained 469 var_with_def_intern(t_u(0),S,Lind,0), % Lind =< 0 => Lind = S with S =< 0 470 basis_add(S,_), % adds S to the basis 471 determine_active_dec(Lind), 472 reconsider(S) 473 ). 474 475 476% update_indep(Strictness,X,K,Bound) 477% 478% Updates the bound of independent variable X where X < Bound or X =< Bound 479% or X > Bound or X >= Bound, depending on Strictness and K. 480 481update_indep(strict,X,K,Bound) :- 482 get_attr(X,itf,Att), 483 arg(2,Att,type(Type)), 484 arg(3,Att,strictness(Old)), 485 arg(4,Att,lin(Lin)), 486 ( K < 0 487 -> uils(Type,X,Lin,Bound,Old) % update independent lowerbound strict 488 ; uius(Type,X,Lin,Bound,Old) % update independent upperbound strict 489 ). 490update_indep(nonstrict,X,K,Bound) :- 491 get_attr(X,itf,Att), 492 arg(2,Att,type(Type)), 493 arg(3,Att,strictness(Old)), 494 arg(4,Att,lin(Lin)), 495 ( K < 0 496 -> uil(Type,X,Lin,Bound,Old) % update independent lowerbound nonstrict 497 ; uiu(Type,X,Lin,Bound,Old) % update independent upperbound nonstrict 498 ). 499 500 501% --------------------------------------------------------------------------------------- 502 503% 504% Update a bound on a var xi 505% 506% a) independent variable 507% 508% a1) update inactive bound: done 509% 510% a2) update active bound: 511% Determine [lu]b including most constraining row R 512% If we are within: done 513% else pivot(R,xi) and introduce bound via (b) 514% 515% a3) introduce a bound on an unconstrained var: 516% All vars that depend on xi are unconstrained (invariant) -> 517% the bound cannot invalidate any Lhs 518% 519% b) dependent variable 520% 521% repair upper or lower (maybe just swap with an unconstrained var from Rhs) 522% 523 524% 525% Sign = 1,0,-1 means inside,at,outside 526% 527 528% Read following predicates as update (dependent/independent) (lowerbound/upperbound) (strict) 529 530% udl(Type,X,Lin,Bound,Strict) 531% 532% Updates lower bound of dependent variable X with linear equation 533% Lin that had type Type and strictness Strict, to the new non-strict 534% bound Bound. 535 536udl(t_none,X,Lin,Bound,_Sold) :- 537 get_attr(X,itf,AttX), 538 arg(5,AttX,order(Ord)), 539 setarg(2,AttX,type(t_l(Bound))), 540 setarg(3,AttX,strictness(0)), 541 ( unconstrained(Lin,Uc,Kuc,Rest) 542 -> Ki is -1 rdiv Kuc, 543 add_linear_ff(Rest,Ki,[0,0,l(X* -1,Ord)],Ki,LinU), 544 get_attr(Uc,itf,AttU), 545 arg(5,AttU,order(OrdU)), 546 arg(6,AttU,class(Class)), 547 backsubst(Class,OrdU,LinU) 548 ; basis_add(X,_), 549 determine_active_inc(Lin), 550 reconsider(X) 551 ). 552udl(t_l(L),X,Lin,Bound,Sold) :- 553 ( Bound > L 554 -> Strict is Sold /\ 1, 555 get_attr(X,itf,Att), 556 setarg(2,Att,type(t_l(Bound))), 557 setarg(3,Att,strictness(Strict)), 558 reconsider_lower(X,Lin,Bound) 559 ; true 560 ). 561 562udl(t_u(U),X,Lin,Bound,_Sold) :- 563 ( Bound < U 564 -> get_attr(X,itf,Att), 565 setarg(2,Att,type(t_lu(Bound,U))), 566 reconsider_lower(X,Lin,Bound) % makes sure that Lin still satisfies lowerbound Bound 567 ; Bound =:= U, 568 solve_bound(Lin,Bound) % new bound is equal to upperbound: solve 569 ). 570udl(t_lu(L,U),X,Lin,Bound,Sold) :- 571 ( Bound > L 572 -> ( Bound < U 573 -> Strict is Sold /\ 1, 574 get_attr(X,itf,Att), 575 setarg(2,Att,type(t_lu(Bound,U))), 576 setarg(3,Att,strictness(Strict)), 577 reconsider_lower(X,Lin,Bound) 578 ; Bound =:= U, 579 Sold /\ 1 =:= 0, 580 solve_bound(Lin,Bound) 581 ) 582 ; true 583 ). 584 585% udls(Type,X,Lin,Bound,Strict) 586% 587% Updates lower bound of dependent variable X with linear equation 588% Lin that had type Type and strictness Strict, to the new strict 589% bound Bound. 590 591udls(t_none,X,Lin,Bound,_Sold) :- 592 get_attr(X,itf,AttX), 593 arg(5,AttX,order(Ord)), 594 setarg(2,AttX,type(t_l(Bound))), 595 setarg(3,AttX,strictness(2)), 596 ( unconstrained(Lin,Uc,Kuc,Rest) 597 -> % X = Lin => U = -1/K*Rest + 1/K*X with U an unconstrained variable 598 Ki is -1 rdiv Kuc, 599 add_linear_ff(Rest,Ki,[0,0,l(X* -1,Ord)],Ki,LinU), 600 get_attr(Uc,itf,AttU), 601 arg(5,AttU,order(OrdU)), 602 arg(6,AttU,class(Class)), 603 backsubst(Class,OrdU,LinU) 604 ; % no unconstrained variables: add X to basis and reconsider basis 605 basis_add(X,_), 606 determine_active_inc(Lin), 607 reconsider(X) 608 ). 609udls(t_l(L),X,Lin,Bound,Sold) :- 610 ( Bound < L 611 -> true 612 ; Bound > L 613 -> Strict is Sold \/ 2, 614 get_attr(X,itf,Att), 615 setarg(2,Att,type(t_l(Bound))), 616 setarg(3,Att,strictness(Strict)), 617 reconsider_lower(X,Lin,Bound) 618 ; % equal to lowerbound: check strictness 619 Strict is Sold \/ 2, 620 get_attr(X,itf,Att), 621 arg(3,Att,strictness(Strict)) 622 ). 623udls(t_u(U),X,Lin,Bound,Sold) :- 624 Bound < U, % smaller than upperbound: set new bound 625 Strict is Sold \/ 2, 626 get_attr(X,itf,Att), 627 setarg(2,Att,type(t_lu(Bound,U))), 628 setarg(3,Att,strictness(Strict)), 629 reconsider_lower(X,Lin,Bound). 630udls(t_lu(L,U),X,Lin,Bound,Sold) :- 631 ( Bound < L 632 -> true % smaller than lowerbound: keep 633 ; Bound > L 634 -> % larger than lowerbound: check upperbound and possibly use new and reconsider basis 635 Bound < U, 636 Strict is Sold \/ 2, 637 get_attr(X,itf,Att), 638 setarg(2,Att,type(t_lu(Bound,U))), 639 setarg(3,Att,strictness(Strict)), 640 reconsider_lower(X,Lin,Bound) 641 ; % equal to lowerbound: put new strictness 642 Strict is Sold \/ 2, 643 get_attr(X,itf,Att), 644 setarg(3,Att,strictness(Strict)) 645 ). 646 647% udu(Type,X,Lin,Bound,Strict) 648% 649% Updates upper bound of dependent variable X with linear equation 650% Lin that had type Type and strictness Strict, to the new non-strict 651% bound Bound. 652 653udu(t_none,X,Lin,Bound,_Sold) :- 654 get_attr(X,itf,AttX), 655 arg(5,AttX,order(Ord)), 656 setarg(2,AttX,type(t_u(Bound))), 657 setarg(3,AttX,strictness(0)), 658 ( unconstrained(Lin,Uc,Kuc,Rest) 659 -> % X = Lin => U = -1/K*Rest + 1/K*X with U an unconstrained variable 660 Ki is -1 rdiv Kuc, 661 add_linear_ff(Rest,Ki,[0,0,l(X* -1,Ord)],Ki,LinU), 662 get_attr(Uc,itf,AttU), 663 arg(5,AttU,order(OrdU)), 664 arg(6,AttU,class(Class)), 665 backsubst(Class,OrdU,LinU) 666 ; % no unconstrained variables: add X to basis and reconsider basis 667 basis_add(X,_), 668 determine_active_dec(Lin), % try to lower R 669 reconsider(X) 670 ). 671udu(t_u(U),X,Lin,Bound,Sold) :- 672 ( Bound < U 673 -> Strict is Sold /\ 2, 674 get_attr(X,itf,Att), 675 setarg(2,Att,type(t_u(Bound))), 676 setarg(3,Att,strictness(Strict)), 677 reconsider_upper(X,Lin,Bound) 678 ; true 679 ). 680udu(t_l(L),X,Lin,Bound,_Sold) :- 681 ( Bound > L 682 -> get_attr(X,itf,Att), 683 setarg(2,Att,type(t_lu(L,Bound))), 684 reconsider_upper(X,Lin,Bound) 685 ; Bound =:= L, 686 solve_bound(Lin,Bound) % equal to lowerbound: solve 687 ). 688udu(t_lu(L,U),X,Lin,Bound,Sold) :- 689 ( Bound < U 690 -> ( Bound > L 691 -> Strict is Sold /\ 2, 692 get_attr(X,itf,Att), 693 setarg(2,Att,type(t_lu(L,Bound))), 694 setarg(3,Att,strictness(Strict)), 695 reconsider_upper(X,Lin,Bound) 696 ; Bound =:= L, 697 Sold /\ 2 =:= 0, 698 solve_bound(Lin,Bound) 699 ) 700 ; true 701 ). 702 703% udus(Type,X,Lin,Bound,Strict) 704% 705% Updates upper bound of dependent variable X with linear equation 706% Lin that had type Type and strictness Strict, to the new strict 707% bound Bound. 708 709udus(t_none,X,Lin,Bound,_Sold) :- 710 get_attr(X,itf,AttX), 711 arg(5,AttX,order(Ord)), 712 setarg(2,AttX,type(t_u(Bound))), 713 setarg(3,AttX,strictness(1)), 714 ( unconstrained(Lin,Uc,Kuc,Rest) 715 -> % X = Lin => U = -1/K*Rest + 1/K*X with U an unconstrained variable 716 Ki is -1 rdiv Kuc, 717 add_linear_ff(Rest,Ki,[0,0,l(X* -1,Ord)],Ki,LinU), 718 get_attr(Uc,itf,AttU), 719 arg(5,AttU,order(OrdU)), 720 arg(6,AttU,class(Class)), 721 backsubst(Class,OrdU,LinU) 722 ; % no unconstrained variables: add X to basis and reconsider basis 723 basis_add(X,_), 724 determine_active_dec(Lin), 725 reconsider(X) 726 ). 727udus(t_u(U),X,Lin,Bound,Sold) :- 728 ( U < Bound 729 -> true % larger than upperbound: keep 730 ; Bound < U 731 -> % smaller than upperbound: update bound and reconsider basis 732 Strict is Sold \/ 1, 733 get_attr(X,itf,Att), 734 setarg(2,Att,type(t_u(Bound))), 735 setarg(3,Att,strictness(Strict)), 736 reconsider_upper(X,Lin,Bound) 737 ; % equal to upperbound: set new strictness 738 Strict is Sold \/ 1, 739 get_attr(X,itf,Att), 740 setarg(3,Att,strictness(Strict)) 741 ). 742udus(t_l(L),X,Lin,Bound,Sold) :- 743 L < Bound, % larger than lowerbound: update and reconsider basis 744 Strict is Sold \/ 1, 745 get_attr(X,itf,Att), 746 setarg(2,Att,type(t_lu(L,Bound))), 747 setarg(3,Att,strictness(Strict)), 748 reconsider_upper(X,Lin,Bound). 749udus(t_lu(L,U),X,Lin,Bound,Sold) :- 750 ( U < Bound 751 -> true % larger than upperbound: keep 752 ; Bound < U 753 -> % smaller than upperbound: check lowerbound, possibly update and reconsider basis 754 L < Bound, 755 Strict is Sold \/ 1, 756 get_attr(X,itf,Att), 757 setarg(2,Att,type(t_lu(L,Bound))), 758 setarg(3,Att,strictness(Strict)), 759 reconsider_upper(X,Lin,Bound) 760 ; % equal to upperbound: update strictness 761 Strict is Sold \/ 1, 762 get_attr(X,itf,Att), 763 setarg(3,Att,strictness(Strict)) 764 ). 765 766% uiu(Type,X,Lin,Bound,Strict) 767% 768% Updates upper bound of independent variable X with linear equation 769% Lin that had type Type and strictness Strict, to the new non-strict 770% bound Bound. 771 772uiu(t_none,X,_Lin,Bound,_) :- % X had no bounds 773 get_attr(X,itf,Att), 774 setarg(2,Att,type(t_u(Bound))), 775 setarg(3,Att,strictness(0)). 776uiu(t_u(U),X,_Lin,Bound,Sold) :- 777 ( U < Bound 778 -> true % larger than upperbound: keep 779 ; Bound < U 780 -> % smaller than upperbound: update. 781 Strict is Sold /\ 2, % update strictness: strictness of lowerbound is kept, 782 % strictness of upperbound is set to non-strict 783 get_attr(X,itf,Att), 784 setarg(2,Att,type(t_u(Bound))), 785 setarg(3,Att,strictness(Strict)) 786 ; true % equal to upperbound and nonstrict: keep 787 ). 788uiu(t_l(L),X,Lin,Bound,_Sold) :- 789 ( Bound > L 790 -> % Upperbound is larger than lowerbound: store new bound 791 get_attr(X,itf,Att), 792 setarg(2,Att,type(t_lu(L,Bound))) 793 ; Bound =:= L, 794 solve_bound(Lin,Bound) % Lowerbound was equal to new upperbound: solve 795 ). 796uiu(t_L(L),X,Lin,Bound,_Sold) :- 797 ( Bound > L 798 -> get_attr(X,itf,Att), 799 setarg(2,Att,type(t_Lu(L,Bound))) 800 ; Bound =:= L, 801 solve_bound(Lin,Bound) 802 ). 803uiu(t_lu(L,U),X,Lin,Bound,Sold) :- 804 ( Bound < U 805 -> ( Bound > L 806 -> Strict is Sold /\ 2, 807 get_attr(X,itf,Att), 808 setarg(2,Att,type(t_lu(L,Bound))), 809 setarg(3,Att,strictness(Strict)) 810 ; Bound =:= L, 811 Sold /\ 2 =:= 0, 812 solve_bound(Lin,Bound) 813 ) 814 ; true 815 ). 816uiu(t_Lu(L,U),X,Lin,Bound,Sold) :- 817 ( Bound < U 818 -> ( L < Bound 819 -> Strict is Sold /\ 2, 820 get_attr(X,itf,Att), 821 setarg(2,Att,type(t_Lu(L,Bound))), 822 setarg(3,Att,strictness(Strict)) 823 ; L =:= Bound, 824 Sold /\ 2 =:= 0, 825 solve_bound(Lin,Bound) 826 ) 827 ; true 828 ). 829uiu(t_U(U),X,_Lin,Bound,Sold) :- 830 ( Bound < U 831 -> Strict is Sold /\ 2, 832 ( get_attr(X,itf,Att), 833 arg(5,Att,order(OrdX)), 834 arg(6,Att,class(ClassX)), 835 lb(ClassX,OrdX,Vlb-Vb-Lb), 836 Bound =< Lb + U 837 -> get_attr(X,itf,Att2), % changed? 838 setarg(2,Att2,type(t_U(Bound))), 839 setarg(3,Att2,strictness(Strict)), 840 pivot_a(Vlb,X,Vb,t_u(Bound)), 841 reconsider(X) 842 ; get_attr(X,itf,Att), 843 arg(5,Att,order(OrdX)), 844 arg(6,Att,class(ClassX)), 845 setarg(2,Att,type(t_U(Bound))), 846 setarg(3,Att,strictness(Strict)), 847 Delta is Bound - U, 848 backsubst_delta(ClassX,OrdX,X,Delta) 849 ) 850 ; true 851 ). 852uiu(t_lU(L,U),X,Lin,Bound,Sold) :- 853 ( Bound < U 854 -> ( L < Bound 855 -> Strict is Sold /\ 2, 856 ( get_attr(X,itf,Att), 857 arg(5,Att,order(OrdX)), 858 arg(6,Att,class(ClassX)), 859 lb(ClassX,OrdX,Vlb-Vb-Lb), 860 Bound =< Lb + U 861 -> get_attr(X,itf,Att2), % changed? 862 setarg(2,Att2,type(t_lU(L,Bound))), 863 setarg(3,Att2,strictness(Strict)), 864 pivot_a(Vlb,X,Vb,t_lu(L,Bound)), 865 reconsider(X) 866 ; get_attr(X,itf,Att), 867 arg(5,Att,order(OrdX)), 868 arg(6,Att,class(ClassX)), 869 setarg(2,Att,type(t_lU(L,Bound))), 870 setarg(3,Att,strictness(Strict)), 871 Delta is Bound - U, 872 backsubst_delta(ClassX,OrdX,X,Delta) 873 ) 874 ; L =:= Bound, 875 Sold /\ 2 =:= 0, 876 solve_bound(Lin,Bound) 877 ) 878 ; true 879 ). 880 881% uius(Type,X,Lin,Bound,Strict) 882% 883% Updates upper bound of independent variable X with linear equation 884% Lin that had type Type and strictness Strict, to the new strict 885% bound Bound. (see also uiu/5) 886 887uius(t_none,X,_Lin,Bound,_Sold) :- 888 get_attr(X,itf,Att), 889 setarg(2,Att,type(t_u(Bound))), 890 setarg(3,Att,strictness(1)). 891uius(t_u(U),X,_Lin,Bound,Sold) :- 892 ( U < Bound 893 -> true 894 ; Bound < U 895 -> Strict is Sold \/ 1, 896 get_attr(X,itf,Att), 897 setarg(2,Att,type(t_u(Bound))), 898 setarg(3,Att,strictness(Strict)) 899 ; Strict is Sold \/ 1, 900 get_attr(X,itf,Att), 901 setarg(3,Att,strictness(Strict)) 902 ). 903uius(t_l(L),X,_Lin,Bound,Sold) :- 904 L < Bound, 905 Strict is Sold \/ 1, 906 get_attr(X,itf,Att), 907 setarg(2,Att,type(t_lu(L,Bound))), 908 setarg(3,Att,strictness(Strict)). 909uius(t_L(L),X,_Lin,Bound,Sold) :- 910 L < Bound, 911 Strict is Sold \/ 1, 912 get_attr(X,itf,Att), 913 setarg(2,Att,type(t_Lu(L,Bound))), 914 setarg(3,Att,strictness(Strict)). 915uius(t_lu(L,U),X,_Lin,Bound,Sold) :- 916 ( U < Bound 917 -> true 918 ; Bound < U 919 -> L < Bound, 920 Strict is Sold \/ 1, 921 get_attr(X,itf,Att), 922 setarg(2,Att,type(t_lu(L,Bound))), 923 setarg(3,Att,strictness(Strict)) 924 ; Strict is Sold \/ 1, 925 get_attr(X,itf,Att), 926 setarg(3,Att,strictness(Strict)) 927 ). 928uius(t_Lu(L,U),X,_Lin,Bound,Sold) :- 929 ( U < Bound 930 -> true 931 ; Bound < U 932 -> L < Bound, 933 Strict is Sold \/ 1, 934 get_attr(X,itf,Att), 935 setarg(2,Att,type(t_Lu(L,Bound))), 936 setarg(3,Att,strictness(Strict)) 937 ; Strict is Sold \/ 1, 938 get_attr(X,itf,Att), 939 setarg(3,Att,strictness(Strict)) 940 ). 941uius(t_U(U),X,_Lin,Bound,Sold) :- 942 ( U < Bound 943 -> true 944 ; Bound < U 945 -> Strict is Sold \/ 1, 946 ( get_attr(X,itf,Att), 947 arg(5,Att,order(OrdX)), 948 arg(6,Att,class(ClassX)), 949 lb(ClassX,OrdX,Vlb-Vb-Lb), 950 Bound =< Lb + U 951 -> get_attr(X,itf,Att2), % changed? 952 setarg(2,Att2,type(t_U(Bound))), 953 setarg(3,Att2,strictness(Strict)), 954 pivot_a(Vlb,X,Vb,t_u(Bound)), 955 reconsider(X) 956 ; get_attr(X,itf,Att), 957 arg(5,Att,order(OrdX)), 958 arg(6,Att,class(ClassX)), 959 setarg(2,Att,type(t_U(Bound))), 960 setarg(3,Att,strictness(Strict)), 961 Delta is Bound - U, 962 backsubst_delta(ClassX,OrdX,X,Delta) 963 ) 964 ; Strict is Sold \/ 1, 965 get_attr(X,itf,Att), 966 setarg(3,Att,strictness(Strict)) 967 ). 968uius(t_lU(L,U),X,_Lin,Bound,Sold) :- 969 ( U < Bound 970 -> true 971 ; Bound < U 972 -> L < Bound, 973 Strict is Sold \/ 1, 974 ( get_attr(X,itf,Att), 975 arg(5,Att,order(OrdX)), 976 arg(6,Att,class(ClassX)), 977 lb(ClassX,OrdX,Vlb-Vb-Lb), 978 Bound =< Lb + U 979 -> get_attr(X,itf,Att2), % changed? 980 setarg(2,Att2,type(t_lU(L,Bound))), 981 setarg(3,Att2,strictness(Strict)), 982 pivot_a(Vlb,X,Vb,t_lu(L,Bound)), 983 reconsider(X) 984 ; get_attr(X,itf,Att), 985 arg(5,Att,order(OrdX)), 986 arg(6,Att,class(ClassX)), 987 setarg(2,Att,type(t_lU(L,Bound))), 988 setarg(3,Att,strictness(Strict)), 989 Delta is Bound - U, 990 backsubst_delta(ClassX,OrdX,X,Delta) 991 ) 992 ; Strict is Sold \/ 1, 993 get_attr(X,itf,Att), 994 setarg(3,Att,strictness(Strict)) 995 ). 996 997% uil(Type,X,Lin,Bound,Strict) 998% 999% Updates lower bound of independent variable X with linear equation 1000% Lin that had type Type and strictness Strict, to the new non-strict 1001% bound Bound. (see also uiu/5) 1002 1003 1004uil(t_none,X,_Lin,Bound,_Sold) :- 1005 get_attr(X,itf,Att), 1006 setarg(2,Att,type(t_l(Bound))), 1007 setarg(3,Att,strictness(0)). 1008uil(t_l(L),X,_Lin,Bound,Sold) :- 1009 ( Bound > L 1010 -> Strict is Sold /\ 1, 1011 get_attr(X,itf,Att), 1012 setarg(2,Att,type(t_l(Bound))), 1013 setarg(3,Att,strictness(Strict)) 1014 ; true 1015 ). 1016uil(t_u(U),X,Lin,Bound,_Sold) :- 1017 ( Bound < U 1018 -> get_attr(X,itf,Att), 1019 setarg(2,Att,type(t_lu(Bound,U))) 1020 ; Bound =:= U, 1021 solve_bound(Lin,Bound) 1022 ). 1023uil(t_U(U),X,Lin,Bound,_Sold) :- 1024 ( Bound < U 1025 -> get_attr(X,itf,Att), 1026 setarg(2,Att,type(t_lU(Bound,U))) 1027 ; Bound =:= U, 1028 solve_bound(Lin,Bound) 1029 ). 1030uil(t_lu(L,U),X,Lin,Bound,Sold) :- 1031 ( Bound > L 1032 -> ( Bound < U 1033 -> Strict is Sold /\ 1, 1034 get_attr(X,itf,Att), 1035 setarg(2,Att,type(t_lu(Bound,U))), 1036 setarg(3,Att,strictness(Strict)) 1037 ; Bound =:= U, 1038 Sold /\ 1 =:= 0, 1039 solve_bound(Lin,Bound) 1040 ) 1041 ; true 1042 ). 1043uil(t_lU(L,U),X,Lin,Bound,Sold) :- 1044 ( Bound > L 1045 -> ( Bound < U 1046 -> Strict is Sold /\ 1, 1047 get_attr(X,itf,Att), 1048 setarg(2,Att,type(t_lU(Bound,U))), 1049 setarg(3,Att,strictness(Strict)) 1050 ; Bound =:= U, 1051 Sold /\ 1 =:= 0, 1052 solve_bound(Lin,Bound) 1053 ) 1054 ; true 1055 ). 1056uil(t_L(L),X,_Lin,Bound,Sold) :- 1057 ( Bound > L 1058 -> Strict is Sold /\ 1, 1059 ( get_attr(X,itf,Att), 1060 arg(5,Att,order(OrdX)), 1061 arg(6,Att,class(ClassX)), 1062 ub(ClassX,OrdX,Vub-Vb-Ub), 1063 Bound >= Ub + L 1064 -> get_attr(X,itf,Att2), % changed? 1065 setarg(2,Att2,type(t_L(Bound))), 1066 setarg(3,Att2,strictness(Strict)), 1067 pivot_a(Vub,X,Vb,t_l(Bound)), 1068 reconsider(X) 1069 ; get_attr(X,itf,Att), 1070 arg(5,Att,order(OrdX)), 1071 arg(6,Att,class(ClassX)), 1072 setarg(2,Att,type(t_L(Bound))), 1073 setarg(3,Att,strictness(Strict)), 1074 Delta is Bound - L, 1075 backsubst_delta(ClassX,OrdX,X,Delta) 1076 ) 1077 ; true 1078 ). 1079uil(t_Lu(L,U),X,Lin,Bound,Sold) :- 1080 ( Bound > L 1081 -> ( Bound < U 1082 -> Strict is Sold /\ 1, 1083 ( get_attr(X,itf,Att), 1084 arg(5,Att,order(OrdX)), 1085 arg(6,Att,class(ClassX)), 1086 ub(ClassX,OrdX,Vub-Vb-Ub), 1087 Bound >= Ub + L 1088 -> get_attr(X,itf,Att2), % changed? 1089 setarg(2,Att2,t_Lu(Bound,U)), 1090 setarg(3,Att2,strictness(Strict)), 1091 pivot_a(Vub,X,Vb,t_lu(Bound,U)), 1092 reconsider(X) 1093 ; get_attr(X,itf,Att), 1094 arg(5,Att,order(OrdX)), 1095 arg(6,Att,class(ClassX)), 1096 setarg(2,Att,type(t_Lu(Bound,U))), 1097 setarg(3,Att,strictness(Strict)), 1098 Delta is Bound - L, 1099 backsubst_delta(ClassX,OrdX,X,Delta) 1100 ) 1101 ; Bound =:= U, 1102 Sold /\ 1 =:= 0, 1103 solve_bound(Lin,Bound) 1104 ) 1105 ; true 1106 ). 1107 1108% uils(Type,X,Lin,Bound,Strict) 1109% 1110% Updates lower bound of independent variable X with linear equation 1111% Lin that had type Type and strictness Strict, to the new strict 1112% bound Bound. (see also uiu/5) 1113 1114uils(t_none,X,_Lin,Bound,_Sold) :- 1115 get_attr(X,itf,Att), 1116 setarg(2,Att,type(t_l(Bound))), 1117 setarg(3,Att,strictness(2)). 1118uils(t_l(L),X,_Lin,Bound,Sold) :- 1119 ( Bound < L 1120 -> true 1121 ; Bound > L 1122 -> Strict is Sold \/ 2, 1123 get_attr(X,itf,Att), 1124 setarg(2,Att,type(t_l(Bound))), 1125 setarg(3,Att,strictness(Strict)) 1126 ; Strict is Sold \/ 2, 1127 get_attr(X,itf,Att), 1128 setarg(3,Att,strictness(Strict)) 1129 ). 1130uils(t_u(U),X,_Lin,Bound,Sold) :- 1131 Bound < U, 1132 Strict is Sold \/ 2, 1133 get_attr(X,itf,Att), 1134 setarg(2,Att,type(t_lu(Bound,U))), 1135 setarg(3,Att,strictness(Strict)). 1136uils(t_U(U),X,_Lin,Bound,Sold) :- 1137 Bound < U, 1138 Strict is Sold \/ 2, 1139 get_attr(X,itf,Att), 1140 setarg(2,Att,type(t_lU(Bound,U))), 1141 setarg(3,Att,strictness(Strict)). 1142uils(t_lu(L,U),X,_Lin,Bound,Sold) :- 1143 ( Bound < L 1144 -> true 1145 ; Bound > L 1146 -> Bound < U, 1147 Strict is Sold \/ 2, 1148 get_attr(X,itf,Att), 1149 setarg(2,Att,type(t_lu(Bound,U))), 1150 setarg(3,Att,strictness(Strict)) 1151 ; Strict is Sold \/ 2, 1152 get_attr(X,itf,Att), 1153 setarg(3,Att,strictness(Strict)) 1154 ). 1155uils(t_lU(L,U),X,_Lin,Bound,Sold) :- 1156 ( Bound < L 1157 -> true 1158 ; Bound > L 1159 -> Bound < U, 1160 Strict is Sold \/ 2, 1161 get_attr(X,itf,Att), 1162 setarg(2,Att,type(t_lU(Bound,U))), 1163 setarg(3,Att,strictness(Strict)) 1164 ; Strict is Sold \/ 2, 1165 get_attr(X,itf,Att), 1166 setarg(3,Att,strictness(Strict)) 1167 ). 1168uils(t_L(L),X,_Lin,Bound,Sold) :- 1169 ( Bound < L 1170 -> true 1171 ; Bound > L 1172 -> Strict is Sold \/ 2, 1173 ( get_attr(X,itf,Att), 1174 arg(5,Att,order(OrdX)), 1175 arg(6,Att,class(ClassX)), 1176 ub(ClassX,OrdX,Vub-Vb-Ub), 1177 Bound >= Ub + L 1178 -> get_attr(X,itf,Att2), % changed? 1179 setarg(2,Att2,type(t_L(Bound))), 1180 setarg(3,Att2,strictness(Strict)), 1181 pivot_a(Vub,X,Vb,t_l(Bound)), 1182 reconsider(X) 1183 ; get_attr(X,itf,Att), 1184 arg(5,Att,order(OrdX)), 1185 arg(6,Att,class(ClassX)), 1186 setarg(2,Att,type(t_L(Bound))), 1187 setarg(3,Att,strictness(Strict)), 1188 Delta is Bound - L, 1189 backsubst_delta(ClassX,OrdX,X,Delta) 1190 ) 1191 ; Strict is Sold \/ 2, 1192 get_attr(X,itf,Att), 1193 setarg(3,Att,strictness(Strict)) 1194 ). 1195uils(t_Lu(L,U),X,_Lin,Bound,Sold) :- 1196 ( Bound < L 1197 -> true 1198 ; Bound > L 1199 -> Bound < U, 1200 Strict is Sold \/ 2, 1201 ( get_attr(X,itf,Att), 1202 arg(5,Att,order(OrdX)), 1203 arg(6,Att,class(ClassX)), 1204 ub(ClassX,OrdX,Vub-Vb-Ub), 1205 Bound >= Ub + L 1206 -> get_attr(X,itf,Att2), % changed? 1207 setarg(2,Att2,type(t_Lu(Bound,U))), 1208 setarg(3,Att2,strictness(Strict)), 1209 pivot_a(Vub,X,Vb,t_lu(Bound,U)), 1210 reconsider(X) 1211 ; get_attr(X,itf,Att), 1212 arg(5,Att,order(OrdX)), 1213 arg(6,Att,class(ClassX)), 1214 setarg(2,Att,type(t_Lu(Bound,U))), 1215 setarg(3,Att,strictness(Strict)), 1216 Delta is Bound - L, 1217 backsubst_delta(ClassX,OrdX,X,Delta) 1218 ) 1219 ; Strict is Sold \/ 2, 1220 get_attr(X,itf,Att), 1221 setarg(3,Att,strictness(Strict)) 1222 ). 1223 1224% reconsider_upper(X,Lin,U) 1225% 1226% Checks if the upperbound of X which is U, satisfies the bounds 1227% of the variables in Lin: let R be the sum of all the bounds on 1228% the variables in Lin, and I be the inhomogene part of Lin, then 1229% upperbound U should be larger than R + I (R may contain 1230% lowerbounds). 1231% See also rcb/3 in bv.pl 1232 1233% The code could probably be further specialized to only 1234% decrement/increment in case a variable takes a value equal to a 1235% _strict_ upper/lower bound. Also note that this is only for the 1236% CLP(Q) version. The CLP(R) fuzzy arithmetic makes it useless to 1237% really distinguish between strict and non-strict inequalities. 1238 1239reconsider_upper(X,[I,R|H],U) :- 1240 R + I >= U, % violation 1241 !, 1242 dec_step(H,Status), % we want to decrement R 1243 rcbl_status(Status,X,[],Binds,[],u(U)), 1244 export_binding(Binds). 1245reconsider_upper( _, _, _). 1246 1247% reconsider_lower(X,Lin,L) 1248% 1249% Checks if the lowerbound of X which is L, satisfies the bounds 1250% of the variables in Lin: let R be the sum of all the bounds on 1251% the variables in Lin, and I be the inhomogene part of Lin, then 1252% lowerbound L should be smaller than R + I (R may contain 1253% upperbounds). 1254% See also rcb/3 in bv.pl 1255 1256reconsider_lower(X,[I,R|H],L) :- 1257 R + I =< L, % violation 1258 !, 1259 inc_step(H,Status), % we want to increment R 1260 rcbl_status(Status,X,[],Binds,[],l(L)), 1261 export_binding(Binds). 1262reconsider_lower(_,_,_). 1263 1264% 1265% lin is dereferenced 1266% 1267 1268% solve_bound(Lin,Bound) 1269% 1270% Solves the linear equation Lin - Bound = 0 1271% Lin is the linear equation of X, a variable whose bounds have narrowed to value Bound 1272 1273solve_bound(Lin,Bound) :- 1274 Bound =:= 0, 1275 !, 1276 solve(Lin). 1277solve_bound(Lin,Bound) :- 1278 Nb is -Bound, 1279 normalize_scalar(Nb,Nbs), 1280 add_linear_11(Nbs,Lin,Eq), 1281 solve(Eq). 1282