b_operation_cache

add_new_vars([],S,S).

add_new_vars([WrittenVar|T],State,[bind(WrittenVar,term(undefined))|ST]) :-
    add_new_vars(T,State,ST).

ahc :- operation_computed(Hash,OpName,ConstID,State,ID),
    operation_computed(Hash,OpName2,ConstID2,State2,ID2),
    (ConstID @> ConstID2 -> true ; ConstID=ConstID2, ID2 > ID),
    format('Hash collision: ~w~n ~w:~w:~w:~w~n ~w:~w:~w:~w~n~n',
    [Hash,OpName,ConstID,State,ID,OpName2,ConstID2,State2,ID2]),
    fail.

ahc.

api_compute_operation_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall) :-
    create_mutable(still_computing,Done),
    %tools:start_ms_timer(Timer),
    (event_occurred_in_error_scope(E)
    -> add_message(b_operation_cache,'Error scope not fresh: ',E),
    enter_new_error_scope(Level)
    ; Level=none),
    call_cleanup(
    com_op_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall,Done),
    (get_mutable(still_computing,Done)
    -> format('Timeout, exception or virtual timeout occured during caching for ~w (cache id ~w)~n',[OpName,NewID]),
    % also happens during -execute due to cut!, hence we now disable preference in -execute
    % stop_ms_timer_with_msg(Timer,'Runtime for computing'),
    exit_scope(Level),
    register_op_cache_time_out(NewID,OpName)
    ; error_occurred_in_error_scope
    -> format('Error occurred during caching for ~w (cache id ~w)~n',[OpName,NewID]),
    invalidate_operation_cache(NewID,OpName),
    exit_scope(Level)
    ; event_occurred_in_error_scope(Event),
    functor(Event,Kind,_),
    format('Event ~w occurred during caching for ~w (cache id ~w)~n',[Kind,OpName,NewID]),
    register_op_cache_enum_warning(NewID,OpName,Event),
    exit_scope(Level),
    fail
    % TODO: should we also check if errors occured
    ; exit_scope(Level)
    )),
    get_mutable(DVal,Done), DVal \= finished. % fail if we are Done;

api_get_op_rw_aux(check_invariant_violated(Nr),UsedIds,Written) :- !, Written=[],
    b_nth1_invariant(Nr,_,UsedIds).

api_get_op_rw_aux(OpName,ReadVariables,WrittenVariables) :-
    b_get_operation_normalized_read_write_info(OpName,ReadVariables,WrittenVariables).

api_get_operation_read_write_info(OpName,ReadVariables,ReadConstants,WrittenVariables) :-
    api_get_op_rw_aux(OpName,ReadIds,WrittenVariables),
    exclude(b_is_constant,ReadIds,ReadVariables),
    include(b_is_constant,ReadIds,ReadConstants).

b_operation_cache_startup :- % call once at startup to ensure all counters exist
    counter_init,
    new_counter(op_cache_id),
    new_counter(inv_cache_nr),
    new_counter(op_cached_failures),
    new_counter(op_cached_successes),
    new_counter(inv_cached_successes),
    new_counter(op_cached_timeouts),
    new_counter(op_cached_enum_warnings),
    new_counter(op_cached_errors).

check_if_op_cache_useful :-
    b_get_machine_variables(Var),length(Var,VLen),
    api_get_operation_read_write_info(OpName,ReadVariables,_ReadConstants,_WrittenVariables),
    length(ReadVariables,ReadLen),
    ReadLen < VLen,
    (inv_op_name(OpName) -> get_preference(use_po,false) ; true),
    format('Operation reuse potentially useful: ~w reads ~w/~w variables~n',[OpName,ReadLen,VLen]),
    fail.

check_if_op_cache_useful.

