39
40:- module(bv_q,
41 [
42 allvars/2,
43 backsubst/3,
44 backsubst_delta/4,
45 basis_add/2,
46 dec_step/2,
47 deref/2,
48 deref_var/2,
49 detach_bounds/1,
50 detach_bounds_vlv/5,
51 determine_active_dec/1,
52 determine_active_inc/1,
53 dump_var/6,
54 dump_nz/5,
55 export_binding/1,
56 get_or_add_class/2,
57 inc_step/2,
58 intro_at/3,
59 iterate_dec/2,
60 lb/3,
61 pivot_a/4,
62 pivot/5,
63 rcbl_status/6,
64 reconsider/1,
65 same_class/2,
66 solve/1,
67 solve_ord_x/3,
68 ub/3,
69 unconstrained/4,
70 var_intern/2,
71 var_intern/3,
72 var_with_def_assign/2,
73 var_with_def_intern/4,
74 maximize/1,
75 minimize/1,
76 sup/2,
77 sup/4,
78 inf/2,
79 inf/4,
80 'solve_<'/1,
81 'solve_=<'/1,
82 'solve_=\\='/1,
83 log_deref/4
84 ]). 85:- use_module(store_q,
86 [
87 add_linear_11/3,
88 add_linear_f1/4,
89 add_linear_ff/5,
90 delete_factor/4,
91 indep/2,
92 isolate/3,
93 nf2sum/3,
94 nf_rhs_x/4,
95 nf_substitute/4,
96 normalize_scalar/2,
97 mult_hom/3,
98 mult_linear_factor/3
99 ]). 100:- use_module('../clpqr/class',
101 [
102 class_allvars/2,
103 class_basis/2,
104 class_basis_add/3,
105 class_basis_drop/2,
106 class_basis_pivot/3,
107 class_new/5
108 ]). 109:- use_module(ineq_q,
110 [
111 ineq/4
112 ]). 113:- use_module(nf_q,
114 [
115 {}/1,
116 split/3,
117 wait_linear/3
118 ]). 119:- use_module(bb_q,
120 [
121 vertex_value/2
122 ]). 123:- use_module(library(ordsets),
124 [
125 ord_add_element/3
126 ]). 127
135
146
149
155
156deref(Lin,Lind) :-
157 split(Lin,H,I),
158 normalize_scalar(I,Nonvar),
159 length(H,Len),
160 log_deref(Len,H,[],Restd),
161 add_linear_11(Nonvar,Restd,Lind).
162
169
170log_deref(0,Vs,Vs,Lin) :-
171 !,
172 Lin = [0,0].
173log_deref(1,[v(K,[X^1])|Vs],Vs,Lin) :-
174 !,
175 deref_var(X,Lx),
176 mult_linear_factor(Lx,K,Lin).
177log_deref(2,[v(Kx,[X^1]),v(Ky,[Y^1])|Vs],Vs,Lin) :-
178 !,
179 deref_var(X,Lx),
180 deref_var(Y,Ly),
181 add_linear_ff(Lx,Kx,Ly,Ky,Lin).
182log_deref(N,V0,V2,Lin) :-
183 P is N >> 1,
184 Q is N - P,
185 log_deref(P,V0,V1,Lp),
186 log_deref(Q,V1,V2,Lq),
187 add_linear_11(Lp,Lq,Lin).
188
193
194deref_var(X,Lin) :-
195 ( get_attr(X,clpqr_itf,Att)
196 -> ( \+ arg(1,Att,clpq)
197 -> throw(error(permission_error('mix CLP(Q) variables with',
198 'CLP(R) variables:',X),context(_)))
199 ; arg(4,Att,lin(Lin))
200 -> true
201 ; setarg(2,Att,type(t_none)),
202 setarg(3,Att,strictness(0)),
203 Lin = [0,0,l(X*1,Ord)],
204 setarg(4,Att,lin(Lin)),
205 setarg(5,Att,order(Ord))
206 )
207 ; Lin = [0,0,l(X*1,Ord)],
208 put_attr(X,clpqr_itf,t(clpq,type(t_none),strictness(0),
209 lin(Lin),order(Ord),n,n,n,n,n,n))
210 ).
211
215
216var_with_def_assign(Var,Lin) :-
217 Lin = [I,_|Hom],
218 ( Hom = []
219 -> 220 Var = I
221 ; Hom = [l(V*K,_)|Cs]
222 -> ( Cs = [],
223 K =:= 1,
224 I =:= 0
225 -> 226 Var = V
227 ; 228 var_with_def_intern(t_none,Var,Lin,0)
229 )
230 ).
231
237
238var_with_def_intern(Type,Var,Lin,Strict) :-
239 put_attr(Var,clpqr_itf,t(clpq,type(Type),strictness(Strict),lin(Lin),
240 order(_),n,n,n,n,n,n)), 241 Lin = [_,_|Hom],
242 get_or_add_class(Var,Class),
243 same_class(Hom,Class).
244
248
249var_intern(Type,Var,Strict) :-
250 put_attr(Var,clpqr_itf,t(clpq,type(Type),strictness(Strict),
251 lin([0,0,l(Var*1,Ord)]),order(Ord),n,n,n,n,n,n)),
252 get_or_add_class(Var,_Class).
253
257
258var_intern(Var,Class) :- 259 get_attr(Var,clpqr_itf,Att),
260 arg(2,Att,type(_)),
261 arg(4,Att,lin(_)),
262 !,
263 get_or_add_class(Var,Class).
264var_intern(Var,Class) :-
265 put_attr(Var,clpqr_itf,t(clpq,type(t_none),strictness(0),
266 lin([0,0,l(Var*1,Ord)]),order(Ord),n,n,n,n,n,n)),
267 get_or_add_class(Var,Class).
268
270
274
275export_binding([]).
276export_binding([X-Y|Gs]) :-
277 Y = X,
278 export_binding(Gs).
279
283
284'solve_='(Nf) :-
285 deref(Nf,Nfd), 286 solve(Nfd).
287
291
292'solve_=\\='(Nf) :-
293 deref(Nf,Lind), 294 Lind = [Inhom,_|Hom],
295 ( Hom = []
296 -> Inhom =\= 0
297 ; 298 var_with_def_intern(t_none,Nz,Lind,0),
299 300 get_attr(Nz,clpqr_itf,Att),
301 setarg(8,Att,nonzero)
302 ).
303
307
308'solve_<'(Nf) :-
309 split(Nf,H,I),
310 ineq(H,I,Nf,strict).
311
315
316'solve_=<'(Nf) :-
317 split(Nf,H,I),
318 ineq(H,I,Nf,nonstrict).
319
320maximize(Term) :-
321 minimize(-Term).
322
348minimize(Term) :-
349 wait_linear(Term,Nf,minimize_lin(Nf)).
350
355
356minimize_lin(Lin) :-
357 deref(Lin,Lind),
358 var_with_def_intern(t_none,Dep,Lind,0),
359 determine_active_dec(Lind),
360 iterate_dec(Dep,Inf),
361 { Dep =:= Inf }.
362
363sup(Expression,Sup) :-
364 sup(Expression,Sup,[],[]).
365
366sup(Expression,Sup,Vector,Vertex) :-
367 inf(-Expression,-Sup,Vector,Vertex).
368
369inf(Expression,Inf) :-
370 inf(Expression,Inf,[],[]).
371
372inf(Expression,Inf,Vector,Vertex) :-
373 374 375 wait_linear(Expression,Nf,inf_lin(Nf,Inf,Vector,Vertex)).
376
377inf_lin(Lin,_,Vector,_) :-
378 deref(Lin,Lind),
379 var_with_def_intern(t_none,Dep,Lind,0), 380 determine_active_dec(Lind), 381 iterate_dec(Dep,Inf),
382 vertex_value(Vector,Values),
383 nb_setval(inf,[Inf|Values]),
384 fail.
385inf_lin(_,Infimum,_,Vertex) :-
386 nb_current(inf,L),
387 nb_delete(inf),
388 assign([Infimum|Vertex],L).
389
395
396assign([],[]).
397assign([X|Xs],[Y|Ys]) :-
398 {X =:= Y}, 399 assign(Xs,Ys).
400
420
421
427
428iterate_dec(OptVar,Opt) :-
429 get_attr(OptVar,clpqr_itf,Att),
430 arg(4,Att,lin([I,R|H])),
431 dec_step(H,Status),
432 ( Status = applied
433 -> iterate_dec(OptVar,Opt)
434 ; Status = optimum,
435 Opt is R + I
436 ).
437
443
444iterate_inc(OptVar,Opt) :-
445 get_attr(OptVar,clpqr_itf,Att),
446 arg(4,Att,lin([I,R|H])),
447 inc_step(H,Status),
448 ( Status = applied
449 -> iterate_inc(OptVar,Opt)
450 ; Status = optimum,
451 Opt is R + I
452 ).
453
460
461
462dec_step_cont([],optimum,Cont,Cont).
463dec_step_cont([l(V*K,OrdV)|Vs],Status,ContIn,ContOut) :-
464 get_attr(V,clpqr_itf,Att),
465 arg(2,Att,type(W)),
466 arg(6,Att,class(Class)),
467 ( dec_step_2_cont(W,l(V*K,OrdV),Class,Status,ContIn,ContOut)
468 -> true
469 ; dec_step_cont(Vs,Status,ContIn,ContOut)
470 ).
471
472inc_step_cont([],optimum,Cont,Cont).
473inc_step_cont([l(V*K,OrdV)|Vs],Status,ContIn,ContOut) :-
474 get_attr(V,clpqr_itf,Att),
475 arg(2,Att,type(W)),
476 arg(6,Att,class(Class)),
477 ( inc_step_2_cont(W,l(V*K,OrdV),Class,Status,ContIn,ContOut)
478 -> true
479 ; inc_step_cont(Vs,Status,ContIn,ContOut)
480 ).
481
482dec_step_2_cont(t_U(U),l(V*K,OrdV),Class,Status,ContIn,ContOut) :-
483 K > 0,
484 ( lb(Class,OrdV,Vub-Vb-_)
485 -> 486 Status = applied,
487 pivot_a(Vub,V,Vb,t_u(U)),
488 replace_in_cont(ContIn,Vub,V,ContOut)
489 ; Status = unlimited(V,t_u(U)),
490 ContIn = ContOut
491 ).
492dec_step_2_cont(t_lU(L,U),l(V*K,OrdV),Class,applied,ContIn,ContOut) :-
493 K > 0,
494 Init is L - U,
495 class_basis(Class,Deps),
496 lb(Deps,OrdV,V-t_Lu(L,U)-Init,Vub-Vb-_),
497 pivot_b(Vub,V,Vb,t_lu(L,U)),
498 replace_in_cont(ContIn,Vub,V,ContOut).
499dec_step_2_cont(t_L(L),l(V*K,OrdV),Class,Status,ContIn,ContOut) :-
500 K < 0,
501 ( ub(Class,OrdV,Vub-Vb-_)
502 -> Status = applied,
503 pivot_a(Vub,V,Vb,t_l(L)),
504 replace_in_cont(ContIn,Vub,V,ContOut)
505 ; Status = unlimited(V,t_l(L)),
506 ContIn = ContOut
507 ).
508dec_step_2_cont(t_Lu(L,U),l(V*K,OrdV),Class,applied,ContIn,ContOut) :-
509 K < 0,
510 Init is U - L,
511 class_basis(Class,Deps),
512 ub(Deps,OrdV,V-t_lU(L,U)-Init,Vub-Vb-_),
513 pivot_b(Vub,V,Vb,t_lu(L,U)),
514 replace_in_cont(ContIn,Vub,V,ContOut).
515dec_step_2_cont(t_none,l(V*_,_),_,unlimited(V,t_none),Cont,Cont).
516
517
518
519inc_step_2_cont(t_U(U),l(V*K,OrdV),Class,Status,ContIn,ContOut) :-
520 K < 0,
521 ( lb(Class,OrdV,Vub-Vb-_)
522 -> Status = applied,
523 pivot_a(Vub,V,Vb,t_u(U)),
524 replace_in_cont(ContIn,Vub,V,ContOut)
525 ; Status = unlimited(V,t_u(U)),
526 ContIn = ContOut
527 ).
528inc_step_2_cont(t_lU(L,U),l(V*K,OrdV),Class,applied,ContIn,ContOut) :-
529 K < 0,
530 Init is L - U,
531 class_basis(Class,Deps),
532 lb(Deps,OrdV,V-t_Lu(L,U)-Init,Vub-Vb-_),
533 pivot_b(Vub,V,Vb,t_lu(L,U)),
534 replace_in_cont(ContIn,Vub,V,ContOut).
535inc_step_2_cont(t_L(L),l(V*K,OrdV),Class,Status,ContIn,ContOut) :-
536 K > 0,
537 ( ub(Class,OrdV,Vub-Vb-_)
538 -> Status = applied,
539 pivot_a(Vub,V,Vb,t_l(L)),
540 replace_in_cont(ContIn,Vub,V,ContOut)
541 ; Status = unlimited(V,t_l(L)),
542 ContIn = ContOut
543 ).
544inc_step_2_cont(t_Lu(L,U),l(V*K,OrdV),Class,applied,ContIn,ContOut) :-
545 K > 0,
546 Init is U - L,
547 class_basis(Class,Deps),
548 ub(Deps,OrdV,V-t_lU(L,U)-Init,Vub-Vb-_),
549 pivot_b(Vub,V,Vb,t_lu(L,U)),
550 replace_in_cont(ContIn,Vub,V,ContOut).
551inc_step_2_cont(t_none,l(V*_,_),_,unlimited(V,t_none),Cont,Cont).
552
553replace_in_cont([],_,_,[]).
554replace_in_cont([H1|T1],X,Y,[H2|T2]) :-
555 ( H1 == X
556 -> H2 = Y,
557 T1 = T2
558 ; H2 = H1,
559 replace_in_cont(T1,X,Y,T2)
560 ).
561
562dec_step([],optimum).
563dec_step([l(V*K,OrdV)|Vs],Status) :-
564 get_attr(V,clpqr_itf,Att),
565 arg(2,Att,type(W)),
566 arg(6,Att,class(Class)),
567 ( dec_step_2(W,l(V*K,OrdV),Class,Status)
568 -> true
569 ; dec_step(Vs,Status)
570 ).
571
572dec_step_2(t_U(U),l(V*K,OrdV),Class,Status) :-
573 K > 0,
574 ( lb(Class,OrdV,Vub-Vb-_)
575 -> 576 Status = applied,
577 pivot_a(Vub,V,Vb,t_u(U))
578 ; Status = unlimited(V,t_u(U))
579 ).
580dec_step_2(t_lU(L,U),l(V*K,OrdV),Class,applied) :-
581 K > 0,
582 Init is L - U,
583 class_basis(Class,Deps),
584 lb(Deps,OrdV,V-t_Lu(L,U)-Init,Vub-Vb-_),
585 pivot_b(Vub,V,Vb,t_lu(L,U)).
586dec_step_2(t_L(L),l(V*K,OrdV),Class,Status) :-
587 K < 0,
588 ( ub(Class,OrdV,Vub-Vb-_)
589 -> Status = applied,
590 pivot_a(Vub,V,Vb,t_l(L))
591 ; Status = unlimited(V,t_l(L))
592 ).
593dec_step_2(t_Lu(L,U),l(V*K,OrdV),Class,applied) :-
594 K < 0,
595 Init is U - L,
596 class_basis(Class,Deps),
597 ub(Deps,OrdV,V-t_lU(L,U)-Init,Vub-Vb-_),
598 pivot_b(Vub,V,Vb,t_lu(L,U)).
599dec_step_2(t_none,l(V*_,_),_,unlimited(V,t_none)).
600
601inc_step([],optimum). 602inc_step([l(V*K,OrdV)|Vs],Status) :-
603 get_attr(V,clpqr_itf,Att),
604 arg(2,Att,type(W)),
605 arg(6,Att,class(Class)),
606 ( inc_step_2(W,l(V*K,OrdV),Class,Status)
607 -> true
608 ; inc_step(Vs,Status)
609 ).
610
611inc_step_2(t_U(U),l(V*K,OrdV),Class,Status) :-
612 K < 0,
613 ( lb(Class,OrdV,Vub-Vb-_)
614 -> Status = applied,
615 pivot_a(Vub,V,Vb,t_u(U))
616 ; Status = unlimited(V,t_u(U))
617 ).
618inc_step_2(t_lU(L,U),l(V*K,OrdV),Class,applied) :-
619 K < 0,
620 Init is L - U,
621 class_basis(Class,Deps),
622 lb(Deps,OrdV,V-t_Lu(L,U)-Init,Vub-Vb-_),
623 pivot_b(Vub,V,Vb,t_lu(L,U)).
624inc_step_2(t_L(L),l(V*K,OrdV),Class,Status) :-
625 K > 0,
626 ( ub(Class,OrdV,Vub-Vb-_)
627 -> Status = applied,
628 pivot_a(Vub,V,Vb,t_l(L))
629 ; Status = unlimited(V,t_l(L))
630 ).
631inc_step_2(t_Lu(L,U),l(V*K,OrdV),Class,applied) :-
632 K > 0,
633 Init is U - L,
634 class_basis(Class,Deps),
635 ub(Deps,OrdV,V-t_lU(L,U)-Init,Vub-Vb-_),
636 pivot_b(Vub,V,Vb,t_lu(L,U)).
637inc_step_2(t_none,l(V*_,_),_,unlimited(V,t_none)).
638
655
656ub(Class,OrdX,Ub) :-
657 class_basis(Class,Deps),
658 ub_first(Deps,OrdX,Ub).
659
666
667ub_first([Dep|Deps],OrdX,Tightest) :-
668 ( get_attr(Dep,clpqr_itf,Att),
669 arg(2,Att,type(Type)),
670 arg(4,Att,lin(Lin)),
671 ub_inner(Type,OrdX,Lin,W,Ub),
672 Ub >= 0
673 -> ub(Deps,OrdX,Dep-W-Ub,Tightest)
674 ; ub_first(Deps,OrdX,Tightest)
675 ).
676
680
681ub([],_,T0,T0).
682ub([Dep|Deps],OrdX,T0,T1) :-
683 ( get_attr(Dep,clpqr_itf,Att),
684 arg(2,Att,type(Type)),
685 arg(4,Att,lin(Lin)),
686 ub_inner(Type,OrdX,Lin,W,Ub),
687 T0 = _-Ubb,
688 Ub < Ubb,
689 Ub >= 0
690 -> ub(Deps,OrdX,Dep-W-Ub,T1) 691 ; ub(Deps,OrdX,T0,T1) 692 ).
693
697
698ub_inner(t_l(L),OrdX,Lin,t_L(L),Ub) :-
699 nf_rhs_x(Lin,OrdX,Rhs,K),
700 K < 0,
701 Ub is (L - Rhs) rdiv K.
702ub_inner(t_u(U),OrdX,Lin,t_U(U),Ub) :-
703 nf_rhs_x(Lin,OrdX,Rhs,K),
704 K > 0,
705 Ub is (U - Rhs) rdiv K.
706ub_inner(t_lu(L,U),OrdX,Lin,W,Ub) :-
707 nf_rhs_x(Lin,OrdX,Rhs,K),
708 ( K < 0 709 -> W = t_Lu(L,U),
710 Ub = (L - Rhs) rdiv K
711 ; K > 0 712 -> W = t_lU(L,U),
713 Ub = (U - Rhs) rdiv K
714 ).
715
724
725lb(Class,OrdX,Lb) :-
726 class_basis(Class,Deps),
727 lb_first(Deps,OrdX,Lb).
728
737
738lb_first([Dep|Deps],OrdX,Tightest) :-
739 ( get_attr(Dep,clpqr_itf,Att),
740 arg(2,Att,type(Type)),
741 arg(4,Att,lin(Lin)),
742 lb_inner(Type,OrdX,Lin,W,Lb),
743 Lb =< 0 744 -> lb(Deps,OrdX,Dep-W-Lb,Tightest)
745 ; lb_first(Deps,OrdX,Tightest)
746 ).
747
752
753lb([],_,T0,T0).
754lb([Dep|Deps],OrdX,T0,T1) :-
755 ( get_attr(Dep,clpqr_itf,Att),
756 arg(2,Att,type(Type)),
757 arg(4,Att,lin(Lin)),
758 lb_inner(Type,OrdX,Lin,W,Lb),
759 T0 = _-Lbb,
760 Lb > Lbb, 761 762 Lb =< 0 763 -> lb(Deps,OrdX,Dep-W-Lb,T1)
764 ; lb(Deps,OrdX,T0,T1)
765 ).
766
779
780lb_inner(t_l(L),OrdX,Lin,t_L(L),Lb) :-
781 nf_rhs_x(Lin,OrdX,Rhs,K), 782 783 784 K > 0,
785 Lb is (L - Rhs) rdiv K.
786lb_inner(t_u(U),OrdX,Lin,t_U(U),Lb) :-
787 nf_rhs_x(Lin,OrdX,Rhs,K),
788 K < 0, 789 Lb is (U - Rhs) rdiv K.
790lb_inner(t_lu(L,U),OrdX,Lin,W,Lb) :-
791 nf_rhs_x(Lin,OrdX,Rhs,K),
792 ( K < 0
793 -> W = t_lU(L,U),
794 Lb is (U - Rhs) rdiv K
795 ; K > 0
796 -> W = t_Lu(L,U),
797 Lb is (L - Rhs) rdiv K
798 ).
799
807
808solve(Lin) :-
809 Lin = [I,_|H],
810 solve(H,Lin,I,Bindings,[]),
811 export_binding(Bindings).
812
816
817solve([],_,I,Bind0,Bind0) :-
818 !,
819 I =:= 0.
820solve(H,Lin,_,Bind0,BindT) :-
821 sd(H,[],ClassesUniq,9-9-0,Category-Selected-_,NV,NVT),
822 get_attr(Selected,clpqr_itf,Att),
823 arg(5,Att,order(Ord)),
824 isolate(Ord,Lin,Lin1), 825 ( Category = 1 826 -> setarg(4,Att,lin(Lin1)),
827 Lin1 = [Inhom,_|Hom],
828 bs_collect_binding(Hom,Selected,Inhom,Bind0,BindT),
829 eq_classes(NV,NVT,ClassesUniq)
830 ; Category = 2 831 -> arg(6,Att,class(NewC)),
832 class_allvars(NewC,Deps),
833 ( ClassesUniq = [_] 834 -> bs_collect_bindings(Deps,Ord,Lin1,Bind0,BindT)
835 ; Bind0 = BindT,
836 bs(Deps,Ord,Lin1)
837 ),
838 eq_classes(NV,NVT,ClassesUniq)
839 ; Category = 3 840 841 -> arg(2,Att,type(Type)),
842 setarg(4,Att,lin(Lin1)),
843 deactivate_bound(Type,Selected),
844 eq_classes(NV,NVT,ClassesUniq),
845 basis_add(Selected,Basis),
846 undet_active(Lin1), 847 848 Lin1 = [Inhom,_|Hom],
849 bs_collect_binding(Hom,Selected,Inhom,Bind0,Bind1), 850 851 rcbl(Basis,Bind1,BindT) 852 ; Category = 4 853 854 -> arg(2,Att,type(Type)),
855 arg(6,Att,class(NewC)),
856 class_allvars(NewC,Deps),
857 ( ClassesUniq = [_] 858 -> bs_collect_bindings(Deps,Ord,Lin1,Bind0,Bind1)
859 ; Bind0 = Bind1,
860 bs(Deps,Ord,Lin1)
861 ),
862 deactivate_bound(Type,Selected),
863 basis_add(Selected,Basis),
864 865 866 equate(ClassesUniq,_),
867 undet_active(Lin1),
868 rcbl(Basis,Bind1,BindT)
869 ).
870
874
878
879solve_x(Lin,X) :-
880 Lin = [I,_|H],
881 solve_x(H,Lin,I,X,Bindings,[]),
882 export_binding(Bindings).
883
884solve_x([],_,I,_,Bind0,Bind0) :-
885 !,
886 I =:= 0.
887solve_x(H,Lin,_,X,Bind0,BindT) :-
888 sd(H,[],ClassesUniq,9-9-0,_,NV,NVT),
889 get_attr(X,clpqr_itf,Att),
890 arg(5,Att,order(OrdX)),
891 isolate(OrdX,Lin,Lin1),
892 ( arg(6,Att,class(NewC))
893 -> class_allvars(NewC,Deps),
894 ( ClassesUniq = [_] 895 -> bs_collect_bindings(Deps,OrdX,Lin1,Bind0,BindT)
896 ; Bind0 = BindT,
897 bs(Deps,OrdX,Lin1)
898 ),
899 eq_classes(NV,NVT,ClassesUniq)
900 ; setarg(4,Att,lin(Lin1)),
901 Lin1 = [Inhom,_|Hom],
902 bs_collect_binding(Hom,X,Inhom,Bind0,BindT),
903 eq_classes(NV,NVT,ClassesUniq)
904 ).
905
910
911solve_ord_x(Lin,OrdX,ClassX) :-
912 Lin = [I,_|H],
913 solve_ord_x(H,Lin,I,OrdX,ClassX,Bindings,[]),
914 export_binding(Bindings).
915
916solve_ord_x([],_,I,_,_,Bind0,Bind0) :-
917 I =:= 0.
918solve_ord_x([_|_],Lin,_,OrdX,ClassX,Bind0,BindT) :-
919 isolate(OrdX,Lin,Lin1),
920 Lin1 = [_,_|H1],
921 sd(H1,[],ClassesUniq1,9-9-0,_,NV,NVT), 922 923 ord_add_element(ClassesUniq1,ClassX,ClassesUniq),
924 class_allvars(ClassX,Deps),
925 ( ClassesUniq = [_] 926 -> bs_collect_bindings(Deps,OrdX,Lin1,Bind0,BindT)
927 ; Bind0 = BindT,
928 bs(Deps,OrdX,Lin1)
929 ),
930 eq_classes(NV,NVT,ClassesUniq).
931
933
939
940sd([],Class0,Class0,Preference0,Preference0,NV0,NV0).
941sd([l(X*K,_)|Xs],Class0,ClassN,Preference0,PreferenceN,NV0,NVt) :-
942 get_attr(X,clpqr_itf,Att),
943 ( arg(6,Att,class(Xc)) 944 -> NV0 = NV1,
945 ord_add_element(Class0,Xc,Class1),
946 ( arg(2,Att,type(t_none))
947 -> preference(Preference0,2-X-K,Preference1)
948 949 ; preference(Preference0,4-X-K,Preference1)
950 951 )
952 ; 953 Class1 = Class0,
954 NV0 = [X|NV1], 955 ( arg(2,Att,type(t_none))
956 -> preference(Preference0,1-X-K,Preference1)
957 958 ; preference(Preference0,3-X-K,Preference1)
959 960 )
961 ),
962 sd(Xs,Class1,ClassN,Preference1,PreferenceN,NV1,NVt).
963
967preference(A,B,Pref) :-
968 A = Px-_-_,
969 B = Py-_-_,
970 ( Px < Py
971 -> Pref = A
972 ; Pref = B
973 ).
974
981
982eq_classes(NV,_,Cs) :-
983 var(NV),
984 !,
985 equate(Cs,_).
986eq_classes(NV,NVT,Cs) :-
987 class_new(Su,clpq,NV,NVT,[]), 988 attach_class(NV,Su), 989 equate(Cs,Su).
990
991equate([],_).
992equate([X|Xs],X) :- equate(Xs,X).
993
997attach_class(Xs,_) :-
998 var(Xs), 999 !.
1000attach_class([X|Xs],Class) :-
1001 get_attr(X,clpqr_itf,Att),
1002 setarg(6,Att,class(Class)),
1003 attach_class(Xs,Class).
1004
1009
1010unconstrained(Lin,Uc,Kuc,Rest) :-
1011 Lin = [_,_|H],
1012 sd(H,[],_,9-9-0,Category-Uc-_,_,_),
1013 Category =< 2,
1014 get_attr(Uc,clpqr_itf,Att),
1015 arg(5,Att,order(OrdUc)),
1016 delete_factor(OrdUc,Lin,Rest,Kuc).
1017
1022same_class([],_).
1023same_class([l(X*_,_)|Xs],Class) :-
1024 get_or_add_class(X,Class),
1025 same_class(Xs,Class).
1026
1031
1032get_or_add_class(X,Class) :-
1033 get_attr(X,clpqr_itf,Att),
1034 arg(1,Att,CLP),
1035 ( arg(6,Att,class(ClassX))
1036 -> ClassX = Class
1037 ; setarg(6,Att,class(Class)),
1038 class_new(Class,CLP,[X|Tail],Tail,[])
1039 ).
1040
1044
1045allvars(X,Allvars) :-
1046 get_attr(X,clpqr_itf,Att),
1047 arg(6,Att,class(C)),
1048 class_allvars(C,Allvars).
1049
1055
1056deactivate_bound(t_l(_),_).
1057deactivate_bound(t_u(_),_).
1058deactivate_bound(t_lu(_,_),_).
1059deactivate_bound(t_L(L),X) :-
1060 get_attr(X,clpqr_itf,Att),
1061 setarg(2,Att,type(t_l(L))).
1062deactivate_bound(t_Lu(L,U),X) :-
1063 get_attr(X,clpqr_itf,Att),
1064 setarg(2,Att,type(t_lu(L,U))).
1065deactivate_bound(t_U(U),X) :-
1066 get_attr(X,clpqr_itf,Att),
1067 setarg(2,Att,type(t_u(U))).
1068deactivate_bound(t_lU(L,U),X) :-
1069 get_attr(X,clpqr_itf,Att),
1070 setarg(2,Att,type(t_lu(L,U))).
1071
1078
1079intro_at(X,Value,Type) :-
1080 get_attr(X,clpqr_itf,Att),
1081 arg(5,Att,order(Ord)),
1082 arg(6,Att,class(Class)),
1083 setarg(2,Att,type(Type)),
1084 ( Value =:= 0
1085 -> true
1086 ; backsubst_delta(Class,Ord,X,Value)
1087 ).
1088
1093
1094undet_active([_,_|H]) :-
1095 undet_active_h(H).
1096
1101
1102undet_active_h([]).
1103undet_active_h([l(X*_,_)|Xs]) :-
1104 get_attr(X,clpqr_itf,Att),
1105 arg(2,Att,type(Type)),
1106 undet_active(Type,X),
1107 undet_active_h(Xs).
1108
1113
1114undet_active(t_none,_). 1115undet_active(t_L(_),_).
1116undet_active(t_Lu(_,_),_).
1117undet_active(t_U(_),_).
1118undet_active(t_lU(_,_),_).
1119undet_active(t_l(L),X) :- intro_at(X,L,t_L(L)).
1120undet_active(t_u(U),X) :- intro_at(X,U,t_U(U)).
1121undet_active(t_lu(L,U),X) :- intro_at(X,L,t_Lu(L,U)).
1122
1129
1130determine_active_dec([_,_|H]) :-
1131 determine_active(H,-1).
1132
1139
1140determine_active_inc([_,_|H]) :-
1141 determine_active(H,1).
1142
1149
1150determine_active([],_).
1151determine_active([l(X*K,_)|Xs],S) :-
1152 get_attr(X,clpqr_itf,Att),
1153 arg(2,Att,type(Type)),
1154 determine_active(Type,X,K,S),
1155 determine_active(Xs,S).
1156
1157determine_active(t_L(_),_,_,_).
1158determine_active(t_Lu(_,_),_,_,_).
1159determine_active(t_U(_),_,_,_).
1160determine_active(t_lU(_,_),_,_,_).
1161determine_active(t_l(L),X,_,_) :- intro_at(X,L,t_L(L)).
1162determine_active(t_u(U),X,_,_) :- intro_at(X,U,t_U(U)).
1163determine_active(t_lu(L,U),X,K,S) :-
1164 KS is K*S,
1165 ( KS < 0
1166 -> intro_at(X,L,t_Lu(L,U))
1167 ; KS > 0
1168 -> intro_at(X,U,t_lU(L,U))
1169 ).
1170
1174
1175detach_bounds(V) :-
1176 get_attr(V,clpqr_itf,Att),
1177 arg(2,Att,type(Type)),
1178 arg(4,Att,lin(Lin)),
1179 arg(5,Att,order(OrdV)),
1180 arg(6,Att,class(Class)),
1181 setarg(2,Att,type(t_none)),
1182 setarg(3,Att,strictness(0)),
1183 ( indep(Lin,OrdV)
1184 -> ( ub(Class,OrdV,Vub-Vb-_)
1185 -> 1186 class_basis_drop(Class,Vub),
1187 pivot(Vub,Class,OrdV,Vb,Type)
1188 ; lb(Class,OrdV,Vlb-Vb-_)
1189 -> class_basis_drop(Class,Vlb),
1190 pivot(Vlb,Class,OrdV,Vb,Type)
1191 ; true
1192 )
1193 ; class_basis_drop(Class,V)
1194 ).
1195
1196detach_bounds_vlv(OrdV,Lin,Class,Var,NewLin) :-
1197 ( indep(Lin,OrdV)
1198 -> Lin = [_,R|_],
1199 ( ub(Class,OrdV,Vub-Vb-_)
1200 -> 1201 1202 class_basis_drop(Class,Var),
1203 pivot_vlv(Vub,Class,OrdV,Vb,R,NewLin)
1204 ; lb(Class,OrdV,Vlb-Vb-_)
1205 -> class_basis_drop(Class,Var),
1206 pivot_vlv(Vlb,Class,OrdV,Vb,R,NewLin)
1207 ; NewLin = Lin
1208 )
1209 ; NewLin = Lin,
1210 class_basis_drop(Class,Var)
1211 ).
1212
1214
1218
1219basis_drop(X) :-
1220 get_attr(X,clpqr_itf,Att),
1221 arg(6,Att,class(Cv)),
1222 class_basis_drop(Cv,X).
1223
1227
1228basis(X,Basis) :-
1229 get_attr(X,clpqr_itf,Att),
1230 arg(6,Att,class(Cv)),
1231 class_basis(Cv,Basis).
1232
1237
1238basis_add(X,NewBasis) :-
1239 get_attr(X,clpqr_itf,Att),
1240 arg(6,Att,class(Cv)),
1241 class_basis_add(Cv,X,NewBasis).
1242
1247
1248basis_pivot(Leave,Enter) :-
1249 get_attr(Leave,clpqr_itf,Att),
1250 arg(6,Att,class(Cv)),
1251 class_basis_pivot(Cv,Enter,Leave).
1252
1254
1260
1264
1265pivot(Dep,Indep) :-
1266 get_attr(Dep,clpqr_itf,AttD),
1267 arg(4,AttD,lin(H)),
1268 arg(5,AttD,order(OrdDep)),
1269 get_attr(Indep,clpqr_itf,AttI),
1270 arg(5,AttI,order(Ord)),
1271 arg(5,AttI,class(Class)),
1272 delete_factor(Ord,H,H0,Coeff),
1273 K is -1 rdiv Coeff,
1274 add_linear_ff(H0,K,[0,0,l(Dep* -1,OrdDep)],K,Lin),
1275 backsubst(Class,Ord,Lin).
1276
1283
1284
1285pivot_a(Dep,Indep,Vb,Wd) :-
1286 basis_pivot(Dep,Indep),
1287 get_attr(Indep,clpqr_itf,Att),
1288 arg(2,Att,type(Type)),
1289 arg(5,Att,order(Ord)),
1290 arg(6,Att,class(Class)),
1291 pivot(Dep,Class,Ord,Vb,Type),
1292 get_attr(Indep,clpqr_itf,Att2), 1293 setarg(2,Att2,type(Wd)).
1294
1295pivot_b(Vub,V,Vb,Wd) :-
1296 ( Vub == V
1297 -> get_attr(V,clpqr_itf,Att),
1298 arg(5,Att,order(Ord)),
1299 arg(6,Att,class(Class)),
1300 setarg(2,Att,type(Vb)),
1301 pivot_b_delta(Vb,Delta), 1302 backsubst_delta(Class,Ord,V,Delta)
1303 ; pivot_a(Vub,V,Vb,Wd)
1304 ).
1305
1306pivot_b_delta(t_Lu(L,U),Delta) :- Delta is L-U.
1307pivot_b_delta(t_lU(L,U),Delta) :- Delta is U-L.
1308
1312
1313select_active_bound(t_L(L),L).
1314select_active_bound(t_Lu(L,_),L).
1315select_active_bound(t_U(U),U).
1316select_active_bound(t_lU(_,U),U).
1317select_active_bound(t_none,0).
1321select_active_bound(t_l(_),0).
1322select_active_bound(t_u(_),0).
1323select_active_bound(t_lu(_,_),0).
1324
1325
1330
1335pivot(Dep,Class,IndepOrd,DepAct,IndAct) :-
1336 get_attr(Dep,clpqr_itf,Att),
1337 arg(4,Att,lin(H)),
1338 arg(5,Att,order(DepOrd)),
1339 setarg(2,Att,type(DepAct)),
1340 select_active_bound(DepAct,AbvD), 1341 select_active_bound(IndAct,AbvI), 1342 delete_factor(IndepOrd,H,H0,Coeff), 1343 AbvDm is -AbvD,
1344 AbvIm is -AbvI,
1345 add_linear_f1([0,AbvIm],Coeff,H0,H1),
1346 K is -1 rdiv Coeff,
1347 add_linear_ff(H1,K,[0,AbvDm,l(Dep* -1,DepOrd)],K,H2),
1348 1349 add_linear_11(H2,[0,AbvIm],Lin),
1350 backsubst(Class,IndepOrd,Lin).
1351
1358
1359pivot_vlv(Dep,Class,IndepOrd,DepAct,AbvI,Lin) :-
1360 get_attr(Dep,clpqr_itf,Att),
1361 arg(4,Att,lin(H)),
1362 arg(5,Att,order(DepOrd)),
1363 setarg(2,Att,type(DepAct)),
1364 select_active_bound(DepAct,AbvD), 1365 delete_factor(IndepOrd,H,H0,Coeff), 1366 AbvDm is -AbvD,
1367 AbvIm is -AbvI,
1368 add_linear_f1([0,AbvIm],Coeff,H0,H1),
1369 K is -1 rdiv Coeff,
1370 add_linear_ff(H1,K,[0,AbvDm,l(Dep* -1,DepOrd)],K,Lin),
1371 1372 add_linear_11(Lin,[0,AbvIm],SubstLin),
1373 backsubst(Class,IndepOrd,SubstLin).
1374
1380
1381backsubst_delta(Class,OrdX,X,Delta) :-
1382 backsubst(Class,OrdX,[0,Delta,l(X*1,OrdX)]).
1383
1388
1389backsubst(Class,OrdX,Lin) :-
1390 class_allvars(Class,Allvars),
1391 bs(Allvars,OrdX,Lin).
1392
1400
1401bs(Xs,_,_) :-
1402 var(Xs),
1403 !.
1404bs([X|Xs],OrdV,Lin) :-
1405 ( get_attr(X,clpqr_itf,Att),
1406 arg(4,Att,lin(LinX)),
1407 nf_substitute(OrdV,Lin,LinX,LinX1) 1408 -> setarg(4,Att,lin(LinX1)),
1409 bs(Xs,OrdV,Lin)
1410 ; bs(Xs,OrdV,Lin)
1411 ).
1412
1416
1426
1427bs_collect_bindings(Xs,_,_,Bind0,BindT) :-
1428 var(Xs),
1429 !,
1430 Bind0 = BindT.
1431bs_collect_bindings([X|Xs],OrdV,Lin,Bind0,BindT) :-
1432 ( get_attr(X,clpqr_itf,Att),
1433 arg(4,Att,lin(LinX)),
1434 nf_substitute(OrdV,Lin,LinX,LinX1) 1435 -> setarg(4,Att,lin(LinX1)),
1436 LinX1 = [Inhom,_|Hom],
1437 bs_collect_binding(Hom,X,Inhom,Bind0,Bind1),
1438 bs_collect_bindings(Xs,OrdV,Lin,Bind1,BindT)
1439 ; bs_collect_bindings(Xs,OrdV,Lin,Bind0,BindT)
1440 ).
1441
1447bs_collect_binding([],X,Inhom) --> [X-Inhom].
1448bs_collect_binding([_|_],_,_) --> [].
1449
1453
1457
1458rcbl([],Bind0,Bind0).
1459rcbl([X|Continuation],Bind0,BindT) :-
1460 ( rcb_cont(X,Status,Violated,Continuation,NewContinuation) 1461 -> rcbl_status(Status,X,NewContinuation,Bind0,BindT,Violated)
1462 ; rcbl(Continuation,Bind0,BindT)
1463 ).
1464
1465rcb_cont(X,Status,Violated,ContIn,ContOut) :-
1466 get_attr(X,clpqr_itf,Att),
1467 arg(2,Att,type(Type)),
1468 arg(4,Att,lin([I,R|H])),
1469 ( Type = t_l(L) 1470 1471 -> R + I =< L,
1472 Violated = l(L),
1473 inc_step_cont(H,Status,ContIn,ContOut)
1474 ; Type = t_u(U) 1475 1476 -> R + I >= U,
1477 Violated = u(U),
1478 dec_step_cont(H,Status,ContIn,ContOut)
1479 ; Type = t_lu(L,U) 1480 -> At is R + I,
1481 ( At =< L
1482 -> Violated = l(L),
1483 inc_step_cont(H,Status,ContIn,ContOut)
1484 ; At >= U
1485 -> Violated = u(U),
1486 dec_step_cont(H,Status,ContIn,ContOut)
1487 )
1488 ). 1489
1490
1491
1496reconsider(X) :-
1497 rcb(X,Status,Violated),
1498 !,
1499 rcbl_status(Status,X,[],Binds,[],Violated),
1500 export_binding(Binds).
1501reconsider(_).
1502
1518
1519rcb(X,Status,Violated) :-
1520 get_attr(X,clpqr_itf,Att),
1521 arg(2,Att,type(Type)),
1522 arg(4,Att,lin([I,R|H])),
1523 ( Type = t_l(L) 1524 1525 -> R + I =< L,
1526 Violated = l(L),
1527 inc_step(H,Status)
1528 ; Type = t_u(U) 1529 1530 -> R + I >= U,
1531 Violated = u(U),
1532 dec_step(H,Status)
1533 ; Type = t_lu(L,U) 1534 -> At is R + I,
1535 ( At =< L
1536 -> Violated = l(L),
1537 inc_step(H,Status)
1538 ; At >= U
1539 -> Violated = u(U),
1540 dec_step(H,Status)
1541 )
1542 ). 1543
1547
1548rcbl_status(optimum,X,Cont,B0,Bt,Violated) :- rcbl_opt(Violated,X,Cont,B0,Bt).
1549rcbl_status(applied,X,Cont,B0,Bt,Violated) :- rcbl_app(Violated,X,Cont,B0,Bt).
1550rcbl_status(unlimited(Indep,DepT),X,Cont,B0,Bt,Violated) :-
1551 rcbl_unl(Violated,X,Cont,B0,Bt,Indep,DepT).
1552
1560rcbl_opt(l(L),X,Continuation,B0,B1) :-
1561 get_attr(X,clpqr_itf,Att),
1562 arg(2,Att,type(Type)),
1563 arg(3,Att,strictness(Strict)),
1564 arg(4,Att,lin(Lin)),
1565 Lin = [I,R|_],
1566 Opt is R + I,
1567 ( L < Opt
1568 -> narrow_u(Type,X,Opt), 1569 rcbl(Continuation,B0,B1)
1570 ; L =:= Opt,
1571 Strict /\ 2 =:= 0, 1572 Mop is -Opt,
1573 normalize_scalar(Mop,MopN),
1574 add_linear_11(MopN,Lin,Lin1),
1575 Lin1 = [Inhom,_|Hom],
1576 ( Hom = []
1577 -> rcbl(Continuation,B0,B1) 1578 ; solve(Hom,Lin1,Inhom,B0,B1)
1579 )
1580 ).
1581rcbl_opt(u(U),X,Continuation,B0,B1) :-
1582 get_attr(X,clpqr_itf,Att),
1583 arg(2,Att,type(Type)),
1584 arg(3,Att,strictness(Strict)),
1585 arg(4,Att,lin(Lin)),
1586 Lin = [I,R|_],
1587 Opt is R + I,
1588 ( U > Opt
1589 -> narrow_l(Type,X,Opt), 1590 rcbl(Continuation,B0,B1)
1591 ; U =:= Opt,
1592 Strict /\ 1 =:= 0, 1593 Mop is -Opt,
1594 normalize_scalar(Mop,MopN),
1595 add_linear_11(MopN,Lin,Lin1),
1596 Lin1 = [Inhom,_|Hom],
1597 ( Hom = []
1598 -> rcbl(Continuation,B0,B1) 1599 ; solve(Hom,Lin1,Inhom,B0,B1)
1600 )
1601 ).
1602
1606rcbl_app(l(L),X,Continuation,B0,B1) :-
1607 get_attr(X,clpqr_itf,Att),
1608 arg(4,Att,lin([I,R|H])),
1609 ( R + I > L 1610 -> rcbl(Continuation,B0,B1)
1611 ; inc_step(H,Status),
1612 rcbl_status(Status,X,Continuation,B0,B1,l(L))
1613 ).
1614rcbl_app(u(U),X,Continuation,B0,B1) :-
1615 get_attr(X,clpqr_itf,Att),
1616 arg(4,Att,lin([I,R|H])),
1617 ( R + I < U 1618 -> rcbl(Continuation,B0,B1)
1619 ; dec_step(H,Status),
1620 rcbl_status(Status,X,Continuation,B0,B1,u(U))
1621 ).
1625rcbl_unl(l(L),X,Continuation,B0,B1,Indep,DepT) :-
1626 pivot_a(X,Indep,t_L(L),DepT), 1627 rcbl(Continuation,B0,B1).
1628rcbl_unl(u(U),X,Continuation,B0,B1,Indep,DepT) :-
1629 pivot_a(X,Indep,t_U(U),DepT), 1630 rcbl(Continuation,B0,B1).
1631
1636
1637narrow_u(t_u(_),X,U) :-
1638 get_attr(X,clpqr_itf,Att),
1639 setarg(2,Att,type(t_u(U))).
1640narrow_u(t_lu(L,_),X,U) :-
1641 get_attr(X,clpqr_itf,Att),
1642 setarg(2,Att,type(t_lu(L,U))).
1643
1648
1649narrow_l( t_l(_), X, L) :-
1650 get_attr(X,clpqr_itf,Att),
1651 setarg(2,Att,type(t_l(L))).
1652
1653narrow_l( t_lu(_,U), X, L) :-
1654 get_attr(X,clpqr_itf,Att),
1655 setarg(2,Att,type(t_lu(L,U))).
1656
1658
1663
1664dump_var(t_none,V,I,H) -->
1665 !,
1666 ( {
1667 H = [l(W*K,_)],
1668 V == W,
1669 I =:= 0,
1670 K =:= 1
1671 }
1672 -> 1673 []
1674 ; {nf2sum(H,I,Sum)},
1675 [V = Sum]
1676 ).
1677dump_var(t_L(L),V,I,H) -->
1678 !,
1679 dump_var(t_l(L),V,I,H).
1683dump_var(t_l(L),V,I,H) -->
1684 !,
1685 {
1686 H = [l(_*K,_)|_], 1687 get_attr(V,clpqr_itf,Att),
1688 arg(3,Att,strictness(Strict)),
1689 Sm is Strict /\ 2,
1690 Kr is 1 rdiv K,
1691 Li is Kr*(L - I),
1692 mult_hom(H,Kr,H1),
1693 nf2sum(H1,0,Sum),
1694 ( K > 0 1695 -> dump_strict(Sm,Sum >= Li,Sum > Li,Result)
1696 ; dump_strict(Sm,Sum =< Li,Sum < Li,Result)
1697 )
1698 },
1699 [Result].
1700dump_var(t_U(U),V,I,H) -->
1701 !,
1702 dump_var(t_u(U),V,I,H).
1703dump_var(t_u(U),V,I,H) -->
1704 !,
1705 {
1706 H = [l(_*K,_)|_], 1707 get_attr(V,clpqr_itf,Att),
1708 arg(3,Att,strictness(Strict)),
1709 Sm is Strict /\ 1,
1710 Kr is 1 rdiv K,
1711 Ui is Kr*(U-I),
1712 mult_hom(H,Kr,H1),
1713 nf2sum(H1,0.0,Sum),
1714 ( K > 0
1715 -> dump_strict(Sm,Sum =< Ui,Sum < Ui,Result)
1716 ; dump_strict(Sm,Sum >= Ui,Sum > Ui,Result)
1717 )
1718 },
1719 [Result].
1720dump_var(t_Lu(L,U),V,I,H) -->
1721 !,
1722 dump_var(t_l(L),V,I,H),
1723 dump_var(t_u(U),V,I,H).
1724dump_var(t_lU(L,U),V,I,H) -->
1725 !,
1726 dump_var(t_l(L),V,I,H),
1727 dump_var(t_u(U),V,I,H).
1728dump_var(t_lu(L,U),V,I,H) -->
1729 !,
1730 dump_var(t_l(L),V,I,H),
1731 dump_var(t_U(U),V,I,H).
1732dump_var(T,V,I,H) --> 1733 [V:T:I+H].
1734
1741
1742dump_strict(0,Result,_,Result).
1743dump_strict(1,_,Result,Result).
1744dump_strict(2,_,Result,Result).
1745
1751
1752dump_nz(_,H,I) -->
1753 {
1754 H = [l(_*K,_)|_],
1755 Kr is 1 rdiv K,
1756 I1 is -Kr*I,
1757 mult_hom(H,Kr,H1),
1758 nf2sum(H1,0,Sum)
1759 },
1760 [Sum =\= I1].
1761
1762 1765:- multifile
1766 sandbox:safe_primitive/1. 1767
1768sandbox:safe_primitive(bv_q:inf(_,_)).
1769sandbox:safe_primitive(bv_q:inf(_,_,_,_)).
1770sandbox:safe_primitive(bv_q:sup(_,_)).
1771sandbox:safe_primitive(bv_q:sup(_,_,_,_)).
1772sandbox:safe_primitive(bv_q:maximize(_)).
1773sandbox:safe_primitive(bv_q:minimize(_))