39
40
43
44:- module(clpcd_itf,
45 [
46 dump_linear/3,
47 dump_nonzero/3
48 ]). 49
50:- use_module(library(neck)). 51:- use_module(library(clpcd/class)). 52:- use_module(library(clpcd/domain_ops)). 53:- use_module(library(clpcd/indep)). 54:- use_module(library(clpcd/bv)). 55:- use_module(library(clpcd/nf)). 56:- use_module(library(clpcd/store)). 57:- use_module(library(clpcd/solve)). 58:- init_expansors. 59
61
68
69dump_strict(0,Result,_,Result).
70dump_strict(1,_,Result,Result).
71dump_strict(2,_,Result,Result).
72
78
79dump_nz(CLP,_,H,I) -->
80 {
81 H = [l(_*K,_)|_],
82 div_d(CLP, 1, K, Kr),
83 eval_d(CLP, -Kr*I, I1),
84 mult_hom(H,CLP,Kr,H1),
85 nf2sum(H1,CLP,0,Sum)
86 },
87 [Sum =\= I1].
88
93
94dump_v(t_none,CLP,V,I,H) -->
95 !,
96 ( {
97 H = [l(W*K,_)],
98 V == W,
99 compare_d(CLP, =, 0, I),
100 compare_d(CLP, =, K, 1)
101 }
102 -> 103 []
104 ; {nf2sum(H,CLP,I,Sum)},
105 [V = Sum]
106 ).
107dump_v(t_L(L),CLP,V,I,H) -->
108 !,
109 dump_v(t_l(L),CLP,V,I,H).
113dump_v(t_l(L),CLP,V,I,H) -->
114 !,
115 {
116 H = [l(_*K,_)|_], 117 get_attr(V,clpcd_itf,Att),
118 arg(3,Att,strictness(Strict)),
119 Sm is Strict /\ 2,
120 div_d(CLP, 1, K, Kr),
121 eval_d(CLP, Kr*(L - I), Li),
122 mult_hom(H,CLP,Kr,H1),
123 nf2sum(H1,CLP,0,Sum),
124 ( compare_d(CLP, <, 0, K)
125 -> dump_strict(Sm,Sum >= Li,Sum > Li,Result)
126 ; dump_strict(Sm,Sum =< Li,Sum < Li,Result)
127 )
128 },
129 [Result].
130dump_v(t_U(U),C,V,I,H) -->
131 !,
132 dump_v(t_u(U),C,V,I,H).
133dump_v(t_u(U),CLP,V,I,H) -->
134 !,
135 {
136 H = [l(_*K,_)|_], 137 get_attr(V,clpcd_itf,Att),
138 arg(3,Att,strictness(Strict)),
139 Sm is Strict /\ 1,
140 div_d(CLP, 1, K, Kr),
141 eval_d(CLP, Kr*(U-I), Ui),
142 mult_hom(H,CLP,Kr,H1),
143 nf2sum(H1,CLP,0,Sum),
144 ( compare_d(CLP, <, 0, K)
145 -> dump_strict(Sm,Sum =< Ui,Sum < Ui,Result)
146 ; dump_strict(Sm,Sum >= Ui,Sum > Ui,Result)
147 )
148 },
149 [Result].
150dump_v(t_Lu(L,U),C,V,I,H) -->
151 !,
152 dump_v(t_l(L),C,V,I,H),
153 dump_v(t_u(U),C,V,I,H).
154dump_v(t_lU(L,U),C,V,I,H) -->
155 !,
156 dump_v(t_l(L),C,V,I,H),
157 dump_v(t_u(U),C,V,I,H).
158dump_v(t_lu(L,U),C,V,I,H) -->
159 !,
160 dump_v(t_l(L),C,V,I,H),
161 dump_v(t_U(U),C,V,I,H).
162dump_v(T,_,V,I,H) --> 163 [V:T:I+H].
164
165
170
171nf2sum([],_,I,I).
172nf2sum([X|Xs],CLP,I,Sum) :-
173 ( compare_d(CLP, =, 0, I)
174 -> X = l(Var*K,_),
175 ( 176 compare_d(CLP, =, K, 1)
177 -> hom2sum(Xs,CLP,Var,Sum)
178 ; 179 compare_d(CLP, =, K, -1)
180 -> hom2sum(Xs,CLP,-Var,Sum)
181 ; hom2sum(Xs,CLP,K*Var,Sum)
182 )
183 ; hom2sum([X|Xs],CLP,I,Sum)
184 ).
185
192
193hom2sum([],_,Term,Term).
194hom2sum([l(Var*K,_)|Cs],CLP,Sofar,Term) :-
195 ( 196 compare_d(CLP, =, K, 1)
197 -> Next = Sofar + Var
198 ; 199 compare_d(CLP, =, K, -1)
200 -> Next = Sofar - Var
201 ; 202 compare_d(CLP, <, K, 0)
203 -> eval_d(CLP, -K, Ka),
204 Next = Sofar - Ka*Var
205 ; Next = Sofar + K*Var
206 ),
207 hom2sum(Cs,CLP,Next,Term).
208
209dump_linear(V) -->
210 {
211 get_attr(V,clpcd_itf,Att),
212 arg(1,Att,CLP),
213 arg(2,Att,type(Type)),
214 arg(4,Att,lin(Lin)),
215 !,
216 Lin = [I,_|H]
217 },
218 ( {
219 Type=t_none
220 ; arg(9,Att,n)
221 }
222 -> []
223 ; dump_v(t_none,CLP,V,I,H)
224 ),
225 ( {
226 Type=t_none,
227 arg(9,Att,n) 228 }
229 -> 230 []
231 ; dump_v(Type,CLP,V,I,H)
232 ).
233dump_linear(_) --> [].
234
235dump_nonzero(V) -->
236 {
237 get_attr(V,clpcd_itf,Att),
238 arg(1,Att,CLP),
239 arg(4,Att,lin(Lin)),
240 arg(8,Att,nonzero),
241 !,
242 Lin = [I,_|H]
243 },
244 dump_nz(CLP,V,H,I).
245dump_nonzero(_) --> [].
246
247attr_unify_hook(t(CLP,n,n,n,n,n,n,n,_,_,_),Y) :-
248 !,
249 ( get_attr(Y,clpcd_itf,AttY),
250 \+ arg(1,AttY,CLP)
251 -> throw(error(permission_error('mix CLP(CD) variables with',
252 'CLP(CD) variables of other subdomain:',Y),context(_)))
253 ; true
254 ).
255attr_unify_hook(t(CLP,Ty,St,Li,Or,Cl,_,No,_,_,_),Y) :-
256 ( get_attr(Y,clpcd_itf,AttY),
257 \+ arg(1,AttY,CLP)
258 -> throw(error(permission_error('mix CLP(CD) variables with',
259 'CLP(CD) variables of other subdomain:',Y),context(_)))
260 ; true
261 ),
262 do_checks(CLP,Y,Ty,St,Li,Or,Cl,No,Later),
263 maplist(call,Later).
264
265do_checks(CLP,Y,Ty,St,Li,Or,Cl,No,Later) :-
266 numbers_only(CLP,Y),
267 verify_nonzero(No,CLP,Y),
268 verify_type(Ty,CLP,St,Y,Later,[]),
269 verify_lin(Or,CLP,Cl,Li,Y),
270 maplist(call,Later).
271
276
277verify_nonzero(nonzero,CLP,Y) :-
278 ( var(Y)
279 -> ( get_attr(Y,clpcd_itf,Att)
280 -> setarg(8,Att,nonzero)
281 ; put_attr(Y,clpcd_itf,t(CLP,n,n,n,n,n,n,nonzero,n,n,n))
282 )
283 ; compare_d(CLP, \=, 0, Y)
284 ).
285verify_nonzero(n,_,_). 286
292
293verify_type(type(Type),CLP,strictness(Strict),Y) -->
294 verify_type2(CLP,Y,Type,Strict).
295verify_type(n,_,n,_) --> [].
296
297verify_type2(C,Y,TypeX,StrictX) -->
298 {var(Y)},
299 !,
300 verify_type_var(TypeX,C,Y,StrictX).
301verify_type2(C,Y,TypeX,StrictX) -->
302 {verify_type_nonvar(TypeX,C,Y,StrictX)}.
303
307
308verify_type_nonvar(t_none,_,_,_).
309verify_type_nonvar(t_l(L),C,Value,S) :- ilb(S,C,L,Value).
310verify_type_nonvar(t_u(U),C,Value,S) :- iub(S,C,U,Value).
311verify_type_nonvar(t_lu(L,U),C,Value,S) :-
312 ilb(S,C,L,Value),
313 iub(S,C,U,Value).
314verify_type_nonvar(t_L(L),C,Value,S) :- ilb(S,C,L,Value).
315verify_type_nonvar(t_U(U),C,Value,S) :- iub(S,C,U,Value).
316verify_type_nonvar(t_Lu(L,U),C,Value,S) :-
317 ilb(S,C,L,Value),
318 iub(S,C,U,Value).
319verify_type_nonvar(t_lU(L,U),C,Value,S) :-
320 ilb(S,C,L,Value),
321 iub(S,C,U,Value).
322
332
333ilb(S,C,L,V) :-
334 between(0, 3, S),
335 ( S /\ 2 =:= 0
336 ->Op = (=<) 337 ; Op = (<) 338 ),
339 neck,
340 compare_d(C, Op, L, V).
341
342iub(S,C,U,V) :-
343 between(0, 3, S),
344 ( S /\ 1 =:= 0
345 ->Op = (=<) 346 ; Op = (<) 347 ),
348 neck,
349 compare_d(C, Op, V, U).
350
355
360
361verify_type_var(t_none,_,_,_) --> [].
362verify_type_var(t_l(L),C,Y,S) --> llb(S,C,L,Y).
363verify_type_var(t_u(U),C,Y,S) --> lub(S,C,U,Y).
364verify_type_var(t_lu(L,U),C,Y,S) -->
365 llb(S,C,L,Y),
366 lub(S,C,U,Y).
367verify_type_var(t_L(L),C,Y,S) --> llb(S,C,L,Y).
368verify_type_var(t_U(U),C,Y,S) --> lub(S,C,U,Y).
369verify_type_var(t_Lu(L,U),C,Y,S) -->
370 llb(S,C,L,Y),
371 lub(S,C,U,Y).
372verify_type_var(t_lU(L,U),C,Y,S) -->
373 llb(S,C,L,Y),
374 lub(S,C,U,Y).
375
380llb(S,C,L,V) -->
381 {S /\ 2 =:= 0 },
382 !,
383 [C:{L =< V}].
384llb(_,C,L,V) -->
385 [C:{L < V}].
386
387lub(S,C,U,V) -->
388 {S /\ 1 =:= 0 },
389 !,
390 [C:{V =< U}].
391lub(_,C,U,V) -->
392 [C:{V < U}].
393
402verify_lin(order(OrdX),CLP,class(Class),lin(LinX),Y) :-
403 !,
404 ( indep(CLP,LinX,OrdX)
405 -> detach_bounds_vlv(CLP,OrdX,LinX,Class,Y,NewLinX),
406 407 class_drop(Class,Y),
408 nf(-Y, CLP, NfY),
409 deref(CLP,NfY,LinY),
410 add_linear_11(CLP, NewLinX, LinY, Lind),
411 ( nf_coeff_of(Lind,OrdX,_)
412 -> 413 solve_ord_x(CLP, Lind, OrdX, Class)
414 ; solve(CLP, Lind) 415 )
416 ; class_drop(Class,Y),
417 nf(-Y, CLP, NfY),
418 deref(CLP,NfY,LinY),
419 add_linear_11(CLP, LinX, LinY, Lind),
420 solve(CLP, Lind)
421 ).
422verify_lin(_,_,_,_,_)