check_if_operation_was_computed(OpName,ConstID,State,Skel,Infos,PackedValList,IsReadingCsts,
    HashConstID,Hash,Res) :-
    (Infos = [packed_state/PS|_]
    -> get_packed_vars(PS,OpName,PackedState),
    remove_bind_skeleton(PackedState,Skel,PackedValList)
    % packing already performed in prepare_state_for_specfile_trans
    ; write(no_packed_state_info(OpName,ConstID)),nl, % shouldn't happen hopefully
    project_in_state(State,OpName,ProjectedInState), % State contains just variables
    pack_bind_list(ProjectedInState,Skel,PackedValList)
    ),
    (IsReadingCsts = false -> HashConstID=root ; HashConstID=ConstID),
    op_hash(OpName,HashConstID,PackedValList,Hash),
    (operation_computed(Hash,OpName,HashConstID,PackedValList,ID)
    -> Res = ID
    ; % operation_guard_read_info(OpKey,GuardVars,_), re_project_state(GuardVars,Skel,PackedValList,GuardPackedVals)
    % op_hash(OpName,HashConstID,GuardPackedVals,GuardHash), op_guard_fails(GuardHash,OpName,GuardPackedVals,ID) -> true
    Res= false).

check_invariant_violated_cache(Nr,State) :-
    %get_store_and_info(State,FullStore,Infos),
    compute_operation_on_expanded_store_cache(check_invariant_violated(Nr),_,State,_,_,-1).

com_op_update_max(_,check_invariant_violated(Nr),Operation,ProjState,NewState,PathInfo,_,Done) :- !,
    NewState =[], PathInfo=invariant, Operation=Nr, % values not used anyway for invariants
    %print(check_invariant(Nr)),nl, bmachine:b_nth1_invariant(Nr,Inv,_UsedIds), translate:print_bexpr(Inv),nl,
    (b_interpreter:check_nth1_invariant(Nr,ProjState )
    -> update_mutable(finished,Done) % will lead to failure above; we store only violations
    ; % invariant violation found
    update_mutable(last_sol_found,Done)
).

com_op_update_max(_,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall,_) :-
    % for CSP||B: clear out any parameters; otherwise we also need to hash the parameters
    reset_max_reached(OpName),
    succeed_max_call_id(OpName,
    b_execute_top_level_operation_update(OpName,Operation,ProjInOutState,NewState,PathInfo),
    MaxForCall).

com_op_update_max(NewID,OpName,_,_,_,_,_,Done) :-
    (NewID \= uncached,
    max_reached(OpName)
    -> assertz(operation_cached_max_reached(NewID,OpName)) % store that we reached max. nr of transitions for this node
    ; true %format('No Timeout or virtual timeout occurred during caching for ~w leading to ~w~n',[OpName,NewID])
    ),
    update_mutable(finished,Done).

compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo,MaxForCall) :-
    get_state_infos(InState,ConstID,Vars,FullStore,Infos), % extract infos from the store
    % TO DO: check if state_id in Infos and if OpName in equivalence class with same proj. vars
    get_opname_key(OpName,OpNameKey),
    get_operation_read_projection_infos(OpNameKey,OpName,Vars,ProjVarsInOrder,IsReadingCsts,AdditionalOutVars),
    !,
    % tools_printing:print_term_summary(proj(OpName,ConstID,ProjInState,FullStore)),nl,
    check_if_operation_was_computed(OpName,ConstID,Vars,ProjVarsInOrder,Infos,PackedValList,IsReadingCsts,
    HashConstID,Hash,ID),
    (ID \= false
    -> % we can reuse the stored operation effect
    %print('+'),
    %hit_profiler:add_hit(operation_reused,OpName),
    (inv_op_name(OpName) -> inc_counter(inv_cached_successes)
    ; inc_counter(op_cached_successes)),
    (operation_cached_results(ID,Operation,PackedNewState,PathInfo),
    unpack_values(PackedNewState,NewState)
    ; operation_cached_max_reached(ID,OpName), % we did not compute all operations
    assert_max_reached(OpName),
    fail
    ; operation_cached_enum_warning(ID,OpName,Event),
    functor(Event,Kind,_),
    format('Regenerating ~w for ~w and cache id ~w~n',[Kind,OpName,ID]),
    add_new_event_in_error_scope(Event),
    fail
    ; operation_cached_time_out(ID,OpName),
    format('Rethrowing cached time_out for ~w and cache id ~w~n',[OpName,ID]),
    throw(time_out)
    )
    ; % we have not computed solutions for this operation for this projected state
    (project_onto_guard(OpName,OpNameKey,HashConstID,ProjVarsInOrder,PackedValList,GuardPackedVals,GuardHash)
    -> true
    ; GuardPackedVals = none),
    (nonvar(GuardHash),
    op_guard_fails(GuardHash,OpName,GuardPackedVals)
    -> % we did already compute this operation for this projected state and it failed
    inc_counter(op_cached_failures),
    fail % the guard is guaranteed to fail
    ; % we have not yet computed this operation; compute it and store solutions as we go
    get_new_operation_computed_id(OpName,HashConstID,PackedValList,Hash,NewID),
    %print('-'),
    %hit_profiler:add_hit(operation_cache_computation,OpName),
    (IsReadingCsts=false
    -> % TO DO: check if this projection is worthwhile
    project_in_state_for_opname_key(Vars,OpNameKey,ProjInState),
    % Note: if no packed_state this projection was already performed in check_if_operation_was_computed
    add_new_vars(AdditionalOutVars,ProjInState,ProjInOutState)
    ; ProjInOutState = FullStore % use full store with constants
    ),
    profile_failure_driven_loop(OpName),
    if(api_compute_operation_update_max(NewID,OpName,Operation,ProjInOutState,NewState,PathInfo,MaxForCall),
    (% Normalise here or in update_max
    pack_values(NewState,PackedNewState),
    (PathInfo=invariant -> StoredPathInfo=Hash
    ; filter_transition_path_info(PathInfo,StoredPathInfo)),
    assertz(operation_cached_results(NewID,Operation,PackedNewState,StoredPathInfo))
    ),
    (nonvar(GuardHash),
    %print(op_guard_fails(GuardHash,OpName,GuardPackedVals)),nl,
    assertz(op_guard_fails(GuardHash,OpName,GuardPackedVals)),
    fail
)
)
)
% TO DO: if we have no successors for ID and if the operation reads less IDs in the guard
% we can replace remaining identifier values by a variable
).

