b_expression_sharing

add_cse_used_ids_info(Ids,OldInfos,NewInfos) :-
    exclude(do_not_copy_info_from_sub_terms,OldInfos,OldInfos1),
    NewInfos=[cse_used_ids(Ids)|OldInfos1].

add_invalidated_ids(b(E,T,I),Ids,b(E,T,[invalidate_ids_for_cse(Ids)|I])).

add_invalidated_ids_to_infos(L,[],R) :- !, R=L.

add_invalidated_ids_to_infos(L,Ids,[invalidate_ids_for_cse(Ids)|L]).

already_cse_optimized(b(_E,_T,I)) :- member(cse_optimized,I).

apply_expression_sharing_to_machine(InMachine,OutMachine) :-
    change_sections(InMachine,InExprs,OutExprs,OutMachine),
    create_stores(0,EmptyStores),
    remove_implicit_negation_l(InExprs,NormedExprs),
    find_common_subexpressions_l(NormedExprs,EmptyStores,true,machine,1,OutExprs,Stores,_Stripped,_UsedIds,_UsedCSEIds),
    ground_reference_counters(Stores),!.

boolean(boolean_true).

boolean(boolean_false).

bup_init_acc(Acc3) :- empty_avl(E),
    avl_store('$used_lazy_lookups',E,[]-[],Acc1), % used directly and indirectly
    avl_store('$identifier_uses',Acc1,[],Acc2),
    avl_store('$lazy_lookups_directly_used',Acc2,[],Acc3).

bup_insert_lazy_lookup_if_necessary(BExpr,LAZYLOOKUP,Acc,NewAcc) :-
    BExpr = b(Expr,Type,Info),
    select(sharing(ID,TotalCount,_,_),Info,Info2), % this expressions is marked as being shared
    TotalCount > 1, % with at least two occurrences
    !,
    %cse_check_ast(avl_store(ID),BExpr), % infos only re-established in TD phase
    bup_update_info(Info2,Acc,Info3),
    (lazy_let_to_be_introduced(ID,UsedLL,IntroLL,_,_)
    -> true /* let already introduced; ensure we use same Ids/version everywhere */
    ; get_used_lazy_lookups(Acc,UsedLL,IntroLL),
    avl_fetch('$identifier_uses',Acc,UsedIds),
    % nl, print(lookup(ID,UsedLL,IntroLL)),nl, translate:print_bexpr_or_subst(BExpr), % portray_avl(Acc),nl,
    register_let_id(ID,UsedLL,IntroLL,UsedIds,b(Expr,Type,Info3)) % store that we need to introduce a lazy_let
    ),
    (UsedLL=[] -> true
    ; last(UsedLL,LastLL),
    (ID > LastLL -> true
    ; format('*** LET ~w depends on later id ~w in ~w~n',[ID,LastLL,UsedLL]))
    ),
    ord_union([ID],UsedLL,NewUsedLL),
    ord_union([ID],IntroLL,NewIntroLL),
    avl_store('$lazy_lookups_directly_used',Acc,[ID],Acc1),
    avl_store('$used_lazy_lookups',Acc1,NewUsedLL-NewIntroLL,NewAcc), % to the outside (above) we only see usage of @ID
    bup_update_info(Info2,NewAcc,LazyLookupInfo),
    gen_lazy_lookup(Type,ID,Info2,LazyLookupInfo,LAZYLOOKUP).

bup_insert_lazy_lookup_if_necessary(b(Expr,Type,Info1),b(Expr,Type,Info2),Acc,Acc) :-
    %nl, print('BUP: '),translate:print_bexpr_or_subst(b(Expr,Type,Info1)), portray_avl(Acc),nl,
    bup_update_info(Info1,Acc,Info2).

bup_insert_lazy_lookups(BE,Res,SubAccs,NewAcc) :-
    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
    % combine all infos about lazy_lets from subexpressions:
    merge_bup_accs(SubAccs,Acc),
    bup_update_identifier_uses(BE,Acc,Acc1),
    bup_insert_lazy_lookup_if_necessary(BE2,Res,Acc1,NewAcc).

