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
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) :- 71 ineq_one(Strictness, CLP, X, K, I).
72ineq_cases([_|_], CLP, _, Lin, Strictness, _, _) :-
73 deref(CLP, Lin, Lind), 74 Lind = [Inhom,_|Hom],
75 ineq_more(Hom, CLP, Inhom, Lind, Strictness).
76
80
81ineq_ground(strict, CLP, I) :- compare_d(CLP, <, I, 0).
82ineq_ground(nonstrict, CLP, I) :- compare_d(CLP, =<, I, 0).
83
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) 92 ; div_d(CLP, I, K, Inhom),
93 ineq_one_s_p_i(CLP, X, Inhom) 94 )
95 ; ( compare_d(CLP, =, 0, I)
96 -> ineq_one_s_n_0(CLP, X) 97 ; div_d(CLP, -I, K, Inhom),
98 ineq_one_s_n_i(CLP, X, Inhom) 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) 105 ; div_d(CLP, I, K, Inhom),
106 ineq_one_n_p_i(CLP, X, Inhom) 107 )
108 ; ( compare_d(CLP, =, 0, I)
109 -> ineq_one_n_n_0(CLP, X) 110 ; div_d(CLP, -I, K, Inhom),
111 ineq_one_n_n_i(CLP, X, Inhom) 112 )
113 ).
114
116
120
121ineq_one_s_p_0(CLP, X) :-
122 get_attr(X,clpcd_itf,Att),
123 arg(4,Att,lin([Ix,_|OrdX])),
124 !, 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) :- 131 var_intern(CLP,t_u(0),X,1). 132
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). 148
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). 165
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). 180
184
185ineq_one_old_s_p_0([], CLP, _, Ix) :- compare_d(CLP, <, Ix, 0). 186ineq_one_old_s_p_0([l(Y*Ky,_)|Tail], CLP, X, Ix) :-
187 ( Tail = [] 188 -> div_d(CLP, -Ix, Ky, Bound),
189 update_indep(strict, CLP, Y, Ky, Bound) 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) 196 ).
197
201
202ineq_one_old_s_n_0([], CLP, _, Ix) :- compare_d(CLP, >, Ix, 0). 203ineq_one_old_s_n_0([l(Y*Ky,_)|Tail], CLP, X, Ix) :-
204 ( Tail = [] 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) 214 ).
215
219
220ineq_one_old_s_p_i([], CLP, I, _, Ix) :- compare_d(CLP, <, I, -Ix). 221ineq_one_old_s_p_i([l(Y*Ky,_)|Tail], CLP, I, X, Ix) :-
222 ( Tail = [] 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) 232 ).
233
237
238ineq_one_old_s_n_i([], CLP, I, _, Ix) :- compare_d(CLP, <, I, Ix). 239ineq_one_old_s_n_i([l(Y*Ky,_)|Tail], CLP, I, X, Ix) :-
240 ( Tail = [] 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) 250 ).
251
253
257
258ineq_one_n_p_0(CLP, X) :-
259 get_attr(X,clpcd_itf,Att),
260 arg(4,Att,lin([Ix,_|OrdX])),
261 !, 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) :- 268 var_intern(CLP,t_u(0),X,0). 269
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). 285
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). 302
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). 318
322
323ineq_one_old_n_p_0([], CLP, _, Ix) :- compare_d(CLP, =<, Ix, 0). 324ineq_one_old_n_p_0([l(Y*Ky,_)|Tail], CLP, X, Ix) :-
325 ( Tail = [] 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) 334 ).
335
339
340ineq_one_old_n_n_0([], CLP, _, Ix) :- compare_d(CLP, >=, Ix, 0). 341ineq_one_old_n_n_0([l(Y*Ky,_)|Tail], CLP, X, Ix) :-
342 ( Tail = [] 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) 352 ).
353
357
358ineq_one_old_n_p_i([], CLP, I, _, Ix) :- compare_d(CLP, =<, I, -Ix). 359ineq_one_old_n_p_i([l(Y*Ky,_)|Tail], CLP, I, X, Ix) :-
360 ( Tail = [] 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) 370 ).
371
375
376ineq_one_old_n_n_i([], CLP, I, _, Ix) :- compare_d(CLP, =<, I, Ix). 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
391
395
396ineq_more([], CLP, I, _, Strictness) :- ineq_ground(Strictness,CLP,I). 397ineq_more([l(X*K,_)|Tail], CLP, Id, Lind, Strictness) :-
398 ( Tail = []
399 -> 400 401 get_or_add_class(X,_), 402 div_d(CLP, -Id, K, Bound),
403 update_indep(Strictness, CLP, X, K, Bound) 404 ; Tail = [_|_]
405 -> ineq_more(Strictness, CLP, Lind)
406 ).
407
411
412ineq_more(strict, CLP, Lind) :-
413 ( unconstrained(CLP,Lind,U,K,Rest)
414 -> 415 416 var_intern(CLP,t_l(0),S,2), 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), 421 LinU = [_,_|Hu],
422 get_or_add_class(U,Class),
423 same_class(Hu,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) 428 ; var_with_def_intern(t_u(0), CLP, S, Lind, 1), 429 basis_add(S,_), 430 determine_active_dec(CLP, Lind), 431 reconsider(CLP, S) 432 ).
433ineq_more(nonstrict, CLP, Lind) :-
434 ( unconstrained(CLP,Lind,U,K,Rest)
435 -> 436 437 var_intern(CLP,t_l(0),S,0), 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), 442 LinU = [_,_|Hu],
443 get_or_add_class(U,Class),
444 same_class(Hu,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) 449 ; 450 var_with_def_intern(t_u(0), CLP, S, Lind, 0), 451 basis_add(S,_), 452 determine_active_dec(CLP, Lind),
453 reconsider(CLP, S)
454 ).
455
456
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) 469 ; uius(Type, CLP, X, Lin, Bound, Old) 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) 478 ; uiu(Type, CLP, X, Lin, Bound, Old) 479 ).
480
481
483
504
508
510
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 -> 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 ; 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 -> 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) 543 ; true 544 ).
545
546udl(t_u(U), CLP, X, Lin, Bound, _Sold) :-
547 ( compare_d(CLP, <, Bound, U)
548 -> 549 get_attr(X,clpcd_itf,Att),
550 setarg(2,Att,type(t_lu(Bound,U))),
551 reconsider_lower(CLP, X, Lin, Bound) 552 ; compare_d(CLP, =, Bound, U),
553 solve_bound(CLP, Lin, Bound) 554 ).
555udl(t_lu(L,U), CLP, X, Lin, Bound, Sold) :-
556 ( compare_d(CLP, >, Bound, L)
557 -> 558 ( compare_d(CLP, <, Bound, U)
559 -> 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 567 Sold /\ 1 =:= 0,
568 solve_bound(CLP, Lin, Bound)
569 )
570 ; true 571 ).
572
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 -> 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 ; 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 600 ; compare_d(CLP, >, Bound, L)
601 -> 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 ; 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), 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 622 ; compare_d(CLP, >, Bound, L)
623 -> 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 ; 631 Strict is Sold \/ 2,
632 get_attr(X,clpcd_itf,Att),
633 setarg(3,Att,strictness(Strict))
634 ).
635
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 -> 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 ; 656 basis_add(X,_),
657 determine_active_dec(CLP, Lin), 658 reconsider(CLP, X)
659 ).
660udu(t_u(U), CLP, X, Lin, Bound, Sold) :-
661 ( compare_d(CLP, <, Bound, U)
662 -> 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 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 -> 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) 679 ).
680udu(t_lu(L,U), CLP, X, Lin, Bound, Sold) :-
681 ( compare_d(CLP, <, Bound, U)
682 -> 683 ( compare_d(CLP, >, Bound, L)
684 -> 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 692 Sold /\ 2 =:= 0,
693 solve_bound(CLP, Lin, Bound)
694 )
695 ; true 696 ).
697
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 -> 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 ; 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 725 ; compare_d(CLP, <, Bound, U)
726 -> 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 ; 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), 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 747 ; compare_d(CLP, <, Bound, U)
748 -> 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 ; 756 Strict is Sold \/ 1,
757 get_attr(X,clpcd_itf,Att),
758 setarg(3,Att,strictness(Strict))
759 ).
760
766
767uiu(t_none, _, X, _Lin, Bound, _) :- 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 774 ; compare_d(CLP, <, Bound, U)
775 -> 776 Strict is Sold /\ 2, 777 778 get_attr(X,clpcd_itf,Att),
779 setarg(2,Att,type(t_u(Bound))),
780 setarg(3,Att,strictness(Strict))
781 ; true 782 ).
783uiu(t_l(L), CLP, X, Lin, Bound, _Sold) :-
784 ( compare_d(CLP, >, Bound, L)
785 -> 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) 790 ).
791uiu(t_L(L), CLP, X, Lin, Bound, _Sold) :-
792 ( compare_d(CLP, >, Bound, L)
793 -> 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) 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 ; 807 compare_d(CLP, =, Bound, L),
808 Sold /\ 2 =:= 0, 809 solve_bound(CLP, Lin, Bound)
810 )
811 ; true 812 ).
813uiu(t_Lu(L,U), CLP, X, Lin, Bound, Sold) :- 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), 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 848 ).
849uiu(t_lU(L,U), CLP, X, Lin, Bound, Sold) :-
850 ( compare_d(CLP, <, Bound, U)
851 -> ( compare_d(CLP, <, L, Bound)
852 -> 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), 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 ; 873 compare_d(CLP, =, L, Bound),
874 Sold /\ 2 =:= 0,
875 solve_bound(CLP, Lin, Bound)
876 )
877 ; true 878 879 ).
880
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), 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), 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
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), 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), 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
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), 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), 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
1232
1233reconsider_upper(CLP, X, [I,R|H], U) :-
1234 compare_d(CLP, >=, R + I, U), 1235 !,
1236 dec_step(H, CLP, Status), 1237 rcbl_status(Status, CLP, X, [], Binds, [], u(U)),
1238 export_binding(Binds).
1239reconsider_upper(_, _, _, _).
1240
1249
1250reconsider_lower(CLP, X, [I,R|H], L) :-
1251 compare_d(CLP, =<, R + I, L), 1252 !,
1253 inc_step(H, CLP, Status), 1254 rcbl_status(Status, CLP, X, [], Binds, [], l(L)),
1255 export_binding(Binds).
1256reconsider_lower(_, _, _, _).
1257
1261
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
1280
1281'solve_<'(CLP, Nf) :-
1282 split(Nf,H,I),
1283 ineq(H, CLP, I, Nf, strict).
1284
1288
1289'solve_=<'(CLP, Nf) :-
1290 split(Nf,H,I),
1291 ineq(H, CLP, I, Nf, nonstrict)