compute_operation_on_expanded_store_cache(OpName,Operation,InState,NewState,PathInfo,MaxForCall) :-
    %hit_profiler:add_hit(operation_not_cached,OpName),
    % operation is not cached
    get_state_infos(InState,_,_,FullStore,_),
    api_compute_operation_update_max(uncached,OpName,Operation,FullStore,NewState,PathInfo,MaxForCall).

exit_scope(none) :- !.

exit_scope(Level) :- exit_error_scope(Level,_).

filter_transition_path_info([],R) :- !, R=[].

filter_transition_path_info([H|T],Res) :- !,
    (keep_transition_info(H) -> Res = [H|RT]
    ; Res=RT), % by default we filter out possibly large path infos (in particular for Event-B)
    filter_transition_path_info(T,RT).

filter_transition_path_info(H,Res) :-
    (keep_transition_info(H) -> Res = H ; Res=[]).

get_new_operation_computed_id(OpName,ConstID,PackedValList,Hash,ID) :-
    inc_counter(op_cache_id,ID),
    (OpName=check_invariant_violated(_) -> inc_counter(inv_cache_nr,_) ; true),
    assertz(operation_computed(Hash,OpName,ConstID,PackedValList,ID)).

get_nr_cache_results(OpName,RNr) :-
    findall(1,(operation_cached_results(_ID,Op,_,_),get_op_name(Op,OpName)),Rs), length(Rs,RNr).

get_nr_next_state_calls(OpName,Nr) :- findall(1,operation_computed(_Hash,OpName,_,_,_ID),Ls), length(Ls,Nr).

get_op_cache_stats([next_state_calls-NrN, % actual calls to the B interpreter to compute next state
    operations_cached-NrC, % number of operations whose calls are cached
    invariants_cached-NrI, % number of invariants whose evaluation is cached
    next_state_guard_failures-NrFails, % number of next-state_call failures stored (disabled operation)
    reused_next_state_calls-SuccCalls,
    reused_next_state_failures-FailCalls,
    inv_check_calls-InvNr, % actual calls to check individual invariants in a state
    reused_inv_check_calls-SuccInvCalls
    ]) :-
    findall(OpKey,(operation_read_projection_cache(OpKey,OpName,_,_,_),atomic(OpName)),OK1),
    length(OK1,NrC),
    findall(OpKey,invariant_op_key(OpKey,_),OK2),
    length(OK2,NrI),
    findall(OpKey,(op_guard_fails(OpKey,_,_)),OK3),
    length(OK3,NrFails),
    get_total_number_of_next_state_calls(NrN,InvNr),
    get_counter(op_cached_failures,FailCalls),
    get_counter(op_cached_successes,SuccCalls),
    get_counter(inv_cached_successes,SuccInvCalls).

