1		% (c) 2025-2026 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		:- meta_predicate apply_binary_pred(2,-,-).
21
22		:- use_module(probsrc(error_manager)).
23		:- use_module(probsrc(debug),[debug_format/3, debug_mode/1]).
24		:- use_module(library(clpfd)).
25		:- use_module(library(lists)).
26		:- use_module(probsrc(bsyntaxtree),[definitely_not_empty_set/1, create_cartesian_product/3]).
27		:- use_module(clingo_interface,[get_string_nr/2]).
28
29		infer_bounds(Paras,Pred,Res) :- infer_bounds(Paras,Pred,[],Res).
30
31		% infer bounds for quantified typed ids inside predicate Pred
32		% valid options are labeling: which forces a CLP(FD) labeling of the bounds variables to check for consistency
33		infer_bounds(Paras,Pred,Options,_Res) :-
34		new_env(Env,Options),
35		debug_format(19,'Inferring bounds for: ~w~n',[Paras]),
36		bb_put(infer_bounds_result,contradiction_found),
37		(add_typed_ids(Paras,LocalBoundsInfo,BAR,Env,Env2),
38		(BAR==bounds_analysis_required -> infer_pred_bounds(Pred,Env2) ; debug_format(19,'No Bounds Analysis required',[]))
39		-> (debug_mode(on) -> portray_env(Env2) ; true),
40		(label_env(Env2,Options)
41		-> bb_put(infer_bounds_result,LocalBoundsInfo)
42		; format(user_output,'No consistent labelled solution exists, predicate unsatisfiable~n',[])
43		)
44		; format(user_output,'No consistent solution exists, predicate unsatisfiable~n',[])
45		),
46		fail. % to avoid pending co-routines / CLPFD variables we fail and recover the result with bb_get:
47		infer_bounds(_,_,_,Res) :- bb_get(infer_bounds_result,Res).
48
49
50		infer_pred_bounds(b(Pred,pred,_Infos),Env) :- !,
51		% format(user_output,' pred --> ~w~n',[Pred]),
52		infer_pred_bounds(Pred,Env).
53		infer_pred_bounds(conjunct(A,B),Env) :- !,
54		infer_pred_bounds(A,Env),
55		infer_pred_bounds(B,Env).
56		% TODO: disjunct: copy env, and then perform LUB
57		infer_pred_bounds(truth,_) :- !.
58		infer_pred_bounds(SubsetAB,Env) :- is_subset(SubsetAB,A,B,EmptyA,EmptyB),
59		infer_set_bounds(A,Env,SetBoundsA),
60		infer_set_bounds(B,Env,SetBoundsB), !,
61		force_non_empty(EmptyA,SetBoundsA),
62		force_non_empty(EmptyB,SetBoundsB),
63		subset_bounds(SetBoundsA,SetBoundsB).
64		infer_pred_bounds(member(A,B),Env) :-
65		infer_scalar_bounds(A,Env,SetBoundsA),
66		infer_set_bounds(B,Env,SetBoundsB), !,
67		mem_bounds(SetBoundsA,SetBoundsB).
68		infer_pred_bounds(equal(A,B),Env) :- is_scalar(A),
69		infer_scalar_bounds(A,Env,ScBoundsA),
70		infer_scalar_bounds(B,Env,ScBoundsB), !,
71		eq_bounds(ScBoundsA,ScBoundsB).
72		infer_pred_bounds(equal(A,B),Env) :- is_set(A),
73		infer_set_bounds(A,Env,SetBoundsA),
74		infer_set_bounds(B,Env,SetBoundsB), !,
75		eq_bounds(SetBoundsA,SetBoundsB).
76		infer_pred_bounds(BOP,Env) :-
77		scalar_binary_pred(BOP,A,B,ClpfdOp),
78		infer_scalar_bounds(A,Env,BoundsA),
79		infer_scalar_bounds(B,Env,BoundsB), !,
80		apply_binary_pred(ClpfdOp,BoundsA,BoundsB).
81		infer_pred_bounds(Uncov,_Env) :- %write(user_output,Uncov),nl,
82		(debug_mode(on)
83		-> functor(Uncov,F,N),write(user_output,uncovered_pred_in_bounds_analysis(F/N)),
84		nl(user_output)
85		; true).
86
87		is_scalar(A) :- get_texpr_type(A,integer).
88		is_scalar(A) :- get_texpr_type(A,string).
89		is_scalar(A) :- get_texpr_type(A,couple(_,_)).
90		is_set(A) :- get_texpr_type(A,TA), is_set_type(TA,_).
91
92		%% true if the bounds of sub-expressions cannot be larger than resulting bound
93		%is_monotonic(b(E,_,_)) :- is_monotonic2(E).
94		%is_monotonic2(interval(_,_)).
95		%is_monotonic2(value(_)).
96		%is_monotonic2(empty_set).
97		%is_monotonic2(union(_,_)).
98		%is_monotonic2(identifier(_)).
99		%is_monotonic2(set_extension(_)). % TODO: check
100		%is_monotonic2(cartesian_product(A,B)) :- is_monotonic(A), is_monotonic(B).
101		%is_monotonic2(image(A,B)) :- is_monotonic(A), is_monotonic(B).
102		%is_monotonic2(union(A,B)) :- is_monotonic(A), is_monotonic(B).
103		%is_monotonic2(iteration(A,_)) :- is_monotonic(A).
104		%is_monotonic2(closure(A)) :- is_monotonic(A).
105		%is_monotonic2(reverse(A)) :- is_monotonic(A).
106		%is_monotonic2(intersection(A,B)) :- pure_value(A), pure_value(B).
107		%is_monotonic2(set_subtraction(A,B)) :- pure_value(A), pure_value(B).
108		%%is_monotonic2(NM) :- write(user_output,non_mon(NM)),nl(user_output),fail.
109		%
110		%% value which does not contain an identifier (which can be instantiated somewhere else)
111		%pure_value(b(E,_,_)) :- pure_value2(E).
112		%pure_value2(interval(_,_)).
113		%pure_value2(value(_)).
114		%pure_value2(empty_set).
115		%pure_value2(cartesian_product(A,B)) :- pure_value(A), pure_value(B).
116		%pure_value2(image(A,B)) :- pure_value(A), pure_value(B).
117		%pure_value2(intersection(A,B)) :- pure_value(A), pure_value(B).
118		%pure_value2(set_subtraction(A,B)) :- pure_value(A), pure_value(B).
119		%pure_value2(union(A,B)) :- pure_value(A), pure_value(B).
120
121		% check if we have a predicate that we should treat like subset
122		is_subset(subset(A,B),A,B, can_be_empty,can_be_empty).
123		is_subset(subset_strict(A,B),A,B,can_be_empty,non_empty).
124		is_subset(member(A,PB),A,B,EmptyA,EmptyB) :- is_pow(PB,B,EmptyA,EmptyB).
125		is_subset(member(A,RelFun),A,Cart,can_be_empty,can_be_empty) :- is_rel_fun(RelFun,Dom,Ran),
126		create_cartesian_product(Dom,Ran,Cart).
127
128		is_rel_fun(b(P,_,_),Dom,Ran) :- is_rel_fun(P,Dom,Ran).
129		is_rel_fun(relations(A,B),A,B).
130		is_rel_fun(total_relation(A,B),A,B).
131		is_rel_fun(total_surjection_relation(A,B),A,B).
132		is_rel_fun(surjection_relation(A,B),A,B).
133		is_rel_fun(partial_function(A,B),A,B).
134		is_rel_fun(partial_injection(A,B),A,B).
135		is_rel_fun(partial_surjection(A,B),A,B).
136		is_rel_fun(partial_bijection(A,B),A,B).
137		is_rel_fun(total_function(A,B),A,B).
138		is_rel_fun(total_injection(A,B),A,B).
139		is_rel_fun(total_surjection(A,B),A,B).
140		is_rel_fun(total_bijection(A,B),A,B).
141		is_rel_fun(perm(B),A,B) :- iset(A,'NATURAL1').
142		is_rel_fun(seq(B),A,B) :- iset(A,'NATURAL1').
143		is_rel_fun(iseq(B),A,B) :- iset(A,'NATURAL1').
144		is_rel_fun(seq1(B),A,B) :- iset(A,'NATURAL1').
145		is_rel_fun(iseq1(B),A,B) :- iset(A,'NATURAL1').
146
147		iset(b(integer_set(SET),set(integer),[]),SET).
148
149		is_pow(b(P,_,_),B,EmptyA,EmptyB) :- is_pow(P,B,EmptyA,EmptyB).
150		is_pow(pow_subset(B),B, can_be_empty,can_be_empty).
151		is_pow(pow1_subset(B),B,non_empty,non_empty).
152		is_pow(fin_subset(B),B, can_be_empty,can_be_empty).
153		is_pow(fin1_subset(B),B,non_empty,non_empty).
154
155		force_non_empty(non_empty,binterval(_,_,NonEmpty)) :- !, NonEmpty=1.
156		force_non_empty(_,_).
157
158		scalar_binary_pred(less(A,B),A,B,'#<').
159		scalar_binary_pred(greater(A,B),A,B,'#>').
160		scalar_binary_pred(less_equal(A,B),A,B,'#=<').
161		scalar_binary_pred(greater_equal(A,B),A,B,'#>=').
162
163		apply_binary_pred(Pred,bint(A),bint(B)) :- !,
164		if(call(Pred,A,B),true, % TODO: catch overflows
165		(format(user_output,'Inconsistent ~w ~w ~w constraint!~n',[A,Pred,B]),fail)).
166		apply_binary_pred(ClpfdOp,BoundsA,BoundsB) :-
167		add_internal_error('Illegal call: ',apply_binary_pred(ClpfdOp,BoundsA,BoundsB)), fail.
168
169
170		mem_bounds(BoundsInfo,SetBounds) :- debug_format(19,'member bounds ~w ~w~n',[BoundsInfo,SetBounds]),
171		if(mem_bounds2(BoundsInfo,SetBounds),true,
172		(format(user_output,'Inconsistent ~w : ~w constraint!~n',[BoundsInfo,SetBounds]),fail)).
173		mem_bounds2(bint(X),binterval(A,B,NonEmpty)) :- !,
174		NonEmpty = 1, % set must be non-empty to contain an element
175		(number(A),number(B) -> X in A..B ; X #>=A #/\ X #=< B).
176		mem_bounds2(bcouple(X,Y),bcart(BoundsA,BoundsB,NonEmpty)) :- !,
177		NonEmpty = 1,
178		mem_bounds2(X,BoundsA), mem_bounds2(Y,BoundsB).
179		mem_bounds2(A,B) :- format(user_output,'Uncovered mem_bounds ~w : ~w~n',[A,B]).
180
181		%:- block subset_list(-,?).
182		%subset_list([],_).
183		%subset_list([H|T],List2) :- member(H,List2), !, % will instantiate List2 if necessary
184		% subset_list(T,List2).
185
186		% equal_bounds(BoundsInfo1,BoundsInfo2)
187		% TODO: check the logic and maybe have another precision flag in the bounds-info rather than this monotonic flag
188		eq_bounds(BoundsInfo,BoundsInfo2) :-
189		debug_format(19,'eq bounds: ~w = ~w~n',[BoundsInfo,BoundsInfo2]),
190		if(eq_bounds2(BoundsInfo,BoundsInfo2),true,
191		(format(user_output,'Inconsistent ~w = ~w constraint!~n',[BoundsInfo,BoundsInfo2]),fail)).
192		eq_bounds2(binterval(A,B,NonEmpty),binterval(A2,B2,NonEmpty2)) :- !,
193		NonEmpty=NonEmpty2, % true for non-monotonic ??
194		eq_interval(NonEmpty,A,B,A2,B2).
195		eq_bounds2(bint(A),bint(B)) :- !, A=B.
196		eq_bounds2(bcouple(A1,A2),bcouple(B1,B2)) :- !, eq_bounds2(A1,B1), eq_bounds2(A2,B2).
197		eq_bounds2(bcart(A1,A2,NonEmptyA),bcart(B1,B2,NonEmptyB)) :- !,
198		NonEmptyA=NonEmptyB, % should we do this also for non-monotonic ?
199		eq_cart(NonEmptyA,A1,B1,A2,B2).
200		eq_bounds2(_,_).
201
202		:- block eq_interval(-,?,?,?,?).
203		eq_interval(0,_,_,_,_). % both empty
204		eq_interval(1,Low1,Up1,Low2,Up2) :-
205		(Low1,Up1) = (Low2,Up2).
206		% Note: in case of x /\ 1..3 = {2} --> we could have a solution of x={2,4}
207		% this is now dealt with in intersection
208		:- block eq_cart(-,?,?,?,?).
209		%eq_cart(NE,A1,B1,A2,B2) :- write(user_output,eq_cart(NE,A1,B1,A2,B2)),nl(user_output),fail.
210		eq_cart(0, _,_,_,_). % both cartesian products empty
211		eq_cart(1, A1,B1,A2,B2) :- eq_bounds2(A1,B1), eq_bounds2(A2,B2).
212		%:- block eq_list(-,?,?).
213		%eq_list(0,_,_). % both cartesian products empty
214		%eq_list(1,A,B) :- subset_list(A,B), subset_list(B,A).
215
216		subset_bounds(BoundsInfo,SetBounds) :- %debug_format(9,'subset_bounds ~w ~w~n',[BoundsInfo,SetBounds]),
217		if(subset_bounds2(BoundsInfo,SetBounds),true,
218		(format(user_output,'Inconsistent ~w <: ~w constraint!~n',[BoundsInfo,SetBounds]),fail)).
219		subset_bounds2(binterval(X,Y,NonEmptyXY),binterval(A,B,NonEmptyAB)) :- !,
220		NonEmptyXY #=< NonEmptyAB, % if RHS A..B is empty then so is LHS X..Y
221		subset_interval(X,Y,NonEmptyXY,A,B,NonEmptyAB).
222		subset_bounds2(bcart(X,Y,NonEmptyXY),bcart(A,B,NonEmptyAB)) :- !,
223		NonEmptyXY #=< NonEmptyAB, % if RHS is empty then so is LHS
224		subset_cart(X,Y,NonEmptyXY,A,B,NonEmptyAB).
225		subset_bounds2(A,B) :- format(user_output,'Uncovered subset_bounds2 ~w : ~w~n',[A,B]).
226
227		:- block subset_interval(?,?,-,?,?,?).
228		subset_interval(_,_,0,_,_,_). % first set empty
229		subset_interval(X,Y,1,A,B,1) :- (X#>= A #/\ Y #=< B).
230
231		:- block subset_cart(?,?,-,?,?,?).
232		subset_cart(_,_,0,_,_,_). % first set empty
233		subset_cart(X,Y,1,A,B,1) :- subset_bounds2(X,A), subset_bounds2(Y,B).
234
235		% --------
236		% SETS
237		% --------
238
239		:- use_module(library(avl),[avl_min/2, avl_max/2, avl_member/2]).
240
241		infer_set_bounds(b(E,Type,_Infos),Env,Bounds) :- !,
242		(finite_type(Type) -> Bounds = Type % we could try and infer bounds for fd(_,_) global set values
243		; infer_set_bounds(E,Type,Env,Bounds)).
244		infer_set_bounds(empty_set,set(integer),_,Bounds) :- !, Bounds = binterval(1,0,0).
245		infer_set_bounds(integer_set('NATURAL'),set(integer),_,Bounds) :- !, init_binterval(0,_,Bounds,1).
246		infer_set_bounds(integer_set('NATURAL1'),set(integer),_,Bounds) :- !, init_binterval(1,_,Bounds,1).
247		infer_set_bounds(value(AVL),ST,Env,Bounds) :- nonvar(AVL), AVL=avl_set(A),
248		is_set_type(ST,Type),!,
249		infer_avl_set_bounds(Type,A,Env,Bounds).
250		infer_set_bounds(value(CS),set(integer),_Env,Bounds) :- nonvar(CS), is_interval_closure(CS,Low,Up),
251		number(Low), number(Up), !, init_binterval(Low,Up,Bounds,_).
252		% TODO: maybe cartesian product closure ?
253		infer_set_bounds(interval(A,B),_,Env,Bounds) :- !,
254		infer_scalar_bounds(A,Env,bint(BA)),
255		infer_scalar_bounds(B,Env,bint(BB)),
256		init_binterval(BA,BB,Bounds,_).
257		infer_set_bounds(intersection(A,B),_,Env,Bounds) :- !,
258		% Note: we assume that Bounds of result are unconstrained; and will only be constrained later by eq_bounds
259		infer_set_bounds(A,Env,BoundsA),
260		infer_set_bounds(B,Env,BoundsB), % TODO: treat if one of the two calls fails
261		%tools_printing:print_term_summary_user_output(inter1(BoundsA,BoundsB,Bounds)),nl,
262		intersect_bounds(BoundsA,BoundsB,Bounds).
263		infer_set_bounds(union(A,B),_,Env,Bounds) :- !,
264		% Note: we assume that Bounds of result are unconstrained; and will only be constrained later by eq_bounds
265		infer_set_bounds(A,Env,BoundsA),
266		infer_set_bounds(B,Env,BoundsB),
267		%tools_printing:print_term_summary_user_output(union1(BoundsA,BoundsB,Bounds)),nl,
268		union_bounds(BoundsA,BoundsB,Bounds).
269		infer_set_bounds(set_subtraction(A,B),_,Env,Bounds) :- !,
270		% Note: we assume that Bounds of result are unconstrained; and will only be constrained later by eq_bounds
271		infer_set_bounds(A,Env,BoundsA),
272		infer_set_bounds(B,Env,BoundsB), % TODO: treat if one of the two calls fails
273		%tools_printing:print_term_summary_user_output(inter1(BoundsA,BoundsB,Bounds)),nl,
274		set_subtract_bounds(BoundsA,BoundsB,Bounds).
275		infer_set_bounds(set_extension(List),_,Env,Bounds) :- !,
276		(List = [A], infer_scalar_bounds(A,Env,bint(BA))
277		-> Bounds = binterval(BA,BA,1)
278		; maplist(infer_set_ext_el(Env,Bounds),List)
279		% TODO: use union code instead? we loose info that these are all the elements of the set
280		).
281		infer_set_bounds(identifier(A),Type,Env,Bounds) :- !,
282		lookup_id_bounds(A,Env,Type,Bounds).
283		infer_set_bounds(cartesian_product(A,B),_,Env,Bounds) :- !,
284		infer_set_bounds(A,Env,BoundsA),
285		infer_set_bounds(B,Env,BoundsB),
286		construct_bcart(A,B,BoundsA,BoundsB,Bounds).
287		infer_set_bounds(domain(A),_,Env,DomBounds) :- !,
288		infer_set_bounds(A,Env,bcart(DomBounds,_,NE)),
289		imply_non_empty(DomBounds,NE). % if domain is non-empty, then full relation must be non-empty
290		infer_set_bounds(range(A),_,Env,RanBounds) :- !,
291		infer_set_bounds(A,Env,bcart(_,RanBounds,NE)),
292		imply_non_empty(RanBounds,NE). % if range is non-empty, then full relation must be non-empty
293		infer_set_bounds(image(Rel,_Set),Type,Env,ImgBounds) :- !,
294		infer_set_bounds(range(Rel),Type,Env,RanBounds),
295		subset_bounds(ImgBounds,RanBounds).
296		infer_set_bounds(reverse(Rel),_Type,Env,IBounds) :- !, % relational inverse
297		infer_set_bounds(Rel,Env,Bounds),
298		Bounds = bcart(BA,BB,NonEmptyAB),
299		IBounds = bcart(BB,BA,NonEmptyAB).
300		infer_set_bounds(closure(Rel),_Type,Env,Bounds) :- !, % transitive closure1
301		infer_set_bounds(Rel,Env,Bounds),
302		Bounds = bcart(_,_,_). % dom(closure1(r)) = dom(r), ditto for ran
303		infer_set_bounds(iteration(Rel,_),_Type,Env,Bounds) :- !, % iterate operator
304		infer_set_bounds(Rel,Env,RelBounds),
305		RelBounds = bcart(_,_,_), % dom(iterate(r,n)) <: dom(r), for n>0, ditto for ran; subset
306		% for n=0 basp translation deviates from B Book and uses elements in domain/range only; so it also holds for n=0
307		subset_bounds(Bounds,RelBounds).
308		infer_set_bounds(Term,_Type,Env,Bounds) :- relational_operator_domran_subset_of_relation(Term,Rel),!,
309		infer_set_bounds(Rel,Env,RelBounds),
310		RelBounds = bcart(_,_,_),
311		subset_bounds(Bounds,RelBounds).
312		infer_set_bounds(composition(A,B),Type,Env,Bounds) :- !,
313		is_set_type(Type,couple(TA,TB)),
314		infer_set_bounds(domain(A),TA,Env,BoundsA),
315		infer_set_bounds(range(B),TB,Env,BoundsB),
316		construct_bcart(domain(A),range(B),BoundsA,BoundsB,CartBounds), % dom(A;B) <: dom(A) and ran(A;B) <: ran(B)
317		subset_bounds(Bounds,CartBounds).
318		infer_set_bounds(S,_,_,_) :- debug_mode(on),
319		functor(S,F,N), write(user_output,uncovered_set_in_bounds_analysis(F,N,S)), nl(user_output),fail.
320
321		% relational operator term whose domain/range are subsets of the relation argument
322		relational_operator_domran_subset_of_relation(domain_restriction(_,R),R). % dom(S <| R) <: dom(R), ditto for ran
323		relational_operator_domran_subset_of_relation(domain_subtraction(_,R),R). % dom(S <<| R) <: dom(R)
324		relational_operator_domran_subset_of_relation(range_restriction(R,_),R).
325		relational_operator_domran_subset_of_relation(range_subtraction(R,_),R).
326		relational_operator_domran_subset_of_relation(front(R),R). % dom(front(R)) <: dom(R), ran(front(R)) <: ran(R)
327		relational_operator_domran_subset_of_relation(tail(R),R).
328		relational_operator_domran_subset_of_relation(restrict_front(R,_),R).
329		relational_operator_domran_subset_of_relation(restrict_tail(R,_),R).
330
331		:- use_module(probsrc(custom_explicit_sets),[domain_of_explicit_set_wf/3,range_of_explicit_set_wf/3,
332		is_interval_closure/3]).
333		infer_avl_set_bounds(integer,A,_,Bounds) :-
334		avl_min(A,int(Min)), %min_of_explicit_set_wf(Val,int(Min),no_wf_available),
335		avl_max(A,int(Max)), Bounds = binterval(Min,Max,1).
336		infer_avl_set_bounds(string,A,_,Bounds) :-
337		findall(Nr,(avl_member(string(S),A), get_string_nr(S,Nr)),Nrs),
338		min_member(Min,Nrs), max_member(Max,Nrs), Bounds = binterval(Min,Max,1).
339		infer_avl_set_bounds(couple(TA,TB),A,Env,Bounds) :-
340		domain_of_explicit_set_wf(avl_set(A),Domain,no_wf_available), DA=b(value(Domain),set(TA),[]),
341		range_of_explicit_set_wf(avl_set(A),Range,no_wf_available), RA=b(value(Range),set(TB),[]),
342		infer_set_bounds(cartesian_product(DA,RA),set(couple(TA,TB)),Env,Bounds).
343
344
345		infer_set_ext_el(Env,Bounds,A) :-
346		(infer_scalar_bounds(A,Env,BoundsA)
347		-> mem_bounds(BoundsA,Bounds)
348		; format(user_output,'Cannot infer bounds for set-ext element:~w~n',[A])
349		).
350
351		intersect_bounds(binterval(Low1,Up1,NE1),binterval(Low2,Up2,NE2),Bounds) :-
352		init_binterval(Low,Up,Bounds,NE),
353		NE #=< NE1, % if set1 is empty the the intersection is empty
354		NE #=< NE2, % ditto for set 2
355		% Note: binterval(Low,Up) does not mean that all values are present
356		% Hence the resulting interval can be smaller than the naive interval intersection
357		% e.g., {2,4} /\ 1..3 = {2} and not 2..3
358		Low #>= max(Low1,Low2), % Hence: we do not set Low to be exactly max(Low1,Low2)
359		Up #=< min(Up1,Up2). % Ditto for Up and min(Up1,Up2)
360		% TODO: we could have a precision flag, detecting when all values are present
361		union_bounds(binterval(Low1,Up1,NE1),binterval(Low2,Up2,NE2),Bounds) :-
362		init_binterval(Low,Up,Bounds,NE),
363		NE1 #=< NE, % if union empty then set1 empty
364		NE2 #=< NE, % ditto for set 2
365		NE #=< NE1+NE2, % if set1 & set2 empty then union is empty
366		(NE1 #= 0) #=> (Low #= Low2 #/\ Up #= Up2), % if set1 empty we copy set2 to result
367		(NE1 #= 1 #/\ NE2 #= 1) #=> (Low #= min(Low1,Low2) #/\ Up #= max(Up1,Up2)).
368		set_subtract_bounds(binterval(Low1,Up1,NE1),binterval(Low2,Up2,NE2),Bounds) :- % Set1 \ Set2 = Result
369		init_binterval(Low,Up,Bounds,NE),
370		NE #=< NE1, % if set1 is empty the the set difference is empty
371		NE2 #= 0 #=> NE #= NE1, % if set2 is empty then set1 is the result
372		Low #>= Low1, Up #=< Up1, % result is contained in Set1, and we do not really know much more unless Set2 is disjoint to Set1
373		Low1 #>= min(Low,Low2), % if Low2>Low then Low1=Low and if Low2<=Low then smallest possible value in Set1 is Low1
374		Up1 #=< max(Up,Up2). % ditto for upper bound
375		% Low2 #> Low #=> Low #= Low1, % then the lower boundary value Low1 cannot have been removed by set subtraction
376		% Up2 #< Up #=> Up #= Up1. % ditto for upper boundary value
377
378
379		init_binterval(Low,Up,binterval(Low,Up,NonEmpty),NonEmpty) :-
380		NonEmpty #<=> (Low #=< Up).
381
382		% construct a bcart/3 term; setting up non-empty flag
383		construct_bcart(A,B,BA,BB,bcart(BA,BB,NonEmptyAB)) :- NonEmptyAB in 0..1,
384		(get_non_empty_flag(A,BA,NonEmptyA),
385		get_non_empty_flag(B,BB,NonEmptyB)
386		-> NonEmptyAB #= NonEmptyA*NonEmptyB % or minimum of both; if one set empty (0) then cartesian product empty
387		; format(user_output,'Could not get non-empty-flags: ~w * ~w~n',[A,B])
388		).
389
390		get_non_empty_flag(Expr,Bounds,NonEmpty) :-
391		(definitely_not_empty_set(Expr) -> NonEmpty=1
392		, debug_format(4,'Definitely non-empty: ~w~n',[Expr])
393		; get_non_empty_flag(Bounds,NonEmpty)).
394
395		get_non_empty_flag(binterval(_,_,NE),R) :- !, R=NE.
396		get_non_empty_flag(bcart(_,_,NE),R) :- !, R=NE.
397		get_non_empty_flag(_,NE) :-
398		NE in 0..1. % we don't know if set is empty or not; TODO: use definitely_not_empty !?
399
400		% if bounds are non-empty force another non-empty flag to be 1
401		imply_non_empty(Bounds,NonEmptyFlag) :- get_non_empty_flag(Bounds,NE),
402		imply_block(NE,NonEmptyFlag).
403		:- block imply_block(-,?).
404		imply_block(1,1).
405		imply_block(0,_).
406
407		% SCALARS
408		% --------
409
410		:- use_module(probsrc(bsyntaxtree),[is_set_type/2]).
411		:- use_module(probsrc(kernel_objects),[max_cardinality/2]).
412		infer_scalar_bounds(b(E,T,_Infos),Env,Bounds) :- !,
413		(finite_type(T) -> Bounds = T % we could try and infer bounds for fd(_,_) global set values
414		; infer_scalar_bounds2(E,T,Env,Bounds)).
415		infer_scalar_bounds2(integer(A),_,_Env,Bounds) :- !, Bounds = bint(A).
416		infer_scalar_bounds2(string(A),_,_Env,Bounds) :- !, get_string_nr(A,Nr),Bounds = bint(Nr).
417		infer_scalar_bounds2(identifier(A),Type,Env,Bounds) :- !, lookup_id_bounds(A,Env,Type,Bounds).
418		infer_scalar_bounds2(card(A),integer,_Env,bint(Card)) :-
419		%infer_set_bounds(A,Env,binterval(Low,Up)),
420		!,
421		% TODO: if Low <= Up -> Card #= 1+Up-Low else = 0
422		(get_texpr_type(A,AType),is_set_type(AType,SType),
423		max_cardinality(SType,MaxCard),number(MaxCard)
424		-> Card in 0..MaxCard ; Card #>= 0).
425		infer_scalar_bounds2(couple(A,B),couple(_TA,_TB),Env,bcouple(BA,BB)) :- !,
426		infer_scalar_bounds(A,Env,BA), % TODO: treat if one of them fails / is finite
427		infer_scalar_bounds(B,Env,BB).
428		infer_scalar_bounds2(function(Rel,_Arg),Type,Env,Bounds) :- !,
429		infer_set_bounds(range(Rel),set(Type),Env,RanBounds), % we ignore Arg
430		%convert_set_bounds_to_scalar(RanBounds,Bounds). % we could use this if TRY_FIND_ABORT is TRUE
431		if(mem_bounds(Bounds,RanBounds),
432		true,
433		create_dummy_value(RanBounds,Bounds)). % empty range probably meaning WD error; just return a concrete dummy value
434		infer_scalar_bounds2(div(A,B),integer,Env,Bounds) :-
435		infer_scalar_bounds(B,Env,BoundsB), BoundsB=bint(BB), integer(BB), BB \= 0, !,
436		infer_scalar_bounds(A,Env,BoundsA),
437		apply_binary_op('/',Bounds,BoundsA,BoundsB).
438		infer_scalar_bounds2(BOP,_,Env,Bounds) :-
439		scalar_binary_op(BOP,A,B,ClpfdOp), !,
440		infer_scalar_bounds(A,Env,BoundsA),
441		infer_scalar_bounds(B,Env,BoundsB),
442		apply_binary_op(ClpfdOp,Bounds,BoundsA,BoundsB).
443		infer_scalar_bounds2(BOP,_,_,_) :- debug_mode(on),
444		functor(BOP,F,N),write(user_output,uncovered_scalar_in_bounds_analysis(F/N)),nl(user_output),fail.
445
446		%convert_set_bounds_to_scalar(binterval(A,B,NonEmpty),bint(X)) :-
447		% (NonEmpty#=1) #=> (X #>= A #/\ X #=< B).
448
449		% create a dummy element for given bounds
450		create_dummy_value(binterval(A,_,_),bint(DA)) :- !, (var(A),fd_min(A,Min),number(Min) -> DA=Min ; DA=0).
451		create_dummy_value(bcart(A,B,_),bcouple(DA,DB)) :- !, create_dummy_value(A,DA), create_dummy_value(B,DB).
452		create_dummy_value(T,T) :- finite_type(T).
453
454		scalar_binary_op(add(A,B),A,B,'+').
455		scalar_binary_op(multiplication(A,B),A,B,'*').
456		scalar_binary_op(minus(A,B),A,B,'-').
457		apply_binary_op(Op,bint(Res),bint(A),bint(B)) :- !, RHS =.. [Op,A,B],
458		if(call('#=',Res,RHS),true, % TODO: catch overflows
459		(format(user_output,'Inconsistent ~w #= (~w ~w ~w) constraint!',[Res, A,Op,B]),fail)).
460		apply_binary_op(ClpfdOp,Bounds,BoundsA,BoundsB) :-
461		add_internal_error('Illegal call: ',apply_binary_op(ClpfdOp,Bounds,BoundsA,BoundsB)), fail.
462
463		:- use_module(probsrc(bsyntaxtree), [def_get_texpr_id/2, get_texpr_id/2, get_texpr_type/2]).
464
465		%relevant_identifier(TID,Env,ID,BoundsInfo) :- get_texpr_id(TID,ID),
466		% lookup_id_bounds(ID,Env,_,BoundsInfo).
467
468
469		% environment utilities:
470
471		new_env(env(E,_),Opts) :-
472		(member(outer_bounds(OB),Opts)
473		-> maplist(add_outer_bound_info,OB,E)
474		% outer bounds are already ground and need no labeling; they provide bounds for outer variables
475		; member(open,Opts) -> true ; E=[]).
476
477		:- use_module(probsrc(btypechecker), [unify_types_strict/2]).
478		lookup_id_bounds(ID,env(Env,_),Type,BoundsInfo) :-
479		(member(bound_internal_info(ID,StoredType,StoredBounds),Env)
480		-> (unify_types_strict(Type,StoredType)
481		-> BoundsInfo=StoredBounds
482		; format(user_output,'Stored type for identifier ~w does not match: ~w vs ~w!!~n',[ID,Type,StoredType]),
483		bounds_type(Type,BoundsInfo,_)
484		)
485		; format(user_output,'Could not find identifier ~w !!~n',[ID]),
486		bounds_type(Type,BoundsInfo,_)). % set up unconstrained bounds
487
488		% add typed ids to environment, also returns list of bounds information for added ids
489		add_typed_ids([],[],_) --> [].
490		add_typed_ids([TID|T],[BoundsInfo|TB],BA_Required) -->
491		add_typed_id(TID,BoundsInfo,BA_Required), add_typed_ids(T,TB,BA_Required).
492
493		add_typed_id(TID,bound_id_info(ID,Type,Bounds),BA_Required,env(Env,Flags),env(NewEnv,Flags)) :-
494		def_get_texpr_id(TID,ID),
495		get_texpr_type(TID,Type),
496		NewEnv = [bound_internal_info(ID,Type,Fresh)|Env],
497		(bounds_type(Type,Fresh,_)
498		-> compute_bound_info(ID,Type,Fresh,Bounds,Flags),
499		BA_Required = bounds_analysis_required
500		; debug_format(9,'Ignoring identifier ~w in analysis (type either bounded or too complex)~n',[ID]),
501		Fresh=Type, Bounds=Type
502		),
503		label_id(ID,Type,Fresh,Flags).
504
505		% add information from outer variables (e.g., computed by infer_bounds for outer predicate)
506		add_outer_bound_info(bound_id_info(ID,Type,Bounds),bound_internal_info(ID,Type,InternalType)) :-
507		convert_bounds_to_internal(Bounds,InternalType).
508
509		convert_bounds_to_internal(integer_in_range(From,To,_),bint(X)) :- !, X in From..To.
510		convert_bounds_to_internal(set(integer_in_range(From,To,_)),binterval(From2,To2,_NonEmpty)) :- !,
511		(number(From) -> From2=From ; true), (number(To) -> To2=To ; true).
512		% we do not know if set is empty or not;
513		% see test 2519 :clingo-double-check x<:1..3 & !y.(y:0..3 & x*(1..2)=(1..2)*(1..y) => y=2)
514		convert_bounds_to_internal(string,bint(Nr)) :- !, Nr #>= 0. % strings number start at 0
515		convert_bounds_to_internal(set(string),binterval(From,_To,_NonEmpty)) :- !,
516		From #>= 0.
517		convert_bounds_to_internal(set(couple(A,B)),BCart) :- !,
518		convert_bounds_to_internal(set(A),BA),
519		convert_bounds_to_internal(set(B),BB),
520		Dummy = b(empty_set,any,[]),
521		construct_bcart(Dummy,Dummy,BA,BB,BCart).
522		convert_bounds_to_internal(X,X).
523
524		finite_type(boolean).
525		finite_type(global(_GS)).
526		finite_type(set(X)) :- finite_type(X).
527		finite_type(couple(X,Y)) :- finite_type(X), finite_type(Y).
528
529		% a type for which we can determine bounds:
530		% it also returns a 0..1 CLP(FD) flag for non-emptyness; useful for sets only
531		bounds_type(integer,bint(_),1).
532		bounds_type(string,bint(_),1).
533		bounds_type(seq(X),BoundsInfo,NonEmpty) :- bounds_type(set(couple(integer,X)),BoundsInfo,NonEmpty).
534		bounds_type(set(integer),binterval(_,_,NonEmpty),NonEmpty).
535		bounds_type(set(string),binterval(_,_,NonEmpty),NonEmpty).
536		bounds_type(couple(A,B),bcouple(BA,BB),1) :-
537		bounds_of_pair(A,B,BA,BB,_). % at least one part requires bounds
538		bounds_type(set(couple(A,B)),bcart(BA,BB,NonEmpty),NonEmpty) :-
539		bounds_of_pair(set(A),set(B),BA,BB,NonEmpty).
540
541		% get bounds of two types, ensuring at least one of them requires bounds inference
542		bounds_of_pair(A,B,BA,BB,NonEmpty) :-
543		(bounds_type(A,BA,NEA)
544		-> (bounds_type(B,BB,NEB) -> NonEmpty #= min(1,NEA+NEB)
545		; BB=B, NonEmpty=NEA)
546		; BA=A, bounds_type(B,BB,NonEmpty)).
547
548		:- block compute_bound_info(?,?,?,?,-).
549		compute_bound_info(ID,Type,Fresh,Bounds,_) :-
550		get_bounds(Fresh,Type,Bounds),
551		debug_format(19,'Computed bounds ~w : ~w --> ~w~n',[ID,Type,Bounds]).
552
553		% get bounds of an internal representation into format suitable for b2asp / other tools
554		% it creates a type term, using integer_in_range/2 in place of integer
555		get_bounds(bint(X),Type,integer_in_range(Min,Max,Type)) :- !, fd_min(X,Min), fd_max(X,Max).
556		get_bounds(binterval(X,Y,NonEmpty),set(Type),set(integer_in_range(Min,Max,Type))) :- !,
557		( NonEmpty == 0 -> Min=1, Max=0
558		; NonEmpty == 1 -> fd_min(X,Min), fd_max(Y,Max)
559		; get_non_empty_interval_bounds(X,Y,NonEmpty,Min,Max) % we do not know if set empty or not
560		).
561		get_bounds(bcouple(A,B),couple(TA,TB),couple(BA,BB)) :- !, get_bounds(A,TA,BA), get_bounds(B,TB,BB).
562		get_bounds(bcart(A,B,NonEmpty),set(couple(TA,TB)),set(couple(BA,BB))) :- !,
563		( NonEmpty == 0 -> get_bounds(A,set(TA),set(BA)), get_bounds(B,set(TB),set(BB)) % we could return empty_set for BA/BB
564		; NonEmpty == 1 -> get_bounds(A,set(TA),set(BA)), get_bounds(B,set(TB),set(BB))
565		; get_non_empty_cart_bounds(A,B,TA,TB,NonEmpty,BA,BB) % we do not know if cartesian product empty or not
566		).
567		get_bounds(B,_,R) :- finite_type(B),!, R=B.
568		get_bounds(B,Type,R) :- format(user_output,'Unknown bound: ~w (type ~w)~n',[B,Type]), R=B.
569
570		% try get bounds assuming set is non-empty; these bounds will be used for enumeration in clingo
571		get_non_empty_interval_bounds(X,Y,NonEmpty,_,_) :-
572		bb_put(bounds_analysis_min_max,(1,0)), % if propagation fails the set must be empty
573		(NonEmpty=1 % force non-empty and check to see in which range the values must be
574		-> fd_min(X,Min2), fd_max(Y,Max2),
575		bb_put(bounds_analysis_min_max,(Min2,Max2))
576		; format(user_output,'Bounds interval cannot be non-empty~n',[])
577		),
578		fail.
579		get_non_empty_interval_bounds(_,_,_,Min,Max) :- bb_get(bounds_analysis_min_max,(Min,Max)).
580
581		% try get bounds assuming cartesian product is non-empty; these bounds will be used for enumeration in clingo
582		get_non_empty_cart_bounds(A,B,TA,TB,NonEmpty,_,_) :-
583		bb_put(bounds_analysis_cart,(empty_set,empty_set)), % if propagation fails the set must be empty
584		(NonEmpty=1 % force non-empty and check to see in which range the values must be
585		-> get_bounds(A,set(TA),set(BA)), get_bounds(B,set(TB),set(BB)),
586		bb_put(bounds_analysis_cart,(BA,BB))
587		; format(user_output,'Bounds cartesian product cannot be non-empty~n',[])
588		),
589		fail.
590		get_non_empty_cart_bounds(_,_,_,_,_,BA,BB) :- bb_get(bounds_analysis_cart,(BA,BB)).
591
592
593		:- block label_id(?,?,?,-).
594		label_id(_ID,_Type,Fresh,copy_bounds(Flag)) :- %format(user_output,'Labeling ~w : ~w~n',[ID,Fresh]),
595		label_bounds(Fresh,Flag).
596
597		% TODO: check if finite:
598		:- block label_bounds(?,-).
599		label_bounds(_,no_labeling) :- !.
600		label_bounds(bint(X),_) :- !, label_fd_var(X).
601		label_bounds(binterval(X,Y,Empty),_) :- !, (Empty=0 ; Empty=1), label_fd_var(X), label_fd_var(Y).
602		label_bounds(bcouple(X,Y),F) :- !, label_bounds(X,F), label_bounds(Y,F).
603		label_bounds(bcart(X,Y,Empty),F) :- !, (Empty=0 ; Empty=1), label_bounds(X,F), label_bounds(Y,F).
604		label_bounds(Term,_) :- ground(Term),finite_type(Term),!.
605		label_bounds(Term,_) :- add_internal_error('Unknown bounds info to label:', label_bounds(Term)).
606
607		label_fd_var(X) :- fd_size(X,Sz), (number(Sz) -> indomain(X) ; true).
608
609
610		portray_env(env(NE,_)) :- portray_env2(NE).
611		portray_env2(X) :- var(X),!, write(user_output,' - ... '),nl(user_output).
612		portray_env2([]) :- !.
613		portray_env2([bound_internal_info(ID,Type,BoundsInfo)|TT]) :- !,
614		format(user_output,' - ~w (~w) : ',[ID,Type]), portray_bounds(BoundsInfo), nl(user_output),
615		portray_env2(TT).
616		portray_env2(E) :-
617		format(user_output,' *** ILLEGAL ENV *** ~w~n',[E]).
618
619		portray_bounds(bint(X)) :- !, portray_int(X).
620		portray_bounds(binterval(X,Y,_E)) :- !,
621		write(user_output,'('), portray_int(X), write(user_output,' .. '), portray_int(Y), write(user_output,')').
622		portray_bounds(bcouple(X,Y)) :- !, portray_bounds(X), write(user_output,' , '), portray_bounds(Y).
623		portray_bounds(bcart(X,Y,_E)) :- !, portray_bounds(X), write(user_output,' * '), portray_bounds(Y).
624		portray_bounds(T) :- finite_type(T), !, write(user_output,T).
625		portray_bounds(U) :- write(user_output,'*** UNKNOWN '), write(user_output,U), write(user_output,' ***').
626
627		portray_int(X) :- nonvar(X),!, write(user_output,X).
628		portray_int(X) :- fd_dom(X,Dom), write(user_output,Dom).
629
630		label_env(env(_,Flags),Options) :- !,Flags=copy_bounds(F2),
631		(member(label,Options) -> F2=label_now ; F2=no_labeling).
632		label_env(E,_) :- add_internal_error('Illegal env: ', label_env(E)).
633
634
635
636		/*
637
638		Encode set union constraints using single fd variable:
639
640		| ?- X in 1..3, Y in 2..5, element([X,Y],Z).
641		X in 1 .. 3,
642		Y in 2 .. 5,
643		Z in 1 .. 5 ?
644
645		Intersection:
646		| ?- X in 1..3, Y in 2..5, element([X],Z), element([Y],Z).
647		X in 2 .. 3,
648		Y in 2 .. 3,
649		Z in 2 .. 3 ?
650		yes
651
652		But how do we encode empty set?
653		| ?- X in 1..3, Y in 4..5, element([X],Z), element([Y],Z).
654		no
655
656		*/