value_persistance

add_new_transition_to_cache_from_expanded_state(InState,OpTerm,OutState) :-
    cache_is_applicable_for_transitions,
    main_machine_name(MachName),
    operation_name(OpTerm,OpName,ParaValues,ResultValues),
    storable_operation(OpName,MachName,InputPattern,Output),
    sort(InState,SortedInState),
    hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash),
    \+ stored_transition(ShortHash,InputHash,_,_), % Is there already a cache entry?
    !,
    MaxReached=true, % TODO: should we check that MAX_OPERATIONS is set to exactly 1
    TransInfo = [], % TODO: preference(eventtrace,true), preference(store_event_transinfo,true)
    Transitions = [trans_cached(ParaValues,ResultValues,Updates,TransInfo)],
    select_values(Output,OutState,Updates),
    store_transition_into_cache(OpName,ShortHash,InputHash,Transitions,MaxReached,MachName),
    flush_data.

add_new_transition_to_cache_from_expanded_state(_,_,_).

add_new_transitions_to_cache(InStateId) :-
    cache_is_applicable_for_transitions,
    visited_expression(InStateId,InState1),
    state_corresponds_to_initialised_b_machine(InState1,InState),
    !,
    add_new_transitions_to_cache1(InStateId,InState).

add_new_transitions_to_cache(_InStateId).

add_new_transitions_to_cache1(InStateId,InState) :-
    get_all_max_reached_operations(MaxReachedList),
    main_machine_name(MachName),
    storable_operation(OpName,MachName,InputPattern,Output),
    \+ time_out_for_node(InStateId,OpName,_),
    (ord_member(OpName,MaxReachedList) -> MaxReached=true ; MaxReached=false),
    sort(InState,SortedInState),
    add_new_transitions_to_cache2(InStateId,SortedInState,OpName,InputPattern,Output,MaxReached,MachName),
    fail.

add_new_transitions_to_cache1(_InStateId,_) :-
    flush_data.

add_new_transitions_to_cache2(InStateId,SortedInState,OpName,InputPattern,Output,MaxReached,MachName) :-
    hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash),
    \+ stored_transition(ShortHash,InputHash,_,_), % Is there already a cache entry?
    find_all_transitions(InStateId,OpName,Output,Transitions),
    length(Transitions,Length),
    %format('value caching: storing ~w transitions for operation ~w in state ~w.~n',
    % [Length,OpName,InStateId]),
    %print(Transitions),nl,
    statistics(runtime,[Start,_]),
    statistics(walltime,[WStart,_]),
    store_transition_into_cache(OpName,ShortHash,InputHash,Transitions,MaxReached,MachName),
    statistics(runtime,[Stop,_]), Time is Stop - Start,
    statistics(walltime,[WStop,_]), WTime is WStop - WStart,
    %%tools:print_memory_used_wo_gc,
    formatsilent('value caching: storing ~w transitions for operation ~w in state ~w (~w, state ~w, [~w] ms).~n',
    [Length,OpName,InStateId,ShortHash,Time,WTime]).

apply_binding(Store,bind(Id,Value)) :-
    lookup_value(Id,Store,SValue),
    equal_object(SValue,Value).

belongs_to_file(FileNumbers,TPred) :-
    get_texpr_info(TPred,Info),
    memberchk(nodeid(Pos),Info),
    get_position_filenumber(Pos,FilePos),
    memberchk(FilePos,FileNumbers).

cache_applicable(operations) :- !, cache_is_applicable_for_transitions.

cache_applicable(_) :- cache_is_applicable.

cache_file_exists(Type,Name,FullName) :-
    storage_file_name(Type,Name,FullName),
    (file_exists(FullName)
    -> debug_format(19,'value caching: ~w cache file ~w exists for ~w.~n',[Type, FullName, Name])
    ; get_tail_filename(FullName,Tail),
    formatsilent('value caching: ~w cache file ~w does not yet exist for ~w.~n',[Type, Tail, Name]),
    fail
).

cache_file_type(constants).

cache_file_type(operations_index).

cache_is_activated :-
    storage_directory(_).

