b_ast_cleanup

add_before_after_info(BeforeAfter,TId,TId2) :-
    def_get_texpr_id(TId,Id),
    ( member(ba(Id,BeforeId),BeforeAfter) ->
    get_texpr_type(TId,Type), get_texpr_info(TId,Info),
    create_texpr(identifier(Id),Type,[before_substitution(Id,BeforeId)|Info],TId2)
    ; TId = TId2 ).

add_field_restriction(FieldName,TRHS,FieldsIn,FieldsOut) :-
    (select(field_set(FieldName,OldSet),FieldsIn,F2)
    -> OldSet = b(_,Type,_),
    safe_create_texpr(intersection(OldSet,TRHS),Type,NewSet),
    FieldsOut = [field_set(FieldName,NewSet)|F2]
    ; FieldsOut = [field_set(FieldName,TRHS)|FieldsIn]).

add_hint_message(_,_Msg,_Term,_Span) :- debug_mode(off),
    get_preference(performance_monitoring_on,false), % should we use another preference?
    !.

add_hint_message(Src,Msg,Term,Span) :-
    add_message(Src,Msg,Term,Span).

add_important_info_from_super_expression(Infos,SubInfos,NewSubInfos) :-
    include(important_info_from_super_expression,Infos,Important), % print(add_important(Important)),nl,
    add_infos_if_new(Important,SubInfos,NewSubInfos).

add_important_infos_to_exists_conjuncts(TPred,SuperInfos,SuperIds,NewTPred) :-
    include(important_info_for_exists,SuperInfos,Important),
    (Important=[]
    -> NewTPred=TPred
    ; add_to_conjuncts_aux(TPred,Important,SuperIds,NewTPred)
).

add_one(b(integer(I),integer,_),Res) :- !, I1 is I+1, Res=integer(I1).

add_one(B,add(B,One)) :- one(One).

add_removed_typing_info(Info,ResInfo) :-
    (memberchk(removed_typing,Info) -> ResInfo = Info ; ResInfo = [removed_typing|Info]).

add_to_conjuncts_aux(b(Pred,Type,Infos),Important,SuperIds,b(NP,Type,NewSubInfos)) :-
    (Pred=conjunct(A,B)
    -> NP=conjunct(NA,NB), NewSubInfos=Infos,
    add_to_conjuncts_aux(A,Important,SuperIds,NA),
    add_to_conjuncts_aux(B,Important,SuperIds,NB)
    ; Pred=exists(InnerIds,_), member(TID,InnerIds),
    def_get_texpr_id(TID,ID),
    ord_member(ID,SuperIds) % the exists is probably related to the outer exists
    % (TODO: it could be a lifted clashing one: perform this annotation directly in construct_optimized_exists !!)
    -> append(Important,Infos,NewSubInfos), % copy infos from original exists
    NP=Pred
    ; NP=Pred, NewSubInfos=Infos).

add_used_identifier_info(_Ids,_P,IOld,INew) :-
    member(used_ids(_),IOld),!,INew=IOld.

add_used_identifier_info(Ids,P,IOld,[used_ids(FoundIds)|IOld]) :-
    % add used identifiers to information
    get_sorted_ids(Ids,Ignore),
    find_identifier_uses(P,Ignore,FoundIds).

add_used_ids_defined_by_equality(_Ids,P,IOld,INew) :-
    member(used_ids(UsedIds),IOld),!,
    findall(ID, (member_in_conjunction(Equality,P),
    identifier_equality(Equality,ID,_TID,Expr),
    ord_member(ID,UsedIds),
    not_occurs_in_expr(ID,Expr)), % TO DO: we could check also other ids defined by equality already found
    IdsDefinedByEquality),
    (select(used_ids_defined_by_equality(_),IOld,I1) -> true ; I1=IOld),
    (IdsDefinedByEquality=[] -> INew=I1
    ; %debug_println(9,used_ids_defined_by_equality(IdsDefinedByEquality)),
    INew = [used_ids_defined_by_equality(IdsDefinedByEquality)|I1]
).

add_used_ids_defined_by_equality(Ids,P,IOld,INew) :-
    add_internal_error('No used_ids info:',add_used_ids_defined_by_equality(Ids,P,IOld,INew)),
    INew=IOld.

always_defined_full_check_or_disprover_mode(_) :- preferences:get_preference(disprover_mode,true),!.

always_defined_full_check_or_disprover_mode(BExpr) :- \+ full_check_is_possibly_undefined(BExpr).

always_wd(bool_set).

always_wd(boolean_false).

always_wd(boolean_true).

always_wd(empty_set).

always_wd(identifier(_)).

always_wd(integer(_)).

always_wd(integer_set(_)).

always_wd(real_set).

always_wd(real(_)).

always_wd(string(_)).

always_wd(string_set).

always_wd(truth).

annotate_becomes_such_vars(Ids1,Pred,Ids2) :-
    find_used_primed_ids(Pred,Ids1,BeforeAfter),
    maplist(add_before_after_info(BeforeAfter),Ids1,Ids2).

assure_single_rules([],_Mode,_Rule) :- !.

assure_single_rules(AppliedRules,Mode,Rule) :-
    assure_single_rules2(AppliedRules,Mode,Rule).

assure_single_rules2(_AppliedRules,_,none) :- !.

assure_single_rules2(_AppliedRules,multi,_) :- !.

assure_single_rules2(AppliedRules,_,Rule) :-
    % typically AppliedRules not very long; would also do: \+ member(Rule, AppliedRules).
    ord_nonmember(Rule,AppliedRules).

avoid_top_level_let_within(card(_)). % reification of card does not work yet with top-level let_predicate, for test 1562

binary_inf_comparison(not_equal(A,B),AA,BB) :- sym_unify(A,B,AA,BB).

binary_inf_comparison(less(A,B),AA,BB) :- sym_unify(A,B,AA,BB).

binary_inf_comparison(less_equal(A,B),AA,BB) :- sym_unify(A,B,AA,BB).

binary_inf_comparison(greater(A,B),AA,BB) :- sym_unify(A,B,AA,BB).

binary_inf_comparison(greater_equal(A,B),AA,BB) :- sym_unify(A,B,AA,BB).

can_be_optimized_away(b(_,_,I)) :- nonmember(do_not_optimize_away,I).

can_be_replaced(RHS,_,Ids) :- get_texpr_id(RHS,RHSID),!,
    \+ (member(TID2,Ids), get_texpr_id(TID2,RHSID)). % ID occurs in Ids, replacing it in Expr will move the scope

can_be_replaced(_RHS,UsedIds,Ids) :- % TO DO: compute used ids
    %find_identifier_uses(RHS,[],UsedIds),
    get_texpr_ids(Ids,AtomicIds), sort(AtomicIds,SortedIds),
    \+ ord_intersect(UsedIds,SortedIds).

check_do_not_enum_result(NewInfos,BInfo) :- member(prob_annotation('DO_NOT_ENUMERATE'(_)),BInfo),!,
    findall(DNID,
    (member(prob_annotation('DO_NOT_ENUMERATE'(DNID)),BInfo), DNID \= '$$NONE$$'), OldIds),
    findall(DNID,
    (member(prob_annotation('DO_NOT_ENUMERATE'(DNID)),NewInfos), DNID \= '$$NONE$$'), NewIds),
    (OldIds = NewIds
    -> format('Same DO_NOT_ENUMERATE result: ~w~n',[OldIds])
    ; format('Difference in DO_NOT_ENUMERATE result:~nOLD: ~w~nNEW: ~w~n',[OldIds,NewIds])
).

check_do_not_enum_result(_,_).

check_forall_lhs_rhs(_,_,_,_) :- preferences:get_preference(perform_stricter_static_checks,false),!.

check_forall_lhs_rhs(_,_,_,_) :- preferences:get_preference(disprover_mode,true),!.

check_forall_lhs_rhs(_,_,_,_) :- animation_minor_mode(eventb),!. % typing predicates get removed it seems

check_forall_lhs_rhs(_,_,I,_) :- member(removed_typing,I),!. % means that typing was possibly removed

check_forall_lhs_rhs(Lhs,_,_,_) :- member_in_conjunction(PC,Lhs),
    get_texpr_info(PC,PI),member(II,PI),
    removed_typing(II),!. % it was something else; does not seem to detect all removed conjunctions, hence we also check I above

check_forall_lhs_rhs(P,_,I,Ids) :- find_identifier_uses_if_necessary(P,[],LhsUsed),
    ord_subtract(Ids,LhsUsed,NotDefined),
    NotDefined=[_|_],
    ajoin_with_sep(NotDefined,',',S),
    translate:translate_bexpression(P,PS),
    ajoin(['Left-hand side "', PS, '" of forall does not define identifier(s): '],Msg),
    add_warning(bmachine_static_checks,Msg,S,I),
    fail.

check_forall_lhs_rhs(_,Rhs,I,Ids) :-
    find_identifier_uses_if_necessary(Rhs,[],RhsUsed),
    (ord_intersect(Ids,RhsUsed) -> true
    ; ajoin_with_sep(Ids,',',S),
    add_warning(bmachine_static_checks,'Right-hand side of forall does not use identifiers: ',S,I)
).

check_generated_info(Info,Rule,Path) :-
    get_preference(prob_safe_mode,true),
    (select(used_ids(_),Info,I1) -> member(used_ids(_),I1)),!,
    format('Illegal used ids generated by ~w within ~w~n Infos=~w~n',[Rule,Path,Info]),
    add_internal_error('Illegal Info generated by rule: ',Rule),
    fail.

check_generated_info(_,_,_).

check_ids([],[CoupleExpr],CoupleExpr). % we terminate with a single expression

check_ids([ID|T],[CoupleExprID|CT],Rest) :-
    same_id(ID,CoupleExprID,_),
    check_ids(T,CT,Rest).

check_is_just_type(_A) :- preferences:get_preference(ignore_prj_types,true),!.

check_is_just_type(A) :- (is_just_type(A) -> true ; debug_println(9,not_type_for_prj(A)),fail).

check_used_ids_info(Parameters,Predicate,StoredUsedIds,PP) :-
    % get_global_identifiers(Ignored), and add to Parameters ??
    (add_used_identifier_info(Parameters,Predicate,[],[used_ids(UsedIds)])
    -> (StoredUsedIds=UsedIds -> true
    ; ord_subset(UsedIds,StoredUsedIds)
    -> format('Suboptimal used_ids info: ~w (actual ~w) [origin ~w with ~w]~n',[StoredUsedIds,UsedIds,PP,Parameters])
    %, print_bexpr(Predicate),nl
    ; add_internal_error('Incorrect used_ids info: ', check_used_ids_info(Parameters,Predicate,UsedIds,PP)),
    print_bexpr(Predicate),nl,
    (extract_span_description(Predicate,PosMsg) -> format('Location: ~w~n',[PosMsg]) ; true),
    ord_subtract(UsedIds,StoredUsedIds,Delta),
    format('Incorrect used_ids info: ~w (actual ~w)~nNot included: ~w~n~n',[StoredUsedIds,UsedIds,Delta])
    %, print_bexpr(Predicate),nl
    )
    ; add_internal_error('Could not computed used ids:',
    add_used_identifier_info(Parameters,Predicate,[],[used_ids(_)]))
).

clean_up(Expr,NonGroundExceptions,CExpr) :- % clean-up with init
    clean_up_init(NonGroundExceptions,Expr,Expr1),
    clean_up_aux(Expr1,NonGroundExceptions,CExpr,[]).

