predicate_evaluator

analyse_quick_time_out(Call) :-
    get_time_out_preference_with_factor(0.05,DTimeOut),
    (DTimeOut > 400 -> TO = 400 ; TO = DTimeOut),
    on_enumeration_warning(
    safe_time_out(Call,TO,Res),
    fail), % in case of enumeration warnings: we could not compute all elements of domain
    \+ is_time_out_result(Res).

analyze_all_conjuncts2(Kind,BExpr, RealCurState, CList) :-
    findall(conj(Nr,Conjunct,Status,EnumWarning,IsExpanded),
    (%get_and_inc_conj_nr(Nr), print(analysing_conjunct(Nr)),nl,
    b_analyse_conjunction(Kind,BExpr,[],RealCurState,Nr,Conjunct,Status,EnumWarning,IsExpanded)
    ),
    CList).

b_analyse_boolean_expression(VAR,Kind,P,L,S) :- var(VAR),!,
    add_internal_error('Illegal call: ',b_analyse_boolean_expression(VAR,Kind,P,L,S)),
    S=[unknown/1].

b_analyse_boolean_expression(BExpr,Kind,Partition,List,
    [total/NrTotal, total_after_expansion/NrTotalExpanded,
    true/NrTrue, true_after_expansion/NrTrueExpanded,
    false/NrFalse, false_after_expansion/NrFalseExpanded,
    unknown/NrUnknown, unknown_after_expansion/NrUnknownExpanded,
    timeout/NrTimeout, runtime/TotalTime, enum_warning/NrEnumWarning]) :-
    get_current_b_expression(RealCurState),
    %reset_conj_nr,
    statistics(walltime,[CurTime,_]), /* get current time in ms */
    b_analyze_all_sub_conjuncts(Kind,Partition,BExpr, RealCurState, CList),
    statistics(walltime,[CurTime2,_]), /* get current time in ms */
    formatsilent('~N=======~NSUMMARY (~w)~N=======~N',[Kind]),
    new_counter(Counter0),
    l_translate_conjunct_analysis_result(CList,List,none/true,'$_no_model'(none),Counter0,ResCounter),
    %print_counter(ResCounter),
    get_counter(total,ResCounter,NrTotal), get_counter(total_after_expansion,ResCounter,NrTotalExpanded),
    get_counter(true,ResCounter,NrTrue), get_counter(true_after_expansion,ResCounter,NrTrueExpanded),
    get_counter(false,ResCounter,NrFalse), get_counter(false_after_expansion,ResCounter,NrFalseExpanded),
    get_counter(unknown,ResCounter,NrUnknown), get_counter(unknown_after_expansion,ResCounter,NrUnknownExpanded),
    get_counter(timeout,ResCounter,NrTimeout), get_counter(enum_warning,ResCounter,NrEnumWarning),
    (silent_mode(on),NrFalse==0,NrUnknown==0 -> true
    ; NrTotal=NrTotalExpanded
    -> format('~p predicates: ~p TRUE, ~p FALSE, ~p UNKNOWN (~p timeouts)~N',[NrTotal,NrTrue,NrFalse,NrUnknown,NrTimeout])
    ; format('~p predicates (~p after expansion): ~p TRUE (~p after expansion), ~p FALSE (~p after expansion), ~p UNKNOWN (~p after expansion) (~p timeouts)~N',[NrTotal,NrTotalExpanded,NrTrue,NrTrueExpanded,NrFalse,NrFalseExpanded,NrUnknown,NrUnknownExpanded,NrTimeout])),
    TotalTime is CurTime2-CurTime,
    formatsilent('~w ms to analyse ~w~n',[TotalTime,Kind]).

b_analyse_conjunction(Kind,Conj, LocalState,State,Nr,EvConjunct,Status,EnumWarning,IsExpanded) :-
    flatten_conjunction(Conj,ConjList,[]),
    nth1(Nr, ConjList, Conjunct),
    b_analyse_conjunction_nr(Kind,Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded).