cache_is_applicable :-
    is_applicable_internal(Applicable),!,Applicable=true.

cache_is_applicable :-
    cache_is_activated,
    % b_mode, % only for B models
    classical_b_mode,
    b_get_machine_refinement_hierarchy([_]), % only if there is no refinement - we cache no refinements
    preferences:get_preference(symmetry_mode,off), % with symmetry on: you cannot simply patch operation updates
    formatsilent('value persistance, cache IS applicable~n',[]),
    assert_once( is_applicable_internal(true) ),!.

cache_is_applicable :-
    debug_format(19,'value persistance, cache NOT applicable~n',[]),
    assert_once( is_applicable_internal(false) ),fail.

cache_is_applicable_for_transitions :-
    cache_is_applicable,
    get_preference(cache_operations,true).

check_if_all_constants_computed(_RefName,S) :-
    % make sure that all solutions have been generated
    load_max_reached(S,false),!.

check_if_all_constants_computed(RefName,_S) :-
    formatsilent('value caching: constants for referenced machine ~w not used because not all solutions were computed.~n',[RefName]),
    fail.

check_if_machine_has_no_parameters(RefName) :-
    machine_identifiers(RefName,Params,_Sets,_AVars,_CVars,_AConsts,_CConsts),
    ( Params=[] -> true
    ;
    formatsilent('value caching: constants of referenced machine ~w are not used because it uses parameters',[Params]),
    fail).

clear_applicable_flag :-
    retractall(is_applicable_internal(_)).

collect_computation_parameters(Name,[machine_name(Name)
    ,prob_revision(Revision)
    %,machine_hash(Hash)
    ,constants_signature(ConstSig)
    |Prefs]) :-
    find_relevant_preferences(Prefs),
    get_revision_info(Revision),
    %machine_hash(Name,Hash),
    compute_constants_signature(Name,ConstSig).

compare_computation_parameters([],[]) :- !.

compare_computation_parameters([CH|CT],[SH|ST]) :-
    !,compare_computation_parameters(CH,SH),
    compare_computation_parameters(CT,ST).

compare_computation_parameters(op_comp_parameters(C),op_comp_parameters(S)) :- !,
    compare_computation_parameters(C,S).

compare_computation_parameters(C,C) :- !.

compare_computation_parameters(C,S) :-
    formatsilent('value caching: parameter difference:~ncurrent is ~w,~n stored is ~w~n',[C,S]),
    fail.

compute_constants_signature(Name,constsig(Name,PropHash,Sublist)) :-
    properties_hash(Name,PropHash),
    findall(Sig,
    ( referenced_machine_with_constants_or_properties(Name,RefName),
    compute_constants_signature(RefName,Sig)),
    SubSigs),
    sort(SubSigs,Sublist).

compute_short_hash([A,B,C,D|_],Short) :-
    Short is A<<24 + B<<16 + C<<8 + D.

create_output_binding(Pattern,trans_cached(Param,Result,New,Info),
    trans_cached(Param,Result,Update,Info)) :-
    copy_term(Pattern,New/Update).

create_output_pattern(Ids,Values/Bindings) :-
    maplist(create_output_pattern2,Ids,Values,Bindings).

create_output_pattern2(Id,Value,bind(Id,Value)).

debug_params(op_comp_parameters(A),op_comp_parameters(B)) :- !,
    debug_params(A,B).

debug_params(preference(P,A),preference(P,B)) :- !,
    (A=B -> true ; print(P), print(':'), print(A/B), print(' ')).

debug_params([],[]) :- !,nl.

debug_params([preference(P1,A)|CT],[preference(P2,B)|ST]) :- !,
    (P1=P2 -> (A=B -> true ; format('Difference in preference ~w : current = ~w, stored = ~w~n',[P1,A,B])),
    debug_params(CT,ST)
    ; P1 @< P2 -> format('New preference ~w = ~w (not stored)~n',[P1,A]), debug_params(CT,[preference(P2,B)|ST])
    ; format('Stored preference removed ~w = ~w~n',[P2,B]), debug_params([preference(P1,A)|CT],ST)
).