clean_up_aux(Expr1,NonGroundExceptions,CExpr,Path) :- % performs no init
    (preferences:get_preference(normalize_ast,true)
    -> cleanups(normalize,Expr1,[],Expr2,Path)
    ; Expr2=Expr1),
    cleanups(pre,Expr2,[],TPExpr,Path),
    remove_bt(TPExpr,PExpr,LExpr,TLExpr),
    syntaxtransformation(PExpr,Subs,_,NewSubs,LExpr),
    functor(PExpr,F,N),
    % recursively clean up sub-expressions
    clean_up_l(Subs,NonGroundExceptions,NewSubs,F/N,1,Path),
    cleanups(post,TLExpr,[],CExpr,Path).

clean_up_init(NonGroundExceptions,Expr,Expr2) :-
    % ensure that WD info is available also for pre phase
    % also pre-transform large set_extensions; they are only later transformed using eval_set_extension
    (transform_bexpr_td_with_scoping(b_ast_cleanup:try_evaluate_set_extension,Expr,Expr1),
    transform_bexpr(b_ast_cleanup:compute_wd_info_and_norm_record_types(NonGroundExceptions),Expr1,Expr2) -> true
    ; add_internal_error('Call failed:',clean_up_init(NonGroundExceptions,Expr,Expr1)), Expr2=Expr).

clean_up_l([],_,[],_Functor,_Nr,_Path).

clean_up_l([Expr|Rest],NonGroundExceptions,[CExpr|CRest],Functor,ArgNr,Path) :-
    clean_up_aux(Expr,NonGroundExceptions,CExpr,[path_arg(Functor,ArgNr)|Path]),
    A1 is ArgNr+1,
    clean_up_l(Rest,NonGroundExceptions,CRest,Functor,A1,Path).

clean_up_l_with_opt([],_,[],_Functor,_Nr,_Path).

clean_up_l_with_opt([Expr|Rest],NonGroundExceptions,[CExpr|CRest],Functor,ArgNr,Path) :-
    %print('Cleaning up: '),translate:print_bexpr_or_subst(Expr),nl,
    clean_up_init(NonGroundExceptions,Expr,Expr1),
    clean_up_pred_or_expr_with_path(NonGroundExceptions,Expr1,CExpr,[path_arg(Functor,ArgNr)|Path]),
    A1 is ArgNr+1,
    clean_up_l_with_opt(Rest,NonGroundExceptions,CRest,Functor,A1,Path).

clean_up_l_with_optimizations(Rest,NonGroundExceptions,CRest,Context) :-
    %clean_up_l(Rest,NonGroundExceptions,CRest,top_level,1,[]).
    (clean_up_l_with_opt(Rest,NonGroundExceptions,CleanedUpRest,top_level(Context),1,[]) -> CRest=CleanedUpRest
    ; add_internal_error('Call failed:',clean_up_l_with_optimizations(Rest,NonGroundExceptions,CRest,Context)),
    CRest=Rest
).

clean_up_l_wo_optimizations(Rest,NonGroundExceptions,CRest,SectionName) :-
    maplist(clean_up_init(NonGroundExceptions),Rest,Rest1),
    clean_up_l(Rest1,NonGroundExceptions,CRest,top_level(SectionName),1,[]).

clean_up_pred(Expr,NonGroundExceptions,CleanedUpExpr) :-
    clean_up(Expr,NonGroundExceptions,CExpr),
    (get_texpr_type(CExpr,pred)
    -> predicate_level_optimizations(CExpr,CleanedUpExpr)
    ; add_internal_error('Not predicate: ',clean_up_pred(Expr,NonGroundExceptions,CleanedUpExpr)),
    CleanedUpExpr = CExpr).

clean_up_pred_or_expr(NonGroundExceptions,Expr,CleanedUpExpr) :-
    clean_up_pred_or_expr_with_path(NonGroundExceptions,Expr,CleanedUpExpr,[]).

clean_up_pred_or_expr_with_path(NonGroundExceptions,Expr,CleanedUpExpr,Path) :-
    clean_up_init(NonGroundExceptions,Expr,Expr1),
    clean_up_aux(Expr1,NonGroundExceptions,CExpr,Path),
    (get_texpr_type(CExpr,pred)
    -> predicate_level_optimizations(CExpr,CleanedUpExpr,Path)
    ; CleanedUpExpr = CExpr).

cleanup_comprehension_set([TID],b(member(LHS,TSet),pred,_),Type,I,Set,I2,multi/remove_useless_comprehension_set) :-
    get_texpr_id(TID,ID),
    get_texpr_id(LHS,ID),
    % {ID|ID:Set} ==> Set
    not_occurs_in_expr(ID,TSet),
    TSet=b(Set,Type,I2),
    !,
    add_hint_message(remove_useless_comprehension_set,'Removing useless comprehension set over: ',ID,I).

