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.