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