value_persistance

add_new_transition_to_cache_from_expanded_state(root,_OpTerm,OutState,_CacheInfo) :-
    OutState = concrete_constants(_),!,
    save_constants_from_expanded_state(OutState).

add_new_transition_to_cache_from_expanded_state(InState,OpTerm,OutState,CacheInfo) :-
    cache_is_applicable_for_transitions,
    main_machine_name(MachName),
    operation_name(OpTerm,OpName,ParaValues,ResultValues),
    storable_operation(OpName,MachName,InputPattern,Output),
    \+ new_transition_not_worthwhile(CacheInfo,OpName),
    sort(InState,SortedInState),
    hash_input_values(OpName,MachName,InputPattern,SortedInState,ShortHash,InputHash), % can be expensive
    \+ 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),
    bb_inc(value_persistance_stored_transitions),
    store_transition_into_cache(OpName,ShortHash,InputHash,Transitions,MaxReached,MachName),
    formatinfo('value caching: storing single transition for operation ~w in execute mode (~w).', [OpName,ShortHash]),
    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,
    bb_inc_by(value_persistance_stored_transitions,Length),
    formatinfo('value caching: storing ~w transitions for operation ~w in state ~w (~w, state ~w, [~w] ms).',
    [Length,OpName,InStateId,ShortHash,Time,WTime]).

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

assert_stored_transition(ShortHash,Hash,OpName,Index) :- store_operation_has_stored_transition(OpName),
    assertz( stored_transition(ShortHash,Hash,OpName,Index) ).

bb_reset(Counter) :- bb_put(Counter,0).

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(constants) :- !, cache_is_applicable_for_constants.

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),
    formatinfo('value caching: ~w cache file ~w does not yet exist for ~w.',[Type, Tail, Name]),
    fail
).

cache_file_suffix(constants,'.probcst').

cache_file_suffix(operations_index,'.probops').

cache_file_suffix(operations_data,'.opdata').

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
    formatinfo('value caching: cache IS applicable',[]),
    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_constants :-
    cache_is_applicable, get_preference(cache_constants,true).

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) :-
    formatwarn('value caching: constants for referenced machine ~w not used because not all solutions were computed.',[RefName]),
    fail.

check_if_machine_has_no_parameters(RefName) :-
    machine_identifiers(RefName,Params,_Sets,_AVars,_CVars,_AConsts,_CConsts),
    ( Params=[] -> true
    ;
    formatwarn('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) :-
    formatwarn('value caching: parameter difference:~ncurrent is ~w,~n stored is ~w.',[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),!,
    formatinfo('value caching: deleting opdata cache file of machine ~w: ~w',[MachName,Filename]),
    delete_file(Filename).

delete_cache_files :-
    reset_operations_index_file_opened, % to ensure we can delete the files
    find_loadable_machines(LoadableMachines),
    maplist(delete_cache_files_for_machine(_),LoadableMachines).

delete_cache_files_for_machine(Machine) :-
    reset_operations_index_file_opened, % to ensure we can delete the files
    delete_cache_files_for_machine(_,loadable(main,Machine)).

delete_cache_files_for_machine(ExpectedType,loadable(_MType,MachName)) :-
    cache_file_suffix(Type,_), % backtracks and also matches operations_data
    (var(ExpectedType) -> true ; ExpectedType=Type),
    (cache_file_exists(Type,MachName,FullName)
    -> get_tail_filename(FullName,FF),
    format_with_colour_nl(user_output,[blue],'Deleting ~w cache file for machine ~w: ~w',[Type,MachName,FF]),
    delete_file(FullName)
    ; format_with_colour_nl(user_output,[blue],'No cache file of type ~w found for machine ~w',[Type,MachName])
    ),fail.

delete_cache_files_for_machine(_,_).

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_main_constants(Constants) :- b_get_machine_constants(C),
    sort(C,Constants).

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 :-
    findall(M,(operations_index_file_opened(M,S),flush_output(S)),L),
    (L=[] -> add_internal_error('No index file opened',flush_data) ; true).

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

format_verbose(_,_,_).

formatdetails(_Format,_Args) :- silent_mode(on), debug_mode(on),
    !.

formatdetails(Format,Args) :-
    format_with_colour_nl(user_output,[grey],Format,Args).

formatgood(_Format,_Args) :- silent_mode(on),!.

formatgood(Format,Args) :-
    format_with_colour_nl(user_output,[green],Format,Args).

formatinfo(_Format,_Args) :- silent_mode(on),!.

formatinfo(Format,Args) :-
    format_with_colour_nl(user_output,[grey],Format,Args).

formatwarn(Format,Args) :-
    format_with_colour_nl(user_output,[orange],Format,Args).

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) :-
    if(machine_operations(MachName,RawOperationNames),
    maplist(get_raw_identifier,RawOperationNames,OperationNames),
    add_error_fail(value_persistance,'Cannot find machine:',MachName)).

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(Machine,OI) :-
    operations_index_file_opened(Machine,F),!,OI=F.

get_operations_index_file(Machine,OI) :-
    add_internal_error('No operations_index file opened',get_operations_index_file(Machine,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$'.

get_value_persistance_stats(List) :-
    findall(Counter-Value,(is_counter(Counter),bb_safe_get(Counter,Value)),List).

hash_input_values(OpName,MachName,InputPattern,SortedInState,Short,Long) :-
    % tools:start_ms_timer(T1),
    % write(hash(OpName,MachName,InputPattern,SortedInState)),nl,
    ( hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long) ->
    true
    %,tools:stop_ms_walltimer_with_msg(T1,time_hashing(OpName,MachName))
    % tools:print_memory_used_wo_gc,
    ; add_failed_call_error(hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long)),
    fail).

hash_input_values2(OpName,MachName,InputPattern,SortedInState,Short,Long) :-
    start_profile(OpName,T1),
    copy_term(InputPattern,lookup_pattern(SortedVars,SortedInputValues,InputVarsAndCsts,InputValues)),
    select_values_sorted(SortedVars,SortedInState,SortedInputValues),
    l_pre_hash(InputVarsAndCsts,InputValues,PreHashedInputValues),
    % terms:term_size(PreHashedInputValues,Sz), write(hash(OpName,SortedVars,Sz)),nl,
    % tools_printing:print_term_summary(raw_sha_hash(OpName,PreHashedInputValues)),nl,
    raw_sha_hash(OpName/MachName/PreHashedInputValues,Long),
    compute_short_hash(Long,Short),
    stop_profile(OpName,cache_hashing_input_values,unknown,T1).

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) :-
    \+ b_top_level_operation(OpName), !,
    % only store top-level operations for which we compute all solutions at the moment
    % for subsidiary operations we do a call by predicate; much more difficult to cache/store
    formatinfo('value caching: Not storing subsidiary operation ~w in machine ~w',[OpName,MachName]).

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)),
    formatinfo('value caching: Storable operation ~w in machine ~w',[OpName,MachName]),
    bb_inc(value_persistance_storeable_operations),
    assertz( storable_operation(OpName,MachName,InputPattern,Output) ),
    % Operations of the main machine are never prefixed
    create_output_pattern(Output,OutputPattern),
    (loadable_operation(OpName,_,_,_,_) -> true
    ; bb_inc(value_persistance_loadable_operations), % see also store_loadable_operation
    assertz( loadable_operation(OpName,OpName,MachName,InputPattern,OutputPattern) )
    )
    ;
    formatwarn('value caching: unable to generate input/output pattern for operation ~w.~n',[OpName])
).

