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