b_analyse_conjunction_nr(Kind,Nr,b(forall(Parameters,LHS,RHS),pred,Info),LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded) :-
    IsExpanded=true,
    get_preference(expand_forall_upto,MaxLenForEpxansion),
    MaxLenForEpxansion>0,
    % print(generating_for_all_domain(Parameters)),nl,
    analyse_quick_time_out((
    kernel_waitflags:init_wait_flags_with_call_stack(WF,[prob_command_context(analyse_quick_time_out,Info)]),
    b_interpreter:b_generate_for_all_list_domain_nolwf(Parameters,LHS,RHS,LocalState,State,AllSols,NewRHS,WF),
    kernel_waitflags:ground_wait_flags(WF))),
    length(AllSols,Len), Len>0, Len=<MaxLenForEpxansion,!,
    (silent_mode(on) -> true ; print('FORALL domain computed: '), translate:print_bexpr(LHS),nl),
    member(ParResult,AllSols),
    set_up_equality(Parameters,ParResult,EqList),
    conjunct_predicates(EqList,EqPred),
    EvConjunct = b(forall(Parameters,EqPred,RHS),pred,Info),
    (debug_mode(on) -> print('Testing: '), print_bexpr(EvConjunct),nl ; true),
    set_up_typed_localstate(Parameters,ParResult,_,LocalState,NewLocalState,positive),
    b_analyse_individual_conjunct(Kind,Nr,NewRHS,NewLocalState,State,_,Status,EnumWarning).

b_analyse_conjunction_nr(Kind,Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded) :-
    %debug:debug_println(9,analysing_conjunct_in_component(Nr)),
    IsExpanded=false,
    b_analyse_individual_conjunct(Kind,Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning).

b_analyse_individual_conjunct(Kind,Nr,Conjunct,LocalState,State,Conjunct,Status,EnumWarning) :-
   
    get_computed_preference(debug_time_out,DTimeOut),
   
    (silent_mode(on) -> true
    ; nl,print('==> '),translate:print_bexpr(Conjunct),nl),
    %translate:print_bexpr_with_limit(Conjunct,250),nl,
    statistics(walltime,[T1,_]),
    enter_new_error_scope(ScopeID,b_analyse_individual_conjunct),
    (time_out_and_catch_errors(b_test_boolean_expression_cs(Conjunct,LocalState,State,Kind,Nr),
    DTimeOut,TimeOutRes) ->
    /* PREDICATE TRUE */
    statistics(walltime,[T2,_]),check_enum_warning(positive,EnumWarning),
    exit_error_scope(ScopeID,ErrOcc,b_analyse_individual_conjunct_true), % Warning: if strict_raise_warnings is set to true we also get the warnings as errors here !!
    (TimeOutRes=time_out
    -> print_red('TIMEOUT'),nl,Status=timeout
    ; ErrOcc=true -> (get_preference(strict_raise_warnings,true) -> print('POSSIBLY ') ; true),
    print_red('NOT-WELL-DEFINED (TRUE)'),nl, Status = wd_error_true
    ; print_true,
    enter_new_error_scope(NegScopeID,b_analyse_double_evaluation_true),
    ((get_preference(double_evaluation_when_analysing,true),
    time_out_and_catch_errors(b_not_test_boolean_expression_cs(Conjunct,LocalState,State,Kind,Nr),
    DTimeOut,TimeOutRes2))
    -> (TimeOutRes2==time_out -> Status = timeout_true
    ; Status = both_true_false,
    add_error(predicate_evaluator,'Conjunct is both true and false: ',Conjunct,Conjunct)
    )
    ; Status = 'TRUE' ),
    check_enum_warning(_,_NegEnumWarning),
    exit_error_scope(NegScopeID,_NegTErrorOccurred,b_analyse_double_evaluation_true) % Should we also report those errors ? + NegEnumWarning ?
    )
    ; /* PREDICATE FALSE */
    statistics(walltime,[T2,_]), check_enum_warning(negative,EnumWarning),
    exit_error_scope(ScopeID,ErrOcc,b_analyse_individual_conjunct_false),
    (ErrOcc=true
    -> print_red('NOT-WELL-DEFINED (FALSE)'),nl, Status = wd_error_false
    ; (EnumWarning=true -> print_red('UNKNOWN'),nl
    ; print_false),
    enter_new_error_scope(NegScopeID,b_analyse_double_evaluation_false),
    ((get_preference(double_evaluation_when_analysing,false) ;
    time_out_and_catch_errors(
    b_not_test_boolean_expression_cs(Conjunct,LocalState,State,Kind,Nr),
    DTimeOut,TimeOutRes2))
    -> (TimeOutRes2==time_out -> Status = timeout_false ; Status = false)
    ; Status = unknown),
    exit_error_scope(NegScopeID,_NegFErrorOccurred,b_analyse_double_evaluation_false) % Should we also report those errors ? + NegEnumWarning ?
    )
    ),
    statistics(walltime,[T3,_]),
    Time1 is T2-T1, Time2 is T3-T2, Time is T3-T1,
    (silent_mode(on) -> true
    ; format('~w (~w ms + ~w ms = ~w ms)',[Status,Time1,Time2,Time]),
    (Status = 'TRUE' -> true
    ; translate:translate_span(Conjunct,SpanS), SpanS \= '' -> print(' '),print(SpanS)
    ; true),nl
).