debug_params([Cur|CT],[Stored|ST]) :- !,
    debug_params(Cur,Stored),
    debug_params(CT,ST).

debug_params(A,B) :- (A=B -> true ; print(A/B),nl).

delete_cache_file(MachName) :-
    cache_file_exists(operations_data,MachName,Filename),!,
    formatsilent('value caching: deleting opsdata cache file of machine ~w: ~w~n',[MachName,Filename]),
    delete_file(Filename).

file_suffix(constants,'.probcst').

file_suffix(operations_index,'.probops').

file_suffix(operations_data,'.opdata').

find_all_transitions(InStateId,OpName,Output,Transitions) :-
    findall( trans_cached(ParaValues,ResultValues,Updates,TransInfo),
    find_transition(InStateId,OpName,Output,ParaValues,ResultValues,Updates,TransInfo),
    Transitions).

find_constants(Name,Constants) :-
    machine_identifiers(Name,Params,_Sets,_AVars,_CVars,AbstractConstants,ConcreteConstants),
    ( Params=[_|_]
    -> add_warning(value_persistance,'Parameters not yet supported.'), % ok to just issue warning ?? or should we generate error ?
    fail
    ; true),
    append(AbstractConstants,ConcreteConstants,RawConstants),
    maplist(get_raw_identifier,RawConstants,Unsorted),
    sort(Unsorted,Constants).

find_constants_stores(Stores) :-
    findall(S,
    ( transition(root,Trans,I),
    functor(Trans,'$setup_constants',_),
    visited_expression(I,concrete_constants(S))
    ),
    Stores).

find_loadable_machines(Solutions) :-
    findall(loadable(Type,Machine),
    find_loadable_machines2(Type,Machine),
    Solutions).

find_loadable_machines2(Type,Machine) :-
    main_machine_name(Main),
    find_loadable_machines_sees_includes(Main,Type,Machine).

find_loadable_machines_includes(Start,Included) :-
    machine_includes(Start,_Prefix1,M),
    ( Included=M
    ; find_loadable_machines_includes(M,Included)).

find_loadable_machines_sees_includes(Main,main,Main).

find_loadable_machines_sees_includes(Main,sub,Seen) :-
    machine_sees(Main,Seen).

find_loadable_machines_sees_includes(Start,sub,Included) :-
    find_loadable_machines_includes(Start,Included).

find_matching_operations(Operation,MachName,FullNames) :-
    findall(O, is_matching_operation(Operation,MachName,O), FullNames).

find_operation_input_output(OpName,Input,Output) :-
    get_operation_info(OpName,Info),
    memberchk(reads(Input1),Info),
    % remove references to global sets and their elements
    get_all_sets_and_enum_ids(SEIds),
    remove_all(Input1,SEIds,Input),
    memberchk(modifies(Output),Info).

find_relevant_preferences(Prefs) :-
    findall(preference(Pref,Value), relevant_preference(Pref,Value), Unsorted),
    sort(Unsorted,Prefs).

find_transition(InStateId,OpName,Output,ParaValues,ResultValues,Updates,TransInfo) :-
    transition(InStateId,Operation,TransId,OutStateId),
    operation_name(Operation,OpName,ParaValues,ResultValues),
    findall(TI,transition_info(TransId,TI),TransInfo),
    visited_expression(OutStateId,OutState1), % we could use packed_visited_expression here ?
    state_corresponds_to_initialised_b_machine(OutState1,OutState),
    select_values(Output,OutState,Updates).

flush_data :-
    operations_index_file_opened(S),!,
    flush_output(S).

flush_data :- add_internal_error('No index file opened',flush_data).

format_verbose(verbose,Str,A) :- !, format(Str,A).

format_verbose(_,_,_).

generate_bindings(_Constants,Store,ConstantsBinding) :-
    % TODO: review this
    Store = ConstantsBinding.

get_all_max_reached_operations(MaxReachedList) :-
    findall(OpName, max_reached(OpName), MaxReached),
    sort(MaxReached,MaxReachedList).

