1		% (c) 2013-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(b_expression_sharing,
6		[ apply_expression_sharing_to_machine/2
7		, create_initial_expression_cache/1
8		, find_common_subexpressions/4
9		, cse_optimize_predicate/2
10		, cse_optimize_substitution/2
11		, expand_cse_lazy_lets/2 ,expand_cse_lazy_lets_if_cse_enabled/2
12		, is_lazy_let_identifier/1
13		]).
14
15		:- use_module(probsrc(module_information),[module_info/2]).
16		:- module_info(group,typechecker).
17		:- module_info(description,'Common-Subexpression Elimination.').
18
19		:- use_module(library(lists)).
20		:- use_module(library(ordsets)).
21		:- use_module(library(avl)).
22
23		:- use_module(probsrc(tools)).
24		:- use_module(probsrc(self_check)).
25		:- use_module(probsrc(error_manager)).
26		:- use_module(probsrc(debug)).
27
28		:- use_module(probsrc(bsyntaxtree)).
29		:- use_module(probsrc(bmachine_structure)).
30
31		:- use_module(probsrc(preferences),[get_preference/2]).
32
33		expression_sharing_enabled :-
34		get_preference(use_common_subexpression_elimination,true).
35
36		create_subcache(Id,cache(Id,Avl)) :- empty_avl(Avl).
37
38		create_initial_expression_cache(A) :-
39		expression_sharing_enabled,!,
40		A=[Cache],create_subcache(top,Cache).
41		create_initial_expression_cache(disabled).
42
43
44		apply_expression_sharing_to_machine(InMachine,OutMachine) :-
45		change_sections(InMachine,InExprs,OutExprs,OutMachine),
46		create_stores(0,EmptyStores),
47		remove_implicit_negation_l(InExprs,NormedExprs),
48		find_common_subexpressions_l(NormedExprs,EmptyStores,true,machine,1,OutExprs,Stores,_Stripped,_UsedIds,_UsedCSEIds),
49		ground_reference_counters(Stores),!.
50
51		change_sections(InMachine,InExprs,OutExprs,OutMachine) :-
52		change_section2([constraints,properties,invariant,
53		assertions,operation_bodies],
54		InMachine,InExprs,OutExprs,OutMachine).
55		change_section2([],Machine,[],[],Machine).
56		change_section2([Sec|Rest],InMachine,InExprs,OutExprs,OutMachine) :-
57		select_section_texprs(Sec,LInExprs,LOutExprs,InMachine,InterMachine),
58		append(LInExprs,RInExprs,InExprs),
59		append(LOutExprs,ROutExprs,OutExprs),
60		change_section2(Rest,InterMachine,RInExprs,ROutExprs,OutMachine).
61
62
63
64		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
65
66		:- use_module(probsrc(bsyntaxtree)).
67
68		% TESTS: x+y >100 & x+y <99 now fails deterministically in REPL with CSE
69
70		% (x+y)+(x+y)=(x+y)
71
72		% Note: we should detect if we are at the invariant level before calling cse_optimize_predicate: do not mess up Rodin rodinpos proof information or syntactically_relevance info
73
74		% new predicate to optimize an operation body; not yet used
75		:- public cse_optimize_operation/1.
76		:- use_module(probsrc(bmachine),[b_top_level_operation/1,b_get_machine_operation/4]).
77		cse_optimize_operation(OpName) :-
78		b_top_level_operation(OpName),
79		b_get_machine_operation(OpName,_Results,_Parameters,Body),
80		print(optimizing(OpName)),nl,
81		cse_optimize_substitution(Body,_Res).
82
83		% no difference thus far with cse_optimize_predicate
84		cse_optimize_substitution(Subst,Res) :- cse_optimize_predicate(Subst,Res),
85		(debug_mode(on) -> nl,print('FINISHED CSE: '),nl, translate:print_subst(Res),nl ; true).
86
87		cse_optimize_predicate(Pred,Res) :- already_cse_optimized(Pred),
88		!,
89		Res=Pred.
90		cse_optimize_predicate(Pred,Res) :-
91		cse_print_check('Running Common Sub Expressions (CSE) Optimization on ', Pred),
92		expand_cse_lazy_lets(Pred,ExpandedPred), % TO DO: see if we can do this more efficiently; do we need it at all ??
93		cse_print_check('Expanded Expression: ', ExpandedPred),
94		% Note: we can still have unexpanded lazy-lets hanging around in ExpandedPred from outer scopes
95	?	find_maximum_lazy_let_id(ExpandedPred,MaxID), % find maximum ID
96		StartNr is MaxID+1, % we will start numbering from there to avoid clashes with existing lazy-lets
97	?	find_common_subexpressions(ExpandedPred,StartNr,true,R,_Refs),
98		cse_print_check('Found common sub expressions: ',R),
99
100		% print('Common: '),nl, translate:nested_print_bexpr_or_subst(R),nl,nl,nl,
101		bup_init_acc(InitialAcc),
102		reset_let_dependency_info,
103		transform_bexpr_with_bup_accs(b_expression_sharing:bup_insert_lazy_lookups,R,R2,InitialAcc,_BUPAcc),
104		%portray_avl(BUPAcc),nl,
105		%print_bexpr_or_subst(R2),nl,nl,
106		% tools_printing:trace_print(R2,6),nl,nl,
107		empty_avl(Empty),
108		avl_store('$maximum_unregistered_lazy_let_id',Empty,MaxID,TDAcc),
109	?	top_down_gen_lazy_lets(R2,TDAcc,OptimizedPred),
110
111		%cse_print_check('Optimized Expression Result: ',OptimizedPred), % info fields not yet set
112		transform_bexpr(b_expression_sharing:cse_cleanup_infos,OptimizedPred,COPred),
113		cse_print_check('Cleaned up Optimized Expression Result: ',COPred),
114
115		% nl,print('FINISHED CSE: '),nl, translate:nested_print_bexpr_or_subst(COPred),nl, %portray_avl(LastAcc),nl,nl,
116		!,
117		mark_as_optimized(COPred,Res).
118		cse_optimize_predicate(P,Res) :-
119		add_internal_error('CSE FAILED: ',cse_optimize_predicate(P,Res)),
120		Res=P.
121
122		already_cse_optimized(b(_E,_T,I)) :- member(cse_optimized,I).
123		mark_as_optimized(b(E,T,I),b(E,T,I2)) :-
124		append(I,[cse_optimized],I2).
125
126		:- use_module(probsrc(translate),[print_bexpr_or_subst/1]).
127		cse_print_check(Msg,Expr) :- debug:debug_mode(on), %%
128		!,
129		print(Msg), print_functor(Expr),
130		print_bexpr_or_subst(Expr), nl,
131		cse_check_ast(Msg,Expr).
132		cse_print_check(_,_).
133
134		print_functor(b(E,T,_)) :- functor(E,F,A), format('Type: ~w, Functor: ~w/~w~n',[T,F,A]).
135		print_functor(E) :- functor(E,F,A), format('Unwrapped, Functor: ~w/~w~n',[F,A]).
136
137		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
138		:- if(environ(prob_safe_mode,true)).
139		% check the AST (should be removed in production version of ProB):
140		cse_check_ast(PP,Pred) :-
141		debug_print(4,'Checking AST : '), debug_println(4,PP), % translate:print_bexpr_or_subst(Pred),nl,
142		check_ast(true,Pred).
143
144		%cse_check_ast_complete(PP,Pred) :- cse_check_ast(PP,Pred),
145		% debug_println(20,checking_ast_complete(PP)),
146		% % currently will generate spurious warnings when the term to start with has @identifiers introduced by LETs higher up
147		% map_over_bexpr_top_down_acc(b_expression_sharing:check_lazy_let_vars,Pred,[]),fail.
148		%cse_check_ast_complete(_,_).
149
150		%check_lazy_let_vars(X,Acc,R) :- print(t(X,Acc,R)),nl,fail.
151		check_lazy_let_vars(lazy_let_expr(TID,_,_),Acc,[ID|Acc]) :- !, get_texpr_id(TID,ID),
152		(member(ID,Acc) -> print('multiply defined id: '), print(ID),nl ; true).
153		check_lazy_let_vars(lazy_let_pred(TID,_,_),Acc,[ID|Acc]) :- !, get_texpr_id(TID,ID),
154		(member(ID,Acc) -> print('multiply defined id: '), print(ID),nl ; true).
155		check_lazy_let_vars(lazy_lookup_pred(ID),Acc,Acc) :- !,
156		(member(ID,Acc) -> true ; add_internal_error('Lazy lookup pred id not defined: ',ID)).
157		check_lazy_let_vars(lazy_lookup_expr(ID),Acc,Acc) :- !,
158		(member(ID,Acc) -> true ; add_internal_error('Lazy lookup expr id not defined: ',ID)).
159		%check_occurs_in_expr(ID,E) :-
160		% (occurs_in_expr(ID,E) -> true
161		% ; add_internal_error('Id does not occur in expression: ',ID),
162		% print('Expression: '), translate:print_bexpr_or_subst(E),nl).
163		:- else.
164		cse_check_ast(_PP,_Pred).
165		%cse_check_ast_complete(_,_).
166		%check_occurs_in_expr(_,_).
167		:- endif.
168
169
170		% -----------------------------------------------
171
172		% utility to expand lazy let expressions for better CSE if repeatedly applied
173		% Note: lazy_lookups could remain if only a partial predicate is passed
174
175		expand_cse_lazy_lets_if_cse_enabled(E,EE) :-
176		(expression_sharing_enabled -> expand_cse_lazy_lets(E,EE) ; E=EE).
177
178		expand_cse_lazy_lets(Expr,ExpandedExpr) :-
179		transform_bexpr(b_expression_sharing:expand_lazy_let,Expr,ExpandedExpr).
180
181		:- public expand_lazy_let/2.
182		%expand_lazy_let(B,R) :- tools_printing:print_term_summary(B),nl,fail.
183	?	expand_lazy_let(b(E,Type,Info),Result) :- expand_lazy_let_aux(E,Type,Info,Result).
184		expand_lazy_let_aux(lazy_let_expr(TID,SharedExpr,MainExpr),_,_,Result) :-
185		get_texpr_id(TID,ID), debug_println(4,expanding(ID)),
186		expand_lazy_lookup(ID,SharedExpr,MainExpr,Result).
187		expand_lazy_let_aux(lazy_let_pred(TID,SharedExpr,MainExpr),_,_,Result) :-
188		get_texpr_id(TID,ID), debug_println(4,expanding(ID)),
189		expand_lazy_lookup(ID,SharedExpr,MainExpr,Result).
190		expand_lazy_let_aux(lazy_let_subst(TID,SharedExpr,MainExpr),_,_,Result) :-
191		get_texpr_id(TID,ID), debug_println(4,expanding(ID)),
192		expand_lazy_lookup(ID,SharedExpr,MainExpr,Result).
193		expand_lazy_let_aux(E,Type,Info,Result) :- E \= value(_), E \= integer(_),
194		compute_static_expression(E,Val),
195		%print(computed(E,Val)),nl,
196		Result=b(value(Val),Type,Info).
197
198		expand_lazy_lookup(ID,SharedExpr,MainExpr,Result) :- \+ atom(ID),!,
199		add_internal_error('Illegal call: ',expand_lazy_lookup(ID,SharedExpr,MainExpr,Result)),
200		Result=MainExpr.
201		expand_lazy_lookup(ID,SharedExpr,MainExpr,Result) :-
202		transform_bexpr(b_expression_sharing:replace_lazy_lookup(ID,SharedExpr),MainExpr,Result).
203
204		% TO DO: unify with b_compile and ast_cleanup !
205		%compute_static_texpression(b(E,_,_),Result) :- compute_static_expression(E,Result).
206		compute_static_int_texpression(b(E,_,_),Result) :- compute_static_expression(E,int(Result)).
207
208		:- use_module(probsrc(kernel_card_arithmetic),[safe_pown/3]).
209		compute_static_expression(add(A,B),int(Result)) :- % plus
210		compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB),
211		Result is IA+IB.
212		compute_static_expression(minus(A,B),int(Result)) :- % plus
213		compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB),
214		Result is IA-IB.
215		compute_static_expression(unary_minus(A),int(Result)) :- % plus
216		compute_static_int_texpression(A,IA),
217		Result is -IA.
218		compute_static_expression(multiplication(A,B),int(Result)) :-
219		compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB),
220		Result is IA*IB.
221		compute_static_expression(div(A,B),int(Result)) :- % TO DO: also add floored_div
222		compute_static_int_texpression(B,IB), IB \= 0,
223		compute_static_int_texpression(A,IA),
224		Result is IA//IB.
225		compute_static_expression(power_of(A,B),int(Result)) :-
226		compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB), IB >= 0,
227		safe_pown(IA,IB,Result), number(Result).
228		% TO DO: modulo, division, set_extension
229		compute_static_expression(integer(I),int(I)).
230		compute_static_expression(value(I),I).
231		compute_static_expression(equal(A,B),I) :- compute_static_int_texpression(A,SA), compute_static_int_texpression(B,SB),
232		(SA==SB -> I = pred_true ; I = pred_false).
233		compute_static_expression(not_equal(A,B),I) :- compute_static_int_texpression(A,SA), compute_static_int_texpression(B,SB),
234		(SA==SB -> I = pred_false ; I = pred_true).
235
236
237		% -----------------------------------------------
238
239		% find maximum id used in lazy lookups; useful to generate new unused identifiers
240		find_maximum_lazy_let_id(BExpr,MaxID) :-
241	?	reduce_over_bexpr(b_expression_sharing:find_maximum_lazy_let_id_aux,BExpr,-1,MaxID).
242
243		:- public find_maximum_lazy_let_id_aux/3.
244		find_maximum_lazy_let_id_aux(lazy_lookup_expr(ID),MaxSoFar,NewMax) :- !,
245		convert_atom_to_nr(ID,IDNr),
246		(IDNr @> MaxSoFar -> NewMax=IDNr ; NewMax=MaxSoFar).
247		find_maximum_lazy_let_id_aux(lazy_lookup_pred(ID),MaxSoFar,NewMax) :-
248		convert_atom_to_nr(ID,IDNr),
249		(IDNr @> MaxSoFar -> NewMax=IDNr ; NewMax=MaxSoFar).
250		find_maximum_lazy_let_id_aux(_,V,V).
251
252		% -----------------------------------------------
253
254		:- use_module(library(ordsets)).
255		:- use_module(library(avl)).
256
257		% BUP traversal; replacing shared expressions by lazy_lookup and propagate usage information upwards
258		% no introduction of lazy_let yet
259		% Accumulator contains list of introduced lazy_lets
260
261		% example call ((x+y)+z)*(x+y)+((x+z)+y) + (x+z) = 0
262
263		% the starting accumulator for this traversal:
264		% '$used_lazy_lookups': special key to store which lazy_lookups occur below
265		bup_init_acc(Acc3) :- empty_avl(E),
266		avl_store('$used_lazy_lookups',E,[]-[],Acc1), % used directly and indirectly
267		avl_store('$identifier_uses',Acc1,[],Acc2),
268		avl_store('$lazy_lookups_directly_used',Acc2,[],Acc3).
269
270		:- public bup_insert_lazy_lookups/4.
271		bup_insert_lazy_lookups(BE,Res,SubAccs,NewAcc) :-
272		BE2=BE, %update_info_field(BE,BE2), % we have just treated sub-expressions and we may insert BE into avl tree of shared expressions; info field is now updated in top-down pass
273		% combine all infos about lazy_lets from subexpressions:
274		merge_bup_accs(SubAccs,Acc),
275		bup_update_identifier_uses(BE,Acc,Acc1),
276		bup_insert_lazy_lookup_if_necessary(BE2,Res,Acc1,NewAcc).
277
278		% also compute used identifiers bup (ignoring @LazyLookup replacements)
279		% a slightly rewritten version of find_typed_identifier_uses2 without recursive calls
280		bup_update_identifier_uses(TExpr,Acc,NewAcc) :-
281		avl_fetch('$identifier_uses',Acc,UsedIds),
282		get_texpr_expr(TExpr,Expr),safe_syntaxelement(Expr,_Subs,TNames,_,_),
283		( bsyntaxtree:uses_an_identifier(Expr,Id)
284		-> ord_add_element(UsedIds,Id,New),avl_store('$identifier_uses',Acc,New,NewAcc)
285		; TNames=[] -> NewAcc=Acc
286		; get_texpr_ids(TNames,Names), % these names are introduced and no longer visible higher up
287		sort(Names,SNames),
288		ord_subtract(UsedIds,SNames,New),
289		avl_store('$identifier_uses',Acc,New,Acc1),
290		% now invalidate all lazy_lookups which use an introduced variable name in SNames
291		avl_fetch('$used_lazy_lookups',Acc1,All-Intro),
292		exclude(filter_lazy_lookup(SNames),All,FAll),
293		exclude(filter_lazy_lookup(SNames),Intro,FIntro),
294		avl_store('$used_lazy_lookups',Acc1,FAll-FIntro,Acc2),
295		avl_fetch('$lazy_lookups_directly_used',Acc2,Direct),
296		exclude(filter_lazy_lookup(SNames),Direct,FDirect),
297		avl_store('$lazy_lookups_directly_used',Acc2,FDirect,NewAcc)
298		%,print(filter(SNames,Intro,FIntro)),nl
299		).
300
301		% detect which lazy lookups are no longer valid higher up the AST
302		filter_lazy_lookup(SortedNames,LazyLookupID) :-
303		lazy_let_to_be_introduced(LazyLookupID,_,_,UsedIds,SharedExpr),
304		(ord_intersect(SortedNames,UsedIds) % if any of the introduced names is used: filter out lazy lookup
305		-> true
306		; get_texpr_info(SharedExpr,Infos),
307		memberchk(contains_wd_condition,Infos)
308		%,print(wd_filter(LazyLookupID)),nl, translate:print_bexpr(SharedExpr),nl
309		).
310		% TO DO: also filter Expressions with WD-condition attached
311
312		% merge accumulators from subexpressions:
313		merge_bup_accs([],Res) :- bup_init_acc(Res).
314		merge_bup_accs([H],Res) :- !, % only one accumulator/argument: remove all ids marked for introduction
315		% they can be introduced in the level below
316		avl_delete('$used_lazy_lookups',H,All-_Intro,Acc1),
317		avl_store('$used_lazy_lookups',Acc1,All-[],Acc2), % set introduce field to []
318		Res=Acc2.
319		merge_bup_accs([H|T],Res) :- avl_fetch('$used_lazy_lookups',H,All1-_),
320		avl_store('$used_lazy_lookups',H,All1-[],InitAcc), % set introduction set to empty
321		merge_bup_accs_aux(T,InitAcc,Res).
322		merge_bup_accs_aux([],R,R).
323		merge_bup_accs_aux([H|T],A,R) :- combine_acc(H,A,A2), merge_bup_accs_aux(T,A2,R).
324
325
326		combine_acc(Acc1,Acc2,NewAcc) :-
327		avl_to_list(Acc1,Acc1List),
328		empty_avl(Empty),
329		combine_acc_aux(Acc1List,Acc2,Empty,NewAcc).
330
331		combine_acc_aux([],_Acc2,Res,Res).
332		combine_acc_aux([Field-Value1|T],Acc2,RAcc,Res) :-
333		avl_delete(Field,Acc2,Value2,Acc3),
334		(field_combinator(Field,Value1,Value2,NewValue)
335		-> avl_store(Field,RAcc,NewValue,RAcc2)
336		; RAcc2=Acc2, Acc3=Acc2),
337		combine_acc_aux(T,Acc3,RAcc2,Res).
338
339		% rules on how to combine the different fields of the accumulators:
340		field_combinator('$identifier_uses',Used1,Used2,Used) :- ord_union(Used1,Used2,Used).
341		field_combinator('$lazy_lookups_directly_used',Used1,Used2,Used) :- ord_union(Used1,Used2,Used).
342		field_combinator('$used_lazy_lookups',All1-_,AccAll-AccIntro,All-Intro) :-
343		ord_union(All1,AccAll,All),
344		ord_intersection(All1,AccAll,I1), % an @ID that is in this branch and some other branch
345		ord_union([I1,AccIntro],Intro).
346
347
348
349
350		% check if we need to introduce a lazy_lookup at the current node
351		bup_insert_lazy_lookup_if_necessary(BExpr,LAZYLOOKUP,Acc,NewAcc) :-
352		BExpr = b(Expr,Type,Info),
353	?	select(sharing(ID,TotalCount,_,_),Info,Info2), % this expressions is marked as being shared
354		TotalCount > 1, % with at least two occurrences
355		!,
356		%cse_check_ast(avl_store(ID),BExpr), % infos only re-established in TD phase
357		bup_update_info(Info2,Acc,Info3),
358		(lazy_let_to_be_introduced(ID,UsedLL,IntroLL,_,_)
359		-> true /* let already introduced; ensure we use same Ids/version everywhere */
360		; get_used_lazy_lookups(Acc,UsedLL,IntroLL),
361		avl_fetch('$identifier_uses',Acc,UsedIds),
362		% nl, print(lookup(ID,UsedLL,IntroLL)),nl, translate:print_bexpr_or_subst(BExpr), % portray_avl(Acc),nl,
363		register_let_id(ID,UsedLL,IntroLL,UsedIds,b(Expr,Type,Info3)) % store that we need to introduce a lazy_let
364		),
365		(UsedLL=[] -> true
366		; last(UsedLL,LastLL),
367		(ID > LastLL -> true
368		; format('*** LET ~w depends on later id ~w in ~w~n',[ID,LastLL,UsedLL]))
369		),
370		ord_union([ID],UsedLL,NewUsedLL),
371		ord_union([ID],IntroLL,NewIntroLL),
372		avl_store('$lazy_lookups_directly_used',Acc,[ID],Acc1),
373		avl_store('$used_lazy_lookups',Acc1,NewUsedLL-NewIntroLL,NewAcc), % to the outside (above) we only see usage of @ID
374		bup_update_info(Info2,NewAcc,LazyLookupInfo),
375		gen_lazy_lookup(Type,ID,Info2,LazyLookupInfo,LAZYLOOKUP).
376		bup_insert_lazy_lookup_if_necessary(b(Expr,Type,Info1),b(Expr,Type,Info2),Acc,Acc) :-
377		%nl, print('BUP: '),translate:print_bexpr_or_subst(b(Expr,Type,Info1)), portray_avl(Acc),nl,
378		bup_update_info(Info1,Acc,Info2).
379
380		bup_update_info(Info0,Acc,Info4) :-
381		delete(Info0,sharing(_,_,_,_),Info1),
382		delete(Info1,cse_used_ids(_),Info2),
383		get_used_lazy_lookups(Acc,_,InterList),
384		avl_fetch('$lazy_lookups_directly_used',Acc,DirectlyUsed),
385		Info3=Info2, %Info3 = [cse_used_ids(DirectlyUsed)|Info2],
386		ord_intersection(InterList,DirectlyUsed,IntroduceHere), % those not directly used will be introduced automatically inside the shared expressions
387		(IntroduceHere=[] -> Info4=Info3
388		%,(DirectlyUsed=[] -> true ; print('*** WARNING: directly used not empty: '),print(DirectlyUsed),nl)
389		; Info4 = ['$introduce_lazy_lookups'/IntroduceHere|Info3]). % store info in node for later top-down traversal).
390
391		get_used_lazy_lookups(Acc,All,Introduce) :-
392		(avl_fetch('$used_lazy_lookups',Acc,A-I) -> All=A,Introduce=I
393		; add_internal_error('Failed: ',get_used_lazy_lookups(Acc,All,Introduce)),
394		All=[], Introduce=[]).
395
396
397		% ----------------------------------
398
399		% PHASE 2: Top-Down Phase to introduce LETs at latest possible moment:
400
401		% top-down traversal to introduce lazy_lets for lazy_lookups we have introduced in bottom-up phase
402		top_down_gen_lazy_lets(InExpr,Acc,ResExpr) :-
403	?	top_down_gen_lazy_lets1(InExpr,Acc,IntExpr),
404		update_info_field(IntExpr,ResExpr). % maybe we should do this only if there was a change
405
406		top_down_gen_lazy_lets1(b(LazyLookup,Type,_Info),Acc,NewExpr1) :-
407		directly_uses_cse_id(LazyLookup,LetID), % check if we have lazy_let_expr/_pred
408		(lazy_let_to_be_introduced(LetID,UsedInside,IntroduceHere,_,SharedExpression) -> true
409		; avl_fetch('$maximum_unregistered_lazy_let_id',Acc,MaxId), % all ids up until MaxId come from a previous run of CSE
410		LetID > MaxId,
411		add_internal_error('**** Unregistered let: ',LetID),fail),
412		\+ avl_fetch(lazy_let_introduced(LetID),Acc,true),
413		!,
414		debug_println(9,inlining_single_usage(LetID,UsedInside,IntroduceHere)),
415		avl_store(lazy_let_inlined(LetID),Acc,true,Acc0), % NOT USED !
416	?	top_down_gen_lazy_lets(SharedExpression,Acc0,NewSharedExpression),
417	?	top_down_gen_lazy_lets_for_list(IntroduceHere,Type,Acc0,_,NewExpr1,NewSharedExpression).
418		top_down_gen_lazy_lets1(b(Expr,Type,Info),Acc,Res) :-
419		%syntaxtraversion(BExpr,Expr,_,_,Subs,_TNames),
420	?	select('$introduce_lazy_lookups'/IntroduceHere,Info,Info2),
421		% functor(Expr,Fun,Arity),print(intro(IntroduceHere,Fun,Arity)),nl, translate:print_bexpr_or_subst(b(Expr,Type,Info)),nl,
422		!,
423		% the lazy lookups in Inter must now be introduced, if not already done so
424	?	top_down_gen_lazy_lets_for_list(IntroduceHere,Type,Acc,NewAcc,Res,InnerRes),
425		syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1),
426		InnerRes=b(NewExpr1,Type,Info2),
427		td_treat_sub_args(Subs,NewAcc,NSubs).
428		top_down_gen_lazy_lets1(b(Expr,Type,Info),Acc,b(NewExpr1,Type,Info)) :-
429		syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1),
430		td_treat_sub_args(Subs,Acc,NSubs).
431
432		% treat sub-arguments of an expression for which we have introduced lets
433		td_treat_sub_args([],_Acc,[]).
434		td_treat_sub_args([TE|T],Acc,[NTE|NT]) :-
435	?	(top_down_gen_lazy_lets(TE,Acc,NTE)
436		-> true
437		; add_internal_error('Call failed: ',top_down_gen_lazy_lets(TE,Acc,NTE)),
438		NTE=TE ),
439		td_treat_sub_args(T,Acc,NT).
440
441
442		top_down_gen_lazy_lets_for_list(IntroHere,Type,Acc,NewAcc,Res,InnerRes) :-
443		% first collect all lazy_lets we need here:
444		%td_collect_lazy_lets_to_introduce_here(Inter,Acc,IntroHere,[]),
445		% now update which lazy_lets are now visible
446		topsort(IntroHere,SortedIntroHere),
447		%print(sorted_intro(IntroHere,SortedIntroHere)),nl,
448	?	td_introduce_lazy_lets(SortedIntroHere,Type,Acc,NewAcc,Res,InnerRes).
449
450		% topological sorting using a naive quadratic algorithm; TO DO: improve
451		topsort([],[]).
452	?	topsort([H|T],Res) :- select(X,T,TT), let_depends_upon(H,X), !,topsort([X,H|TT],Res).
453		topsort([H|T],[H|ST]) :- topsort(T,ST).
454
455		:- dynamic let_depends_upon/2, lazy_let_to_be_introduced/5.
456		% a fact to store which let depends directly upon which other let
457		% UsedLL: Used LazyLet @IDs, IntroduceLL: LazyLet @IDs to be introduced, UsedIds: regular identifiers referenced directly or via other lazy_lookups
458		register_let_id(ID,UsedLL,IntroduceLL,UsedIds,SharedExpr) :-
459		assertz(lazy_let_to_be_introduced(ID,UsedLL,IntroduceLL,UsedIds,SharedExpr)),
460		%format('LAZY LET ~w (depends on ~w) [uses ~w ids]~n',[ID,UsedLL,UsedIds]),
461	?	member(ID2,UsedLL),
462		assertz(let_depends_upon(ID,ID2)),
463		% now do transitive closure in one direction
464		%let_depends_upon(ID0,ID),assertz(let_depends_upon(ID0,ID2)),
465		fail.
466		register_let_id(ID,UsedLL,_,_,_) :- fail,
467		% now do transitive closue in other direction
468		member(ID2,UsedLL),
469		let_depends_upon(ID2,ID3),
470		assertz(let_depends_upon(ID,ID3)),fail.
471		register_let_id(_,_,_,_,_).
472
473		reset_let_dependency_info :- retractall(let_depends_upon(_,_)),
474		retractall(lazy_let_to_be_introduced(_,_,_,_,_)).
475
476
477		% introduce lets in order
478		td_introduce_lazy_lets([],_,Acc,Acc,R,R).
479		td_introduce_lazy_lets([],Ty,Acc,AccR,T,RT) :-
480		add_internal_error('Call failed: ',td_introduce_lazy_lets([],Ty,Acc,AccR,T,RT)),fail.
481		td_introduce_lazy_lets([LetID|T],Type,Acc,Acc1,OuterTerm,InnerTerm) :-
482		avl_fetch(lazy_let_introduced(LetID),Acc,true),!,
483	?	td_introduce_lazy_lets(T,Type,Acc,Acc1,OuterTerm,InnerTerm).
484		td_introduce_lazy_lets([LetID|T],Type,Acc,Acc1,OuterTerm,InnerTerm) :-
485		avl_store(lazy_let_introduced(LetID),Acc,true,Acc0),
486	?	td_introduce_lazy_lets(T,Type,Acc0,Acc1,MidTerm,InnerTerm),
487		% now introduce let for ID
488		lazy_let_to_be_introduced(LetID,_,_,UsedIds,SharedExpression),
489	?	top_down_gen_lazy_lets(SharedExpression,Acc0,NewSharedExpression), % the lazy_lets introduced inside are not visible
490		%tools_printing:print_term_summary(gen_lazy_let(Type,LetID,NewSharedExpression,MidTerm,OuterTerm)),nl,
491		gen_lazy_let(Type,LetID,UsedIds,NewSharedExpression,MidTerm,OuterTerm).
492
493
494
495		% -----------------------------------------------
496
497
498		% copy position information; important e.g. for discharged checks for theorems and invariants
499		/*
500		copy_position_info(From,b(To,Type,Info1),b(To,Type,Info3)) :-
501		get_texpr_pos(From,PositionInfo),!,
502		delete(Info1,nodeid(_),Info2),
503		Info3 = [nodeid(PositionInfo)|Info2].
504		copy_position_info(_,E,E).
505		*/
506
507		:- use_module(probsrc(b_ast_cleanup),[recompute_used_ids_info/2]).
508		% update info field of a typed expression after a modification of the expression
509		update_info_field(TE,NewTE) :-
510		update_wd_condition(TE,TE2),
511		recompute_used_ids_info(TE2,NewTE). % inserting lazy_lookups changes used ids for exists/forall
512
513		% check if we need to add contains_wd_condition info field
514		update_wd_condition(b(E,Type,Info1),Res) :-
515		nonmember(contains_wd_condition,Info1), % inlined update_wd_condition_info to just copy E in clause below; not sure this helps memory performance
516	?	sub_expression_contains_wd_condition(E),
517		!,
518		Res = b(E,Type,[contains_wd_condition|Info1]).
519		update_wd_condition(E,E).
520
521		update_wd_condition_info(E,Info1,Info2) :-
522		nonmember(contains_wd_condition,Info1),
523		sub_expression_contains_wd_condition(E),
524		!,
525		Info2 = [contains_wd_condition|Info1].
526		update_wd_condition_info(_,I,I).
527
528
529
530		% Remove sharing/4 info from SharedExpression + avoid reusing it for CSE if algorithm applied second time
531		%delete_sharing_info(b(E,T,Info),b(E,T,NewInfo)) :- delete(Info,sharing(_,_,_,_),NewInfo).
532
533		:- public cse_cleanup_infos/2.
534		% Remove info that is no longer necessary once CSE has run to completion:
535		cse_cleanup_infos(b(E,T,Info),Res) :-
536	?	cse_cleanup_infos1(E,T,Info,Res).
537
538		cse_cleanup_infos1(lazy_let_pred(ID,SharedExpr,Body),T,_,Res) :-
539		collect_important_info(SharedExpr,Body,Info),
540		cse_cleanup_aux(lazy_let_pred(ID,SharedExpr,Body),T,Info,Res).
541		cse_cleanup_infos1(lazy_let_expr(ID,SharedExpr,Body),T,_,Res) :-
542		collect_important_info(SharedExpr,Body,Info),
543		cse_cleanup_aux(lazy_let_expr(ID,SharedExpr,Body),T,Info,Res).
544		cse_cleanup_infos1(lazy_let_subst(ID,SharedExpr,Body),T,_,Res) :-
545		collect_important_info(SharedExpr,Body,Info),
546		cse_cleanup_aux(lazy_let_subst(ID,SharedExpr,Body),T,Info,Res).
547		cse_cleanup_infos1(sequence(Seq),T,Info,Res) :- !, % re-flatten sequences that were binarized for CSE sharing analysis
548		flatten_sequence(Seq,FSeq,WD),
549		(WD==contains_wd_condition, nonmember(contains_wd_condition,Info) ->
550		Info1 = [contains_wd_condition|Info] ; Info1=Info),
551		cse_cleanup_aux(sequence(FSeq),T,Info1,Res).
552		cse_cleanup_infos1(E,T,Info,Res) :- cse_cleanup_aux(E,T,Info,Res).
553
554		flatten_sequence([H,b(sequence(T),subst,Info)],[H|FT],WD) :- member(cse_generated,Info),
555		!,
556		% check if this sequence contains a WD condition
557		(var(WD),member(contains_wd_condition,Info) -> WD=contains_wd_condition ; true),
558		flatten_sequence(T,FT,WD).
559		flatten_sequence(X,X,_WD).
560
561
562		cse_cleanup_aux(E,T,Info,b(NewE,T,NewInfo)) :-
563		delete(Info,cse_used_ids(_),Info2),
564		( nonmember(contains_wd_condition,Info2), % TO DO: allow in DISPROVER_MODE
565		post_cse_simplifier(E,SE) -> NewE = SE, NewInfo=Info2 % Note: maybe some lets no longer necessary now
566	?	; reorder_lazy_let_expr(E,T,Info2,NewE,NewInfo) -> true
567		; NewE=E,NewInfo=Info2).
568
569		% reorder/move lazy lets outside if this leads to better optimizations being applicable
570		reorder_lazy_let_expr(Expr,Type,Info,NewExpr,NewInfo) :-
571	?	reorder_argument(Expr,FunctorID,Match,TArgToReorder,OtherArgs,_),
572		get_texpr_expr(TArgToReorder,ArgToReorder),
573		is_lazy_let(ArgToReorder,LLType,ID,ShExpr,BodyA),
574		get_texpr_expr(BodyA,Match),
575		debug_println(19,reorder_lazy_let_expr(ID,FunctorID)),
576		!,
577	?	reorder_argument(NewBinExpr,FunctorID,_,BodyA,OtherArgs,Recur),
578		!, % FunctorID ensures only one possible solution for reorder_argument
579		( Recur=recur, % we may have to re-order again
580		reorder_lazy_let_expr(NewBinExpr,Type,Info,NewBinExpr2,Info2)
581		-> NewInnerExpr = b(NewBinExpr2,Type,Info2)
582		; NewInnerExpr = b(NewBinExpr,Type,Info)),
583	?	is_lazy_let(NewExpr,LLType,ID,ShExpr,NewInnerExpr), % TYPE MAY HAVE TO CHANGE for CASE ?? TO DO: Check with appropriate B Machine
584		% copy important info from InfoA ??
585		update_wd_condition_info(NewExpr,Info,NewInfo).
586		% TO DO: add more cases + what if both arguments need reordering --> fixpoint computation ?
587
588		is_lazy_let(lazy_let_expr(ID,ShExpr,BodyA),lazy_let_expr,ID,ShExpr,BodyA).
589		is_lazy_let(lazy_let_subst(ID,ShExpr,BodyA),lazy_let_subst,ID,ShExpr,BodyA).
590		is_lazy_let(lazy_let_pred(ID,ShExpr,BodyA),lazy_let_pred,ID,ShExpr,BodyA).
591
592		% reorder argument 1 (i.e., move lazy_let out) in case we match a certain pattern
593		% reorder_argument(Expression, ID, MATCH, ARG_TO_REORDER, OtherArgs)
594		reorder_argument(function(A,B),function_1,set_extension(_),A,B,do_not_recur). % there is optimized code: b_apply_function_set_extension
595		reorder_argument(max(A),max,set_extension(_),A,nil,do_not_recur). % we have optimized code for min({a,b,...}) and max
596		reorder_argument(min(A),min,set_extension(_),A,nil,do_not_recur).
597		reorder_argument(card(A),card,set_extension(_),A,nil,do_not_recur).
598		reorder_argument(image(A,B),image_1,closure(_),A,B,recur).
599		reorder_argument(image(B,A),image_2,set_extension(_),A,B,recur).
600		% avoid that Lazy Lets stand at illegal places
601		% avoid IF THEN LET(... ELSIF P THEN ....) if_elsif term
602	?	reorder_argument(if(IfList),if1,_,A,Rest,recur) :- select(A,IfList,Rest).
603		% avoid lazy let in place of a CASE case_or term
604		reorder_argument(case(Expr,Cases,Else),case_element,_,A,[Expr,Else|Rest],recur) :- select(A,Cases,Rest).
605		% avoid lazy let for a select_when term:
606	?	reorder_argument(select(SelWhenList),select,_,A,Rest,recur) :- select(A,SelWhenList,Rest). % SelWhenList: a list containing select_when/2 terms
607		reorder_argument(select(SelWhenList,Else),select_else,_,A,(Rest,Else),recur) :- select(A,SelWhenList,Rest).
608		% CSE will sometimes insert a lazy_let_subst where an if_elsif should stand; this not supported by the interpreter
609		%reorder_argument(while(COND,TSubst,INV,VARIANT),while_subst,_,TSubst,[COND,INV,VARIANT]). % TO DO: check if lazy_let does not depend on variables modified in loop
610
611		% TO DO: bring this in accordance with do_not_share_this rules:
612
613		% detect certain obvious inconsistencies / tautologies introduced by CSE
614		post_cse_simplifier(equal(A,B),truth) :- same_lazy_lookup(A,B).
615		post_cse_simplifier(not_equal(A,B),falsity) :- same_lazy_lookup(A,B).
616		post_cse_simplifier(greater(A,B),falsity) :- same_lazy_lookup(A,B).
617		post_cse_simplifier(greater_equal(A,B),truth) :- same_lazy_lookup(A,B).
618		post_cse_simplifier(less(A,B),falsity) :- same_lazy_lookup(A,B).
619		post_cse_simplifier(less_real(A,B),falsity) :- same_lazy_lookup(A,B).
620		post_cse_simplifier(less_equal(A,B),truth) :- same_lazy_lookup(A,B).
621		post_cse_simplifier(less_equal_real(A,B),truth) :- same_lazy_lookup(A,B).
622		post_cse_simplifier(subset(A,B),truth) :- same_lazy_lookup(A,B).
623		post_cse_simplifier(not_subset(A,B),falsity) :- same_lazy_lookup(A,B).
624		post_cse_simplifier(subset_strict(A,B),falsity) :- same_lazy_lookup(A,B).
625		post_cse_simplifier(not_subset_strict(A,B),truth) :- same_lazy_lookup(A,B).
626
627		/*
628		TO DO:
629		split up lazy_let_pred; as previously done in gen_lazy_let
630		gen_lazy_let(pred,CSEID,_UsedIds,SharedExpr,Body,Result) :-
631		true, % TO DO <------------- RENABLE
632		% check if we can split off Prefix and/or Suffix of Body not using CSEID
633		cse_split_conjunct(Body, CSEID, Prefix, MainBody, Suffix),
634		!,
635		print(optimizing_let_with_conjunction_body(CSEID)),nl,
636		gen_id(CSEID,SharedExpr,ID),
637		cse_conjunct_predicates(MainBody,NewBody),
638		%get_texpr_info(NewBody,NewInfo),
639		collect_important_info(SharedExpr,NewBody,NewInfo), % we could remove ID from cse_used_ids
640		LET = b(lazy_let_pred(ID,SharedExpr,NewBody),pred,NewInfo),
641		append(Prefix,[LET|Suffix],ConjunctionList),
642		cse_conjunct_predicates(ConjunctionList,Result).
643		*/
644
645		same_lazy_lookup(A,B) :- get_lazy_lookup_id(A,ID), get_lazy_lookup_id(B,ID).
646
647		get_lazy_lookup_id(b(E,Type,_),Type,ID) :- get_lazy_lookup_id_aux(E,ID).
648		get_lazy_lookup_id(b(E,_,_),ID) :- get_lazy_lookup_id_aux(E,ID).
649		get_lazy_lookup_id_aux(lazy_lookup_expr(ID),ID).
650		get_lazy_lookup_id_aux(lazy_lookup_pred(ID),ID).
651		% there is no lazy_lookup_subst(ID)
652
653		%gen_lazy_let_with_check(Type, Identifier, UsedIds,SharedExpression, SubExpressionInsideLet, Result) :-
654		% cse_check_ast(before_gen_lazy_let_shared,SharedExpression),
655		% cse_check_ast(before_gen_lazy_let_body,SubExpressionInsideLet),
656		% (gen_lazy_let(Type, Identifier, UsedIds,SharedExpression, SubExpressionInsideLet, Result)
657		% -> cse_check_ast(gen_lazy_let,Result)
658		% ; add_internal_error('Call failed: ',gen_lazy_let_with_check(Type, Identifier, UsedIds,SharedExpression, SubExpressionInsideLet, Result)),
659		% fail).
660
661		% TO DO: maybe check that we are not in a bad context to prevent optimized treatment (e.g. {1|->a,2|->b}(x) ), rather than delegating this to reorder lazy_let code above ?
662		% gen_lazy_let(Type, Identifier, UsedIds,SharedExpression, SubExpressionInsideLet, Result)
663		gen_lazy_let(pred,A,_UsedIds,SharedExpr,Body,b(R,pred,[])) :-
664		% Info field will be set later in cse_cleanup_infos
665		!,
666		gen_id(A,SharedExpr,ID), debug_println(4,generating_lazy_let_pred(A,ID)),
667		R = lazy_let_pred(ID,SharedExpr,Body).
668		gen_lazy_let(subst,A,_UsedIds,SharedExpr,Body,b(R,subst,[])) :-
669		!,
670		gen_id(A,SharedExpr,ID), debug_println(4,generating_lazy_let_subst(A,ID)),
671		R = lazy_let_subst(ID,SharedExpr,Body).
672		gen_lazy_let(Type,A,_UsedIds,SharedExpr,C,b(lazy_let_expr(ID,SharedExpr,C),Type,[])) :-
673		gen_id(A,SharedExpr,ID).
674
675		% ----------------------
676
677
678		collect_important_info(SubA,SubB,Info) :- (var(SubA) ; var(SubB)), !,
679		add_internal_error('Illegal call: ',collect_important_info(SubA,SubB,Info)),fail.
680		collect_important_info(SubA,SubB,Info) :-
681		extract_info(SubA,SubB,Info1), % WD info (bsyntaxtree utility)
682		% was collect_uses_cse_id([SubA,SubB],IDS), % CSE usage info
683		exclude(do_not_copy_info_from_sub_terms,Info1,Info2), % is this necessary ??
684		Info=Info2. %Info = [cse_used_ids(IDS)|Info2].
685
686		% ----------------------
687
688		gen_lazy_lookup(pred,A,Infos,LazyLookupInfo,R) :- !, convert_to_atom(A,ID),
689	?	(member(negated_cse,Infos)
690		-> R = b(negation(b(lazy_lookup_pred(ID),pred,LazyLookupInfo)),pred,OuterInfos),
691		delete(LazyLookupInfo,'$introduce_lazy_lookups'/_,OuterInfos) % we do not need to generate the lazy_lookups here; they can be created inside the negation
692		%,print(create_neg_lookup(ID,LazyLookupInfo,OuterInfos)),nl
693		; R = b(lazy_lookup_pred(ID),pred,LazyLookupInfo)).
694		gen_lazy_lookup(Type,A,_,LazyLookupInfo,
695		b(lazy_lookup_expr(ID),Type,LazyLookupInfo)) :- convert_to_atom(A,ID).
696
697		% generate atoms: many identifier treating predicates expect atoms
698		gen_id(A,B,b(identifier(ID),Type,[])) :- get_texpr_type(B,Type),convert_to_atom(A,ID).
699
700		convert_to_atom(A,ID) :- var(A),!, add_internal_error('Illegal call: ', convert_to_atom(A,ID)),fail.
701		convert_to_atom(A,ID) :- atom(A),!, ID=A.
702		convert_to_atom(Nr,ID) :- number_codes(Nr,C), atom_codes(ID,[64|C]). % 64 = @
703
704		convert_atom_to_nr(Atom,Nr) :- var(Atom),!, add_internal_error('Illegal call: ',convert_atom_to_nr(Atom,Nr)),fail.
705		convert_atom_to_nr(Atom,Nr) :- atom_codes(Atom,[64|C]), number_codes(Nr,C).
706
707		% check if an identifier is (potentially) a lazy_let ID starting with @
708		is_lazy_let_identifier(Atom) :- atom(Atom), atom_codes(Atom,[64|_]).
709
710
711		/*
712		collect_uses_cse_id([],[]).
713		collect_uses_cse_id([H|T],Res) :-
714		get_cse_used_ids_info(H,CSE),!,
715		collect_uses_cse_id(T,CSET),
716		ord_union(CSE,CSET,Res).
717
718		uses_cse_id(ID,Expr) :- get_cse_used_ids_info(Expr,List),!,
719		member(ID,List).
720		uses_cse_id(_ID,Expr) :- print('Could not extract cse_used_ids info: '), print(Expr),nl,
721		true.
722
723		% CSE Identifier usage infor either form info field or from direct usage by lazy_lookups
724		get_cse_used_ids_info(TExpr,IDList) :- get_texpr_expr(TExpr,E),
725		directly_uses_cse_id(E,UsedID),!,
726		IDList = [UsedID].
727		get_cse_used_ids_info(TExpr,IDList) :- get_texpr_info(TExpr,Info),
728		member(cse_used_ids(IDList),Info),!.
729		get_cse_used_ids_info(TE,L) :- print('Could not get cse_used_ids info: '), print(TE),
730		L=[].
731		*/
732
733		directly_uses_cse_id(E,ID) :- var(E),!, add_internal_error('Illegal call: ',directly_uses_cse_id(E,ID)),fail.
734		directly_uses_cse_id(lazy_lookup_pred(AtomID),ID) :- convert_atom_to_nr(AtomID,ID).
735		directly_uses_cse_id(lazy_lookup_expr(AtomID),ID) :- convert_atom_to_nr(AtomID,ID).
736		% there is no lazy_lookup_subst
737
738		:- public print_cse_id_used/1.
739		print_cse_id_used(TypedExpr) :- get_texpr_info(TypedExpr,Info),
740		member(cse_used_ids(L),Info),!,
741		print(L).
742		print_cse_id_used(_) :- print(' no cse used id info ').
743
744		:- public replace_lazy_lookup/4.
745		:- use_module(probsrc(btypechecker), [unify_types_strict/2]).
746		% TO DO: maybe remove cse_used_ids ??
747		%replace_lazy_lookup(_,_,T,_) :- print(T),nl,fail.
748		replace_lazy_lookup(ID,SharedExpr,BExpr,SharedExpr) :-
749		get_lazy_lookup_id(BExpr,Type,TID),
750		!,
751		TID=ID,
752		get_texpr_type(SharedExpr,SharedType),
753		(my_unify_types(SharedType,Type) -> true
754		; add_internal_error('Incompatible type: ',replace_lazy_lookup(ID,'\\='(SharedType,Type),BExpr,SharedExpr))).
755		replace_lazy_lookup(_,_,E,Res) :- update_info_field(E,Res). % probably not necessary ?!
756
757		:- if(environ(prob_safe_mode,true)).
758		my_unify_types(T1,T2) :- (\+ ground(T1) ; \+ ground(T2)),
759		format('*** Non-ground type unification: ~w = ~w~n~n',[T1,T2]),
760		fail.
761		:- endif.
762		my_unify_types(T1,T2) :- unify_types_strict(T1,T2).
763
764		% -----------------
765
766
767		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
768		% common subexpression detection
769
770		:- assert_must_succeed(
771		( find_common_subexpressions(b(identifier(i),integer,[]),0,false,R),
772		R == b(identifier(i),integer,[sharing(0,1,top,[]),cse_used_ids([])])
773		)).
774		:- assert_must_succeed(
775		( find_common_subexpressions(b(identifier(i),integer,[]),0,true,R),
776		R == b(identifier(i),integer,[cse_used_ids([])])
777		)).
778		:- assert_must_succeed(
779		( I = b(identifier(i),integer,[]),
780		O = b(identifier(i),integer,[sharing(0,2,top,[]),cse_used_ids([])]),
781		find_common_subexpressions(b(add(I,I),integer,[]),0,false,R),
782		R == b(add(O,O),integer,[sharing(1,1,top,[]),cse_used_ids([0])])
783		)).
784		:- assert_must_succeed(
785		( I = b(identifier(i),integer,[]),
786		O = b(identifier(i),integer,[cse_used_ids([])]),
787		find_common_subexpressions(b(add(I,I),integer,[]),0,true,R),
788		R == b(add(O,O),integer,[sharing(0,1,top,[]),cse_used_ids([])])
789		)).
790		% two quantifiers with the same variable name must not share
791		% expressions that contain the variable, other expressions should be
792		% shared
793		:- assert_must_succeed(
794		( C = b(identifier(c),integer,[]),
795		X = b(identifier(x),integer,[]),
796		I = b(identifier(i),set(integer),[]),
797		O = b(integer(1),integer,[]),
798		% !x.(x:I => x<c+1)
799		F = b(forall([X],
800		b(member(X,I),pred,[]),
801		b(less(X,b(add(C,O),integer,[])),pred,[])),pred,[]),
802		% !x.(x:I => x>c+1)
803		Fx = b(forall([X],
804		b(member(X,I),pred,[]),
805		b(greater(X,b(add(C,O),integer,[])),pred,[])),pred,[]),
806		C1 = b(identifier(c),integer,[sharing(3,2,top,[]),cse_used_ids([])]),
807		X1 = b(identifier(x),integer,[sharing(0,3,7,[]),cse_used_ids([])]),
808		I1 = b(identifier(i),set(integer),[sharing(1,2,top,[]),cse_used_ids([])]),
809		O1 = b(integer(1),integer,[sharing(4,2,top,[]),cse_used_ids([])]),
810		F1 = b(forall([X1],
811		b(member(X1,I1),pred,[sharing(2,1,7,[]),cse_used_ids([0,1])]),
812		b(less(X1,b(add(C1,O1),integer,[sharing(5,2,top,[]),cse_used_ids([3,4])])),
813		pred,[sharing(6,1,7,[]),cse_used_ids([0,3,4,5])])),
814		pred,[sharing(7,1,top,[0]),cse_used_ids([0,1,2,3,4,5,6])]),
815		% e.g. c+1 should be shared (ref. 5)
816		% x and x:I must not be shared, they get a new reference (8 and 9)
817		X2 = b(identifier(x),integer,[sharing(8,3,11,[]),cse_used_ids([])]),
818		F2 = b(forall([X2],
819		b(member(X2,I1),pred,[sharing(9,1,11,[]),cse_used_ids([1,8])]),
820		b(greater(X2,b(add(C1,O1),integer,[sharing(5,2,top,[]),cse_used_ids([3,4])])),
821		pred,[sharing(10,1,11,[]),cse_used_ids([3,4,5,8])])),
822		pred,[sharing(11,1,top,[8]),cse_used_ids([1,3,4,5,8,9,10])]),
823		find_common_subexpressions(b(conjunct(F,Fx),pred,[]),0,false,R),
824		R == b(conjunct(F1,F2),pred,[sharing(12,1,top,[]),cse_used_ids([0,1,2,3,4,5,6,7,8,9,10,11])])
825		)).
826
827		% find_common_subexpressions/4 searches for common subexpressions and adds an
828		% information field sharing/4 to each AST node.
829		% find_common_subexpressions(+TExpr,+Start,+SkipSimple,-NTExpr):
830		% TExpr: the original AST
831		% Start: at which number the IDs should start (usually 0)
832		% NTExpr: the AST, each node annotated with an sharing(ID,Counter,SubId,References) information field
833		% two syntax nodes share the same ID when they should yield always the same
834		% value. Counter counts the number of occurrences of the same expression in
835		% the given AST. SubId is the unique reference of the quantified expression
836		% where a used ID is introduced, top if there is no such quantifier.
837		% References is a list of ids that are are sub-expressions of the node which
838		% occur more than once and which depend on the newly introduced identifiers
839		% (Please note: The declaration of a variable in a quantified expression
840		% is an occurrence of its own.)
841		% SkipSimple: set to true if expression sharing should not be applied to simple
842		% expressions like identifier(_), integer(_), etc.
843		find_common_subexpressions(TExpr,Start,SkipSimple,NTExpr) :-
844		find_common_subexpressions(TExpr,Start,SkipSimple,NTExpr,_).
845		find_common_subexpressions(TExpr,Start,SkipSimple,NTExpr,References) :-
846		create_stores(Start,EmptyStores),
847	?	find_common_subexpressions2(TExpr,EmptyStores,SkipSimple,root/1,NTExpr,Stores,_Stripped,_UsedIds,_UsedCSEIds),
848		ground_reference_counters(Stores),
849		get_current_references(Stores,References). % needed ??
850
851		:- if(environ(prob_safe_mode,true)).
852		add_cse_used_ids_info(Ids,OldInfos,NewInfos) :- (var(Ids) ; \+ ground(OldInfos)),!,
853		add_internal_error('Illegal Call: ',add_cse_used_ids_info(Ids,OldInfos,NewInfos)),
854		NewInfos = OldInfos.
855		:- endif.
856		add_cse_used_ids_info(Ids,OldInfos,NewInfos) :-
857		exclude(do_not_copy_info_from_sub_terms,OldInfos,OldInfos1),
858		NewInfos=[cse_used_ids(Ids)|OldInfos1].
859
860		do_not_copy_info_from_sub_terms(cse_used_ids(_)). % is_cse_used_ids
861		do_not_copy_info_from_sub_terms(negated_cse).
862
863		% find_common_subexpressions2(+TExpr,+InStores,+SkipSimple,+OuterFunctor,-NTExpr,-OutStores,-Stripped,-UsedIds,-UsedCSEIds):
864		find_common_subexpressions2(TExpr,InStores,SkipSimple,OuterFunctor,NTExpr,OutStores,Stripped,UsedIds,UsedCSEIds) :-
865		% decompose the typed expression into its components (Subs), look up the newly introduced
866		% identifiers (NewIds) and create a new typed expression (NTExpr) with the modified components
867		% (NSubs) and the new Info field (Info)
868	?	fc_parts(TExpr,Expr,Type,Subs,NewQuantifiedIds,InvalidatedIds,NSubs,OldInfos,NewInfos,NTExpr),
869		% introduce a map from expression to reference that is only visible to this node
870		% and it subnodes if new identifiers (NewIds) are introduced
871		% OutStores1 and OutStores contain a pattern such that if OutStores1 is set,
872		% OutStores is exactly like OutStores1 but without visibility of the newly introduced
873		% identifiers.
874		append(InvalidatedIds,NewQuantifiedIds,NewIds),
875		create_substore(NewIds,ID,InStores,SubStores),
876		% apply subexpression detection on the subexpressions
877		functor(Expr,OuterExprFunctor,_), % memorise functor for sub-expressions (allows deciding if sharing makes sense)
878	?	find_common_subexpressions_l(Subs,SubStores,SkipSimple,OuterExprFunctor,1,
879		NSubs,SubStores1,StrippedSubs,UsedSubIds,SubUsedCSEIds),
880		% create a stripped (i.e. no info field, no types) version of the syntax node for look ups
881		(Type==subst -> Stripped=not_relevant % substitions are never shared (and everything containing a subst is a subst itself)
882	?	; create_stripped(Expr,StrippedSubs,Stripped)),
883		LookupKey = cse_lookup_key(Stripped,Type), % we also store the type along with the stripped AST (avoid sharing, e.g., two prj1/2 functions with different types, see test 255 !)
884		% merge the used ids of the subnodes with the used ids in this node,
885		% subtract newly introduced quantified identifiers because they are not visible from outside
886		update_used_ids(Expr,NewQuantifiedIds,UsedSubIds,UsedIds),
887		% if a substore was introduced due to newly introduced identifiers, remove it
888		%%(OuterExprFunctor=while -> portray_stores(SubStores1) ; true),
889		remove_last_substore(NewIds,SubStores1,Stores1,References),
890		% try to find the expression in the stores
891	?	(do_not_share_this(SkipSimple,Stripped,UsedIds,OuterFunctor,Type,OldInfos) ->
892		OutStores = Stores1,
893		add_cse_used_ids_info(SubUsedCSEIds,OldInfos,NewInfos),
894		UsedCSEIds = SubUsedCSEIds,
895		store_expression(LookupKey,UsedIds,Stores1,_,_,ID) /* just ground ID; used for Sub expressions */
896		%, print(not_sharing(ID))
897		; lookup_cse(Type,LookupKey,UsedIds,Stores1,OutStores,SharingInfo,Negated,ID) ->
898		/* it is shared */
899		% print(looked_up(ID,Negated,used(UsedIds,sub(UsedSubIds)),Stores1)),nl,
900		(Negated=negated_cse
901		-> NewInfos=[Negated,SharingInfo|OldInfos1]
902		; NewInfos=[SharingInfo|OldInfos1]),
903		add_cse_used_ids_info(SubUsedCSEIds,OldInfos,OldInfos1),
904		ord_union([ID],SubUsedCSEIds,UsedCSEIds),
905		set_references(References,SharingInfo)
906		% In this case we do not need to look for sharing in the sub-expressions !!
907		%,check_sharing_info(lookup,SharingInfo)
908		;
909		% if not found, store the expression: it will be shared if we use it again later
910		store_expression(LookupKey,UsedIds,Stores1,OutStores,SharingInfo,ID),
911		ord_union([ID],SubUsedCSEIds,UsedCSEIds),
912		% print(new_id(ID,UsedIds,SubUsedCSEIds,OutStores)),nl,
913		% TO DO: what if later we find out that it is shared after all -> we should remove sub-expression counts
914		add_cse_used_ids_info(SubUsedCSEIds,OldInfos,OldInfos1),
915		NewInfos=[SharingInfo|OldInfos1],
916		set_references(References,SharingInfo)
917		%,check_sharing_info(new,SharingInfo)
918		). % print(done_find(NTExpr,OutStores,UsedIds,UsedCSEIds)),nl.
919
920		lookup_cse(Type,LookupKey,UsedIds,Stores1,OutStores,SharingInfo,Negated,ID) :-
921		(lookup_expression(LookupKey,UsedIds,Stores1,OutStores,SharingInfo,ID)
922		-> Negated = normal_cse
923		; Type=pred, negate_lookup_key(LookupKey,NegKey), % try looking up negation
924		lookup_expression(NegKey,UsedIds,Stores1,OutStores,SharingInfo,ID),
925		Negated = negated_cse).
926
927		negate_lookup_key(cse_lookup_key(P,pred),cse_lookup_key(NP,pred)) :-
928		negate_norm_strip(P,NP).
929
930		%check_sharing_info(_,sharing(Id,_RefCounter,Level,Refs)) :- number(Id), ground(Level), ground(Refs),!.
931		%check_sharing_info(PP,SI) :- print(illegal_sharing_info(PP,SI)),nl.
932
933		% NewIds = introduced IDs or modified Ids
934		fc_parts(TExpr,Expr,Type,Subs,SQuantifiedNewIds,InvalidatedIds,NSubs,OldInfos2,NewInfos,NTExpr) :-
935	?	my_decompose_texpr(TExpr,Expr,Type,OldInfos),
936		cse_syntaxtransformation(Expr,Subs,Names,NSubs,NExpr),
937		get_texpr_ids(Names,QuantifiedNewIds), list_to_ord_set(QuantifiedNewIds,SQuantifiedNewIds),
938	?	(select(invalidate_ids_for_cse(ModifiedIDs),OldInfos,OldInfos2)
939		% we have a stored invalidation info for CSE
940		-> InvalidatedIds=ModifiedIDs
941		; InvalidatedIds= [],OldInfos=OldInfos2),
942		%functor(Expr,F,A), format('-> ~w/~w : ~w + ~w~n',[F,A,SQuantifiedNewIds,InvalidatedIds]),
943		create_texpr(NExpr,Type,NewInfos,NTExpr).
944		% TO DO: re-flatten the sequential compositions later
945
946		% CSE traversal which ignores certain sub-arguments (mainly LHS of assignments)
947		cse_syntaxtransformation(assign(LHS,RHS),RHS,[],NRHS,NExpr) :- !, % print(assign(LHS)),nl,
948		same_length(RHS,NRHS),
949		NExpr=assign(LHS,NRHS).
950		cse_syntaxtransformation(becomes_element_of(LHS,RHS),[RHS],[],[NRHS],NExpr) :- !,
951		NExpr=becomes_element_of(LHS,NRHS).
952		cse_syntaxtransformation(becomes_such(LHS,RHS),[RHS],[],[NRHS],NExpr) :- !,
953		NExpr=becomes_such(LHS,NRHS).
954		cse_syntaxtransformation(evb2_becomes_such(LHS,RHS),[RHS],[],[NRHS],NExpr) :- !,
955		NExpr=evb2_becomes_such(LHS,NRHS).
956		cse_syntaxtransformation(assign_single_id(Id,RHS),[RHS],[],[NRHS],NExpr) :- !,
957		NExpr=assign_single_id(Id,NRHS).
958		cse_syntaxtransformation(Expr,Subs,Names,NSubs,NExpr) :- syntaxtransformation(Expr,Subs,Names,NSubs,NExpr).
959		% TO DO: rlevent(Id,Section,Status,Parameters,Guard,Theorems,Actions,VWitnesses,PWitnesses,_Unmod,Refines)
960
961		:- use_module(probsrc(b_read_write_info), [get_accessed_vars/4]).
962	?	my_decompose_texpr(b(Expr,Type,Infos),Expr2,Type,Infos2) :- my_decompose2(Expr,Expr2,ModifiedIDs),
963		add_invalidated_ids_to_infos(Infos,ModifiedIDs,Infos2).
964		% decompose sequence into left and right part and store invalidated parts on the right
965		my_decompose2(sequence([TSubst|T]),Res,[]) :- !,
966		Res=sequence([TSubst|NT]),
967		get_accessed_vars(TSubst,[],ModifiedIDs,_),
968		debug_println(19,modified_sequence(ModifiedIDs)),
969		construct_seq_tail(T,ModifiedIDs,NT).
970		% annotate parts of while loop with variables which are invalidated by loop iteration
971		% note the While loop itself also invalidates the same variables, ensures that a substore
972		% is already set-up when entering the sub-nodes; TO DO: examine whether we can simplify this by improving the way shared expressions are stored above
973		my_decompose2(while(COND,TSubst,INV,VARIANT),while(COND2,TSubst2,INV2,VARIANT2),ModifiedIDs) :-
974		get_accessed_vars(TSubst,[],ModifiedIDs,_),
975		debug_println(19,modified_while(ModifiedIDs)),
976		add_invalidated_ids(TSubst,ModifiedIDs,TSubst2),
977		add_invalidated_ids(COND,ModifiedIDs,COND2),
978		add_invalidated_ids(INV,ModifiedIDs,INV2),
979		add_invalidated_ids(VARIANT,ModifiedIDs,VARIANT2).
980		my_decompose2(X,X,[]).
981
982		add_invalidated_ids_to_infos(L,[],R) :- !, R=L.
983		add_invalidated_ids_to_infos(L,Ids,[invalidate_ids_for_cse(Ids)|L]).
984
985		add_invalidated_ids(b(E,T,I),Ids,b(E,T,[invalidate_ids_for_cse(Ids)|I])).
986
987		construct_seq_tail([],_,[]) :- !.
988		%construct_seq_tail([X],[X]) :- !.
989		construct_seq_tail([H|T],ModifiedIDs,[b(sequence([H|T]),subst,[cse_generated,invalidate_ids_for_cse(ModifiedIDs)])]). % store that modified vars are invalid for CSE in tail
990
991
992
993		find_common_subexpressions_l([],Stores,_SkipSimple,_OuterFunctor,_,[],Stores,[],[],[]).
994		find_common_subexpressions_l([Expr|Erest],InStores,SkipSimple,OuterFunctor,ArgNr,
995		[NExpr|Nrest],OutStores,[Stripped|Srest],UsedIds,UsedCSEIds) :-
996	?	find_common_subexpressions2(Expr,InStores,SkipSimple,outer(OuterFunctor,ArgNr),NExpr,InterStores,Stripped,UsedIds1,UsedCSEIds1),
997		A1 is ArgNr+1,
998	?	find_common_subexpressions_l(Erest,InterStores,SkipSimple,OuterFunctor,A1,Nrest,OutStores,Srest,UsedIds2,UsedCSEIds2),
999		ord_union(UsedIds1,UsedIds2,UsedIds), % the B identifiers used
1000		ord_union(UsedCSEIds1,UsedCSEIds2,UsedCSEIds). % the identifiers to CSE used
1001
1002		boolean(boolean_true).
1003		boolean(boolean_false).
1004
1005
1006		do_not_share_this(_,_,_,_,Type,_) :- \+ ground(Type),!. % it could be that the Type is ground, but the sub-expressions contain non-ground types; see test 1090 size(arr)
1007		% nl,print(not_sharing_non_ground_type(Type)),nl,nl.
1008		% TO DO: can we maybe still share non-ground type terms if we are careful ? see also tests 402, 403 ?
1009		do_not_share_this(_,_,_,_,Type,_) :- do_not_share_type(Type),!.
1010		do_not_share_this(_,_Stripped,_,_Functor,_Type,Infos) :-
1011		memberchk(contains_wd_condition,Infos),
1012		get_preference(use_common_subexpression_wd_only,true),
1013		!. % also examine DISPROVER MODE ?
1014		do_not_share_this(_,_Stripped,_,_Functor,Type,_Infos) :- Type==pred,
1015		get_preference(use_common_subexpression_also_for_predicates,false),
1016		!.
1017		do_not_share_this(SkipSimple,Stripped,UsedIds,OuterFunctor,_Type,_Infos) :-
1018		SkipSimple==true,
1019	?	do_not_share_this_3(Stripped,UsedIds,OuterFunctor).
1020
1021		do_not_share_type(subst).
1022		do_not_share_type(status). % Event-B Event Status
1023
1024		:- use_module(probsrc(external_functions),[not_declarative/1]).
1025
1026		%do_not_share_this_3(card(identifier(DeferredSet)),_,outer(Comparison,_)) :-
1027		% b_global_sets:b_global_deferred_set(DeferredSet),
1028		% %we would like to avoid interfering with deferred set card detection, see test 893
1029		% member(Comparison,[equal,greater_equal,less_equal,greater,less]),!.
1030		do_not_share_this_3(case_or(_,_),_,_) :- !. % why does this have a pred type ?
1031		do_not_share_this_3(if_elsif(_,_),_,_) :- !.
1032		do_not_share_this_3(select_when(_,_),_,_) :- !. % has subst type; so will not be shared
1033		do_not_share_this_3(set_extension(X),_,outer(OuterFunctor,ArgNr)) :- !,
1034		%nl,print(sx(X,OuterFunctor/ArgNr)),nl,
1035		(X = [V], simple_explicit_value(V) ; % singleton set with simple value
1036		set_extension_optimized_treatment_available(OuterFunctor,ArgNr)).
1037		do_not_share_this_3(comprehension_set(_Id,_),_,M) :-
1038		% optimized treatment available; important for test 1079
1039	?	(nmem(M) -> true ; symbolic_set_op(M)). % -> true ; print(share(_Id,M)),nl,nl,fail).
1040		do_not_share_this_3(union(_,_),_,M) :-
1041		% union often used for composing functions
1042		(nmem(M) -> true ; symbolic_set_op(M)). % -> true ; print(share_union(M)),nl,nl,fail).
1043		% lambda is already translated into comprehension_set here
1044		%do_not_share_this_3(closure(_L),_,outer(OuterFunctor,ArgNr)) :- !,
1045		% closure1_optimized_treatment_available(OuterFunctor,ArgNr).
1046		%do_not_share_this_3(sequence_extension(_L),_,outer(OuterFunctor,ArgNr)) :- !, % we need to add b_compute_card2 for seq ?
1047		/*
1048		do_not_share_this_3(X,_,M) :- nmem(M), functor(X,F),
1049		(kernel_mappings:symbolic_closure_unary_operator(F) ;
1050		kernel_mappings:symbolic_closure_binary_operator(F)).
1051
1052		% case for unary_in_boolean_type solutions:
1053		*/
1054	?	do_not_share_this_3(pow_subset(X),_,M) :- nmem(M) ; infinite_set(X).
1055		do_not_share_this_3(fin_subset(X),_,M) :- nmem(M) ; infinite_set(X).
1056		do_not_share_this_3(pow1_subset(X),_,M) :- nmem(M) ; infinite_set(X).
1057		do_not_share_this_3(fin1_subset(X),_,M) :- nmem(M) ; infinite_set(X).
1058		do_not_share_this_3(struct(_),_,M) :- nmem(M).
1059	?	do_not_share_this_3(seq(X),_,M) :- nmem(M) ; infinite_set(X).
1060		do_not_share_this_3(iseq(X),_,M) :- nmem(M) ; infinite_set(X).
1061	?	do_not_share_this_3(perm(_),_,M) :- nmem(M).
1062	?	do_not_share_this_3(domain(_),_,M) :- nmem(M).
1063		do_not_share_this_3(seq1(X),_,M) :- nmem(M) ; infinite_set(X).
1064		do_not_share_this_3(iseq1(X),_,M) :- nmem(M) ; infinite_set(X).
1065		do_not_share_this_3(identity(X),_,M) :- nmem(M) ; infinite_set(X).
1066		do_not_share_this_3(closure(_),_,M) :- nmem(M).
1067		do_not_share_this_3(external_pred_call(FunName,_Args),_,_) :- not_declarative(FunName). % in principle any element containing this should not be shared (but anyway there are little gurantees about preservation and order of side-effects)
1068		do_not_share_this_3(external_function_call(FunName,_Args),_,_) :- not_declarative(FunName).
1069		% case for binary_not_in_boolean_type solutions:
1070		/*
1071		do_not_share_this_3(partial_bijection(_,_),_,M) :- nmem(M).
1072		do_not_share_this_3(total_relation(_,_),_,M) :- nmem(M).
1073		do_not_share_this_3(surjection_relation(_,_),_,M) :- nmem(M).
1074		do_not_share_this_3(total_surjection_relation(_,_),_,M) :- nmem(M).
1075		do_not_share_this_3(parallel_product(_,_),_,M) :- nmem(M).
1076		% set_subtraction, intersection not covered
1077		*/
1078	?	do_not_share_this_3(interval(A,B),_,M) :- nmem(M) ; small_interval(A,B).
1079	?	do_not_share_this_3(total_function(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).
1080		do_not_share_this_3(total_injection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).
1081		do_not_share_this_3(total_surjection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).
1082		do_not_share_this_3(total_bijection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).
1083	?	do_not_share_this_3(partial_function(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).
1084		do_not_share_this_3(partial_injection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). % >+>
1085		do_not_share_this_3(partial_surjection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).
1086	?	do_not_share_this_3(relations(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).
1087	?	do_not_share_this_3(cartesian_product(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).
1088		%do_not_share_this_3(div(A,B),_,_) :- A=identifier(xx), B=integer(1000000000). % xx / 1000000000 ; purpose: test vesg performance issue
1089		%do_not_share_this_3(range(identifier('Block_Id')),_,_). % for vesg performance test in INVARIANT
1090
1091		do_not_share_this_3(Stripped,UsedIds,_OuterFunctor) :- too_simple_for_sharing2(Stripped,UsedIds).
1092
1093		% check if expression used as second arg of member check:
1094		nmem(outer(M,2)) :- mem_op(M).
1095		nmem(outer(M,_)) :- (M=partial_function ; M=total_function ; M=relations).
1096		mem_op(member).
1097		mem_op(not_member).
1098		symbolic_set_op(outer(M,P)) :- (M=union; M=function,P=1).
1099
1100		small_interval(integer(A),integer(B)) :- number(A),number(B), B < A+10000000.
1101		infinite_set(integer_set(_)). % :- (X='INTEGER' ; X = 'NATURAL' ; X = 'NATURAL1').
1102		infinite_set(real_set).
1103		infinite_set(string_set).
1104		% TO DO : couple
1105		simple_explicit_value(integer(_)).
1106		simple_explicit_value(string(_)).
1107		simple_explicit_value(boolean_true).
1108		simple_explicit_value(boolean_false).
1109		simple_explicit_value(identifier(_Id)). % :- b_global_sets:is_b_global_constant(_,_,Id). % no guarantee that this is really an enumerated set element because a local variable could overide this; but
1110		% TO DO: should any identifier not be ok here: basically, we just gain the lookup when sharing ??
1111		%simple_explicit_value(V) :- print(sev(V)),nl,fail.
1112
1113		set_extension_optimized_treatment_available(card,1).
1114		set_extension_optimized_treatment_available(min,1). % we have optimized code for min({a,b,...}) and max
1115		set_extension_optimized_treatment_available(max,1).
1116		set_extension_optimized_treatment_available(function,1).
1117		set_extension_optimized_treatment_available(subset,2). % there is a rule in cleanup_post which will rewrite this to member checks {x1,x2,...} <: B <=> x1:B & x2:B & ...; we could also try and ensure that this runs first !
1118		set_extension_optimized_treatment_available(image,2). % ??
1119
1120		%closure1_optimized_treatment_available(image,1). % there is some custom code for: image_for_closure1_wf; but it is also called if we do CSE ??!!
1121
1122		:- use_module(probsrc(external_functions),[performs_io/1]).
1123
1124		too_simple_for_sharing2(equal(A,B),_) :-
1125		(A = identifier(_Id), boolean(B) ;
1126		B = identifier(_Id), boolean(A) ).
1127		too_simple_for_sharing2(identifier(Id),[Id]).
1128		too_simple_for_sharing2(unary_minus(Int),[]) :- Int = integer(_).
1129		too_simple_for_sharing2(integer(_),[]).
1130		too_simple_for_sharing2(value(_),[]).
1131		too_simple_for_sharing2(boolean_true,[]).
1132		too_simple_for_sharing2(boolean_false,[]).
1133		too_simple_for_sharing2(integer_set(_),[]).
1134		too_simple_for_sharing2(bool_set,[]).
1135		too_simple_for_sharing2(float_set,[]).
1136		too_simple_for_sharing2(real_set,[]).
1137		too_simple_for_sharing2(typeset,[]).
1138		too_simple_for_sharing2(string(_),[]).
1139		too_simple_for_sharing2(string_set,[]).
1140		too_simple_for_sharing2(empty_set,[]).
1141		too_simple_for_sharing2(empty_sequence,[]).
1142		too_simple_for_sharing2(lazy_lookup_pred(_),_).
1143		too_simple_for_sharing2(lazy_lookup_expr(_),_).
1144		too_simple_for_sharing2(lazy_let_expr(_,_,_),_).
1145		too_simple_for_sharing2(lazy_let_pred(_,_,_),_).
1146		too_simple_for_sharing2(lazy_let_subst(_,_,_),_).
1147		too_simple_for_sharing2(couple(_,_),_). % maybe could be useful nonetheless ??
1148		%too_simple_for_sharing2(interval(integer(_),integer(_)),_).
1149		% TO DO: do not share arithmetic expressions which can be constant folded ??
1150		% or maybe perform constant folding at the same time ??
1151		too_simple_for_sharing2(truth,[]).
1152		too_simple_for_sharing2(falsity,[]).
1153		too_simple_for_sharing2(max_int,[]).
1154		too_simple_for_sharing2(min_int,[]).
1155		% TO DO: completely avoid sharing those expressions ? but usually they should not occur inside predicates/expressions anyway
1156		too_simple_for_sharing2(external_pred_call(FunName,_Args),_) :-
1157		performs_io(FunName).
1158		too_simple_for_sharing2(external_function_call(FunName,_Args),_) :-
1159		performs_io(FunName).
1160
1161
1162		set_references(References,sharing(_Id,_RefCounter,_Level,References)).
1163
1164		% the stores data type has the following form:
1165		% stores(Counter,References,Top,Substores)
1166		% - Counter is the next ID for new expressions, the same expressions
1167		% share the same id
1168		% - References is a mapping from an ID to a term rc(C,R) where C
1169		% contains the number of occurrences of the expressions so far and R the
1170		% final number of occurrences of this expression. Until the end, R is a variable
1171		% that will be unified with the last value of C
1172		% - Top is a mapping from a stripped expression to an ID. This mapping is for all
1173		% expressions that do not contain references to quantified variables
1174		% - Substores is a list of terms substore(Ids,SubStore) where Ids is a list of
1175		% introduced identifiers in a qualified expression and Substore is a mapping from
1176		% a stripped expression to its ID. The expression contains references to identifiers
1177		% in Ids. In case of nested quantified expressions, the inner expression has
1178		% a substore entry before the outer expression in the list.
1179		create_stores(Start,stores(Start,Empty,Empty,[])) :-
1180		empty_avl(Empty).
1181		create_substore([],_SubId,Stores,Stores) :- !.
1182		create_substore(NewIds,ID,InStores,SubStores) :-
1183		force_create_substore(NewIds,ID,InStores,SubStores).
1184		force_create_substore(Ids,SubId,
1185		stores(Counter,IR,Top, InSubs),
1186		stores(Counter,IR,Top, [substore(OrdIds,Empty,SubId,[])|InSubs])) :-
1187		list_to_ord_set(Ids,OrdIds),
1188		empty_avl(Empty).
1189
1190		% remove_last_substore(+Names,+InSubStores,-OutSubStores,-References)
1191		remove_last_substore([],Stores,Stores,[]).
1192		remove_last_substore([_|_], % new ids have been introduced; local scope / substore was added
1193		stores(Counter,IR,Top,[Substore|Subs]),
1194		stores(Counter,IR,Top,Subs),
1195		References) :-
1196		Substore = substore(_Names,_Store,_SubId,References).
1197
1198		% try and get references to common sub expression ids + the corresponding expressions
1199		get_current_references(stores(_Counter,IR,TopStore,_Subs),References) :-
1200		avl_to_list(IR,Refs),
1201		convlist(reused_expression(TopStore),Refs,References).
1202		reused_expression(TopStore,ID-rc(Count,Count),cse(ID,Expr,Count)) :- Count>1,
1203	?	avl_member(Expr,TopStore,ID). % reverse lookup; not efficient !
1204
1205		lookup_expression(Stripped,UsedIds,InStores,OutStores,sharing(Id,RefCounter,Level,_References),Id) :-
1206		InStores = stores(Counter,InRefCounter, TopStore,OldSubStores),
1207		OutStores = stores(Counter,OutRefCounter,TopStore,NewSubStores),
1208		lookup_expression2(OldSubStores,TopStore,Stripped,UsedIds,Id,Level,NewSubStores),!,
1209		avl_fetch(Id,InRefCounter,rc(OC,RefCounter)),
1210		NC is OC+1,
1211		avl_store(Id,InRefCounter,rc(NC,RefCounter),OutRefCounter).
1212		lookup_expression2([],TopStore,Stripped,_UsedIds,Id,top,[]) :-
1213		avl_fetch(Stripped,TopStore,Id).
1214		lookup_expression2([substore(Names,Store,SubId,OldRefs)|Rest],_TopStore,Stripped,_UsedIds,Id,SubId,
1215		[substore(Names,Store,SubId,NewRefs)|Rest]) :-
1216		avl_fetch(Stripped,Store,Id),!,
1217		ord_add_element(OldRefs,Id,NewRefs).
1218		lookup_expression2([substore(Names,Store,SubId,Refs)|Rest],TopStore,Stripped,UsedIds,Id,Level,
1219		[substore(Names,Store,SubId,Refs)|NRest]) :-
1220		ord_disjoint(UsedIds,Names),
1221		!,
1222		lookup_expression2(Rest,TopStore,Stripped,UsedIds,Id,Level,NRest).
1223
1224		%lookup_next_id(stores(Id,_,_,_),Id).
1225
1226		store_expression(Stripped,UsedIds,InStores,OutStores,sharing(Id,RefCounter,Level,_References),Id) :-
1227		InStores = stores(Id,InRefCounter,InTopStore,InSubStores),
1228		Counter is Id+1, % Generate a new CSE Identifier
1229		OutStores = stores(Counter,OutRefCounter,OutTopStore,OutSubStores),
1230		store_expression2(InSubStores,InTopStore,Stripped,UsedIds,Id,OutSubStores,OutTopStore,Level),
1231		avl_store(Id,InRefCounter,rc(1,RefCounter),OutRefCounter).
1232		store_expression2([],InTopStore,Stripped,_UsedIds,Id,[],OutTopStore,top) :-
1233		avl_store(Stripped,InTopStore,Id,OutTopStore).
1234		store_expression2([substore(Names,InStore,SubId,Refs) |Srest],TopStore,Stripped,UsedIds,Id,
1235		[substore(Names,OutStore,SubId,Refs)|Srest],TopStore,SubId) :-
1236		ord_intersect(Names,UsedIds),!, % the Shared Expression makes use of identifiers/names introduced at that level; it cannot be re-used higher up
1237		avl_store(Stripped,InStore,Id,OutStore).
1238		store_expression2([Substore|ISrest],InTopStore,Stripped,UsedIds,Id,
1239		[Substore|OSrest],OutTopStore,Level) :-
1240		store_expression2(ISrest,InTopStore,Stripped,UsedIds,Id,OSrest,OutTopStore,Level).
1241
1242		:- public portray_stores/1. % for debugging
1243		portray_stores(stores(Counter,RefCounter,TopStore,SubStores)) :-
1244		format('Store Counter:~w ~n Reference Counts: ',[Counter]),
1245		portray_avl(RefCounter),nl,
1246		print('Top = '), portray_avl(TopStore),nl,
1247		(maplist(portray_substore,SubStores) -> true ; print('Illegal Substores: '),nl).
1248		portray_substore(substore(Names,OutStore,_SubId,Refs)) :-
1249		format('--> Substore [Names=~w, Refs=~w]~n Store = ',[Names,Refs]),
1250		portray_avl(OutStore),nl.
1251
1252		update_used_ids(Expr,NewlyIntroducedIds,UsedSubIds,UsedIds) :-
1253		update_used_ids2(Expr,UsedSubIds,UsedIds1),
1254		ord_subtract(UsedIds1,NewlyIntroducedIds,UsedIds). % remove NewlyIntroducedIds; they are not visible outside
1255		update_used_ids2(identifier(Id),UsedSubIds,UsedIds) :- !, % we directly use an identifier
1256		ord_add_element(UsedSubIds,Id,UsedIds).
1257		update_used_ids2(_Expr,UsedSubIds,UsedIds) :- !, UsedSubIds=UsedIds.
1258
1259		% We do not have to use strip_and_norm_ast/2 from bsyntaxtree though
1260		% the result should be the same. We already have the stripped versions
1261		% of the subexpressions, so we can re-use that information
1262		create_stripped(Expr,StrippedSubs,NormStripped) :-
1263		(cse_syntaxtransformation(Expr,_Subs,_Names,StrippedSubs,Stripped)
1264	?	-> norm_strip(Stripped,NormStripped)
1265		; add_internal_error('Illegal Expression: ',create_stripped(Expr,StrippedSubs,NormStripped)),
1266		NormStripped = Expr).
1267
1268		ground_reference_counters(stores(_Counter,RefCounter,_TopStore,_SubStores)) :-
1269		avl_to_list(RefCounter,List),
1270		maplist(ground_reference_counter,List).
1271		ground_reference_counter(_Id-rc(C,C)).
1272
1273		:- use_module(library(samsort)).
1274		norm_strip(empty_sequence,R) :- !, R = empty_set.
1275		norm_strip(greater_equal(A,B),R) :- !, R = less_equal(B,A).
1276		norm_strip(greater(A,B),R) :- !, R = less(B,A).
1277		norm_strip(set_extension(SX),R) :- !,
1278		sort(SX,SSX),
1279		R = set_extension(SSX).
1280		norm_strip(negation(A),R) :- negate_norm_strip(A,R).
1281		norm_strip(Old,New) :-
1282		functor(Old,Functor,2),
1283		is_commutative(Functor),!,
1284		norm_commutative(Functor,Old,New).
1285		norm_strip(Old,Old).
1286
1287		negate_norm_strip(equal(A,B),R) :- !, R=not_equal(A,B).
1288		negate_norm_strip(not_equal(A,B),R) :- !, R=equal(A,B).
1289		negate_norm_strip(less_equal(A,B),R) :- !, R=less(B,A).
1290		negate_norm_strip(less_equal_real(A,B),R) :- !, R=less_real(B,A).
1291		negate_norm_strip(less(A,B),R) :- !, R=less_equal(B,A).
1292		negate_norm_strip(less_real(A,B),R) :- !, R=less_equal_real(B,A).
1293		negate_norm_strip(member(A,B),R) :- !, R=not_member(A,B).
1294		negate_norm_strip(not_member(A,B),R) :- !, R=member(A,B).
1295		negate_norm_strip(subset(A,B),R) :- !, R=not_subset(A,B).
1296		negate_norm_strip(not_subset(A,B),R) :- !, R=subset(A,B).
1297		negate_norm_strip(subset_strict(A,B),R) :- !, R=not_subset_strict(A,B).
1298		negate_norm_strip(not_subset_strict(A,B),R) :- !, R=subset_strict(A,B).
1299		negate_norm_strip(conjunct(C),R) :- !,
1300		maplist(negate_norm_strip,C,NC),
1301		R=disjunct(NC).
1302		negate_norm_strip(disjunct(C),R) :- !,
1303		maplist(negate_norm_strip,C,NC),
1304		R=conjunct(NC).
1305		negate_norm_strip(negation(A),R) :- !, R=A.
1306		% what about implication, equivalence, exists, forall
1307		negate_norm_strip(X,negation(X)).
1308
1309		norm_commutative(Functor,Old,New) :- is_associative(Functor), !,
1310		functor(Old,Functor,2), arg(1,Old,OA), arg(2,Old,OB),
1311		% now collect all args with same functor in left and right:
1312		get_top_level_functor_arguments(OA,Functor,LeftArgs),
1313		get_top_level_functor_arguments(OB,Functor,RightArgs),
1314		append(LeftArgs,RightArgs,Args),
1315		samsort(Args,SortedArgs),
1316		New =.. [Functor,SortedArgs].
1317		norm_commutative(Functor,Old,New) :- % the functor is not associative (or cannot appear at top-level in OA,OB)
1318		functor(Old,Functor,2), arg(1,Old,OA), arg(2,Old,OB),
1319		New =.. [Functor,NA,NB],
1320		(OA @>= OB -> OA=NB,OB=NA ; OA=NA,OB=NB).
1321
1322		% we could use this instead of samsort
1323		% but we get error message e.g. for % (x\/y\/v\/x) /= (v\/x\/y) & x<:BOOL as an expression appears within itself ?!
1324		%sort_args(Functor,Args,SortedArgs) :-
1325		% (idempotent(Functor) -> sort(Args,SortedArgs) % we can remove duplicates
1326		% ; samsort(Args,SortedArgs)).
1327
1328
1329		get_top_level_functor_arguments(Top,Functor,Args) :- % must also be associative
1330		functor(Top,Functor,N), !,
1331		(N=2 -> Top =.. [Functor|Args] % no normalisation applied
1332		; arg(1,Top,Args)). % Note: we do not recurse: we assume normalisation has already been applied fully below
1333		get_top_level_functor_arguments(Top,_,[Top]).
1334
1335		%is_commutative(_) :- !,fail.
1336		is_commutative(conjunct). % commutative only if there are no WD issues !
1337		is_commutative(disjunct). % commutative only if there are no WD issues !
1338		is_commutative(equivalence).
1339		is_commutative(equal).
1340		is_commutative(not_equal).
1341		is_commutative(add).
1342		is_commutative(multiplication).
1343		is_commutative(union).
1344		is_commutative(intersection).
1345
1346
1347		%is_associative(_) :- !,fail.
1348		is_associative(conjunct). % even if there are WD issues !
1349		is_associative(disjunct). % even if there are WD issues !
1350		is_associative(add).
1351		is_associative(multiplication).
1352		is_associative(union).
1353		is_associative(intersection).
1354		is_associative(concat).
1355		is_associative(composition).
1356
1357		% not used at the moment:
1358		:- public idempotent/1.
1359		idempotent(conjunct).
1360		idempotent(disjunct).
1361		idempotent(union).
1362
1363		%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1364		% removing implicit negation:
1365		% predicates of the form a/=b (resp. a/:b, ...) are
1366		% rewritten to not(a=b), (resp. not(a:b), ...) to enable sharing of the
1367		% predicate a=b.
1368
1369		remove_implicit_negation(TExpr,NTExpr) :-
1370		remove_bt(TExpr,Expr,NewExpr,TExpr2),
1371		syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr),
1372		remove_implicit_negation_l(Subs,NSubs),
1373		remove_implicit_negation2(TExpr2,NTExpr).
1374
1375		remove_implicit_negation_l([],[]).
1376		remove_implicit_negation_l([OExpr|ORest],[NExpr|NRest]) :-
1377		remove_implicit_negation(OExpr,NExpr),
1378		remove_implicit_negation_l(ORest,NRest).
1379
1380		remove_implicit_negation2(TExpr,NTExpr) :-
1381		get_texpr_expr(TExpr,Expr),
1382		remove_implicit_negation3(Expr,NTExpr),!.
1383		remove_implicit_negation2(TExpr,TExpr).
1384
1385		remove_implicit_negation3(negation(P),R) :-
1386		get_texpr_expr(P,negation(Q)),!,R=Q. % eliminate double negation
1387		remove_implicit_negation3(not_equal(A,B),R) :- negate_bexpr(equal(A,B),A,B,R).
1388		remove_implicit_negation3(not_member(A,B),R) :- negate_bexpr(member(A,B),A,B,R).
1389		remove_implicit_negation3(not_subset(A,B),R) :- negate_bexpr(subset(A,B),A,B,R).
1390		remove_implicit_negation3(not_subset_strict(A,B),R) :- negate_bexpr(subset_strict(A,B),A,B,R).
1391
1392		negate_bexpr(Expr,SubA,SubB,R) :- extract_info(SubA,SubB,Info),
1393		create_texpr(Expr,pred,Info,P),
1394		create_negation(P,R).
1395
1396
1397		% TO DO: optimize away unnecessary nested LETs as below:
1398		% Optimized pred:
1399		% !(sddb1,sddb2).((sddb1 : INTEGER & sddb2 : INTEGER) & (sddb1 |-> sddb2 : dom(SDDBs_Signal) & (Signals_Cap__Name~)(Routes_Cap__Opposite_Signal_ID(route)) : ran(SDDBs_Signal(sddb1 |-> sddb2))) => (LET (@9)==ran(tses) IN (LET (@10)==dom(@9) IN sddb1 /: @10 & sddb2 /: @10)))
1400
1401
1402		/*
1403
1404		Code currently not used; but possibly to be re-included :
1405
1406
1407		% a version of conjunction which recomputes the cse_used_ids INFO
1408		cse_conjunct_predicates(L,Res) :- cse_conjunct_predicates2(L,b(E,pred,I)),
1409		(collect_uses_cse_id(L,CSEINFO)
1410		-> Res = b(E,pred,[cse_used_ids(CSEINFO)|I1]),
1411		exclude(do_not_copy_info_from_sub_terms,I,I1) %delete(I,cse_used_ids(_),I1)
1412		; print('*** Could not collect uses_cse_id INFO :'), print(L),nl,
1413		Res = b(E,pred,I)).
1414
1415		% sometimes we get identical conjuncts; TO DO: generalize to longer lists,... (test 351 still leaves redundant conjuncts inside let body)
1416		cse_conjunct_predicates2([A,B],R) :- A==B, !, R=A.
1417		cse_conjunct_predicates2(L,R) :- conjunct_predicates(L,R).
1418
1419
1420		% find prefix list of conjuncts which do not use CSEID:
1421		find_prefix_not_using_cse_id([],_CSEID,[],[]).
1422		find_prefix_not_using_cse_id([H|T],CSEID,Prefix,Rest) :-
1423		(uses_cse_id(CSEID,H)
1424		-> Prefix=[], Rest= [H|T]
1425		; % print('NOT USING '), print(CSEID),nl, translate:print_bexpr_or_subst(H),nl,
1426		Prefix = [H|TP],
1427		find_prefix_not_using_cse_id(T,CSEID,TP,Rest)).
1428
1429		% split a conjunct into PREFIX & MAIN & SUFFIX such that PREFIX/SUFFIX do not use CSEID identifier
1430		cse_split_conjunct(Conjunct,CSEID, PREFIX,MAIN,SUFFIX) :-
1431		is_a_conjunct(Conjunct,_,_),
1432		% try removing conjuncts which do not use CSEID by flattening first:
1433		conjunction_to_list(Conjunct,List),
1434		find_prefix_not_using_cse_id(List,CSEID,PREFIX,Rest1),
1435		reverse(Rest1,RevRest1),
1436		find_prefix_not_using_cse_id(RevRest1,CSEID,RevSuffix,RevMain),
1437		(PREFIX \= [] ; RevSuffix \= []), % only succeed if there is a non-trivial split
1438		reverse(RevMain,MAIN),
1439		reverse(RevSuffix,SUFFIX).
1440
1441
1442		% binders which pose problem for lazy_let introduction in case SharedExpression depends on bound variables
1443		non_unary_binder(b(P,_Type,_I),Ids) :-
1444		non_unary_binder_aux(P,Ids,_Left,_Right).
1445		non_unary_binder_aux(forall(Ids,A,B),Ids,A,B).
1446		non_unary_binder_aux(let_predicate(Ids,A,B),Ids,A,B).
1447		% expressions
1448		non_unary_binder_aux(general_sum(Ids,A,B),Ids,A,B).
1449		non_unary_binder_aux(general_product(Ids,A,B),Ids,A,B).
1450		non_unary_binder_aux(quantified_union(Ids,A,B),Ids,A,B).
1451		non_unary_binder_aux(quantified_intersection(Ids,A,B),Ids,A,B).
1452		non_unary_binder_aux(general_product(Ids,A,B),Ids,A,B).
1453		non_unary_binder_aux(event_b_comprehension_set(Ids,A,B),Ids,A,B).
1454		non_unary_binder_aux(lambda(Ids,A,B),Ids,A,B).
1455		non_unary_binder_aux(let_expression(Ids,A,B),Ids,A,B).
1456		%subst
1457		non_unary_binder_aux(let(Ids,A,B),Ids,A,B).
1458		non_unary_binder_aux(any(Ids,A,B),Ids,A,B).
1459		% TO DO: add more subst
1460
1461		% binders which only have a single sub-expression; here we just have to decide whether to introduce the let inside or outside
1462		unary_binder(b(P,_Type,_I),Ids) :-
1463		unary_binder_aux(P,Ids,_Left).
1464		unary_binder_aux(exists(Ids,A),Ids,A).
1465		unary_binder_aux(comprehension_set(Ids,A),Ids,A).
1466
1467
1468		*/