b_analyze_all_sub_conjuncts(Kind,true,BExpr, RealCurState, CList) :- !,
    bsyntaxtree:predicate_components(BExpr,Components), % Note: does not support list of conjunctions (as generated by b_get_assertions_from_machine)
    findall(comp_res(CCList,CompVars),
    (member(component(CompBExpr,CompVars),Components),
    analyze_all_conjuncts2(Kind,CompBExpr, RealCurState, CCList)),CompRes),
    flatten_comp_res(CompRes,CList).

b_analyze_all_sub_conjuncts(Kind,_Partition,BExpr, RealCurState, CList) :-
    analyze_all_conjuncts2(Kind,BExpr, RealCurState, CList).

call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, TranslatedConjunct) :-
    convert_status(Status,ConvStatus),
    conjunct_error_hook_pred(Pred),
    call(Pred,Conjunct,ConvStatus,EnumWarning,IsExpanded, TranslatedConjunct).

call_residue_check(Call) :-
    call_residue(Call,Residue),
    (Residue = [] -> true
    ; add_internal_error('Call had residue: ',residue(Residue)/call(Call)),
    print_goal(Residue),nl
).

check_enum_warning(positive,EnumWarning) :- !,
    (enumeration_warning_occured_in_error_scope
    -> print('### Enumeration warnings not critical (solution found)'),nl %, error_manager:trace_if_user_wants_it
    ; true), EnumWarning = false.

check_enum_warning(_,EnumWarning) :-
    \+ critical_enumeration_warning_occured_in_error_scope,!,
    EnumWarning = false.

check_enum_warning(_,EnumWarning) :-
    (event_occurred_in_error_scope(enumeration_warning(enumerating(_),_,_,_,_))
    -> print('### Warning: infinite types were enumerated'),nl, E1=true
    ; true),
    (event_occurred_in_error_scope(enumeration_warning(checking_finite_closure,_,_,_,_))
    -> print('### Warning: finiteness of comprehension sets could not be determined'),nl, E2=true
    ; true),
    (var(E1),var(E2)
    -> print('### Unknown enumeration warning occurred !')
    ; true),
    EnumWarning = true.

check_summary_all_true(L) :-
    member(total_after_expansion/Nr,L), member(true_after_expansion/Nr,L),
    member(false/0,L), member(unknown/0,L), member(timeout/0,L).

combine_static_dynamic_result([],L,L).

combine_static_dynamic_result(L,[],L).