get_all_sets_and_enum_ids(SEIds) :-
    findall(Id,
    ( is_b_global_constant(_,_,Id)
    ; b_global_set(Id)),
    SEIds).

get_bind_id(bind(Id,_),Id).

get_ids([Binding|_],Names) :- maplist(get_name,Binding,Names).

get_name(bind(ID,_),ID) :- !.

get_name(X,X).

get_operation_names(MachName,OperationNames) :-
    machine_operations(MachName,RawOperationNames),
    maplist(get_raw_identifier,RawOperationNames,OperationNames).

get_operations_computation_parameters(Name,op_comp_parameters(OpParams)) :-
    find_relevant_preferences(Prefs),
    get_revision_info(Revision),
    OpParams = [machine_name(Name),prob_revision(Revision)|Prefs].

get_operations_index_file(OI) :-
    operations_index_file_opened(OI),!.

get_operations_index_file(OI) :-
    add_internal_error('No operations_index file opened',get_operations_index_file(OI)),fail.

get_raw_identifier(identifier(_Pos,Id),Id).

get_raw_identifier(description(_Pos,_Desc,Raw),Id) :- get_raw_identifier(Raw,Id).

get_revision_info(info(V1,V2,V3,V4,ValuePersistanceRevision)) :-
    % revision(Revision), % revision not used: it differs between probcli and ProB Tcl/Tk
    version(V1,V2,V3,V4),
    ValuePersistanceRevision = '$Rev$'.

hash_input_values(OpName,MachName,InputPattern,SortedInState,Short,Long) :-
    %%statistics(runtime,[Start,_]), statistics(walltime,[WStart,_]),
    ( hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long) ->
    true
    %, statistics(runtime,[Stop,_]), Time is Stop - Start,
    % statistics(walltime,[WStop,_]), WTime is WStop - WStart,
    % tools:print_memory_used_wo_gc,
    % format('hashing time for ~w:~w = ~w (~w)~n',[OpName,MachName,Time,WTime])
    ; add_failed_call_error(hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long)),
    fail).

hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long) :-
    copy_term(InputPattern,lookup_pattern(SortedVars,SortedInputValues,_,InputValues)),
    select_values_sorted(SortedVars,SortedInState,SortedInputValues),
    raw_sha_hash(OpName/MachName/InputValues,Long),
    compute_short_hash(Long,Short).

inc_counter(C) :- (retract(counter(C,Nr)) -> N1 is Nr+1 ; N1 = 1),
    assertz(counter(C,N1)).

init_operation_cache(MachName,OpName) :-
    storable_operation(OpName,MachName,_InputPattern,_Output),!. % ignore, already registered

init_operation_cache(MachName,OpName) :-
    ( find_operation_input_output(OpName,Input,Output) ->
    lookup_pattern(Input,InputPattern),
    debug_println(9,find_operation_input_output(OpName,Input,Output)),
    assertz( storable_operation(OpName,MachName,InputPattern,Output) ),
    % Operations of the main machine are never prefixed
    create_output_pattern(Output,OutputPattern),
    assertz( loadable_operation(OpName,OpName,MachName,InputPattern,OutputPattern) )
    ;
    format('value caching: unable to generate input/output pattern for operation ~w.~n',
    [OpName])
).

initialise_operation_caching :-
    clear_applicable_flag,
    cache_is_applicable_for_transitions,
    main_machine_name(MachName), % if we have no machine name, fail silently (for default machine)
    !,
    % check wich operations are cachable and prepare information for them
    debug_println(9,initialise_operation_caching),
    retract_all_op_cache_data,
    try_to_load_operations_cache_for_all_machines,
    get_operation_names(MachName,OperationNames),
    maplist(init_operation_cache(MachName),OperationNames),
    save_operations_index_cache(MachName,OperationNames),
    open_data_file(MachName).

initialise_operation_caching :-
    retract_all_op_cache_data.

irrelevant_category(alloy2b).

irrelevant_category(cbc_commands). %cbc_provide_explanations

irrelevant_category(distb).

irrelevant_category(dot).

irrelevant_category(dot_definitions).

irrelevant_category(dot_event_hierarchy).