get_op_name(Nr,check_invariant_violated(Nr)) :- number(Nr),!.

get_op_name(Op,OpName) :- get_operation_name(Op,OpName).

get_operation_read_projection_infos(OpNameKey,OpName,_,ProjVars,IsReadingCsts,AdditionalOutVars) :-
    operation_read_projection_cache(OpNameKey,OpName,ProjVars,IsReadingCsts,AdditionalOutVars),!,
    ProjVars \= no_caching.

get_operation_read_projection_infos(OpNameKey,OpName,_,_,_,_) :- atom(OpName),
    b_definition_prefixed(_, 'OPERATION_REUSE_OFF_', OpName, _DefName,_),
    !,
    format('Ignoring operation ~w for reuse~n',[OpName]),
    assertz(operation_read_projection_cache(OpNameKey,OpName,no_caching,no_caching,[])),
    fail.

get_operation_read_projection_infos(OpNameKey,OpName,InState,ProjVarsInOrder,IsReadingCsts,AdditionalOutVars) :-
    api_get_operation_read_write_info(OpName,ReadVariables,ReadConstants,WrittenVariables),
    (ReadConstants=[] -> IsReadingCsts=false ; IsReadingCsts=true),
    debug_println(19,operation_reads_vars_consts(OpName,ReadVariables,ReadConstants)),
    (project_state_onto_vars(InState,ReadVariables,ProjVarsInOrder,_RelevantState,0,NrDeleted)
    -> % TO DO: if we have constants in the state which are deterministic anyway, then they should not count
    % TO DO: statically pre-compute which operations are worthwhile for this treatment
    ((NrDeleted>0 % we project away at least one variable and thus hope to cache operation results
    ; csp_with_bz_mode) % in CSP||B mode, the same operation may be called with different CSP controllers
    -> ord_subtract(WrittenVariables,ReadVariables,AdditionalOutVars), % vars written but not read
    assertz(operation_read_projection_cache(OpNameKey,OpName,ProjVarsInOrder,IsReadingCsts,AdditionalOutVars)),
    assertz(operation_read_constants(OpNameKey,ReadConstants)),
    % ,print(proj(OpName,ProjVarsInOrder,AdditionalOutVars)),nl,
    (get_preference(try_operation_reuse,full),
    b_get_operation_read_guard_vars(OpName,true,ReadVarsInGuard,precise),
    exclude(member_ord(ReadVarsInGuard),ProjVarsInOrder,IrrelevantVars),
    % TO DO: analyse if projection really useful
    IrrelevantVars \= []
    -> include(member_ord(ReadVarsInGuard),ProjVarsInOrder,ReadVarsInGuard),
    debug_println(19,guard_reads_subset_of_vars(OpName,OpNameKey,ReadVarsInGuard,IrrelevantVars)),
    assertz(operation_guard_read_info(OpNameKey,ReadVarsInGuard,IrrelevantVars))
    ; true)
    ; assertz(operation_read_projection_cache(OpNameKey,OpName,no_caching,no_caching,[])),
    perfmessage('Not caching operation for reuse: ',OpName),
    fail
    )
    ; add_internal_error('Projection failed for: ', project_state_onto_vars(InState,ReadVariables,_,_,0,_)),
    assertz(operation_read_projection_cache(OpNameKey,OpName,no_caching,no_caching,[])),
    fail
).

get_opname_key(Name,Res) :- var(Name),!,
    add_internal_error('Variable opname: ',get_opname_key(Name,Res)), Res=Name.

get_opname_key(check_invariant_violated(Nr),Key) :- !, Key=Nr.

get_opname_key(Name,Name).

get_packed_vars(const_and_vars(_,Vars),OpName,PackedVars) :- !, project_in_state(Vars,OpName,PackedVars).

get_packed_vars(PS,OpName,PackedVars) :- !, project_in_state(PS,OpName,PackedVars).

get_state_infos(expanded_const_and_vars(ID,Vars,FullStore,I),ConstID,Vars,FullStore,Infos) :- !,ConstID=ID,Infos=I.