bup_update_identifier_uses(TExpr,Acc,NewAcc) :-
    avl_fetch('$identifier_uses',Acc,UsedIds),
    get_texpr_expr(TExpr,Expr),safe_syntaxelement(Expr,_Subs,TNames,_,_),
    ( bsyntaxtree:uses_an_identifier(Expr,Id)
    -> ord_add_element(UsedIds,Id,New),avl_store('$identifier_uses',Acc,New,NewAcc)
    ; TNames=[] -> NewAcc=Acc
    ; get_texpr_ids(TNames,Names), % these names are introduced and no longer visible higher up
    sort(Names,SNames),
    ord_subtract(UsedIds,SNames,New),
    avl_store('$identifier_uses',Acc,New,Acc1),
    % now invalidate all lazy_lookups which use an introduced variable name in SNames
    avl_fetch('$used_lazy_lookups',Acc1,All-Intro),
    exclude(filter_lazy_lookup(SNames),All,FAll),
    exclude(filter_lazy_lookup(SNames),Intro,FIntro),
    avl_store('$used_lazy_lookups',Acc1,FAll-FIntro,Acc2),
    avl_fetch('$lazy_lookups_directly_used',Acc2,Direct),
    exclude(filter_lazy_lookup(SNames),Direct,FDirect),
    avl_store('$lazy_lookups_directly_used',Acc2,FDirect,NewAcc)
%,print(filter(SNames,Intro,FIntro)),nl
).

bup_update_info(Info0,Acc,Info4) :-
    delete(Info0,sharing(_,_,_,_),Info1),
    delete(Info1,cse_used_ids(_),Info2),
    get_used_lazy_lookups(Acc,_,InterList),
    avl_fetch('$lazy_lookups_directly_used',Acc,DirectlyUsed),
    Info3=Info2, %Info3 = [cse_used_ids(DirectlyUsed)|Info2],
    ord_intersection(InterList,DirectlyUsed,IntroduceHere), % those not directly used will be introduced automatically inside the shared expressions
    (IntroduceHere=[] -> Info4=Info3
    %,(DirectlyUsed=[] -> true ; print('*** WARNING: directly used not empty: '),print(DirectlyUsed),nl)
    ; Info4 = ['$introduce_lazy_lookups'/IntroduceHere|Info3]). % store info in node for later top-down traversal).

change_section2([],Machine,[],[],Machine).

change_section2([Sec|Rest],InMachine,InExprs,OutExprs,OutMachine) :-
    select_section_texprs(Sec,LInExprs,LOutExprs,InMachine,InterMachine),
    append(LInExprs,RInExprs,InExprs),
    append(LOutExprs,ROutExprs,OutExprs),
    change_section2(Rest,InterMachine,RInExprs,ROutExprs,OutMachine).

change_sections(InMachine,InExprs,OutExprs,OutMachine) :-
    change_section2([constraints,properties,invariant,
    assertions,operation_bodies],
    InMachine,InExprs,OutExprs,OutMachine).

collect_important_info(SubA,SubB,Info) :- (var(SubA) ; var(SubB)), !,
    add_internal_error('Illegal call: ',collect_important_info(SubA,SubB,Info)),fail.

collect_important_info(SubA,SubB,Info) :-
    extract_info(SubA,SubB,Info1), % WD info (bsyntaxtree utility)
    % was collect_uses_cse_id([SubA,SubB],IDS), % CSE usage info
    exclude(do_not_copy_info_from_sub_terms,Info1,Info2), % is this necessary ??
    Info=Info2. %Info = [cse_used_ids(IDS)|Info2].

combine_acc(Acc1,Acc2,NewAcc) :-
    avl_to_list(Acc1,Acc1List),
    empty_avl(Empty),
    combine_acc_aux(Acc1List,Acc2,Empty,NewAcc).

combine_acc_aux([],_Acc2,Res,Res).

combine_acc_aux([Field-Value1|T],Acc2,RAcc,Res) :-
    avl_delete(Field,Acc2,Value2,Acc3),
    (field_combinator(Field,Value1,Value2,NewValue)
    -> avl_store(Field,RAcc,NewValue,RAcc2)
    ; RAcc2=Acc2, Acc3=Acc2),
    combine_acc_aux(T,Acc3,RAcc2,Res).

compute_static_expression(add(A,B),int(Result)) :- % plus
    compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB),
    Result is IA+IB.

compute_static_expression(minus(A,B),int(Result)) :- % plus
    compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB),
    Result is IA-IB.

compute_static_expression(unary_minus(A),int(Result)) :- % plus
    compute_static_int_texpression(A,IA),
    Result is -IA.

compute_static_expression(multiplication(A,B),int(Result)) :-
    compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB),
    Result is IA*IB.

compute_static_expression(div(A,B),int(Result)) :- % TO DO: also add floored_div
    compute_static_int_texpression(B,IB), IB \= 0,
    compute_static_int_texpression(A,IA),
    Result is IA//IB.

compute_static_expression(power_of(A,B),int(Result)) :-
    compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB), IB >= 0,
    safe_pown(IA,IB,Result), number(Result).

