operation_reuse.pl

add_additional_destination_infos(FromID,ActionName,ToID) :-
    preference(try_operation_reuse,true),
    ToID \= FromID,
    animation_mode(b),
    preference(symmetry_mode,MODE), (MODE=off ; MODE=flood),
    % TO DO: can we enable this trick in symmetry mode ?
    bmachine:reuse_operation_effect(ActionName,OtherAction),
    \+ reuse_operation(ToID,OtherAction,_,_),
    assertz(reuse_operation(ToID,OtherAction,FromID,ActionName)),
    % print(reuse_operation(ToID,OtherAction,FromID,ActionName)),nl,
    fail.

candidate_operation_for_reuse_calc(Op) :- reuse_operation_effect(_,Op). % no need to avoid multiple solutions; auto_precompile will remove them

lookup_variable(const_and_vars(_ConstID,Vars),Var,Val) :- !,
    lookup_value_for_existing_id(Var,Vars,Val).

lookup_variable(expanded_const_and_vars(_ConstID,Vars,_FullState,_),Var,Val) :- !,
    lookup_value_for_existing_id(Var,Vars,Val).

lookup_variable(Store,Var,Val) :- lookup_value_for_existing_id(Var,Store,Val).

patch_state(const_and_vars(ConstID,Vars),WrittenVariables,PrevState,
    const_and_vars(ConstID,PatchedVars)) :- !,
    patch_state(Vars,WrittenVariables,PrevState,PatchedVars).

patch_state(expanded_const_and_vars(ConstID,Vars,_FullState,_),WrittenVariables,PrevState,
    const_and_vars(ConstID,PatchedVars)) :- !,
    patch_state(Vars,WrittenVariables,PrevState,PatchedVars).

patch_state(expanded_vars(Vars,_),WrittenVariables,PrevState,PatchedVars) :- !,
    patch_state(Vars,WrittenVariables,PrevState,PatchedVars).

patch_state([],_Write,_Prev,[]) :- !.

patch_state([bind(Variable,Value)|T],WrittenVariables,PrevState,[bind(Variable,NewValue)|PT]) :- !,
    (ord_member(Variable,WrittenVariables)
    -> lookup_variable(PrevState,Variable,NewValue)
    ; NewValue=Value
    ), patch_state(T,WrittenVariables,PrevState,PT).

patch_state(S,WV,PS,Res) :- add_internal_error('Illegal state: ',patch_state(S,WV,PS,Res)), Res=S.

precompiled_predicate_phase2(reuse_operation_effect/2).

precompiled_predicate_phase2(candidate_operation_for_reuse/1).

print_reuse :-
    findall((G,H),reuse_operation_effect(G,H),L),
    print_reuse_info(L).

print_reuse_info([]).

print_reuse_info([(G,H)|T]) :- print('When applying '),print(H),print(' after '),
    print(G),print(' recalculate only '),
    b_get_operation_normalized_read_write_info(H,_ReadH,WriteH),
    print(WriteH),nl, print_reuse_info(T).

reuse_operation_effect_calc(G,H) :- get_preference(try_operation_reuse,true),
    (specfile:animation_minor_mode(xeventb) -> print('% OPERATION_REUSE not available for Event-B models'),nl,fail
    % this didn't work ; see eg. prob_examples/examples/EventBPrologPackages/Advance_WP2/v6_Sep2014/ex_mch.eventb -animate 300 which generates deadlock
    ; true),
    b_is_operation_name(G),
    b_get_operation_normalized_read_write_info(G,_ReadG,WriteG), %print(analyse_reuse(G,_ReadG,WriteG)),nl,
    WriteG \= [], /* otherwise we have a skip operation; we will not recompute state anyway */
    b_get_machine_operation(H,_Results,_Parameters,_Body,OpType,_), % TO DO: check if _Body complicated enough
    b_get_operation_normalized_read_write_info(H,ReadH,WriteH),
    \+ ord_intersect(WriteG,ReadH),
    (OpType = classic
    -> \+ ord_intersect(WriteG,WriteH) % because for the moment we do not yet detect whether a potentially written variable by H is really written !
    % TO DO: either store in reuse_operation the actual variables written, then we can remove the above line
    % or compute the variables that are potentially written PotWriteH and intersect with those
    ; true
    ),
    (debug:debug_mode(on) -> format('After: ~w reuse: ~w~n',[G,H]) ; true)
%,format('~nAfter: ~w (writes ~w)~n reuse: ~w (reads ~w, writes ~w)~n',[G,WriteG,H,ReadH,WriteH])
.

reuse_operation_effect_calc(_,_) :- get_preference(try_operation_reuse,true),
    findall(G,b_is_operation_name(G),LG), length(LG,NrOps), TotPairs is NrOps*NrOps,
    findall((G,H),reuse_operation_effect(G,H),Pairs), length(Pairs,NrReuse),
    formatsilent('OPERATION_REUSE Statistics: ~w reuse pairs (for ~w operations, i.e. ~w pairs)~n',[NrReuse,NrOps,TotPairs]),
    fail.