irrelevant_category(dot_formula_tree).

irrelevant_category(dot_machine_hierarchy).

irrelevant_category(dot_graph_generator).

irrelevant_category(dot_projection).

irrelevant_category(dot_state_graph).

irrelevant_category(dot_state_space).

irrelevant_category(dot_variable_modification).

irrelevant_category(gui_prefs).

irrelevant_category(latex).

irrelevant_category(mc_dc_commands).

irrelevant_category(smtlib2b).

irrelevant_category(state_as_graph).

irrelevant_category(syntax_highlighting).

irrelevant_category(table_commands).

irrelevant_category(trace_generator).

irrelevant_category(wd_commands).

irrelevant_preference(expand_avl_upto). % only affects pretty-printing

irrelevant_preference(bool_expression_as_predicate). % only used inside REPL/eval

irrelevant_preference(use_large_jvm_for_parser).

irrelevant_preference(expand_forall_upto). % only relevant in predicate analysis

irrelevant_preference(time_out). % if time_out occurs: no re-use anyway

irrelevant_preference(performance_monitoring_on). % just prints messages

irrelevant_preference(performance_monitoring_expansion_limit).

irrelevant_preference(kodkod_for_components) :- \+ preference(use_solver_on_load,kodkod).

irrelevant_preference(do_neginvariant_checking). % just indicates whether invariant evaluated doubly

irrelevant_preference(provide_trace_information). % just provides feedback; should not change values

irrelevant_preference(prob_profiling_on). % ditto

irrelevant_preference(prob_source_profiling_on). % ditto

irrelevant_preference(use_closure_expansion_memoization). % only influences performance

irrelevant_preference(warn_when_expanding_infinite_closures). % only generates extra warnings

irrelevant_preference(use_small_window).

irrelevant_preference(tk_show_source_pane).

irrelevant_preference(check_prolog_b_ast).

irrelevant_preference(use_font_size_for_columns).

irrelevant_preference(user_is_an_expert_with_accessto_source_distribution).

irrelevant_preference(default_to_runtime_type_checking_on_startup_for_expert).

irrelevant_preference(number_of_recent_documents).

irrelevant_preference(number_of_searched_patterns).

irrelevant_preference(number_of_replaced_patterns).

irrelevant_preference(number_of_eval_history_elements).

irrelevant_preference(number_of_eval_csp_history_elements).

irrelevant_preference(number_of_checked_ltl_formulas).

irrelevant_preference(machines_path).

irrelevant_preference(tlc_number_of_workers).

irrelevant_preference(tlc_use_prob_constant_setup).

irrelevant_preference(unsat_core_algorithm).

irrelevant_preference(deterministic_trace_replay).

irrelevant_preference(dot_use_ps_viewer).

irrelevant_preference(generate_minimal_nr_of_testcases).

irrelevant_preference(ltl_to_ba_tool).

irrelevant_preference(path_to_atb_krt).

irrelevant_preference(path_to_bcomp).

irrelevant_preference(path_to_cspm).

irrelevant_preference(path_to_csp_typechecker).

irrelevant_preference(path_to_dot).

irrelevant_preference(path_to_dotty).

irrelevant_preference(path_to_fdr).

irrelevant_preference(path_to_fuzz). %% ??

irrelevant_preference(path_to_latex).

irrelevant_preference(path_to_ltsmin).

irrelevant_preference(path_to_probe).

irrelevant_preference(path_to_ps_viewer).

irrelevant_preference(path_to_spin).

irrelevant_preference(path_to_text_editor).

irrelevant_preference(path_to_text_editor_launch).

irrelevant_preference(repl_cache_parsing).

irrelevant_preference(show_bvisual_formula_explanations).

irrelevant_preference(show_bvisual_formula_functor_from).

irrelevant_preference(show_function_tuples_in_property).

irrelevant_preference(symbolic_mc_try_other_solvers).

irrelevant_preference(use_scope_predicate).

irrelevant_preference(path_to_java).

irrelevant_preference(translate_print_all_sequences).

irrelevant_preference(translate_print_cs_style_sequences).

