1		% (c) 2009-2024 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(kernel_mappings,
6		[ unary_function/3,
7		binary_function/3, binary_arg1_determines_value/3,
8		unary_in_boolean_type/2, unary_not_in_boolean_type/2,
9		unary_in_definitely_true/2,
10		binary_in_boolean_type/2,
11		binary_not_in_boolean_type/2,
12		binary_in_definitely_true/2,
13		cst_in_boolean_type/2, cst_not_in_boolean_type/2,
14		binary_boolean_operator/3,
15		negate_binary_boolean_operator/2,
16		negate_binary_boolean_operator_swap/2,
17		symbolic_closure_binary_operator/1, is_definitely_empty/3, do_not_keep_symbolic/5,
18		symbolic_closure_unary_operator/1, do_not_keep_symbolic_unary/2,
19
20		special_binary_predicate/6,
21
22		unary_kernel_call/8,
23		binary_kernel_call/9,
24		unary_in_kernel_call/6,
25		binary_in_kernel_call/7,
26		kernel_call_predicate/4,
27		kernel_call_predicate_check_element_of_wf/4, kernel_call_predicate_equal_object_optimized/3,
28		kernel_call_predicate_not_equal_object/4,
29		kernel_call_predicate_not_element_of_wf/3,
30		kernel_call/4,
31		kernel_call_apply_to/6,
32
33		kernel_call_predicate3/7, kernel_call_predicate2/6
34		]).
35
36		% new profiler
37		%:- use_module('../extensions/profiler/profiler.pl').
38		%:- use_module('../extensions/profiler/profiler_te.pl').
39		%:- enable_profiling(must_succ_kernel_call/4).
40		%:- enable_profiling(kernel_call_predicate/4).
41		%:- enable_profiling(kernel_call/4).
42		%:- enable_profiling(kernel_call_apply_to/5).
43		%:- enable_profiling(kernel_call_or/5).
44
45		% old profiler
46		%:- use_module(covsrc(hit_profiler), [add_profile_hit/1,add_profile_hit/2]).
47
48		:- use_module(tools).
49
50		:- use_module(module_information,[module_info/2]).
51		:- module_info(group,kernel).
52		:- module_info(description,'This module translates AST constructs to calls in the ProB kernel.').
53
54		:- use_module(self_check).
55		:- use_module(kernel_waitflags,[get_wait_flag0/2]).
56		:- use_module(kernel_tools,[ground_value_check/2, ground_value_opt_check/3]).
57		:- use_module(kernel_z). % compaction and bag_items
58
59		:- meta_predicate kernel_call_or(0,*,*,*,*).
60		:- meta_predicate kernel_call(0,*,*,*).
61
62
63
64		unary_kernel_call(Module,KernelFunction,ESV1,Value,WF,Expr,Type,Span) :-
65		(expects_waitflag_and_span(KernelFunction)
66		-> KernelCall =.. [KernelFunction,ESV1,Value,Span,WF]
67		; expects_waitflag(KernelFunction) -> KernelCall =.. [KernelFunction,ESV1,Value,WF]
68		; KernelCall =.. [KernelFunction,ESV1,Value]
69		),
70		(type_ok_for_wf0(Type) ->
71		Module:KernelCall
72		; reversible_unary_function(KernelFunction)
73		-> kernel_call_or(Module:KernelCall,ESV1,Value,WF,Expr) % if either value is bound it is ok to perform call
74	?	; must_succ_kernel_call(Module:KernelCall,ESV1,WF,Expr)
75		).
76
77		% result is ok for wf0: no optimized AVL representation exists; we do not need to delay calling function
78		type_ok_for_wf0(integer).
79		type_ok_for_wf0(boolean).
80		type_ok_for_wf0(global(_)).
81		type_ok_for_wf0(string).
82
83
84		binary_kernel_call(_,KernelFunction,ESV1,ESV2,Value,WF,_Expr,_Type,Span) :-
85		determined_binary_integer_function(KernelFunction),
86		!,
87		get_wait_flag0(WF,WF0),
88		call_determined_integer_function(KernelFunction,ESV1,ESV2,Value,WF0,WF,Span).
89		%binary_kernel_call(kernel_objects,in_nat_range_wf,ESV1,ESV2,Value,WF,Expr,Type,Span) :- !,
90		% in_nat_range_wf(ESV1,ESV2,Value,WF). % a common call; TO DO: provide optimized treatment
91		binary_kernel_call(Module,KernelFunction,ESV1,ESV2,Value,WF,Expr,Type,Span) :-
92		(expects_waitflag_and_span(KernelFunction)
93		-> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,Span,WF]
94		; expects_waitflag(KernelFunction)
95		-> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,WF]
96		; expects_waitflag_and_type(KernelFunction)
97		-> KernelCall =.. [KernelFunction,ESV1,ESV2,Value,Type,WF]
98		; KernelCall =.. [KernelFunction,ESV1,ESV2,Value]
99		),
100		special_propagate_binary_function(KernelFunction,ESV1,ESV2,Value,WF),
101		must_succ_kernel_call(Module:KernelCall,(ESV1,ESV2),WF,Expr).
102
103		% calls for El : BOP(SV1,SV2) where BOP is a binary operator
104		binary_in_kernel_call(Module,Kernel_predicate,ElValue,SV1,SV2,WF,_Expr) :-
105		get_wait_flag0(WF,WF0),
106		binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0).
107
108		:- block binary_in_kernel_call2(?,?,-,?,?,?,-). % wait until either WF0 set or ElValue
109		binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0) :- nonvar(WF0),!,
110		call(Module:Kernel_predicate,ElValue,SV1,SV2,WF).
111		binary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0) :-
112		not_symbolic_when_var(ElValue,WF0,EWait),
113		% ensure that we do not call this in case ElValue is a closure which may need expanding
114		binary_in_kernel_call3(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0,EWait).
115
116		:- block binary_in_kernel_call3(?,?,?,?,?,?,-,-).
117		binary_in_kernel_call3(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0,_EWait) :- nonvar(WF0),!,
118		call(Module:Kernel_predicate,ElValue,SV1,SV2,WF).
119		binary_in_kernel_call3(Module,Kernel_predicate,ElValue,SV1,SV2,WF,WF0,EWait) :-
120		ground_value_check(SV1,G1),
121		ground_value_check(SV2,G2),
122		% when((nonvar(WF0) ; ground(EWait), nonvar(G1), nonvar(G2)),
123		call_nv4(Module:Kernel_predicate,ElValue,SV1,SV2,WF, WF0,EWait,G1,G2).
124
125		% wait for either WF0 or all others
126		:- block call_nv4(?,?,?,?,?,-,?,?,-),call_nv4(?,?,?,?,?,-,?,-,?),call_nv4(?,?,?,?,?,-,-,?,?).
127		call_nv4(Call,A,B,C,D,_WF0,_,_G1,_G2) :-
128		call(Call,A,B,C,D).
129
130		% trigger WaitVariable before WF0 when first arg is not a symbolic closure and becomes ground
131		:- block not_symbolic_when_var(-,-,?).
132		not_symbolic_when_var(_,WF0,_) :- nonvar(WF0),!. % WV not required
133		not_symbolic_when_var(closure(_,_,_),_,_) :- !.
134		not_symbolic_when_var(X,WF0,WV) :-
135		% initially used: value_variables(X,WV). %
136		ground_value_opt_check(X,WF0,WV).
137		% using ground_value_check instead of ground_value_opt_check means that co-routines can remain attached,
138		% which means things like enumeration_only_fdvar will fail and lead to issues in tests 1924, 1925, 1492
139
140		unary_in_kernel_call(Module,Kernel_predicate,ElValue,SV1,WF,_Expr) :-
141		%KernelCall =.. [Kernel_predicate,ElValue,SV1,WF],
142		%kernel_call(Module:KernelCall,(ElValue,SV1),WF,Expr).
143		get_wait_flag0(WF,WF0),
144		unary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,WF,WF0).
145
146		:- block unary_in_kernel_call2(?,?,-,?,?,-). % wait until either WF0 set or ElValue
147		unary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,WF,WF0) :- nonvar(WF0),!,
148		call(Module:Kernel_predicate,ElValue,SV1,WF).
149		unary_in_kernel_call2(Module,Kernel_predicate,ElValue,SV1,WF,WF0) :-
150		not_symbolic_when_var(ElValue,WF0,EWait),
151		% ensure that we do not call this in case ElValue is a closure which may need expanding;
152		% then we should at least wait until WF0 is ground
153		ground_value_opt_check(SV1,WF0,G1),
154		call_nv3(Module:Kernel_predicate,ElValue,SV1,WF,WF0,EWait,G1).
155
156		% wait for either WF0 or all others
157		:- block call_nv3(?,?,?,?,-,?,-),call_nv3(?,?,?,?,-,-,?).
158		call_nv3(Call,A,B,C,_WF0,_,_) :-
159		call(Call,A,B,C).
160
161		%must_succ_kernel_call(kernel_objects:equal_object_optimized(A,B),(A1,A2),WF,Expr) :- !,
162		% Call = kernel_objects:equal_object_optimized(A,B),
163		% kernel_call_or(Call,A1,A2,WF,Expr).
164		must_succ_kernel_call(Call,HasToBeGround,WF,_Expr) :-
165	?	get_wait_flag0(WF,WF0),
166		(nonvar(WF0)
167		-> call(Call)
168		; %hit_profiler:add_profile_hit(must_succ_kernel_call(Call,WF0),3),
169		%ground_value_check(HasToBeGround,G1), % using this made test 1562 fail; probably because co-routines remain active after WF0 has been set, leading un bound variables preventing optimisations in kernel_objects
170		ground_value_opt_check(HasToBeGround,WF0,VG1),
171		call_nv(Call,WF0,VG1)
172		).
173
174		%:- block must_succ_kernel_call2(?,-,-).
175		%must_succ_kernel_call2(Call,_,_) :- call(Call).
176
177
178		kernel_call_predicate(equal_object_optimized(A,B),kernel_objects,WF,_) :- !,
179		get_wait_flag0(WF,WF0),
180		equal_obj(A,B,WF0,WF).
181		% equality is the only predicate that can generate AVL trees
182		% OTHER CALLS: partition_wf, member of empty set or singleton set, CLPFD operators: TO DO add
183
184		kernel_call_predicate(not_equal_object_wf(A,B,WF),kernel_objects,WF,Expr) :- !,
185		get_wait_flag0(WF,WF0),not_eq_wf(A,B,WF,WF0,Expr).
186		kernel_call_predicate(partition_wf(A,B,PWF),kernel_objects,WF,Expr) :- !,
187		(nonvar(B),B=[B1|T],T==[] % just one set
188		-> kernel_call_predicate(equal_object_optimized(A,B1),kernel_objects,WF,Expr)
189		; all_but_one_set_known([A|B],Known),
190		kernel_call(kernel_objects:partition_wf(A,B,PWF),Known,WF,Expr)).
191		kernel_call_predicate(less_than(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than(A,B).
192		kernel_call_predicate(less_than_equal(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than_equal(A,B).
193		kernel_call_predicate(greater_than(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than(B,A).
194		kernel_call_predicate(greater_than_equal(A,B),kernel_objects,_WF,_Expr) :- !, kernel_objects:less_than_equal(B,A).
195		kernel_call_predicate(check_element_of_wf(A,B,PWF),kernel_objects,WF,Expr) :- !,
196		get_wait_flag0(WF,WF0), check_element_of_wf0(A,B,PWF,WF0,Expr).
197		kernel_call_predicate(is_natural(A,WF),kernel_objects,WF,_Expr) :- !, kernel_objects:is_natural(A,WF). % see test 2092
198		kernel_call_predicate(is_natural1(A,WF),kernel_objects,WF,_Expr) :- !, kernel_objects:is_natural1(A,WF).
199		kernel_call_predicate(is_not_natural(A),kernel_objects,_WF,_Expr) :- !, kernel_objects:is_not_natural(A).
200		kernel_call_predicate(is_not_natural1(A),kernel_objects,_WF,_Expr) :- !, kernel_objects:is_not_natural1(A).
201		kernel_call_predicate(Call,Module,WF,_Expr) :- get_wait_flag0(WF,WF0),
202		%hit_profiler:add_profile_hit(kernel_call_predicate(Call,WF0),2),
203		call_wf0(Module:Call,WF0).
204		%kernel_call_predicate(Call,HasToBeGround,WF,Expr) :- kernel_call(Call,HasToBeGround,WF,Expr).
205
206		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
207		:- if(environ(prob_use_timer,true)).
208		:- block call_wf0(?,-).
209		call_wf0(X,_) :- debug:timer_call(X). %debug:watch(10,X).
210		:- else.
211		:- block call_wf0(?,-).
212		call_wf0(Call,_) :- call(Call).
213		:- endif.
214
215		% unfolded version of above (for efficiency):
216		kernel_call_predicate_equal_object_optimized(A,B,WF) :-
217		get_wait_flag0(WF,WF0),equal_obj(A,B,WF0,WF).
218		kernel_call_predicate_check_element_of_wf(A,B,WF,Span) :-
219		get_wait_flag0(WF,WF0), check_element_of_wf0(A,B,WF,WF0,Span).
220		kernel_call_predicate_not_equal_object(A,B,WF,Expr) :-
221		get_wait_flag0(WF,WF0),not_eq_wf(A,B,WF,WF0,Expr).
222		kernel_call_predicate_not_element_of_wf(A,B,WF) :-
223		get_wait_flag0(WF,WF0),not_element_of_wf0(A,B,WF,WF0).
224
225		:- block not_element_of_wf0(?,?,?,-).
226		not_element_of_wf0(ElemValue,SetValue,WF,_) :- kernel_objects:not_element_of_wf(ElemValue,SetValue,WF).
227
228		kernel_call_predicate3(KernelCall,Arg1,Arg2,Arg3,Module,WF,_Expression) :-
229		get_wait_flag0(WF,WF0),
230		call_wf0_3(Module:KernelCall,Arg1,Arg2,Arg3,WF,WF0).
231		:- block call_wf0_3(?, ?,?,?,?, -).
232		call_wf0_3(Call,A1,A2,A3,WF,_) :- call(Call,A1,A2,A3,WF).
233
234		kernel_call_predicate2(KernelCall,Arg1,Arg2,Module,WF,_Expression) :-
235		get_wait_flag0(WF,WF0),
236		call_wf0_2(Module:KernelCall,Arg1,Arg2,WF,WF0).
237		:- block call_wf0_2(?, ?,?,?, -).
238		call_wf0_2(Call,A1,A2,WF,_) :- call(Call,A1,A2,WF).
239
240		:- use_module(custom_explicit_sets,[singleton_set/2]).
241		:- block check_element_of_wf0(?,-,?,-,?).
242		check_element_of_wf0(A,B,WF,_WF0,_) :- var(B),!, % means nonvar(WF0)
243	?	kernel_objects:check_element_of_wf(A,B,WF).
244		check_element_of_wf0(_A,B,_WF,_,_) :- B=[],!,fail. % nothing can be element of empty set; CAN PREVENT WD-ERRORS from being detected !
245		check_element_of_wf0(A,B,WF,_WF0,_) :-
246		singleton_set(B,B1),!, /* also does var check */
247		equal_object_optimized_wf(A,B1,check_element_of_wf0,WF). %was equal_obj(A,B1,WF0) but as B1 is ground value will always call equal_object_optimized directly
248		% below B must be nonvar
249		check_element_of_wf0(A,global_set(GS),WF,_,Span) :- nonvar(A),
250		!, % be sure that we check something like int(-1) : NATURAL
251		%kernel_objects:check_element_of_wf(A,global_set(GS),WF).
252		kernel_objects:element_of_global_set_wf(A,GS,WF,Span). % Span for enumeration warnings
253		check_element_of_wf0(A,avl_set(AVL),WF,_,_) :- simple_ground_value(A),
254		!, % we can already check this efficiently in phase 0
255		custom_explicit_sets:element_of_avl_set_wf(AVL,A,WF). % we could even call avl_fetch directly
256		% kernel_objects:check_element_of_wf(A,avl_set(AVL),WF).
257		check_element_of_wf0(A,B,WF,WF0,Span) :-
258	?	check_element_of_wf0_aux(A,B,WF,WF0,Span).
259		:- block check_element_of_wf0_aux(?,?,?,-,?).
260		check_element_of_wf0_aux(A,global_set(GS),WF,_WF0,Span) :- !,
261		kernel_objects:element_of_global_set_wf(A,GS,WF,Span). % Span for enumeration warnings
262		check_element_of_wf0_aux(A,avl_set(AVL),_WF,_WF0,b(EE,TT,Span)) :-
263		member(prob_annotation('ENUM'),Span),!, % force early enumeration via 'ENUM' external function annotation
264		(debug:debug_mode(on) -> add_message(enum,'Early enumeration of: ',b(EE,TT,Span),Span) ; true),
265		custom_explicit_sets:safe_avl_member(A,AVL). % TO DO: use avl_fetch if A known? + cover ENUM annotation also if set is known later
266	?	check_element_of_wf0_aux(A,B,WF,_WF0,_Span) :- kernel_objects:check_element_of_wf(A,B,WF).
267
268		simple_ground_value(A) :- nonvar(A), simple_ground_value_aux(A).
269		simple_ground_value_aux(int(X)) :- number(X).
270		simple_ground_value_aux(fd(X,_)) :- number(X).
271		simple_ground_value_aux(string(S)) :- ground(S).
272		simple_ground_value_aux((A,B)) :- simple_ground_value(A), simple_ground_value(B).
273		simple_ground_value_aux(rec(F)) :- simple_ground_fields(F).
274		simple_ground_value_aux([]).
275
276		simple_ground_fields(Var) :- var(Var),!,fail. % TO DO: we could activate check as soon as it becomes ground
277		simple_ground_fields([]).
278		simple_ground_fields([field(N,V)|T]) :- nonvar(N),simple_ground_value(V),simple_ground_fields(T).
279
280		:- assert_must_succeed( kernel_mappings:not_eq_wf(int(1),int(2),_,_,_) ).
281		:- assert_must_succeed( kernel_mappings:not_eq_wf([int(1)],[int(2)],_,0,_) ).
282		:- block not_eq_wf(-,?,?,-,?), not_eq_wf(?,-,?,-,?).
283		not_eq_wf(A,B,WF,_,_) :- efficient_value(A),efficient_value(B),!, %tools_printing:print_term_summary(not_eq_wf(A,B)),
284		kernel_objects:not_equal_object_wf(A,B,WF).
285		not_eq_wf(A,B,WF,WF0,Expr) :- not_eq_wf0(A,B,WF,WF0,Expr).
286		:- block not_eq_wf0(?,?,?,-,?).
287		not_eq_wf0(A,B,WF,_,_Expr) :-
288		%((var(A),var(B)) -> instantiate_argument(Expr,A) ; true),
289		kernel_objects:not_equal_object_wf(A,B,WF).
290
291		/* not required anymore ?!
292		% instantiate argument according to type of expression to ensure not_equal_object (or other calls) are triggered and do not wait setting up dif constraints
293		instantiate_argument(not_equal(AE,_),A) :-
294		bsyntaxtree:get_texpr_type(AE,Type),!, print(instantiate(Type,A)),nl,
295		instantiate_arg(Type,A).
296		instantiate_argument(_,_).
297
298		instantiate_arg(string,R) :- !, R=string(_).
299		instantiate_arg(integer,R) :- !, R=int(_).
300		% missing: more cases global(G),.... ?
301		instantiate_arg(_,_).
302		*/
303
304		% check whether disequality can be efficiently checked (already in WF0 phase)
305		efficient_value(X) :- var(X),!,fail.
306		efficient_value(int(_)).
307		efficient_value(avl_set(_)).
308		efficient_value([]).
309		efficient_value(fd(_,_)).
310		efficient_value(string(_)).
311		efficient_value((A,B)) :- nonvar(A),nonvar(B),efficient_value(A), efficient_value(B).
312		efficient_value(pred_true). efficient_value(pred_false).
313		efficient_value(term(_)). % will usually be floating: :- nonvar(X),X=floating(_).
314
315
316
317		%:- meta_predicate kernel_call(0,*,*,*).
318		kernel_call(Call,HasToBeGround,WF,_Expr) :-
319		get_wait_flag0(WF,WF0),
320		%hit_profiler:add_profile_hit(kernel_call(Call,WF),2),
321		%print(kc(WF0,Call)),nl,
322		(nonvar(WF0)
323		-> call(Call)
324		; ground_value_opt_check(HasToBeGround,WF0,G1),
325		call_nv(Call,WF0,G1)
326		).
327
328		:- block call_nv(?,-,-).
329		call_nv(Call,_,_) :-
330		% ( (var(WF0) -> print('enter :'),tools_printing:print_term_summary(Call) ; true),
331	?	call(Call).
332
333		% optimized custom versions of kernel_call for performacne:
334		:- use_module(bsets_clp,[apply_to/6]).
335		kernel_call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF) :-
336		%hit_profiler:add_profile_hit(kernel_call_apply_to(FValue,ArgValue,Res,WF)),
337		get_wait_flag0(WF,WF0),
338		(var(WF0) %(var(WF0), \+ ground(ArgValue), \+ ground(FValue))
339		-> ground_value_check((FValue,ArgValue),WF1), % often FValue is an avl_set, avoid pending co-routines later by checking it first for groundness
340		call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF,WF0,WF1)
341		; apply_to(FValue,ArgValue,Res,FunctionType,Span,WF)
342		).
343		% TO DO: maybe transmit Type information for using with element/3
344
345		:- block call_apply_to(?,?,?,?,?,?,-,-).
346		call_apply_to(FValue,ArgValue,Res,FunctionType,Span,WF,_,_Gr) :-
347		%discard_ground_value_check(Gr),
348		bsets_clp:apply_to(FValue,ArgValue,Res,FunctionType,Span,WF).
349
350
351		/* ------------------------------- */
352
353		:- use_module(kernel_objects,[equal_object_optimized_wf/4]).
354		:- block equal_obj(-,-,-,?).
355
356		equal_obj(A,B,WF0,WF) :- nonvar(WF0),!,
357		equal_object_optimized_wf(A,B,equal_obj1,WF).
358		equal_obj(A,B,WF0,WF) :- %hit_profiler:add_profile_hit(eq(A,B)),
359		non_simple_ground_value_check(A,VA),
360		(nonvar(VA) -> equal_object_optimized_wf(A,B,equal_obj2,WF)
361		; non_simple_ground_value_check(B,VB),
362		(nonvar(VB) -> equal_object_optimized_wf(A,B,equal_obj3,WF)
363		; equal_obj_block(A,B,WF,WF0,VA,VB)
364		)
365		).
366		:- block equal_obj_block(?,?,?,-,-,-).
367		equal_obj_block(A,B,WF,_,_,_) :-
368		equal_object_optimized_wf(A,B,equal_obj4,WF).
369
370		% a version of ground_value_check that also returns [] in some cases where there is a variable but equal_object can be called
371		non_simple_ground_value_check(V,Vars) :- var(V),!, Vars=[V].
372		non_simple_ground_value_check(pred_false,Vars) :- !, Vars=[].
373		non_simple_ground_value_check(pred_true,Vars) :- !, Vars=[].
374		non_simple_ground_value_check(int(_),Vars) :- !, Vars=[]. % may contain var; but we can unify nonetheless
375		non_simple_ground_value_check(string(_),Vars) :- !, Vars=[]. % ditto
376		non_simple_ground_value_check(fd(_,_),Vars) :- !, Vars=[]. % ditto
377		non_simple_ground_value_check(A,Vars) :- !, ground_value_check(A,Vars).
378
379
380
381		% used for reversible calls: if one argument is ground we can evaluate the call and compute the other one
382		kernel_call_or(Call,HasToBeGround1,HasToBeGround2,WF,_Expr) :-
383		get_wait_flag0(WF,WF0),
384		(nonvar(WF0) -> call(Call)
385		; ground_value_check(HasToBeGround1,G1),
386		(nonvar(G1) -> call(Call)
387		; ground_value_check(HasToBeGround2,G2),
388		%hit_profiler:add_profile_hit(kernel_call_or(Call,WF0),2),
389		call_nv_or3(Call,WF0,G1,G2)
390		)
391		).
392
393		:- block call_nv_or3(?,-,-,-).
394		call_nv_or3(Call,_,_,_) :-
395		call(Call).
396
397
398		% special case for calling binary integer functions: here we can use more efficient block declarations
399		call_determined_integer_function(KF,V1,V2,Val,WF0,WF,Span) :-
400		determined(V1,V2,Val,Determined,WF0),
401		call_determined_integer_function2(KF,V1,V2,Val,WF0,Determined,WF,Span).
402		:- block call_determined_integer_function2(?,?,?,?,-,-,?,?).
403		%call_determined_integer_function2(KF,V1,V2,V,WF0,Det,_,_) :-
404		% print(kernel_det_call(KF,V1,V2,V,WF0,Det)),nl,fail.
405		call_determined_integer_function2(division,V1,V2,Val,_,_,WF,Span) :-
406		kernel_objects:division(V1,V2,Val,Span,WF).
407		call_determined_integer_function2(floored_division,V1,V2,Val,_,_,WF,Span) :-
408		kernel_objects:floored_division(V1,V2,Val,Span,WF).
409		call_determined_integer_function2(int_minus,V1,V2,Val,_,_,_WF,_Span) :-
410		kernel_objects:int_minus(V1,V2,Val).
411		call_determined_integer_function2(int_plus,V1,V2,Val,_,_,_WF,_Span) :-
412		% kernel_call_determined(kernel_objects:int_plus(V1,V2,Val),V1,V2,Val,WF,integer).
413		kernel_objects:int_plus(V1,V2,Val).
414		call_determined_integer_function2(int_power,V1,V2,Val,_,_,WF,Span) :-
415		kernel_objects:int_power(V1,V2,Val,Span,WF).
416		call_determined_integer_function2(modulo,V1,V2,Val,_,_,WF,Span) :-
417		kernel_objects:modulo(V1,V2,Val,Span,WF).
418		call_determined_integer_function2(times,V1,V2,Val,_,_,_WF,_Span) :-
419		kernel_objects:times(V1,V2,Val).
420
421		% sets last argument to determined without instantiating its first three args
422		% it is set when two integer values are known
423		:- block determined(-,-,?,?,-), determined(-,?,-,?,-), determined(?,-,-,?,-).
424		%:- block determined(-,-,?,?,?), determined(-,?,-,?,?), determined(?,-,-,?,?).
425		%determined(Y,V,X,Det,WF0) :- print(determined(Y,V,X,Det,WF0)),nl,fail.
426		determined(_X,_Y,_Z,Det,WF0) :- nonvar(WF0),!,Det=determined.
427		% ((nonvar(_X),nonvar(_Y), \+ ground(_Y), var(_V)) -> trace ; true).
428		determined(X,Y,V,Det,_) :- var(X),!, Y=int(YY),V=int(VV), %(YY=0 -> X=V ; true),
429		determined2(X,YY,VV,Det).
430		determined(Y,X,V,Det,_) :- var(X),!, Y=int(YY),V=int(VV), %(YY=0 -> X=V ; true),
431		determined2(X,YY,VV,Det).
432		determined(Y,V,X,Det,_) :- Y=int(YY),V=int(VV), %(YY=0 -> X=V ; VV=0 -> X=Y),
433		determined2(X,YY,VV,Det).
434		:- block determined2(-,-,?,?), determined2(-,?,-,?), determined2(?,-,-,?).
435		%determined2(Y,V,X,Det) :- print(determined2(Y,V,X,Det)),nl,fail.
436		determined2(X,_,_,Det) :- var(X),!,Det=determined.
437		determined2(int(XX),YY,VV,Det) :- determined3(XX,YY,VV,Det).
438		:- block determined3(-,-,?,?), determined3(-,?,-,?), determined3(?,-,-,?).
439		%determined3(Y,V,X,Det) :- print(determined3(Y,V,X,Det)),nl,fail.
440		determined3(_,_,_,determined).
441
442
443
444
445		:- use_module(error_manager).
446
447	?	invalid_call(X) :- \+ check_valid_kernel_call(X,_).
448	?	check_valid_kernel_call(X,unary) :- unary_function(_,_,X).
449	?	check_valid_kernel_call(X,binary) :- binary_function(_,_,X).
450		check_valid_kernel_call(X,_) :- add_error(check_valid_kernel_call,'Illegal Kernel Call: ',X),fail.
451		:- assert_must_fail((kernel_mappings:expects_waitflag_and_span(X),
452		kernel_mappings:invalid_call(X))).
453
454		expects_waitflag_and_span(first_sequence).
455		expects_waitflag_and_span(last_sequence).
456		expects_waitflag_and_span(tail_sequence).
457		expects_waitflag_and_span(front_sequence).
458		expects_waitflag_and_span(minimum_of_set).
459		expects_waitflag_and_span(maximum_of_set).
460		expects_waitflag_and_span(intersection_generalized_wf).
461
462		expects_waitflag_and_span(division).
463		expects_waitflag_and_span(floored_division).
464		expects_waitflag_and_span(modulo).
465		expects_waitflag_and_span(int_power).
466		expects_waitflag_and_span(real_power_of_wf).
467		expects_waitflag_and_span(singleton_set_element).
468		expects_waitflag_and_span(real_division_wf).
469		expects_waitflag_and_span(real_maximum_of_set).
470		expects_waitflag_and_span(real_minimum_of_set).
471
472		:- assert_must_fail((kernel_mappings:expects_waitflag(X),
473		kernel_mappings:invalid_call(X))).
474		:- assert_must_fail((kernel_mappings:expects_waitflag(X),
475		kernel_mappings:expects_waitflag_and_span(X))).
476		/*
477		comment in if we want to ensure that all kernel predicates take at least the WF
478		:- assert_must_fail((kernel_mappings:unary_function(_,_,X),
479		\+ (kernel_mappings:expects_waitflag(X) ;
480		kernel_mappings:expects_waitflag_and_span(X)),
481		print(unary_no_waitflag(X)),nl )).
482		:- assert_must_fail((kernel_mappings:binary_function(_,_,X),
483		\+ (kernel_mappings:expects_waitflag(X) ;
484		kernel_mappings:expects_waitflag_and_span(X)),
485		print(binary_no_waitflag(X)),nl )).
486		*/
487
488		expects_waitflag(append_sequence).
489		expects_waitflag(bag_items).
490		expects_waitflag(cartesian_product_wf).
491		expects_waitflag(compaction).
492		expects_waitflag(concat_sequence).
493		expects_waitflag(concatentation_of_sequences).
494		expects_waitflag(difference_set_wf).
495		expects_waitflag(direct_product_wf).
496		expects_waitflag(parallel_product_wf).
497		expects_waitflag(domain_restriction_wf).
498		expects_waitflag(domain_subtraction_wf).
499		expects_waitflag(domain_wf).
500		expects_waitflag(finite_cardinality_as_int_wf).
501		expects_waitflag(identity_relation_over_wf).
502		expects_waitflag(image_wf).
503		expects_waitflag(intersection).
504		expects_waitflag(invert_relation_wf).
505		expects_waitflag(relational_trans_closure_wf).
506		expects_waitflag(override_relation).
507		expects_waitflag(prefix_sequence_wf).
508		expects_waitflag(prepend_sequence).
509		expects_waitflag(range_restriction_wf).
510		expects_waitflag(range_subtraction_wf).
511		expects_waitflag(range_wf).
512		expects_waitflag(real_addition_wf).
513		%expects_waitflag(real_division_wf).
514		expects_waitflag(real_multiplication_wf).
515		expects_waitflag(real_subtraction_wf).
516		expects_waitflag(real_unary_minus_wf).
517		%expects_waitflag(rel_composition_wf).
518		%expects_waitflag(rel_iterate_wf).
519		expects_waitflag(rev_sequence).
520		expects_waitflag(size_of_sequence).
521		expects_waitflag(square).
522		expects_waitflag(suffix_sequence).
523		expects_waitflag(unary_minus_wf).
524		expects_waitflag(union_generalized_wf).
525		expects_waitflag(union_wf).
526
527		expects_waitflag_and_type(rel_iterate_wf).
528		expects_waitflag_and_type(rel_composition_wf).
529
530		:- use_module(bsyntaxtree,[get_texpr_set_type/2]).
531		% only used when not in CLPFD mode:
532		special_binary_predicate(greater(b(card(X),integer,_),Y), kernel_objects:cardinality_greater,X,TypeX,Y,integer) :-
533		get_texpr_set_type(X,TypeX).
534		special_binary_predicate(less(Y,b(card(X),integer,_)), kernel_objects:cardinality_greater,X,TypeX,Y,integer) :-
535		get_texpr_set_type(X,TypeX).
536		special_binary_predicate(greater_equal(b(card(X),integer,_),Y), kernel_objects:cardinality_greater_equal,X,TypeX,Y,integer) :-
537		get_texpr_set_type(X,TypeX).
538		special_binary_predicate(less_equal(Y,b(card(X),integer,_)), kernel_objects:cardinality_greater_equal,X,TypeX,Y,integer) :-
539		get_texpr_set_type(X,TypeX).
540
541
542
543		/* EXPRESSIONS */
544
545
546		:- assert_must_fail((kernel_mappings:reversible_unary_function(X),
547		kernel_mappings:invalid_call(X))).
548
549		reversible_unary_function(invert_relation_wf).
550		reversible_unary_function(rev_sequence).
551		reversible_unary_function(unary_minus_wf).
552
553		unary_function(reverse,bsets_clp,invert_relation_wf).
554		unary_function(closure,bsets_clp,relational_trans_closure_wf). % this is closure1
555		%unary_function(reflexive_closure,bsets_clp,relational_reflexive_closure). % now done in ast_cleanup
556		unary_function(domain,bsets_clp,domain_wf).
557		unary_function(range,bsets_clp,range_wf).
558
559		unary_function(general_union,kernel_objects,union_generalized_wf).
560		unary_function(general_intersection,kernel_objects,intersection_generalized_wf).
561
562		unary_function(first,bsets_clp,first_sequence).
563		unary_function(size,bsets_clp,size_of_sequence).
564		unary_function(front,bsets_clp,front_sequence).
565		unary_function(tail,bsets_clp,tail_sequence).
566		unary_function(rev,bsets_clp,rev_sequence).
567		unary_function(last,bsets_clp,last_sequence).
568
569		unary_function(card,kernel_cardinality_attr,finite_cardinality_as_int_wf).
570		unary_function(pow_subset,kernel_objects,power_set). % not really necessary anymore,
571		% because of symbolic_closure_unary_operator treatment,
572		% except for empty set and singleton sets (see do_not_keep_symbolic_unary)
573		unary_function(fin_subset,kernel_objects,power_set). % not really necessary anymore, ditto
574		unary_function(pow1_subset,kernel_objects,non_empty_power_set). % not really necessary anymore
575		unary_function(fin1_subset,kernel_objects,non_empty_power_set). % not really necessary anymore
576		unary_function(identity,bsets_clp,identity_relation_over_wf).
577		%unary_function(perm,bsets_clp,enumerate_permutation_sequence).
578		% unary_function(iseq,bsets_clp,enumerate_injective_sequence).
579		%unary_function(iseq1,bsets_clp,enumerate_non_empty_injective_sequence).
580		%unary_function(seq,bsets_clp,enumerate_sequence).
581		%unary_function(seq1,bsets_clp,enumerate_non_empty_sequence).
582		%unary_function(struct,kernel_records,enumerate_records).
583
584		unary_function(general_concat,bsets_clp,concatentation_of_sequences). % conc operator, mapped to STRING_CONC for strings
585		unary_function(unary_minus,kernel_objects,unary_minus_wf).
586		unary_function(unary_minus_real,kernel_reals,real_unary_minus_wf).
587		unary_function(square_multiplication,kernel_objects,square). % artificial construct, detected when X*X is evaluated by interpreter; but square is directly called
588		unary_function(max,kernel_objects,maximum_of_set).
589		unary_function(max_real,kernel_reals,real_maximum_of_set).
590		unary_function(min,kernel_objects,minimum_of_set).
591		unary_function(min_real,kernel_reals,real_minimum_of_set).
592
593		unary_function(first_of_pair,kernel_objects,first_of_pair). % prj1 for full types
594		unary_function(second_of_pair,kernel_objects,second_of_pair). % prj2 for full types
595		unary_function(mu,kernel_objects,singleton_set_element). % Z MU operator
596
597		unary_function(compaction,kernel_z,compaction).
598		unary_function(bag_items,kernel_z,bag_items).
599
600		unary_function(convert_real,kernel_reals,convert_int_to_real).
601		unary_function(convert_int_floor,kernel_reals,real_floor).
602		unary_function(convert_int_ceiling,kernel_reals,real_ceiling).
603
604
605		:- assert_must_fail((kernel_mappings:determined_binary_integer_function(X),
606		kernel_mappings:invalid_call(X))).
607		/* binary functions where 1 argument is determined from the other two */
608		determined_binary_integer_function(division). % isn't really determined X / 10 = 2 --> many possible values
609		determined_binary_integer_function(int_minus).
610		determined_binary_integer_function(int_plus).
611		determined_binary_integer_function(int_power).
612		determined_binary_integer_function(modulo). % isn't really determined; X mod 10 = 0 --> many possible values
613		determined_binary_integer_function(times).
614
615		%:- assert_must_fail((kernel_mappings:determined_binary_function(X),
616		% kernel_mappings:invalid_call(X))).
617		%determined_binary_function(nat_range).
618		%determined_binary_function(concat_sequence).
619		%determined_binary_function(prepend_sequence).
620		%determined_binary_function(cartesian_product).
621
622		% set up any special propagation rules which should trigger before Args1 and 2 are fully known:
623		% we should probably move these rules down to kernel_objects, bsets_clp ... and validate them
624		% maybe we can even store them in B format, prove them and read them in
625		special_propagate_binary_function(union_wf,A,B,Res,WF) :- !,
626		propagate_empty_set(Res,A,WF), % A\/B ={} => A={}
627		propagate_empty_set(Res,B,WF). % A\/B ={} => B={}
628		special_propagate_binary_function(override_relation,A,B,Res,WF) :- !, % used causes small slowdown for ticket 184??
629		propagate_empty_set(Res,A,WF), % A<+B ={} => A={}
630		propagate_empty_set(Res,B,WF), % A<+B ={} => B={}
631		propagate_empty_set_eq(A,B,Res,WF), % if A ={} => A <+ B = B
632		propagate_empty_set_eq(B,A,Res,WF). % if B ={} => A <+ B = A
633		special_propagate_binary_function(intersection,A,B,Res,WF) :- !,
634		propagate_empty_set(A,Res,WF), % A={} => A /\ B = {}
635		propagate_empty_set(B,Res,WF). % B={} => A /\ B = {}
636		special_propagate_binary_function(difference_set_wf,A,B,Res,WF) :- !,
637		propagate_empty_set(A,Res,WF), % A={} => A \ B = {}
638		propagate_empty_set_eq(B,A,Res,WF). % B={} => A \ B = A
639		special_propagate_binary_function(image_wf,A,B,Res,WF) :- !,
640		propagate_empty_set(B,Res,WF), % B={} => A[B] = {}
641		propagate_id_eq(A,B,Res,WF). % (A={} => A[B] = {}) & (A=id => A[B] = B)
642		special_propagate_binary_function(domain_restriction_wf,S,_R,Res,WF) :- !,
643		propagate_empty_set(S,Res,WF). % if S ={} => S <| R = {}
644		special_propagate_binary_function(domain_subtraction_wf,S,R,Res,WF) :- !,
645		propagate_empty_set_eq(S,R,Res,WF). % if S ={} => S <<| R = R
646		special_propagate_binary_function(range_restriction_wf,_R,S,Res,WF) :- !,
647		propagate_empty_set(S,Res,WF). % if S ={} => R |> S = {}
648		special_propagate_binary_function(range_subtraction_wf,R,S,Res,WF) :- !,
649		propagate_empty_set_eq(S,R,Res,WF). % if S ={} => R |>> S = R
650		special_propagate_binary_function(composition,A,B,Res,WF) :- !,
651		propagate_empty_set(A,Res,WF), % A={} => (A ; B) = {}
652		propagate_empty_set(B,Res,WF). % B={} => (A ; B) = {}
653		special_propagate_binary_function(_,_,_,_,_WF). % no propagators available
654		:- block propagate_empty_set(-,?,?).
655		propagate_empty_set([],A,WF) :- !,
656		% (A==[] -> true ; print(prop_empty(A)),nl), %%
657		kernel_objects:empty_set_wf(A,WF).
658		propagate_empty_set(_,_,_).
659		:- block propagate_empty_set_eq(-,?,?,?).
660		propagate_empty_set_eq([],A,B,WF) :- !,kernel_objects:equal_object_wf(A,B,propagate_empty_set_eq,WF).
661		propagate_empty_set_eq(_,_,_,_).
662		:- block propagate_id_eq(-,?,?,?).
663		propagate_id_eq([],_A,B,WF) :- !,kernel_objects:empty_set_wf(B,WF).
664		propagate_id_eq(closure(Par,Types,Body),A,B,WF) :- custom_explicit_sets:is_full_id_closure(Par,Types,Body),
665		% print(prop_id_eq(A,B)),nl,
666		!,kernel_objects:equal_object_wf(A,B,propagate_id_eq,WF).
667		propagate_id_eq(_,_,_,_).
668
669		binary_function(concat,bsets_clp,concat_sequence). % ^
670		binary_function(insert_front,bsets_clp,prepend_sequence).
671		binary_function(insert_tail,bsets_clp,append_sequence).
672		binary_function(restrict_front,bsets_clp,prefix_sequence_wf). % s /|\ n
673		binary_function(restrict_tail,bsets_clp,suffix_sequence). % WF
674		binary_function(union,kernel_objects,union_wf).
675		binary_function(intersection,kernel_objects,intersection).
676		binary_function(set_subtraction,kernel_objects,difference_set_wf).
677		binary_function(cartesian_product,kernel_objects,cartesian_product_wf). % always converted into closure
678		binary_function(add,kernel_objects,int_plus).
679		binary_function(add_real,kernel_reals,real_addition_wf).
680		binary_function(multiplication,kernel_objects,times).
681		binary_function(multiplication_real,kernel_reals,real_multiplication_wf).
682		binary_function(minus,kernel_objects,int_minus).
683		binary_function(minus_real,kernel_reals,real_subtraction_wf).
684		binary_function(modulo,kernel_objects,modulo).
685		binary_function(power_of,kernel_objects,int_power).
686		binary_function(power_of_real,kernel_reals,real_power_of_wf).
687		binary_function(div,kernel_objects,division).
688		binary_function(div_real,kernel_reals,real_division_wf).
689		binary_function(floored_div,kernel_objects,floored_division).
690		%binary_function(interval,kernel_objects,nat_range). % always converted into closure, unless empty or singleton
691		binary_function(image,bsets_clp,image_wf).
692		%binary_function(function,apply_to).
693		binary_function(domain_restriction,bsets_clp,domain_restriction_wf).
694		binary_function(domain_subtraction,bsets_clp,domain_subtraction_wf).
695		binary_function(range_subtraction,bsets_clp,range_subtraction_wf).
696		binary_function(range_restriction,bsets_clp,range_restriction_wf).
697		binary_function(overwrite,bsets_clp,override_relation).
698		binary_function(composition,bsets_clp,rel_composition_wf).
699		binary_function(iteration,bsets_clp,rel_iterate_wf).
700		binary_function(direct_product,bsets_clp,direct_product_wf).
701		binary_function(parallel_product,bsets_clp,parallel_product_wf).
702		% functions below always converted into closure
703		%binary_function(total_function,bsets_clp,enumerate_total_function).
704		%binary_function(partial_function,bsets_clp,enumerate_partial_function).
705		%binary_function(total_bijection,bsets_clp,enumerate_total_bijection).
706		%binary_function(relations,bsets_clp,enumerate_relation).
707		%binary_function(partial_injection,bsets_clp,enumerate_partial_injection).
708		%binary_function(partial_surjection,bsets_clp,enumerate_partial_surjection).
709		%binary_function(total_surjection,bsets_clp,enumerate_total_surjection).
710		%binary_function(total_relation,bsets_clp,enumerate_total_relation).
711		%binary_function(total_injection,bsets_clp,enumerate_total_injection).
712		%binary_function(partial_bijection,bsets_clp,enumerate_partial_bijection).
713		%binary_function(surjection_relation,bsets_clp,enumerate_surjection_relation).
714		%binary_function(total_surjection_relation,bsets_clp,enumerate_total_surjection_relation).
715
716		% check if the first argument determines the value of a binary_function:
717		binary_arg1_determines_value(multiplication,A1,int(0)) :- zero(A1).
718		binary_arg1_determines_value(intersection,A1,[]) :- A1==[].
719		binary_arg1_determines_value(set_subtraction,A1,[]) :- A1==[].
720		binary_arg1_determines_value(domain_restriction,A1,[]) :- A1==[]. % first arg is set
721		binary_arg1_determines_value(range_subtraction,A1,[]) :- A1==[]. % first arg is rel
722		binary_arg1_determines_value(range_restriction,A1,[]) :- A1==[]. % first arg is rel
723		binary_arg1_determines_value(cartesian_product,A1,[]) :- A1==[].
724		binary_arg1_determines_value(composition,A1,[]) :- A1==[].
725		binary_arg1_determines_value(direct_product,A1,[]) :- A1==[].
726		binary_arg1_determines_value(parallel_product,A1,[]) :- A1==[].
727
728
729		zero(X) :- nonvar(X), X=int(X1),X1==0.
730
731		/* add PartialBijection .... */
732
733		/* BOOLEAN EXPRESSIONS */
734
735
736		:- assert_must_succeed(kernel_mappings:symbolic_closure_binary_operator(partial_function)).
737		:- assert_must_succeed(kernel_mappings:symbolic_closure_binary_operator(total_function)).
738
739		symbolic_closure_binary_operator(Op) :-
740		binary_in_boolean_type(Op,_),
741		binary_not_in_boolean_type(Op,_),
742		\+ not_symbolic_binary(Op).
743		/* note every symbolic closure operator must be dealt with by a binary_in and
744		a binary_not_in clause below, otherwise we have a problem */
745
746		%not_symbolic_binary(set_subtraction). % initially test 426 failed or runtime went from 6 to 12 secs ; now with do_not_keep_symbolic rules below it is fine and runtime is 3 secs
747		%not_symbolic_binary(intersection). % seems to be ok to allow symbolic treatment
748		not_symbolic_binary(range_subtraction). % important for test 1001
749		not_symbolic_binary(range_restriction).
750		not_symbolic_binary(domain_subtraction). % important for test 1001
751		not_symbolic_binary(domain_restriction).
752		not_symbolic_binary(composition). % for tests 525, 1001; there are quite a few rules to compute symbolic compositions
753		% TO DO: see if we can remove the need for symbolic composition rules and just rely on in_composition_wf
754		% this would also make this faster: 50 |-> res : ((f ; succ) ; succ)
755		% where we have defined :let f = {x,y|x:1..50 & y : 1..250 & (x+y) mod 2 = 0}
756		% currently 0 |-> res : (f ; (succ ; succ)) is fast (1 ms vs 21 ms)
757		/* interval symbolic: because we often have expressions of the form a..b where b is > MAXINT */
758
759		% return true if a symbolic closure for a binary operator would be definitely empty:
760		is_definitely_empty(interval,int(A),int(B)) :- number(A),number(B), A>B.
761		is_definitely_empty(cartesian_product,A,B) :- (B==[]->true ; A==[]). % A==[] actually already checked in binary_arg1_determines_value
762		is_definitely_empty(parallel_product,A,B) :- (A==[]->true ; B==[]).
763		is_definitely_empty(total_relation,A,B) :- B==[], definitely_not_empty(A).
764		is_definitely_empty(total_function,A,B) :- B==[], definitely_not_empty(A). % {} --> {} = {{}}
765		is_definitely_empty(total_injection,A,B) :- B==[], definitely_not_empty(A).
766		is_definitely_empty(total_surjection,A,B) :- B==[], definitely_not_empty(A).
767		is_definitely_empty(total_bijection,A,B) :- B==[], definitely_not_empty(A).
768		is_definitely_empty(intersection,A,B) :- (A==[] ; B==[]).
769		is_definitely_empty(set_subtraction,A,B) :-
770		(A==[] ; nonvar(B), custom_explicit_sets:is_definitely_maximal_set(B)).
771
772		:- use_module(kernel_freetypes,[is_non_empty_freetype/1]).
773		definitely_not_empty(X) :- nonvar(X), definitely_not_empty_aux(X).
774		definitely_not_empty_aux([_|_]).
775		definitely_not_empty_aux(avl_set(_)).
776		definitely_not_empty_aux(global_set(_)).
777		definitely_not_empty_aux(freetype(ID)) :- is_non_empty_freetype(ID).
778
779		% check if it is worthwhile keeping a binary operator symbolic, if so: return value
780		do_not_keep_symbolic(cartesian_product,Set1,Set2,Res,WF) :- %print(cart(Set1,Set2)),nl,
781		(singleton_set(Set1,_) -> small_known_set(Set2)
782		; singleton_set(Set2,_) -> small_known_set(Set1)
783		),
784		kernel_objects:cartesian_product_wf(Set1,Set2,Res,WF).
785		do_not_keep_symbolic(interval,int(A),int(B),Res,_WF) :-
786		(integer(A),nonvar(B),A=B % or B-A < some limit
787		-> custom_explicit_sets:convert_to_avl([int(A)],Res)).
788		do_not_keep_symbolic(parallel_product,Rel1,Rel2,Res,WF) :-
789		not_closure(Rel1), not_closure(Rel2),
790		bsets_clp:parallel_product_wf(Rel1,Rel2,Res,WF).
791		%do_not_keep_symbolic(overwrite,Rel1,Rel2,Res,WF) :-
792		% not_closure(Rel1), not_closure(Rel2),
793		% bsets_clp:override_relation(Rel1,Rel2,Res,WF).
794		do_not_keep_symbolic(intersection,Set1,Set2,Res,_WF) :- nonvar(Set1), nonvar(Set2),
795		% only keep symbolic if at least one non-interval closure
796		nonvar_non_interval_closure(Set1,Set2,R12),
797		(R12=1 ->
798		\+ small_known_set(Set2) % intersection with singleton set can always be computed
799		; R12=2 -> \+ small_known_set(Set1)),
800		!,
801		(same_closure(Set1,Set2) -> Res = Set1 % Set1 /\ Set1 = Set1
802		; %% print(symbolic_intersection),nl, translate:print_bvalue(Set1),nl, translate:print_bvalue(Set2),nl,nl, %%
803		fail).
804		do_not_keep_symbolic(intersection,Set1,Set2,Res,WF) :- % otherwise: compute intersection normally
805		Call=kernel_objects:intersection(Set1,Set2,Res,WF),
806		must_succ_kernel_call(Call,[Set1,Set2],WF,Call).
807		do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,_WF) :- Set2 == [],!,
808		Res = Set1.
809		do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,_WF) :- nonvar(Set1),
810		% only keep symbolic if at least one non-interval closure
811		nonvar_non_interval_closure(Set1,Set2,_),
812		% check if we cannot construct a complement closure:
813		\+ can_construct_complement_closure(Set1,Set2),
814		\+ small_known_set(Set1),
815		!,
816		(same_closure(Set1,Set2) -> Res = [] % Set \ Set = {}
817		; %nl,print(symbolic_set_subtr(Set1,Set2)),nl,nl, %%
818		fail).
819		do_not_keep_symbolic(set_subtraction,Set1,Set2,Res,WF) :- % otherwise: compute difference normally
820		Call=kernel_objects:difference_set_wf(Set1,Set2,Res,WF), % print(diff_set(Set1,Set2,Res)),nl,
821		must_succ_kernel_call(Call,[Set1,Set2],WF,Call).
822
823		% should succeed if we do not want to keep a unary operator symbolic
824		do_not_keep_symbolic_unary(_,ArgValue) :- ArgValue==[],!.
825		do_not_keep_symbolic_unary(closure,Set1) :- % this is closure1
826		very_small_known_avl_set(Set1).
827		do_not_keep_symbolic_unary(pow_subset,Set1) :- singleton_set(Set1,_).
828		do_not_keep_symbolic_unary(fin_subset,Set1) :- singleton_set(Set1,_).
829		do_not_keep_symbolic_unary(pow1_subset,Set1) :- singleton_set(Set1,_).
830		do_not_keep_symbolic_unary(fin1_subset,Set1) :- singleton_set(Set1,_).
831
832		can_construct_complement_closure(Set1,Set2) :-
833		nonvar(Set1), nonvar(Set2), Set2 = avl_set(_),
834		custom_explicit_sets:is_very_large_maximal_global_set(Set1,_).
835
836		nonvar_non_interval_closure(A,B,R) :- (nonvar_non_interval_closure(A) -> R=1 ; nonvar_non_interval_closure(B) -> R=2).
837		nonvar_non_interval_closure(A) :- nonvar(A), A=closure(_,_,_),
838		\+ custom_explicit_sets:is_interval_closure_or_integerset(A,_,_),
839		\+ custom_explicit_sets:is_not_member_value_closure(A,_Type,_MS2). % there isn't full support for this for intersection yet ! TODO fix
840
841		% happens quite often e.g. when expanding in state view
842		same_closure(X,Y) :- (var(X);var(Y)),!,fail.
843		same_closure(closure(P1,T1,B1),closure(P2,T2,B2)) :-
844		custom_explicit_sets:same_closure_body(P1,T1, B1, P2,T2,B2).
845
846		:- use_module(custom_explicit_sets,[quick_custom_explicit_set_approximate_size/2]).
847		small_known_set(AVL) :- nonvar(AVL), AVL=avl_set(A),!,
848		quick_custom_explicit_set_approximate_size(avl_set(A),Size),
849		Size < 150.
850		small_known_set(Closure) :- nonvar(Closure),
851		% also accept small intervals;
852		% useful e.g., for primes = {x | x>1 & ¬(∃y.(y>1 ∧ y<x ∧ x mod y=0))} ∧ res = primes /\ 1..50
853		custom_explicit_sets:is_interval_closure(Closure,From,To), integer(From), integer(To),
854		1+To-From < 150.
855
856		very_small_known_avl_set(AVL) :- nonvar(AVL), AVL=avl_set(A),
857		quick_custom_explicit_set_approximate_size(avl_set(A),Size),
858		Size < 50.
859
860		not_closure(X) :- nonvar(X), \+ functor(X,closure,3). %X \= closure(_,_,_).
861
862		% explicit_set([]). explicit_set([_|_]). explicit_set(avl_set(_)).
863
864		:- assert_must_fail((kernel_mappings:binary_in_boolean_type(Op,_),
865		\+(kernel_mappings:binary_not_in_boolean_type(Op,_)))).
866		:- assert_must_fail((kernel_mappings:binary_not_in_boolean_type(Op,_),
867		\+(kernel_mappings:binary_in_boolean_type(Op,_)))).
868		:- assert_must_fail((kernel_mappings:binary_in_boolean_type(Op,_), \+(kernel_mappings:binary_function(Op,_,_)),
869		kernel_mappings:not_symbolic_binary(Op) )).
870
871		binary_in_boolean_type(partial_function,bsets_clp:partial_function_wf).
872		binary_in_boolean_type(total_function,bsets_clp:total_function_wf).
873		binary_in_boolean_type(cartesian_product,kernel_objects:is_cartesian_pair_wf).
874		binary_in_boolean_type(partial_surjection,bsets_clp:partial_surjection_wf).
875		binary_in_boolean_type(partial_injection,bsets_clp:partial_injection_wf).
876		binary_in_boolean_type(total_injection,bsets_clp:total_injection_wf). % >->
877		binary_in_boolean_type(partial_bijection,bsets_clp:partial_bijection_wf).
878		binary_in_boolean_type(total_surjection,bsets_clp:total_surjection_wf). % -->>
879		binary_in_boolean_type(total_bijection,bsets_clp:total_bijection_wf). % >->>
880		binary_in_boolean_type(relations,bsets_clp:relation_over_wf).
881		binary_in_boolean_type(total_relation,bsets_clp:total_relation_wf).
882		binary_in_boolean_type(surjection_relation,bsets_clp:surjection_relation_wf).
883		binary_in_boolean_type(total_surjection_relation,bsets_clp:total_surjection_relation_wf).
884		binary_in_boolean_type(interval,kernel_objects:in_nat_range_wf).
885		binary_in_boolean_type(parallel_product,bsets_clp:in_parallel_product_wf).
886		binary_in_boolean_type(set_subtraction,kernel_objects:in_difference_set_wf).
887		binary_in_boolean_type(intersection,kernel_objects:in_intersection_set_wf).
888		%binary_in_boolean_type(union,bsets_clp:in_union_set_wf). % makes some CBC checks fail; TO DO: investigate
889		binary_in_boolean_type(range_subtraction,bsets_clp:in_range_subtraction_wf).
890		binary_in_boolean_type(range_restriction,bsets_clp:in_range_restriction_wf).
891		binary_in_boolean_type(domain_subtraction,bsets_clp:in_domain_subtraction_wf).
892		binary_in_boolean_type(domain_restriction,bsets_clp:in_domain_restriction_wf).
893		%binary_in_boolean_type(overwrite,bsets_clp:in_override_relation_wf). % TO DO: add this, for a more principled symbolic treatment (see test 1491)
894		binary_in_boolean_type(composition,bsets_clp:in_composition_wf).
895
896		% check whether a binary operator is definitely true; irrespective of arguments
897		binary_in_definitely_true(BOP,ValueOfEl) :- nonvar(ValueOfEl),
898		binary_definitely_true_based_on_element_value(BOP,ValueOfEl).
899
900		binary_definitely_true_based_on_element_value(partial_function,[]). % {} : A +-> B
901		binary_definitely_true_based_on_element_value(partial_injection,[]). % {} : A >+> B
902		binary_definitely_true_based_on_element_value(relations,[]). % {} : A <-> B
903
904		% all make use of WF now:
905		binary_not_in_boolean_type(interval,kernel_objects:not_in_nat_range_wf).
906		binary_not_in_boolean_type(partial_function,bsets_clp:not_partial_function).
907		binary_not_in_boolean_type(partial_surjection,bsets_clp:not_partial_surjection_wf).
908		binary_not_in_boolean_type(total_surjection,bsets_clp:not_total_surjection_wf).
909		binary_not_in_boolean_type(partial_injection,bsets_clp:not_partial_injection).
910		binary_not_in_boolean_type(total_injection,bsets_clp:not_total_injection).
911		binary_not_in_boolean_type(partial_bijection,bsets_clp:not_partial_bijection).
912		binary_not_in_boolean_type(cartesian_product,kernel_objects:not_is_cartesian_pair).
913		binary_not_in_boolean_type(relations,bsets_clp:not_relation_over).
914		binary_not_in_boolean_type(total_function,bsets_clp:not_total_function).
915		binary_not_in_boolean_type(total_bijection,bsets_clp:not_total_bijection).
916		binary_not_in_boolean_type(total_relation,bsets_clp:not_total_relation_wf).
917		binary_not_in_boolean_type(surjection_relation,bsets_clp:not_surjection_relation_wf).
918		binary_not_in_boolean_type(total_surjection_relation,bsets_clp:not_total_surjection_relation_wf).
919		binary_not_in_boolean_type(parallel_product,bsets_clp:not_in_parallel_product_wf).
920		binary_not_in_boolean_type(set_subtraction,kernel_objects:not_in_difference_set_wf).
921		binary_not_in_boolean_type(intersection,kernel_objects:not_in_intersection_set_wf).
922		%binary_not_in_boolean_type(union,bsets_clp:not_in_union_set_wf).
923		binary_not_in_boolean_type(range_subtraction,bsets_clp:not_in_range_subtraction_wf).
924		binary_not_in_boolean_type(range_restriction,bsets_clp:not_in_range_restriction_wf).
925		binary_not_in_boolean_type(domain_subtraction,bsets_clp:not_in_domain_subtraction_wf).
926		binary_not_in_boolean_type(domain_restriction,bsets_clp:not_in_domain_restriction_wf).
927		binary_not_in_boolean_type(composition,bsets_clp:not_in_composition_wf).
928		%binary_not_in_boolean_type(overwrite,bsets_clp:not_in_override_relation_wf).
929		% ex: not(f<+{TRUE |-> cT} : BOOL --> NATURAL) & f : BOOL --> NATURAL & cT:NATURAL
930
931
932		symbolic_closure_unary_operator(Op) :-
933		(unary_in_boolean_type(Op,_)),
934		unary_not_in_boolean_type(Op,_),
935		\+ not_symbolic_unary(Op).
936
937		not_symbolic_unary(domain).
938		%not_symbolic_unary(identity). % for Siemens Models
939
940		:- assert_must_fail((kernel_mappings:unary_in_boolean_type(Op,_),
941		\+(kernel_mappings:unary_not_in_boolean_type(Op,_)))).
942		/* note every symbolic closure operator must be dealt with by a unary_in and
943		a unary_not_in clause below, otherwise we have a problem */
944		:- assert_must_fail((kernel_mappings:unary_in_boolean_type(UnOp,_),
945		\+ kernel_mappings:symbolic_closure_unary_operator(UnOp),
946		\+ kernel_mappings:unary_function(UnOp,_,_) )).
947
948
949		/* a waitflags version is available for these taking one extra argument (the waitflags): */
950		unary_in_boolean_type(pow_subset,kernel_objects:check_subset_of_wf).
951		unary_in_boolean_type(fin_subset,kernel_objects:check_finite_subset_of_wf).
952		unary_in_boolean_type(pow1_subset,kernel_objects:check_non_empty_subset_of_wf).
953		unary_in_boolean_type(fin1_subset,kernel_objects:check_finite_non_empty_subset_of_wf).
954		unary_in_boolean_type(struct,kernel_records:is_a_record_wf).
955		unary_in_boolean_type(seq,bsets_clp:is_sequence_wf). /* last arg: basic type */
956		unary_in_boolean_type(iseq,bsets_clp:injective_sequence_wf).
957		unary_in_boolean_type(perm,bsets_clp:permutation_sequence_wf).
958		unary_in_boolean_type(domain, bsets_clp:in_domain_wf).
959		unary_in_boolean_type(seq1,bsets_clp:finite_non_empty_sequence).
960		unary_in_boolean_type(iseq1,bsets_clp:injective_non_empty_sequence).
961		unary_in_boolean_type(identity,bsets_clp:in_identity).
962		unary_in_boolean_type(closure,bsets_clp:in_closure1_wf). %element_of_closure1_wf). % this is closure1
963		%unary_in_boolean_type(reflexive_closure,bsets_clp:element_of_reflexive_closure_wf). % this is closure
964		% we could add : inverse?, general_concat, .... ? range: in_range_wf
965
966
967		% check whether a unary operator is definitely true; irrespective of arguments
968		unary_in_definitely_true(BOP,ValueOfEl) :- nonvar(ValueOfEl),
969		unary_definitely_true_based_on_element_value(BOP,ValueOfEl).
970
971		unary_definitely_true_based_on_element_value(pow_subset,[]).
972		unary_definitely_true_based_on_element_value(fin_subset,[]).
973		unary_definitely_true_based_on_element_value(seq,[]).
974		unary_definitely_true_based_on_element_value(iseq,[]).
975
976		unary_not_in_boolean_type(domain, bsets_clp:not_in_domain_wf).
977		unary_not_in_boolean_type(iseq,bsets_clp:not_injective_sequence).
978		unary_not_in_boolean_type(struct,kernel_records:not_is_a_record_wf).
979		unary_not_in_boolean_type(pow_subset,kernel_objects:not_subset_of_wf).
980		unary_not_in_boolean_type(pow1_subset,kernel_objects:not_non_empty_subset_of_wf).
981		unary_not_in_boolean_type(fin_subset,kernel_objects:not_finite_subset_of_wf).
982		unary_not_in_boolean_type(fin1_subset,kernel_objects:not_non_empty_finite_subset_of_wf).
983		unary_not_in_boolean_type(seq,bsets_clp:not_is_sequence_wf).
984		unary_not_in_boolean_type(seq1,bsets_clp:not_is_non_empty_sequence_wf).
985		unary_not_in_boolean_type(iseq1,bsets_clp:not_non_empty_injective_sequence).
986		unary_not_in_boolean_type(perm,bsets_clp:not_permutation_sequence).
987		unary_not_in_boolean_type(identity,bsets_clp:not_in_identity).
988		unary_not_in_boolean_type(closure,bsets_clp:not_in_closure1_wf). %not_element_of_closure1_wf). % this is closure1
989		%unary_not_in_boolean_type(reflexive_closure,bsets_clp:not_element_of_reflexive_closure_wf).
990
991
992		:- assert_must_fail(( kernel_mappings:cst_in_boolean_type(X,_),
993		\+ kernel_mappings:cst_not_in_boolean_type(X,_) )).
994		:- assert_must_fail(( kernel_mappings:cst_not_in_boolean_type(X,_),
995		\+ kernel_mappings:cst_in_boolean_type(X,_) )).
996
997		cst_in_boolean_type(string_set,kernel_objects:is_string).
998		cst_in_boolean_type(real_set,kernel_reals:is_real_wf).
999		cst_in_boolean_type(float_set,kernel_reals:is_float_wf).
1000	?	cst_in_boolean_type(integer_set(IntSet),Call) :- integerset_in_boolean_type(IntSet,Call).
1001
1002
1003		:- assert_must_fail(( kernel_mappings:integerset_in_boolean_type(X,_),
1004		\+ kernel_mappings:integerset_not_in_boolean_type(X,_) )).
1005		:- assert_must_fail(( kernel_mappings:integerset_not_in_boolean_type(X,_),
1006		\+ kernel_mappings:integerset_in_boolean_type(X,_) )).
1007
1008		integerset_in_boolean_type('INTEGER',kernel_objects:is_integer).
1009		integerset_in_boolean_type('NATURAL',kernel_objects:is_natural).
1010		integerset_in_boolean_type('NATURAL1',kernel_objects:is_natural1).
1011		integerset_in_boolean_type('INT',kernel_objects:is_implementable_int).
1012		integerset_in_boolean_type('NAT',kernel_objects:is_implementable_nat).
1013		integerset_in_boolean_type('NAT1',kernel_objects:is_implementable_nat1).
1014
1015		cst_not_in_boolean_type(string_set,kernel_objects:is_not_string).
1016		cst_not_in_boolean_type(real_set,kernel_reals:is_not_real).
1017		cst_not_in_boolean_type(float_set,kernel_reals:is_not_float).
1018	?	cst_not_in_boolean_type(integer_set(IntSet),Call) :- integerset_not_in_boolean_type(IntSet,Call).
1019
1020		integerset_not_in_boolean_type('INTEGER',kernel_objects:is_not_integer).
1021		integerset_not_in_boolean_type('NATURAL',kernel_objects:is_not_natural).
1022		integerset_not_in_boolean_type('NATURAL1',kernel_objects:is_not_natural1).
1023		integerset_not_in_boolean_type('INT',kernel_objects:is_not_implementable_int).
1024		integerset_not_in_boolean_type('NAT',kernel_objects:is_not_implementable_nat).
1025		integerset_not_in_boolean_type('NAT1',kernel_objects:is_not_implementable_nat1).
1026
1027		% binary_boolean_operator(B-AST-NAME, Module:Predicate, WF_ENABLED)
1028		%binary_boolean_operator(member,kernel_objects:element_of). /* not really used: interpreter deals with In explicitly */
1029		%binary_boolean_operator(not_member,kernel_objects:not_element_of_wf,yes). /* not really used: interpreter deals with In explicitly */
1030		binary_boolean_operator(not_equal,kernel_objects:not_equal_object_wf,yes).
1031		binary_boolean_operator(equal,kernel_objects:equal_object_optimized,no).
1032		binary_boolean_operator(less,kernel_objects:less_than,no).
1033		binary_boolean_operator(less_equal,kernel_objects:less_than_equal,no).
1034		binary_boolean_operator(less_real,kernel_reals:real_less_than_wf,yes).
1035		binary_boolean_operator(less_equal_real,kernel_reals:real_less_than_equal_wf,yes).
1036		binary_boolean_operator(greater,kernel_objects:greater_than,no).
1037		binary_boolean_operator(greater_equal,kernel_objects:greater_than_equal,no).
1038		binary_boolean_operator(subset,kernel_objects:check_subset_of_wf,yes).
1039		binary_boolean_operator(subset_strict,kernel_objects:strict_subset_of_wf,yes).
1040		binary_boolean_operator(not_subset_strict,kernel_objects:not_strict_subset_of_wf,yes).
1041		binary_boolean_operator(not_subset,kernel_objects:not_subset_of_wf,yes).
1042
1043		:- assert_must_fail(( kernel_mappings:binary_boolean_operator(X,_,_),
1044		\+ kernel_mappings:negate_binary_boolean_operator(X,_),
1045		\+ negate_binary_boolean_operator_swap(X,_) )).
1046		:- assert_must_fail(( kernel_mappings:binary_boolean_operator(X,_,_),
1047		kernel_mappings:negate_binary_boolean_operator(X,Y), Y=X )).
1048		:- assert_must_fail(( kernel_mappings:negate_binary_boolean_operator(X,X) )).
1049
1050		negate_binary_boolean_operator(X,Y) :-
1051		( negate_binary_boolean_operator2(X,Y) -> true
1052	?	; negate_binary_boolean_operator2(Y,X)).
1053		negate_binary_boolean_operator2(member,not_member).
1054		negate_binary_boolean_operator2(subset,not_subset).
1055		negate_binary_boolean_operator2(subset_strict,not_subset_strict).
1056
1057		negate_binary_boolean_operator2(equal,not_equal).
1058		negate_binary_boolean_operator2(less,greater_equal).
1059		negate_binary_boolean_operator2(less_equal,greater).
1060
1061		% negate where we have to swap arguments
1062		negate_binary_boolean_operator_swap(less_equal_real,less_real).
1063		negate_binary_boolean_operator_swap(less_real,less_equal_real).
1064
1065
1066		% input must be list of sets -> second argument set to true if all but one set is known
1067		:- block all_but_one_set_known(-,?).
1068		all_but_one_set_known([],true).
1069		all_but_one_set_known([H|T],KNOWN) :-
1070		(T==[] -> KNOWN=true
1071		; all_but_one(T,H,KNOWN)).
1072		:- block all_but_one(-,?,?).
1073		all_but_one([],_H,true).
1074		all_but_one([H2|T],H1,KNOWN) :- known_value(H2,K2), known_value(H1,K1), all_but_one_wait(K1,K2,T,KNOWN).
1075
1076		:- block all_but_one_wait(-,-,?,?), all_but_one_wait(?,?,-,?).
1077		all_but_one_wait(K1,K2,[],true) :- K1=true,K2=true.
1078		all_but_one_wait(K1,K2,[H3|T],KNOWN) :- known_value(H3,K3),
1079		(var(K2) -> all_but_one_wait(K2,K3,T,KNOWN) ; all_but_one_wait(K1,K3,T,KNOWN)).
1080
1081		:- block known_value(-,-).
1082		known_value(_,T) :- T==true,!.
1083		known_value(int(X),K) :- !, known_atomic(X,K).
1084		known_value(pred_true /* bool_true */,K) :- !, K=true.
1085		known_value(pred_false /* bool_false */,K) :- !, K=true.
1086		known_value(string(X),K) :- !, known_atomic(X,K).
1087		known_value([],K) :- !, K=true.
1088		known_value(avl_set(_A),K) :- !, K=true.
1089		known_value(global_set(X),K) :- !,known_atomic(X,K).
1090		known_value(freetype(X),K) :- !,known_atomic(X,K).
1091		known_value(A,K) :- when(ground(A),K=true).
1092
1093		:- block known_atomic(-,?).
1094		known_atomic(_,true).
1095
1096
1097		% some code to automatically generate documentation for kernel predicates:
1098		kernel_predicate(M,P,expression,1,BAST,BOP,WF) :-
1099	?	unary_function(BAST,M,P), get_waitflag_info(P,WF),
1100		(translate:unary_prefix(BAST,BOP,_) -> true
1101		; translate:unary_postfix(BAST,BOP,_) -> true
1102		; translate:function_like(BAST,BOP) -> true
1103		; BOP = '??').
1104		kernel_predicate(M,P,expression,2,BAST,BOP,WF) :-
1105	?	binary_function(BAST,M,P), get_waitflag_info(P,WF),
1106		(translate:binary_infix(BAST,BOP,_,_) -> true
1107		; translate:function_like(BAST,BOP) -> true ; BOP = '??').
1108		kernel_predicate(M,P,predicate,2,BAST,BOP,WF) :-
1109	?	binary_boolean_operator(BAST,M:P,WF),
1110		(translate:binary_infix(BAST,BOP,_,_) -> true
1111		; translate:function_like(BAST,BOP) -> true ; BOP = '??').
1112
1113		get_waitflag_info(P,WF) :-
1114		(expects_waitflag_and_span(P) -> WF = wf_span ;
1115		expects_waitflag_and_span(P) -> WF = yes ;
1116		WF = no).
1117		:- public generate_documentation/0.
1118		generate_documentation :-
1119	?	kernel_predicate(M,P,_T,ARITY,BAST,BOP,_WF),
1120		( symbolic_closure_unary_operator(BOP) -> Sym=' (symbolic_unary)'
1121		; symbolic_closure_binary_operator(BOP) -> Sym=' (symbolic_binary)' % these not printed as binary_function does not include them
1122		; Sym= ''),
1123		format(' ~w (~w/~w) --> ~w:~w ~w~n',[BOP,BAST,ARITY,M,P,Sym]),
1124		fail.
1125		generate_documentation.
1126
1127		:- use_module(library(codesio), [with_output_to_codes/2]).
1128		:- assert_must_succeed((with_output_to_codes(kernel_mappings:generate_documentation, Codes), Codes \= [])).
1129