cleanup_comprehension_set([TID],Body,_Type,I,NewExpr,NewInfo,single/detect_seq_comprehension_set) :-
    get_texpr_id(TID,ID),
    % {ID | #LenID. (ID : 1..LenID --> Set)} ==> seq(Set)
    % {ID | #LenID. (ID : 1..LenID >-> Set)} ==> iseq(Set)
    get_texpr_expr(Body,exists([TLen],TIBody)),
    get_texpr_id(TLen,LenID), LenID \= ID,
    get_texpr_expr(TIBody,IBody),
    get_member(IBody,LenID,ISet,TID2,FUNCTION),
    get_texpr_id(TID2,ID),
    get_seq_fun_aux(FUNCTION,ISet,Interval,SeqTypeSet),
    get_texpr_expr(Interval,interval(ONE,TLen2)),
    get_texpr_id_with_offset(TLen2,LenID,Offset), % LenID or something like LenID-1
    get_integer(ONE,StartingIndex),!,
    (StartingIndex = 1, Offset=0 % TODO: check if a negative offset is always ok for all Seq Types
    -> add_hint_message(detect_seq_comprehension_set,'Detecting sequence operator: ',ID,I),
    NewExpr = SeqTypeSet, NewInfo=I
    ; % we have something sequence like but with indexes not starting at 1, maybe at 0
    % e.g. {ID | #LenID. (ID : 0..LenID-1 --> Set)}; happens in Soton/UML-B drone model
    add_hint_message(detect_seq_comprehension_set,'Marking sequence like operator as symbolic, indexes are not starting at 1: ',ID,I),
    NewExpr = comprehension_set([TID],Body),
    %add_texpr_infos(Body,[prob_annotation('SYMBOLIC')],Body2),
    add_info_if_new(I,prob_annotation('SYMBOLIC'),NewInfo)
).

cleanup_comprehension_set([TID],Body, _Type, I, range(Func), I, multi/detect_tla_range_comprehension_set) :-
    Body = b(exists([DomTID],EBody),pred,_),
    EBody = b(conjunct(LHS,RHS),pred,_),
    is_membership(LHS,DomTID1,b(domain(Func),_,_)),
    same_id(DomTID,DomTID1,_),
    is_equality(RHS,TID1,FunCall),
    FunCall = b(function(Func1,DomTID2),_,_),
    same_id(TID,TID1,_),
    same_id(DomTID,DomTID2,_),
    same_texpr(Func,Func1),
    always_well_defined_or_disprover_mode(FunCall), % we could also allow TLA minor mode
    add_hint_message(detect_tla_range_comprehension_set,'Detected range set-comprehension: ',Func,I).

cleanup_comprehension_set([TID],Pred,Type,I,
    struct(b(rec(NewFieldSets),record(FieldTypes),I)),
    I,single/simplify_record) :-
    % {r|r'a : 1..1000 & r'b : 1..100 & r:struct(a:INTEGER,b:NAT,c:BOOL)} --> struct(a:1..1000,b:1..100,c:BOOL)
    % these kind of set comprehensions are generated by ProZ, see ROZ example model.tex test 1858
    % TO DO: maybe generalise this optimisation: currently it only works if all predicates can be assimilated into struct expression
    TID = b(identifier(ID),record(FieldTypes),_),
    conjunction_to_list(Pred,PL),
    l_update_record_field_membership(PL,ID,[],FieldSetsOut),
    maplist(construct_field_sets(FieldSetsOut),FieldTypes,NewFieldSets),
    (debug_mode(off) -> true
    ; print('Detected Record set comprehension: '),
    print_bexpr(b(struct(b(rec(NewFieldSets),record(FieldTypes),I)),Type,I)),nl).

cleanup_comprehension_set(Ids1,E,_Type,I,comprehension_set(Ids2,E2),I,single/detect_lambda) :-
    preferences:get_preference(detect_lambdas,true),
    % used to lead to *** Enumerating lambda result warnings for test 1162, not anymore
    % does not yet detect: f = {x,y|x:NATURAL & (x> 1 &y=x+2)} & res = f[3..4]
    E = b(conjunct(LHS,Equality),pred,Info),
    nonmember(prob_annotation('LAMBDA'),Info), % not already processed
    identifier_equality(Equality,ID,TID1,Expr1),
    last(Ids1,TID), get_texpr_id(TID,ID),
    not_occurs_in_expr(ID,Expr1),
    not_occurs_in_predicate([ID],LHS),
    !,
    get_texpr_info(Equality,EqInfo),
    get_unique_id_inside('_lambda_result_',LHS,Expr1,ResultId), % currently the info field lambda_result is not enough: several parts of the ProB kernel match on the identifier name '_lambda_result_'
    TID1 = b(identifier(_),Type1,Info1),
    add_texpr_infos(b(identifier(ResultId),Type1,Info1),[lambda_result(ResultId),lambda_result_id_was(ID)],TID2),
    Equality2 = b(equal(TID2,Expr1),pred,[prob_annotation('LAMBDA-EQUALITY')|EqInfo]),
    E2 = b(conjunct(LHS,Equality2),pred,[prob_annotation('LAMBDA')|Info]),
    append(Ids0,[_],Ids1),
    append(Ids0,[TID2],Ids2),
    % code exists which is simpler, but has disadvantage of losing position info for equality
    (debug_mode(off) -> true ; format('Lambda using ~w detected: ',[ID]),print_bexpr(E2),nl).

cleanup_function_projection(first_projection(A,B),Argument,I,Result) :-
    gen_assertion_expression(A,B,Argument,first_of_pair(Argument),first,I,Result).

cleanup_function_projection(second_projection(A,B),Argument,I,Result) :-
    gen_assertion_expression(A,B,Argument,second_of_pair(Argument),second,I,Result).

cleanup_function_projection(event_b_second_projection(A),Argument,_I,Result) :- % old style Rodin projection
    check_is_just_type(A),Result = first_of_pair(Argument).

cleanup_function_projection(event_b_second_projection(A),Argument,_I,Result) :- % old style Rodin projection
    check_is_just_type(A),Result = second_of_pair(Argument).

cleanup_function_projection(event_b_first_projection_v2,Argument,_I,Result) :- Result = first_of_pair(Argument).

cleanup_function_projection(event_b_second_projection_v2,Argument,_I,Result) :- Result = second_of_pair(Argument).

cleanup_normalize(Expr,Type,Info,NewExpr,NewType,NewInfo, multi/apply_normalization_rule(Rule)) :-
    b_ast_cleanup_rewrite_rules:normalization_rule_with_rename(Expr,Type,Info,NewExpr,NewType,NewInfo,Rule),
    (debug_mode(off) -> true
    ; format('Use rewrite_rule_normalize ~w~n',[Rule]),
    print_bexpr(b(NewExpr,NewType,NewInfo)),nl
    ),
    (ground(NewExpr) -> true
    ; print(not_ground_rewrite(Rule,Type,Info)),nl,
    write(Expr),nl, write(' --> '),nl, write(NewExpr),nl,
    fail).

cleanup_phase(Phase,OTExpr,NTExpr,Mode/Rule,Path) :-
    create_texpr(OExpr,OType,OInfo,OTExpr),
    check_generated_info(OInfo,entry,Path),
    create_texpr(NExpr,NType,NInfo,NTExpr),
    cleanup_phase2(Phase,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path),
    check_generated_info(NInfo,Rule,Path).

cleanup_phase2(normalize,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,_Path) :-
    decompose_rule(Mode_Rule,Mode,Rule),
    cleanup_normalize(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule),
    (debug_mode(off) -> true
    ; print('Rewritten: '), print_bexpr(b(OExpr,OType,OInfo)),nl,
    print(' Into: '), print_bexpr(b(NExpr,NType,NInfo)),nl
).

cleanup_phase2(pre,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path) :-
    decompose_rule(Mode_Rule,Mode,Rule),
    cleanup_pre_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,Path).

cleanup_phase2(post,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path) :-
    decompose_rule(Mode_Rule,Mode,Rule),
    cleanup_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,Path).

cleanup_post(conjunct(b(truth,pred,I1),b(B,pred,I2)),pred,I0,B,pred,NewI,multi/remove_truth_conj1) :- !,
    include_important_info_from_removed_pred(I1,I2,I3), % ensure was,... information propagated
    add_important_info_from_super_expression(I0,I3,NewI).

cleanup_post(conjunct(b(A,pred,I2),b(truth,pred,I1)),pred,I0,A,pred,NewI,multi/remove_truth_conj2) :- !,
    include_important_info_from_removed_pred(I1,I2,I3),
    add_important_info_from_super_expression(I0,I3,NewI).

cleanup_post(conjunct(b(falsity,pred,I1),b(_,_,I2)),pred,I0,falsity,pred,NewI,multi/simplify_falsity_conj1) :- !,
    include_important_info_from_removed_pred(I2,I1,I3),
    add_important_info_from_super_expression(I0,I3,NewI).

cleanup_post(conjunct(LHS,b(falsity,pred,I2)),pred,I0,falsity,pred,NewI,multi/simplify_falsity_conj2) :-
    always_well_defined_or_wd_reorderings_allowed(LHS), % we can only improve WD here,
    % also checks allow_improving_wd_mode preference
    !, % Note: ProB would treat falsity first anyway; so in principle this could be done always for solving
    get_texpr_info(LHS,I1),
    include_important_info_from_removed_pred(I1,I2,I3),
    add_important_info_from_super_expression(I0,I3,NewI).

cleanup_post(conjunct(AA,BB),pred,I,Res,pred,I,multi/modus_ponens) :-
    Impl = b(implication(A,B),pred,_),
    ((AA,BB) = (Impl,A2) ; (BB,AA) = (Impl,A2)),
    same_texpr(A,A2),
    % arises e.g., for predicates such as IF x:0..3 THEN y=2 ELSE 1=0 END ; works with simplify_falsity_impl3 rule
    % rewrite (A=>B) & A into (A&B)
    !,
    (debug_mode(off) -> true ; print('Modus Ponens: '),print_bexpr(A), print(' => '), print_bexpr(B),nl),
    Res = conjunct(A,B).

cleanup_post(conjunct(LHS,b(Comparison1,pred,_)),pred,I0,Result,pred,RInfo,multi/detect_interval1) :-
    % X <= UpBound & X >= LowBound <=> X : UpBound .. LowBound (particularly useful when CLPFD FALSE, causes problem with test 1771)
    % Note: x>18 & y<1024 & x<20 & y>1020 now works, it is bracketed ((()) & y>1020)
    get_preference(use_clpfd_solver,false),
    \+ data_validation_mode, % this rule may lead to additional enumerations
    get_leq_comparison(Comparison1,X,UpBound),
    select_conjunct(b(Comparison2,_,_),LHS,Prefix,Suffix),
    get_geq_comparison(Comparison2,X2,LowBound),
    same_texpr(X,X2),
    (always_well_defined_or_disprover_mode(UpBound)
    -> true
    ; % as we may move valuation earlier, we have to be careful
    % we check if Comparison2 is last conjunct; x=7 & x:8..(1/0) raises no WD error in ProB
    Suffix=[]
    ),
    !,
    create_interval_member(X,LowBound,UpBound,Member),
    append(Prefix,[Member|Suffix],ResultList),
    conjunct_predicates(ResultList,TResult),
    TResult = b(Result,pred,I1),
    add_important_info_from_super_expression(I0,I1,RInfo),
    (debug_mode(off) -> true ; print(' Detected interval membership (1): '),print_bexpr(b(Result,pred,RInfo)),nl).

cleanup_post(conjunct(LHS,b(Comparison1,pred,_)),pred,I0,Result,pred,RInfo,multi/detect_interval2) :-
    % X >= LowBound & X <= UpBound <=> X : UpBound .. LowBound
    get_preference(use_clpfd_solver,false),
    \+ data_validation_mode, % this rule may lead to additional enumerations
    get_geq_comparison(Comparison1,X,LowBound),
    select_conjunct(b(Comparison2,_,_),LHS,Prefix,Suffix),
    get_leq_comparison(Comparison2,X2,UpBound),
    same_texpr(X,X2),
    (always_well_defined_or_disprover_mode(LowBound)
    -> true
    ; % as we may move valuation earlier, we have to be careful
    % we check if Comparison2 is last conjunct; x=7 & x:8..(1/0) raises no WD error in ProB
    Suffix=[]
    ),
    !,
    create_interval_member(X,LowBound,UpBound,Member),
    append(Prefix,[Member|Suffix],ResultList),
    conjunct_predicates(ResultList,TResult),
    TResult = b(Result,pred,I1),
    add_important_info_from_super_expression(I0,I1,RInfo),
    (debug_mode(off) -> true ; print(' Detected interval membership (2): '),print_bexpr(b(Result,pred,RInfo)),nl).

cleanup_post(disjunct(b(truth,pred,I1),_),pred,I0,truth,pred,I,multi/simplify_truth_disj1) :- !,
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(disjunct(b(A,pred,I1),b(falsity,pred,_)),pred,I0,A,pred,I,multi/remove_falsity_disj1) :- !,
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(disjunct(b(falsity,pred,_),b(B,pred,I1)),pred,I0,B,pred,I,multi/remove_falsity_disj2) :- !,
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(disjunct(Expr1,b(truth,pred,I1)),pred,I0,truth,pred,I,multi/simplify_truth_disj2) :-
    always_well_defined_or_wd_reorderings_allowed(Expr1), !, % we can only improve WD here
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(disjunct(Equality1,Equality2),pred,I,New,pred,I,multi/rewrite_disjunct_to_member1) :-
    identifier_equality(Equality2,ID,_,Expr2),
    always_well_defined_or_disprover_mode(Expr2),
    get_texpr_type(Expr2,Type2),
    type_contains_no_sets(Type2), % we do not want to generate sets of sets, or worse sets with infinite sets (x=NATURAL1 or ...) which cannot be converted to AVL
    identifier_equality(Equality1,ID,TID,Expr1),
    % Rewrite (ID = Expr1 or ID = Expr2) into ID: {Expr1,Expr2} ; good if FD information can be extracted for ID
    % But: can be bad for reification, in particular when set extension cannot be computed fully
    % TO DO: also deal with ID : {Values} and more general extraction of more complicated disjuncts
    % TO DO: also apply for implication (e.g., ID /= E1 => ID=E2)
    !,
    construct_set_extension(Expr1,Expr2,SetX),
    New=member(TID,SetX),
    (debug_mode(off) -> true
    ; format('Rewrite disjunct (1) ~w: ',[ID]),print_bexpr(SetX),nl).

cleanup_post(disjunct(LHS1,LHS2),pred,I,New,pred,I,multi/rewrite_disjunct_to_member2) :-
    id_member_of_set_extension(LHS2,ID,TID1,LExpr2), % also detects equalities
    get_texpr_type(TID1,Type),
    get_preference(use_clpfd_solver,true),type_contains_fd_index(Type), % merging is potentially useful
    maplist(always_well_defined_or_disprover_mode,LExpr2), % TODO: check that merging makes sense, e.g., definite FD values or simple identfiiers
    id_member_of_set_extension(LHS1,ID,TID,LExpr1),
    % Rewrite (ID : {Expr1,...} or ID : {Expr2,...} into ID: {Expr1,Expr2}
    l_construct_set_extension(LExpr1,LExpr2,SetX),
    New=member(TID,SetX),
    (debug_mode(off) -> true
    ; format('Rewrite disjunct (2) ~w: ',[ID]),print_bexpr(SetX),nl).

cleanup_post(disjunct(P1,NegP1),pred,Info,truth,pred,Info,multi/tautology_disjunction) :-
    % P1 or not(P1) == truth (was created by Rodin for WD)
    (get_texpr_expr(NegP1,negation(P1bis)) -> same_texpr(P1,P1bis)
    ; get_texpr_expr(P1,negation(NP1)) -> same_texpr(NP1,NegP1)),
    (debug_mode(off) -> true
    ; format('Detected useless disjunction (tautology): ',[]),print_bexpr(b(disjunct(P1,NegP1),pred,Info)),nl).

cleanup_post(disjunct(CEquality1,CEquality2),pred,IOld,New,pred,INew,multi/factor_common_pred_in_disjunction) :-
    % (x=2 & y=3) or (x=2 & y=4) -> x=2 & (y=3 or y=4) to improve constraint propagation
    factor_disjunct(CEquality1,CEquality2,IOld,New,INew),
    (debug_mode(off) -> true
    ; format('Factor disjunct: ',[]),print_bexpr(b(New,pred,INew)),nl).

cleanup_post(implication(b(truth,pred,_),b(B,pred,I1)),pred,I0,B,pred,I,multi/remove_truth_impl1) :- !,
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(implication(b(falsity,pred,I1),_),pred,I0,truth,pred,I,multi/simplify_falsity_impl1) :- !,
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(implication(_,b(truth,pred,I1)),pred,I0,truth,pred,I,multi/simplify_truth_impl2) :- !,
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(implication(P,b(falsity,pred,_)),pred,I,NotP,pred,[was(implication)|I],multi/simplify_falsity_impl3) :- !,
    create_negation(P,TNotP),
    (debug_mode(off) -> true ; print_bexpr(P), print(' => FALSE simplified'),nl),
    get_texpr_expr(TNotP,NotP).

cleanup_post(equivalence(b(truth,pred,_),b(B,pred,I1)),pred,I0,B,pred,I,multi/remove_truth_equiv1) :- !,
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(equivalence(b(A,pred,I),b(truth,pred,I1)),pred,I0,A,pred,I,multi/remove_truth_equiv2) :- !,
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(lazy_let_pred(_ID,_,b(Sub,pred,I1)),pred,I0,Sub,pred,I,multi/remove_lazy_let_pred) :-
    (Sub=truth ; Sub=falsity), !,
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(IFTHENELSE,T,_,Res,T,[was(ifthenelse)|NI],single/remove_if_then_else) :-
    explicit_if_then_else(IFTHENELSE,IF,THEN,ELSE),
    (is_falsity(IF) -> b(Res,_,NI)=ELSE
    ; is_truth(IF) -> b(Res,_,NI)=THEN
    ),
    (debug_mode(off) -> true
    ; print('Simplified IF-THEN-ELSE: '), print_bexpr(IF),nl).

cleanup_post(member(X,B),pred,I,truth,pred,[was(member(X,B))|I],multi/remove_type_member) :-
    is_just_type(B),
    nonmember(label(_),I), % the user has explicitly labeled this conjunct
    !. % print('REMOVE: '),print_bexpr(b(member(X,B),pred,[])),nl, print(I),nl.

cleanup_post(not_member(X,B),pred,I,falsity,pred,[was(not_member(X,B))|I],multi/remove_type_not_member) :-
    is_just_type(B),
    nonmember(label(_),I), % the user has explicitly labeled this conjunct
    !.

cleanup_post(member(X,TSet),pred,I,equal(X,One),pred,I,multi/remove_member_one_element_set) :-
    singleton_set_extension(TSet,One),
    !,
    % X:{One} <=> X=One
    true. %,print('Introducing equality: '),print_bexpr(X), print(' = '), print_bexpr(One),nl.

cleanup_post(member(X,b(Set,_,_)),pred,I,not_equal(X,One),pred,I,multi/remove_member_setdiff) :-
    Set = set_subtraction(MaximalSet,SONE),
    singleton_set_extension(SONE,One),
    definitely_maximal_set(MaximalSet),
    !, % x : INTEGER-{One} <=> x/=One
    (debug_mode(off) -> true
    ; print('Replacing member of set_subtraction: '), print_bexpr(MaximalSet), print(' - '), print_bexpr(SONE),nl).

cleanup_post(not_member(X,TSet),pred,I,not_equal(X,One),pred,I,multi/remove_member_one_element_set) :-
    singleton_set_extension(TSet,One),
    !,
    % X/:{One} <=> X/=One
    true.

cleanup_post(member(E,b(fin_subset(E2),_,_)),pred,I,finite(E),pred,I,multi/introduce_finite) :-
    (same_texpr(E,E2); is_just_type(E2)),!. % print(introduce(finite(E))),nl.

cleanup_post(not_member(E,b(fin_subset(E2),_,_)),pred,I,NotFinite,pred,I,multi/introduce_not_finite) :-
    (same_texpr(E,E2); is_just_type(E2)),!,
    create_negation(b(finite(E),pred,I),TNotP), get_texpr_expr(TNotP,NotFinite).

cleanup_post(member(b(couple(A,B),couple(TA,TB),IC),b(reverse(Rel),_,_)),pred,I,member(ICouple,Rel),pred,I,multi/remove_reverse) :- !,
    % (A,B) : Rel~ ===> (B,A) : Rel
    % can be detrimental for performance when A is known and B is not and Rel is large
    \+ data_validation_mode,
    (debug_mode(off) -> true ; print('Removed inverse (~): '),print_bexpr(Rel),nl),
    ICouple = b(couple(B,A),couple(TB,TA),IC).

cleanup_post(member(LHS,ITE),pred,I,Result,pred,I,multi/member_if_then_else) :-
    get_texpr_expr(ITE,if_then_else(IFPRED,THEN,ELSE)),
    (definitely_empty_set(ELSE)
    -> A=THEN, P = IFPRED
    ; definitely_empty_set(THEN)
    -> A=ELSE, create_negation(IFPRED,P)
    ),
    % x: IF P THEN A ELSE {} END --> P & x:A
    % x: IF P THEN {} ELSE A END --> not(P) & x:A
    % appears in some generated Caval machines
    % x: IF a=TRUE THEN {11} ELSE {} END & x>11 can now be solved deterministically
    MEM = b(member(LHS,A),pred,I),
    conjunct_predicates([P,MEM],TR),
    (debug_mode(off) -> true ; print('Replace member of if-then-else by: '),print_bexpr(TR),nl),
    get_texpr_expr(TR,Result).

cleanup_post(member(LHS,Comprehension),pred,I,Result,pred,NewInfo,multi/remove_member_comprehension) :-
    Comprehension = b(ComprSet,_,_),
    is_comprehension_set(ComprSet,[TID],Body),
    get_texpr_id(TID,ID),
    % LHS:{x|P(x)} ==> P(LHS)
    replace_id_by_expr_with_count(Body,ID,LHS,TResult,Count),
    % rewrite could duplicate LHS: not an issue in CSE mode; optimization relevant in normalize_ast mode
    is_replace_id_by_expr_ok(LHS,ID,Count,remove_member_comprehension),
    !,
    % could introduce LET if necessary because ID occurs multiple times (Count>1)
    get_texpr_expr(TResult,Result),
    get_texpr_info(TResult,I1),
    add_important_info_from_super_expression(I,I1,NewInfo),
    (debug_mode(off) -> true ; print('Remove element of comprehension_set: '),print_bexpr(Comprehension),nl,
    format(' rewriting to (~w): ',[Count]),print_bexpr(TResult),nl).

cleanup_post(not_member(LHS,Comprehension),pred,I,Result,pred,I,multi/remove_not_member_comprehension) :-
    Comprehension = b(ComprSet,_,_),
    is_comprehension_set(ComprSet,[TID],Body),
    get_texpr_id(TID,ID),
    % LHS/:{x|P(x)} ==> not(P(LHS))
    replace_id_by_expr_with_count(Body,ID,LHS,TResult,Count),
    % rewrite could duplicate LHS: not an issue in CSE mode; optimization relevant in normalize_ast mode
    is_replace_id_by_expr_ok(LHS,ID,Count,remove_not_member_comprehension),
    !,
    Result = negation(TResult),
    (debug_mode(off) -> true ; print('Remove not element of comprehension_set: '),print_bexpr(Comprehension),nl,
    format(' rewriting to (~w): not(',[Count]),print_bexpr(TResult),print(')'),nl).

cleanup_post(comprehension_set(Ids,Body),Type,I,NewExpr,Type,I2,Rule) :-
    cleanup_comprehension_set(Ids,Body,Type,I,NewExpr,I2,Rule),
    !.

cleanup_post(subset(A,B),pred,I,truth,pred,[was(subset(A,B))|I],multi/remove_type_subset) :-
    is_just_type(B),
    nonmember(label(_),I), % the user has explicitly labeled this conjunct
    !.

cleanup_post(not_subset(A,B),pred,I,falsity,pred,[was(not_subset(A,B))|I],multi/remove_type_not_subset) :-
    is_just_type(B),
    nonmember(label(_),I), % the user has explicitly labeled this conjunct
    !.

cleanup_post(SUB,pred,I,NewPred,pred,[generated_conjunct|I],multi/replace_subset_by_element) :-
    is_subset(SUB,A,B),
    is_set_extension(A,List),
    !, % for sequence extension we don't need this as the interpreter knows exactly the cardinality of a sequence_extension ?
    % applying rule {x1,x2,...} <: B <=> x1:B & x2:B & ...
    maplist(gen_member_predicates(B),List,Conjuncts),
    conjunct_predicates(Conjuncts,TNewPred),
    % print('detected subset-member rule: '),print_bexpr(TNewPred),nl,
    get_texpr_expr(TNewPred,NewPred).

cleanup_post(SUB,pred,I,NewPred,pred,[generated_conjunct|I],multi/replace_union_subset) :-
    is_subset(SUB,A,B),
    % mark conjunct as generated: used e.g. by flatten_conjunct in predicate_evaluator
    get_texpr_expr(A,union(_,_)),!,
    % applying rule A1 \/ A2 <: B <=> A1 <: B & A2 <: B
    % could be detrimental if checking that something is an element of B is expensive
    extract_unions(A,As),
    findall(Subi,(member(Ai,As),safe_create_texpr(subset(Ai,B),pred,I,Subi)),Conj), % we could try and re-run clean-up ? safe_create_texpr will ensure WD info set
    conjunct_predicates(Conj,TNewPred),
    get_texpr_expr(TNewPred,NewPred).

cleanup_post(Comp,pred,I,SComp,pred,I,multi/simplify_cse_comparison) :-
    % simplify comparison operations; can result in improved constraint propagation
    % e.g., ia + CSE1 * 2 > ia + fa <=> CSE1 * 2 > fa for Setlog/prob-ttf/qsee-TransmitMemoryDumpOk21_SP_3.prob
    comparison(Comp,A,B,SComp,SA,SB),
    simplify_comparison_terms(A,B,SA,SB),!,
    (debug_mode(off) -> true
    ; print('Simplified: '),print_bexpr(b(Comp,pred,I)),
    print(' <=> '),print_bexpr(b(SComp,pred,I)),nl).

cleanup_post(EMPTYSET,T,I,empty_set,T,[was(EMPTYSET)|I],multi/detect_emptyset) :- EMPTYSET \= empty_set,
    definitely_empty_set(b(EMPTYSET,T,I)),
    (debug_mode(off) -> true
    ; print('Detected empty set: '), print_bexpr(b(EMPTYSET,T,I)),nl).

cleanup_post(equal(A,B),pred,I,truth,pred,[was(equal(A,B))|I],multi/remove_equality) :-
    same_texpr(A,B),always_well_defined_or_disprover_mode(A),!. % ,print(removed_equal(A,B)),nl.

cleanup_post(equal(A,B),pred,I,equal(A2,B2),pred,I,multi/simplify_equality) :-
    simplify_equality(A,B,A2,B2).

cleanup_post(not_equal(A,B),pred,I,not_equal(A2,B2),pred,I,multi/simplify_inequality) :-
    simplify_equality(A,B,A2,B2).

cleanup_post(equal(A,B),pred,I,falsity,pred,[was(equal(A,B))|I],multi/remove_equality_false) :-
    different_texpr_values(A,B),!. %,print(removed_equal_false(A,B)),nl.

cleanup_post(equal(A,B),pred,I,greater(Low,Up),pred,I,multi/remove_equality) :-
    % Low..Up = {} <=> Low>Up % is also handled by constraint solver; but other simplifications can apply here
    (definitely_empty_set(B), is_interval(A,Low,Up) ;
    definitely_empty_set(A), is_interval(B,Low,Up)),!,
    (debug_mode(off) -> true
    ; print('Simplified: '), print_bexpr(b(equal(A,B),pred,I)), print(' <=> '),
    print_bexpr(b(greater(Low,Up),pred,I)),nl).

cleanup_post(CardGt0Expr,pred,I,not_equal(X,EmptySet),pred,I,multi/remove_cardgt0) :-
    get_geq_comparison(CardGt0Expr,Card,One),
    % card(P) > 0 -> P\={} if wd guaranteed; also rewrites card(P) >= 1
    Card = b(card(X),integer,_), get_integer(One,1),
    finite_set_or_disprover_mode(X), % as we keep X, it is sufficient for X to be finite for the rule to be ok
    get_texpr_type(X,TX), get_texpr_info(One,I0),
    EmptySet = b(empty_set,TX,I0),!,
    (debug_mode(off) -> true ; print('Removed card(.) > 0 for set: '), print_bexpr(X), nl).

cleanup_post(CardEq0Expr,pred,I,equal(X,EmptySet),pred,I,multi/remove_cardeq0) :-
    is_equality(b(CardEq0Expr,pred,I),Card,Zero),
    % card(P) = 0 -> P={} if wd guaranteed
    Card = b(card(X),integer,_), get_integer(Zero,0),
    finite_set_or_disprover_mode(X),
    get_texpr_type(X,TX), get_texpr_info(Zero,I0),
    EmptySet = b(empty_set,TX,I0),!,
    (debug_mode(off) -> true ; print('Removed card(.) = 0 for set: '), print_bexpr(X), nl).

cleanup_post(CardLt1Expr,pred,I,equal(X,EmptySet),pred,I,multi/remove_cardlt1) :-
    get_leq_comparison(CardLt1Expr,Card,Zero),
    % card(P) <= 0 -> P={} if wd guaranteed; TODO: also detect card(P) < 1
    Card = b(card(X),integer,_), get_integer(Zero,0),
    finite_set_or_disprover_mode(X),
    get_texpr_type(X,TX), get_texpr_info(Zero,I0),
    EmptySet = b(empty_set,TX,I0),!,
    (debug_mode(off) -> true ; print('Removed card(.) <= 0 for set: '), print_bexpr(X), nl).

cleanup_post(member(Card,Natural),pred,I,truth,pred,I,multi/remove_card_natural) :-
    % card(P) : NATURAL -> truth if wd guaranteed
    Card = b(card(X),integer,_),
    is_integer_set(Natural,'NATURAL'),
    always_well_defined_or_disprover_mode(Card),
    !,
    (debug_mode(off) -> true ; print('Removed card(.):NATURAL for set: '), print_bexpr(X), nl).

cleanup_post(not_equal(A,B),pred,I,less_equal(Low,Up),pred,I,multi/remove_equality) :-
    % Low..Up \= {} <=> Low<=Up % is also handled by constraint solver; but other simplifications can apply here
    (definitely_empty_set(B), is_interval(A,Low,Up) ;
    definitely_empty_set(A), is_interval(B,Low,Up)),!,
    (debug_mode(off) -> true
    ; print('Simplified: '), print_bexpr(b(equal(A,B),pred,I)), print(' <=> '),
    print_bexpr(b(less_equal(Low,Up),pred,I)),nl).

cleanup_post(equal(A,B),pred,I,equal(A,RLet),pred,I,single/detect_recursion) :-
    % "A" should be an identifier
    get_texpr_id(A,ID),
    % check if some side conditions are fulfilled where the recursion detection can be enabled
    recursion_detection_enabled(A,B,I),
    % A must be recursively used in B:
    find_recursive_usage(B,ID),
    % TO DO: also find mutual recursion !
    debug_println(9,recursion_detected(ID)),
    !, % create an recursive_let where the body is annotated to be symbolic
    get_texpr_type(B,Type), add_texpr_infos(B,[prob_annotation('SYMBOLIC')],B2),
    mark_recursion(B2,ID,B3),
    %print(marked_recursion(ID)),nl,
    safe_create_texpr(recursive_let(A,B3),Type,RLet).

cleanup_post(recursive_let(TID,TBody),T,_,Body,T,I2,single/remove_recursive_let) :- get_texpr_id(TID,ID),
    \+ occurs_in_expr(ID,TBody),
    debug_println(19,removing_recursive_let(ID)), % required for test 1225
    TBody = b(Body,_,I2).

cleanup_post(equal(A,B),pred,Info1,ResultExpr,pred,Info3,multi/simplify_bool_true_false) :-
    % simplify bool(X)=TRUE -> X and bool(X)=FALSE -> not(X)
    ( get_texpr_expr(A,convert_bool(X)), get_texpr_boolean(B,BOOLVAL)
    ;
    get_texpr_boolean(A,BOOLVAL),get_texpr_expr(B,convert_bool(X))
    ),
    get_texpr_info(X,Info2),
    add_important_info_from_super_expression(Info1,Info2,Info3),
    (BOOLVAL = boolean_true -> get_texpr_expr(X,ResultExpr) ;
    BOOLVAL = boolean_false -> create_negation(X,TNX), get_texpr_expr(TNX,ResultExpr)),
    !,
    (debug_mode(off) -> true
    ; format('Simplifying bool(.)=~w to ',[BOOLVAL]),translate:print_bexpr(b(ResultExpr,pred,Info3)),nl).

cleanup_post(not_equal(A,B),pred,I,falsity,pred,[was(not_equal(A,B))|I],multi/remove_disequality) :-
    same_texpr(A,B),always_well_defined_or_disprover_mode(A),!. % ,print(removed_not_equal(A,B)),nl.

cleanup_post(not_equal(A,B),pred,I,truth,pred,[was(not_equal(A,B))|I],multi/remove_disequality_false) :-
    different_texpr_values(A,B),!. % ,print(removed_not_equal_false(A,B)),nl.

cleanup_post(not_equal(A,B),pred,I,NewP,pred,[was(not_equal(A,B))|I],multi/not_disjoint_disequality) :-
    /* Set1 /\ Set2 /= {} <===> #(zz).(zz:Set1 & zz:Set2) */
    preferences:preference(use_smt_mode,true), /* currently this rewriting makes test 1112 fail; TO DO: investigate */
    definitely_empty_set(B),
    get_texpr_expr(A,intersection(Set1,Set2)),!,
    get_texpr_type(Set1,Set1Type), unify_types_strict(Set1Type,set(T)),
    ID = b(identifier('_zzzz_unary'),T,[generated]),
    ESet1 = b(member(ID,Set1),pred,[]),
    ESet2 = b(member(ID,Set2),pred,[]),
    create_exists_opt([ID],[ESet1,ESet2],NewPredicate),
    (debug_mode(off) -> true
    ; print('Transformed not disjoint disequality: '),print_bexpr(NewPredicate),nl),
    get_texpr_expr(NewPredicate,NewP).

cleanup_post(equal(b(intersection(A,B),_,_),Empty),pred,I,not_equal(El1,El2),pred,[was(intersection)|I],multi/detect_not_equal) :-
    % {El1} /\ {El2} = {} --> El1 \= El2 (disjoint sets)
    singleton_set_extension(A,El1),
    singleton_set_extension(B,El2),
    definitely_empty_set(Empty).

cleanup_post(equal(b(intersection(A,B),_,_),Empty),pred,I,NewDisequality,pred,[was(intersection)|I],multi/detect_disjoint_set_extensions) :-
    % {El1,...} /\ {El2,...} = {} --> El1 \= El2 & .... (disjoint sets)
    get_texpr_expr(A,set_extension(Els1)), length(Els1,Len1), Len1 < 20,
    get_texpr_expr(B,set_extension(Els2)), length(Els2,Len2), Len2 < 20,
    Len1 * Len2 < 100,
    definitely_empty_set(Empty),
    maplist(simple_expression,Els1), % avoid duplication of computation
    maplist(simple_expression,Els2), % ditto
    findall(NotEqual, (member(A1,Els1),member(B1,Els2),safe_create_texpr(not_equal(A1,B1),pred,NotEqual)),
    NotEquals),
    conjunct_predicates(NotEquals,TRes),
    (debug_mode(off) -> true
    ; write('Expanding disjoint set constraint: '),translate:print_bexpr(TRes),nl
    ),
    get_texpr_expr(TRes,NewDisequality).

cleanup_post(greater(A,B),pred,I,Res,pred,[was(greater(A,B))|I],multi/eval_greater) :-
    get_integer(A,IA), get_integer(B,IB),
    (IA>IB -> Res = truth ; Res=falsity).

cleanup_post(less(A,B),pred,I,Res,pred,[was(less(A,B))|I],multi/eval_less) :-
    get_integer(A,IA), get_integer(B,IB),
    (IA<IB -> Res = truth ; Res=falsity).

cleanup_post(greater_equal(A,B),pred,I,Res,pred,[was(greater_equal(A,B))|I],multi/eval_greater_equal) :-
    get_integer(A,IA), get_integer(B,IB),
    (IA >= IB -> Res = truth ; Res=falsity).

cleanup_post(less_equal(A,B),pred,I,Res,pred,[was(less_equal(A,B))|I],multi/eval_less_equal) :-
    get_integer(A,IA), get_integer(B,IB),
    (IA =< IB -> Res = truth ; Res=falsity).

cleanup_post(CHOOSE,real,I,div_real(A,B),real,I,multi/replace_tla_real_division) :-
    is_tla_real_division(CHOOSE,A,B),
    % Detect TLA real division defined by Div_1(a, b) == CHOOSE({m|m:REAL & m*b=a})
    add_debug_message(ast_cleanup,'Translated TLA+ division to real division: ',b(div_real(A,B),real,I),I).

cleanup_post(negation(A),pred,I,falsity,pred,[was(negation(A))|I],multi/remove_negation_truth) :-
    is_truth(A),!. % ,print(negation(A)),nl.

cleanup_post(negation(A),pred,I,truth,pred,[was(negation(A))|I],multi/remove_negation_falsity) :-
    is_falsity(A),!. % ,print(negation(A)),nl.

cleanup_post(convert_bool(A),boolean,I,Res,boolean,I,multi/remove_convert_bool) :-
    (is_truth(A) -> Res = boolean_true
    ; is_falsity(A) -> Res = boolean_false
    ; is_equality(A,LHS,BoolTRUE), get_texpr_boolean(BoolTRUE,boolean_true) % bool(LHS=TRUE) --> LHS
    -> get_texpr_expr(LHS,Res)
    ; A=not_equal(LHS,BoolFALSE), get_texpr_boolean(BoolFALSE,boolean_false) % bool(LHS/=FALSE) --> LHS
    -> get_texpr_expr(LHS,Res)
    ),!.

cleanup_post(assertion_expression(Cond,_ErrMsg,Expr),_T,I0,BE,TE,IE,multi/remove_assertion_expression) :-
    is_truth(Cond),!,
    Expr = b(BE,TE,I1),
    add_important_info_from_super_expression(I0,I1,IE).

cleanup_post(card(INTERVAL), T, I, Res, T, I, single/card_of_interval) :-
    % e.g., card(1..4) -> 4
    is_interval(INTERVAL, LowerBound, UpperBound),
    get_integer(LowerBound, L),
    number(L),
    get_integer(UpperBound, U),
    number(U),
    (L > U -> Card = 0 ; Card is 1+(U - L)),
    !,
    Res = integer(Card).

cleanup_post(member(Empty,TPow),T,I,Res,T,I,single/empty_set_in_pow_subset) :-
    definitely_empty_set(Empty), % useful for z3 integration to prevent powerset constraint
    TPow = b(POW,_,_),
    (POW=pow_subset(_) -> RT=truth
    ; POW=fin_subset(_) -> RT=truth
    ; POW=pow1_subset(_) -> RT=falsity
    ; POW=fin1_subset(_) -> RT=falsity),
    always_well_defined_or_disprover_mode(TPow),
    !,
    Res = RT.

cleanup_post(card(Empty),T,I,Res,T,I,single/card_singleton_set) :-
    Empty = b(empty_set,_,_), % useful for z3 integration to prevent cardinality constraint
    !,
    Res = integer(0).

cleanup_post(card(SONE),T,I,Res,T,I,single/card_singleton_set) :-
    singleton_set_extension(SONE,One), % card({One}) = 1 ; useful for alloy2b
    always_well_defined_or_disprover_mode(One),
    !,
    Res = integer(1).

cleanup_post(cartesian_product(A,B),T,I,Res,T,I,single/cartesian_product_to_pair) :-
    singleton_set_extension(A,El1),
    singleton_set_extension(B,El2), % {A}*{B} -> {A|->B} ; happens in Alloy translations a lot
    !,
    get_texpr_type(El1,T1), get_texpr_type(El2,T2),
    safe_create_texpr(couple(El1,El2),couple(T1,T2),Pair),
    Res = set_extension([Pair]).

cleanup_post(image(Fun,Empty),T,I,empty_set,T,I,multi/image_empty_optimisation) :-
    definitely_empty_set(Empty),
    always_well_defined_or_wd_improvements_allowed(Fun),
    !,
    (debug_mode(off) -> true
    ; add_message(ast_cleanup,'Removing unnecessary image of empty set: ',Fun,I)).

cleanup_post(union(A,B),T,I,Res,T,[add_element_to_set|I],multi/add_element_to_set) :- % multi: cycle check done in info field
    \+ member(add_element_to_set,I),
    ( singleton_set_extension(B,_El) -> Res = union(A,B)
    ; singleton_set_extension(A,_El) -> Res = union(B,A)),
    !. %,print(detected_add_singleton_element(_El)),nl.

cleanup_post(union(A,B),T,I,Res,T,I,multi/union_empty_set) :-
    ( definitely_empty_set(A) -> get_texpr_expr(B,Res) % {} \/ B = B
    ; definitely_empty_set(B) -> get_texpr_expr(A,Res) % A \/ {} = A
    ),
    !.

cleanup_post(intersection(A,B),T,I,empty_set,T,I,multi/intersection_empty_set) :-
    ( definitely_empty_set(A) -> true % A /\ {} = {}
    ; definitely_empty_set(B) -> true % {} /\ B = {}
    ),
    !.

cleanup_post(set_subtraction(A,B),T,I,Res,T,I,multi/intersection_empty_set) :-
    ( definitely_empty_set(A) -> Res=empty_set % {} - B = {}
    ; definitely_empty_set(B) -> get_texpr_expr(A,Res) % A - {} = A
    ),
    !.

cleanup_post(general_union(SetExt),Type,I0,Res,Type,Info,multi/general_union_set_extension) :- % union_generalized
    % union({a,b,c,...}) = a \/ b \/ c ...
    SetExt = b(set_extension(LIST),_,I1),
    add_important_info_from_super_expression(I0,I1,Info),
    % no need to apply rule if already transformed into avl in cleanup_pre, hence we do not call is_set_extension
    construct_union_from_list(LIST,Type,Info,TRes),
    !,
    (debug_mode(on) -> print('translated_general_union: '), print_bexpr(TRes),nl ; true),
    get_texpr_expr(TRes,Res).

cleanup_post(general_intersection(SetExt),Type,I0,Res,Type,Info,multi/general_inter_set_extension) :- % inter_generalized
    % inter({a,b,c,...}) = a /\ b /\ c ...
    SetExt = b(set_extension(LIST),_,I1),
    add_important_info_from_super_expression(I0,I1,Info),
    % no need to apply rule if already transformed into avl in cleanup_pre, hence we do not call is_set_extension
    construct_inter_from_list(LIST,Type,Info,TRes),
    !,
    (debug_mode(on) -> print('translated_general_intersection: '), print_bexpr(TRes),nl ; true),
    get_texpr_expr(TRes,Res).

cleanup_post(SUB,pred,I0,FORALL,pred,FInfo,multi/general_union_subset) :-
    is_subset(SUB,UNION,T),
    % union(S) <: T ===> !x.(x:S => x <: T)
    % currently: subsets of T may be generated, but it does not propagate well to S
    UNION = b(general_union(S),_,_),
    !,
    get_unique_id_inside('_zzzz_unary',S,T,ID),
    get_texpr_type(S,SType), is_set_type(SType,IDType),
    TID = b(identifier(ID),IDType,[generated]),
    safe_create_texpr(member(TID,S),pred,LHS),
    safe_create_texpr(subset(TID,T),pred,RHS),
    create_implication(LHS,RHS,NewForallBody),
    create_forall([TID],NewForallBody,TFORALL),
    TFORALL = b(FORALL,pred,I1),
    add_important_info_from_super_expression(I0,I1,FInfo),
    % see test 1854, and ProZ ROZ/model.tex
    (debug_mode(on) -> print('translated_general_union subset: '), print_bexpr(TFORALL),nl ; true).

cleanup_post(size(Seq),integer,Info,Res,integer,Info,multi/size_append) :-
    get_texpr_expr(Seq,concat(A,B)),
    % size(A^B) = size(A)+size(B) useful e.g. for test 1306
    !,
    Res = add(b(size(A),integer,Info),b(size(B),integer,Info)).

cleanup_post(concat(A,B),Type,I0,Seq,Type,[was(concat)|NewInfo],multi/concat_empty) :-
    ( definitely_empty_set(A) -> b(Seq,_,I1)=B
    ; definitely_empty_set(B) -> b(Seq,_,I1)=A
    ),!,
    add_important_info_from_super_expression(I0,I1,NewInfo).

cleanup_post(concat(A,B),Type,I0,Seq,Type,[was(concat)|I0],multi/concat_singleton_seq) :-
    ( is_singleton_sequence(B,Element) -> Seq = insert_tail(A,Element)
    ; is_singleton_sequence(A,Element) -> Seq = insert_front(Element,B)
    ),!,
    debug_format(19,'Concat with singleton sequence detected~n',[]).

cleanup_post(E,integer,I,Res,integer,[was(Operator)|I],multi/constant_expression) :-
    pre_compute_static_int_expression(E,Result),!,
    functor(E,Operator,_),
    % format('Precomputed: ~w for ',[Result]), translate:print_bexpr(b(E,integer,[])),nl,
    Res = integer(Result).

cleanup_post(min(Interval),integer,I0,Res,integer,Info,multi/eval_min_interval) :-
    is_interval_or_singleton(Interval,Low,Up),
    get_integer(Low,L), number(L),
    get_integer(Up,U), number(U), L =< U, % non-empty interval
    debug_println(5,simplified_min_interval(L,U,L)),
    Res = integer(L), get_texpr_info(Low,I1),
    add_important_info_from_super_expression(I0,I1,Info).

cleanup_post(max(Interval),integer,I0,Res,integer,Info,multi/eval_max_interval) :-
    is_interval_or_singleton(Interval,Low,Up),
    get_integer(Low,L), number(L),
    get_integer(Up,U), number(U), L =< U, % non-empty interval
    debug_println(5,simplified_max_interval(L,U,U)),
    Res = integer(U), get_texpr_info(Low,I1),
    add_important_info_from_super_expression(I0,I1,Info).

cleanup_post(first(Seq),Type,I0,Res,Type,Info,multi/first_seq_extension) :-
    is_sequence_extension(Seq,List), List = [First|Rest],
    (Rest == [] -> true ; preferences:get_preference(disprover_mode,true)), % we may remove WD issue otherwise (TO DO: check if Rest contains any problematic elements)
    !,
    First = b(Res,Type,I1),
    add_important_info_from_super_expression(I0,I1,Info).

cleanup_post(last(Seq),Type,I0,Res,Type,Info,multi/first_seq_extension) :-
    is_sequence_extension(Seq,List), List = [First|Rest],
    (Rest == [] -> true ; preferences:get_preference(disprover_mode,true)), % we may remove WD issue otherwise (TO DO: check if list contains any problematic elements)
    !,
    last([First|Rest],b(Res,Type,I1)),
    add_important_info_from_super_expression(I0,I1,Info).

cleanup_post(function(Fun,Arg),Type,Info,New,Type,NewInfo,Rule) :-
    cleanup_post_function(Fun,Arg,Type,Info,New,NewInfo,Rule).

cleanup_post(range(SETC),Type,I, comprehension_set(RangeIds2,NewCompPred),Type,I,single/range_setcompr) :-
    % translate ran({x1,...xn|P}) into {xn| #(x1,...).(P)} ; particularly interesting if x1... contains large datavalues (e.g., C_02_001.mch from test 1131)
    get_texpr_expr(SETC,comprehension_set(CompIds,CompPred)),
    get_domain_range_ids(CompIds,DomainIds,RangeIds), % print(range(CompIds,DomainIds,RangeIds)),nl,
    %\+((member(ID,RangeIds),get_texpr_id(ID,'_lambda_result_'))), % for test 612; maybe disable optimisation if memory consumption of variables small
    !, % TO DO: also detect patterns such as dom(dom( or ran(ran( ... [Done ??]
    rename_lambda_result_id(RangeIds,CompPred,RangeIds2,CompPred1),
    rename_lambda_result_id(DomainIds,CompPred1,DomainIds2,CompPred2),
    create_outer_exists_for_dom_range(DomainIds2,CompPred2,NewCompPred), % will mark the exists; so that during expansion we will treat it differently for enumeration
    (debug_mode(off) -> true
    ; print('Encode range as existential quantification: '), print_bexpr(NewCompPred),nl).

cleanup_post(domain(SETC),Type,I, comprehension_set(DomainIds2,NewCompPred),Type,I,single/domain_setcompr) :-
    % translate dom({x1,...xn|P}) into {x1,..| #(xn).(P)} ; particularly interesting if xn contains large datavalues
    % used to fail test 306 ; fixed by allow_to_lift_exists annotation
    \+ data_validation_mode, % sometimes this optimisation is counter-productive for data_validation, problem: test 1945
    get_texpr_expr(SETC,comprehension_set(CompIds,CompPred)),
    get_domain_range_ids(CompIds,DomainIds,RangeIds), % print(domain(CompIds,DomainIds,RangeIds)),nl,
    % \+ (member(ID,CompIds),get_texpr_id(ID,'_lambda_result_')),
    % WE HAVE TO BE CAREFUL if xn = LAMBDA_RESULT ; TO DO rename like above for range
    % example from test 292: rel(fnc({x,y|x:1..10 & y:1..x})) = {x,y|x:1..10 & y:1..x}
    %\+ data_validation_mode, % test 1945 fails with WD errors if we disable this rule
    !,
    % TO DO: detect when closure is lambda; e.g., for e.g. dom(pred) = INTEGER in test 292 : split(CompIds,Args,Types), closures:is_lambda_value_domain_closure(Args,Types,B, DomainValue, _),; currently create_exists_opt deals with most of this
    rename_lambda_result_id(DomainIds,CompPred,DomainIds2,CompPred1),
    rename_lambda_result_id(RangeIds,CompPred1,RangeIds2,CompPred2),
    create_outer_exists_for_dom_range(RangeIds2,CompPred2,NewCompPred),
    (debug_mode(off) -> true
    ; get_texpr_ids(DomainIds,DIS), get_texpr_ids(RangeIds,RIS),
    ajoin(['Encode domain over ',DIS,' as existential quantification over ',RIS,' : '],Msg),
    add_message(ast_cleanup,Msg,NewCompPred,I)).

cleanup_post(domain(SETC),Type,I, comprehension_set(DomainIds,RestPred),Type,I,single/domain_setcompr) :-
    % translate dom({x1,...xn|P & xn=E}) into {x1,..| P} ; particularly interesting if xn contains large datavalues
    get_texpr_expr(SETC,comprehension_set(CompIds,CompPred)),
    get_domain_range_ids(CompIds,DomainIds,RangeIds), % print(domain(CompIds,DomainIds,RangeIds)),nl,
    \+ (member(ID,CompIds),get_texpr_id(ID,'_lambda_result_')),
    conjunction_to_list(CompPred,Preds),
    RangeIds = [TId],
    get_sorted_ids(RangeIds,Blacklist),
    select_equality(TId,Preds,Blacklist,_Eq,_Expr,RestPreds,_,check_well_definedness), % We could do check_well_definedness only if preference set
    conjunct_predicates_with_pos_info(RestPreds,RestPred),
    not_occurs_in_predicate(Blacklist,RestPred),
    !,
    % TO DO: use create_optimized exists; also treat inner existential quantification and merge
    (debug_mode(off) -> true
    ; write('Encode domain of lambda abstraction: '),print_bexpr(RestPred),nl).

cleanup_post(precondition(TP,TS),subst,I0,S,subst,Info,multi/remove_triv_precondition) :-
    % remove trivial preconditions
    get_texpr_expr(TP,truth),!,
    get_texpr_expr(TS,S),get_texpr_info(TS,I1),
    add_important_info_from_super_expression(I0,I1,Info).

cleanup_post(external_function_call('ENUM',[TA]),T,I,A,T,[prob_annotation('ENUM')|I],single/process_ENUM) :-
    (debug_mode(on) -> format(' Processing ENUM (~w): ',[T]),translate:print_bexpr(TA),nl ; true),
    % TO DO: do not process in DEFINITION of ENUM in LibraryProB.def
    get_texpr_expr(TA,A).

cleanup_post(comprehension_set(TIds,Body),T,I1,comprehension_set(TIds,Body2),T,I1,single/detect_lambda_result_auto) :-
    get_texpr_info(Body,BI),
    (TIds=[_,_,_|_] % check if at least three ids
    -> true % for example useful here: {x,y,v| x:INTEGER & y:INTEGER & #z.(z=x+1 & x = y*y & v=z*z & y:1..10)} it could be useful to detect x as DO_NOT_ENUMERATE; currently we only enable this analysis for four ids at least
    ; nonmember(prob_annotation('LAMBDA'),BI) % it is a lambda with one argument, no use to do analysis
    ),
    perform_do_not_enumerate_analysis(TIds,Body,'SET COMPREHENSION',I1,Body2).

cleanup_post(comprehension_set(Ids1,E1),T,I,comprehension_set(Ids2,E2),T,I,multi/detect_lambda_result_user_ann) :-
    get_texpr_expr(DNE,external_pred_call('DO_NOT_ENUMERATE',[TID])),
    get_texpr_id(TID,ID),
    member_in_conjunction(DNE,E1),
    NewInfo = prob_annotation('DO_NOT_ENUMERATE'(ID)), % similar to lambda_result
    E1 = b(PRED,pred,I1),
    nonmember(NewInfo,I1),
    get_texpr_id(TID,ID),
    nth1(Pos,Ids1,TID1,Rest),
    add_texpr_infos(TID1,[NewInfo],TID2),
    nth1(Pos,Ids2,TID2,Rest),
    add_message(detect_lambda_result,'Annotating comprehension set identifier with DO_NOT_ENUMERATE: ',ID,I1),
    E2 = b(PRED,pred,[NewInfo|I1]).

cleanup_post(record_field(b(rec(Fields),TR,IR),Field),T,I,FieldVal,T,I, single/remove_field_access) :-
    always_well_defined_or_disprover_mode(b(rec(Fields),TR,IR)),
    member(field(Field,TFieldVal),Fields),!,
    (debug_mode(off) -> true ; add_message(remove_field_access,'Remove static field access: ',Field,I)), % cf test 1294
    get_texpr_expr(TFieldVal,FieldVal).

cleanup_post(sequence([S1,b(sequence(S2),subst,_)]),subst,I,sequence([S1|S2]),subst,I, single/flatten_sequence2) :-
    debug_println(9,flatten_sequence2). % do we need something for longer sequences?

cleanup_post(sequence([b(sequence(S1),subst,_)|S2]),subst,I,sequence(NewSeq),subst,I, single/flatten_sequence1) :-
    append(S1,S2,NewSeq),
    % avoid maybe calling filter_useless_subst_in_sequence again
    debug_println(9,flatten_sequence1).

cleanup_post(sequence(S1),subst,I,sequence(S2),subst,I, single/remove_useless_subst_in_seuence) :-
    get_preference(useless_code_elimination,true),
    filter_useless_subst_in_sequence(S1,Change,S2), debug_println(filter_sequence(9,Change)).

cleanup_post(sequence(Statements),subst,I,Result,subst,I, single/sequence_to_multi_assign) :-
    % merge sequence of assignments if possible
    merge_assignments(Statements,Merge,New), Merge==merged,
    construct_sequence(New,Result).

cleanup_post(parallel(Statements),subst,I,Result,subst,I, single/parallel_to_multi_assign) :-
    % this merges multiple assignments into a single one: advantage: only one waitflag set up
    % should probably not be done in INITIALISATION
    % print(parallel(Statements)),nl,trace,
    extract_assignments(Statements,LHS,RHS,Rest,Nr), % print(extracted(Nr,LHS)),nl,
    Nr>1,!,
    (debug_mode(on) ->
    print('Parallel to Assignment: '), translate:print_subst(b(parallel(Statements),subst,I)),nl
    ; true),
    (Rest == [] -> Result = assign(LHS,RHS)
    ; Result = parallel([b(assign(LHS,RHS),subst,[])|Rest])).

cleanup_post(select([CHOICE|Rest]),subst,I0,S,subst,Info,single/remove_select) :-
    Rest = [], % SELECT can have multiple true branches
    CHOICE=b(select_when(TRUTH,Subst),subst,_),
    is_truth(TRUTH),!,
    debug_println(19,'Removing useless SELECT'),
    get_texpr_expr(Subst,S),get_texpr_info(Subst,I1),
    add_hint_message(remove_select,'Removing useless SELECT','',I1),
    add_important_info_from_super_expression(I0,I1,Info).

cleanup_post(select([CHOICE|Rest],_ELSE),subst,OldInfo,Res,subst,I,single/remove_select_else) :-
    CHOICE=b(select_when(TRUTH,Subst),subst,_),
    is_truth(TRUTH),!,
    (Rest = [] % completely useless SELECT
    -> add_hint_message(remove_select_else,'Removing useless SELECT','',OldInfo),
    get_texpr_expr(Subst,Res),get_texpr_info(Subst,I1),
    add_important_info_from_super_expression(OldInfo,I1,I)
    ; add_hint_message(remove_select_else,'Removing useless SELECT ELSE branch','',OldInfo),
    Res = select([CHOICE|Rest]), I=OldInfo).

cleanup_post(let_expression([],[],TExpr),Type,I0,Expr,Type,I,multi/remove_let_expression) :- !,
    % remove trivial let expressions without any introduced identifiers
    % this rule makes only sense in combination with the next rule which removes
    % simple let identifiers
    get_texpr_expr(TExpr,Expr),
    get_texpr_info(TExpr,I1),
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(let([],Pred,TExpr),Type,I0,Expr,Type,I,multi/remove_let) :- is_truth(Pred),!,
    % remove trivial let expressions without any introduced identifiers
    % this rule makes only sense in combination with the next rule which removes
    % simple let identifiers
    get_texpr_expr(TExpr,Expr),
    get_texpr_info(TExpr,I1),
    add_important_info_from_super_expression(I0,I1,I).

cleanup_post(let_expression(TIds,Exprs,Expr),Type,I,
    let_expression(NIds,NExprs,NExpr),Type,I,multi/remove_let_expression2) :-
    simplify_let(TIds,Exprs,Expr,NIds,NExprs,NExpr),!,
    %format('~n Simplified Let ~w --> ~w~n',[TIds,NIds]),
    true.

cleanup_post(let_predicate(TIds,Exprs,Body),Type,I,
    let_predicate(NIds,NExprs,NBody),Type,I,multi/remove_let_predicate2) :-
    simplify_let(TIds,Exprs,Body,NIds,NExprs,NBody),!,
    %format('~n Simplified Let ~w --> ~w~n',[TIds,NIds]),
    (is_truth(NBody) -> print(useless_let),nl,nl ; true).

cleanup_post(let_predicate(TIds,Exprs,Body),Type,I,
    NewExpr,Type,NewI,single/useless_let_message_or_removal) :-
    is_truth(Body),
    nonmember(useless_let,I),
    get_texpr_ids(TIds,Ids),
    TE=b(let_predicate(TIds,Exprs,Body),Type,I),
    (always_well_defined_or_wd_improvements_allowed(TE)
    -> NewExpr = truth, delete(I,contains_wd_condition,NewI),
    (always_well_defined_or_disprover_mode(TE)
    -> true
    ; add_message(b_ast_cleanup,'Removing useless existentially quantified variables: ',Ids,TIds)
    )
    ; NewExpr = let_predicate(TIds,Exprs,Body), NewI=[useless_let|I],
    TIds= [TID1|_], get_texpr_info(TID1,BInfo),
    nonmember(generated_exists_parameter,BInfo),
    % otherwise this was generated programmatically, e.g., in get_operation_enabling_condition, see test 625
    (nonmember(allow_to_lift_exists,I) -> true % ditto, e.g., by create_outer_exists_for_dom_range, see test 1945
    ; get_preference(data_validation_mode,true)),
    add_message(b_ast_cleanup,'Useless existentially quantified variables: ',Ids,TIds)
).

cleanup_post(let(Ids,Pred,Subst),Type,I,
    let(NIds,NPred,NSubst),Type,I,multi/remove_let_subst2) :-
    simplify_let_subst(Ids,Pred,Subst,NIds,NPred,NSubst),! ,
    true. % translate:print_subst(b(let(NIds,NPred,NSubst),subst,[])),nl.

cleanup_post(forall([ID],LHS,RHS),pred,IOld,Res,pred,IOld,single/expand_forall_set_extension) :-
    % expand !x.(x:{a,b,...} => RHS) into conjunction
    % can be useful e.g. for KODKOD when we pick an element from a set of sets
    \+ preferences:has_default_value(use_solver_on_load), % prob, used to be only enabled in Kodkod mode
    % TO DO: enable always; but maybe check that set_extension can be computed (which eval_set_extension will do) to avoid duplicating checks (!y.(y:{v,w} => expensive_pred) + what if v=w
    nonmember(do_not_optimize_away,IOld),
    get_texpr_expr(LHS,member(ID2,Set)),
    same_texpr(ID,ID2),
    is_set_extension(Set,SList),
    get_texpr_id(ID,AID),
    debug_format(19,'Expanding forall ~w ',[AID]),
    findall(C, (member(SEL,SList),replace_id_by_expr(RHS,AID,SEL,C)),Conjuncts),
    conjunct_predicates_with_pos_info(Conjuncts,ExpandedForAll),
    (silent_mode(on) -> true ; print_bexpr(ExpandedForAll),nl),
    get_texpr_expr(ExpandedForAll,Res).

cleanup_post(forall(Ids1,LHS,RHS),pred,IOld,
    forall(Ids,NewLHS,NewRHS),pred,INew,multi/merge_forall) :-
    is_truth(LHS),
    RHS = b(forall(Ids2,NewLHS,NewRHS),pred,_),
    %((member(b(identifier(_),Type,_),Ids1), is_infinite_ground_type(Type)) -> true), % could be useful for tests 1441, 1447 ??
    (disjoint_ids(Ids1,Ids2)
    -> append(Ids1,Ids2,Ids),
    % !x.(truth => !y.(P=>Q) <==> !(x,y).(P=>Q)
    (debug_mode(off) -> true ; format('Merging forall ~w: ',[Ids]), print_bexpr(NewLHS),nl),
    add_removed_typing_info(IOld,INew)
    ; \+ preferences:get_preference(disprover_mode,true),
    translate:translate_bexpression(b(forall(Ids1,LHS,RHS),pred,IOld),PS),
    add_warning(b_ast_cleanup,'Variable clash in nested universal quantification: ',PS,IOld),
    fail
).

cleanup_post(forall(Ids,LHS,RHS),pred,IOld,
    implication(Outer,FORALL),pred,IOld,single/detect_global_preds_forall1) :-
    % !x.(P(x) & Q => R(x) <==> Q => !x.(P(x) => R(x))
    % TO DO: maybe we should not lift things like printf, ... ?
    bsyntaxtree:detect_global_predicates(Ids,LHS,Outer,Inner),
    (debug_mode(off) -> true ; format('Lifting predicate (lhs) of forall ~w: ',[Ids]), print_bexpr(Outer),nl),
    construct_inner_forall(Ids,Inner,RHS,IOld,FORALL).

cleanup_post(forall(Ids,LHS,RHS),pred,IOld,
    conjunct(Outer,FORALL),pred,IOld,single/detect_global_preds_forall2) :-
    is_truth(LHS),
    % !x.(truth => Q & R(x) <==> Q & !x.(truth => R(x))
    bsyntaxtree:detect_global_predicates(Ids,RHS,Outer,Inner),
    (debug_mode(off) -> true ; format('Lifting predicate (rhs &) of forall ~w: ',[Ids]), print_bexpr(Outer),nl),
    construct_inner_forall(Ids,LHS,Inner,IOld, FORALL). % print_bexpr(FORALL),nl,nl.

cleanup_post(forall(Ids,LHS,RHS),pred,IOld,
    implication(Outer,FORALL),pred,IOld,single/detect_global_preds_forall3) :-
    is_truth(LHS),
    RHS = b(implication(RHS1,RHS2),pred,_),
    % !x.(truth => (Q & R(x) => S(x)) <==> Q => !x.(truth => R(x) => S(x))
    bsyntaxtree:detect_global_predicates(Ids,RHS1,Outer,Inner),
    create_implication(Inner,RHS2,NewRHS),
    (debug_mode(off) -> true ; format('Lifting predicate (rhs =>) of forall ~w: ',[Ids]), print_bexpr(Outer),nl),
    construct_inner_forall(Ids,LHS,NewRHS,IOld, FORALL).

cleanup_post(forall([TID1,TID2|OTHER],LHS,RHS),pred,IOld,
    forall([TID1,TID2|OTHER],NewLHS,RHS),pred,[prob_symmetry(ID1,ID2)|IOld],single/symmetry_detection) :-
    % DETECT Symmetries such as !(x,y).(x /= y => x=TRUE or y=TRUE)
    % !(x2,y).(x2 /= y & x2:s & y:s => x2=aa or y=aa)
    % f:1..n --> 1..(n-1) & !(x,y).(x/=y &x:dom(f) & y:1..n => f(x) /= f(y)) & n=9 (runtime 1 sec -> 0.78 sec)
    get_texpr_type(TID1,T), get_texpr_type(TID2,T),
    \+ preferences:get_preference(use_solver_on_load,kodkod), % e.g., Kodkod cannot properly deal with LEQ_SYM_BREAK, treats it like truth
    preferences:get_preference(use_static_symmetry_detection,true),
    sym_break_supported_type(T), % LEQ_SYM_BREAK not yet fully functional with SET types; TO DO: fix
    get_texpr_id(TID1,ID1), get_texpr_id(TID2,ID2),
    nonmember(prob_symmetry(ID1,ID2),IOld),
    rename_bt(LHS,[rename(ID1,ID2),rename(ID2,ID1)],LHS2),
    same_norm_texpr(LHS,LHS2),
    rename_bt(RHS,[rename(ID1,ID2),rename(ID2,ID1)],RHS2),
    same_norm_texpr(RHS,RHS2),
    construct_sym_break(T,TID1,TID2,LHS,SYMBREAK),
    conjunct_predicates_with_pos_info(LHS,SYMBREAK,NewLHS),
    (debug_mode(off) -> true
    ; format('SYMMETRY BREAKING FORALL: !(~w,~w).(',[ID1,ID2]),print_bexpr(NewLHS),
    print(' => '), print_bexpr(RHS),print(')'),nl).

cleanup_post(forall(AllIds,P,Rhs),pred,I,NewPred,pred,INew,multi/forall_splitting) :-
    AllIds = [TID1|TRestIDs], TRestIDs = [_|_], % TO DO: maybe not require that TID1 is the first id
    get_preference(use_clpfd_solver,true), % with CLPFD false: maybe more likely to reduce performance
    % NOTE: we could destroy symmetry reduction detection if TRestIDs = [TID2], but we run after symmetry detection
    % !(x,y,...).(x:SET & RestPred => Rhs) == !x.(x:SET => !(y,..).(RestPred => Rhs))
    conjunction_to_list(P,[MEM|RestPreds]),
    is_membership(MEM,TID,Set),
    same_id(TID1,TID,ID),
    \+ definitely_infinite(Set), % prevent !(x,y).(x:NATURAL & x<10 & y :1..x => x+y<20)
    %\+ known_set(Set), % rewriting makes sense if Set is not fully known and will be instantiated during solving
    % used to prevent known sets, but rewriting also useful for known sets (QueensWithEvents_ForallTest2b)
    get_sorted_ids(TRestIDs,RestIDs),
    not_occurs_in_predicate(RestIDs,Set),
    NewPred = forall([TID1],MEM,InnerForall),
    conjunct_predicates_with_pos_info(RestPreds,InnerForallLhs),
    construct_inner_forall(TRestIDs,InnerForallLhs,Rhs,I,InnerForall),
    !,
    delete(I,used_ids(_),I1), % should in principle still be ok at outer level; but just be sure
    add_removed_typing_info(I1,INew),
    (debug_mode(on) -> format('FORALL SPLITTING ~w (from ~w) for better propagation: ',[ID,RestIDs]),
    print_bexpr(b(NewPred,pred,INew)),nl
    ; true).

cleanup_post(exists([TID],MemPred),pred,IOld,
    Res,pred,IOld, single/replace_exists_by_not_empty) :-
    % simplify #ID.(ID:E) <=> E /= {}
    % simplify #ID.(ID:E1 & ID:E2) <=> E1 /\ E2 /= {} , etc...
    % important e.g. for y:20..30000000000 & not(#x.(x:1..10 & x:8..y))
    is_valid_id_member_check(MemPred,TID,E),
    !,
    (definitely_not_empty_set(E) -> Res= truth
    ; get_texpr_type(E,Type), EmptySet=b(empty_set,Type,[]),
    Res = not_equal(E,EmptySet)),
    (debug_mode(off) -> true
    ; get_texpr_id(TID,ID),
    format('Removing existential quantifier: ~w~n',[ID]),
    print_bexpr(b(Res,pred,IOld)),nl).

cleanup_post(exists([TID],b(NotMemPred,_,_)),pred,IOld,
    not_equal(E,TypeExpr),pred,IOld, single/replace_exists_by_not_full) :-
    % simplify #ID.(ID/:E) <=> E /= FullType
    % important e.g. for y:7..30000000000 & not(#x.(x /: 1..y))
    is_not_member(NotMemPred,MID,E),
    same_id(TID,MID,SID),
    % + check that MID does not occur in E
    \+ occurs_in_expr(SID,E),
    get_texpr_type(E,SType),
    is_set_type(SType,Type),
    create_maximal_type_set(Type,TypeExpr), % Note: no longer introduces identifiers but value(.) results
    !,
    (debug_mode(off) -> true
    ; format('Removing existential quantifier: ~w~n',[SID]),
    print_bexpr(b(not_equal(E,TypeExpr),pred,IOld)),nl).

cleanup_post(exists([TID],b(Pred,_,_)),pred,IOld,
    truth,pred,IOld, single/replace_exists_by_truth) :-
    b_interpreter_check:arithmetic_op(Pred,_Op,X,Y),
    ( (same_id(TID,X,SID), \+ occurs_in_expr(SID,Y), always_well_defined_or_disprover_mode(Y)) ;
    (same_id(TID,Y,SID), \+ occurs_in_expr(SID,X), always_well_defined_or_disprover_mode(X))
    ),
    !, % we have a formula of the form #SID.(SID > Expr); provided Expr is well-defined, this is always true
    (debug_mode(off) -> true
    ; format('Removing existential quantifier: ~w~n',[SID]),
    print_bexpr(b(Pred,pred,[])),nl).

cleanup_post(exists([TID1,TID2|OTHER],RHS),pred,IOld,
    exists([TID1,TID2|OTHER],NewRHS),pred,[prob_symmetry(ID1,ID2)|IOld],single/symmetry_detection) :-
    % DETECT Symmetries such as #(x,y).(x /= y & (x=TRUE or y=TRUE))
    % #(x2,y).(x2 /= y & x2:s & y:s & x2=aa or y=aa)
    get_texpr_type(TID1,T), get_texpr_type(TID2,T),
    \+ preferences:get_preference(use_solver_on_load,kodkod),
    preferences:get_preference(use_static_symmetry_detection,true),
    sym_break_supported_type(T), % LESS not yet fully functional with SET types; TO DO: fix
    get_texpr_id(TID1,ID1), get_texpr_id(TID2,ID2),
    nonmember(prob_symmetry(ID1,ID2),IOld),
    \+(contains_equality(TID1,TID2,RHS)), % IDs are already equal; no use in sym breaking
    rename_bt(RHS,[rename(ID1,ID2),rename(ID2,ID1)],RHS2),
    same_norm_texpr(RHS,RHS2),
    construct_sym_break(T,TID1,TID2,RHS,SYMBREAK),
    conjunct_predicates_with_pos_info(RHS,SYMBREAK,NewRHS),
    (debug_mode(off) -> true
    ; format('SYMMETRY BREAKING EXISTS: #(~w,~w).(',[ID1,ID2]),print_bexpr(NewRHS),print(')'),nl).

cleanup_post(Expr,T,I1,NewExpr,T,I1,single/detect_lambda_result_quant_auto) :-
    construct_for_find_do_not_enumerate(Expr,KIND,TIds,Body,NewExpr,NewBody),
    perform_do_not_enumerate_analysis(TIds,Body,KIND,I1,NewBody).

cleanup_post(Expr, Type, I, NExpr, Type, NI, single/normalize_commutative_args) :-
    preferences:get_preference(normalize_ast_sort_commutative, true),
    sort_commutative_args(Expr, I, NExpr, NI).

cleanup_post(Expr, pred, I, Expr, pred, [DI|I], single/detect_prob_ignore) :-
    get_info_labels(I,Labels), member(Label,Labels),
    is_prob_ignore_label(Label),
    !,
    DI=description('prob-ignore'), % detected by info_has_ignore_pragma/1
    nonmember(DI,I),
    add_message(detect_prob_ignore,'Detected prob-ignore label: ',Label,I).