irrelevant_preference(view_probcli_errors_using_bbresults).

irrelevant_preference(trace_upon_error).

irrelevant_preference(error_log_file).

irrelevant_preference(tk_custom_state_viewer_padding).

irrelevant_preference(tk_custom_state_viewer_str_padding).

irrelevant_preference(tk_custom_state_viewer_font_name).

irrelevant_preference(tk_custom_state_viewer_font_size).

irrelevant_preference(use_tk_custom_state_viewer).

irrelevant_preference(X) :- preference_category(X,Cat), irrelevant_category(Cat).

is_matching_operation(Operation,MachName,Operation) :-
    % there is an operation with exactly the same name
    operation_with_machine(Operation,MachName).

is_matching_operation(Operation,MachName,FullName) :-
    atom_concat('.',Operation,DottedOp),
    operation_with_machine(FullName,MachName),
    atom_concat(_,DottedOp,FullName).

is_relevant_preference(Pref,_) :- nonvar(Pref),
    irrelevant_preference(Pref),!,fail.

is_relevant_preference(_Pref,animation).

is_relevant_preference(_Pref,hidden).

is_relevant_preference(_Pref,advanced).

is_usable_data(Constants,Stores) :-
    % at least one constant exists
    Constants = [_|_],
    % at least one state with computed constants was generated
    Stores = [_|_],
    % all constants have been computed
    \+ not_all_transitions_added(root),
    % no time-out in the root node
    \+ time_out_for_node(root).

load_constant_values(S,Stores) :-
    safe_constants_read(S,Term),
    ( Term = end_of_file ->
    Stores = []
    ; Term = values(constants,Store) ->
    unpack_constants(Store,UPS),
    Stores = [UPS|Rest],
    load_constant_values(S,Rest)).

load_constants(ConstantStores,MaxReached) :-
    cache_is_applicable, % check if storing/re-using constants is activated
    main_machine_name(Name),
    machine_file_exists(Name,FullName),
    open(FullName,read,S,[type(binary)]),
    call_cleanup(load_constants2(S,Name,ConstantStores,MaxReached),
    my_close(S)),!.

load_constants2(S,Name,ConstantStores,MaxReached) :-
    load_parameters(S,StoredParameters), % if the relevant computation parameters
    collect_computation_parameters(Name,CurrentParameters), % are different, we cannot re-use the
    (compare_computation_parameters(StoredParameters,CurrentParameters) % values stored in the file
    -> true
    ; formatsilent('value caching: parameters changed; not reusing previously computed constants for ~w.~n',[Name]),
    fail
    ),
    load_max_reached(S,MaxReached),
    load_constant_values(S,ConstantStores),
    (debug_mode(off) -> true
    ; length(ConstantStores,Len),
    get_ids(ConstantStores,CstNames),
    formatsilent('value caching: re-using ~w previously computed solutions for constants ~w for ~w.~n',[Len,CstNames,Name])
    ),
    assert_once( constants_loaded_from_file ).

load_max_reached(S,MR) :-
    safe_constants_read(S,maximum_reached(MR)).

load_parameters(S,StoredParameters) :-
    safe_constants_read(S,comp_parameters(StoredParameters)).

load_partial_constants(ConstantsBindings,InProperties,OutProperties) :-
    % TODO: - check if parameters / constraints have been used (what are the implications?)
    cache_is_applicable, % check if storing/re-using constants is activated
    main_machine_name(Name),
    findall( partial(MName,NewBindings),
    try_to_reuse_referenced_machine(Name,MName,NewBindings),
    PSol),
    PSol = [_|_],!,
    remove_evaluated_properties(PSol,InProperties,OutProperties),
    select_and_apply_binding(PSol,ConstantsBindings).

load_partial_constants(_ConstantsBindings,Properties,Properties).

load_sol_aux(FilenameData,Index,Solutions) :-
    open(FilenameData,read,S,[type(binary),reposition(true)]),
    call_cleanup((seek(S,Index,bof,_),
    fast_read(S,Solutions)), % read list of transition terms
    my_close(S)).