combine_static_dynamic_result(S,D,List) :-
    List = ['STATIC ASSERTIONS:\n'|List0],
    append(S,['DYNAMIC ASSERTIONS:\n'|D],List0).

combine_status(true,X,R) :- convert_status(X,R).

combine_status(false,_,false).

combine_status(unknown,false,R) :- !,R=false.

combine_status(unknown,_,unknown).

combine_summary([],S,S).

combine_summary([K/V|T],S,R) :- update(S,K,V,S2), combine_summary(T,S2,R).

conjunct_error_hook_pred(default_hook).

convert_status('TRUE',true) :- !.

convert_status(timeout_true,true) :- !.

convert_status(false,false) :- !.

convert_status(timeout_false,false) :- !.

convert_status(_,unknown).

current_b_state_with_all_constants_valued :-
    (current_state_corresponds_to_setup_constants_b_machine -> true
    ; \+ b_machine_has_constants). % also allow analysis if we have no constants (but possibly properties)

default_hook(_,_Status,_,_, _CS).

do_not_decompose(C) :- bsyntaxtree:get_texpr_labels(C,_),!. % otherwise the user wants to group it

do_not_decompose(C) :- get_texpr_info(C,Infos),
    member(generated_conjunct,Infos). % the conjunct has been generated, e.g., by b_ast_cleanup

empty_summary([total/0, total_after_expansion/0,
    true/0, true_after_expansion/0, false/0, false_after_expansion/0,
    unknown/0, unknown_after_expansion/0, timeout/0, runtime/0, enum_warning/0]).

flatten_comp([],[],0).

flatten_comp([H|T],['COMPONENT:\n'|Res],NrConjuncts) :-
    flatten_comp(T,TR,TNr),
    length(H,LH), NrConjuncts is LH+TNr,
    append(H,TR,Res).

flatten_comp_res([],[]).

flatten_comp_res([comp_res(CCList,Vars)|T],Res) :-
    flatten_comp_res(T,FT),
    append([vars(Vars)|CCList],FT,Res).

flatten_conjunction([]) --> !, [].

flatten_conjunction([H|T]) --> !, flatten_conjunction(H),flatten_conjunction(T).

flatten_conjunction(C) --> {is_a_conjunct(C,LHS,RHS)},
    {\+ do_not_decompose(C)}, % otherwise the user wants to group it
    !,
    flatten_conjunction(LHS), flatten_conjunction(RHS).

flatten_conjunction(C) --> [C].

flush_cur_status(CurConjNr,CurStatus,Acc,NewAcc2) :-
    (CurConjNr==none -> Acc=NewAcc2
    ; inc_counter(total,Acc,NewAcc1),
    (CurStatus = true -> inc_counter(true,NewAcc1,NewAcc2)
    ; CurStatus = false -> inc_counter(false,NewAcc1,NewAcc2)
    ; inc_counter(unknown,NewAcc1,NewAcc2)) ).

get_as_undefined(Conjunct,Translation) :- translate_conj_status(Conjunct,undefined,false,Translation).

get_assertions_as_undefined(ALL,SD,List) :-
    b_get_assertions(ALL,SD,Ass),
    flatten_conjunction(Ass,FAss,[]),
    maplist(get_as_undefined,FAss,List).

get_conjunct(C,Conjunct,Status) :- is_a_conjunct(C,LHS,RHS),!,
    (get_conjuncts(LHS,Conjunct,Status) ; get_conjuncts(RHS,Conjunct,Status)).

get_conjunct(Conjunct,Translation,Status) :-
    translate_conj_status(Conjunct,Status,false,Translation).

get_conjuncts(BoolExpr,Conjuncts,Status) :- findall(C,get_conjunct(BoolExpr,C,Status),Conjuncts).

get_counter(Key,C,Val) :- (get_assoc(Key,C,Val) -> true ; Val =0).

get_current_b_expression(S) :-
    (current_b_expression(S) -> true
    ; current_state_id(root), \+ b_machine_has_constants -> S = []
    ; add_internal_error('Could not get B state for analysis',get_current_b_expression(S)),S=[]
).

