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