| 1 | | % (c) 2009-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(b_global_sets, |
| 6 | | [b_get_global_constants/1, b_get_enumerated_set_constants/1, |
| 7 | | b_get_global_enumerated_sets/1, b_get_global_sets/1, |
| 8 | | lookup_global_constant/2, |
| 9 | | is_b_global_constant/3, |
| 10 | | is_b_global_constant_hash/3, % a variation with indexing of first two args |
| 11 | | is_used_b_global_constant/3, is_unused_b_global_constant/2, |
| 12 | | |
| 13 | | b_global_set/1, b_non_empty_global_set/1, b_empty_global_set/1, |
| 14 | | b_global_deferred_set/1, |
| 15 | | b_global_set_with_potential_symmetry/1, b_global_deferred_set_with_card_gt1/1, |
| 16 | | b_partially_deferred_set/1, |
| 17 | | |
| 18 | | enumerated_set/1, |
| 19 | | unfixed_deferred_set/1, unfixed_deferred_set_exists/0, |
| 20 | | fixed_deferred_set_size/2, |
| 21 | | provably_finite_global_set/1, infinite_global_set/1, |
| 22 | | contains_unfixed_deferred_set/1, contains_unfixed_deferred_set/2, |
| 23 | | b_supplementary_global_set/1, % introduced when untyped ids are allowed |
| 24 | | |
| 25 | | inferred_minimum_global_set_cardinality/2, |
| 26 | | inferred_maximum_global_set_cardinality/2, |
| 27 | | b_exists_global_set_with_potential_symmetry/0, |
| 28 | | b_global_set_cardinality/2, |
| 29 | | |
| 30 | | b_clear_global_set_type_definitions/0, |
| 31 | | |
| 32 | | % three phases of precompilation: |
| 33 | | b_check_and_precompile_enumerated_sets/0, |
| 34 | | b_check_and_precompile_deferred_sets/0, |
| 35 | | b_check_and_precompile_global_set_symmetry/0, |
| 36 | | % can be called before precompilation: |
| 37 | | register_enumerated_sets/2, |
| 38 | | |
| 39 | | b_get_prob_deferred_set_elements/2, |
| 40 | | add_prob_deferred_set_elements_to_store/3, |
| 41 | | inline_prob_deferred_set_elements_into_bexpr/2, |
| 42 | | prob_deferred_set_element/4, |
| 43 | | |
| 44 | | find_inequal_global_set_identifiers/4, |
| 45 | | static_symmetry_reduction_for_global_sets/1, |
| 46 | | |
| 47 | | b_integer_set/1, b_integer_or_real_or_string_set/1, b_integer_or_real_set/1, |
| 48 | | b_type2_set/2, try_b_type2global_set/2, |
| 49 | | |
| 50 | | %b_fd_type/3, |
| 51 | | b_get_fd_type_bounds/3, |
| 52 | | b_fd_card/2, |
| 53 | | is_global_set_of_cardinality_one/2, %is_global_set_of_cardinality_two/3, |
| 54 | | global_type/2, global_type_wf/3, |
| 55 | | get_global_type_value/3, |
| 56 | | enum_global_type_limited/2, enumerate_global_type_with_enum_warning/4, |
| 57 | | |
| 58 | | all_elements_of_type/2, all_elements_of_type_wf/3, |
| 59 | | all_elements_of_type_rand_wf/3, |
| 60 | | |
| 61 | | set_user_defined_scope/2, get_user_defined_scope/4, |
| 62 | | |
| 63 | | generate_fresh_supplementary_global_set/1, |
| 64 | | register_replaced_global_set/2, b_replaced_global_set/2, |
| 65 | | %,add_global_set_with_named_constants/2 /* for use by Z,... */ |
| 66 | | list_contains_unfixed_deferred_set_id/1 |
| 67 | | ]). |
| 68 | | |
| 69 | | :- use_module(debug). |
| 70 | | :- use_module(tools). |
| 71 | | :- use_module(library(lists)). |
| 72 | | :- use_module(library(ordsets)). |
| 73 | | :- use_module(library(avl)). |
| 74 | | :- use_module(self_check). |
| 75 | | :- use_module(preferences). |
| 76 | | :- use_module(error_manager). |
| 77 | | :- use_module(bsyntaxtree). |
| 78 | | :- use_module(library(between),[between/3]). |
| 79 | | :- use_module(gensym,[gensym/2]). |
| 80 | | |
| 81 | | :- use_module(module_information,[module_info/2]). |
| 82 | | :- module_info(group,kernel). |
| 83 | | :- module_info(description,'This module provides support for deferred/enumerated set elements in B.'). |
| 84 | | |
| 85 | | :- use_module(bmachine,[b_get_properties_from_machine/1, |
| 86 | | b_get_machine_constants/1, b_get_machine_variables/1, |
| 87 | | b_get_named_machine_set/2, b_get_machine_set/1, |
| 88 | | b_get_all_used_identifiers/1, % required for symmetry-related infos |
| 89 | | b_get_disjoint_constants_of_type/3, |
| 90 | | b_extract_values_clause_assignment/3, |
| 91 | | b_get_typed_definition/3, b_get_machine_setscope/2]). |
| 92 | | |
| 93 | | /* what we call global sets here usually called "given sets", which can be |
| 94 | | either enumerated or deferred */ |
| 95 | | |
| 96 | | |
| 97 | | :- dynamic b_global_constant/3. % named element of a deferred or enumerated set |
| 98 | | % for enumerated sets S = {a,b,c} we would have entries a,b,c as b_global_constant |
| 99 | | % for deferred set S, we may add CONSTANTS which are element of S as b_global_constant |
| 100 | | :- dynamic used_b_global_constant/3. |
| 101 | | |
| 102 | | :- dynamic inferred_minimum_global_set_cardinality/2. |
| 103 | | :- dynamic inferred_maximum_global_set_cardinality/2. |
| 104 | | |
| 105 | | %% b_get_global_enumerated_sets(-GSets). |
| 106 | | % Returns all fully and partially enumerated sets. |
| 107 | | b_get_global_enumerated_sets(GSets) :- |
| 108 | | findall(GS, (b_global_set(GS), \+ b_global_deferred_set(GS)), GSets). |
| 109 | | b_get_global_sets(GSets) :- |
| 110 | | findall(GS, b_global_set(GS), GSets). |
| 111 | | |
| 112 | | b_get_global_constants(Csts) :- findall(Cst,is_b_global_constant(_,_,Cst),Csts). |
| 113 | | % only get those elements that have been explicitly marked as enumerated; excludes partially enumerated sets. |
| 114 | | %b_get_enumerated_set_constants(Set,Csts) :- enumerated_set(Set),findall(Cst,is_b_global_constant(Set,_,Cst),Csts). |
| 115 | | b_get_enumerated_set_constants(Csts) :- findall(Cst,(enumerated_set(Set),is_b_global_constant(Set,_,Cst)),Csts). |
| 116 | | |
| 117 | | % getting named elements of SETS: |
| 118 | ? | is_b_global_constant(Set,Nr,Cst) :- b_global_constant(Set,Nr,Cst). |
| 119 | | |
| 120 | | :- use_module(library(terms),[term_hash/2]). |
| 121 | | % efficient indexing if both GS and X are known, useful for large global sets |
| 122 | | is_b_global_constant_hash(GS,Nr,Name) :- |
| 123 | ? | term_hash(fd(Nr,GS),Hash), b_global_constant_hash(Hash,GS,Nr,Name). |
| 124 | | |
| 125 | | is_unused_b_global_constant(Set,Nr) :- |
| 126 | | b_get_fd_type_bounds_limited(Set,Low,Up), |
| 127 | ? | between(Low,Up,Nr), |
| 128 | | \+ used_b_global_constant(Set,Nr,_). |
| 129 | | is_used_b_global_constant(Set,Nr,Cst) :- |
| 130 | | used_b_global_constant(Set,Nr,Cst). |
| 131 | | |
| 132 | | b_get_fd_type_bounds_limited(GlobalSet,Low,UpLimited) :- |
| 133 | | b_get_fd_type_bounds(GlobalSet,Low,Up), |
| 134 | | (Up=inf -> add_message(b_global_sets,'Limiting infinite deferred set elements to 999: ',GlobalSet), |
| 135 | | UpLimited=999 |
| 136 | | ; UpLimited=Up). |
| 137 | | |
| 138 | | :- dynamic lookup_global_constant/2, b_global_constant_hash/4. |
| 139 | | %lookup_global_constant(Id,Val) :- |
| 140 | | % b_global_constant(Set,Nr,Id), % not an indexed lookup ; now we assert lookup_global_constant below |
| 141 | | % Val = fd(Nr,Set). |
| 142 | | |
| 143 | | |
| 144 | | :- dynamic b_precompiled_global_set/1. |
| 145 | | b_precompiled_global_set(_) :- print_error('*** b_global_set not precompiled'),fail. |
| 146 | | |
| 147 | ? | b_global_set(GS) :- b_precompiled_global_set(GS) ; b_supplementary_global_set(GS). |
| 148 | | |
| 149 | | % a version of b_global_set which does not leave a trailing choice point for b_supplementary_global_set around |
| 150 | | % has to be called with GS ground |
| 151 | | %b_global_set_ground(GS) :- if(b_precompiled_global_set(GS),true,b_supplementary_global_set(GS)). |
| 152 | | |
| 153 | | % Does not contain partially enumerated sets. |
| 154 | | b_global_deferred_set(GS) :- |
| 155 | ? | b_global_set(GS), |
| 156 | ? | \+ is_b_global_constant(GS,_Nr,_Cst). % note : some deferred sets are translated into partially_deferred_set |
| 157 | | |
| 158 | | % either an enumerated set with unused constants or a deferred set where some constants were lifted into the deferred set |
| 159 | | b_partially_deferred_set(GS) :- |
| 160 | | b_global_set(GS), |
| 161 | | (is_b_global_constant(GS,_Nr,_Cst) -> true), % GS is in principle enumerated |
| 162 | | (is_unused_b_global_constant(GS,_X) -> true). |
| 163 | | |
| 164 | | |
| 165 | | b_global_set_with_potential_symmetry(GS) :- |
| 166 | ? | b_global_set(GS), |
| 167 | ? | (b_global_deferred_set_with_card_gt1(GS) -> true |
| 168 | ? | ; (is_unused_b_global_constant(GS,X), |
| 169 | ? | is_unused_b_global_constant(GS,Y), |
| 170 | | X\=Y -> true % At least two unused constants exist |
| 171 | | ; fail)). |
| 172 | | |
| 173 | | b_global_deferred_set_with_card_gt1(GS) :- |
| 174 | ? | b_global_deferred_set(GS), |
| 175 | | extract_setsize_from_machine_cache(GS,Low,Up), |
| 176 | | inf_greater(Up,Low). |
| 177 | | |
| 178 | | inf_greater(X,Y) :- (X=inf -> integer(Y) ; X>Y). |
| 179 | | inf_add(X,Y,XY) :- (X=inf -> XY=inf ; Y=inf -> XY=inf ; XY is X+Y). |
| 180 | | |
| 181 | | :- volatile b_exists_global_set_with_potential_symmetry/0. |
| 182 | | :- dynamic b_exists_global_set_with_potential_symmetry/0. |
| 183 | | :- dynamic precompilation_phase/1. |
| 184 | | |
| 185 | | % ------------------------------------------- |
| 186 | | |
| 187 | | % Phase 1 of precompilation: |
| 188 | | b_check_and_precompile_enumerated_sets :- |
| 189 | | b_reset_global_set_type_definitions, |
| 190 | | retractall(b_exists_global_set_with_potential_symmetry), |
| 191 | | retractall(precompilation_phase(_)), |
| 192 | | assertz(precompilation_phase(1)), |
| 193 | | debug_println(9,'Preprocessing enumerated sets: '), |
| 194 | | debug_print(9,'% '), |
| 195 | ? | b_get_named_machine_set(Set,_Els), % treat enumerated sets first; their cardinality is obvious |
| 196 | | precompile_global_set(Set), % will only require b_get_named_machine_set/2 from bmachine |
| 197 | | fail. |
| 198 | | b_check_and_precompile_enumerated_sets :- |
| 199 | | retractall(precompilation_phase(_)), |
| 200 | | assertz(precompilation_phase(2)), |
| 201 | | debug_nl(9). |
| 202 | | |
| 203 | | % Phase 2 of precompilation: |
| 204 | | b_check_and_precompile_deferred_sets :- |
| 205 | | (deferred_sets_precompiled |
| 206 | | -> add_internal_error('Deferred sets already precompiled',b_check_and_precompile_deferred_sets) |
| 207 | | ; enumerated_sets_precompiled -> true |
| 208 | | ; add_internal_error('Enumerated sets not yet precompiled',b_check_and_precompile_deferred_sets)), |
| 209 | | retractall(precompilation_phase(_)), |
| 210 | | assertz(precompilation_phase(3)), |
| 211 | ? | check_enumerated_set_scope(_), |
| 212 | | fail. |
| 213 | | b_check_and_precompile_deferred_sets :- |
| 214 | | debug_println(9,'Inferring cardinality and disjoint elements of deferred sets: '), |
| 215 | | debug_print(9,'% '), |
| 216 | ? | b_get_machine_set(Set), |
| 217 | | \+ b_get_named_machine_set(Set,_), % not enumerated |
| 218 | | precompile_global_set(Set), |
| 219 | | fail. |
| 220 | | b_check_and_precompile_deferred_sets :- |
| 221 | | retractall(precompilation_phase(_)), |
| 222 | | assertz(precompilation_phase(4)), |
| 223 | | debug_nl(9). |
| 224 | | |
| 225 | | enumerated_sets_precompiled :- precompilation_phase(X), X >= 2. |
| 226 | | deferred_sets_precompiled :- precompilation_phase(X), X >= 4. |
| 227 | | |
| 228 | | precompile_global_set(Set) :- |
| 229 | | add_new_global_set(Set), |
| 230 | ? | (b_extract_fd_type(Set,LowBnd,UpBnd) /* also computes & caches the size of the SET */ |
| 231 | | -> debug_print(9,' '),debug_print(9,Set), |
| 232 | | debug_print(9,'=='),debug_print(9,LowBnd),debug_print(9,'..'),debug_print(9,UpBnd) |
| 233 | | ; add_internal_error('No b_extract_fd_type/3 solution for global set: ',b_extract_fd_type(Set,_,_)) |
| 234 | | ),debug_print(9,' '). |
| 235 | | |
| 236 | | % check if there are any conflicts between scope annotations and enumerated set |
| 237 | | check_enumerated_set_scope(GlobalSetName) :- |
| 238 | ? | enumerated_set(GlobalSetName), |
| 239 | | extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound), |
| 240 | | (get_user_defined_scope(GlobalSetName,DL,DU,Span), |
| 241 | | DU-DL =\= UpBound-LowBound |
| 242 | | -> UserSize is 1+DU-DL, |
| 243 | | EnumSize is 1+UpBound-LowBound, |
| 244 | | ajoin(['Conflict between cardinality of scope_',GlobalSetName, |
| 245 | | ' DEFINITION (',UserSize,') and enumeration (',EnumSize,') of SET:'],Msg), |
| 246 | | add_error(extract_setsize_from_machine,Msg,GlobalSetName,Span) |
| 247 | | ; true |
| 248 | | ). |
| 249 | | |
| 250 | | :- use_module(library(avl),[avl_fetch/2]). |
| 251 | | % Phase 3 of precompilation: |
| 252 | | % This can be done after bmachine pre-compile is finished |
| 253 | | b_check_and_precompile_global_set_symmetry :- |
| 254 | | (retract(precompilation_phase(4)) -> true |
| 255 | | ; add_internal_error('Deferred sets not yet precompiled',b_check_and_precompile_global_set_symmetry)), |
| 256 | | assertz(precompilation_phase(5)), |
| 257 | | find_all_used_enumerated_elements(UsedEnumsAVL), |
| 258 | ? | b_extract_fd_type(GS,_Low,_Up), |
| 259 | ? | (is_b_global_constant(GS,_Nr,_Cst) -> true), % GS is in principle enumerated |
| 260 | | (user_forced_symmetry(GS) |
| 261 | | -> print('FORCING SYMMETRY: '), print(GS), nl, |
| 262 | | fail % not asserting used_b_global_constant; every constant becomes "virtually" unused |
| 263 | | ; true |
| 264 | | ), |
| 265 | ? | is_b_global_constant_hash(GS,X,Name), |
| 266 | | avl_fetch(Name,UsedEnumsAVL), |
| 267 | | assertz(used_b_global_constant(GS,X,deferred)), % by storing that it is not used, we enable symmetry reduction |
| 268 | | debug_println(9,used_b_global_constant(GS:Name)), |
| 269 | | fail. |
| 270 | | b_check_and_precompile_global_set_symmetry :- %print(precomp_gs_3), debug:nl_time, |
| 271 | ? | (b_global_set_with_potential_symmetry(_) |
| 272 | | -> assertz(b_exists_global_set_with_potential_symmetry), |
| 273 | | debug_println(9,'% Symmetry is potentially useful for this machine') |
| 274 | | ; true), |
| 275 | | debug_nl(9), |
| 276 | | /* clean up: */ |
| 277 | | reset_global_set_user_defined_scope. |
| 278 | | |
| 279 | | % ------------------------------------------- |
| 280 | | |
| 281 | | % peform MACE style static symmetry reduction for those global constants |
| 282 | | % that have not already been fixed |
| 283 | | % 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 |
| 284 | | |
| 285 | | static_symmetry_reduction_for_global_sets(_ConstantsState) :- |
| 286 | | get_preference(use_solver_on_load,kodkod),!. % no idea which numbering Kodkod might return/expect ?! |
| 287 | | static_symmetry_reduction_for_global_sets(_ConstantsState) :- |
| 288 | | get_preference(use_static_symmetry_detection,false),!. |
| 289 | | static_symmetry_reduction_for_global_sets(ConstantsState) :- |
| 290 | | findall(gs_info(GS,FirstAvailableNewIdx,Low,Up,Other), |
| 291 | | static_symmetry_reduction_possible(GS,FirstAvailableNewIdx,Low,Up,Other),L), |
| 292 | | maplist(perform_static_symmetry_reduction(ConstantsState),L). |
| 293 | | |
| 294 | | :- use_module(static_symmetry_reduction,[static_symmetry_reduction_possible/5, perform_ssr/8]). |
| 295 | | perform_static_symmetry_reduction(ConstantsState,gs_info(GS,First,Low,Up,Other)) :- |
| 296 | | if(perform_ssr(Other,[],First,First,GS,Low,Up,ConstantsState),true, |
| 297 | | add_internal_error('Call failed: ',perform_ssr(Other,[],First,First,GS,Low,Up,ConstantsState))). |
| 298 | | |
| 299 | | |
| 300 | | |
| 301 | | % -------------------- |
| 302 | | |
| 303 | | |
| 304 | | :- use_module(avl_tools,[ord_domain_list_to_avl/2]). |
| 305 | | find_all_used_enumerated_elements(ElementsAVL) :- |
| 306 | | b_get_all_used_identifiers(Identifiers), |
| 307 | | b_get_machine_variables(TVariables),get_texpr_ids(TVariables,Variables), |
| 308 | | % We assume that b_get_all_used_identifiers/1 is a proper ordset. (sorted with sort/2) |
| 309 | | % As an optimisation, we remove the variables, they cannot be enumerated elements. |
| 310 | | list_to_ord_set(Variables,OVariables), |
| 311 | | ord_subtract(Identifiers,OVariables,Elements), |
| 312 | | ord_domain_list_to_avl(Elements,ElementsAVL),!. |
| 313 | | find_all_used_enumerated_elements(_Elements) :- |
| 314 | | add_error_and_fail(b_global_sets, 'find_all_used_enumerated_elements failed'). |
| 315 | | |
| 316 | | |
| 317 | | reset_global_set_user_defined_scope :- |
| 318 | | retract(global_set_user_defined_scope(GS,_Scope)), |
| 319 | | (is_b_precompiled_globalset(GS) |
| 320 | | -> true |
| 321 | | ; add_error(b_global_sets,'Trying to set scope of unknown SET: ',GS) |
| 322 | | ),fail. |
| 323 | | reset_global_set_user_defined_scope. |
| 324 | | |
| 325 | | % Return those constants which are implicitly introduced by ProB, but not really |
| 326 | | % part of the model. These are the elements of a deferred set. |
| 327 | | b_get_prob_deferred_set_elements(TIds,AllOrVisible) :- |
| 328 | | findall( TId, |
| 329 | | ( prob_deferred_set_element(GS,_Nr,Id,AllOrVisible), |
| 330 | | create_texpr(identifier(Id),global(GS),[],TId)), |
| 331 | | TIds). |
| 332 | | |
| 333 | | |
| 334 | | |
| 335 | | :- use_module(bsyntaxtree,[transform_bexpr_with_scoping/3]). |
| 336 | | % inline probids (prob deferred set ids) as values into a predicate or expression |
| 337 | | inline_prob_deferred_set_elements_into_bexpr(Pred,CompiledPred) :- |
| 338 | | add_prob_deferred_set_elements_to_store([], State, visible), % visible: only those Ids which do not clash with variables, constants, ... are added |
| 339 | | State \= [], !, |
| 340 | | sort(State,S), |
| 341 | | debug_println(19,compiling_probids_into_bexpr(S)), |
| 342 | | transform_bexpr_with_scoping(b_global_sets:inline_state(S),Pred,CompiledPred). |
| 343 | | inline_prob_deferred_set_elements_into_bexpr(Pred,Pred). |
| 344 | | |
| 345 | | :- use_module(tools_lists,[ord_member_nonvar_chk/2]). |
| 346 | | :- use_module(library(ordsets),[ord_nonmember/2]). |
| 347 | | % difference with compile from b_compiler: no need to specify parameters, no errors if identifier not found |
| 348 | | inline_state(State,b(identifier(ID),Type,I),b(value(Val),Type,I),LocalIds) :- |
| 349 | | ord_member_nonvar_chk(bind(ID,Val),State), % the ID appears in the binding list |
| 350 | | ord_nonmember(ID,LocalIds). % The ID is not overriden by a locally quantified variable |
| 351 | | |
| 352 | | add_prob_deferred_set_elements_to_store(OldStore,NewStore,AllOrVisible) :- % add prob_ids |
| 353 | | is_list(OldStore),!, |
| 354 | | %print(add_prob_deferred_set_elements_to_store(OldStore)),nl, |
| 355 | | findall(bind(Id,fd(Nr,GS)),(prob_deferred_set_element(GS,Nr,Id,AllOrVisible), |
| 356 | | \+ member(bind(Id,_),OldStore)), |
| 357 | | NewStore, OldStore). |
| 358 | | add_prob_deferred_set_elements_to_store(OldStore,NewStore,_) :- |
| 359 | | add_internal_error('Cannot add deferred set elements to this store: ',OldStore), |
| 360 | | NewStore=OldStore. |
| 361 | | |
| 362 | | % virtual deferred set elements generated by ProB |
| 363 | | prob_deferred_set_element(GlobalSet,Elem,Id,AllOrVisible) :- |
| 364 | | b_global_set(GlobalSet), |
| 365 | | atom_codes(GlobalSet,GlobalSetCodes),append(GlobalSetCodes,ECodes,NameCodes), |
| 366 | | b_get_fd_type_bounds(GlobalSet,Low,Up), |
| 367 | | (Up=inf -> UpLimited=999, |
| 368 | | debug_format(19,'Limiting ProB IDs for deferred set ~w to ~w..~w elements~n',[GlobalSet,Low,UpLimited]) |
| 369 | | ; Up>999 -> UpLimited=999, % TODO: provide preference/option ? |
| 370 | | debug_format(19,'Limiting ProB IDs for deferred set ~w to ~w..~w elements~n',[GlobalSet,Low,UpLimited]) |
| 371 | | ; UpLimited=Up), |
| 372 | | between(Low,UpLimited,Elem), |
| 373 | | (AllOrVisible = all -> true |
| 374 | | ; % only visible ones |
| 375 | | \+ is_b_global_constant_hash(GlobalSet,Elem,_) % the identifier is not used somewhere else |
| 376 | | ), |
| 377 | | number_codes(Elem,ECodes), |
| 378 | | atom_codes(Id,NameCodes), |
| 379 | | \+ b_global_set(Id), % not used as another SET name |
| 380 | | \+ lookup_global_constant(Id,_). % not used as another SET element |
| 381 | | |
| 382 | | |
| 383 | | user_forced_symmetry(GS) :- % check if the user defined FORCE_SYMMETRY_GS == TRUE |
| 384 | | string_concatenate('FORCE_SYMMETRY_',GS,DefName), |
| 385 | | b_get_typed_definition(DefName,[],F), get_texpr_expr(F,boolean_true). |
| 386 | | |
| 387 | | |
| 388 | | %is_global_set_of_cardinality_two(Type,LowBnd,UpBnd) :- |
| 389 | | % b_get_fd_type_bounds(Type,LowBnd,UpBnd), |
| 390 | | % LowBnd+1 =:= UpBnd. |
| 391 | | |
| 392 | | :- volatile is_global_set_of_cardinality_one/2. |
| 393 | | :- dynamic is_global_set_of_cardinality_one/2. |
| 394 | | % should be called when unloading a machine, before type-checking etc... |
| 395 | | % TO DO: use :- use_module(eventhandling,[register_event_listener/3]). |
| 396 | | b_clear_global_set_type_definitions :- % nl,print(clearing_gs),nl, |
| 397 | | retractall(b_supplementary_global_set(_)), |
| 398 | | retractall(b_replaced_global_set(_,_)), |
| 399 | | b_reset_global_set_type_definitions, |
| 400 | | retractall(global_set_user_defined_scope(_,_)). |
| 401 | | |
| 402 | | b_reset_global_set_type_definitions :- %nl,print(reset_gs),nl, |
| 403 | | % print_message('resetting global sets'), |
| 404 | | retractall(b_precompiled_global_set(_)), |
| 405 | | retractall(enumerated_set(_)), |
| 406 | | retractall(fixed_deferred_set_size(_,_)), |
| 407 | | retractall(extract_setsize_from_machine_cache(_,_,_)), |
| 408 | | retractall(find_minimum_cardinality_cache(_,_)), |
| 409 | | retractall(is_global_set_of_cardinality_one(_,_)), |
| 410 | | retractall(b_global_constant(_,_,_)), |
| 411 | | retractall(b_global_constant_hash(_,_,_,_)), |
| 412 | | retractall(lookup_global_constant(_,_)), |
| 413 | | retractall(used_b_global_constant(_,_,_)), |
| 414 | | retractall(inferred_minimum_global_set_cardinality(_,_)), |
| 415 | | retractall(inferred_maximum_global_set_cardinality(_,_)). |
| 416 | | |
| 417 | | |
| 418 | | add_new_global_set(Set) :- |
| 419 | | (b_precompiled_global_set(Set) |
| 420 | | -> add_internal_error('Global set already exists: ',add_new_global_set(Set)) |
| 421 | | ; b_integer_or_real_or_string_set(Set) |
| 422 | | % should only occur in Event-B mode, or possibly in Z, TLA; in Atelier-B these are reserved keywords |
| 423 | | % this can cause problems as we currently create symbolic set values global_set('STRING'), ... |
| 424 | | -> add_warning(add_new_global_set,'Global set name can cause internal name clashes: ',Set), |
| 425 | | assertz(b_precompiled_global_set(Set)) |
| 426 | | ; assertz(b_precompiled_global_set(Set))). |
| 427 | | |
| 428 | | |
| 429 | | :- dynamic b_supplementary_global_set/1, b_replaced_global_set/2. |
| 430 | | b_supplementary_global_set(GS) :- b_supplementary_global_set(GS). |
| 431 | | |
| 432 | | % these should be called before we precompile the global set definitions |
| 433 | | generate_fresh_supplementary_global_set(FRESHID) :- |
| 434 | | gensym('__DEFERREDSET__',FRESHID), |
| 435 | | debug_println(10,generate_fresh_supplementary_global_set(FRESHID)), |
| 436 | | assertz(b_supplementary_global_set(FRESHID)). |
| 437 | | |
| 438 | | % called by record construction, when a global deferred set gets replaced by something else |
| 439 | | % we register it here for safety and better error messages |
| 440 | | % in some contexts (like freetype constructors/destructors) the old type may accidentally get used; but we should remove all references to old type |
| 441 | | register_replaced_global_set(ID,_) :- |
| 442 | | b_global_set(ID),!, |
| 443 | | add_warning(b_global_sets,'Global set already exists: ',ID). |
| 444 | | register_replaced_global_set(ID,_) :- |
| 445 | | b_replaced_global_set(ID,_),!, |
| 446 | | add_warning(b_global_sets,'Global set already registered as replaced: ',ID). |
| 447 | | register_replaced_global_set(ID,NewTypeExpr) :- |
| 448 | | assertz(b_replaced_global_set(ID,NewTypeExpr)). |
| 449 | | |
| 450 | | /* --------------------------------------------------------- */ |
| 451 | | /* Extracting Finite Domain type information from the B machine */ |
| 452 | | /* --------------------------------------------------------- */ |
| 453 | | |
| 454 | | |
| 455 | | |
| 456 | | /* below treats annotations in the form: |
| 457 | | DEFINITIONS |
| 458 | | scope_Name == 1..3; |
| 459 | | scope_Code == 4..8 |
| 460 | | which inform us about which finidte domain ranges we should |
| 461 | | give to global sets defined in SETS |
| 462 | | */ |
| 463 | | |
| 464 | | :- use_module(tools_printing,[print_error/1, format_error_with_nl/2]). |
| 465 | | :- dynamic extract_setsize_from_machine_cache/3. |
| 466 | | extract_setsize_from_machine_cache(_,_,_) :- |
| 467 | | print_error('*** extract_setsize_from_machine not precompiled'),fail. |
| 468 | | |
| 469 | | try_extract_setsize_from_machine(GlobalSetName,_LowBound,_UpBound) :- |
| 470 | | start_extracting_setsize(GlobalSetName),!,fail. % cyclic dependency; abort computation |
| 471 | | try_extract_setsize_from_machine(GlobalSetName,LowBound,UpBound) :- |
| 472 | | extract_setsize_from_machine(GlobalSetName,LowBound,UpBound). |
| 473 | | |
| 474 | | % Determine if GlobalSetName is enumerated or deferred and if we can infer cardinality (bounds) |
| 475 | | extract_setsize_from_machine(GlobalSetName,LowBound,UpBound) :- |
| 476 | | extract_setsize_from_machine_cache(GlobalSetName,L,U),!, |
| 477 | | LowBound=L,UpBound=U. |
| 478 | | extract_setsize_from_machine(GlobalSetName,LowBound,UpBound) :- |
| 479 | | start_extracting_setsize_from_machine(GlobalSetName), |
| 480 | | b_get_named_machine_set(GlobalSetName,ListOfConstants), % find explicitly declared ENUMERATED SETS |
| 481 | | !, |
| 482 | | assert_enumerated_set(GlobalSetName,ListOfConstants,LowBound,UpBound). % will also assert_extract_setsize_from_machine_cache |
| 483 | | extract_setsize_from_machine(GlobalSetName,L,U) :- |
| 484 | | b_supplementary_global_set(GlobalSetName),!, % deferred set that was added for untyped ID,... |
| 485 | | default_deferred_set_bounds(LowBound,UpBound), |
| 486 | | assert_extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound), |
| 487 | | (LowBound,UpBound)=(L,U). |
| 488 | | extract_setsize_from_machine(GlobalSetName,L,U) :- |
| 489 | | /* we have a DEFERRED SET */ |
| 490 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,LowBound,UpBound), |
| 491 | | (LowBound=UpBound -> assertz(is_global_set_of_cardinality_one(GlobalSetName,LowBound)) ; true), |
| 492 | | assert_extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound), |
| 493 | | % determine if some of the elements are ENUMERATED: |
| 494 | | (b_get_disjoint_constants_of_type(GlobalSetName, DisjointConstants,_) |
| 495 | | % DISABLE for Disprover ?? what if selected hyps does not contain this |
| 496 | | -> /* 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 */ |
| 497 | | debug_format(19,'Adding enumerated disjoint constants ~w : ~w~n~n',[GlobalSetName,DisjointConstants]), |
| 498 | | add_named_constants_to_global_set(GlobalSetName,LowBound,DisjointConstants) |
| 499 | | ; true |
| 500 | | ), |
| 501 | | debug_println(9,setsize(GlobalSetName,LowBound,UpBound)), |
| 502 | | (LowBound,UpBound)=(L,U). |
| 503 | | |
| 504 | | |
| 505 | | /* for Deferred SETS : */ |
| 506 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,L,U) :- |
| 507 | | b_extract_values_clause_assignment(GlobalSetName,_Type,TVal), % VALUES clause |
| 508 | | (get_interval(TVal,Low,Up) -> true |
| 509 | | ; add_error(b_global_sets,'VALUES clause must set deferred set to an interval: ',GlobalSetName,TVal),fail), |
| 510 | | (evaluable_integer_expression(Low,[],LowBound) -> true |
| 511 | | ; add_error(b_global_sets,'Cannot extract lower bound from VALUES interval for: ',GlobalSetName,Low),fail), |
| 512 | | (evaluable_integer_expression(Up,[],UpBound) -> true |
| 513 | | ; add_error(b_global_sets,'Cannot extract upper bound from VALUES interval for: ',GlobalSetName,Up),fail), |
| 514 | | !, |
| 515 | | check_compatible_with_user_scope(GlobalSetName,UpBound,LowBound), |
| 516 | | LowBound=L,UpBound=U. |
| 517 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,L,U) :- |
| 518 | ? | b_get_properties_from_machine(Properties), member_in_conjunction(C,Properties), |
| 519 | | (is_equality_card_global_set(C,GlobalSetName,Properties,Card) |
| 520 | | % check if the PROPERTIES contain an expression of the form card(GS) = Nr |
| 521 | | -> true |
| 522 | | ; is_infinite_global_set_pred(C,GlobalSetName) |
| 523 | | % look for predicates which stipulate that the set is infinite |
| 524 | | -> Card=inf |
| 525 | | ), |
| 526 | | !, |
| 527 | | assertz(fixed_deferred_set_size(GlobalSetName,Card)), |
| 528 | | LowBound=1, UpBound = Card, |
| 529 | | check_compatible_with_user_scope(GlobalSetName,UpBound,LowBound), |
| 530 | | LowBound=L,UpBound=U. |
| 531 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,L,U) :- /* check if there is a scope_ DEFINITION */ |
| 532 | | get_user_defined_scope(GlobalSetName,LowBound,UpBound,_),!, |
| 533 | | LowBound=L,UpBound=U. |
| 534 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,LowBound,UpBound) :- |
| 535 | | get_preference(globalsets_fdrange,DefaultUpperBound), |
| 536 | | find_minimum_cardinality(GlobalSetName,MinCard), |
| 537 | | assertz(inferred_minimum_global_set_cardinality(GlobalSetName,MinCard)), |
| 538 | | !, |
| 539 | | LowBound = 1, |
| 540 | | (find_maximum_cardinality(GlobalSetName,MaxCard) |
| 541 | | -> (MaxCard=MinCard -> assertz(fixed_deferred_set_size(GlobalSetName,MinCard)), |
| 542 | | debug_println(9,fixed_deferred_set_size(GlobalSetName,MinCard)), |
| 543 | | UpBound = MinCard |
| 544 | | ; DefaultUpperBound>MaxCard -> |
| 545 | | debug_println(9,reducing_deferred_set_size(GlobalSetName,MaxCard)), |
| 546 | | UpBound=MaxCard |
| 547 | | ; DefaultUpperBound<MinCard -> |
| 548 | | debug_println(9,inferred_minimum_global_set_cardinality(GlobalSetName,MinCard)), |
| 549 | | UpBound=MinCard |
| 550 | | ; UpBound is MinCard |
| 551 | | ) |
| 552 | | ; MinCard>DefaultUpperBound -> UpBound=MinCard |
| 553 | | ; UpBound=DefaultUpperBound), |
| 554 | | debug_println(4,inferred(GlobalSetName,UpBound)). |
| 555 | | extract_DEFERRED_setsize_from_machine(GlobalSetName,LowBound,UpBound) :- |
| 556 | | % No Minimum cardinality was inferred |
| 557 | | LowBound=1, get_preference(globalsets_fdrange,DefaultUpperBound), |
| 558 | | find_maximum_cardinality(GlobalSetName,MaxCard), |
| 559 | | !, |
| 560 | | (MaxCard=1 -> UpBound=1, assertz(fixed_deferred_set_size(GlobalSetName,1)) |
| 561 | | ; inf_greater(DefaultUpperBound,MaxCard) -> |
| 562 | | debug_println(9,reducing_deferred_set_size(GlobalSetName,MaxCard)), |
| 563 | | UpBound=MaxCard |
| 564 | | % does not have the case: DefaultUpperBound<MinCard -> UpBound=MinCard |
| 565 | | ; UpBound=DefaultUpperBound). |
| 566 | | extract_DEFERRED_setsize_from_machine(_GlobalSetName,LowBound,UpBound) :- |
| 567 | | % No Minimum cardinality was inferred |
| 568 | | default_deferred_set_bounds(LowBound,UpBound). |
| 569 | | |
| 570 | | default_deferred_set_bounds(1,UpBound) :- get_preference(globalsets_fdrange,UpBound). |
| 571 | | |
| 572 | | check_compatible_with_user_scope(GlobalSetName,UpBound,LowBound) :- |
| 573 | | (get_user_defined_scope(GlobalSetName,DL,DU,Span), |
| 574 | | DU-DL =\= UpBound-LowBound |
| 575 | | -> add_error(extract_DEFERRED_setsize_from_machine,'Conflict between scope_ Definition and PROPERTIES:',GlobalSetName,Span) |
| 576 | | ; true |
| 577 | | ). |
| 578 | | |
| 579 | | |
| 580 | | find_maximum_cardinality(GlobalSetName,MaxCard) :- |
| 581 | | find_maximum_cardinality1(GlobalSetName,MaxCard), |
| 582 | | assertz(inferred_maximum_global_set_cardinality(GlobalSetName,MaxCard)). |
| 583 | | |
| 584 | | find_maximum_cardinality1(GlobalSetName,MaxCard) :- |
| 585 | | b_get_machine_constants(Csts), |
| 586 | | b_get_properties_from_machine(Properties), |
| 587 | | findall(MC2,find_maximum_cardinality2(Csts,Properties,GlobalSetName,MC2),List), |
| 588 | | min_member(MaxCard,List). |
| 589 | | find_maximum_cardinality2(_Csts,Properties,GlobalSetName,MaxCard) :- |
| 590 | | get_card_upper_bound(Properties,GlobalSetName,MaxCard). |
| 591 | | find_maximum_cardinality2(_Csts,Properties,GlobalSetName,MaxCard) :- |
| 592 | ? | get_equality(Properties,GlobalSetName,EXPR,RestProp), % GlobalSetName = EXPR |
| 593 | | maximum_cardinality_of_expression(EXPR,RestProp,MaxCard). |
| 594 | | find_maximum_cardinality2(_Csts,Properties,GlobalSetName,MaxCard) :- |
| 595 | ? | member_in_conjunction(C,Properties), |
| 596 | | get_texpr_expr(C,partition(Set,DisjSets)), % partition(GlobalSetName, DisjSets) |
| 597 | | global_set_identifier(Set,GlobalSetName), |
| 598 | | max_card_of_partition_list(DisjSets,Properties,0,MaxCard). |
| 599 | | |
| 600 | | |
| 601 | | get_equality(Properties,ID,R,RestProp) :- |
| 602 | ? | select_member_in_conjunction(C,Properties,RestProp), |
| 603 | | get_texpr_expr(C,equal(LHS,RHS)), |
| 604 | | ( get_texpr_expr(LHS,identifier(ID)), R=RHS |
| 605 | | ; get_texpr_expr(RHS,identifier(ID)), R=LHS ). |
| 606 | | |
| 607 | | % find card(ID) <= MaxCard |
| 608 | | get_card_upper_bound(Properties,ID,MaxCard) :- |
| 609 | | LHS = b(card(TID),_,_), |
| 610 | | get_texpr_expr(TID,identifier(ID)), |
| 611 | ? | select_member_in_conjunction(C,Properties,RestProp), |
| 612 | | ( get_texpr_expr(C,less_equal(LHS,RHS)), Strict=false ; |
| 613 | | get_texpr_expr(C,greater_equal(RHS,LHS)), Strict=false ; |
| 614 | | get_texpr_expr(C,less(LHS,RHS)), Strict=true ; |
| 615 | | get_texpr_expr(C,greater(RHS,LHS)), Strict=true |
| 616 | | ), |
| 617 | | evaluable_integer_expression(RHS,RestProp,R), |
| 618 | | (Strict=true -> MaxCard is R-1 ; MaxCard = R). |
| 619 | | |
| 620 | | maximum_cardinality_of_expression(b(E,_,_),Props,MC) :- maximum_cardinality_of_expression2(E,Props,MC). |
| 621 | | maximum_cardinality_of_expression2(set_extension(SetExtElements),_,MaxCard) :- |
| 622 | | length(SetExtElements,MaxCard). |
| 623 | | % we assume that all elements in List can be different |
| 624 | | maximum_cardinality_of_expression2(union(A,B),Props,MaxCard) :- |
| 625 | | maximum_cardinality_of_expression(A,Props,MA), |
| 626 | | maximum_cardinality_of_expression(B,Props,MB), MaxCard is MA+MB. |
| 627 | | maximum_cardinality_of_expression2(intersection(A,B),Props,MaxCard) :- |
| 628 | | maximum_cardinality_of_expression(A,Props,MA), |
| 629 | | maximum_cardinality_of_expression(B,Props,MB), MaxCard is min(MA,MB). |
| 630 | | maximum_cardinality_of_expression2(set_subtraction(A,_),Props,MaxCard) :- |
| 631 | | maximum_cardinality_of_expression(A,Props,MaxCard). |
| 632 | | maximum_cardinality_of_expression2(cartesian_product(A,B),Props,MaxCard) :- |
| 633 | | maximum_cardinality_of_expression(A,Props,MA), |
| 634 | | maximum_cardinality_of_expression(B,Props,MB), MaxCard is MA*MB. |
| 635 | | maximum_cardinality_of_expression2(identifier(ID),Props,MaxCard) :- % tested in testcase 1917 |
| 636 | | maximum_cardinality_of_identifier(ID,Props,MaxCard). |
| 637 | | maximum_cardinality_of_expression2(empty_set,_,0). |
| 638 | | % TO DO: generalized union... |
| 639 | | %maximum_cardinality_of_expression2(Ex,_) :- nl, print(uncov_max_partition_card(Ex)),nl,nl,fail. |
| 640 | | % TO DO: other cases |
| 641 | | |
| 642 | | maximum_cardinality_of_identifier(ID,Properties,MaxCard) :- |
| 643 | | TID = b(identifier(ID),_,_), |
| 644 | ? | member_in_conjunction(EqCardExpr,Properties), % look for card(ID) = MaxCard |
| 645 | | is_equality_card_expression(EqCardExpr,Properties,TID,MaxCard), % this is actually an exact card |
| 646 | | !. % TODO: also check for card(ID) <= Bound |
| 647 | | maximum_cardinality_of_identifier(ID,Properties,MaxCard) :- |
| 648 | | get_equality(Properties,ID,EXPR,RestProp), % ID = EXPR, |
| 649 | | % remove equality to avoid loops, TO DO: try several equalities? |
| 650 | | maximum_cardinality_of_expression(EXPR,RestProp,MaxCard). |
| 651 | | maximum_cardinality_of_identifier(ID,Properties,MaxCard) :- |
| 652 | | get_texpr_id(Set,ID), |
| 653 | | get_texpr_expr(C,partition(Set,DisjSets)), % partition(ID, DisjSets) |
| 654 | | select_member_in_conjunction(C,Properties,RestProp), % remove partition to avoid loops |
| 655 | | max_card_of_partition_list(DisjSets,RestProp,0,MaxCard). |
| 656 | | |
| 657 | | % determine maximum cardinality of partition RHS-List (partition(Set,RHS-List)) |
| 658 | | max_card_of_partition_list([],_,Acc,Acc). |
| 659 | | max_card_of_partition_list([TPartSet|T],Properties,Acc,Res) :- |
| 660 | | maximum_cardinality_of_expression(TPartSet,Properties,Max),!, |
| 661 | | NAcc is Acc+Max, |
| 662 | | max_card_of_partition_list(T,Properties,NAcc,Res). |
| 663 | | |
| 664 | | |
| 665 | | :- dynamic find_minimum_cardinality_cache/2. |
| 666 | | find_minimum_cardinality(GS,MC) :- |
| 667 | | find_minimum_cardinality_cache(GS,Nr),!, %print(min_card_cache(GS,Nr)),nl, |
| 668 | | % avoid loops; e.g., if we have N1 >->> N2 and N2 >->> N1 |
| 669 | | number(Nr), |
| 670 | | MC=Nr. |
| 671 | | find_minimum_cardinality(GlobalSetName,Res) :- % print(find_min_card(GlobalSetName)),nl, |
| 672 | | /* try to find out from the Properties whether there is an implied minimum cardinality */ |
| 673 | | b_get_machine_constants(Csts), |
| 674 | | b_get_properties_from_machine(Properties), |
| 675 | | assertz(find_minimum_cardinality_cache(GlobalSetName,unknown)), |
| 676 | | findall(MinCard2,find_minimum_cardinality2(Csts,Properties,GlobalSetName,MinCard2),List), |
| 677 | | debug_println(9,mincard_list(GlobalSetName,List)), |
| 678 | | max_member(MinCard,List), % we do not allow empty global sets anymore, allow_empty_global_sets is obsolete |
| 679 | | inf_greater(MinCard,0), |
| 680 | | retract(find_minimum_cardinality_cache(GlobalSetName,_)), |
| 681 | | assertz(find_minimum_cardinality_cache(GlobalSetName,MinCard)), |
| 682 | | Res=MinCard. |
| 683 | | |
| 684 | | find_minimum_cardinality2(_,Properties,GlobalSetName,MinCard) :- |
| 685 | ? | member_in_conjunction(C,Properties), |
| 686 | ? | find_minimum_cardinality3(C,Properties,GlobalSetName,MinCard). |
| 687 | | find_minimum_cardinality2(_Constants,_Properties,GlobalSetName,MinCard) :- |
| 688 | | %print(trying_find_min_card(GlobalSetName,Constants)),nl, |
| 689 | | b_get_disjoint_constants_of_type(GlobalSetName, DisjointConstants,_), |
| 690 | | length(DisjointConstants,MinCard), inf_greater(MinCard,1). |
| 691 | | |
| 692 | | |
| 693 | | :- use_module(partition_detection,[is_disjoint_pred/4]). |
| 694 | | |
| 695 | | find_minimum_cardinality3(C,Properties,GlobalSetName,MinCard) :- |
| 696 | | % check if the PROPERTIES contain an expression of the form card(GS) >= Nr or similar |
| 697 | | is_greaterequalthan_card_global_set(C,GlobalSetName,Properties,MinCard). |
| 698 | | find_minimum_cardinality3(C,Properties,GlobalSetName,MinCard) :- |
| 699 | | % find things like partition(GlobalSetName,S1,...,SN) |
| 700 | | get_texpr_expr(C,partition(Set,DisjSets)), |
| 701 | | global_set_identifier(Set,GlobalSetName), |
| 702 | | % print(partition(Set,DisjSets,GlobalSetName)),nl, |
| 703 | | find_min_card_of_disjoint_sets(DisjSets,Properties,MinCard). % ,print(min(MinCard)),nl. |
| 704 | | find_minimum_cardinality3(C,_Properties,GlobalSetName,MinCard) :- |
| 705 | | get_texpr_expr(C,member(_Something,SURJ)), |
| 706 | ? | is_surjection(SURJ,Set,OTHERSET), |
| 707 | | global_set_identifier(Set,GlobalSetName), |
| 708 | | \+ global_set_identifier(OTHERSET,GlobalSetName), % Surjection on itself; no use in narrowing down cardinality |
| 709 | | (minimum_cardinality(OTHERSET,MinCard) |
| 710 | | -> true |
| 711 | | ; print('*** could not compute mincard: '), print(OTHERSET),nl,fail), |
| 712 | | (MinCard=inf -> add_error(b_global_sets,'Set has to be of infinite cardinality: ',GlobalSetName),fail ; true). |
| 713 | | find_minimum_cardinality3(C,Properties,GlobalSetName,MinCard) :- |
| 714 | | is_disjoint_pred(C,set(global(GlobalSetName)),A,B), % A /\ B = {} with A<:GS and B<:GS |
| 715 | | minimum_cardinality_of_set(A,Properties,MinA), number(MinA), inf_greater(MinA,0), |
| 716 | | minimum_cardinality_of_set(B,Properties,MinB), number(MinB), inf_greater(MinB,0), |
| 717 | | inf_add(MinA,MinB,MinCard). |
| 718 | | % TO DO: store information and try to combine with other disjointedness infos |
| 719 | | |
| 720 | | % TO DO: detect that if f is total function from non_empty set to set X, then card(X)>0 |
| 721 | | |
| 722 | | % is a surjective function |
| 723 | | is_surjection(SURJ,FromSet,ToSet) :- get_texpr_expr(SURJ,total_surjection(FromSet,ToSet)). |
| 724 | | is_surjection(SURJ,FromSet,ToSet) :- get_texpr_expr(SURJ,partial_surjection(FromSet,ToSet)). |
| 725 | | is_surjection(SURJ,FromSet,ToSet) :- get_texpr_expr(SURJ,total_bijection(FromSet,ToSet)). % here we know the exact cardinality - TO DO: use this fact |
| 726 | | is_surjection(SURJ,FromSet,ToSet) :- get_texpr_expr(SURJ,partial_bijection(FromSet,ToSet)). |
| 727 | | is_surjection(SURJ,FromSet,ToSet) :- get_texpr_expr(SURJ,total_injection(ToSet,FromSet)). % inverse is surjective |
| 728 | | |
| 729 | | |
| 730 | | |
| 731 | | % compute the minmum cardinality of an expression |
| 732 | | minimum_cardinality(ID,MinCard) :- global_set_identifier(ID,GlobalSet),!, |
| 733 | ? | (b_extract_fd_type(GlobalSet,LowBnd,UpBnd) |
| 734 | | -> MinCard is 1+UpBnd-LowBnd |
| 735 | | ; print('*** Do not know card of : '), print(GlobalSet),nl, |
| 736 | | % TO DO: do full blown cardinality analysis of deferred sets |
| 737 | | fail). |
| 738 | | minimum_cardinality(b(EXPR,TYPE,_INFO),MinCard) :- |
| 739 | | minimum_cardinality2(EXPR,TYPE,MinCard). |
| 740 | | |
| 741 | | %minimum_cardinality2(A,T,R) :- print(mincard(A,T,R)),nl,fail. |
| 742 | | minimum_cardinality2(bool_set,_,2). |
| 743 | | minimum_cardinality2(cartesian_product(A,B),_,Res) :- minimum_cardinality(A,CA), |
| 744 | | minimum_cardinality(B,CB), kernel_objects:safe_mul(CA,CB,Res). |
| 745 | | minimum_cardinality2(interval(A,B),_,Res) :- |
| 746 | | b_get_properties_from_machine(Properties), |
| 747 | | evaluable_integer_expression(A,Properties,EA), |
| 748 | | evaluable_integer_expression(B,Properties,EB), |
| 749 | | (EB >= EA -> Res is EB+1-EA ; Res=0). |
| 750 | | % TO DO: enumerated sets, ... seq, relations, ... ? |
| 751 | | |
| 752 | | |
| 753 | | find_min_card_of_disjoint_sets([],_Properties,0). |
| 754 | | find_min_card_of_disjoint_sets([H|T],Properties,R) :- |
| 755 | | find_min_card_of_disjoint_sets(T,Properties,TN), |
| 756 | | (minimum_cardinality_of_set(H,Properties,MC) |
| 757 | | -> true %,print(min_card(MC,H)),nl |
| 758 | | ; add_internal_error('Call failed: ',minimum_cardinality_of_set(H,Properties,MC)), MC=1), |
| 759 | | R is TN+MC. |
| 760 | | |
| 761 | | |
| 762 | | minimum_cardinality_of_set(b(Expr,set(Type),_),Properties,MC) :- |
| 763 | | minimum_cardinality_of_set_aux(Expr,Type,Properties,MC). |
| 764 | | |
| 765 | | %minimum_cardinality_of_set_aux(P,Type,_,_MC) :- print(min_card(P,Type)),nl,fail. |
| 766 | | minimum_cardinality_of_set_aux(set_extension(List),GlobalSetName,Properties,MinCard) :- !, |
| 767 | | get_texpr_ids(List,AtomicIDList), |
| 768 | | find_inequal_global_set_identifiers(AtomicIDList,GlobalSetName,Properties,DisjointConstants), |
| 769 | | length(DisjointConstants,MinCard). % , print(disj_set_ext(MinCard,DisjointConstants)),nl,nl. |
| 770 | | minimum_cardinality_of_set_aux(identifier(CST),_Type,_Properties,MinCard) :- |
| 771 | | find_minimum_cardinality_cache(CST,Nr),!, |
| 772 | | number(Nr), |
| 773 | | MinCard=Nr. |
| 774 | | minimum_cardinality_of_set_aux(identifier(CST),Type,Properties,MinCard) :- |
| 775 | | Cst_Template = b(identifier(CST),set(Type),_), |
| 776 | | min_card_of_identifier(Cst_Template,CST,Type,Properties,MC), |
| 777 | | !, |
| 778 | | MinCard=MC, |
| 779 | | assertz(find_minimum_cardinality_cache(CST,MC)). % global sets and constants cannot have the same name |
| 780 | | % TO DO: add more cases ? sequence extension cannot appear |
| 781 | | minimum_cardinality_of_set_aux(_,_,_,0). |
| 782 | | |
| 783 | | % determine minimum cardinality of an identifier; usually a constant (cannot be another global set due to B typing). |
| 784 | | min_card_of_identifier(Cst_Template,_CST,_Type,Properties,MinCard) :- |
| 785 | ? | member_in_conjunction(EqCardExpr,Properties), % look for card(CstTemplate) = MinCard |
| 786 | | is_equality_card_expression(EqCardExpr,Properties,Cst_Template,MinCard), % this is actually an exact card |
| 787 | | !. |
| 788 | | min_card_of_identifier(_Cst_Template,CST,_Type,Properties,MinCard) :- |
| 789 | ? | member_in_conjunction(EqCardExpr,Properties), % look for card(CstTemplate) = MinCard |
| 790 | | is_greaterequalthan_card_global_set_id(EqCardExpr,CST,_GS,Properties,MinCard), |
| 791 | | MinCard > 0, % otherwise not helpful; maybe we can find a better bound below |
| 792 | | !. |
| 793 | | min_card_of_identifier(Cst_Template,_,_Type,Properties,MC) :- |
| 794 | | get_texpr_expr(PT,partition(Cst_Template,DisjSets)), |
| 795 | | member_in_conjunction(PT,Properties), |
| 796 | | find_min_card_of_disjoint_sets(DisjSets,Properties,MC),!. |
| 797 | | min_card_of_identifier(Cst_Template,_,Type,Properties,MinCard) :- |
| 798 | | % id1:CST ... idk:CST & all_different(id1,...,idk) => card(CST) >= k |
| 799 | | get_texpr_id(TID,ID), |
| 800 | | get_texpr_expr(EL,member(TID,Cst_Template)), |
| 801 | | findall(ID,member_in_conjunction(EL,Properties),AtomicIDList), |
| 802 | | % find all identifiers such that we have id : CST |
| 803 | | AtomicIDList \= [], |
| 804 | | !, % now detect which of these can be inferred to be disjoint |
| 805 | | find_inequal_global_set_identifiers(AtomicIDList,Type,Properties,DisjointConstants), |
| 806 | | length(DisjointConstants,MinCard). |
| 807 | | min_card_of_identifier(Cst_Template,_,_Type,Properties,MC) :- % x:CST => card(CST) >= 1 |
| 808 | | get_texpr_expr(EL,member(_,Cst_Template)), |
| 809 | | member_in_conjunction(EL,Properties), |
| 810 | | !, |
| 811 | | MC=1. |
| 812 | | min_card_of_identifier(Cst_Template,_,_Type,Properties,MC) :- % ID /= {} => card(ID) >= 1 |
| 813 | ? | member_in_conjunction(Pred,Properties), |
| 814 | | not_empty(Pred,Cst_Template), |
| 815 | | !, |
| 816 | | MC=1. |
| 817 | | |
| 818 | | not_empty(b(E,pred,_),A) :- |
| 819 | | not_empty_aux(E,A). |
| 820 | | not_empty_aux(not_equal(A,B),R) :- |
| 821 | | (definitely_empty_set(B) -> R=A ; definitely_empty_set(A),R=B). |
| 822 | | not_empty_aux(negation(b(equal(A,B),pred,_)),R) :- not_empty_aux(not_equal(A,B),R). |
| 823 | | % card() >= dealt with above |
| 824 | | % not_empty_aux(member(_,TotalFunction)) x: Dom --> R & Dom /= {} ---> R /={} |
| 825 | | |
| 826 | | |
| 827 | | |
| 828 | | |
| 829 | | % DETECT ENUMERATED constants part of a deferred set |
| 830 | | % the following could be further improved |
| 831 | | % try and find out how many different identifiers are in a list in the context of a predicate Prop |
| 832 | | % it is also called by b_get_disjoint_constants_of_type_calc in bmachine |
| 833 | | %find_inequal_global_set_identifiers(L,GS,_P,_R) :- print(find_inequal_global_set_identifiers(L,GS)),nl,fail. |
| 834 | | |
| 835 | | :- use_module(bsyntaxtree,[conjunction_to_list/2]). |
| 836 | | find_inequal_global_set_identifiers(IDS,GS,Prop,Res) :- |
| 837 | | sort(IDS,SIDS), |
| 838 | | conjunction_to_list(Prop,Preds), |
| 839 | | find_inequal_global_set_identifiers1(SIDS,GS,Preds,Res). |
| 840 | | find_inequal_global_set_identifiers1(SIDS,GS,Preds,Res) :- |
| 841 | | length(SIDS,Card), Card>50, |
| 842 | | % try find all_different predicate first, especially for very large deferred sets the code below is slow |
| 843 | | member(b(C,pred,_),Preds), |
| 844 | | all_different(C,List1,Card,GS,Preds), % we have found an all_different predicate of the right size |
| 845 | | get_texpr_ids(List1,L1), |
| 846 | | sort(L1,SIDS),!, % the all_different predicate matches all our identifiers |
| 847 | | debug_println(9,detected_all_diff_global_set(GS,Card)), |
| 848 | | Res=SIDS. |
| 849 | | find_inequal_global_set_identifiers1(SIDS,GS,Preds,Res) :- |
| 850 | | %format('Finding enumerated elements of ~w (over ~w) in: ',[GS,IDS]),translate:print_bexpr(Prop),nl, |
| 851 | | % first apply nested partition predicates as much as possible to obtain max. large partitions of distinct elements |
| 852 | | get_relevant_partition_preds(Preds,GS,RelevantPartitionPreds), % TO DO: cache this computation |
| 853 | | findall(TP,find_a_transitive_partition(RelevantPartitionPreds,TP),TransitivePartitions), |
| 854 | | append(TransitivePartitions,Preds,Preds2), |
| 855 | | add_true(SIDS,TIDS),ord_list_to_avl(TIDS,IDS_AVL), |
| 856 | | find_inequal_global_set_identifiers2(SIDS,IDS_AVL,GS,Preds2,Res). |
| 857 | | |
| 858 | | % utility to be able to call list_to_avl |
| 859 | | add_true([],[]). |
| 860 | | add_true([H|T],[H-true|TT]) :- add_true(T,TT). |
| 861 | | |
| 862 | | |
| 863 | | find_inequal_global_set_identifiers2([],_,_,_,[]). |
| 864 | | find_inequal_global_set_identifiers2([ID|T],AVL,GS,Preds,Res) :- |
| 865 | | (atomic(ID) -> true |
| 866 | | ; add_internal_error('Not atomic id: ',find_inequal_global_set_identifiers([ID|T],GS,Preds,Res)),fail), |
| 867 | | avl_delete(ID,AVL,_,AVL1), |
| 868 | | findall(ID2, (find_inequality(GS,Preds,ID,ID2), |
| 869 | | avl_fetch(ID2, AVL1,_) |
| 870 | | ), DiffIDs), |
| 871 | | sort(DiffIDs,SortedDiffIDs), % also remove duplicates |
| 872 | | (SortedDiffIDs=[],T=[_,_|_] % then try to proceed with T, ignoring ID |
| 873 | | -> find_inequal_global_set_identifiers2(T,AVL1,GS,Preds,Res) |
| 874 | | ; add_true(SortedDiffIDs,SIDT),ord_list_to_avl(SIDT,AVL2), |
| 875 | | Res = [ID|RT], |
| 876 | | find_inequal_global_set_identifiers2(SortedDiffIDs,AVL2,GS,Preds,RT) |
| 877 | | ). |
| 878 | | |
| 879 | | %find_inequality(_,_,ID,ID2) :- % TODO: make usable; currently VALUES clause is precompiled after this is used |
| 880 | | % b_extract_values_clause_assignment(ID,Type,TVal1), |
| 881 | | % b_extract_values_clause_assignment(ID2,Type,TVal2), |
| 882 | | % ID \= ID2, TVal1 \= TVal2. |
| 883 | | find_inequality(GS,Preds,ID,ID2) :- |
| 884 | ? | member(Conjunct,Preds), %print(chck(C)),nl, |
| 885 | | %translate:print_bexpr_with_limit(Conjunct,100),debug:nl_time, |
| 886 | ? | inequality(Conjunct,GS,ID,ID2,Preds). |
| 887 | | |
| 888 | | |
| 889 | | get_relevant_partition_preds(Preds,GS,SortedRelevantPartitionPreds) :- |
| 890 | | % detect which partition predicates are relevant for this global set |
| 891 | | findall(partition(Set,Subsets), |
| 892 | | (member(C,Preds), |
| 893 | | is_relevant_partition(C,GS,Set,Subsets)), RelevantPartitionPreds), |
| 894 | | sort(RelevantPartitionPreds,SortedRelevantPartitionPreds). |
| 895 | | is_relevant_partition(b(partition(Set,Subsets),pred,_),GS,Set,Subsets) :- |
| 896 | | get_texpr_type(Set,set(GS)). % , translate:print_bexpr(b(partition(Set,Subsets),pred,[])),nl. |
| 897 | | |
| 898 | | % if we have partition(A,[B,C]) and partition(B,[E,F]) --> generate partition(A,[E,F,C]) |
| 899 | | find_a_transitive_partition(Preds,b(partition(A,C),pred,[generated])) :- |
| 900 | ? | member(partition(A,B),Preds), |
| 901 | | inline_subsets(B,Preds,Inlined,C), Inlined==inlined. |
| 902 | | inline_subsets([],_,_,[]). |
| 903 | | inline_subsets([Subset1|TS],Preds,inlined,Result) :- get_texpr_id(Subset1,SubID), |
| 904 | | %prefix(Pred,[partition(S2,SubList)|Pred2]), |
| 905 | ? | select(partition(Subset2,SubList),Preds,Pred2), |
| 906 | | get_texpr_id(Subset2,SubID), |
| 907 | | debug_format(19,'Inlining nested partition predicate for set ~w~n',[SubID]), |
| 908 | | !, |
| 909 | | append(SubList,TS,NewList), |
| 910 | | inline_subsets(NewList,Pred2,_,Result). |
| 911 | | inline_subsets([Subset1|TS],Preds,Inlined,[Subset1|TSRes]) :- inline_subsets(TS,Preds,Inlined,TSRes). |
| 912 | | |
| 913 | | |
| 914 | | inequality(b(P,pred,_),GS,ID,OtherID,FullProps) :- |
| 915 | ? | inequality_aux(P,GS,ID,OtherID,FullProps). |
| 916 | | inequality_aux(not_equal(I1,I2),GS,ID,OtherID,_) :- |
| 917 | | gs_identifier(I1,GS,ID1), gs_identifier(I2,GS,ID2), |
| 918 | | (ID=ID1 -> OtherID=ID2 ; ID=ID2,OtherID=ID1). |
| 919 | | inequality_aux(not_equal(I1,I2),GS,ID,OtherID,_) :- % treat {aa} \= {bb} or more generally {aa,bb} \= {aa,cc} |
| 920 | | % two identifiers of global sets need not be different |
| 921 | | % in order for two set extensions to be inequal |
| 922 | | % first we check if I1, I2 are in fact subsets of global sets |
| 923 | | get_texpr_type(I1,set(global(_))), |
| 924 | | get_texpr_expr(I1,set_extension(IDs1)), % TODO: is there something more general than a set_extension? |
| 925 | | get_texpr_expr(I2,set_extension(IDs2)), % should full sets or set identifiers added? |
| 926 | | % remove the common elements and see if we find a pair of identifiers |
| 927 | | maplist(remove_all_infos_and_ground,IDs1,IDs1NoInfos), |
| 928 | | maplist(remove_all_infos_and_ground,IDs2,IDs2NoInfos), |
| 929 | | % TODO: maybe it is same to assume the order? |
| 930 | | list_to_ord_set(IDs1NoInfos,IDs1Set), list_to_ord_set(IDs2NoInfos,IDs2Set), |
| 931 | | ord_subtract(IDs1Set,IDs2Set,[E1]), % each set has one identifier that is not in the other one |
| 932 | | ord_subtract(IDs2Set,IDs1Set,[E2]), |
| 933 | | E1 \= E2, % and they are not the same |
| 934 | | gs_identifier(E1,GS,ID1), gs_identifier(E2,GS,ID2), |
| 935 | | set_ids(ID1,ID2,ID,OtherID). |
| 936 | | inequality_aux(negation( b(equal(I1,I2),pred,_)),GS,ID,OtherID,_) :- |
| 937 | | gs_identifier(I1,GS,ID1), gs_identifier(I2,GS,ID2), |
| 938 | | set_ids(ID1,ID2,ID,OtherID). |
| 939 | | inequality_aux(partition(Set,DisjSets),GS,ID,OtherID,Preds) :- |
| 940 | | get_texpr_type(Set,set(GS)), % only look at relevant partitions of correct type |
| 941 | | %nl,print(part(_Set,DisjSets,GS,ID,OtherID)),nl, |
| 942 | | % detect such things as partition(_,{...ID...},...{...OtherID...}...) |
| 943 | ? | select(Set1,DisjSets,Rest), set_extension_list(Set1,Preds,List1), |
| 944 | ? | member(O1,List1), gs_identifier(O1,GS,ID), |
| 945 | ? | member(Set2,Rest), set_extension_list(Set2,Preds,List2), |
| 946 | ? | member(O2,List2), gs_identifier(O2,GS,OtherID). |
| 947 | | inequality_aux(member(I1,SetDiff),GS,ID,OtherID,_Preds) :- |
| 948 | | % detect ID : SUPERSET - { ... OtherID ...} => ID:SUPERSET & ID /= OtherID |
| 949 | | get_texpr_expr(SetDiff,set_subtraction(_SuperSet,b(OtherSet,_,_))), |
| 950 | | gs_identifier(I1,GS,ID1), |
| 951 | | id_element_of_set(OtherSet,GS,ID2), |
| 952 | | set_ids(ID1,ID2,ID,OtherID). |
| 953 | | inequality_aux(AllDiff,GS,ID,OtherID,Preds) :- |
| 954 | | all_different(AllDiff,List1,_Card,GS,Preds), |
| 955 | | select(O1,List1,RestList), gs_identifier(O1,GS,ID), |
| 956 | | member(O2,RestList), gs_identifier(O2,GS,OtherID). |
| 957 | | |
| 958 | | set_ids(ID1,ID2,ID,OtherID) :- (ID=ID1 -> OtherID=ID2 ; ID=ID2,OtherID=ID1). |
| 959 | | |
| 960 | | id_element_of_set(set_extension(List),GS,ID) :- |
| 961 | | member(I2,List), |
| 962 | | gs_identifier(I2,GS,ID). |
| 963 | | |
| 964 | | % detect card({x1,....,xn}) = n as an all-different predicate |
| 965 | | all_different(equal(A,B),List,Card,Type,Preds) :- |
| 966 | | all_diff_aux(A,B,List,Card,Type,Preds) ; all_diff_aux(B,A,List,Card,Type,Preds). |
| 967 | | all_diff_aux(A,B,List1,Card,Type,Preds) :- |
| 968 | | A=b(card(Set1),_,_), |
| 969 | | get_texpr_type(Set1,set(Type)), % TO DO: also match seq type ? (in case we use predicate in other context) |
| 970 | | set_extension_list(Set1,Preds,List1), |
| 971 | | evaluable_integer_expression(B,b(truth,pred,[]),Card), |
| 972 | | length(List1,Card). |
| 973 | | |
| 974 | | set_extension_list(b(set_extension(List),_,_),_,List). |
| 975 | | set_extension_list(b(identifier(ID),_,_),Preds,List) :- |
| 976 | | % accept card(GS) = nr & ... GS = {....} |
| 977 | ? | member(Eq,Preds), |
| 978 | | equality(Eq,TID,b(set_extension(List),_,_)), |
| 979 | | get_texpr_id(TID,ID). |
| 980 | | |
| 981 | | equality(b(equal(LHS,RHS),pred,_),L,R) :- ( (L,R)=(LHS,RHS) ; (L,R)=(RHS,LHS) ). |
| 982 | | |
| 983 | | gs_identifier(b(identifier(ID),GS,_),GS,ID). |
| 984 | | |
| 985 | | :- 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) |
| 986 | | ). |
| 987 | | :- 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), |
| 988 | | GS=='TITLE', Card=4) |
| 989 | | ). |
| 990 | | |
| 991 | | is_equality_card_expression(TE,Properties,Expr,Card) :- |
| 992 | | get_texpr_expr(TE,equal(LHS,RHS)), |
| 993 | | get_texpr_expr(LHS,L), get_texpr_expr(RHS,R), |
| 994 | | ( L=card(Expr), evaluable_integer_expression(R,Properties,Card) |
| 995 | | ; R=card(Expr), evaluable_integer_expression(L,Properties,Card)). |
| 996 | | |
| 997 | | is_equality_card_global_set(TE,GlobalSet,Properties,Card) :- |
| 998 | | is_equality_card_expression(TE,Properties,Expr,Card), |
| 999 | | global_set_identifier(Expr,GlobalSet), |
| 1000 | | get_texpr_type(Expr,set(global(GlobalSet))). |
| 1001 | | |
| 1002 | | % detect a predicate that stipulates that given Set is infinite |
| 1003 | | % i.e., we detect not(finite(GS)) which can be rewritten from not(GS:FIN(GS)) in ast_cleanup by introduce_finite rule |
| 1004 | | is_infinite_global_set_pred(Pred,GlobalSetName) :- |
| 1005 | | get_texpr_expr(Pred,negation(Pred2)), |
| 1006 | | get_texpr_expr(Pred2,finite(ID)), |
| 1007 | | get_texpr_id(ID,GlobalSetName). |
| 1008 | | |
| 1009 | | %evaluable_integer_expression(X,_Y,_) :- print(ev(X)),nl,fail. |
| 1010 | | % TO DO: maybe we should do some kind of constant folding or call b_compile ?? |
| 1011 | | evaluable_integer_expression(b(E,integer,_),Properties,R) :- |
| 1012 | | evaluable_integer_expression(E,Properties,R). |
| 1013 | | evaluable_integer_expression(max_int,_,R) :- preferences:preference(maxint,R). |
| 1014 | | evaluable_integer_expression(min_int,_,R) :- preferences:preference(minint,R). |
| 1015 | | evaluable_integer_expression(identifier(ID),Properties,R) :- |
| 1016 | | get_texpr_expr(Eq,equal(LHS,RHS)), get_texpr_id(LHS,ID), |
| 1017 | | select_member_in_conjunction(Eq,Properties,RestProp), % avoids loops; but an identifier cannot be used multiple times N+N |
| 1018 | | evaluable_integer_expression(RHS,RestProp,R). |
| 1019 | | evaluable_integer_expression(card(Set),Properties,Card) :- |
| 1020 | | Set = b(identifier(GlobalSetName),set(global(GlobalSetName)),_), |
| 1021 | | (extract_setsize_from_machine_cache(GlobalSetName,L,U) |
| 1022 | | -> Card is U+1-L |
| 1023 | | ; select_member_in_conjunction(Eq,Properties,RestProp), |
| 1024 | | is_equality_card_global_set(Eq,GlobalSetName,RestProp,Card) |
| 1025 | | ). |
| 1026 | | evaluable_integer_expression(integer(Card),_,Card). |
| 1027 | | evaluable_integer_expression(div(A,B),Properties,Res) :- |
| 1028 | | evaluable_integer_expression(A,Properties,RA), |
| 1029 | | evaluable_integer_expression(B,Properties,RB), Res is RA // RB. |
| 1030 | | evaluable_integer_expression(multiplication(A,B),Properties,Res) :- |
| 1031 | | evaluable_integer_expression(A,Properties,RA), |
| 1032 | | evaluable_integer_expression(B,Properties,RB), Res is RA*RB. |
| 1033 | | evaluable_integer_expression(add(A,B),Properties,Res) :- |
| 1034 | | evaluable_integer_expression(A,Properties,RA), |
| 1035 | | evaluable_integer_expression(B,Properties,RB), Res is RA+RB. |
| 1036 | | evaluable_integer_expression(minus(A,B),Properties,Res) :- |
| 1037 | | evaluable_integer_expression(A,Properties,RA), |
| 1038 | | evaluable_integer_expression(B,Properties,RB), Res is RA-RB. |
| 1039 | | evaluable_integer_expression(unary_minus(A),Properties,Res) :- |
| 1040 | | evaluable_integer_expression(A,Properties,RA), Res is 0-RA. |
| 1041 | | |
| 1042 | | % checks if we have an identifier or a precompiled global_set value |
| 1043 | | global_set_identifier(C,GS) :- get_texpr_expr(C,BE), global_set_identifier2(BE,GS). |
| 1044 | | global_set_identifier2(identifier(GlobalSet),GlobalSet). |
| 1045 | | global_set_identifier2(value(global_set(GlobalSet)),GlobalSet). % generated by Z |
| 1046 | | |
| 1047 | | % check for card(GlobalSet) >= Card or similar |
| 1048 | | is_greaterequalthan_card_global_set(TE,GlobalSet,Properties,Card) :- |
| 1049 | | is_greaterequalthan_card_global_set_id(TE,GlobalSet,GlobalSet,Properties,Card). |
| 1050 | | % check for card(Identifier) >= Card or similar with Identifier of type GlobalSet |
| 1051 | | is_greaterequalthan_card_global_set_id(TE,Identifier,GlobalSet,Properties,Card) :- |
| 1052 | | (get_texpr_expr(TE,greater_equal(LHS,RHS)) ; |
| 1053 | | get_texpr_expr(TE,less_equal(RHS,LHS)) ), |
| 1054 | | get_texpr_expr(LHS,card(C)), |
| 1055 | | get_minimum_or_exact_value(RHS,Properties,Card), |
| 1056 | | global_set_identifier(C,Identifier), |
| 1057 | | get_texpr_type(C,set(global(GlobalSet))). |
| 1058 | | is_greaterequalthan_card_global_set_id(TE,Identifier,GlobalSet,Properties,Card1) :- |
| 1059 | | (get_texpr_expr(TE,greater(LHS,RHS)) ; |
| 1060 | | get_texpr_expr(TE,less(RHS,LHS)) ), |
| 1061 | | get_texpr_expr(LHS,card(C)), |
| 1062 | | get_minimum_or_exact_value(RHS,Properties,Card), |
| 1063 | | number(Card), Card1 is Card+1, |
| 1064 | | global_set_identifier(C,Identifier), |
| 1065 | | get_texpr_type(C,set(global(GlobalSet))). |
| 1066 | | is_greaterequalthan_card_global_set_id(TE,GlobalSet,GlobalSet,_Properties,2) :- |
| 1067 | | %% preferences:get_preference(allow_empty_global_sets,false), preference no longer exists |
| 1068 | | /* GlobalSet /= { ANY } -> as GlobalSet cannot be empty & as ANY must be well-typed: |
| 1069 | | we need at least one more element of GlobalSet */ |
| 1070 | | get_texpr_expr(TE,not_equal(LHS,RHS)), |
| 1071 | | ( get_texpr_expr(LHS,identifier(GlobalSet)) |
| 1072 | | -> get_texpr_expr(RHS,set_extension([b(_X,global(GlobalSet),_)])) |
| 1073 | | ; get_texpr_expr(RHS,identifier(GlobalSet)), |
| 1074 | | get_texpr_expr(LHS,set_extension([b(_X,global(GlobalSet),_)])) |
| 1075 | | ). |
| 1076 | | %%print(not_equal(GlobalSet,_X)),nl. |
| 1077 | | % 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))])) |
| 1078 | | |
| 1079 | | % get mininimum or exact value for an expression |
| 1080 | | get_minimum_or_exact_value(TE,Properties,N) :- %print(get_min(TE,Properties)),nl,nl, |
| 1081 | | get_texpr_expr(TE,E), |
| 1082 | | get_minimum_or_exact_value_aux(E,Properties,N). |
| 1083 | | get_minimum_or_exact_value_aux(integer(N),_,N). |
| 1084 | | get_minimum_or_exact_value_aux(identifier(ID),Properties,N) :- |
| 1085 | | %(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 |
| 1086 | | findall(NVal,extract_min_or_exact_value_for_id(ID,Properties,NVal),NVals), |
| 1087 | | max_member(N,NVals). % find the maximum value for which we need to be greater(_equal) to |
| 1088 | | |
| 1089 | | get_minimum_or_exact_value_aux(add(A,B),Properties,Res) :- |
| 1090 | | get_minimum_or_exact_value(A,Properties,RA), |
| 1091 | | get_minimum_or_exact_value(B,Properties,RB), Res is RA+RB. |
| 1092 | | % TO DO: other operators |
| 1093 | | get_minimum_or_exact_value_aux(card(Set),_Properties,Card) :- |
| 1094 | | Set = b(identifier(GlobalSetName),set(global(GlobalSetName)),_), |
| 1095 | | try_extract_setsize_from_machine(GlobalSetName,L,U), % will try extraction; unless a cycle is hit |
| 1096 | | Card is U+1-L. |
| 1097 | | |
| 1098 | | extract_min_or_exact_value_for_id(ID,Properties,N) :- |
| 1099 | | member_in_conjunction(TE,Properties), |
| 1100 | | get_texpr_expr(TE,E), |
| 1101 | | get_value_bound(E,ID,N). |
| 1102 | | |
| 1103 | | % equalities already inlined |
| 1104 | | get_value_bound(equal(LHS,RHS),ID,N) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N). |
| 1105 | | get_value_bound(equal(RHS,LHS),ID,N) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N). |
| 1106 | | get_value_bound(greater(LHS,RHS),ID,N1) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N), N1 is N+1. |
| 1107 | | get_value_bound(less(RHS,LHS),ID,N1) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N), N1 is N+1. |
| 1108 | | get_value_bound(greater_equal(LHS,RHS),ID,N) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N). |
| 1109 | | get_value_bound(less_equal(RHS,LHS),ID,N) :- get_texpr_id(LHS,ID), get_texpr_integer(RHS,N). |
| 1110 | | |
| 1111 | | get_texpr_integer(b(integer(N),_,_),N). |
| 1112 | | |
| 1113 | | |
| 1114 | | :- volatile global_set_user_defined_scope/2. |
| 1115 | | :- dynamic global_set_user_defined_scope/2. |
| 1116 | | |
| 1117 | | /* allow to set scope for specific sets, e.g., via command-line */ |
| 1118 | | set_user_defined_scope(GS,X) :- |
| 1119 | | \+ number(X),!, |
| 1120 | | add_internal_error('Scope must be number: ',set_user_defined_scope(GS,X)). |
| 1121 | | set_user_defined_scope(GS,X) :- |
| 1122 | | format('% Setting user defined scope: ~w == ~w~n',[GS,X]), |
| 1123 | | assertz(global_set_user_defined_scope(GS,X)). |
| 1124 | | |
| 1125 | | get_user_defined_scope(GlobalSetName,_,_,_) :- var(GlobalSetName),!, |
| 1126 | | add_internal_error('Arg is variable: ',get_user_defined_scope(GlobalSetName)). |
| 1127 | | get_user_defined_scope(GlobalSetName,LowBound,UpBound,Span) :- |
| 1128 | | (global_set_user_defined_scope(GlobalSetName,UpBound) % from command-line |
| 1129 | | -> LowBound=1, Span = unknown |
| 1130 | | ; extract_setsize_from_defs(GlobalSetName,LowBound,UpBound,Span) % scopeSET == Low..Up from DEFINITIONS |
| 1131 | | ). |
| 1132 | | |
| 1133 | | :- use_module(translate,[translate_bexpression/2]). |
| 1134 | | % find scope_NAME == Low..Up in DEFINITIONS |
| 1135 | | extract_setsize_from_defs(GlobalSetName,LowBound,UpBound,DefTerm) :- |
| 1136 | | b_get_machine_setscope(GlobalSetName,DefTerm), |
| 1137 | | get_texpr_expr(DefTerm,DefExpr), |
| 1138 | | (extract_integer_range(DefExpr,LowBound,UpBound) |
| 1139 | | -> true |
| 1140 | | ; translate_bexpression(DefTerm,DS), |
| 1141 | | add_warning(extract_setsize_from_defs,'scope DEFINITION for deferred set should be number or interval: ',DS,DefTerm), |
| 1142 | | fail |
| 1143 | | ). |
| 1144 | | |
| 1145 | | extract_integer_range(interval(LB,UB), LowBound, UpBound) :- |
| 1146 | | get_texpr_expr(LB,integer(LowBound)), get_texpr_expr(UB,integer(UpBound)). |
| 1147 | | %extract_integer_range(set_extension(CstList),LowBound,UpBound) :- |
| 1148 | | % LowBound = 1, length(CstList,UpBound). % extract names of constants in list for pretty printing; check that different names |
| 1149 | | %extract_integer_range(value(avl_set(A)),LowBound,UpBound) :- |
| 1150 | | % LowBound = 1, avl_size(A,UpBound). |
| 1151 | | extract_integer_range(integer(UpBound),LowBound,UpBound) :- |
| 1152 | | LowBound = 1, UpBound>0. |
| 1153 | | |
| 1154 | | |
| 1155 | | :- dynamic start_extracting_setsize/1. |
| 1156 | | |
| 1157 | | start_extracting_setsize_from_machine(GlobalSetName) :- %print(start(GlobalSetName)),nl, |
| 1158 | | (start_extracting_setsize(GlobalSetName) |
| 1159 | | -> add_internal_error('Cyclic computation: ',start_extracting_setsize_from_machine(GlobalSetName)) |
| 1160 | | ; assertz(start_extracting_setsize(GlobalSetName))). |
| 1161 | | |
| 1162 | | assert_extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound) :- |
| 1163 | | retractall(start_extracting_setsize(GlobalSetName)), |
| 1164 | | %print(finished(GlobalSetName,LowBound,UpBound)),nl, |
| 1165 | | (retract(extract_setsize_from_machine_cache(GlobalSetName,L,U)) |
| 1166 | | -> print(overriding_set_size(GlobalSetName,LowBound-UpBound,L-U)),nl |
| 1167 | | ; true), |
| 1168 | | assertz(extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound)), |
| 1169 | | (integer(UpBound), UpBound<LowBound |
| 1170 | | -> format_error_with_nl('*** Illegal empty global set ~w, bounds ~w:~w',[GlobalSetName,LowBound,UpBound]) |
| 1171 | | ; true |
| 1172 | | ). |
| 1173 | | |
| 1174 | | |
| 1175 | | %% b_try_update_fd_cardinality has been removed |
| 1176 | | |
| 1177 | | :- volatile enumerated_set/1, fixed_deferred_set_size/2. |
| 1178 | | :- dynamic enumerated_set/1, fixed_deferred_set_size/2. |
| 1179 | | % true if GS is a deferred set whose size was not fixed; i.e., ProB has not inspected all possible instantiations |
| 1180 | | % TODO: rename to unfixed_or_infinite_deferred_set |
| 1181 | | unfixed_deferred_set(GS) :- |
| 1182 | ? | if(b_global_set(GS), |
| 1183 | | (\+ enumerated_set(GS), |
| 1184 | | \+ fixed_finite_deferred_set_size(GS,_)), |
| 1185 | | (debug_println(unknown_global_set(GS)),fail)). % triggered in test 2063 |
| 1186 | | |
| 1187 | ? | unfixed_deferred_set_exists :- b_global_set(GS), unfixed_deferred_set(GS),!. |
| 1188 | | |
| 1189 | | % a global set that is treated as infinite by ProB |
| 1190 | | % not unfixed deferred sets may still in principle allowed to be infinite, but could be give a finite card by ProB |
| 1191 | | infinite_global_set(GlobalSetName) :- |
| 1192 | | (fixed_deferred_set_size(GlobalSetName,X) -> X=inf |
| 1193 | | ; inferred_maximum_global_set_cardinality(GlobalSetName,MaxCard) -> MaxCard=inf % should not happen |
| 1194 | | ; enumerated_set(GlobalSetName) -> false |
| 1195 | | % ; (precompilation_phase(Phase) -> true ; Phase=0), |
| 1196 | | % nl,print(not_provably_infinite_global_set(GlobalSetName,Phase)),nl,nl,portray_global_sets,nl,fail |
| 1197 | | ). |
| 1198 | | |
| 1199 | | provably_finite_global_set(GlobalSetName) :- |
| 1200 | | enumerated_set(GlobalSetName),!. |
| 1201 | | provably_finite_global_set(GlobalSetName) :- |
| 1202 | | fixed_deferred_set_size(GlobalSetName,X),!, number(X). |
| 1203 | | provably_finite_global_set(GlobalSetName) :- |
| 1204 | | inferred_maximum_global_set_cardinality(GlobalSetName,MaxCard),!, |
| 1205 | | integer(MaxCard). |
| 1206 | | %provably_finite_global_set(GS) :- (precompilation_phase(Phase) -> true ; Phase=0), |
| 1207 | | % nl,print(not_provably_finite_global_set(GS,Phase)),nl,nl,portray_global_sets,nl,fail. |
| 1208 | | |
| 1209 | | fixed_finite_deferred_set_size(Set,Card) :- fixed_deferred_set_size(Set,Card), integer(Card). |
| 1210 | | |
| 1211 | ? | contains_unfixed_deferred_set(Type) :- (contains_unfixed_deferred_set(Type,_) -> true). |
| 1212 | | |
| 1213 | ? | contains_unfixed_deferred_set(global(Type),DS) :- unfixed_deferred_set(Type),DS=Type. |
| 1214 | ? | contains_unfixed_deferred_set(set(Type),DS) :- contains_unfixed_deferred_set(Type,DS). |
| 1215 | | contains_unfixed_deferred_set(seq(Type),DS) :- contains_unfixed_deferred_set(Type,DS). |
| 1216 | | contains_unfixed_deferred_set(couple(Type1,Type2),DS) :- |
| 1217 | | (contains_unfixed_deferred_set(Type1,DS) -> true ; contains_unfixed_deferred_set(Type2,DS)). |
| 1218 | | contains_unfixed_deferred_set(record(Fields),DS) :- |
| 1219 | | (member(field(_,Type),Fields), contains_unfixed_deferred_set(Type,DS) -> true). |
| 1220 | | |
| 1221 | | |
| 1222 | | % enumerated sets can be registered here, before cleaning up a machine |
| 1223 | | % this way we already know which sets are enumerated and definitely finite |
| 1224 | | % and we can also register the enumerated set elements |
| 1225 | | register_enumerated_sets([],_). |
| 1226 | | register_enumerated_sets([TID|T],Elems) :- def_get_texpr_id(TID,ID), get_texpr_type(TID,set(Type)), |
| 1227 | | El = b(identifier(Elem),Type,_), |
| 1228 | | findall(Elem,member(El,Elems),EnumElems), |
| 1229 | | pre_register_enumerated_set_with_elems(ID,EnumElems), |
| 1230 | | register_enumerated_sets(T,Elems). |
| 1231 | | |
| 1232 | | pre_register_enumerated_set_with_elems(GlobalSetName,ListOfConstants) :- |
| 1233 | | (enumerated_set(GlobalSetName) -> true |
| 1234 | | ; debug_format(19,'Pre-register ~w = ~w~n',[GlobalSetName,ListOfConstants]), |
| 1235 | | assertz(enumerated_set(GlobalSetName)), |
| 1236 | | LowBound=1, |
| 1237 | | add_named_constants_to_global_set(GlobalSetName,LowBound,ListOfConstants) % probably only lookup_global_constant relevant |
| 1238 | | ). |
| 1239 | | % pre-registering just the enumerated set name |
| 1240 | | pre_register_enumerated_set(GlobalSetName) :- |
| 1241 | | (enumerated_set(GlobalSetName) -> true |
| 1242 | | ; debug_format(9,'Pre-register ~w~n',[GlobalSetName]), |
| 1243 | | assertz(enumerated_set(GlobalSetName)) |
| 1244 | | ). |
| 1245 | | |
| 1246 | | |
| 1247 | | :- assert_pre(b_global_sets:assert_enumerated_set(_GS,_L,_,_),true). |
| 1248 | | % TODO(DP, 7.8.2008) |
| 1249 | | % (atomic(GS),type_check(L,list(xml_identifier)))). |
| 1250 | | :- assert_post(b_global_sets:assert_enumerated_set(_,_,L,U),(number(L),number(U))). |
| 1251 | | |
| 1252 | | % TODO: also process b_extract_values_clause_assignment(Cst,integer,Nr) facts ! |
| 1253 | | assert_enumerated_set(GlobalSetName,ListOfConstants,LowBound,UpBound) :- |
| 1254 | | pre_register_enumerated_set(GlobalSetName), |
| 1255 | | % print_message(enum_set(GlobalSetName,ListOfConstants)), |
| 1256 | | LowBound = 1, |
| 1257 | | length(ListOfConstants,UpBound), |
| 1258 | | assert_extract_setsize_from_machine_cache(GlobalSetName,LowBound,UpBound), |
| 1259 | | add_named_constants_to_global_set(GlobalSetName,LowBound,ListOfConstants). |
| 1260 | | |
| 1261 | | add_named_constants_to_global_set(GlobalSetName,LowBound,ListOfConstants) :- |
| 1262 | | (b_global_constant(GlobalSetName,CurNr,CurCst) |
| 1263 | | -> add_error_fail(add_named_constants_to_global_set,'Globalset already has constants: ', |
| 1264 | | b_global_constant(GlobalSetName,CurNr,CurCst)) |
| 1265 | | ; true), |
| 1266 | ? | nth0(Nr0,ListOfConstants,Cst), |
| 1267 | | (lookup_global_constant(Cst,fd(_,GS2)) |
| 1268 | | -> (GS2=GlobalSetName |
| 1269 | | -> add_internal_error('Duplicate element in global set:',(Cst,GS2)) % error is already caught by type checker |
| 1270 | | ; add_internal_error('Element appears in multiple sets:',(Cst,GS2,GlobalSetName)) % ditto |
| 1271 | | ) |
| 1272 | | ; true |
| 1273 | | ), |
| 1274 | | Nr is Nr0+LowBound, |
| 1275 | | assertz(b_global_constant(GlobalSetName,Nr,Cst)), |
| 1276 | | term_hash(fd(Nr,GlobalSetName),Hash), |
| 1277 | | assertz(b_global_constant_hash(Hash,GlobalSetName,Nr,Cst)), |
| 1278 | | assertz(lookup_global_constant(Cst,fd(Nr,GlobalSetName))), |
| 1279 | | %format('Added ~w as nr ~w to ~w~n',[Cst,Nr,GlobalSetName]), |
| 1280 | | fail. |
| 1281 | | add_named_constants_to_global_set(_,_,_). |
| 1282 | | |
| 1283 | | |
| 1284 | | %add_global_set_with_named_constants(GlobalSetName,ListOfConstants) :- |
| 1285 | | % (b_global_sets:assert_enumerated_set(GlobalSetName,ListOfConstants,_,_)), |
| 1286 | | % add_new_global_set(GlobalSetName). |
| 1287 | | |
| 1288 | | |
| 1289 | | |
| 1290 | | :- assert_pre(b_global_sets:b_extract_fd_type(_G,_L,_U),true). |
| 1291 | | :- assert_post(b_global_sets:b_extract_fd_type(G,L,U),(atomic(G),(integer(L),integer(U)))). |
| 1292 | | |
| 1293 | | b_extract_fd_type(GlobalSetName,LowBound,UpBound) :- |
| 1294 | ? | b_global_set(GlobalSetName), % was b_get_machine_set(GlobalSetName), |
| 1295 | | extract_setsize_from_machine(GlobalSetName,LowBound,UpBound). |
| 1296 | | |
| 1297 | | is_b_precompiled_globalset(GlobalSetName) :- extract_setsize_from_machine_cache(GlobalSetName,_,_). |
| 1298 | | |
| 1299 | | % like b_extract_fd_type above, but with GS known (avoids backtracking b_supplementary_global_set) |
| 1300 | | b_get_fd_type_bounds(NonvarGlobalSetname,LowBound,UpBound) :- nonvar(NonvarGlobalSetname), |
| 1301 | | extract_setsize_from_machine_cache(NonvarGlobalSetname,L,U), |
| 1302 | | !, |
| 1303 | | (LowBound,UpBound)=(L,U). |
| 1304 | | b_get_fd_type_bounds(GS,L,U) :- b_replaced_global_set(GS,_),!, |
| 1305 | | add_internal_error('Global set has been replaced: ',b_get_fd_type_bounds(GS,L,U)),fail. |
| 1306 | | b_get_fd_type_bounds(GS,L,U) :- |
| 1307 | | add_internal_error('Illegal call: ',b_get_fd_type_bounds(GS,L,U)),fail. |
| 1308 | | |
| 1309 | | |
| 1310 | | b_global_set_cardinality('STRING',Card) :- !, Card=inf. |
| 1311 | | b_global_set_cardinality('REAL',Card) :- !, Card=inf. |
| 1312 | | b_global_set_cardinality('FLOAT',Card) :- !, Card=18446744073709551616. % 2^64 - TO DO: check |
| 1313 | | b_global_set_cardinality('NAT',Card) :- !, get_preference(maxint,MaxInt), Card is MaxInt+1. |
| 1314 | | b_global_set_cardinality('NATURAL',Card) :- !, Card=inf. %get_preference(maxint,MaxInt), Card is MaxInt+1. |
| 1315 | | b_global_set_cardinality('NAT1',Card) :- !, get_preference(maxint,Card). |
| 1316 | | b_global_set_cardinality('NATURAL1',Card) :- !, Card=inf. % get_preference(maxint,Card). |
| 1317 | | b_global_set_cardinality('INT',Card) :- !, get_preference(maxint,MaxInt), |
| 1318 | | get_preference(minint,MinInt), |
| 1319 | | (MaxInt >= MinInt -> Card is MaxInt-MinInt+1 |
| 1320 | | ; add_error(b_global_set_cardinality,'MININT larger than MAXINT',(MinInt:MaxInt)), |
| 1321 | | Card = 0 |
| 1322 | | ). |
| 1323 | | b_global_set_cardinality('INTEGER',Card) :- !, Card=inf. % b_global_set_cardinality('INT',Card). |
| 1324 | | b_global_set_cardinality(GlobalSet,Card) :- nonvar(GlobalSet),!, |
| 1325 | | (b_fd_card(GlobalSet,C) -> Card=C |
| 1326 | | ; b_replaced_global_set(GlobalSet,_) -> |
| 1327 | | add_internal_error('Global set has been replaced: ', b_global_set_cardinality(GlobalSet,Card)), |
| 1328 | | fail |
| 1329 | | ; add_internal_error('Unknown global set: ', b_global_set_cardinality(GlobalSet,Card)), |
| 1330 | | fail). |
| 1331 | | b_global_set_cardinality(GlobalSet,Card) :- %b_global_set(GlobalSet), |
| 1332 | | b_extract_fd_type(GlobalSet,Low,Up), Card is 1+ Up - Low. |
| 1333 | | % enum_warning_for_global_set(GlobalSet,'assuming deferred set to be of given cardinality',Card,trigger_true(card)). |
| 1334 | | %% Note: The Disprover now checks whether unfixed_deferred sets were involved; keeping track of implicit enumerations of deferred sets is just too difficult |
| 1335 | | |
| 1336 | | b_fd_card(GlobalSet,Card) :- b_get_fd_type_bounds(GlobalSet,Low,Up), |
| 1337 | | (Up=inf -> Card=inf ; Card is 1+Up-Low). |
| 1338 | | |
| 1339 | | b_non_empty_global_set(_). % allow_empty_global_sets no longer exists; all global_sets are non-empty |
| 1340 | | %b_non_empty_global_set(IntSet) :- b_integer_or_real_or_string_set(IntSet). |
| 1341 | | %b_non_empty_global_set(GlobalSet) :- b_global_set(GlobalSet), |
| 1342 | | % b_get_fd_type_bounds(GlobalSet,Low,Up), Up >= Low. |
| 1343 | | |
| 1344 | | b_empty_global_set(_) :- fail. % allow_empty_global_sets no longer exists; all global_sets are non-empty |
| 1345 | | %b_empty_global_set(GlobalSet) :- %b_global_set(GlobalSet), |
| 1346 | | % b_get_fd_type_bounds(GlobalSet,Low,Up), Up < Low. |
| 1347 | | |
| 1348 | | |
| 1349 | | b_integer_or_real_or_string_set('STRING'). |
| 1350 | | b_integer_or_real_or_string_set('FLOAT'). |
| 1351 | | b_integer_or_real_or_string_set('REAL'). |
| 1352 | | b_integer_or_real_or_string_set(X) :- b_integer_set(X). |
| 1353 | | |
| 1354 | | b_integer_or_real_set('REAL'). |
| 1355 | | b_integer_or_real_set('FLOAT'). |
| 1356 | | b_integer_or_real_set(X) :- b_integer_set(X). |
| 1357 | | |
| 1358 | | b_integer_set('NAT'). b_integer_set('NATURAL'). |
| 1359 | | b_integer_set('NAT1'). b_integer_set('NATURAL1'). |
| 1360 | | b_integer_set('INT'). b_integer_set('INTEGER'). |
| 1361 | | |
| 1362 | | % convert a type term into a global_set term |
| 1363 | | try_b_type2global_set(string,R) :- !, R= global_set('STRING'). |
| 1364 | | try_b_type2global_set(integer,R) :- !, R= global_set('INTEGER'). |
| 1365 | | try_b_type2global_set(real,R) :- !, R= global_set('REAL'). |
| 1366 | ? | try_b_type2global_set(global(GS),R) :- b_global_set(GS),!, R=global_set(GS). |
| 1367 | | try_b_type2global_set(freetype(ID),R) :- !, R=freetype(ID). |
| 1368 | | try_b_type2global_set(boolean,R) :- !, |
| 1369 | | %custom_explicit_sets:construct_avl_from_lists([pred_false /* bool_false */,pred_true /* bool_true */],R). |
| 1370 | | R = avl_set(node(pred_false,true,1,empty,node(pred_true,true,0,empty,empty))). |
| 1371 | | |
| 1372 | | b_type2_set(GS,Res) :- try_b_type2global_set(GS,GR),!, Res=GR. |
| 1373 | | b_type2_set(Type,Res) :- Res = closure(['_zzzz_unary'],[Type],b(truth,pred,[])). |
| 1374 | | %b_type2global_set(GS,_) :- add_error_and_fail(b_type2_set,'Type cannot be converted to global_set: ',GS). |
| 1375 | | |
| 1376 | | :- use_module(fd_utils_clpfd). % in_fd, fd_domain |
| 1377 | | |
| 1378 | | global_type(fd(X,GlobalSet),GlobalSet) :- %b_global_set(GlobalSet), |
| 1379 | | if(b_get_fd_type_bounds(GlobalSet,Low,Up), %print(b_get_fd_type_bounds(X,GlobalSet,Low,Up)),nl, when(nonvar(X),trace), |
| 1380 | | % print(in_fd(X,Low,Up)),nl, |
| 1381 | | in_fd(X,Low,Up), |
| 1382 | | add_internal_error('Illegal global set: ',global_type(fd(X,GlobalSet),GlobalSet))). |
| 1383 | | global_type2(X,GlobalSet) :- %b_global_set(GlobalSet), |
| 1384 | | if(b_get_fd_type_bounds(GlobalSet,Low,Up), |
| 1385 | | in_fd(X,Low,Up), |
| 1386 | | add_internal_error('Illegal global set: ',global_type2(X,GlobalSet))). |
| 1387 | | |
| 1388 | | global_type_wf(fd(X,GlobalSet),GlobalSet,WF) :- %b_global_set(GlobalSet), |
| 1389 | | b_get_fd_type_bounds(GlobalSet,Low,Up), %print(b_get_fd_type_bounds(X,GlobalSet,Low,Up)),nl, |
| 1390 | | in_fd_wf(X,Low,Up,WF). |
| 1391 | | |
| 1392 | | % get value and setup global_type FD constraint if it is a variable |
| 1393 | | get_global_type_value(FD,Type,X) :- |
| 1394 | | (var(FD) % print(fresh(Type,FD)),nl, |
| 1395 | | -> (nonvar(Type) |
| 1396 | | -> global_type2(X,Type) % instantiate FD bounds if we create a fresh FD variable X |
| 1397 | | ; true |
| 1398 | | ), |
| 1399 | | FD = fd(X,Type) |
| 1400 | | ; FD = fd(X,TypeX), |
| 1401 | | (Type \== TypeX, nonvar(Type), nonvar(TypeX) |
| 1402 | | -> add_internal_error('FD Type error:',get_global_type_value(FD,Type,X)) |
| 1403 | | ; true), |
| 1404 | | TypeX=Type |
| 1405 | | ). |
| 1406 | | |
| 1407 | | % like enum_global_type but with a nonvar GlobalSet + generate enum_warning for deferred set (currently commented out) |
| 1408 | | enumerate_global_type_with_enum_warning(R,GlobalSet,EnumWarning,WF) :- var(R),!, % print(enum_var(R,GlobalSet)),nl, |
| 1409 | | b_get_fd_type_bounds_with_enum_warning(X,GlobalSet,Low,Up,EnumWarning,WF), |
| 1410 | | % first setup CLP(FD) bounds before enumerating |
| 1411 | | in_fd(X,Low,Up), % Note: Up can be the restricted range for infinite sets |
| 1412 | | R=fd(X,GlobalSet), |
| 1413 | ? | enum_fd(X,Low,Up). |
| 1414 | | enumerate_global_type_with_enum_warning(fd(X,GlobalSet),GlobalSet,EnumWarning,WF) :- |
| 1415 | | (nonvar(X) -> true |
| 1416 | | ; b_get_fd_type_bounds_with_enum_warning(X,GlobalSet,Low,Up,EnumWarning,WF), |
| 1417 | ? | enum_fd(X,Low,Up) |
| 1418 | | ). |
| 1419 | | |
| 1420 | | b_get_fd_type_bounds_with_enum_warning(X,GlobalSet,Low2,Up2,EnumWarning,WF) :- |
| 1421 | | b_get_fd_type_bounds(GlobalSet,Low,Up), |
| 1422 | | (Up=inf |
| 1423 | | -> fd_domain(X,LowX,UpX), |
| 1424 | | (integer(UpX), integer(LowX) -> Low2=LowX, Up2=UpX |
| 1425 | | ; get_preference(maxint,MaxInt), |
| 1426 | | (integer(LowX), LowX >= MaxInt -> |
| 1427 | | gen_enum_warning_wf(GlobalSet,Low:Up,LowX:LowX,EnumWarning,unknown,WF), |
| 1428 | | Low2=LowX, Up2=LowX % we could increase Up2, e.g., to LowX+MaxInt |
| 1429 | | ; gen_enum_warning_wf(GlobalSet,Low:Up,Low:MaxInt,EnumWarning,unknown,WF), |
| 1430 | | Low2=Low, Up2=MaxInt |
| 1431 | | ) |
| 1432 | | ) |
| 1433 | | ; Low2=Low,Up2=Up |
| 1434 | | ). |
| 1435 | | |
| 1436 | | % enumerate global types, but limit infinite ones |
| 1437 | | enum_global_type_limited(fd(X,GlobalSet),GlobalSet) :- %b_global_set(GlobalSet), |
| 1438 | | (nonvar(GlobalSet) -> |
| 1439 | ? | (b_get_fd_type_bounds_limited(GlobalSet,Low,Up) -> enum_global_type_aux(X,Low,Up,GlobalSet) |
| 1440 | | ; add_internal_error('Illegal value: ',enum_global_type(fd(X,GlobalSet),GlobalSet)),fail) |
| 1441 | | ; b_global_set(GlobalSet), |
| 1442 | | b_get_fd_type_bounds(GlobalSet,Low,Up), |
| 1443 | | enum_global_type_aux(X,Low,Up,GlobalSet) |
| 1444 | | ). |
| 1445 | | |
| 1446 | | enum_global_type_aux(X,Low,Up,GlobalSet) :- |
| 1447 | | atomic(X), |
| 1448 | | !, |
| 1449 | | (number(X),X >= Low, X =< Up |
| 1450 | | -> true |
| 1451 | | ; add_internal_error('Illegal value: ', enum_global_type_aux(X,Low,Up,GlobalSet))). |
| 1452 | | enum_global_type_aux(X,Low,Up,_GlobalSet) :- |
| 1453 | ? | enum_fd(X,Low,Up). |
| 1454 | | |
| 1455 | | % get range information for global set and generate warning if necessary |
| 1456 | | %b_fd_type_with_enum_warning(GlobalSet,Low,Up) :- |
| 1457 | | % b_fd_type(GlobalSet,Low,Up), |
| 1458 | | % enum_warning_for_global_set(GlobalSet,'assuming deferred set to be of finite cardinality',Up,trigger_true(card)). |
| 1459 | | |
| 1460 | | /* ------------------------------------- */ |
| 1461 | | |
| 1462 | | all_elements_of_type(Type,Set) :- |
| 1463 | | all_elements_of_type_wf(Type,Set,no_wf_available). |
| 1464 | | |
| 1465 | | :- block all_elements_of_type_wf(-,?,?). |
| 1466 | | all_elements_of_type_wf(Type,Set,WF) :- % print(all_elements(Type,Set)),nl, |
| 1467 | | all_elements_of_type2(Type,Set,WF). |
| 1468 | | |
| 1469 | | :- use_module(kernel_objects,[all_strings_wf/2, gen_enum_warning_wf/6]). |
| 1470 | | all_elements_of_type2('STRING',Res,WF) :- !, |
| 1471 | | all_strings_wf(Res,WF). |
| 1472 | | all_elements_of_type2('NAT',Res,_WF) :- !, get_preference(maxint,MaxInt), |
| 1473 | | gen_int_set(0,MaxInt,Res). |
| 1474 | | all_elements_of_type2('NATURAL',Res,WF) :- !, get_preference(maxint,MaxInt), |
| 1475 | | gen_enum_warning_wf('NATURAL',0:sup,0:MaxInt,trigger_throw('NATURAL'),unknown,WF), %print('### Warning: expanding NATURAL'),nl, |
| 1476 | | gen_int_set(0,MaxInt,Res). |
| 1477 | | all_elements_of_type2('NAT1',Res,_WF) :- !, get_preference(maxint,MaxInt), |
| 1478 | | gen_int_set(1,MaxInt,Res). |
| 1479 | | all_elements_of_type2('NATURAL1',Res,WF) :- !, |
| 1480 | | get_preference(maxint,MaxInt), |
| 1481 | | gen_enum_warning_wf('NATURAL1',1:sup,1:MaxInt,trigger_throw('NATURAL1'),unknown,WF), %print('### Warning: expanding NATURAL1'),nl, |
| 1482 | | gen_int_set(1,MaxInt,Res). |
| 1483 | | all_elements_of_type2('INT',Res,_WF) :- !, get_preference(maxint,MaxInt), |
| 1484 | | get_preference(minint,MinInt), |
| 1485 | | gen_int_set(MinInt,MaxInt,Res). |
| 1486 | | all_elements_of_type2('INTEGER',Res,WF) :- !, get_preference(maxint,MaxInt), |
| 1487 | | get_preference(minint,MinInt), |
| 1488 | | gen_enum_warning_wf('INTEGER',inf:sup,MinInt:MaxInt,trigger_throw('INTEGER'),unknown,WF), %print('### Warning: expanding INTEGER'),nl, |
| 1489 | | gen_int_set(MinInt,MaxInt,Res). |
| 1490 | | all_elements_of_type2('FLOAT',Res,WF) :- !, all_elements_of_type2('REAL',Res,WF). |
| 1491 | | all_elements_of_type2('REAL',Res,WF) :- !, |
| 1492 | | gen_enum_warning_wf('REAL',inf:sup,0.0:1.0,trigger_throw('REAL'),unknown,WF), |
| 1493 | | Res = [term(floating(0.0)),term(floating(1.0))]. % not sure this will ever be used |
| 1494 | | all_elements_of_type2(Type,Set,WF) :- |
| 1495 | | b_get_fd_type_bounds(Type,Low,Up), |
| 1496 | | (Up=inf |
| 1497 | | -> get_preference(maxint,MaxInt), % infinite deferred set |
| 1498 | | gen_enum_warning_wf(Type,Low:Up,Low:MaxInt,trigger_throw(Type),unknown,WF), |
| 1499 | | findall(fd(El,Type),enum_fd_linear(El,Low,MaxInt),Set) |
| 1500 | | ; % ensure we do not use Random enumeration |
| 1501 | | findall(fd(El,Type),enum_fd_linear(El,Low,Up),Set) |
| 1502 | | ). |
| 1503 | | |
| 1504 | | % a version of all_elements_of_type which may randomise element order if preference set |
| 1505 | | :- block all_elements_of_type_rand_wf(-,?,?). |
| 1506 | | all_elements_of_type_rand_wf(Type,Set,WF) :- % print(all_elements(Type,Set)),nl, |
| 1507 | | all_elements_of_type_rand2(Type,Set,WF). |
| 1508 | | |
| 1509 | ? | all_elements_of_type_rand2(Type,Set,_WF) :- b_global_set(Type),!, |
| 1510 | | b_get_fd_type_bounds(Type,Low,Up), |
| 1511 | | % may use Random enumeration if preference RANDOMISE_ENUMERATION_ORDER set |
| 1512 | | findall(fd(El,Type),enum_fd(El,Low,Up),Set). |
| 1513 | | all_elements_of_type_rand2(Type,Set,WF) :- % TO DO: we could permute the solution here; but currently all_elements_of_type_rand2 is only called for enumerated/deferred sets |
| 1514 | | all_elements_of_type2(Type,Set,WF). |
| 1515 | | |
| 1516 | | |
| 1517 | | gen_int_set(Min,Max,Set) :- |
| 1518 | | (Min>Max -> Set = [] |
| 1519 | | ; Set = [int(Min)|RSet], |
| 1520 | | M1 is Min+1, |
| 1521 | | gen_int_set(M1,Max,RSet)). |
| 1522 | | |
| 1523 | | %% list_contains_unfixed_deferred_set_id(+TypedIds). |
| 1524 | | list_contains_unfixed_deferred_set_id([b(identifier(_),Type,_)|_]) :- |
| 1525 | | contains_unfixed_deferred_set(Type), |
| 1526 | | !. |
| 1527 | | list_contains_unfixed_deferred_set_id([_|T]) :- |
| 1528 | | list_contains_unfixed_deferred_set_id(T). |
| 1529 | | |
| 1530 | | % ----------------- |
| 1531 | | :- public portray_global_sets/0. % debugging utility |
| 1532 | | portray_global_sets :- |
| 1533 | | (enumerated_sets_precompiled -> Comp=true ; Comp=false), |
| 1534 | | format('ENUMERATED SETS (precompiled=~w):~n ',[Comp]), |
| 1535 | | enumerated_set(GS), |
| 1536 | | format(' ~w ',[GS]), |
| 1537 | | fail. |
| 1538 | | portray_global_sets :- |
| 1539 | | (deferred_sets_precompiled -> Comp=true ; Comp=false), |
| 1540 | | format('~nDEFERRED SETS with some constants (precompiled=~w):~n ',[Comp]), |
| 1541 | | b_partially_deferred_set(GS), |
| 1542 | | (is_b_global_constant(GS,_Nr,Cst) -> true), |
| 1543 | | format(' ~w {~w,...} ',[GS, Cst]), |
| 1544 | | (fixed_deferred_set_size(GS,RCard) |
| 1545 | | -> format('(fixed card ~w) ',[RCard]) |
| 1546 | | ; inferred_maximum_global_set_cardinality(GS,MaxCard) |
| 1547 | | -> format('(max card ~w) ',[MaxCard])), |
| 1548 | | fail. |
| 1549 | | portray_global_sets :- |
| 1550 | | (deferred_sets_precompiled -> Comp=true ; Comp=false), |
| 1551 | | format('~nDEFERRED SETS (precompiled=~w):~n ',[Comp]), |
| 1552 | | b_global_deferred_set(GS), |
| 1553 | | format(' ~w ',[GS]), |
| 1554 | | (fixed_deferred_set_size(GS,RCard) |
| 1555 | | -> format('(fixed card ~w) ',[RCard]) |
| 1556 | | ; inferred_maximum_global_set_cardinality(GS,MaxCard) |
| 1557 | | -> format('(max card ~w) ',[MaxCard])), |
| 1558 | | fail. |
| 1559 | | portray_global_sets :- nl. |