inc_counter(Key,C,NC) :- (get_assoc(Key,C,Val) -> NewVal is Val+1 ; NewVal =1),
    put_assoc(Key,C,NewVal,NC).

l_translate_conjunct_analysis_result([],[],CurConjNr/CurStatus,_LastModel,Acc,ResAcc) :-
    flush_cur_status(CurConjNr,CurStatus,Acc,ResAcc).

l_translate_conjunct_analysis_result([vars(Vars)|T],Res,CurConjNr/CurStatus,_LastModel,Acc,CRes) :-
    flush_cur_status(CurConjNr,CurStatus,Acc,Acc1),
    (Vars=[] -> Res = ['** ISOLATED CONJUNCT **\n'|TT]
    ; Res = [CS,CV,' **\n'|TT], CS = '** CONJUNCTS OVER IDENTIFIERS:'),
    translate_term_into_atom(Vars,CV),
    l_translate_conjunct_analysis_result(T,TT,none/true,'$_no_model'(none),Acc1,CRes).

l_translate_conjunct_analysis_result([conj(NextNr,Conjunct,Status,EnumWarning,IsExpanded)|T],TranslationResult,CurConjNr/CurStatus,LastModel,Acc,CRes) :-
    translate_conjunct(Conjunct,Status,EnumWarning,CS),
    inc_counter(total_after_expansion,Acc,AA),
    (EnumWarning==true -> inc_counter(enum_warning,AA,A1) ; AA=A1),
    ( Status = 'TRUE' -> inc_counter(true_after_expansion,A1,NewAcc)
    ; Status = timeout_true -> inc_counter(true_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc)
    ; Status = false -> inc_counter(false_after_expansion,A1,NewAcc)
    ; Status = timeout_false -> inc_counter(false_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc)
    ; Status = both_true_false -> inc_counter(unknown_after_expansion,A1,NewAcc)
    ; Status = wd_error_true -> inc_counter(unknown_after_expansion,A1,NewAcc)
    ; Status = wd_error_false -> inc_counter(unknown_after_expansion,A1,NewAcc)
    ; inc_counter(unknown_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc)
    ),
    (call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, CS) -> true
    ; add_internal_error('Conjunct error hook failed: ',
    call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, CS))),
    (CurConjNr==NextNr
    -> combine_status(CurStatus,Status,NewStatus), NewAcc=NewAcc2 % still the same conjunct; combine status
    ; flush_cur_status(CurConjNr,CurStatus,NewAcc,NewAcc2),
    convert_status(Status,NewStatus)),
    ((get_rodin_model_name(Conjunct,NewModel), NewModel \= LastModel)
    -> TranslationResult = [' * MODEL: ',NewModel,'\n',CS|TT] % show from which model the conjuncts come from
    ; NewModel = LastModel, TranslationResult = [CS|TT]),
    l_translate_conjunct_analysis_result(T,TT,NextNr/NewStatus,NewModel,NewAcc2,CRes).

new_counter(C) :- empty_assoc(C).

print_false :- silent_mode(on),!.

print_false :- print_red('FALSE'),nl.

print_true :- silent_mode(on),!.

print_true :- print_green('TRUE'),nl.

register_conjunct_error_hook(Pred) :- retractall(conjunct_error_hook_pred(_)), assertz(conjunct_error_hook_pred(Pred)).

register_conjunct_register_error_span :- register_conjunct_error_hook(register_span_hook).

register_span_hook(Conjunct,ConvStatus,_EnumWarning,_IsExpanded, _TranslatedConjunct) :-
    %print(status(ConvStatus)),nl,
    (ConvStatus=true -> true ; register_error_span(predicate_evaluator,Conjunct)). % store positions for Tcl/Tk

reset_conjunct_error_hook :- retractall(conjunct_error_hook_pred(_)), assertz(conjunct_error_hook_pred(default_hook)).

set_up_equality([],[],[]).