get_state_infos(expanded_vars(V,I),ConstID,Vars,FullStore,Infos) :- !, ConstID=root,Vars=V,FullStore=V,Infos=I.

get_state_infos(const_and_vars(ConstID,Vars),ConstID,Vars,FullStore,Infos) :- !,
    add_warning(get_state_infos,'State not prepared for caching: ',const_and_vars(ConstID,Vars)),
    Infos=[],
    expand_const_and_vars_to_full_store(const_and_vars(ConstID,Vars),FullStore).

get_state_infos(csp_and_b(_,State),ConstID,Vars,FullStore,Infos) :- !,
    get_state_infos(State,ConstID,Vars,FullStore,Infos).

get_state_infos(Vars,unknown,Vars,Vars,[]).

get_total_number_of_next_state_calls(OpNr,InvNr) :-
    get_counter(op_cache_id,TotNr),
    get_counter(inv_cache_nr,InvNr),
    OpNr is TotNr-InvNr.

inv_op_name(check_invariant_violated(_)).

invalidate_operation_cache(ID,OpName) :-
    inc_counter(op_cached_errors),
    retractall(operation_cached_results(ID,_Operation,_,_)),
    retractall(operation_computed(_,OpName,_,_,ID)). % can be expensive

invariant_op_key(OpKey,InvNr) :- operation_read_projection_cache(OpKey,check_invariant_violated(InvNr),_,_,_).

member_ord(List,X) :- ord_member(X,List). % for maplist, exclude,...

op_hash(OpName,HashConstID,PackedValList,Hash) :- get_preference(use_state_packing,false),!,
    my_term_hash((OpName,HashConstID,PackedValList),Hash). % will user super_hash

op_hash(OpName,HashConstID,PackedValList,Hash) :-
    % we use state packing and thus replace AVL sets by identifiers, ...: a simpler hash suffices, but we get collisions for Train1_Lukas_POR (which do not seem to matter); we get an improvement for ifm18/Ref5_Switch_mch.eventb
    term_hash((OpName,HashConstID,PackedValList),
    [range(smallint),algorithm(sdbm),depth(infinite),if_var(ignore)], % djb2
    Hash).

print_op_cache_profile :- \+ operation_computed(_,_,_,_,_),!, % print nothing
    (get_preference(try_operation_reuse,false) -> format('OPERATION_REUSE preference not set to TRUE~n',[]) ; true),
    format('No operation cached~n',[]),
    check_if_op_cache_useful.

print_op_cache_profile :-
    b_get_machine_variables(Var),length(Var,VLen),
    operation_read_projection_cache(OpKey,OpName,ProjVars,_,WV), (ProjVars = [] ; ProjVars = [_|_]),
    length(ProjVars,Len),
    operation_read_constants(OpKey,ReadConstants),
    (operation_guard_read_info(OpKey,_,IrrelevantVars)
    -> format('Operation ~w cached onto ~w/~w variables: ~w (not relevant for guard: ~w, only written: ~w, constants read: ~w)~n',[OpName,Len,VLen,ProjVars,IrrelevantVars,WV,ReadConstants])
    ; format('Operation ~w cached onto ~w/~w variables: ~w (only written: ~w, constants read: ~w)~n',[OpName,Len,VLen,ProjVars,WV,ReadConstants])
    ),fail.

print_op_cache_profile :- findall(OpName,operation_read_projection_cache(_,OpName,no_caching,_,_),Ls),
    format('Operations not cached: ~w~n',[Ls]),fail.

print_op_cache_profile :- operation_read_projection_cache(OpKey,OpName,ProjVars,_,_), ProjVars = [_|_],
    get_nr_next_state_calls(OpName,Nr),
    get_nr_cache_results(OpName,RNr),
    (inv_op_name(OpName) -> Results='violations' ; Results = 'results'),
    format('Next-state-calls for ~w: ~w (~w ~w)~n',[OpName,Nr,RNr,Results]),
    operation_guard_read_info(OpKey,RelVars,_),
    findall(1,op_guard_fails(_,OpName,_),Fails), length(Fails,NrFails),
    format(' projected-failures (on ~w): ~w~n',[RelVars,NrFails]),
    fail.

