| 1 | | % (c) 2009-2019 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(b_global_sets, |
| 6 | | [b_get_global_constants/1, b_get_global_enumerated_sets/1, b_get_global_sets/1, |
| 7 | | lookup_global_constant/2, |
| 8 | | is_b_global_constant/3, |
| 9 | | is_used_b_global_constant/3, is_unused_b_global_constant/3, |
| 10 | | |
| 11 | | b_global_set/1, b_non_empty_global_set/1, b_empty_global_set/1, |
| 12 | | b_global_deferred_set/1, |
| 13 | | b_global_set_with_potential_symmetry/1, b_global_deferred_set_with_card_gt1/1, |
| 14 | | b_partially_deferred_set/1, |
| 15 | | |
| 16 | | unfixed_deferred_set/1, |
| 17 | | contains_unfixed_deferred_set/1, |
| 18 | | b_supplementary_global_set/1, % introduced when untyped ids are allowed |
| 19 | | |
| 20 | | inferred_minimum_global_set_cardinality/2, |
| 21 | | inferred_maximum_global_set_cardinality/2, |
| 22 | | b_exists_global_set_with_potential_symmetry/0, |
| 23 | | b_global_set_cardinality/2, |
| 24 | | |
| 25 | | b_clear_global_set_type_definitions/0, |
| 26 | | b_check_and_precompile_global_set_type_definitions/0, |
| 27 | | %b_precompile_used_global_set_information/0, |
| 28 | | |
| 29 | | b_get_prob_deferred_set_elements/2,add_prob_deferred_set_elements_to_store/3, |
| 30 | | prob_deferred_set_element/4, |
| 31 | | |
| 32 | | find_inequal_global_set_identifiers/4, |
| 33 | | static_symmetry_reduction_for_global_sets/1, |
| 34 | | |
| 35 | | b_integer_set/1, b_integer_or_string_set/1, |
| 36 | | b_type2_set/2, try_b_type2global_set/2, |
| 37 | | |
| 38 | | %b_fd_type/3, |
| 39 | | b_get_fd_type_bounds/3, |
| 40 | | b_fd_card/2, |
| 41 | | is_global_set_of_cardinality_one/2, %is_global_set_of_cardinality_two/3, |
| 42 | | global_type/2, global_type_wf/3, |
| 43 | | get_global_type_value/3, |
| 44 | | enum_global_type/2, enumerate_global_type_with_enum_warning/3, |
| 45 | | |
| 46 | | all_elements_of_type/2, all_elements_of_type_rand/2, |
| 47 | | |
| 48 | | set_user_defined_scope/2, |
| 49 | | |
| 50 | | fixed_deferred_set_size/2, |
| 51 | | |
| 52 | | add_new_global_set/1, |
| 53 | | generate_fresh_supplementary_global_set/1 |
| 54 | | %,add_global_set_with_named_constants/2 /* for use by Z,... */ |
| 55 | | ]). |
| 56 | | |
| 57 | | :- use_module(debug). |
| 58 | | :- use_module(tools). |
| 59 | | :- use_module(library(lists)). |
| 60 | | :- use_module(library(ordsets)). |
| 61 | | :- use_module(self_check). |
| 62 | | :- use_module(preferences). |
| 63 | | :- use_module(error_manager). |
| 64 | | :- use_module(bsyntaxtree). |
| 65 | | :- use_module(library(between),[between/3]). |
| 66 | | :- use_module(gensym,[gensym/2]). |
| 67 | | |
| 68 | | :- use_module(module_information,[module_info/2]). |
| 69 | | :- module_info(group,kernel). |
| 70 | | :- module_info(description,'This module provides support for deferred/enumerated set elements in B.'). |
| 71 | | |
| 72 | | :- use_module(bmachine). |
| 73 | | |
| 74 | | /* what we call global sets here usually called "given sets", which can be |
| 75 | | either enumerated or deferred */ |
| 76 | | |
| 77 | | |
| 78 | | :- dynamic b_global_constant/3. % named element of a deferred or enumerated set |
| 79 | | % for enumerated sets S = {a,b,c} we would have entries a,b,c as b_global_constant |
| 80 | | % for deferred set S, we may add CONSTANTS which are element of S as b_global_constant |
| 81 | | :- dynamic unused_b_global_constant/3. % TO DO: compute properly again !! |
| 82 | | |
| 83 | | :- dynamic inferred_minimum_global_set_cardinality/2. |
| 84 | | :- dynamic inferred_maximum_global_set_cardinality/2. |
| 85 | | |
| 86 | | b_get_global_enumerated_sets(GSets) :- |
| 87 | | findall(GS, (b_global_set(GS), is_b_global_constant(GS,_Nr,_Cst)), GSets). |
| 88 | | b_get_global_sets(GSets) :- |
| 89 | | findall(GS, b_global_set(GS), GSets). |
| 90 | | |
| 91 | | b_get_global_constants(Csts) :- findall(Cst,is_b_global_constant(_,_,Cst),Csts). |
| 92 | | |
| 93 | ? | is_b_global_constant(Set,Nr,Cst) :- b_global_constant(Set,Nr,Cst). |
| 94 | | is_unused_b_global_constant(Set,Nr,Cst) :- unused_b_global_constant(Set,Nr,Cst). |
| 95 | | is_used_b_global_constant(Set,Nr,Cst) :- |
| 96 | | b_global_constant(Set,Nr,Cst), \+ unused_b_global_constant(Set,Nr,_). |
| 97 | | |
| 98 | | :- dynamic lookup_global_constant/2. |
| 99 | | %lookup_global_constant(Id,Val) :- |
| 100 | | % b_global_constant(Set,Nr,Id), % not an indexed lookup ; now we assert lookup_global_constant below |
| 101 | | % Val = fd(Nr,Set). |
| 102 | | |
| 103 | | |
| 104 | | :- dynamic b_precompiled_global_set/1. |
| 105 | | b_precompiled_global_set(_) :- print_error('*** b_global_set not precompiled'),fail. |
| 106 | | |
| 107 | ? | b_global_set(GS) :- b_precompiled_global_set(GS) ; b_supplementary_global_set(GS). |
| 108 | | |
| 109 | | % a version of b_global_set which does not leave a trailing choice point for b_supplementary_global_set around |
| 110 | | % has to be called with GS ground |
| 111 | | %b_global_set_ground(GS) :- if(b_precompiled_global_set(GS),true,b_supplementary_global_set(GS)). |
| 112 | | |
| 113 | | |
| 114 | | b_global_deferred_set(GS) :- |
| 115 | ? | b_global_set(GS), |
| 116 | ? | \+ is_b_global_constant(GS,_Nr,_Cst). % note : some deferred sets are translated into partially_deferred_set |
| 117 | | |
| 118 | | % either an enumerated set with unused constants or a deferred sets where some constants were lifted into the deferred set |
| 119 | | b_partially_deferred_set(GS) :- |
| 120 | | b_global_set(GS), |
| 121 | | (is_b_global_constant(GS,_Nr,_Cst) -> true), % GS is in principle enumerated |
| 122 | | (unused_b_global_constant(GS,_X,_) -> true). |
| 123 | | |
| 124 | | |
| 125 | | b_global_set_with_potential_symmetry(GS) :- |
| 126 | ? | b_global_set(GS), |
| 127 | ? | (b_global_deferred_set_with_card_gt1(GS) -> true |
| 128 | ? | ; ((unused_b_global_constant(GS,X,_), |
| 129 | ? | unused_b_global_constant(GS,Y,_), X\=Y) -> true % At least two unused constants exist |
| 130 | | ; fail)). |
| 131 | | |
| 132 | | b_global_deferred_set_with_card_gt1(GS) :- |
| 133 | ? | b_global_deferred_set(GS), |
| 134 | | extract_setsize_from_machine_cache(GS,Low,Up), |
| 135 | | Up>Low. |
| 136 | | |
| 137 | | :- volatile b_exists_global_set_with_potential_symmetry/0. |
| 138 | | :- dynamic b_exists_global_set_with_potential_symmetry/0. |
| 139 | | |
| 140 | | b_check_and_precompile_global_set_type_definitions :- |
| 141 | | /* must be called before the animator can run !! */ |
| 142 | | b_reset_global_set_type_definitions, |
| 143 | | retractall(b_exists_global_set_with_potential_symmetry), |
| 144 | | debug_println(9,'Checking existence of global type definitions: '), |
| 145 | | debug_print(9,'% '), |
| 146 | ? | (b_get_named_machine_set(Set,_) % treat enumerated sets first; their cardinality is obvious |
| 147 | ? | ; b_get_machine_set(Set), \+ b_get_named_machine_set(Set,_) |
| 148 | | ), |
| 149 | | add_new_global_set(Set), |
| 150 | ? | (b_extract_fd_type(Set,LowBnd,UpBnd) /* also computes & caches the size of the SET */ |
| 151 | | -> debug_print(9,' '),debug_print(9,Set), |
| 152 | | debug_print(9,'=='),debug_print(9,LowBnd),debug_print(9,'..'),debug_print(9,UpBnd) |
| 153 | | ; add_internal_error('No b_extract_fd_type/3 solution for global set: ',b_extract_fd_type(Set,_,_)) |
| 154 | | ),debug_print(9,' '), |
| 155 | | fail. |
| 156 | | b_check_and_precompile_global_set_type_definitions :- |
| 157 | | find_all_used_enumerated_elements(UsedEnumeratedElements), |
| 158 | ? | b_extract_fd_type(GS,Low,Up), |
| 159 | ? | (is_b_global_constant(GS,_Nr,_Cst) -> true), % GS is in principle enumerated |
| 160 | | (user_forced_symmetry(GS) |
| 161 | | -> ForceSymm=true, print('FORCING SYMMETRY: '), print(GS), print(' ') |
| 162 | | ; ForceSymm=false |
| 163 | | ), |
| 164 | ? | enum_fd(X,Low,Up), /* enumerate all elements of GS */ |
| 165 | | can_symmetry_reduction_be_applied_to_constant(ForceSymm,GS,X,UsedEnumeratedElements,Display), |
| 166 | | assert(unused_b_global_constant(GS,X,deferred)), % by storing that it is not used, we enable symmetry reduction |
| 167 | | debug_println(9,unused_b_global_constant(Display)), |
| 168 | | fail. |
| 169 | | b_check_and_precompile_global_set_type_definitions :- |
| 170 | ? | (b_global_set_with_potential_symmetry(_) |
| 171 | | -> assert(b_exists_global_set_with_potential_symmetry), |
| 172 | | debug_println(9,'% Symmetry is potentially useful for this machine') |
| 173 | | ; true), |
| 174 | | debug_nl(9), |
| 175 | | /* clean up: */ |
| 176 | | reset_global_set_user_defined_scope. |
| 177 | | |
| 178 | | % -------------------- |
| 179 | | |
| 180 | | % peform MACE style static symmetry reduction for those global constants |
| 181 | | % that have not already been fixed |
| 182 | | % e.g., for constants aa,bb,cc,dd of type ID and bb/=cc --> nrs of bb,cc will be fixed as 1 and 2; we will ensure that numbers of aa:1..3 and dd:1..4 and that dd=4 only if aa=3 |
| 183 | | |
| 184 | | static_symmetry_reduction_for_global_sets(_ConstantsState) :- |
| 185 | | get_preference(try_kodkod_on_load,true),!. % no idea which numbering Kodkod might return/expect ?! |
| 186 | | static_symmetry_reduction_for_global_sets(_ConstantsState) :- |
| 187 | | get_preference(use_static_symmetry_detection,false),!. |
| 188 | | static_symmetry_reduction_for_global_sets(ConstantsState) :- |
| 189 | | findall(gs_info(GS,FirstAvailableNewIdx,Low,Up,Other), |
| 190 | | static_symmetry_reduction_possible(GS,FirstAvailableNewIdx,Low,Up,Other),L), |
| 191 | | maplist(perform_static_symmetry_reduction(ConstantsState),L). |
| 192 | | |
| 193 | | :- use_module(static_symmetry_reduction,[static_symmetry_reduction_possible/5, perform_ssr/8]). |
| 194 | | perform_static_symmetry_reduction(ConstantsState,gs_info(GS,First,Low,Up,Other)) :- |
| 195 | | if(perform_ssr(Other,[],First,First,GS,Low,Up,ConstantsState),true, |
| 196 | | add_internal_error('Call failed: ',perform_ssr(Other,[],First,First,GS,Low,Up,ConstantsState))). |
| 197 | | |
| 198 | | |
| 199 | | |
| 200 | | % -------------------- |
| 201 | | |
| 202 | | can_symmetry_reduction_be_applied_to_constant(true,GS,X,_Enums,GS/X). % true means symmetry forced |
| 203 | | % if symmetry enforced, all elements are subject to symmetry reduction |
| 204 | | can_symmetry_reduction_be_applied_to_constant(false,GS,X,UsedEnums,Display) :- |
| 205 | | ( is_b_global_constant(GS,X,Name) -> % sym-reduction can be applied to an enumerated set member |
| 206 | | nonmember(Name,UsedEnums), % if it's not used anywhere |
| 207 | | Display=Name |
| 208 | | ; otherwise -> Display=GS/X). % sym-reduction can be applied to deferred set elements |
| 209 | | |
| 210 | | |
| 211 | | find_all_used_enumerated_elements(Elements) :- |
| 212 | | b_get_all_used_identifiers(Identifiers), |
| 213 | | b_get_machine_variables(TVariables),get_texpr_ids(TVariables,Variables), |
| 214 | | % We assume that b_get_all_used_identifiers/1 is a proper ordset. (sorted with sort/2) |
| 215 | | % As an optimisation, we remove the variables, they cannot be enumerated elements. |
| 216 | | list_to_ord_set(Variables,OVariables), |
| 217 | | ord_subtract(Identifiers,OVariables,Elements),!. |
| 218 | | find_all_used_enumerated_elements(_Elements) :- |
| 219 | | add_error_and_fail(b_global_sets, 'find_all_used_enumerated_elements failed'). |
| 220 | | |
| 221 | | |
| 222 | | reset_global_set_user_defined_scope :- |
| 223 | | retract(global_set_user_defined_scope(GS,_Scope)), |
| 224 | | (is_b_precompiled_globalset(GS) |
| 225 | | -> true |
| 226 | | ; add_error(b_global_sets,'Trying to set scope of unknown SET: ',GS) |
| 227 | | ),fail. |
| 228 | | reset_global_set_user_defined_scope. |
| 229 | | |
| 230 | | % Return those constants which are implicitly introduced by ProB, but not really |
| 231 | | % part of the model. These are the elements of a deferred set. |
| 232 | | b_get_prob_deferred_set_elements(TIds,AllOrVisible) :- |
| 233 | | findall( TId, |
| 234 | | ( prob_deferred_set_element(GS,_Nr,Id,AllOrVisible), |
| 235 | | create_texpr(identifier(Id),global(GS),[],TId)), |
| 236 | | TIds). |
| 237 | | |
| 238 | | add_prob_deferred_set_elements_to_store(OldStore,NewStore,AllOrVisible) :- % add prob_ids |
| 239 | | %print(add_prob_deferred_set_elements_to_store(OldStore)),nl, |
| 240 | | findall(bind(Id,fd(Nr,GS)),(prob_deferred_set_element(GS,Nr,Id,AllOrVisible), |
| 241 | | \+ member(bind(Id,_),OldStore)), |
| 242 | | NewStore, OldStore). |
| 243 | | |
| 244 | | prob_deferred_set_element(GlobalSet,Elem,Id,AllOrVisible) :- |
| 245 | | b_global_set(GlobalSet), |
| 246 | | atom_codes(GlobalSet,GlobalSetCodes),append(GlobalSetCodes,ECodes,NameCodes), |
| 247 | | b_get_fd_type_bounds(GlobalSet,Low,Up), |
| 248 | | between(Low,Up,Elem), |
| 249 | | (AllOrVisible = all -> true |
| 250 | | ; % only visible ones |
| 251 | | \+ is_b_global_constant(GlobalSet,Elem,_) % the identifier is not used somewhere else |
| 252 | | ), |
| 253 | | number_codes(Elem,ECodes), |
| 254 | | atom_codes(Id,NameCodes), |
| 255 | | \+ b_global_set(Id), % not used as another SET name |
| 256 | | \+ lookup_global_constant(Id,_). % not used as another SET element |
| 257 | | |
| 258 | | |
| 259 | | user_forced_symmetry(GS) :- % check if the user defined FORCE_SYMMETRY_GS == TRUE |
| 260 | | string_concatenate('FORCE_SYMMETRY_',GS,DefName), |
| 261 | | b_get_typed_definition(DefName,[],F), get_texpr_expr(F,boolean_true). |
| 262 | | |
| 263 | | % TO DO: re-add this feature, so that unused enumerated set elements can be detected |
| 264 | | % :- use_module(bmachine,[used_identifier/1]). |
| 265 | | %b_precompile_used_global_set_information :- |
| 266 | | % b_precompute_used_identifiers, |
| 267 | | % b_global_constant(GlobalSetName,Nr,CstName), |
| 268 | | % (used_identifier(CstName) -> true |
| 269 | | % ; (assert(unused_b_global_constant(GlobalSetName,Nr,CstName)), |
| 270 | | % debug_print(9,unused_b_global_constant(GlobalSetName,Nr,CstName)), debug_nl(9)) |
| 271 | | % ), |
| 272 | | % fail. |
| 273 | | %b_precompile_used_global_set_information :- |
| 274 | | % retractall(b_exists_deferred_set_or_unused_csts_with_card_gt_1), |
| 275 | | % ((b_global_deferred_set_with_card_gt1(_GS) ; |
| 276 | | % (is_unused_b_global_constant(GS,Nr,_), |
| 277 | | % is_unused_b_global_constant(GS,Nr2,_), Nr2 \= Nr)) |
| 278 | | % -> (assert(b_exists_deferred_set_or_unused_csts_with_card_gt_1), |
| 279 | | % print_message('symmetry can be used for this machine')) |
| 280 | | % ; true |
| 281 | | % ). |
| 282 | | |
| 283 | | %is_global_set_of_cardinality_two(Type,LowBnd,UpBnd) :- |
| 284 | | % b_get_fd_type_bounds(Type,LowBnd,UpBnd), |
| 285 | | % LowBnd+1 =:= UpBnd. |
| 286 | | |
| 287 | | :- volatile is_global_set_of_cardinality_one/2. |
| 288 | | :- dynamic is_global_set_of_cardinality_one/2. |
| 289 | | % should be called when unloading a machine, before type-checking etc... |
| 290 | | % TO DO: use :- use_module(eventhandling,[register_event_listener/3]). |
| 291 | | b_clear_global_set_type_definitions :- % nl,print(clearing_gs),nl, |
| 292 | | retractall(b_supplementary_global_set(_)), |
| 293 | | b_reset_global_set_type_definitions. |
| 294 | | |
| 295 | | b_reset_global_set_type_definitions :- %nl,print(reset_gs),nl, |
| 296 | | % print_message('resetting global sets'), |
| 297 | | retractall(b_precompiled_global_set(_)), |
| 298 | | retractall(enumerated_set(_)), |
| 299 | | retractall(fixed_deferred_set_size(_,_)), |
| 300 | | retractall(extract_setsize_from_machine_cache(_,_,_)), |
| 301 | | retractall(find_minimum_cardinality_cache(_,_)), |
| 302 | | retractall(is_global_set_of_cardinality_one(_,_)), |
| 303 | | retractall(b_global_constant(_,_,_)), |
| 304 | | retractall(lookup_global_constant(_,_)), |
| 305 | | retractall(unused_b_global_constant(_,_,_)), |
| 306 | | retractall(inferred_minimum_global_set_cardinality(_,_)), |
| 307 | | retractall(inferred_maximum_global_set_cardinality(_,_)). |
| 308 | | |
| 309 | | add_new_global_set(Set) :- |
| 310 | | (b_precompiled_global_set(Set) |
| 311 | | -> add_internal_error('Global set already exists: ',add_new_global_set(Set)) |
| 312 | | ; assert(b_precompiled_global_set(Set))). |
| 313 | | |
| 314 | | :- dynamic b_supplementary_global_set/1. |
| 315 | | |
| 316 | | % these should be called before we precompile the global set definitions |
| 317 | | generate_fresh_supplementary_global_set(FRESHID) :- |
| 318 | | gensym('__DEFERREDSET__',FRESHID), |
| 319 | | debug_println(10,generate_fresh_supplementary_global_set(FRESHID)), |
| 320 | | assert(b_supplementary_global_set(FRESHID)). |
| 321 | | |
| 322 | | /* --------------------------------------------------------- */ |
| 323 | | /* Extracting Finite Domain type information from the B machine */ |
| 324 | | /* --------------------------------------------------------- */ |
| 325 | | |
| 326 | | |
| 327 | | |
| 328 | | /* below treats annotations in the form: |
| 329 | | DEFINITIONS |
| 330 | | scope_Name == 1..3; |
| 331 | | scope_Code == 4..8 |
| 332 | | which inform us about which finidte domain ranges we should |
| 333 | | give to global sets defined in SETS |
| 334 | | */ |
| 335 | | |
| 336 | | :- use_module(tools_printing,[print_error/1, format_error/2]). |
| 337 | | :- dynamic extract_setsize_from_machine_cache/3. |
| 338 | | extract_setsize_from_machine_cache(_,_,_) :- |
| 339 | | print_error('*** extract_setsize_from_machine not precompiled'),fail. |
| 340 | | |
| 341 | | try_extract_setsize_from_machine(GlobalSetName,_LowBound,_UpBound) :- |
| 342 | | start_extracting_setsize(GlobalSetName),!,fail. % cyclic dependency; abort computation |
| 343 | | try_extract_setsize_from_machine(GlobalSetName,LowBound,UpBound) :- |
| 344 | | extract_setsize_from_machine(GlobalSetName,LowBound,UpBound). |
| 345 | | |
| 346 | | extract_setsize_from_machine(GlobalSetName,LowBound,UpBound) :- |
| 347 | | extract_setsize_from_machine_cache(GlobalSetName,L,U),!, |
| 348 | | LowBound=L,UpBound=U. |
| 349 | | extract_setsize_from_machine(GlobalSetName,LowBound,UpBound) :- |
| 350 | | start_extracting_setsize_from_machine(GlobalSetName), |
| 351 | | b_get_named_machine_set(GlobalSetName,ListOfConstants), |
| 352 | | !, |
| 353 | | assert_enumerated_set(GlobalSetName,ListOfConstants,LowBound,UpBound), % will also assert_extract_setsize_from_machine_cache |
| 354 | | (get_user_defined_scope(GlobalSetName,DL,DU), |
| 355 | | DU-DL =\= UpBound-LowBound |
| 356 | | -> add_error(extract_setsize_from_machine,'Conflict between scope_ Definition and explicit enumeration of SET:',GlobalSetName) |
| 357 | | ; true |
| 358 | | ). |
| 359 | | extract_setsize_from_machine(GlobalSetName,L,U) :- |
| 360 | | b_supplementary_global_set(GlobalSetName),!, % deferred set that was added for untyped ID,... |
| 361 | | default_deferred_set_bounds(LowBound,UpBound), |
| 362 | | assert_extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound), |
| 363 | | (LowBound,UpBound)=(L,U). |
| 364 | | extract_setsize_from_machine(GlobalSetName,L,U) :- |
| 365 | | /* we have a DEFERRED SET */ |
| 366 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,LowBound,UpBound), |
| 367 | | (LowBound=UpBound -> assert(is_global_set_of_cardinality_one(GlobalSetName,LowBound)) ; true), |
| 368 | | assert_extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound), |
| 369 | | (b_get_disjoint_constants_of_type(GlobalSetName, DisjointConstants,_) |
| 370 | | -> /* add those constants to the deferred set as though they were enumerated set elements: improves performance by avoiding redundant permutations; is a kind of symmetry breaking */ |
| 371 | | debug_println(9,adding_disjoint_constants(GlobalSetName,DisjointConstants)), |
| 372 | | ~~mnf(add_named_constants_to_global_set(GlobalSetName,DisjointConstants)) |
| 373 | | ; true |
| 374 | | ), |
| 375 | | debug_println(9,setsize(GlobalSetName,LowBound,UpBound)), |
| 376 | | (LowBound,UpBound)=(L,U). |
| 377 | | |
| 378 | | /* for Deferred SETS : */ |
| 379 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,L,U) :- |
| 380 | | b_extract_values_clause_assignment(GlobalSetName,_Type,TVal), |
| 381 | | (TVal = b(interval(Low,Up),_,_) -> true |
| 382 | | ; add_error(b_global_sets,'VALUES clause must set deferred set to an interval: ',GlobalSetName,TVal),fail), |
| 383 | | (evaluable_integer_expression(Low,[],LowBound) -> true |
| 384 | | ; add_error(b_global_sets,'Cannot extract lower bound from VALUES interval for: ',GlobalSetName,Low),fail), |
| 385 | | (evaluable_integer_expression(Up,[],UpBound) -> true |
| 386 | | ; add_error(b_global_sets,'Cannot extract upper bound from VALUES interval for: ',GlobalSetName,Up),fail), |
| 387 | | !, |
| 388 | | check_compatible_with_user_scope(GlobalSetName,UpBound,LowBound), |
| 389 | | LowBound=L,UpBound=U. |
| 390 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,L,U) :- |
| 391 | ? | b_get_properties_from_machine(Properties), member_in_conjunction(C,Properties), |
| 392 | | % check if the PROPERTIES contain an expression of the form card(GS) = Nr |
| 393 | | is_equality_card_global_set(C,GlobalSetName,Properties,Card),!, |
| 394 | | assert(fixed_deferred_set_size(GlobalSetName,Card)), |
| 395 | | LowBound=1, UpBound = Card, |
| 396 | | check_compatible_with_user_scope(GlobalSetName,UpBound,LowBound), |
| 397 | | LowBound=L,UpBound=U. |
| 398 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,L,U) :- /* check if there is a scope_ DEFINITION */ |
| 399 | | get_user_defined_scope(GlobalSetName,LowBound,UpBound),!, |
| 400 | | LowBound=L,UpBound=U. |
| 401 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,LowBound,UpBound) :- |
| 402 | | get_preference(globalsets_fdrange,DefaultUpperBound), |
| 403 | | find_minimum_cardinality(GlobalSetName,MinCard), |
| 404 | | assert(inferred_minimum_global_set_cardinality(GlobalSetName,MinCard)), |
| 405 | | !, |
| 406 | | LowBound = 1, |
| 407 | | (find_maximum_cardinality(GlobalSetName,MaxCard) |
| 408 | | -> (MaxCard=MinCard -> assert(fixed_deferred_set_size(GlobalSetName,MinCard)), |
| 409 | | debug_println(9,fixed_deferred_set_size(GlobalSetName,MinCard)), |
| 410 | | UpBound = MinCard |
| 411 | | ; DefaultUpperBound>MaxCard -> |
| 412 | | debug_println(9,reducing_deferred_set_size(GlobalSetName,MaxCard)), |
| 413 | | UpBound=MaxCard |
| 414 | | ; DefaultUpperBound<MinCard -> |
| 415 | | debug_println(9,inferred_minimum_global_set_cardinality(GlobalSetName,MinCard)), |
| 416 | | UpBound=MinCard |
| 417 | | ; otherwise -> UpBound is MinCard |
| 418 | | ) |
| 419 | | ; MinCard>DefaultUpperBound -> UpBound=MinCard |
| 420 | | ; UpBound=DefaultUpperBound), |
| 421 | | debug_println(4,inferred(GlobalSetName,UpBound)). |
| 422 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,LowBound,UpBound) :- |
| 423 | | % No Minimum cardinality was inferred |
| 424 | | LowBound=1, get_preference(globalsets_fdrange,DefaultUpperBound), |
| 425 | | find_maximum_cardinality(GlobalSetName,MaxCard), |
| 426 | | !, |
| 427 | | (MaxCard=1 -> UpBound=1, assert(fixed_deferred_set_size(GlobalSetName,1)) |
| 428 | | ; DefaultUpperBound>MaxCard -> |
| 429 | | debug_println(9,reducing_deferred_set_size(GlobalSetName,MaxCard)), |
| 430 | | UpBound=MaxCard |
| 431 | | % does not have the case: DefaultUpperBound<MinCard -> UpBound=MinCard |
| 432 | | ; UpBound=DefaultUpperBound). |
| 433 | | extract_DEFERRED_setsize_from_machine(_GlobalSetName,LowBound,UpBound) :- |
| 434 | | % No Minimum cardinality was inferred |
| 435 | | default_deferred_set_bounds(LowBound,UpBound). |
| 436 | | |
| 437 | | default_deferred_set_bounds(1,UpBound) :- get_preference(globalsets_fdrange,UpBound). |
| 438 | | |
| 439 | | check_compatible_with_user_scope(GlobalSetName,UpBound,LowBound) :- |
| 440 | | (get_user_defined_scope(GlobalSetName,DL,DU), |
| 441 | | DU-DL =\= UpBound-LowBound |
| 442 | | -> add_error(extract_DEFERRED_setsize_from_machine,'Conflict between scope_ Definition and PROPERTIES:',GlobalSetName) |
| 443 | | ; true |
| 444 | | ). |
| 445 | | |
| 446 | | |
| 447 | | find_maximum_cardinality(GlobalSetName,MaxCard) :- |
| 448 | | find_maximum_cardinality1(GlobalSetName,MaxCard), |
| 449 | | assert(inferred_maximum_global_set_cardinality(GlobalSetName,MaxCard)). |
| 450 | | |
| 451 | | find_maximum_cardinality1(GlobalSetName,MaxCard) :- |
| 452 | | b_get_machine_constants(Csts), |
| 453 | | b_get_properties_from_machine(Properties), |
| 454 | | findall(MC2,find_maximum_cardinality2(Csts,Properties,GlobalSetName,MC2),List), |
| 455 | | debug_println(9,maxcard_list(GlobalSetName,List)), |
| 456 | | min_member(MaxCard,List). |
| 457 | | find_maximum_cardinality2(_Csts,Properties,GlobalSetName,MaxCard) :- |
| 458 | | get_card_upper_bound(Properties,GlobalSetName,MaxCard). |
| 459 | | find_maximum_cardinality2(_Csts,Properties,GlobalSetName,MaxCard) :- |
| 460 | | get_equality(Properties,GlobalSetName,R,RestProp), |
| 461 | | maximum_cardinality_of_expression(R,RestProp,MaxCard). |
| 462 | | find_maximum_cardinality2(_Csts,Properties,GlobalSetName,MaxCard) :- |
| 463 | ? | member_in_conjunction(C,Properties), |
| 464 | | get_texpr_expr(C,partition(Set,DisjSets)), |
| 465 | | global_set_identifier(Set,GlobalSetName), |
| 466 | | max_partition_card(DisjSets,Properties,0,MaxCard). |
| 467 | | |
| 468 | | get_equality(Properties,ID,R,RestProp) :- |
| 469 | ? | select_member_in_conjunction(C,Properties,RestProp), |
| 470 | | get_texpr_expr(C,equal(LHS,RHS)), |
| 471 | | ( get_texpr_expr(LHS,identifier(ID)), R=RHS |
| 472 | | ; get_texpr_expr(RHS,identifier(ID)), R=LHS ). |
| 473 | | |
| 474 | | % find card(ID) <= MaxCard |
| 475 | | get_card_upper_bound(Properties,ID,MaxCard) :- |
| 476 | | LHS = b(card(TID),_,_), |
| 477 | | get_texpr_expr(TID,identifier(ID)), |
| 478 | ? | select_member_in_conjunction(C,Properties,RestProp), |
| 479 | | ( get_texpr_expr(C,less_equal(LHS,RHS)), Strict=false ; |
| 480 | | get_texpr_expr(C,greater_equal(RHS,LHS)), Strict=false ; |
| 481 | | get_texpr_expr(C,less(LHS,RHS)), Strict=true ; |
| 482 | | get_texpr_expr(C,greater(RHS,LHS)), Strict=true |
| 483 | | ), |
| 484 | | evaluable_integer_expression(RHS,RestProp,R), |
| 485 | | (Strict=true -> MaxCard is R-1 ; MaxCard = R). |
| 486 | | |
| 487 | | maximum_cardinality_of_expression(b(E,_,_),Props,MC) :- maximum_cardinality_of_expression2(E,Props,MC). |
| 488 | | maximum_cardinality_of_expression2(set_extension(SetExtElements),_,MaxCard) :- |
| 489 | | length(SetExtElements,MaxCard). |
| 490 | | % we assume that all elements in List can be different |
| 491 | | maximum_cardinality_of_expression2(union(A,B),Props,MaxCard) :- |
| 492 | | maximum_cardinality_of_expression(A,Props,MA), |
| 493 | | maximum_cardinality_of_expression(B,Props,MB), MaxCard is MA+MB. |
| 494 | | maximum_cardinality_of_expression2(intersection(A,B),Props,MaxCard) :- |
| 495 | | maximum_cardinality_of_expression(A,Props,MA), |
| 496 | | maximum_cardinality_of_expression(B,Props,MB), MaxCard is min(MA,MB). |
| 497 | | maximum_cardinality_of_expression2(set_subtraction(A,_),Props,MaxCard) :- |
| 498 | | maximum_cardinality_of_expression(A,Props,MaxCard). |
| 499 | | maximum_cardinality_of_expression2(cartesian_product(A,B),Props,MaxCard) :- |
| 500 | | maximum_cardinality_of_expression(A,Props,MA), |
| 501 | | maximum_cardinality_of_expression(B,Props,MB), MaxCard is MA*MB. |
| 502 | | maximum_cardinality_of_expression2(identifier(ID),Props,MaxCard) :- % tested in testcase 1917 |
| 503 | | get_equality(Props,ID,RHS,RestProps),!, % remove equality to avoid loops, TO DO: try several equalities? |
| 504 | | maximum_cardinality_of_expression(RHS,RestProps,MaxCard). |
| 505 | | maximum_cardinality_of_expression2(empty_set,_,0). |
| 506 | | % TO DO: generalized union... |
| 507 | | %maximum_cardinality_of_expression2(Ex,_) :- nl, print(uncov_max_partition_card(Ex)),nl,nl,fail. |
| 508 | | % TO DO: other cases |
| 509 | | |
| 510 | | max_partition_card([],_,Acc,Acc). |
| 511 | | max_partition_card([TPartSet|T],Properties,Acc,Res) :- |
| 512 | | maximum_cardinality_of_expression(TPartSet,Properties,Max), |
| 513 | | NAcc is Acc+Max, |
| 514 | | max_partition_card(T,Properties,NAcc,Res). |
| 515 | | |
| 516 | | |
| 517 | | :- dynamic find_minimum_cardinality_cache/2. |
| 518 | | find_minimum_cardinality(GS,MC) :- |
| 519 | | find_minimum_cardinality_cache(GS,Nr),!, %print(min_card_cache(GS,Nr)),nl, |
| 520 | | % avoid loops; e.g., if we have N1 >->> N2 and N2 >->> N1 |
| 521 | | number(Nr), |
| 522 | | MC=Nr. |
| 523 | | find_minimum_cardinality(GlobalSetName,Res) :- % print(find_min_card(GlobalSetName)),nl, |
| 524 | | /* try to find out from the Properties whether there is an implied minimum cardinality */ |
| 525 | | b_get_machine_constants(Csts), |
| 526 | | b_get_properties_from_machine(Properties), |
| 527 | | assert(find_minimum_cardinality_cache(GlobalSetName,unknown)), |
| 528 | | findall(MinCard2,find_minimum_cardinality2(Csts,Properties,GlobalSetName,MinCard2),List), |
| 529 | | debug_println(9,mincard_list(GlobalSetName,List)), |
| 530 | | max_member(MinCard,List), % we do not allow empty global sets anymore, allow_empty_global_sets is obsolete |
| 531 | | MinCard>0, |
| 532 | | retract(find_minimum_cardinality_cache(GlobalSetName,_)), |
| 533 | | assert(find_minimum_cardinality_cache(GlobalSetName,MinCard)), |
| 534 | | Res=MinCard. |
| 535 | | |
| 536 | | find_minimum_cardinality2(_,Properties,GlobalSetName,MinCard) :- |
| 537 | ? | member_in_conjunction(C,Properties), |
| 538 | | find_minimum_cardinality3(C,Properties,GlobalSetName,MinCard). |
| 539 | | find_minimum_cardinality2(_Constants,_Properties,GlobalSetName,MinCard) :- |
| 540 | | %print(trying_find_min_card(GlobalSetName,Constants)),nl, |
| 541 | | b_get_disjoint_constants_of_type(GlobalSetName, DisjointConstants,_), |
| 542 | | length(DisjointConstants,MinCard), MinCard>1. |
| 543 | | |
| 544 | | find_minimum_cardinality3(C,Properties,GlobalSetName,MinCard) :- |
| 545 | | % check if the PROPERTIES contain an expression of the form card(GS) >= Nr or similar |
| 546 | | is_greaterequalthan_card_global_set(C,GlobalSetName,Properties,MinCard). |
| 547 | | find_minimum_cardinality3(C,Properties,GlobalSetName,MinCard) :- |
| 548 | | % find things like partition(GlobalSetName,S1,...,SN) |
| 549 | | get_texpr_expr(C,partition(Set,DisjSets)), |
| 550 | | global_set_identifier(Set,GlobalSetName), |
| 551 | | % print(partition(Set,DisjSets,GlobalSetName)),nl, |
| 552 | | find_min_card_of_disjoint_sets(DisjSets,Properties,MinCard). % ,print(min(MinCard)),nl. |
| 553 | | find_minimum_cardinality3(C,_Properties,GlobalSetName,MinCard) :- |
| 554 | | get_texpr_expr(C,member(_Something,SURJ)), |
| 555 | ? | is_surjection(SURJ,Set,OTHERSET), |
| 556 | | global_set_identifier(Set,GlobalSetName), |
| 557 | | \+ global_set_identifier(OTHERSET,GlobalSetName), % Surjection on itself; no use in narrowing down cardinality |
| 558 | | (minimum_cardinality(OTHERSET,MinCard) |
| 559 | | -> true |
| 560 | | ; print('*** could not compute mincard: '), print(OTHERSET),nl,fail), |
| 561 | | (MinCard=inf -> add_error(b_global_sets,'Set has to be of infinite cardinality: ',GlobalSetName),fail ; true). |
| 562 | | |
| 563 | | % is a surjective function |
| 564 | | is_surjection(SURJ,FromSet,ToSet) :- get_texpr_expr(SURJ,total_surjection(FromSet,ToSet)). |
| 565 | | is_surjection(SURJ,FromSet,ToSet) :- get_texpr_expr(SURJ,partial_surjection(FromSet,ToSet)). |
| 566 | | is_surjection(SURJ,FromSet,ToSet) :- get_texpr_expr(SURJ,total_bijection(FromSet,ToSet)). % here we know the exact cardinality - TO DO: use this fact |
| 567 | | is_surjection(SURJ,FromSet,ToSet) :- get_texpr_expr(SURJ,partial_bijection(FromSet,ToSet)). |
| 568 | | is_surjection(SURJ,FromSet,ToSet) :- get_texpr_expr(SURJ,total_injection(ToSet,FromSet)). % inverse is surjective |
| 569 | | |
| 570 | | |
| 571 | | |
| 572 | | % compute the minmum cardinality of an expression |
| 573 | | minimum_cardinality(ID,MinCard) :- global_set_identifier(ID,GlobalSet),!, |
| 574 | | (b_extract_fd_type(GlobalSet,LowBnd,UpBnd) |
| 575 | | -> MinCard is 1+UpBnd-LowBnd |
| 576 | | ; print('*** Do not know card of : '), print(GlobalSet),nl, |
| 577 | | % TO DO: do full blown cardinality analysis of deferred sets |
| 578 | | fail). |
| 579 | | minimum_cardinality(b(EXPR,TYPE,_INFO),MinCard) :- |
| 580 | | minimum_cardinality2(EXPR,TYPE,MinCard). |
| 581 | | |
| 582 | | %minimum_cardinality2(A,T,R) :- print(mincard(A,T,R)),nl,fail. |
| 583 | | minimum_cardinality2(bool_set,_,2). |
| 584 | | minimum_cardinality2(cartesian_product(A,B),_,Res) :- minimum_cardinality(A,CA), |
| 585 | | minimum_cardinality(B,CB), kernel_objects:safe_mul(CA,CB,Res). |
| 586 | | minimum_cardinality2(interval(A,B),_,Res) :- |
| 587 | | b_get_properties_from_machine(Properties), |
| 588 | | evaluable_integer_expression(A,Properties,EA), |
| 589 | | evaluable_integer_expression(B,Properties,EB), |
| 590 | | (EB >= EA -> Res is EB+1-EA ; Res=0). |
| 591 | | % TO DO: enumerated sets, ... seq, relations, ... ? |
| 592 | | |
| 593 | | |
| 594 | | find_min_card_of_disjoint_sets([],_Properties,0). |
| 595 | | find_min_card_of_disjoint_sets([H|T],Properties,R) :- |
| 596 | | find_min_card_of_disjoint_sets(T,Properties,TN), |
| 597 | | (minimum_cardinality_of_set(H,Properties,MC) |
| 598 | | -> true %,print(min_card(MC,H)),nl |
| 599 | | ; add_internal_error('Call failed: ',minimum_cardinality_of_set(H,Properties,MC)), MC=1), |
| 600 | | R is TN+MC. |
| 601 | | |
| 602 | | |
| 603 | | minimum_cardinality_of_set(b(Expr,set(Type),_),Properties,MC) :- |
| 604 | | minimum_cardinality_of_set_aux(Expr,Type,Properties,MC). |
| 605 | | |
| 606 | | %minimum_cardinality_of_set_aux(P,Type,_,_MC) :- print(min_card(P,Type)),nl,fail. |
| 607 | | minimum_cardinality_of_set_aux(set_extension(List),GlobalSetName,Properties,MinCard) :- !, |
| 608 | | def_get_texpr_ids(List,AtomicIDList), |
| 609 | | find_inequal_global_set_identifiers(AtomicIDList,GlobalSetName,Properties,DisjointConstants), |
| 610 | | length(DisjointConstants,MinCard). % , print(disj_set_ext(MinCard,DisjointConstants)),nl,nl. |
| 611 | | minimum_cardinality_of_set_aux(identifier(CST),_Type,_Properties,MinCard) :- |
| 612 | | find_minimum_cardinality_cache(CST,Nr),!, |
| 613 | | number(Nr), |
| 614 | | MinCard=Nr. |
| 615 | | minimum_cardinality_of_set_aux(identifier(CST),Type,Properties,MinCard) :- |
| 616 | | Cst_Template = b(identifier(CST),set(Type),_), |
| 617 | | min_card_of_identifier(Cst_Template,Type,Properties,MC), |
| 618 | | !, |
| 619 | | MinCard=MC, |
| 620 | | assert(find_minimum_cardinality_cache(CST,MC)). % global sets and constants cannot have the same name |
| 621 | | % TO DO: add more cases ? sequence extension cannot appear |
| 622 | | minimum_cardinality_of_set_aux(_,_,_,0). |
| 623 | | |
| 624 | | % determine minimum cardinality of an identifier; usually a constant (cannot be another global set due to B typing). |
| 625 | | min_card_of_identifier(Cst_Template,_Type,Properties,MinCard) :- |
| 626 | | member_in_conjunction(EqCardExpr,Properties), % look for card(CstTemplate) = MinCard |
| 627 | | is_equality_card_expression(EqCardExpr,Properties,Cst_Template,MinCard),!. % this is actually an exact card |
| 628 | | min_card_of_identifier(Cst_Template,_Type,Properties,MC) :- |
| 629 | | get_texpr_expr(PT,partition(Cst_Template,DisjSets)), |
| 630 | | member_in_conjunction(PT,Properties), |
| 631 | | find_min_card_of_disjoint_sets(DisjSets,Properties,MC),!. |
| 632 | | min_card_of_identifier(Cst_Template,Type,Properties,MinCard) :- % x:ID => card(ID) >= 1 |
| 633 | | get_texpr_id(TID,ID), |
| 634 | | get_texpr_expr(EL,member(TID,Cst_Template)), |
| 635 | | findall(ID,member_in_conjunction(EL,Properties),AtomicIDList), |
| 636 | | % find all identifiers such that we have id : CST |
| 637 | | AtomicIDList \= [], |
| 638 | | !, |
| 639 | | find_inequal_global_set_identifiers(AtomicIDList,Type,Properties,DisjointConstants), |
| 640 | | length(DisjointConstants,MinCard). |
| 641 | | min_card_of_identifier(Cst_Template,_Type,Properties,MC) :- % x:ID => card(ID) >= 1 |
| 642 | | get_texpr_expr(EL,member(_,Cst_Template)), |
| 643 | | member_in_conjunction(EL,Properties), |
| 644 | | %translate:print_bexpr(EL),nl, |
| 645 | | !, |
| 646 | | MC=1. |
| 647 | | min_card_of_identifier(Cst_Template,Type,Properties,MC) :- % ID /= {} => card(ID) >= 1 |
| 648 | | EMPTYSET = b(empty_set,set(Type),_), |
| 649 | | get_texpr_expr(NEQ,not_equal(LHS,RHS)), |
| 650 | | member_in_conjunction(NEQ,Properties), |
| 651 | | (LHS=Cst_Template, RHS=EMPTYSET ; |
| 652 | | RHS=Cst_Template, LHS=EMPTYSET ), |
| 653 | | %print(neq(NEQ,CST,RHS)),nl, |
| 654 | | !, |
| 655 | | MC=1. |
| 656 | | |
| 657 | | |
| 658 | | % the following could be further improved |
| 659 | | % try and find out how many different identifiers are in a list in the context of a predicate Prop |
| 660 | | % it is also called by b_get_disjoint_constants_of_type_calc in bmachine |
| 661 | | %find_inequal_global_set_identifiers(L,GS,_P,_R) :- print(find_inequal_global_set_identifiers(L,GS)),nl,fail. |
| 662 | | |
| 663 | | :- use_module(bsyntaxtree,[conjunction_to_list/2]). |
| 664 | | find_inequal_global_set_identifiers(IDS,GS,Prop,Res) :- |
| 665 | | conjunction_to_list(Prop,Preds), |
| 666 | | % first apply nested partition predicates as much as possible, to obtain maximally large partitions of distinct elements |
| 667 | | get_relevant_partition_preds(Preds,GS,RelevantPartitionPreds), % TO DO: cache this computation |
| 668 | | findall(TP,find_a_transitive_partition(RelevantPartitionPreds,TP),TransitivePartitions), |
| 669 | | append(TransitivePartitions,Preds,Preds2), |
| 670 | | find_inequal_global_set_identifiers2(IDS,GS,Preds2,Res). |
| 671 | | |
| 672 | | find_inequal_global_set_identifiers2([],_,_,[]). |
| 673 | | find_inequal_global_set_identifiers2([ID|T],GS,Preds,Res) :- |
| 674 | | (atomic(ID) -> true |
| 675 | | ; add_internal_error('Not atomic id: ',find_inequal_global_set_identifiers([ID|T],GS,Preds,Res)),fail), |
| 676 | | findall(ID2, (member(C,Preds), %print(chck(C)),nl, |
| 677 | | inequality(C,GS,ID,ID2,Preds), |
| 678 | | member(ID2,T)), DiffIDs), |
| 679 | | sort(DiffIDs,SortedDiffIDs), % also remove duplicates |
| 680 | | (SortedDiffIDs=[],T=[_,_|_] % then try to proceed with T, ignoring ID |
| 681 | | -> find_inequal_global_set_identifiers2(T,GS,Preds,Res) |
| 682 | | ; find_inequal_global_set_identifiers2(SortedDiffIDs,GS,Preds,RT), Res = [ID|RT] |
| 683 | | ). |
| 684 | | |
| 685 | | get_relevant_partition_preds(Preds,GS,SortedRelevantPartitionPreds) :- |
| 686 | | % detect which partition predicates are relevant for this global set |
| 687 | | findall(partition(Set,Subsets), |
| 688 | | (member(C,Preds), |
| 689 | | is_relevant_partition(C,GS,Set,Subsets)), RelevantPartitionPreds), |
| 690 | | sort(RelevantPartitionPreds,SortedRelevantPartitionPreds). |
| 691 | | is_relevant_partition(b(partition(Set,Subsets),pred,_),GS,Set,Subsets) :- |
| 692 | | get_texpr_type(Set,set(GS)). % , translate:print_bexpr(b(partition(Set,Subsets),pred,[])),nl. |
| 693 | | |
| 694 | | % if we have partition(A,[B,C]) and partition(B,[E,F]) --> generate partition(A,[E,F,C]) |
| 695 | | find_a_transitive_partition(Preds,b(partition(A,C),pred,[generated])) :- |
| 696 | | member(partition(A,B),Preds), |
| 697 | | inline_subsets(B,Preds,Inlined,C), Inlined==inlined. |
| 698 | | inline_subsets([],_,_,[]). |
| 699 | | inline_subsets([Subset1|TS],Preds,inlined,Result) :- get_texpr_id(Subset1,SubID), |
| 700 | | %prefix(Pred,[partition(S2,SubList)|Pred2]), |
| 701 | | select(partition(Subset2,SubList),Preds,Pred2), |
| 702 | | get_texpr_id(Subset2,SubID), |
| 703 | | format('Inlining nested partition predicate for set ~w~n',[SubID]), |
| 704 | | !, |
| 705 | | append(SubList,TS,NewList), |
| 706 | | inline_subsets(NewList,Pred2,_,Result). |
| 707 | | inline_subsets([Subset1|TS],Preds,Inlined,[Subset1|TSRes]) :- inline_subsets(TS,Preds,Inlined,TSRes). |
| 708 | | |
| 709 | | |
| 710 | | inequality(b(P,pred,_),GS,ID,OtherID,FullProps) :- |
| 711 | | inequality_aux(P,GS,ID,OtherID,FullProps). |
| 712 | | inequality_aux(not_equal(I1,I2),GS,ID,OtherID,_) :- |
| 713 | | gs_identifier(I1,GS,ID1), gs_identifier(I2,GS,ID2), |
| 714 | | (ID=ID1 -> OtherID=ID2 ; ID=ID2,OtherID=ID1). |
| 715 | | inequality_aux(not_equal(I1,I2),GS,ID,OtherID,_) :- % treat {aa} \= {bb} or more generally {aa,bb} \= {aa,cc} |
| 716 | | % two identifiers of global sets need not be different |
| 717 | | % in order for two set extensions to be inequal |
| 718 | | % first we check if I1, I2 are in fact subsets of global sets |
| 719 | | get_texpr_type(I1,set(global(_))), |
| 720 | | get_texpr_expr(I1,set_extension(IDs1)), % TODO: is there something more general than a set_extension? |
| 721 | | get_texpr_expr(I2,set_extension(IDs2)), % should full sets or set identifiers added? |
| 722 | | % remove the common elements and see if we find a pair of identifiers |
| 723 | | maplist(remove_all_infos_and_ground,IDs1,IDs1NoInfos), maplist(remove_all_infos_and_ground,IDs2,IDs2NoInfos), |
| 724 | | % TODO: maybe it is same to assume the order? |
| 725 | | list_to_ord_set(IDs1NoInfos,IDs1Set), list_to_ord_set(IDs2NoInfos,IDs2Set), |
| 726 | | ord_subtract(IDs1Set,IDs2Set,[E1]), % each set has one identifier that is not in the other one |
| 727 | | ord_subtract(IDs2Set,IDs1Set,[E2]), |
| 728 | | E1 \= E2, % and they are not the same |
| 729 | | gs_identifier(E1,GS,ID1), gs_identifier(E2,GS,ID2), |
| 730 | | (ID=ID1 -> OtherID=ID2 ; ID=ID2,OtherID=ID1). |
| 731 | | inequality_aux(negation( b(equal(I1,I2),pred,_)),GS,ID,OtherID,_) :- |
| 732 | | gs_identifier(I1,GS,ID1), gs_identifier(I2,GS,ID2), |
| 733 | | (ID=ID1 -> OtherID=ID2 ; ID=ID2,OtherID=ID1). |
| 734 | | inequality_aux(partition(Set,DisjSets),GS,ID,OtherID,Preds) :- |
| 735 | | get_texpr_type(Set,set(GS)), % only look at relevant partitions of correct type |
| 736 | | %nl,print(part(_Set,DisjSets,GS,ID,OtherID)),nl, |
| 737 | | % detect such things as partition(_,{...ID...},...{...OtherID...}...) |
| 738 | | select(Set1,DisjSets,Rest), set_extension_list(Set1,Preds,List1), |
| 739 | | member(O1,List1), gs_identifier(O1,GS,ID), |
| 740 | | member(Set2,Rest), set_extension_list(Set2,Preds,List2), |
| 741 | | member(O2,List2), gs_identifier(O2,GS,OtherID). |
| 742 | | inequality_aux(AllDiff,GS,ID,OtherID,Preds) :- |
| 743 | | all_different(AllDiff,List1,GS,Preds), |
| 744 | | select(O1,List1,RestList), gs_identifier(O1,GS,ID), |
| 745 | | member(O2,RestList), gs_identifier(O2,GS,OtherID). |
| 746 | | |
| 747 | | % detect card({x1,....,xn}) = n as an all-different predicate |
| 748 | | all_different(equal(A,B),List,Type,Preds) :- |
| 749 | | all_diff_aux(A,B,List,Type,Preds) ; all_diff_aux(B,A,List,Type,Preds). |
| 750 | | all_diff_aux(A,B,List1,Type,Preds) :- |
| 751 | | A=b(card(Set1),_,_), |
| 752 | | get_texpr_type(Set1,set(Type)), % TO DO: also match seq type ? (in case we use predicate in other context) |
| 753 | | set_extension_list(Set1,Preds,List1), |
| 754 | | evaluable_integer_expression(B,b(truth,pred,[]),Card), |
| 755 | | length(List1,Card). |
| 756 | | |
| 757 | | set_extension_list(b(set_extension(List),_,_),_,List). |
| 758 | | set_extension_list(b(identifier(ID),_,_),Preds,List) :- |
| 759 | | % accept card(GS) = nr & ... GS = {....} |
| 760 | | member(Eq,Preds), |
| 761 | | equality(Eq,TID,b(set_extension(List),_,_)), |
| 762 | | get_texpr_id(TID,ID). |
| 763 | | |
| 764 | | equality(b(equal(LHS,RHS),pred,_),L,R) :- ( (L,R)=(LHS,RHS) ; (L,R)=(RHS,LHS) ). |
| 765 | | |
| 766 | | gs_identifier(b(identifier(ID),GS,_),GS,ID). |
| 767 | | |
| 768 | | :- assert_must_succeed(( b_global_sets:is_equality_card_global_set(b(equal(b(card(b(identifier('FACES'),set(global('FACES')),[])),integer,[]),b(integer(6),integer,[])),pred,[]),GS,[],Card),GS='FACES',Card=6) |
| 769 | | ). |
| 770 | | :- assert_must_succeed(( b_global_sets:is_equality_card_global_set(b(equal(b(card(b(value(global_set('TITLE')),set(global('TITLE')),[])),integer,[]),b(integer(4),integer,[])),pred,[]),GS,[],Card), |
| 771 | | GS=='TITLE', Card=4) |
| 772 | | ). |
| 773 | | |
| 774 | | is_equality_card_expression(TE,Properties,Expr,Card) :- |
| 775 | ? | get_texpr_expr(TE,equal(LHS,RHS)), |
| 776 | ? | get_texpr_expr(LHS,L), get_texpr_expr(RHS,R), |
| 777 | ? | ( L=card(Expr),evaluable_integer_expression(R,Properties,Card) |
| 778 | | ; R=card(Expr),evaluable_integer_expression(L,Properties,Card)). |
| 779 | | |
| 780 | | is_equality_card_global_set(TE,GlobalSet,Properties,Card) :- |
| 781 | ? | is_equality_card_expression(TE,Properties,Expr,Card), |
| 782 | | global_set_identifier(Expr,GlobalSet), |
| 783 | | get_texpr_type(Expr,set(global(GlobalSet))). |
| 784 | | |
| 785 | | %evaluable_integer_expression(X,Y) :- print(ev(X,Y)),nl,fail. |
| 786 | | % TO DO: maybe we should do some kind of constant folding or call b_compile ?? |
| 787 | | evaluable_integer_expression(b(E,integer,_),Properties,R) :- |
| 788 | | evaluable_integer_expression(E,Properties,R). |
| 789 | | evaluable_integer_expression(max_int,_,R) :- preferences:preference(maxint,R). |
| 790 | | evaluable_integer_expression(min_int,_,R) :- preferences:preference(minint,R). |
| 791 | | evaluable_integer_expression(identifier(ID),Properties,R) :- |
| 792 | ? | get_texpr_expr(Eq,equal(LHS,RHS)), get_texpr_id(LHS,ID), |
| 793 | ? | select_member_in_conjunction(Eq,Properties,RestProp), % avoids loops; but an identifier cannot be used multiple times N+N |
| 794 | | evaluable_integer_expression(RHS,RestProp,R). |
| 795 | | evaluable_integer_expression(card(Set),_Properties,Card) :- % only works if we have already treated GlobalSetName ! TO DO: infer CLPFD constraints or treat sets in some order or look for definition in Properties (beware of cycles) |
| 796 | | Set = b(identifier(GlobalSetName),set(global(GlobalSetName)),_), |
| 797 | | extract_setsize_from_machine_cache(GlobalSetName,L,U), |
| 798 | | Card is U+1-L. |
| 799 | | evaluable_integer_expression(integer(Card),_,Card). |
| 800 | | evaluable_integer_expression(div(A,B),Properties,Res) :- |
| 801 | | evaluable_integer_expression(A,Properties,RA), |
| 802 | | evaluable_integer_expression(B,Properties,RB), Res is RA // RB. |
| 803 | | evaluable_integer_expression(multiplication(A,B),Properties,Res) :- |
| 804 | | evaluable_integer_expression(A,Properties,RA), |
| 805 | | evaluable_integer_expression(B,Properties,RB), Res is RA*RB. |
| 806 | | evaluable_integer_expression(add(A,B),Properties,Res) :- |
| 807 | | evaluable_integer_expression(A,Properties,RA), |
| 808 | | evaluable_integer_expression(B,Properties,RB), Res is RA+RB. |
| 809 | | evaluable_integer_expression(minus(A,B),Properties,Res) :- |
| 810 | | evaluable_integer_expression(A,Properties,RA), |
| 811 | | evaluable_integer_expression(B,Properties,RB), Res is RA-RB. |
| 812 | | evaluable_integer_expression(unary_minus(A),Properties,Res) :- |
| 813 | | evaluable_integer_expression(A,Properties,RA), Res is 0-RA. |
| 814 | | |
| 815 | | global_set_identifier(C,GS) :- get_texpr_expr(C,BE), global_set_identifier2(BE,GS). |
| 816 | | global_set_identifier2(identifier(GlobalSet),GlobalSet). |
| 817 | | global_set_identifier2(value(global_set(GlobalSet)),GlobalSet). % generated by Z |
| 818 | | |
| 819 | | % check for card(GlobalSet) >= Card or similar |
| 820 | | is_greaterequalthan_card_global_set(TE,GlobalSet,Properties,Card) :- |
| 821 | | (get_texpr_expr(TE,greater_equal(LHS,RHS)) ; |
| 822 | | get_texpr_expr(TE,less_equal(RHS,LHS)) ), |
| 823 | | get_texpr_expr(LHS,card(C)), |
| 824 | | get_minimum_or_exact_value(RHS,Properties,Card), |
| 825 | | global_set_identifier(C,GlobalSet), |
| 826 | | get_texpr_type(C,set(global(GlobalSet))). |
| 827 | | is_greaterequalthan_card_global_set(TE,GlobalSet,Properties,Card1) :- |
| 828 | ? | (get_texpr_expr(TE,greater(LHS,RHS)) ; |
| 829 | | get_texpr_expr(TE,less(RHS,LHS)) ), |
| 830 | | get_texpr_expr(LHS,card(C)), |
| 831 | | get_minimum_or_exact_value(RHS,Properties,Card), |
| 832 | | number(Card), Card1 is Card+1, |
| 833 | | global_set_identifier(C,GlobalSet), |
| 834 | | get_texpr_type(C,set(global(GlobalSet))). |
| 835 | | is_greaterequalthan_card_global_set(TE,GlobalSet,_Properties,2) :- |
| 836 | | %% preferences:get_preference(allow_empty_global_sets,false), preference no longer exists |
| 837 | | /* GlobalSet /= { ANY } -> as GlobalSet cannot be empty & as ANY must be well-typed: |
| 838 | | we need at least one more element of GlobalSet */ |
| 839 | | get_texpr_expr(TE,not_equal(LHS,RHS)), |
| 840 | | ( get_texpr_expr(LHS,identifier(GlobalSet)) |
| 841 | | -> get_texpr_expr(RHS,set_extension([b(_X,global(GlobalSet),_)])) |
| 842 | | ; get_texpr_expr(RHS,identifier(GlobalSet)), |
| 843 | | get_texpr_expr(LHS,set_extension([b(_X,global(GlobalSet),_)])) |
| 844 | | ). |
| 845 | | %%print(not_equal(GlobalSet,_X)),nl. |
| 846 | | % not_equal(S_CHEMIN_ID,b(set_extension([b(identifier(C_NULL_CHEMIN_ID),global(S_CHEMIN_ID),[nodeid(pos(35,1,80,27,80,42)),loc(local,emi,concrete_constants)])]),set(global(S_CHEMIN_ID)),[nodeid(pos(34,1,80,26,80,43))])) |
| 847 | | |
| 848 | | % get mininimum or exact value for an expression |
| 849 | | get_minimum_or_exact_value(TE,Properties,N) :- %print(get_min(TE,Properties)),nl,nl, |
| 850 | | get_texpr_expr(TE,E), |
| 851 | | get_minimum_or_exact_value_aux(E,Properties,N). |
| 852 | | get_minimum_or_exact_value_aux(integer(N),_,N). |
| 853 | | get_minimum_or_exact_value_aux(identifier(ID),Properties,N) :- |
| 854 | | (extract_min_or_exact_value_for_id(ID,Properties,N) -> true). % avoid backtracking; TO DO: in future all this should be part of constraint solving |
| 855 | | get_minimum_or_exact_value_aux(add(A,B),Properties,Res) :- |
| 856 | | get_minimum_or_exact_value(A,Properties,RA), |
| 857 | | get_minimum_or_exact_value(B,Properties,RB), Res is RA+RB. |
| 858 | | % TO DO: other operators |
| 859 | | get_minimum_or_exact_value_aux(card(Set),_Properties,Card) :- |
| 860 | | Set = b(identifier(GlobalSetName),set(global(GlobalSetName)),_), |
| 861 | | try_extract_setsize_from_machine(GlobalSetName,L,U), % will try extraction; unless a cycle is hit |
| 862 | | Card is U+1-L. |
| 863 | | |
| 864 | | extract_min_or_exact_value_for_id(ID,Properties,N) :- |
| 865 | | member_in_conjunction(TE,Properties), |
| 866 | | get_texpr_expr(TE,E), |
| 867 | | get_value_bound(E,ID,N). |
| 868 | | |
| 869 | | % equalities already inlined |
| 870 | | get_value_bound(equal(LHS,RHS),ID,N) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N). |
| 871 | | get_value_bound(equal(RHS,LHS),ID,N) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N). |
| 872 | | get_value_bound(greater(LHS,RHS),ID,N1) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N), N1 is N+1. |
| 873 | | get_value_bound(less(RHS,LHS),ID,N1) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N), N1 is N+1. |
| 874 | | get_value_bound(greater_equal(LHS,RHS),ID,N) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N). |
| 875 | | get_value_bound(less_equal(RHS,LHS),ID,N) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N). |
| 876 | | |
| 877 | | get_texpr_integer(b(integer(N),_,_),N). |
| 878 | | |
| 879 | | |
| 880 | | :- volatile global_set_user_defined_scope/2. |
| 881 | | :- dynamic global_set_user_defined_scope/2. |
| 882 | | |
| 883 | | /* allow to set scope for specific sets, e.g., via command-line */ |
| 884 | | set_user_defined_scope(GS,X) :- |
| 885 | | \+ number(X),!, |
| 886 | | add_internal_error('Scope must be number: ',set_user_defined_scope(GS,X)). |
| 887 | | set_user_defined_scope(GS,X) :- |
| 888 | | format('% Setting user defined scope: ~w == ~w~n',[GS,X]), |
| 889 | | assert(global_set_user_defined_scope(GS,X)). |
| 890 | | |
| 891 | | get_user_defined_scope(GlobalSetName,LowBound,UpBound) :- |
| 892 | | (var(GlobalSetName) |
| 893 | | -> add_error(get_user_defined_scope,'Arg is variable: ',get_user_defined_scope) ; true), |
| 894 | | (global_set_user_defined_scope(GlobalSetName,UpBound) |
| 895 | | -> LowBound=1 |
| 896 | | ; extract_setsize_from_defs(GlobalSetName,LowBound,UpBound)). |
| 897 | | |
| 898 | | :- use_module(translate,[translate_bexpression/2]). |
| 899 | | extract_setsize_from_defs(GlobalSetName,LowBound,UpBound) :- |
| 900 | | b_get_machine_setscope(GlobalSetName,DefTerm), |
| 901 | | get_texpr_expr(DefTerm,DefExpr), |
| 902 | | (extract_integer_range(DefExpr,LowBound,UpBound) |
| 903 | | -> true |
| 904 | | ; translate_bexpression(DefTerm,DS), |
| 905 | | add_warning(extract_setsize_from_defs,'scope DEFINITION for deferred set should be number or interval: ',DS,DefTerm), |
| 906 | | fail |
| 907 | | ). |
| 908 | | |
| 909 | | extract_integer_range(interval(LB,UB), LowBound, UpBound) :- |
| 910 | | get_texpr_expr(LB,integer(LowBound)), get_texpr_expr(UB,integer(UpBound)). |
| 911 | | %extract_integer_range(set_extension(CstList),LowBound,UpBound) :- |
| 912 | | % LowBound = 1, length(CstList,UpBound). % extract names of constants in list for pretty printing; check that different names |
| 913 | | %extract_integer_range(value(avl_set(A)),LowBound,UpBound) :- |
| 914 | | % LowBound = 1, avl:avl_size(A,UpBound). |
| 915 | | extract_integer_range(integer(UpBound),LowBound,UpBound) :- |
| 916 | | LowBound = 1, UpBound>0. |
| 917 | | |
| 918 | | |
| 919 | | :- dynamic start_extracting_setsize/1. |
| 920 | | |
| 921 | | start_extracting_setsize_from_machine(GlobalSetName) :- %print(start(GlobalSetName)),nl, |
| 922 | | (start_extracting_setsize(GlobalSetName) |
| 923 | | -> add_internal_error('Cyclic computation: ',start_extracting_setsize_from_machine(GlobalSetName)) |
| 924 | | ; assert(start_extracting_setsize(GlobalSetName))). |
| 925 | | |
| 926 | | assert_extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound) :- |
| 927 | | retractall(start_extracting_setsize(GlobalSetName)), |
| 928 | | %print(finished(GlobalSetName,LowBound,UpBound)),nl, |
| 929 | | (retract(extract_setsize_from_machine_cache(GlobalSetName,L,U)) |
| 930 | | -> print(overriding_set_size(GlobalSetName,LowBound-UpBound,L-U)),nl |
| 931 | | ; true), |
| 932 | | assert(extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound)), |
| 933 | | (UpBound<LowBound |
| 934 | | -> format_error('*** illegal empty global set ~w, bounds ~w:~w~n',[GlobalSetName,LowBound,UpBound]) |
| 935 | | ; true |
| 936 | | ). |
| 937 | | |
| 938 | | |
| 939 | | %% b_try_update_fd_cardinality has been removed |
| 940 | | |
| 941 | | :- volatile enumerated_set/1, fixed_deferred_set_size/2. |
| 942 | | :- dynamic enumerated_set/1, fixed_deferred_set_size/2. |
| 943 | | % true if GS is a deferred set whose size was not fixed; i.e., ProB has not inspected all possible instantiations |
| 944 | | unfixed_deferred_set(GS) :- |
| 945 | | b_global_set(GS), \+ enumerated_set(GS), \+ fixed_deferred_set_size(GS,_). |
| 946 | | |
| 947 | | contains_unfixed_deferred_set(Type) :- unfixed_deferred_set(Type). |
| 948 | | contains_unfixed_deferred_set(global(Type)) :- contains_unfixed_deferred_set(Type). |
| 949 | | contains_unfixed_deferred_set(set(Type)) :- contains_unfixed_deferred_set(Type). |
| 950 | | contains_unfixed_deferred_set(seq(Type)) :- contains_unfixed_deferred_set(Type). |
| 951 | | contains_unfixed_deferred_set(couple(Type1,Type2)) :- |
| 952 | | contains_unfixed_deferred_set(Type1) ; contains_unfixed_deferred_set(Type2). |
| 953 | | contains_unfixed_deferred_set(record(Fields)) :- |
| 954 | | ((member(field(_,Type),Fields), contains_unfixed_deferred_set(Type)) -> true). |
| 955 | | |
| 956 | | :- assert_pre(b_global_sets:assert_enumerated_set(_GS,_L,_,_),true). |
| 957 | | % TODO(DP, 7.8.2008) |
| 958 | | % (atomic(GS),type_check(L,list(xml_identifier)))). |
| 959 | | :- assert_post(b_global_sets:assert_enumerated_set(_,_,L,U),(number(L),number(U))). |
| 960 | | |
| 961 | | assert_enumerated_set(GlobalSetName,ListOfConstants,LowBound,UpBound) :- |
| 962 | | assert(enumerated_set(GlobalSetName)), |
| 963 | | % print_message(enum_set(GlobalSetName,ListOfConstants)), |
| 964 | | LowBound = 1, |
| 965 | | length(ListOfConstants,UpBound), |
| 966 | | assert_extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound), |
| 967 | | add_named_constants_to_global_set(GlobalSetName,ListOfConstants). |
| 968 | | |
| 969 | | add_named_constants_to_global_set(GlobalSetName,ListOfConstants) :- |
| 970 | | (b_global_constant(GlobalSetName,CurNr,CurCst) |
| 971 | | -> add_error_fail(add_named_constants_to_global_set,'Globalset already has constants: ', |
| 972 | | b_global_constant(GlobalSetName,CurNr,CurCst)) |
| 973 | | ; true), |
| 974 | ? | nth1(Nr,ListOfConstants,Cst), |
| 975 | | (b_global_constant(GS2,_,Cst) |
| 976 | | -> (GS2=GlobalSetName |
| 977 | | -> add_internal_error('Duplicate element in global set:',(Cst,GS2)) % error is already caught by type checker |
| 978 | | ; add_internal_error('Element appears in multiple sets:',(Cst,GS2,GlobalSetName)) % ditto |
| 979 | | ) |
| 980 | | ; true |
| 981 | | ), |
| 982 | | assert(b_global_constant(GlobalSetName,Nr,Cst)), |
| 983 | | assert(lookup_global_constant(Cst,fd(Nr,GlobalSetName))), |
| 984 | | fail. |
| 985 | | add_named_constants_to_global_set(_,_). |
| 986 | | |
| 987 | | |
| 988 | | %add_global_set_with_named_constants(GlobalSetName,ListOfConstants) :- |
| 989 | | % ~~pp_mnf(b_global_sets:assert_enumerated_set(GlobalSetName,ListOfConstants,_,_)), |
| 990 | | % add_new_global_set(GlobalSetName). |
| 991 | | |
| 992 | | |
| 993 | | |
| 994 | | :- assert_pre(b_global_sets:b_extract_fd_type(_G,_L,_U),true). |
| 995 | | :- assert_post(b_global_sets:b_extract_fd_type(G,L,U),(atomic(G),(integer(L),integer(U)))). |
| 996 | | |
| 997 | | b_extract_fd_type(GlobalSetName,LowBound,UpBound) :- |
| 998 | ? | b_global_set(GlobalSetName), % was b_get_machine_set(GlobalSetName), |
| 999 | | extract_setsize_from_machine(GlobalSetName,LowBound,UpBound). |
| 1000 | | |
| 1001 | | is_b_precompiled_globalset(GlobalSetName) :- extract_setsize_from_machine_cache(GlobalSetName,_,_). |
| 1002 | | |
| 1003 | | % like b_extract_fd_type above, but with GS known (avoids backtracking b_supplementary_global_set) |
| 1004 | | b_get_fd_type_bounds(NonvarGlobalSetname,LowBound,UpBound) :- nonvar(NonvarGlobalSetname), |
| 1005 | | extract_setsize_from_machine_cache(NonvarGlobalSetname,L,U), |
| 1006 | | !, |
| 1007 | | (LowBound,UpBound)=(L,U). |
| 1008 | | b_get_fd_type_bounds(GS,L,U) :- add_internal_error('Illegal call: ',b_get_fd_type_bounds(GS,L,U)),fail. |
| 1009 | | |
| 1010 | | b_global_set_cardinality('STRING',Card) :- !, Card=inf. |
| 1011 | | b_global_set_cardinality('NAT',Card) :- !, get_preference(maxint,MaxInt), Card is MaxInt+1. |
| 1012 | | b_global_set_cardinality('NATURAL',Card) :- !, Card=inf. %get_preference(maxint,MaxInt), Card is MaxInt+1. |
| 1013 | | b_global_set_cardinality('NAT1',Card) :- !, get_preference(maxint,Card). |
| 1014 | | b_global_set_cardinality('NATURAL1',Card) :- !, Card=inf. % get_preference(maxint,Card). |
| 1015 | | b_global_set_cardinality('INT',Card) :- !, get_preference(maxint,MaxInt), |
| 1016 | | get_preference(minint,MinInt), |
| 1017 | | (MaxInt >= MinInt -> Card is MaxInt-MinInt+1 |
| 1018 | | ; add_error(b_global_set_cardinality,'MININT larger than MAXINT',(MinInt:MaxInt)), |
| 1019 | | Card = 0 |
| 1020 | | ). |
| 1021 | | b_global_set_cardinality('INTEGER',Card) :- !, Card=inf. % b_global_set_cardinality('INT',Card). |
| 1022 | | b_global_set_cardinality(GlobalSet,Card) :- nonvar(GlobalSet),!, |
| 1023 | | (b_get_fd_type_bounds(GlobalSet,Low,Up) -> Card is 1+ Up - Low |
| 1024 | | ; add_internal_error('Unknown global set: ', b_global_set_cardinality(GlobalSet,Card)), |
| 1025 | | fail). |
| 1026 | | b_global_set_cardinality(GlobalSet,Card) :- %b_global_set(GlobalSet), |
| 1027 | | b_extract_fd_type(GlobalSet,Low,Up), Card is 1+ Up - Low. |
| 1028 | | % enum_warning_for_global_set(GlobalSet,'assuming deferred set to be of given cardinality',Card,trigger_true(card)). |
| 1029 | | %% Note: The Disprover now checks whether unfixed_deferred sets were involved; keeping track of implicit enumerations of deferred sets is just too difficult |
| 1030 | | |
| 1031 | | b_fd_card(GlobalSet,Card) :- b_get_fd_type_bounds(GlobalSet,Low,Up), Card is 1+ Up - Low. |
| 1032 | | |
| 1033 | | b_non_empty_global_set(_). % allow_empty_global_sets no longer exists; all global_sets are non-empty |
| 1034 | | %b_non_empty_global_set(IntSet) :- b_integer_or_string_set(IntSet). |
| 1035 | | %b_non_empty_global_set(GlobalSet) :- b_global_set(GlobalSet), |
| 1036 | | % b_get_fd_type_bounds(GlobalSet,Low,Up), Up >= Low. |
| 1037 | | |
| 1038 | | b_empty_global_set(_) :- fail. % allow_empty_global_sets no longer exists; all global_sets are non-empty |
| 1039 | | %b_empty_global_set(GlobalSet) :- %b_global_set(GlobalSet), |
| 1040 | | % b_get_fd_type_bounds(GlobalSet,Low,Up), Up < Low. |
| 1041 | | |
| 1042 | | |
| 1043 | | b_integer_or_string_set('STRING'). |
| 1044 | | b_integer_or_string_set(X) :- b_integer_set(X). |
| 1045 | | |
| 1046 | | b_integer_set('NAT'). b_integer_set('NATURAL'). |
| 1047 | | b_integer_set('NAT1'). b_integer_set('NATURAL1'). |
| 1048 | | b_integer_set('INT'). b_integer_set('INTEGER'). |
| 1049 | | |
| 1050 | | % convert a type term into a global_set term |
| 1051 | | try_b_type2global_set(string,R) :- !, R= global_set('STRING'). |
| 1052 | | try_b_type2global_set(integer,R) :- !, R= global_set('INTEGER'). |
| 1053 | ? | try_b_type2global_set(global(GS),R) :- b_global_set(GS),!, R=global_set(GS). |
| 1054 | | try_b_type2global_set(freetype(ID),R) :- !, R=freetype(ID). |
| 1055 | | try_b_type2global_set(boolean,R) :- !, |
| 1056 | | %custom_explicit_sets:construct_avl_from_lists([pred_false /* bool_false */,pred_true /* bool_true */],R). |
| 1057 | | R = avl_set(node(pred_false,true,1,empty,node(pred_true,true,0,empty,empty))). |
| 1058 | | |
| 1059 | | b_type2_set(GS,Res) :- try_b_type2global_set(GS,GR),!, Res=GR. |
| 1060 | | b_type2_set(Type,Res) :- Res = closure(['_zzzz_unary'],[Type],b(truth,pred,[])). |
| 1061 | | %b_type2global_set(GS,_) :- add_error_and_fail(b_type2_set,'Type cannot be converted to global_set: ',GS). |
| 1062 | | |
| 1063 | | %:- use_module(fd_utils). |
| 1064 | | :- use_module(fd_utils_clpfd). |
| 1065 | | |
| 1066 | | global_type(fd(X,GlobalSet),GlobalSet) :- %b_global_set(GlobalSet), |
| 1067 | | if(b_get_fd_type_bounds(GlobalSet,Low,Up), %print(b_get_fd_type_bounds(X,GlobalSet,Low,Up)),nl, when(nonvar(X),trace), |
| 1068 | | % print(in_fd(X,Low,Up)),nl, |
| 1069 | | in_fd(X,Low,Up), |
| 1070 | | add_internal_error('Illegal global set: ',global_type(fd(X,GlobalSet),GlobalSet))). |
| 1071 | | global_type2(X,GlobalSet) :- %b_global_set(GlobalSet), |
| 1072 | | if(b_get_fd_type_bounds(GlobalSet,Low,Up), |
| 1073 | | in_fd(X,Low,Up), |
| 1074 | | add_internal_error('Illegal global set: ',global_type2(X,GlobalSet))). |
| 1075 | | |
| 1076 | | global_type_wf(fd(X,GlobalSet),GlobalSet,WF) :- %b_global_set(GlobalSet), |
| 1077 | | b_get_fd_type_bounds(GlobalSet,Low,Up), %print(b_get_fd_type_bounds(X,GlobalSet,Low,Up)),nl, |
| 1078 | | in_fd_wf(X,Low,Up,WF). |
| 1079 | | |
| 1080 | | % get value and setup global_type FD constraint if it is a variable |
| 1081 | | get_global_type_value(FD,Type,X) :- |
| 1082 | | (var(FD), % print(fresh(Type,FD)),nl, |
| 1083 | | nonvar(Type) -> global_type2(X,Type) % instantiate FD bounds if we create a fresh FD variable X |
| 1084 | | ; true), |
| 1085 | | FD = fd(X,Type). |
| 1086 | | |
| 1087 | | % like enum_global_type but with a nonvar GlobalSet + generate enum_warning for deferred set (currently commented out) |
| 1088 | | enumerate_global_type_with_enum_warning(R,GlobalSet,_EnumWarning) :- var(R),!, % print(enum_var(R,GlobalSet)),nl, |
| 1089 | | b_get_fd_type_bounds(GlobalSet,Low,Up), % first setup CLP(FD) bounds before instantiating |
| 1090 | | in_fd(X,Low,Up), |
| 1091 | | R=fd(X,GlobalSet), |
| 1092 | | enum_fd(X,Low,Up). |
| 1093 | | enumerate_global_type_with_enum_warning(fd(X,GlobalSet),GlobalSet,_EnumWarning) :- |
| 1094 | ? | (nonvar(X) -> true |
| 1095 | ? | ; b_get_fd_type_bounds(GlobalSet,Low,Up), |
| 1096 | | %enum_warning_for_global_set(GlobalSet,'assuming deferred set to be of finite cardinality','?',EnumWarning), |
| 1097 | ? | enum_fd(X,Low,Up) |
| 1098 | | ). |
| 1099 | | |
| 1100 | | |
| 1101 | | enum_global_type(fd(X,GlobalSet),GlobalSet) :- %b_global_set(GlobalSet), |
| 1102 | ? | (nonvar(GlobalSet) -> |
| 1103 | | (b_get_fd_type_bounds(GlobalSet,Low,Up) -> enum_global_type_aux(X,Low,Up,GlobalSet) |
| 1104 | | ; add_internal_error('Illegal value: ',enum_global_type(fd(X,GlobalSet),GlobalSet)),fail) |
| 1105 | ? | ; b_global_set(GlobalSet), |
| 1106 | ? | b_get_fd_type_bounds(GlobalSet,Low,Up), |
| 1107 | ? | enum_global_type_aux(X,Low,Up,GlobalSet) |
| 1108 | | ). |
| 1109 | | |
| 1110 | | enum_global_type_aux(X,Low,Up,GlobalSet) :- |
| 1111 | | atomic(X), |
| 1112 | | !, |
| 1113 | | ((number(X),X >= Low, X =< Up) |
| 1114 | | -> true |
| 1115 | | ; add_internal_error('Illegal value: ', enum_global_type_aux(X,Low,Up,GlobalSet))). |
| 1116 | | enum_global_type_aux(X,Low,Up,_GlobalSet) :- |
| 1117 | ? | enum_fd(X,Low,Up). |
| 1118 | | |
| 1119 | | % get range information for global set and generate warning if necessary |
| 1120 | | %b_fd_type_with_enum_warning(GlobalSet,Low,Up) :- |
| 1121 | | % b_fd_type(GlobalSet,Low,Up), |
| 1122 | | % enum_warning_for_global_set(GlobalSet,'assuming deferred set to be of finite cardinality',Up,trigger_true(card)). |
| 1123 | | |
| 1124 | | /* ------------------------------------- */ |
| 1125 | | |
| 1126 | | |
| 1127 | | :- block all_elements_of_type(-,?). |
| 1128 | | all_elements_of_type(Type,Set) :- % print(all_elements(Type,Set)),nl, |
| 1129 | | all_elements_of_type2(Type,Set). |
| 1130 | | |
| 1131 | | :- use_module(kernel_objects,[all_strings/1, enum_warning/5]). |
| 1132 | | all_elements_of_type2('STRING',Res) :- !, |
| 1133 | | all_strings(Res). |
| 1134 | | all_elements_of_type2('NAT',Res) :- !, get_preference(maxint,MaxInt), |
| 1135 | | gen_int_set(0,MaxInt,Res). |
| 1136 | | all_elements_of_type2('NATURAL',Res) :- !, get_preference(maxint,MaxInt), |
| 1137 | | enum_warning('NATURAL',0:sup,0:MaxInt,trigger_throw('NATURAL'),unknown), %print('### Warning: expanding NATURAL'),nl, |
| 1138 | | gen_int_set(0,MaxInt,Res). |
| 1139 | | all_elements_of_type2('NAT1',Res) :- !, get_preference(maxint,MaxInt), |
| 1140 | | gen_int_set(1,MaxInt,Res). |
| 1141 | | all_elements_of_type2('NATURAL1',Res) :- !, |
| 1142 | | get_preference(maxint,MaxInt), |
| 1143 | | enum_warning('NATURAL1',1:sup,1:MaxInt,trigger_throw('NATURAL1'),unknown), %print('### Warning: expanding NATURAL1'),nl, |
| 1144 | | gen_int_set(1,MaxInt,Res). |
| 1145 | | all_elements_of_type2('INT',Res) :- !, get_preference(maxint,MaxInt), |
| 1146 | | get_preference(minint,MinInt), |
| 1147 | | gen_int_set(MinInt,MaxInt,Res). |
| 1148 | | all_elements_of_type2('INTEGER',Res) :- !, get_preference(maxint,MaxInt), |
| 1149 | | get_preference(minint,MinInt), |
| 1150 | | enum_warning('INTEGER',inf:sup,MinInt:MaxInt,trigger_throw('INTEGER'),unknown), %print('### Warning: expanding INTEGER'),nl, |
| 1151 | | gen_int_set(MinInt,MaxInt,Res). |
| 1152 | | all_elements_of_type2(Type,Set) :- |
| 1153 | | b_get_fd_type_bounds(Type,Low,Up), |
| 1154 | | % ensure we do not use Random enumeration |
| 1155 | | findall(fd(El,Type),enum_fd_linear(El,Low,Up),Set). |
| 1156 | | |
| 1157 | | % a version of all_elements_of_type which may randomise element order if preference set |
| 1158 | | :- block all_elements_of_type_rand(-,?). |
| 1159 | | all_elements_of_type_rand(Type,Set) :- % print(all_elements(Type,Set)),nl, |
| 1160 | | all_elements_of_type_rand2(Type,Set). |
| 1161 | | |
| 1162 | | all_elements_of_type_rand2(Type,Set) :- b_global_set(Type),!, |
| 1163 | | b_get_fd_type_bounds(Type,Low,Up), |
| 1164 | | % may use Random enumeration if preference RANDOMISE_ENUMERATION_ORDER set |
| 1165 | | findall(fd(El,Type),enum_fd(El,Low,Up),Set). |
| 1166 | | all_elements_of_type_rand2(Type,Set) :- % TO DO: we could permute the solution here; but currently all_elements_of_type_rand2 is only called for enumerated/deferred sets |
| 1167 | | all_elements_of_type2(Type,Set). |
| 1168 | | |
| 1169 | | |
| 1170 | | gen_int_set(Min,Max,Set) :- |
| 1171 | | ((Min>Max) -> (Set = []) |
| 1172 | | ; (Set = [int(Min)|RSet], |
| 1173 | | M1 is Min+1, |
| 1174 | | gen_int_set(M1,Max,RSet))). |