set_up_equality([Identifier|IR],[Val|VR],[b(equal(Identifier,b(value(Val),IDType,[])),pred,[])|TE]) :-
    get_texpr_type(Identifier,IDType),
    set_up_equality(IR,VR,TE).

tcltk_analyse_assertions(List,Summary) :- tcltk_analyse_assertions(all,List,Summary).

tcltk_analyse_assertions(_ALL,list(['CSP Assertions'|CA]),TSummary) :-
    (animation_mode(cspm) ; csp_with_bz_mode),!,
    statistics(walltime,[CurTime,_]), /* get current time in ms */
    tcltk_interface:tcltk_check_csp_assertions(CA,Summary),
    statistics(walltime,[CurTime2,_]), /* get current time in ms */
    Delta is CurTime2-CurTime,
    TSummary = [runtime/Delta|Summary],
    format('% CSP Assertion Checks Completed: ~w~n',[CA]).

tcltk_analyse_assertions(all,list(['This Machine has no ASSERTIONS.']),Summ) :-
    b_get_dynamic_assertions_from_machine([]),b_get_static_assertions_from_machine([]),!,empty_summary(Summ).

tcltk_analyse_assertions(main,list(['The Main Machine has no ASSERTIONS.']),Summ) :-
    b_main_machine_has_no_assertions,
    !,empty_summary(Summ).

tcltk_analyse_assertions(ALL,list(List),Summary) :-
    current_state_corresponds_to_fully_setup_b_machine,!,
    %conjunct_predicates(Ass,BExpr)
    b_get_assertions(ALL,static,SAss),
    println_silent('Checking Static Assertions'),
    % translate:nested_print_bexpr(SAss),
    b_analyse_boolean_expression(SAss,'ASSERTIONS (static)',false,SList,SSummary),
    b_get_assertions(ALL,dynamic,DAss),
    println_silent('Checking Dynamic Assertions'),
    b_analyse_boolean_expression(DAss,'ASSERTIONS (dynamic)',false,DList,DSummary),
    combine_summary(SSummary,DSummary,Summary),
    combine_static_dynamic_result(SList,DList,List).

tcltk_analyse_assertions(ALL,list(ListRes),Summary) :-
    current_b_state_with_all_constants_valued,
    b_get_assertions(ALL,static,Ass),Ass\=[],!,
    b_analyse_boolean_expression(Ass,'ASSERTIONS',false,SList,SSummary),
    b_get_assertions(ALL,dynamic,DynAss),
    (DynAss=[] -> ListRes = List, Summary = SSummary
    ; ListRes = ['Only evaluating STATIC ASSERTIONS.\nInitialise machine to evaluate other ASSERTIONS.\n\n'|List],
    (length(DynAss,Len) -> true ; Len=1),
    unknown_summary(Len,US),combine_summary(US,SSummary,Summary)
    ),
    get_assertions_as_undefined(ALL,dynamic,DList),
    combine_static_dynamic_result(SList,DList,List).

tcltk_analyse_assertions(ALL,list(['Cannot evaluate assertions yet.\nInitialise machine first.\n\n'|List]),Summary) :-
    print('*** Cannot evaluate ASSERTIONS\nSPECIFICATION not initialised.'),nl,
    get_assertions_as_undefined(ALL,static,SList),
    get_assertions_as_undefined(ALL,dynamic,DList),
    length(SList,SL), length(DList,DL), TL is SL+DL, unknown_summary(TL,Summary),
    combine_static_dynamic_result(SList,DList,List).

tcltk_analyse_deadlock(list(List),Summary) :- current_state_corresponds_to_fully_setup_b_machine,!,
    get_unsorted_all_guards_false_pred(BExpr),
    b_analyse_boolean_expression(BExpr,'DEADLOCK (guard disjunction)',false,List,Summary).

tcltk_analyse_deadlock(list(['Cannot evaluate deadlock yet.\nInitialise machine first.\n\n'|List]),[]) :-
    get_unsorted_all_guards_false_pred(BExpr),
    get_conjuncts(BExpr,List,undefined).