print_op_cache_profile :-
    get_total_number_of_next_state_calls(Nr,InvNr),
    format('Total Number of Next-state-calls for Operations: ~w~n',[Nr]),
    get_counter(op_cached_failures,FailCalls),
    format(' - Reused guard failures: ~w~n',[FailCalls]),
    get_counter(op_cached_successes,SuccCalls),
    format(' - Reused successful operation call results: ~w~n',[SuccCalls]),
    format('Total Number of Invariant-check-calls: ~w~n',[InvNr]),
    get_counter(inv_cached_successes,SuccInvCalls),
    format(' - Reused invariant check results: ~w~n',[SuccInvCalls]),
    get_counter(op_cached_errors,Errs),
    format('Errors during calls: ~w~n',[Errs]),
    get_counter(op_cached_timeouts,Timeouts),
    format('Timeouts during calls: ~w~n',[Timeouts]),
    get_counter(op_cached_enum_warnings,EnumWarns),
    format('Enumeration warnings during calls: ~w~n',[EnumWarns]),
    fail.

print_op_cache_profile :- debug_mode(on), nl,
    operation_read_projection_cache(_,OpName,Skel,_,_),
    format('~n** Local Operation Cache Info for ~w ** (projected on ~w):~n',[OpName,Skel]),
    operation_computed(_Hash,OpName,ConstID,PackedValList,ID),
    (operation_cached_max_reached(ID,OpName) -> MaxR='(max reached, not all transitions computed)'
    ; MaxR=''),
    format('~nNode ID = ~w, Operation = ~w ~w~n',[ID,OpName,MaxR]),
    unpack_bind_list(PackedValList,Skel,State), translate_bstate_limited(State,NodeDesc),
    format(' projected state : (ConstID ~w) ~w~n',[ConstID,NodeDesc]),
    operation_cached_results(ID,Operation,PackedNewState,_PathInfo),
    translate_event_with_limit(Operation,100,OpStr),
    unpack_values(PackedNewState,NewState), translate:translate_bstate_limited(NewState,UpdateStr),
    format(' ~w -upd-> ~w~n',[OpStr,UpdateStr]),
    fail.

print_op_cache_profile :- print_violated_invariants,fail.

print_op_cache_profile :- ahc,print('----------'),nl.

print_violated_invariants :-
    operation_cached_results(ID,Nr,[],Hash),number(Nr),
    b_nth1_invariant(Nr,Invariant,_UsedIds),
    format('Invariant ~w violated (op-cache-id ~w)~n ',[Nr,ID]),
    translate:print_bexpr(Invariant),nl,
    % now try and recover state where it was violated:
    operation_computed(Hash,OpName,ConstID,PackedValList,ID),
    operation_read_projection_cache(_,OpName,Skel,_,_),
    unpack_bind_list(PackedValList,Skel,State), translate_bstate_limited(State,StateDesc),
    format(' in state (ConstID ~w) ~w~n',[ConstID,StateDesc]),
    fail.

print_violated_invariants.

project_in_state(VarsInState,OpName,ProjectedInState) :-
    get_opname_key(OpName,OpNameKey),
    project_in_state_for_opname_key(VarsInState,OpNameKey,ProjectedInState).

project_in_state_for_opname_key(InState,OpNameKey,ProjectedInState) :-
    get_operation_read_projection_infos(OpNameKey,_,InState,ProjVars,_,_),
    (re_project_state(ProjVars,InState,Res) -> ProjectedInState=Res
    ; add_internal_error('Re-Projection failed: ',re_project_state(ProjVars,InState,_)),
    ProjectedInState = InState).

project_onto_guard(OpName,OpKey,HashConstID,Skel,PackedValList,GuardPackedVals,GuardHash) :-
    operation_guard_read_info(OpKey,_,IgnoredVars),
    remove_ignored_vars(IgnoredVars,Skel,PackedValList,GuardPackedVals),
    op_hash(OpName,HashConstID,GuardPackedVals,GuardHash).

project_state_onto_vars([],_,[],[],Acc,Acc).

project_state_onto_vars([Elem|Rest],ReadVariables,ProjVars,ProjState,NrDelAcc,NrDel) :-
    Elem = bind(Var,_),
    (ord_member(Var,ReadVariables) % TO DO: we could improve performance by sorting Elements
    -> ProjVars=[Var|PT], ProjState=[Elem|AR], ND1=NrDelAcc
    ; ProjVars=PT, ProjState=AR, ND1 is NrDelAcc+1),
    project_state_onto_vars(Rest,ReadVariables,PT,AR,ND1,NrDel).