initialise_op_cache_for_machine(loadable(_,MachName)) :-
    bb_inc(value_persistance_op_cache_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 :-
    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(MachName)),
    retract_all_op_cache_data,
    try_to_load_operations_cache_for_all_machines,
    %initialise_op_cache_for_machine(MachName),
    find_loadable_machines(LoadableMachines),
    formatinfo('value caching: loadable machines: ~w',[LoadableMachines]),
    maplist(initialise_op_cache_for_machine,LoadableMachines).

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(visb).

irrelevant_category(wd_commands).

irrelevant_preference(cache_operations_runtime_limit). % only influences what gets stored; re-use always safe

irrelevant_preference(cache_constants). % ditto

irrelevant_preference(cache_operations). % ditto

irrelevant_preference(clash_strict_checks). % no influence on values computed

irrelevant_preference(strict_raise_warnings). % no influence on values computed

irrelevant_preference(warn_if_definition_hides_variable). % no influence on values computed

irrelevant_preference(jvm_parser_heap_size_mb). % no influence on values computed

irrelevant_preference(jvm_parser_additional_args). % ditto

irrelevant_preference(use_safety_ltl_model_checker). % ditto

irrelevant_preference(store_only_one_incoming_transition). % ditto

irrelevant_preference(forget_state_space). % ditto

irrelevant_preference(type_check_definitions). % ditto

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_clingo).

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_bvisual_proof_info_icons).

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(translate_suppress_rodin_positions_flag).

irrelevant_preference(translate_ids_to_parseable_format).

irrelevant_preference(translate_print_frozen_infos).

irrelevant_preference(translate_print_typing_infos).

irrelevant_preference(translate_force_all_typing_infos).

irrelevant_preference(prob_lastchangedate_info). % what about prob_revision_info ?

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

is_counter(value_persistance_constants_loaded).

is_counter(value_persistance_ref_constants_loaded).

is_counter(value_persistance_loadable_operations).

is_counter(value_persistance_op_cache_machines).

is_counter(value_persistance_loadable_operations).

is_counter(value_persistance_storeable_operations).

is_counter(value_persistance_reused_transitions).

is_counter(value_persistance_stored_transitions).

is_counter(value_persistance_not_worth_transitions).

is_counter(value_persistance_refresh_transitions).

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(MachName,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)
    -> formatwarn('value caching: not storing constants for ~w as not all transitions computed.',[MachName]), fail
    ; true),
    % no time-out in the root node
    (time_out_for_node(root)
    -> formatwarn('value caching: not storing constants for ~w as TIME_OUT occured.',[MachName]), fail
    ; true).