compute_static_expression(integer(I),int(I)).

compute_static_expression(value(I),I).

compute_static_expression(equal(A,B),I) :- compute_static_int_texpression(A,SA), compute_static_int_texpression(B,SB),
    (SA==SB -> I = pred_true ; I = pred_false).

compute_static_expression(not_equal(A,B),I) :- compute_static_int_texpression(A,SA), compute_static_int_texpression(B,SB),
    (SA==SB -> I = pred_false ; I = pred_true).

compute_static_int_texpression(b(E,_,_),Result) :- compute_static_expression(E,int(Result)).

construct_seq_tail([],_,[]) :- !.

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

convert_atom_to_nr(Atom,Nr) :- var(Atom),!, add_internal_error('Illegal call: ',convert_atom_to_nr(Atom,Nr)),fail.

convert_atom_to_nr(Atom,Nr) :- atom_codes(Atom,[64|C]), number_codes(Nr,C).

convert_to_atom(A,ID) :- var(A),!, add_internal_error('Illegal call: ', convert_to_atom(A,ID)),fail.

convert_to_atom(A,ID) :- atom(A),!, ID=A.

convert_to_atom(Nr,ID) :- number_codes(Nr,C), atom_codes(ID,[64|C]). % 64 = @

create_initial_expression_cache(A) :-
    expression_sharing_enabled,!,
    A=[Cache],create_subcache(top,Cache).

create_initial_expression_cache(disabled).

create_stores(Start,stores(Start,Empty,Empty,[])) :-
    empty_avl(Empty).

create_stripped(Expr,StrippedSubs,NormStripped) :-
    (cse_syntaxtransformation(Expr,_Subs,_Names,StrippedSubs,Stripped)
    -> norm_strip(Stripped,NormStripped)
    ; add_internal_error('Illegal Expression: ',create_stripped(Expr,StrippedSubs,NormStripped)),
    NormStripped = Expr).

create_subcache(Id,cache(Id,Avl)) :- empty_avl(Avl).

create_substore([],_SubId,Stores,Stores) :- !.

create_substore(NewIds,ID,InStores,SubStores) :-
    force_create_substore(NewIds,ID,InStores,SubStores).

cse_check_ast(_PP,_Pred).

cse_cleanup_aux(E,T,Info,b(NewE,T,NewInfo)) :-
    delete(Info,cse_used_ids(_),Info2),
    ( nonmember(contains_wd_condition,Info2), % TO DO: allow in DISPROVER_MODE
    post_cse_simplifier(E,SE) -> NewE = SE, NewInfo=Info2 % Note: maybe some lets no longer necessary now
    ; reorder_lazy_let_expr(E,T,Info2,NewE,NewInfo) -> true
    ; NewE=E,NewInfo=Info2).

cse_cleanup_infos(b(E,T,Info),Res) :-
    cse_cleanup_infos1(E,T,Info,Res).

cse_cleanup_infos1(lazy_let_pred(ID,SharedExpr,Body),T,_,Res) :-
    collect_important_info(SharedExpr,Body,Info),
    cse_cleanup_aux(lazy_let_pred(ID,SharedExpr,Body),T,Info,Res).

cse_cleanup_infos1(lazy_let_expr(ID,SharedExpr,Body),T,_,Res) :-
    collect_important_info(SharedExpr,Body,Info),
    cse_cleanup_aux(lazy_let_expr(ID,SharedExpr,Body),T,Info,Res).

cse_cleanup_infos1(lazy_let_subst(ID,SharedExpr,Body),T,_,Res) :-
    collect_important_info(SharedExpr,Body,Info),
    cse_cleanup_aux(lazy_let_subst(ID,SharedExpr,Body),T,Info,Res).

cse_cleanup_infos1(sequence(Seq),T,Info,Res) :- !, % re-flatten sequences that were binarized for CSE sharing analysis
    flatten_sequence(Seq,FSeq,WD),
    (WD==contains_wd_condition, nonmember(contains_wd_condition,Info) ->
    Info1 = [contains_wd_condition|Info] ; Info1=Info),
    cse_cleanup_aux(sequence(FSeq),T,Info1,Res).

cse_cleanup_infos1(E,T,Info,Res) :- cse_cleanup_aux(E,T,Info,Res).

cse_optimize_operation(OpName) :-
    b_top_level_operation(OpName),
    b_get_machine_operation(OpName,_Results,_Parameters,Body),
    print(optimizing(OpName)),nl,
    cse_optimize_substitution(Body,_Res).