re_project_state([],_,[]).

re_project_state([VarToProject|PT],[Elem|Rest],A) :-
    arg(1,Elem,Var), %Elem = bind(Var,_),
    (VarToProject==Var
    -> A=[Elem|AR],re_project_state(PT,Rest,AR)
    ; re_project_state2(VarToProject,PT,Rest,A)).

re_project_state2(VarToProject,PT,[Elem|Rest],A) :-
    arg(1,Elem,Var), %Elem = bind(Var,_),
    (VarToProject==Var
    -> A=[Elem|AR],re_project_state(PT,Rest,AR)
    ; re_project_state2(VarToProject,PT,Rest,A)).

register_op_cache_enum_warning(ID,OpName,Event) :-
    inc_counter(op_cached_enum_warnings),
    assertz(operation_cached_enum_warning(ID,OpName,Event)).

register_op_cache_time_out(ID,OpName) :-
    inc_counter(op_cached_timeouts),
    assertz(operation_cached_time_out(ID,OpName)).

remove_bind_skeleton([],[],R) :- !, R=[].

remove_bind_skeleton([bind(Var,Val)|T],[Var|VT],[Val|RT]) :- !,
    remove_bind_skeleton(T,VT,RT).

remove_bind_skeleton(L,V,R) :- add_internal_error('Illegal store: ',remove_bind_skeleton(L,V,R)), R=L.

remove_ignored_vars([],_,PackedVals,Res) :- Res=PackedVals.

remove_ignored_vars([ID|T],[ID|ST],[_|PackedVals],GuardPackedVals) :- !,
    remove_ignored_vars(T,ST,PackedVals,GuardPackedVals).

remove_ignored_vars(Ignored,[_|ST],[PV|PackedVals],[PV|GuardPackedVals]) :-
    remove_ignored_vars(Ignored,ST,PackedVals,GuardPackedVals).

reset_b_operation_cache :-
    retractall(operation_read_projection_cache(_,_,_,_,_)),
    retractall(operation_read_constants(_,_)),
    retractall(operation_guard_read_info(_,_,_)),
    retractall(operation_computed(_,_,_,_,_)),
    retractall(operation_cached_results(_,_,_,_)),
    retractall(operation_cached_max_reached(_,_)),
    retractall(operation_cached_time_out(_,_)),
    retractall(operation_cached_enum_warning(_,_,_)),
    retractall(op_guard_fails(_,_,_)),
    reset_counter(op_cache_id),
    reset_counter(inv_cache_nr),
    reset_counter(op_cached_failures),
    reset_counter(op_cached_successes),
    reset_counter(inv_cached_successes).

reset_b_operation_cache_with_statistics :-
    retract_with_statistics(b_operation_cache,
    [operation_read_projection_cache(_,_,_,_,_),
    operation_read_constants(_,_),operation_guard_read_info(_,_,_),
    operation_computed(_,_,_,_,_), operation_cached_results(_,_,_,_),
    operation_cached_max_reached(_,_),
    operation_cached_time_out(_,_),
    operation_cached_enum_warning(_,_,_),
    op_guard_fails(_,_,_)
    ]
    ),
    reset_b_operation_cache.

tcltk_op_cache_stats(list([list(['Operation','#Next-State', '#Results',
    '# Proj.Vars','Proj.Vars', 'ReadCsts', 'OnlyWritten'])|SEntries])) :-
    %b_get_machine_variables(Var),length(Var,VLen),
    findall(list([OP,NrCalls,RNr,NrProjVars,ProjVars,ReadConstants,AdditionalOutVars]),
    (operation_read_projection_cache(OpKey,OpName,ProjVars,_,AdditionalOutVars),
    (OpName = check_invariant_violated(Nr) -> ajoin(['Invariant',Nr],OP) ; OP=OpName),
    length(ProjVars,NrProjVars),
    operation_read_constants(OpKey,ReadConstants),
    get_nr_next_state_calls(OpName,NrCalls),
    get_nr_cache_results(OpName,RNr)
    ), Entries), sort(Entries,SEntries).