39
40:- module(clpcd_redund,
41 [
42 redundancy_vars/2,
43 systems/3
44 ]). 45
46:- use_module(library(clpcd/domain_ops)). 47:- use_module(library(clpcd/bv)). 48:- use_module(library(clpcd/nf)). 49:- use_module(library(clpcd/solve)). 50
58
63
64systems([],Si,Si).
65systems([V|Vs],Si,So) :-
66 ( var(V),
67 get_attr(V,clpcd_itf,Att),
68 arg(6,Att,class(C)),
69 not_memq(Si,C)
70 -> systems(Vs,[C|Si],So)
71 ; systems(Vs,Si,So)
72 ).
73
77
78not_memq([],_).
79not_memq([Y|Ys],X) :-
80 X \== Y,
81 not_memq(Ys,X).
82
87
88redundancy_vars(Vs, CLP) :-
89 !,
90 redundancy_vs(Vs, CLP).
91redundancy_vars(Vs, CLP) :-
92 statistics(runtime,[Start|_]),
93 redundancy_vs(Vs, CLP),
94 statistics(runtime,[End|_]),
95 Duration is End-Start,
96 format(user_error,"% Redundancy elimination took ~d msec~n",Duration).
97
98
102
103redundancy_vs(Vs, _) :-
104 var(Vs),
105 !.
106redundancy_vs([], _).
107redundancy_vs([V|Vs], CLP) :-
108 ( get_attr(V,clpcd_itf,Att),
109 arg(2,Att,type(Type)),
110 arg(3,Att,strictness(Strict)),
111 redundant(Type,CLP,V,Strict)
112 -> redundancy_vs(Vs, CLP)
113 ; redundancy_vs(Vs, CLP)
114 ).
115
122
123redundant(t_l(L),CLP,X,Strict) :-
124 get_attr(X,clpcd_itf,Att),
125 arg(1,Att,CLP),
126 detach_bounds(CLP,X), 127 128 negate_l(Strict,CLP,L,X),
129 red_t_l. 130redundant(t_u(U),CLP,X,Strict) :-
131 get_attr(X,clpcd_itf,Att),
132 arg(1,Att,CLP),
133 detach_bounds(CLP,X),
134 negate_u(Strict,CLP,U,X),
135 red_t_u.
136redundant(t_lu(L,U),CLP,X,Strict) :-
137 strictness_parts(Strict,Sl,Su),
138 ( get_attr(X,clpcd_itf,Att),
139 arg(1,Att,CLP),
140 setarg(2,Att,type(t_u(U))),
141 setarg(3,Att,strictness(Su)),
142 negate_l(Strict,CLP,L,X)
143 -> red_t_l,
144 ( redundant(t_u(U),CLP,X,Strict)
145 -> true
146 ; true
147 )
148 ; get_attr(X,clpcd_itf,Att),
149 arg(1,Att,CLP),
150 setarg(2,Att,type(t_l(L))),
151 setarg(3,Att,strictness(Sl)),
152 negate_u(Strict,CLP,U,X)
153 -> red_t_u
154 ; true
155 ).
156redundant(t_L(L),CLP,X,Strict) :-
157 get_attr(X,clpcd_itf,Att),
158 arg(1,Att,CLP),
159 eval_d(CLP, -L, Bound),
160 intro_at(CLP, X, Bound, t_none), 161 detach_bounds(CLP,X),
162 negate_l(Strict,CLP,L,X),
163 red_t_L.
164redundant(t_U(U),CLP,X,Strict) :-
165 get_attr(X,clpcd_itf,Att),
166 arg(1,Att,CLP),
167 eval_d(CLP, -U, Bound),
168 intro_at(CLP, X, Bound, t_none), 169 detach_bounds(CLP,X),
170 negate_u(Strict,CLP,U,X),
171 red_t_U.
172redundant(t_Lu(L,U),CLP,X,Strict) :-
173 strictness_parts(Strict,Sl,Su),
174 ( eval_d(CLP, -L, Bound),
175 get_attr(X,clpcd_itf,Att),
176 arg(1,Att,CLP),
177 intro_at(CLP, X, Bound, t_u(U)),
178 get_attr(X,clpcd_itf,Att2), 179 setarg(3,Att2,strictness(Su)),
180 negate_l(Strict,CLP,L,X)
181 -> red_t_l,
182 ( redundant(t_u(U),CLP,X,Strict)
183 -> true
184 ; true
185 )
186 ; get_attr(X,clpcd_itf,Att),
187 arg(1,Att,CLP),
188 setarg(2,Att,type(t_L(L))),
189 setarg(3,Att,strictness(Sl)),
190 negate_u(Strict,CLP,U,X)
191 -> red_t_u
192 ; true
193 ).
194redundant(t_lU(L,U),CLP,X,Strict) :-
195 strictness_parts(Strict,Sl,Su),
196 ( get_attr(X,clpcd_itf,Att),
197 arg(1,Att,CLP),
198 setarg(2,Att,type(t_U(U))),
199 setarg(3,Att,strictness(Su)),
200 negate_l(Strict,CLP,L,X)
201 -> red_t_l,
202 ( redundant(t_U(U),CLP,X,Strict)
203 -> true
204 ; true
205 )
206 ; get_attr(X,clpcd_itf,Att),
207 arg(1,Att,CLP),
208 eval_d(CLP, -U, Bound),
209 intro_at(CLP, X, Bound, t_l(L)),
210 get_attr(X,clpcd_itf,Att2), 211 setarg(3,Att2,strictness(Sl)),
212 negate_u(Strict,CLP,U,X)
213 -> red_t_u
214 ; true
215 ).
216
221
222strictness_parts(Strict,Lower,Upper) :-
223 Lower is Strict /\ 2,
224 Upper is Strict /\ 1.
225
231
232negate_l(0,CLP,L,X) :-
233 add_constraint(L > X, CLP),
234 !,
235 fail.
236negate_l(1,CLP,L,X) :-
237 add_constraint(L > X, CLP),
238 !,
239 fail.
240negate_l(2,CLP,L,X) :-
241 add_constraint(L >= X, CLP),
242 !,
243 fail.
244negate_l(3,CLP,L,X) :-
245 add_constraint(L >= X, CLP),
246 !,
247 fail.
248negate_l(_,_,_,_).
249
255
256negate_u(0,CLP,U,X) :-
257 add_constraint(U < X, CLP),
258 !,
259 fail.
260negate_u(1,CLP,U,X) :-
261 add_constraint(U =< X, CLP),
262 !,
263 fail.
264negate_u(2,CLP,U,X) :-
265 add_constraint(U < X, CLP),
266 !,
267 fail.
268negate_u(3,CLP,U,X) :-
269 add_constraint(U =< X, CLP),
270 !,
271 fail.
272negate_u(_,_,_,_).
273
276
277red_t_l.
278red_t_u.
279red_t_L.
280red_t_U