cse_optimize_predicate(Pred,Res) :- already_cse_optimized(Pred),
    !,
    Res=Pred.

cse_optimize_predicate(Pred,Res) :-
    cse_print_check('Running Common Sub Expressions (CSE) Optimization on ', Pred),
    expand_cse_lazy_lets(Pred,ExpandedPred), % TO DO: see if we can do this more efficiently; do we need it at all ??
    cse_print_check('Expanded Expression: ', ExpandedPred),
    % Note: we can still have unexpanded lazy-lets hanging around in ExpandedPred from outer scopes
    find_maximum_lazy_let_id(ExpandedPred,MaxID), % find maximum ID
    StartNr is MaxID+1, % we will start numbering from there to avoid clashes with existing lazy-lets
    find_common_subexpressions(ExpandedPred,StartNr,true,R,_Refs),
    cse_print_check('Found common sub expressions: ',R),
   
    % print('Common: '),nl, translate:nested_print_bexpr_or_subst(R),nl,nl,nl,
    bup_init_acc(InitialAcc),
    reset_let_dependency_info,
    transform_bexpr_with_bup_accs(b_expression_sharing:bup_insert_lazy_lookups,R,R2,InitialAcc,_BUPAcc),
    %portray_avl(BUPAcc),nl,
    %print_bexpr_or_subst(R2),nl,nl,
    % tools_printing:trace_print(R2,6),nl,nl,
    empty_avl(Empty),
    avl_store('$maximum_unregistered_lazy_let_id',Empty,MaxID,TDAcc),
    top_down_gen_lazy_lets(R2,TDAcc,OptimizedPred),
   
    %cse_print_check('Optimized Expression Result: ',OptimizedPred), % info fields not yet set
    transform_bexpr(b_expression_sharing:cse_cleanup_infos,OptimizedPred,COPred),
    cse_print_check('Cleaned up Optimized Expression Result: ',COPred),
   
    % nl,print('FINISHED CSE: '),nl, translate:nested_print_bexpr_or_subst(COPred),nl, %portray_avl(LastAcc),nl,nl,
    !,
    mark_as_optimized(COPred,Res).

cse_optimize_predicate(P,Res) :-
    add_internal_error('CSE FAILED: ',cse_optimize_predicate(P,Res)),
    Res=P.

cse_optimize_substitution(Subst,Res) :- cse_optimize_predicate(Subst,Res),
    (debug_mode(on) -> nl,print('FINISHED CSE: '),nl, translate:print_subst(Res),nl ; true).

cse_print_check(Msg,Expr) :- debug:debug_mode(on),
    !,
    print(Msg), print_functor(Expr),
    print_bexpr_or_subst(Expr), nl,
    cse_check_ast(Msg,Expr).

cse_print_check(_,_).

cse_syntaxtransformation(assign(LHS,RHS),RHS,[],NRHS,NExpr) :- !, % print(assign(LHS)),nl,
    same_length(RHS,NRHS),
    NExpr=assign(LHS,NRHS).

cse_syntaxtransformation(becomes_element_of(LHS,RHS),[RHS],[],[NRHS],NExpr) :- !,
    NExpr=becomes_element_of(LHS,NRHS).

cse_syntaxtransformation(becomes_such(LHS,RHS),[RHS],[],[NRHS],NExpr) :- !,
    NExpr=becomes_such(LHS,NRHS).

cse_syntaxtransformation(evb2_becomes_such(LHS,RHS),[RHS],[],[NRHS],NExpr) :- !,
    NExpr=evb2_becomes_such(LHS,NRHS).

cse_syntaxtransformation(assign_single_id(Id,RHS),[RHS],[],[NRHS],NExpr) :- !,
    NExpr=assign_single_id(Id,NRHS).

cse_syntaxtransformation(Expr,Subs,Names,NSubs,NExpr) :- syntaxtransformation(Expr,Subs,Names,NSubs,NExpr).

directly_uses_cse_id(E,ID) :- var(E),!, add_internal_error('Illegal call: ',directly_uses_cse_id(E,ID)),fail.

directly_uses_cse_id(lazy_lookup_pred(AtomID),ID) :- convert_atom_to_nr(AtomID,ID).

directly_uses_cse_id(lazy_lookup_expr(AtomID),ID) :- convert_atom_to_nr(AtomID,ID).

do_not_copy_info_from_sub_terms(cse_used_ids(_)). % is_cse_used_ids

do_not_copy_info_from_sub_terms(negated_cse).

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)

do_not_share_this(_,_,_,_,Type,_) :- do_not_share_type(Type),!.