tcltk_analyse_goal(List) :- tcltk_analyse_goal(List,_).

tcltk_analyse_goal(list(List),Summary) :-
    current_b_state_with_all_constants_valued,
    b_get_machine_goal(Goal),!,
    b_analyse_boolean_expression(Goal,'GOAL',false,List,Summary).

tcltk_analyse_goal(list(['Cannot evaluate GOAL yet.\nSetup constants first.\n\n'|List]),Summary) :-
    b_get_machine_goal(Goal),!,
    get_conjuncts(Goal,List,undefined), unknown_summary(1,Summary).

tcltk_analyse_goal(list(['Cannot find GOAL DEFINITION (must be a predicate).\n']),Summary) :-
    unknown_summary(1,Summary).

tcltk_analyse_invariant(list(List),Summary) :-
    current_state_corresponds_to_fully_setup_b_machine,!,
    b_get_invariant_from_machine(Invariant),
    get_preference(partition_predicates,Partition),
    b_analyse_boolean_expression(Invariant,'INVARIANT',Partition,List,Summary).

tcltk_analyse_invariant(list(['Cannot evaluate invariant yet.\nInitialise machine first.\n\n'|List]),Summary) :-
    b_get_invariant_from_machine(Invariant),
    get_conjuncts(Invariant,List,undefined),
    length(List,TL), unknown_summary(TL,Summary).

tcltk_analyse_properties(list([Res]),[]) :-
    b_get_properties_from_machine(b(truth,_,_)),!,
    (b_machine_has_constants
    -> Res = 'This Machine has only typing information in the PROPERTIES.'
    ; Res = 'This Machine has no PROPERTIES clause.'
).

tcltk_analyse_properties(list(List),Summary) :-
    current_b_state_with_all_constants_valued,
    !,
    b_get_properties_from_machine(Prop),
    get_preference(partition_predicates,Partition),
    b_analyse_boolean_expression(Prop,'PROPERTIES',Partition,List,Summary).

tcltk_analyse_properties(list(['Cannot evaluate properties yet.\nSet up constants first.\n\n'|List]),Summary) :-
    b_get_properties_from_machine(Prop),
    (get_preference(partition_predicates,false)
    -> get_conjuncts(Prop,List,undefined), length(List,NrConjuncts)
    ; bsyntaxtree:predicate_components(Prop,Components),
    findall(CList,
    (member(component(CP,_CompVars),Components),
    get_conjuncts(CP,CList,undefined)), CCList),
    flatten_comp(CCList,List,NrConjuncts)
    ),
    unknown_summary(NrConjuncts,Summary).

time_out_and_catch_errors(Call,TimeOut,Result) :-
    catch(
    safe_time_out(catch_clpfd_overflow_call1(call_residue_check(Call)),TimeOut,Result),
    enumeration_warning(_,_,_,_,_),
    (print('Treating enumeration warning as TIMEOUT !'),nl,
    Result=time_out)).

translate_conj_status(Conjunct,Status,EnumWarning,Translation) :-
    translate_bexpression_with_limit(Conjunct,500,TC),
    (EnumWarning=true ->
    ajoin([TC,'\n == ',Status,' (#### infinite set expanded ####)\n\n'],Translation)
    ; ajoin([TC,'\n == ',Status,'\n\n'],Translation)).

translate_conjunct([],_Status,_EnumWarning,'EmptyInvariant') :- !.

translate_conjunct(Conjunct,Status,EnumWarning,Translation) :-
    translate_conj_status(Conjunct,Status,EnumWarning,Translation).

unknown_summary(Nr,[total/Nr,unknown/Nr,unknown_after_expansion/Nr]).

update([],K,V,[K/V]).

update([K1/V1|T],K1,V2,[K1/NV|T]) :- !,NV is V1+V2.

update([K1/V1|T],K,V,[K1/V1|NT]) :- update(T,K,V,NT).