load_solutions(MachName,Index,Info,Solutions) :-
    storage_file_name(operations_data,MachName,FilenameData),
    catch(load_sol_aux(FilenameData,Index,ReadSolutions),
    Exc,
    (ajoin(['Corrupt opdata cache file for ',MachName,':'],Msg),
    add_error_fail(value_persistance,Msg,Exc))
    ),
    (ReadSolutions = trans_info(II,S) -> Solutions=S, Info=II ; Solutions=ReadSolutions, Info=[]).

lookup_cached_transitions(PrefixedOpName,InState,Info,OutputBindings) :-
    cache_is_applicable_for_transitions,
    loadable_operation(PrefixedOpName,OpName,MachName,InputPattern,OutputPattern),
    sort(InState,SortedInState),
    % statistics(runtime,[Start,_]), statistics(walltime,[WStart,_]),
    hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash),
    stored_transition(ShortHash,InputHash,OpName,Index),!,
    formatsilent('value caching: re-using values for operation ~w (~w -> ~w).~n',[OpName,ShortHash,Index]),
    ( load_solutions(MachName,Index,Info,Solutions) -> true
    %length(Solutions,Sn),
    %format('value caching: re-using ~w solutions for operation ~w of machine ~w.~n',
    % [Sn,OpName,MachName])
    ;
    format('value caching: re-using values for operation ~w failed.~n',[OpName]),
    fail),
    %print(solution(Solutions)),nl, print(pattern(OutputPattern)),nl,
    % OutputPattern is of the form [V1,...]/[bind(v1,V1),...]
    maplist(create_output_binding(OutputPattern),Solutions,OutputBindings).

lookup_pattern(Variables,lookup_pattern(SortedVariables,SortedValues,Variables,Values)) :-
    maplist(variable_value_pair,Variables,VarValues,Values),
    sort(VarValues,SortedVarValues),
    maplist(variable_value_pair,SortedVariables,SortedVarValues,SortedValues).

machine_file_exists(Name,FullName) :-
    cache_file_exists(constants,Name,FullName).

machine_file_number(Name,Nr) :-
    get_machine_file_number(Name,Ext,Nr,_),
    Ext \= 'def',!.

machine_file_number(Name,Nr) :-
    add_error(value_persistance,'Could not find machine name:',Name),
    bmachine:portray_filenumbers,
    Nr = -99.

machine_has_constants_or_properties(Name) :-
    machine_identifiers(Name,_Params,Sets,_AVars,_CVars,AConsts,CConsts),
    ( Sets=[_|_] ; AConsts==[_|_] ; CConsts=[_|_]),!.

machine_has_constants_or_properties_trans(Name) :-
    machine_has_constants_or_properties(Name),!.

machine_has_constants_or_properties_trans(Name) :-
    referenced_machine(Name,Ref,_,_),
    machine_has_constants_or_properties_trans(Ref),!.

machine_includes(MachA,Prefix,MachB) :-
    machine_references(MachA,References),
    member(ref(Type,MachB,Prefix),References),
    memberchk(Type,[includes,extends]).

machine_sees(MachA,MachB) :-
    machine_references(MachA,References),
    member(ref(Type,MachB,''),References),
    memberchk(Type,[sees,uses]).

my_close(Stream) :- !, close(Stream).

my_close(Stream) :- stream_property(Stream,file_name(F)),!,
    formatsilent('Closing ~w -> ~w~n',[F, Stream]),
    close(Stream).

my_close(Stream) :-
    formatsilent('Closing -> ~w~n',[Stream]),
    close(Stream).

my_open(File,Mode,St,Opt) :- !, safe_open_file(File,Mode,St,Opt).

my_open(File,Mode,St,Opt) :-
    safe_open_file(File,Mode,St,Opt),
    formatsilent('Opened file (~w) ~w -> ~w~n',[Mode,File,St]).

open_cache_file(Type,Name,Stream,Call) :-
    cache_file_exists(Type,Name,FullName),
    my_open(FullName,read,Stream,[type(binary)]),
    debug_format(19,'Opened cache file ~w~n',[FullName]),
    call_cleanup( (call(Call),!),my_close(Stream)).