do_not_share_this(_,_Stripped,_,_Functor,_Type,Infos) :-
    memberchk(contains_wd_condition,Infos),
    get_preference(use_common_subexpression_wd_only,true),
    !. % also examine DISPROVER MODE ?

do_not_share_this(_,_Stripped,_,_Functor,Type,_Infos) :- Type==pred,
    get_preference(use_common_subexpression_also_for_predicates,false),
    !.

do_not_share_this(SkipSimple,Stripped,UsedIds,OuterFunctor,_Type,_Infos) :-
    SkipSimple==true,
    do_not_share_this_3(Stripped,UsedIds,OuterFunctor).

do_not_share_this_3(case_or(_,_),_,_) :- !. % why does this have a pred type ?

do_not_share_this_3(if_elsif(_,_),_,_) :- !.

do_not_share_this_3(select_when(_,_),_,_) :- !. % has subst type; so will not be shared

do_not_share_this_3(set_extension(X),_,outer(OuterFunctor,ArgNr)) :- !,
    %nl,print(sx(X,OuterFunctor/ArgNr)),nl,
    (X = [V], simple_explicit_value(V) ; % singleton set with simple value
    set_extension_optimized_treatment_available(OuterFunctor,ArgNr)).

do_not_share_this_3(comprehension_set(_Id,_),_,M) :-
    % optimized treatment available; important for test 1079
    (nmem(M) -> true ; symbolic_set_op(M)). % -> true ; print(share(_Id,M)),nl,nl,fail).

do_not_share_this_3(union(_,_),_,M) :-
    % union often used for composing functions
    (nmem(M) -> true ; symbolic_set_op(M)). % -> true ; print(share_union(M)),nl,nl,fail).

do_not_share_this_3(pow_subset(X),_,M) :- nmem(M) ; infinite_set(X).

do_not_share_this_3(fin_subset(X),_,M) :- nmem(M) ; infinite_set(X).

do_not_share_this_3(pow1_subset(X),_,M) :- nmem(M) ; infinite_set(X).

do_not_share_this_3(fin1_subset(X),_,M) :- nmem(M) ; infinite_set(X).

do_not_share_this_3(struct(_),_,M) :- nmem(M).

do_not_share_this_3(seq(X),_,M) :- nmem(M) ; infinite_set(X).

do_not_share_this_3(iseq(X),_,M) :- nmem(M) ; infinite_set(X).

do_not_share_this_3(perm(_),_,M) :- nmem(M).

do_not_share_this_3(domain(_),_,M) :- nmem(M).

do_not_share_this_3(seq1(X),_,M) :- nmem(M) ; infinite_set(X).

do_not_share_this_3(iseq1(X),_,M) :- nmem(M) ; infinite_set(X).

do_not_share_this_3(identity(X),_,M) :- nmem(M) ; infinite_set(X).

do_not_share_this_3(closure(_),_,M) :- nmem(M).

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)

do_not_share_this_3(external_function_call(FunName,_Args),_,_) :- not_declarative(FunName).

do_not_share_this_3(interval(A,B),_,M) :- nmem(M) ; small_interval(A,B).

