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