1 % (c) 2025-2025 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2 % Heinrich Heine Universitaet Duesseldorf
3 % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5 :- module(bounds_analysis,[infer_bounds/3, infer_bounds/4]).
6 :- use_module(probsrc(module_information),[module_info/2]).
7 :- module_info(group,b2asp).
8 :- module_info(description,'Perform bounds analysis on predicates for integer values.').
9
10 % we use CLP(FD) to implement the bounds propagation
11 % bint(FDVAR) : the possible values of an integer
12 % binterval(FDVAR1,FDVAR2,NonEmptyVar) :
13 % all values of the set must lie within FDVAR1 and FDVAR2
14 % NonEmptyVar is a reification of NonEmptyVar #<=> FDVAR1 #=< FDVAR2
15
16
17 % bound_id_info(ID,Type,Bounds) : information provided to the outside users of the module
18 % bound_internal_info(ID,Type,InternalBoundsRepresentation) : internal bounds info and representation
19
20 :- use_module(probsrc(error_manager)).
21 :- use_module(library(clpfd)).
22 :- use_module(library(lists)).
23 :- use_module(probsrc(bsyntaxtree),[definitely_not_empty_set/1, create_cartesian_product/3]).
24 :- use_module(clingo_interface,[get_string_nr/2]).
25
26 infer_bounds(Paras,Pred,Res) :- infer_bounds(Paras,Pred,[],Res).
27
28 % infer bounds for quantified typed ids inside predicate Pred
29 % valid options are labeling: which forces a CLP(FD) labeling of the bounds variables to check for consistency
30 infer_bounds(Paras,Pred,Options,_Res) :-
31 new_env(Env,Options),
32 format(user_output,'Inferring bounds for: ~w~n',[Paras]),
33 bb_put(infer_bounds_result,contradiction_found),
34 (add_typed_ids(Paras,LocalBoundsInfo,Env,Env2),
35 infer_pred_bounds(Pred,Env2)
36 -> portray_env(Env2),
37 (label_env(Env2,Options)
38 -> bb_put(infer_bounds_result,LocalBoundsInfo)
39 ; format(user_output,'No consistent labelled solution exists, predicate unsatisfiable~n',[])
40 )
41 ; format(user_output,'No consistent solution exists, predicate unsatisfiable~n',[])
42 ),
43 fail. % to avoid pending co-routines / CLPFD variables we fail and recover the result with bb_get:
44 infer_bounds(_,_,_,Res) :- bb_get(infer_bounds_result,Res).
45
46
47 infer_pred_bounds(b(Pred,pred,_Infos),Env) :- !,
48 % format(user_output,' pred --> ~w~n',[Pred]),
49 infer_pred_bounds(Pred,Env).
50 infer_pred_bounds(conjunct(A,B),Env) :- !,
51 infer_pred_bounds(A,Env),
52 infer_pred_bounds(B,Env).
53 % TODO: disjunct: copy env, and then perform LUB
54 infer_pred_bounds(truth,_) :- !.
55 infer_pred_bounds(member(A,B),Env) :-
56 infer_scalar_bounds(A,Env,SetBoundsA),
57 infer_set_bounds(B,Env,SetBoundsB), !,
58 mem_bounds(SetBoundsA,SetBoundsB).
59 infer_pred_bounds(SubsetAB,Env) :- is_subset(SubsetAB,A,B,EmptyA,EmptyB),
60 infer_set_bounds(A,Env,SetBoundsA),
61 infer_set_bounds(B,Env,SetBoundsB), !,
62 force_non_empty(EmptyA,SetBoundsA),
63 force_non_empty(EmptyB,SetBoundsB),
64 subset_bounds(SetBoundsA,SetBoundsB).
65 infer_pred_bounds(equal(A,B),Env) :- is_scalar(A),
66 infer_scalar_bounds(A,Env,ScBoundsA),
67 infer_scalar_bounds(B,Env,ScBoundsB), !,
68 eq_bounds(ScBoundsA,ScBoundsB).
69 infer_pred_bounds(equal(A,B),Env) :- is_set(A),
70 infer_set_bounds(A,Env,SetBoundsA),
71 infer_set_bounds(B,Env,SetBoundsB), !,
72 eq_bounds(SetBoundsA,SetBoundsB).
73 infer_pred_bounds(BOP,Env) :-
74 scalar_binary_pred(BOP,A,B,ClpfdOp),
75 infer_scalar_bounds(A,Env,BoundsA),
76 infer_scalar_bounds(B,Env,BoundsB), !,
77 apply_binary_pred(ClpfdOp,BoundsA,BoundsB).
78 infer_pred_bounds(Uncov,_Env) :- write(user_output,uncovered_pred(Uncov)), nl(user_output).
79
80 is_scalar(A) :- get_texpr_type(A,integer).
81 is_scalar(A) :- get_texpr_type(A,string).
82 is_scalar(A) :- get_texpr_type(A,couple(_,_)).
83 is_set(A) :- get_texpr_type(A,TA), is_set_type(TA,_).
84
85 % check if we have a predicate that we should treat like subset
86 is_subset(subset(A,B),A,B, can_be_empty,can_be_empty).
87 is_subset(subset_strict(A,B),A,B,can_be_empty,non_empty).
88 is_subset(member(A,PB),A,B,EmptyA,EmptyB) :- is_pow(PB,B,EmptyA,EmptyB).
89 is_subset(member(A,RelFun),A,Cart,can_be_empty,can_be_empty) :- is_rel_fun(RelFun,Dom,Ran),
90 create_cartesian_product(Dom,Ran,Cart).
91
92 is_rel_fun(b(P,_,_),Dom,Ran) :- is_rel_fun(P,Dom,Ran).
93 is_rel_fun(relations(A,B),A,B).
94 is_rel_fun(total_relation(A,B),A,B).
95 is_rel_fun(partial_function(A,B),A,B).
96 is_rel_fun(partial_injection(A,B),A,B).
97 is_rel_fun(partial_surjection(A,B),A,B).
98 is_rel_fun(partial_bijection(A,B),A,B).
99 is_rel_fun(total_function(A,B),A,B).
100 is_rel_fun(total_injection(A,B),A,B).
101 is_rel_fun(total_surjection(A,B),A,B).
102 is_rel_fun(total_bijection(A,B),A,B).
103 is_rel_fun(perm(B),A,B) :- iset(A,'NATURAL1').
104 is_rel_fun(seq(B),A,B) :- iset(A,'NATURAL1').
105 is_rel_fun(iseq(B),A,B) :- iset(A,'NATURAL1').
106 is_rel_fun(seq1(B),A,B) :- iset(A,'NATURAL1').
107 is_rel_fun(iseq1(B),A,B) :- iset(A,'NATURAL1').
108
109 iset(b(integer_set(SET),set(integer),[]),SET).
110
111 is_pow(b(P,_,_),B,EmptyA,EmptyB) :- is_pow(P,B,EmptyA,EmptyB).
112 is_pow(pow_subset(B),B, can_be_empty,can_be_empty).
113 is_pow(pow1_subset(B),B,non_empty,non_empty).
114 is_pow(fin_subset(B),B, can_be_empty,can_be_empty).
115 is_pow(fin1_subset(B),B,non_empty,non_empty).
116
117 force_non_empty(non_empty,binterval(_,_,NonEmpty)) :- !, NonEmpty=1.
118 force_non_empty(_,_).
119
120 scalar_binary_pred(less(A,B),A,B,'#<').
121 scalar_binary_pred(greater(A,B),A,B,'#>').
122 scalar_binary_pred(less_equal(A,B),A,B,'#=<').
123 scalar_binary_pred(greater_equal(A,B),A,B,'#>=').
124
125 apply_binary_pred(Pred,bint(A),bint(B)) :- !,
126 if(call(Pred,A,B),true, % TODO: catch overflows
127 (format(user_output,'Inconsistent ~w ~w ~w constraint!~n',[A,Pred,B]),fail)).
128 apply_binary_pred(ClpfdOp,BoundsA,BoundsB) :-
129 add_internal_error('Illegal call: ',apply_binary_pred(ClpfdOp,BoundsA,BoundsB)), fail.
130
131
132 mem_bounds(BoundsInfo,SetBounds) :- format(user_output,'member ~w ~w~n',[BoundsInfo,SetBounds]),
133 if(mem_bounds2(BoundsInfo,SetBounds),true,
134 (format(user_output,'Inconsistent ~w : ~w constraint!~n',[BoundsInfo,SetBounds]),fail)).
135 mem_bounds2(bint(X),binterval(A,B,NonEmpty)) :- !,
136 NonEmpty = 1, % set must be non-empty to contain an element
137 (number(A),number(B) -> X in A..B ; X #>=A #/\ X #=< B).
138 mem_bounds2(bcouple(X,Y),bcart(BoundsA,BoundsB,NonEmpty)) :- !,
139 NonEmpty = 1,
140 mem_bounds2(X,BoundsA), mem_bounds2(Y,BoundsB).
141 mem_bounds2(A,B) :- format(user_output,'Uncovered mem_bounds ~w : ~w~n',[A,B]).
142
143 :- block subset_list(-,?).
144 subset_list([],_).
145 subset_list([H|T],List2) :- member(H,List2), !, % will instantiate List2 if necessary
146 subset_list(T,List2).
147
148 eq_bounds(BoundsInfo,BoundsInfo2) :- format(user_output,'eq bounds: ~w = ~w~n',[BoundsInfo,BoundsInfo2]),
149 if(eq_bounds2(BoundsInfo,BoundsInfo2),true,
150 (format(user_output,'Inconsistent ~w = ~w constraint!~n',[BoundsInfo,BoundsInfo2]),fail)).
151 eq_bounds2(binterval(A,B,NonEmpty),binterval(A2,B2,NonEmpty2)) :- !,
152 NonEmpty=NonEmpty2,
153 eq_interval(NonEmpty,A,B,A2,B2).
154 eq_bounds2(bint(A),bint(B)) :- !, A=B.
155 eq_bounds2(bcouple(A1,A2),bcouple(B1,B2)) :- !, eq_bounds2(A1,B1), eq_bounds2(A2,B2).
156 eq_bounds2(bcart(A1,A2,NonEmptyA),bcart(B1,B2,NonEmptyB)) :- !,
157 NonEmptyA=NonEmptyB,
158 eq_cart(NonEmptyA,A1,B1,A2,B2).
159 eq_bounds2(_,_).
160
161 :- block eq_interval(-,?,?,?,?).
162 eq_interval(0,_,_,_,_). % both empty
163 eq_interval(1,A,B,X,Y) :- (A,B) = (X,Y).
164 :- block eq_cart(-,?,?,?,?).
165 %eq_cart(NE,A1,B1,A2,B2) :- write(user_output,eq_cart(NE,A1,B1,A2,B2)),nl(user_output),fail.
166 eq_cart(0,_,_,_,_). % both cartesian products empty
167 eq_cart(1,A1,B1,A2,B2) :- eq_bounds2(A1,B1), eq_bounds2(A2,B2).
168 :- block eq_list(-,?,?).
169 eq_list(0,_,_). % both cartesian products empty
170 eq_list(1,A,B) :- subset_list(A,B), subset_list(B,A).
171
172 subset_bounds(BoundsInfo,SetBounds) :- format(user_output,'subset_bounds ~w ~w~n',[BoundsInfo,SetBounds]),
173 if(subset_bounds2(BoundsInfo,SetBounds),true,
174 (format(user_output,'Inconsistent ~w <: ~w constraint!~n',[BoundsInfo,SetBounds]),fail)).
175 subset_bounds2(binterval(X,Y,NonEmptyXY),binterval(A,B,NonEmptyAB)) :- !,
176 NonEmptyXY #=< NonEmptyAB, % if RHS A..B is empty then so is LHS X..Y
177 subset_interval(X,Y,NonEmptyXY,A,B,NonEmptyAB).
178 subset_bounds2(bcart(X,Y,NonEmptyXY),bcart(A,B,NonEmptyAB)) :- !,
179 NonEmptyXY #=< NonEmptyAB, % if RHS is empty then so is LHS
180 subset_cart(X,Y,NonEmptyXY,A,B,NonEmptyAB).
181 subset_bounds2(A,B) :- format(user_output,'Uncovered subset_bounds2 ~w : ~w~n',[A,B]).
182
183 :- block subset_interval(?,?,-,?,?,?).
184 subset_interval(_,_,0,_,_,_). % first set empty
185 subset_interval(X,Y,1,A,B,1) :- (X#>= A #/\ Y #=< B).
186
187 :- block subset_cart(?,?,-,?,?,?).
188 subset_cart(_,_,0,_,_,_). % first set empty
189 subset_cart(X,Y,1,A,B,1) :- subset_bounds2(X,A), subset_bounds2(Y,B).
190
191 % --------
192 % SETS
193 % --------
194
195 :- use_module(library(avl),[avl_min/2, avl_max/2, avl_member/2]).
196
197 infer_set_bounds(b(E,Type,_Infos),Env,Bounds) :- !,
198 (finite_type(Type) -> Bounds = Type % we could try and infer bounds for fd(_,_) global set values
199 ; infer_set_bounds(E,Type,Env,Bounds)).
200 infer_set_bounds(empty_set,set(integer),_,Bounds) :- !, Bounds = binterval(1,0,0).
201 infer_set_bounds(integer_set('NATURAL'),set(integer),_,Bounds) :- !, init_binterval(0,_,Bounds,1).
202 infer_set_bounds(integer_set('NATURAL1'),set(integer),_,Bounds) :- !, init_binterval(1,_,Bounds,1).
203 infer_set_bounds(value(AVL),set(integer),_Env,Bounds) :- nonvar(AVL), AVL=avl_set(A), !,
204 avl_min(A,int(Min)), %min_of_explicit_set_wf(Val,int(Min),no_wf_available),
205 avl_max(A,int(Max)), Bounds = binterval(Min,Max,1).
206 infer_set_bounds(value(AVL),set(string),_Env,Bounds) :- nonvar(AVL), AVL=avl_set(A), !,
207 findall(Nr,(avl_member(string(S),A), get_string_nr(S,Nr)),Nrs),
208 min_member(Min,Nrs), max_member(Max,Nrs), Bounds = binterval(Min,Max,1).
209 infer_set_bounds(interval(A,B),_,Env,Bounds) :- !,
210 infer_scalar_bounds(A,Env,bint(BA)),
211 infer_scalar_bounds(B,Env,bint(BB)),
212 init_binterval(BA,BB,Bounds,_).
213 infer_set_bounds(intersection(A,B),_,Env,Bounds) :- !,
214 infer_set_bounds(A,Env,BoundsA),
215 infer_set_bounds(B,Env,BoundsB), % TODO: treat if one of the two calls fails
216 intersect_bounds(BoundsA,BoundsB,Bounds).
217 infer_set_bounds(union(A,B),_,Env,Bounds) :- !,
218 infer_set_bounds(A,Env,BoundsA),
219 infer_set_bounds(B,Env,BoundsB),
220 union_bounds(BoundsA,BoundsB,Bounds).
221 infer_set_bounds(set_extension(List),_,Env,Bounds) :- !,
222 (List = [A], infer_scalar_bounds(A,Env,bint(BA))
223 -> Bounds = binterval(BA,BA,1)
224 ; maplist(infer_set_ext_el(Env,Bounds),List)
225 % TODO: use union code instead? we loose info that these are all the elements of the set
226 ).
227 infer_set_bounds(identifier(A),Type,Env,Bounds) :- !,
228 lookup_id_bounds(A,Env,Type,Bounds).
229 infer_set_bounds(cartesian_product(A,B),_,Env,Bounds) :- !,
230 infer_set_bounds(A,Env,BoundsA),
231 infer_set_bounds(B,Env,BoundsB),
232 construct_bcart(A,B,BoundsA,BoundsB,Bounds).
233 infer_set_bounds(domain(A),_,Env,DomBounds) :- !,
234 infer_set_bounds(A,Env,bcart(DomBounds,_,NE)),
235 imply_non_empty(DomBounds,NE). % if domain is non-empty, then full relation must be non-empty
236 infer_set_bounds(range(A),_,Env,RanBounds) :- !,
237 infer_set_bounds(A,Env,bcart(_,RanBounds,NE)),
238 imply_non_empty(RanBounds,NE). % if range is non-empty, then full relation must be non-empty
239 infer_set_bounds(image(Rel,_Set),Type,Env,RanBounds) :- !,
240 infer_set_bounds(range(Rel),Type,Env,RanBounds). % we ignore Set
241 infer_set_ext_el(Env,Bounds,A) :-
242 (infer_scalar_bounds(A,Env,BoundsA)
243 -> mem_bounds(BoundsA,Bounds)
244 ; format(user_output,'Cannot infer bounds for set-ext element:~w~n',[A])
245 ).
246
247 intersect_bounds(binterval(Low1,Up1,NE1),binterval(Low2,Up2,NE2),Bounds) :-
248 init_binterval(Low,Up,Bounds,NE),
249 NE #=< NE1, % if set1 empty intersection empty
250 NE #=< NE2, % ditto for set 2
251 Low #= max(Low1,Low2), Up #= min(Up1,Up2).
252 union_bounds(binterval(Low1,Up1,NE1),binterval(Low2,Up2,NE2),Bounds) :-
253 init_binterval(Low,Up,Bounds,NE),
254 NE1 #=< NE, % if union empty then set1 empty
255 NE2 #=< NE, % ditto for set 2
256 NE #=< NE1+NE2, % if set1 & set2 empty then union is empty
257 (NE1 #= 0) #=> (Low #= Low2 #/\ Up #= Up2), % if set1 empty we copy set2 to result
258 (NE1 #= 1 #/\ NE2 #= 1) #=> (Low #= min(Low1,Low2) #/\ Up #= max(Up1,Up2)).
259
260 init_binterval(Low,Up,binterval(Low,Up,NonEmpty),NonEmpty) :-
261 NonEmpty #<=> (Low #=< Up).
262
263 % construct a bcart/3 term; setting up non-empty flag
264 construct_bcart(A,B,BA,BB,bcart(BA,BB,NonEmptyAB)) :- NonEmptyAB in 0..1,
265 (get_non_empty_flag(A,BA,NonEmptyA),
266 get_non_empty_flag(B,BB,NonEmptyB)
267 -> NonEmptyAB #= NonEmptyA*NonEmptyB % or minimum of both; if one set empty (0) then cartesian product empty
268 ; format(user_output,'Could not get non-empty-flags: ~w * ~w~n',[A,B])
269 ).
270
271 get_non_empty_flag(Expr,Bounds,NonEmpty) :-
272 (definitely_not_empty_set(Expr) -> NonEmpty=1
273 , format(user_output,'Def non-empty: ~w~n',[Expr])
274 ; get_non_empty_flag(Bounds,NonEmpty)).
275
276 get_non_empty_flag(binterval(_,_,NE),R) :- !, R=NE.
277 get_non_empty_flag(bcart(_,_,NE),R) :- !, R=NE.
278 get_non_empty_flag(_,NE) :-
279 NE in 0..1. % we don't know if set is empty or not; TODO: use definitely_not_empty !?
280
281 % if bounds are non-empty force another non-empty flag to be 1
282 imply_non_empty(Bounds,NonEmptyFlag) :- get_non_empty_flag(Bounds,NE),
283 imply_block(NE,NonEmptyFlag).
284 :- block imply_block(-,?).
285 imply_block(1,1).
286 imply_block(0,_).
287
288 % SCALARS
289 % --------
290
291 :- use_module(probsrc(bsyntaxtree),[is_set_type/2]).
292 :- use_module(probsrc(kernel_objects),[max_cardinality/2]).
293 infer_scalar_bounds(b(E,T,_Infos),Env,Bounds) :- !,
294 (finite_type(T) -> Bounds = T % we could try and infer bounds for fd(_,_) global set values
295 ; infer_scalar_bounds2(E,T,Env,Bounds)).
296 infer_scalar_bounds2(integer(A),_,_Env,Bounds) :- !, Bounds = bint(A).
297 infer_scalar_bounds2(string(A),_,_Env,Bounds) :- !, get_string_nr(A,Nr),Bounds = bint(Nr).
298 infer_scalar_bounds2(identifier(A),Type,Env,Bounds) :- !, lookup_id_bounds(A,Env,Type,Bounds).
299 infer_scalar_bounds2(card(A),integer,_Env,bint(Card)) :-
300 %infer_set_bounds(A,Env,binterval(Low,Up)),
301 !,
302 % TODO: if Low <= Up -> Card #= 1+Up-Low else = 0
303 (get_texpr_type(A,AType),is_set_type(AType,SType),
304 max_cardinality(SType,MaxCard),number(MaxCard)
305 -> Card in 0..MaxCard ; Card #>= 0).
306 infer_scalar_bounds2(couple(A,B),couple(_TA,_TB),Env,bcouple(BA,BB)) :- !,
307 infer_scalar_bounds(A,Env,BA), % TODO: treat if one of them fails / is finite
308 infer_scalar_bounds(B,Env,BB).
309 infer_scalar_bounds2(function(Rel,_Arg),Type,Env,Bounds) :- !,
310 infer_set_bounds(range(Rel),set(Type),Env,RanBounds), % we ignore Arg
311 %convert_set_bounds_to_scalar(RanBounds,Bounds). % we could use this if TRY_FIND_ABORT is TRUE
312 if(mem_bounds(Bounds,RanBounds),
313 true,
314 create_dummy_value(RanBounds,Bounds)). % empty range probably meaning WD error; just return a concrete dummy value
315 infer_scalar_bounds2(BOP,_,Env,Bounds) :-
316 scalar_binary_op(BOP,A,B,ClpfdOp), !,
317 infer_scalar_bounds(A,Env,BoundsA),
318 infer_scalar_bounds(B,Env,BoundsB),
319 apply_binary_op(ClpfdOp,Bounds,BoundsA,BoundsB).
320 infer_scalar_bounds2(BOP,_,_,_) :- write(user_output,uncov_scalar(BOP)),nl(user_output),fail.
321
322 %convert_set_bounds_to_scalar(binterval(A,B,NonEmpty),bint(X)) :-
323 % (NonEmpty#=1) #=> (X #>= A #/\ X #=< B).
324
325 % create a dummy element for given bounds
326 create_dummy_value(binterval(A,_,_),bint(DA)) :- !, (var(A),fd_min(A,Min),number(Min) -> DA=Min ; DA=0).
327 create_dummy_value(bcart(A,B,_),bcouple(DA,DB)) :- !, create_dummy_value(A,DA), create_dummy_value(B,DB).
328 create_dummy_value(T,T) :- finite_type(T).
329
330 scalar_binary_op(add(A,B),A,B,'+').
331 scalar_binary_op(multiplication(A,B),A,B,'*').
332 scalar_binary_op(minus(A,B),A,B,'-').
333 apply_binary_op(Op,bint(Res),bint(A),bint(B)) :- !, RHS =.. [Op,A,B],
334 if(call('#=',Res,RHS),true, % TODO: catch overflows
335 (format(user_output,'Inconsistent ~w #= (~w ~w ~w) constraint!',[Res, A,Op,B]),fail)).
336 apply_binary_op(ClpfdOp,Bounds,BoundsA,BoundsB) :-
337 add_internal_error('Illegal call: ',apply_binary_op(ClpfdOp,Bounds,BoundsA,BoundsB)), fail.
338
339 :- use_module(probsrc(bsyntaxtree), [def_get_texpr_id/2, get_texpr_id/2, get_texpr_type/2]).
340
341 %relevant_identifier(TID,Env,ID,BoundsInfo) :- get_texpr_id(TID,ID),
342 % lookup_id_bounds(ID,Env,_,BoundsInfo).
343
344
345 % environment utilities:
346
347 new_env(env(E,_),Opts) :-
348 (member(outer_bounds(OB),Opts)
349 -> maplist(add_outer_bound_info,OB,E)
350 % outer bounds are already ground and need no labeling; they provide bounds for outer variables
351 ; member(open,Opts) -> true ; E=[]).
352
353 lookup_id_bounds(ID,env(Env,_),Type,BoundsInfo) :-
354 (member(bound_internal_info(ID,Type,StoredBounds),Env)
355 -> BoundsInfo=StoredBounds
356 ; format(user_output,'Could not find identifier ~w !!~n',[ID]),
357 bounds_type(Type,BoundsInfo,_)). % set up unconstrained bounds
358
359 % add typed ids to environment, also returns list of bounds information for added ids
360 add_typed_ids([],[]) --> [].
361 add_typed_ids([TID|T],[BoundsInfo|TB]) --> add_typed_id(TID,BoundsInfo), add_typed_ids(T,TB).
362
363 add_typed_id(TID,bound_id_info(ID,Type,Bounds),env(Env,Flags),env(NewEnv,Flags)) :- def_get_texpr_id(TID,ID),
364 get_texpr_type(TID,Type),
365 NewEnv = [bound_internal_info(ID,Type,Fresh)|Env],
366 (bounds_type(Type,Fresh,_)
367 -> compute_bound_info(ID,Type,Fresh,Bounds,Flags)
368 ; format(user_output,'Ignoring identifier ~w in analysis~n',[ID]),
369 Fresh=Type, Bounds=Type),
370 label_id(ID,Type,Fresh,Flags).
371
372 % add information from outer variables (e.g., computed by infer_bounds for outer predicate)
373 add_outer_bound_info(bound_id_info(ID,Type,Bounds),bound_internal_info(ID,Type,InternalType)) :-
374 convert_bounds_to_internal(Bounds,InternalType).
375
376 convert_bounds_to_internal(integer_in_range(From,To,_),bint(X)) :- !, X in From..To.
377 convert_bounds_to_internal(set(integer_in_range(From,To,_)),binterval(From2,To2,_NonEmpty)) :- !,
378 (number(From) -> From2=From ; true), (number(To) -> To2=To ; true).
379 % we do not know if set is empty or not;
380 % see test 2519 :clingo-double-check x<:1..3 & !y.(y:0..3 & x*(1..2)=(1..2)*(1..y) => y=2)
381 convert_bounds_to_internal(string,bint(Nr)) :- !, Nr #>= 0. % strings number start at 0
382 convert_bounds_to_internal(set(string),binterval(From,_To,_NonEmpty)) :- !,
383 From #>= 0.
384 convert_bounds_to_internal(set(couple(A,B)),BCart) :- !,
385 convert_bounds_to_internal(set(A),BA),
386 convert_bounds_to_internal(set(B),BB),
387 Dummy = b(empty_set,any,[]),
388 construct_bcart(Dummy,Dummy,BA,BB,BCart).
389 convert_bounds_to_internal(X,X).
390
391 finite_type(boolean).
392 finite_type(global(_GS)).
393 finite_type(set(X)) :- finite_type(X).
394 finite_type(couple(X,Y)) :- finite_type(X), finite_type(Y).
395
396 % a type for which we can determine bounds:
397 % it also returns a 0..1 CLP(FD) flag for non-emptyness; useful for sets only
398 bounds_type(integer,bint(_),1).
399 bounds_type(string,bint(_),1).
400 bounds_type(set(integer),binterval(_,_,NonEmpty),NonEmpty).
401 bounds_type(set(string),binterval(_,_,NonEmpty),NonEmpty).
402 bounds_type(couple(A,B),bcouple(BA,BB),1) :-
403 bounds_of_pair(A,B,BA,BB,_). % at least one part requires bounds
404 bounds_type(set(couple(A,B)),bcart(BA,BB,NonEmpty),NonEmpty) :-
405 bounds_of_pair(set(A),set(B),BA,BB,NonEmpty).
406
407 % get bounds of two types, ensuring at least one of them requires bounds inference
408 bounds_of_pair(A,B,BA,BB,NonEmpty) :-
409 (bounds_type(A,BA,NEA)
410 -> (bounds_type(B,BB,NEB) -> NonEmpty #= min(1,NEA+NEB)
411 ; BB=B, NonEmpty=NEA)
412 ; BA=A, bounds_type(B,BB,NonEmpty)).
413
414 :- block compute_bound_info(?,?,?,?,-).
415 compute_bound_info(ID,Type,Fresh,Bounds,_) :-
416 get_bounds(Fresh,Type,Bounds),
417 format(user_output,'Computed bounds ~w : ~w --> ~w~n',[ID,Type,Bounds]).
418
419 % get bounds of an internal representation into format suitable for b2asp / other tools
420 % it creates a type term, using integer_in_range/2 in place of integer
421 get_bounds(bint(X),Type,integer_in_range(Min,Max,Type)) :- !, fd_min(X,Min), fd_max(X,Max).
422 get_bounds(binterval(X,Y,NonEmpty),set(Type),set(integer_in_range(Min,Max,Type))) :- !,
423 ( NonEmpty == 0 -> Min=1, Max=0
424 ; NonEmpty == 1 -> fd_min(X,Min), fd_max(Y,Max)
425 ; get_non_empty_interval_bounds(X,Y,NonEmpty,Min,Max) % we do not know if set empty or not
426 ).
427 get_bounds(bcouple(A,B),couple(TA,TB),couple(BA,BB)) :- !, get_bounds(A,TA,BA), get_bounds(B,TB,BB).
428 get_bounds(bcart(A,B,NonEmpty),set(couple(TA,TB)),set(couple(BA,BB))) :- !,
429 ( NonEmpty == 0 -> get_bounds(A,set(TA),set(BA)), get_bounds(B,set(TB),set(BB)) % we could return empty_set for BA/BB
430 ; NonEmpty == 1 -> get_bounds(A,set(TA),set(BA)), get_bounds(B,set(TB),set(BB))
431 ; get_non_empty_cart_bounds(A,B,TA,TB,NonEmpty,BA,BB) % we do not know if cartesian product empty or not
432 ).
433 get_bounds(B,_,R) :- finite_type(B),!, R=B.
434 get_bounds(B,Type,R) :- format(user_output,'Unknown bound: ~w (type ~w)~n',[B,Type]), R=B.
435
436 % try get bounds assuming set is non-empty; these bounds will be used for enumeration in clingo
437 get_non_empty_interval_bounds(X,Y,NonEmpty,_,_) :-
438 bb_put(bounds_analysis_min_max,(1,0)), % if propagation fails the set must be empty
439 (NonEmpty=1 % force non-empty and check to see in which range the values must be
440 -> fd_min(X,Min2), fd_max(Y,Max2),
441 bb_put(bounds_analysis_min_max,(Min2,Max2))
442 ; format(user_output,'Bounds interval cannot be non-empty~n',[])
443 ),
444 fail.
445 get_non_empty_interval_bounds(_,_,_,Min,Max) :- bb_get(bounds_analysis_min_max,(Min,Max)).
446
447 % try get bounds assuming cartesian product is non-empty; these bounds will be used for enumeration in clingo
448 get_non_empty_cart_bounds(A,B,TA,TB,NonEmpty,_,_) :-
449 bb_put(bounds_analysis_cart,(empty_set,empty_set)), % if propagation fails the set must be empty
450 (NonEmpty=1 % force non-empty and check to see in which range the values must be
451 -> get_bounds(A,set(TA),set(BA)), get_bounds(B,set(TB),set(BB)),
452 bb_put(bounds_analysis_cart,(BA,BB))
453 ; format(user_output,'Bounds cartesian product cannot be non-empty~n',[])
454 ),
455 fail.
456 get_non_empty_cart_bounds(_,_,_,_,_,BA,BB) :- bb_get(bounds_analysis_cart,(BA,BB)).
457
458
459 :- block label_id(?,?,?,-).
460 label_id(_ID,_Type,Fresh,copy_bounds(Flag)) :- %format(user_output,'Labeling ~w : ~w~n',[ID,Fresh]),
461 label_bounds(Fresh,Flag).
462
463 % TODO: check if finite:
464 :- block label_bounds(?,-).
465 label_bounds(_,no_labeling) :- !.
466 label_bounds(bint(X),_) :- !, label_fd_var(X).
467 label_bounds(binterval(X,Y,Empty),_) :- !, (Empty=0 ; Empty=1), label_fd_var(X), label_fd_var(Y).
468 label_bounds(bcouple(X,Y),F) :- !, label_bounds(X,F), label_bounds(Y,F).
469 label_bounds(bcart(X,Y,Empty),F) :- !, (Empty=0 ; Empty=1), label_bounds(X,F), label_bounds(Y,F).
470 label_bounds(Term,_) :- ground(Term),finite_type(Term),!.
471 label_bounds(Term,_) :- add_internal_error('Unknown bounds info to label:', label_bounds(Term)).
472
473 label_fd_var(X) :- fd_size(X,Sz), (number(Sz) -> indomain(X) ; true).
474
475
476 portray_env(env(NE,_)) :- portray_env2(NE).
477 portray_env2(X) :- var(X),!, write(user_output,' - ... '),nl(user_output).
478 portray_env2([]) :- !.
479 portray_env2([bound_internal_info(ID,Type,BoundsInfo)|TT]) :- !,
480 format(user_output,' - ~w (~w) : ',[ID,Type]), portray_bounds(BoundsInfo), nl(user_output),
481 portray_env2(TT).
482 portray_env2(E) :-
483 format(user_output,' *** ILLEGAL ENV *** ~w~n',[E]).
484
485 portray_bounds(bint(X)) :- !, portray_int(X).
486 portray_bounds(binterval(X,Y,_E)) :- !,
487 write(user_output,'('), portray_int(X), write(user_output,' .. '), portray_int(Y), write(user_output,')').
488 portray_bounds(bcouple(X,Y)) :- !, portray_bounds(X), write(user_output,' , '), portray_bounds(Y).
489 portray_bounds(bcart(X,Y,_E)) :- !, portray_bounds(X), write(user_output,' * '), portray_bounds(Y).
490 portray_bounds(T) :- finite_type(T), !, write(user_output,T).
491 portray_bounds(U) :- write(user_output,'*** UNKNOWN '), write(user_output,U), write(user_output,' ***').
492
493 portray_int(X) :- nonvar(X),!, write(user_output,X).
494 portray_int(X) :- fd_dom(X,Dom), write(user_output,Dom).
495
496 label_env(env(_,Flags),Options) :- !,Flags=copy_bounds(F2),
497 (member(label,Options) -> F2=label_now ; F2=no_labeling).
498 label_env(E,_) :- add_internal_error('Illegal env: ', label_env(E)).
499
500
501
502 /*
503
504 Encode set union constraints using single fd variable:
505
506 | ?- X in 1..3, Y in 2..5, element([X,Y],Z).
507 X in 1 .. 3,
508 Y in 2 .. 5,
509 Z in 1 .. 5 ?
510
511 Intersection:
512 | ?- X in 1..3, Y in 2..5, element([X],Z), element([Y],Z).
513 X in 2 .. 3,
514 Y in 2 .. 3,
515 Z in 2 .. 3 ?
516 yes
517
518 But how do we encode empty set?
519 | ?- X in 1..3, Y in 4..5, element([X],Z), element([Y],Z).
520 no
521
522 */