do_not_share_this_3(total_function(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).

do_not_share_this_3(total_injection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).

do_not_share_this_3(total_surjection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).

do_not_share_this_3(total_bijection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).

do_not_share_this_3(partial_function(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).

do_not_share_this_3(partial_injection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). % >+>

do_not_share_this_3(partial_surjection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).

do_not_share_this_3(relations(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).

do_not_share_this_3(cartesian_product(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B).

do_not_share_this_3(Stripped,UsedIds,_OuterFunctor) :- too_simple_for_sharing2(Stripped,UsedIds).

do_not_share_type(subst).

do_not_share_type(status). % Event-B Event Status

expand_cse_lazy_lets(Expr,ExpandedExpr) :-
    transform_bexpr(b_expression_sharing:expand_lazy_let,Expr,ExpandedExpr).

expand_cse_lazy_lets_if_cse_enabled(E,EE) :-
    (expression_sharing_enabled -> expand_cse_lazy_lets(E,EE) ; E=EE).

expand_lazy_let(b(E,Type,Info),Result) :- expand_lazy_let_aux(E,Type,Info,Result).

expand_lazy_let_aux(lazy_let_expr(TID,SharedExpr,MainExpr),_,_,Result) :-
    get_texpr_id(TID,ID), debug_println(4,expanding(ID)),
    expand_lazy_lookup(ID,SharedExpr,MainExpr,Result).

expand_lazy_let_aux(lazy_let_pred(TID,SharedExpr,MainExpr),_,_,Result) :-
    get_texpr_id(TID,ID), debug_println(4,expanding(ID)),
    expand_lazy_lookup(ID,SharedExpr,MainExpr,Result).

expand_lazy_let_aux(lazy_let_subst(TID,SharedExpr,MainExpr),_,_,Result) :-
    get_texpr_id(TID,ID), debug_println(4,expanding(ID)),
    expand_lazy_lookup(ID,SharedExpr,MainExpr,Result).

expand_lazy_let_aux(E,Type,Info,Result) :- E \= value(_), E \= integer(_),
    compute_static_expression(E,Val),
    %print(computed(E,Val)),nl,
    Result=b(value(Val),Type,Info).

expand_lazy_lookup(ID,SharedExpr,MainExpr,Result) :- \+ atom(ID),!,
    add_internal_error('Illegal call: ',expand_lazy_lookup(ID,SharedExpr,MainExpr,Result)),
    Result=MainExpr.

expand_lazy_lookup(ID,SharedExpr,MainExpr,Result) :-
    transform_bexpr(b_expression_sharing:replace_lazy_lookup(ID,SharedExpr),MainExpr,Result).

expression_sharing_enabled :-
    get_preference(use_common_subexpression_elimination,true).

fc_parts(TExpr,Expr,Type,Subs,SQuantifiedNewIds,InvalidatedIds,NSubs,OldInfos2,NewInfos,NTExpr) :-
    my_decompose_texpr(TExpr,Expr,Type,OldInfos),
    cse_syntaxtransformation(Expr,Subs,Names,NSubs,NExpr),
    get_texpr_ids(Names,QuantifiedNewIds), list_to_ord_set(QuantifiedNewIds,SQuantifiedNewIds),
    (select(invalidate_ids_for_cse(ModifiedIDs),OldInfos,OldInfos2)
    % we have a stored invalidation info for CSE
    -> InvalidatedIds=ModifiedIDs
    ; InvalidatedIds= [],OldInfos=OldInfos2),
    %functor(Expr,F,A), format('-> ~w/~w : ~w + ~w~n',[F,A,SQuantifiedNewIds,InvalidatedIds]),
    create_texpr(NExpr,Type,NewInfos,NTExpr).

field_combinator('$identifier_uses',Used1,Used2,Used) :- ord_union(Used1,Used2,Used).

field_combinator('$lazy_lookups_directly_used',Used1,Used2,Used) :- ord_union(Used1,Used2,Used).

field_combinator('$used_lazy_lookups',All1-_,AccAll-AccIntro,All-Intro) :-
    ord_union(All1,AccAll,All),
    ord_intersection(All1,AccAll,I1), % an @ID that is in this branch and some other branch
    ord_union([I1,AccIntro],Intro).

filter_lazy_lookup(SortedNames,LazyLookupID) :-
    lazy_let_to_be_introduced(LazyLookupID,_,_,UsedIds,SharedExpr),
    (ord_intersect(SortedNames,UsedIds) % if any of the introduced names is used: filter out lazy lookup
    -> true
    ; get_texpr_info(SharedExpr,Infos),
    memberchk(contains_wd_condition,Infos)
%,print(wd_filter(LazyLookupID)),nl, translate:print_bexpr(SharedExpr),nl
).

find_common_subexpressions(TExpr,Start,SkipSimple,NTExpr) :-
    find_common_subexpressions(TExpr,Start,SkipSimple,NTExpr,_).

find_common_subexpressions(TExpr,Start,SkipSimple,NTExpr,References) :-
    create_stores(Start,EmptyStores),
    find_common_subexpressions2(TExpr,EmptyStores,SkipSimple,root/1,NTExpr,Stores,_Stripped,_UsedIds,_UsedCSEIds),
    ground_reference_counters(Stores),
    get_current_references(Stores,References). % needed ??

find_common_subexpressions2(TExpr,InStores,SkipSimple,OuterFunctor,NTExpr,OutStores,Stripped,UsedIds,UsedCSEIds) :-
    % decompose the typed expression into its components (Subs), look up the newly introduced
    % identifiers (NewIds) and create a new typed expression (NTExpr) with the modified components
    % (NSubs) and the new Info field (Info)
    fc_parts(TExpr,Expr,Type,Subs,NewQuantifiedIds,InvalidatedIds,NSubs,OldInfos,NewInfos,NTExpr),
    % introduce a map from expression to reference that is only visible to this node
    % and it subnodes if new identifiers (NewIds) are introduced
    % OutStores1 and OutStores contain a pattern such that if OutStores1 is set,
    % OutStores is exactly like OutStores1 but without visibility of the newly introduced
    % identifiers.
    append(InvalidatedIds,NewQuantifiedIds,NewIds),
    create_substore(NewIds,ID,InStores,SubStores),
    % apply subexpression detection on the subexpressions
    functor(Expr,OuterExprFunctor,_), % memorise functor for sub-expressions (allows deciding if sharing makes sense)
    find_common_subexpressions_l(Subs,SubStores,SkipSimple,OuterExprFunctor,1,
    NSubs,SubStores1,StrippedSubs,UsedSubIds,SubUsedCSEIds),
    % create a stripped (i.e. no info field, no types) version of the syntax node for look ups
    (Type==subst -> Stripped=not_relevant % substitions are never shared (and everything containing a subst is a subst itself)
    ; create_stripped(Expr,StrippedSubs,Stripped)),
    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 !)
    % merge the used ids of the subnodes with the used ids in this node,
    % subtract newly introduced quantified identifiers because they are not visible from outside
    update_used_ids(Expr,NewQuantifiedIds,UsedSubIds,UsedIds),
    % if a substore was introduced due to newly introduced identifiers, remove it
    %%(OuterExprFunctor=while -> portray_stores(SubStores1) ; true),
    remove_last_substore(NewIds,SubStores1,Stores1,References),
    % try to find the expression in the stores
    (do_not_share_this(SkipSimple,Stripped,UsedIds,OuterFunctor,Type,OldInfos) ->
    OutStores = Stores1,
    add_cse_used_ids_info(SubUsedCSEIds,OldInfos,NewInfos),
    UsedCSEIds = SubUsedCSEIds,
    store_expression(LookupKey,UsedIds,Stores1,_,_,ID) /* just ground ID; used for Sub expressions */
    %, print(not_sharing(ID))
    ; lookup_cse(Type,LookupKey,UsedIds,Stores1,OutStores,SharingInfo,Negated,ID) ->
    /* it is shared */
    % print(looked_up(ID,Negated,used(UsedIds,sub(UsedSubIds)),Stores1)),nl,
    (Negated=negated_cse
    -> NewInfos=[Negated,SharingInfo|OldInfos1]
    ; NewInfos=[SharingInfo|OldInfos1]),
    add_cse_used_ids_info(SubUsedCSEIds,OldInfos,OldInfos1),
    ord_union([ID],SubUsedCSEIds,UsedCSEIds),
    set_references(References,SharingInfo)
    % In this case we do not need to look for sharing in the sub-expressions !!
    %,check_sharing_info(lookup,SharingInfo)
    ;
    % if not found, store the expression: it will be shared if we use it again later
    store_expression(LookupKey,UsedIds,Stores1,OutStores,SharingInfo,ID),
    ord_union([ID],SubUsedCSEIds,UsedCSEIds),
    % print(new_id(ID,UsedIds,SubUsedCSEIds,OutStores)),nl,
    % TO DO: what if later we find out that it is shared after all -> we should remove sub-expression counts
    add_cse_used_ids_info(SubUsedCSEIds,OldInfos,OldInfos1),
    NewInfos=[SharingInfo|OldInfos1],
    set_references(References,SharingInfo)
%,check_sharing_info(new,SharingInfo)
). % print(done_find(NTExpr,OutStores,UsedIds,UsedCSEIds)),nl.

find_common_subexpressions_l([],Stores,_SkipSimple,_OuterFunctor,_,[],Stores,[],[],[]).

find_common_subexpressions_l([Expr|Erest],InStores,SkipSimple,OuterFunctor,ArgNr,
    [NExpr|Nrest],OutStores,[Stripped|Srest],UsedIds,UsedCSEIds) :-
    find_common_subexpressions2(Expr,InStores,SkipSimple,outer(OuterFunctor,ArgNr),NExpr,InterStores,Stripped,UsedIds1,UsedCSEIds1),
    A1 is ArgNr+1,
    find_common_subexpressions_l(Erest,InterStores,SkipSimple,OuterFunctor,A1,Nrest,OutStores,Srest,UsedIds2,UsedCSEIds2),
    ord_union(UsedIds1,UsedIds2,UsedIds), % the B identifiers used
    ord_union(UsedCSEIds1,UsedCSEIds2,UsedCSEIds). % the identifiers to CSE used

find_maximum_lazy_let_id(BExpr,MaxID) :-
    reduce_over_bexpr(b_expression_sharing:find_maximum_lazy_let_id_aux,BExpr,-1,MaxID).

find_maximum_lazy_let_id_aux(lazy_lookup_expr(ID),MaxSoFar,NewMax) :- !,
    convert_atom_to_nr(ID,IDNr),
    (IDNr @> MaxSoFar -> NewMax=IDNr ; NewMax=MaxSoFar).

find_maximum_lazy_let_id_aux(lazy_lookup_pred(ID),MaxSoFar,NewMax) :-
    convert_atom_to_nr(ID,IDNr),
    (IDNr @> MaxSoFar -> NewMax=IDNr ; NewMax=MaxSoFar).

find_maximum_lazy_let_id_aux(_,V,V).

flatten_sequence([H,b(sequence(T),subst,Info)],[H|FT],WD) :- member(cse_generated,Info),
    !,
    % check if this sequence contains a WD condition
    (var(WD),member(contains_wd_condition,Info) -> WD=contains_wd_condition ; true),
    flatten_sequence(T,FT,WD).

flatten_sequence(X,X,_WD).

force_create_substore(Ids,SubId,
    stores(Counter,IR,Top, InSubs),
    stores(Counter,IR,Top, [substore(OrdIds,Empty,SubId,[])|InSubs])) :-
    list_to_ord_set(Ids,OrdIds),
    empty_avl(Empty).

gen_id(A,B,b(identifier(ID),Type,[])) :- get_texpr_type(B,Type),convert_to_atom(A,ID).

gen_lazy_let(pred,A,_UsedIds,SharedExpr,Body,b(R,pred,[])) :-
    % Info field will be set later in cse_cleanup_infos
    !,
    gen_id(A,SharedExpr,ID), debug_println(4,generating_lazy_let_pred(A,ID)),
    R = lazy_let_pred(ID,SharedExpr,Body).

gen_lazy_let(subst,A,_UsedIds,SharedExpr,Body,b(R,subst,[])) :-
    !,
    gen_id(A,SharedExpr,ID), debug_println(4,generating_lazy_let_subst(A,ID)),
    R = lazy_let_subst(ID,SharedExpr,Body).

gen_lazy_let(Type,A,_UsedIds,SharedExpr,C,b(lazy_let_expr(ID,SharedExpr,C),Type,[])) :-
    gen_id(A,SharedExpr,ID).

gen_lazy_lookup(pred,A,Infos,LazyLookupInfo,R) :- !, convert_to_atom(A,ID),
    (member(negated_cse,Infos)
    -> R = b(negation(b(lazy_lookup_pred(ID),pred,LazyLookupInfo)),pred,OuterInfos),
    delete(LazyLookupInfo,'$introduce_lazy_lookups'/_,OuterInfos) % we do not need to generate the lazy_lookups here; they can be created inside the negation
    %,print(create_neg_lookup(ID,LazyLookupInfo,OuterInfos)),nl
    ; R = b(lazy_lookup_pred(ID),pred,LazyLookupInfo)).

gen_lazy_lookup(Type,A,_,LazyLookupInfo,
    b(lazy_lookup_expr(ID),Type,LazyLookupInfo)) :- convert_to_atom(A,ID).

get_current_references(stores(_Counter,IR,TopStore,_Subs),References) :-
    avl_to_list(IR,Refs),
    convlist(reused_expression(TopStore),Refs,References).

get_lazy_lookup_id(b(E,_,_),ID) :- get_lazy_lookup_id_aux(E,ID).

get_lazy_lookup_id(b(E,Type,_),Type,ID) :- get_lazy_lookup_id_aux(E,ID).

get_lazy_lookup_id_aux(lazy_lookup_expr(ID),ID).

get_lazy_lookup_id_aux(lazy_lookup_pred(ID),ID).

get_top_level_functor_arguments(Top,Functor,Args) :- % must also be associative
    functor(Top,Functor,N), !,
    (N=2 -> Top =.. [Functor|Args] % no normalisation applied
    ; arg(1,Top,Args)). % Note: we do not recurse: we assume normalisation has already been applied fully below

get_top_level_functor_arguments(Top,_,[Top]).

get_used_lazy_lookups(Acc,All,Introduce) :-
    (avl_fetch('$used_lazy_lookups',Acc,A-I) -> All=A,Introduce=I
    ; add_internal_error('Failed: ',get_used_lazy_lookups(Acc,All,Introduce)),
    All=[], Introduce=[]).

ground_reference_counter(_Id-rc(C,C)).

ground_reference_counters(stores(_Counter,RefCounter,_TopStore,_SubStores)) :-
    avl_to_list(RefCounter,List),
    maplist(ground_reference_counter,List).

idempotent(conjunct).

idempotent(disjunct).

idempotent(union).