1		% (c) 2009-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(predicate_evaluator,[tcltk_analyse_goal/1, tcltk_analyse_goal/2,
6		tcltk_analyse_invariant/2,
7		tcltk_analyse_assertions/2, tcltk_analyse_assertions/3,
8		tcltk_analyse_properties/2, check_summary_all_true/1,
9		tcltk_analyse_deadlock/2,
10		%get_analyse_error_span_linecol/4,
11
12		% a way to customize what is done with false/unknown conjuncts
13		reset_conjunct_error_hook/0, register_conjunct_error_hook/1,
14		register_conjunct_register_error_span/0 % conjuncts which are not true are registered as error spans
15		]).
16
17		% a simple textual analysis of the conjuncts of a predicate
18
19		:- meta_predicate register_conjunct_error_hook(5).
20		:- meta_predicate analyse_quick_time_out(0).
21		:- meta_predicate call_residue_check(0).
22		:- meta_predicate time_out_and_catch_errors(0,*,*).
23
24		:- use_module(tools).
25
26		:- use_module(module_information,[module_info/2]).
27		:- module_info(group,misc).
28		:- module_info(description,'Various tools to analyse conjunctions of predicates textually (along with statistics).').
29
30		:- use_module(bmachine).
31		:- use_module(error_manager).
32		:- use_module(translate).
33		:- use_module(debug).
34		:- use_module(preferences,[get_computed_preference/2,get_preference/2,get_time_out_preference_with_factor/2]).
35		:- use_module(state_space,[current_state_corresponds_to_setup_constants_b_machine/0,
36		current_state_corresponds_to_fully_setup_b_machine/0]).
37
38
39
40		current_b_state_with_all_constants_valued :-
41		(current_state_corresponds_to_setup_constants_b_machine -> true
42		; \+ b_machine_has_constants). % also allow analysis if we have no constants (but possibly properties)
43
44		tcltk_analyse_goal(List) :- tcltk_analyse_goal(List,_).
45		tcltk_analyse_goal(list(List),Summary) :-
46		current_b_state_with_all_constants_valued,
47		b_get_machine_goal(Goal),!,
48		b_analyse_boolean_expression(Goal,'GOAL',false,List,Summary).
49		tcltk_analyse_goal(list(['Cannot evaluate GOAL yet.\nSetup constants first.\n\n'|List]),Summary) :-
50		b_get_machine_goal(Goal),!,
51		get_conjuncts(Goal,List,undefined), unknown_summary(1,Summary).
52		tcltk_analyse_goal(list(['Cannot find GOAL DEFINITION (must be a predicate).\n']),Summary) :-
53		unknown_summary(1,Summary).
54
55		tcltk_analyse_invariant(list(List),Summary) :-
56		current_state_corresponds_to_fully_setup_b_machine,!,
57		b_get_invariant_from_machine(Invariant),
58		get_preference(partition_predicates,Partition),
59		b_analyse_boolean_expression(Invariant,'INVARIANT',Partition,List,Summary).
60		tcltk_analyse_invariant(list(['Cannot evaluate invariant yet.\nInitialise machine first.\n\n'|List]),Summary) :-
61		b_get_invariant_from_machine(Invariant),
62		get_conjuncts(Invariant,List,undefined),
63		length(List,TL), unknown_summary(TL,Summary).
64
65		:- use_module(specfile,[animation_mode/1, csp_with_bz_mode/0]).
66		tcltk_analyse_assertions(List,Summary) :- tcltk_analyse_assertions(all,List,Summary).
67		tcltk_analyse_assertions(_ALL,list(['CSP Assertions'|CA]),TSummary) :-
68		(animation_mode(cspm) ; csp_with_bz_mode),!,
69		statistics(walltime,[CurTime,_]), /* get current time in ms */
70		tcltk_interface:tcltk_check_csp_assertions(CA,Summary),
71		statistics(walltime,[CurTime2,_]), /* get current time in ms */
72		Delta is CurTime2-CurTime,
73		TSummary = [runtime/Delta|Summary],
74		format('% CSP Assertion Checks Completed: ~w~n',[CA]).
75		tcltk_analyse_assertions(all,list(['This Machine has no ASSERTIONS.']),Summ) :-
76		b_get_dynamic_assertions_from_machine([]),b_get_static_assertions_from_machine([]),!,empty_summary(Summ).
77		tcltk_analyse_assertions(main,list(['The Main Machine has no ASSERTIONS.']),Summ) :-
78		b_main_machine_has_no_assertions,
79		!,empty_summary(Summ).
80		tcltk_analyse_assertions(ALL,list(List),Summary) :-
81		current_state_corresponds_to_fully_setup_b_machine,!,
82		%conjunct_predicates(Ass,BExpr)
83	?	b_get_assertions(ALL,static,SAss),
84		println_silent('Checking Static Assertions'),
85		% translate:nested_print_bexpr(SAss),
86		b_analyse_boolean_expression(SAss,'ASSERTIONS (static)',false,SList,SSummary),
87		b_get_assertions(ALL,dynamic,DAss),
88		println_silent('Checking Dynamic Assertions'),
89		b_analyse_boolean_expression(DAss,'ASSERTIONS (dynamic)',false,DList,DSummary),
90		combine_summary(SSummary,DSummary,Summary),
91	?	combine_static_dynamic_result(SList,DList,List).
92		tcltk_analyse_assertions(ALL,list(ListRes),Summary) :-
93		current_b_state_with_all_constants_valued,
94	?	b_get_assertions(ALL,static,Ass),Ass\=[],!,
95		b_analyse_boolean_expression(Ass,'ASSERTIONS',false,SList,SSummary),
96		b_get_assertions(ALL,dynamic,DynAss),
97		(DynAss=[] -> ListRes = List, Summary = SSummary
98		; ListRes = ['Only evaluating STATIC ASSERTIONS.\nInitialise machine to evaluate other ASSERTIONS.\n\n'|List],
99		(length(DynAss,Len) -> true ; Len=1),
100		unknown_summary(Len,US),combine_summary(US,SSummary,Summary)
101		),
102		get_assertions_as_undefined(ALL,dynamic,DList),
103	?	combine_static_dynamic_result(SList,DList,List).
104		tcltk_analyse_assertions(ALL,list(['Cannot evaluate assertions yet.\nInitialise machine first.\n\n'|List]),Summary) :-
105		print('*** Cannot evaluate ASSERTIONS\nSPECIFICATION not initialised.'),nl,
106		get_assertions_as_undefined(ALL,static,SList),
107		get_assertions_as_undefined(ALL,dynamic,DList),
108		length(SList,SL), length(DList,DL), TL is SL+DL, unknown_summary(TL,Summary),
109		combine_static_dynamic_result(SList,DList,List).
110
111		:- use_module(library(lists),[maplist/3]).
112		get_assertions_as_undefined(ALL,SD,List) :-
113		b_get_assertions(ALL,SD,Ass),
114		flatten_conjunction(Ass,FAss,[]),
115		maplist(get_as_undefined,FAss,List).
116		% (Ass=[] -> List=[] ; conjunct_predicates(Ass,BExpr),get_conjuncts(BExpr,List,undefined)).
117
118		get_as_undefined(Conjunct,Translation) :- translate_conj_status(Conjunct,undefined,false,Translation).
119
120		combine_static_dynamic_result([],L,L).
121		combine_static_dynamic_result(L,[],L).
122		combine_static_dynamic_result(S,D,List) :-
123		List = ['STATIC ASSERTIONS:\n'|List0],
124		append(S,['DYNAMIC ASSERTIONS:\n'|D],List0).
125
126		unknown_summary(Nr,[total/Nr,unknown/Nr,unknown_after_expansion/Nr]).
127		combine_summary([],S,S).
128		combine_summary([K/V|T],S,R) :- update(S,K,V,S2), combine_summary(T,S2,R).
129		update([],K,V,[K/V]).
130		update([K1/V1|T],K1,V2,[K1/NV|T]) :- !,NV is V1+V2.
131		update([K1/V1|T],K,V,[K1/V1|NT]) :- update(T,K,V,NT).
132
133		:- use_module(b_state_model_check,[get_unsorted_all_guards_false_pred/1]).
134		tcltk_analyse_deadlock(list(List),Summary) :- current_state_corresponds_to_fully_setup_b_machine,!,
135		get_unsorted_all_guards_false_pred(BExpr),
136		b_analyse_boolean_expression(BExpr,'DEADLOCK (guard disjunction)',false,List,Summary).
137		tcltk_analyse_deadlock(list(['Cannot evaluate deadlock yet.\nInitialise machine first.\n\n'|List]),[]) :-
138		get_unsorted_all_guards_false_pred(BExpr),
139		get_conjuncts(BExpr,List,undefined).
140
141		tcltk_analyse_properties(list([Res]),[]) :-
142		b_get_properties_from_machine(b(truth,_,_)),!,
143		(b_machine_has_constants
144		-> Res = 'This Machine has only typing information in the PROPERTIES.'
145		; Res = 'This Machine has no PROPERTIES clause.'
146		).
147		tcltk_analyse_properties(list(List),Summary) :-
148		current_b_state_with_all_constants_valued,
149		!,
150		b_get_properties_from_machine(Prop),
151		get_preference(partition_predicates,Partition),
152	?	b_analyse_boolean_expression(Prop,'PROPERTIES',Partition,List,Summary).
153		tcltk_analyse_properties(list(['Cannot evaluate properties yet.\nSet up constants first.\n\n'|List]),Summary) :-
154		b_get_properties_from_machine(Prop),
155		(get_preference(partition_predicates,false)
156		-> get_conjuncts(Prop,List,undefined), length(List,NrConjuncts)
157		; bsyntaxtree:predicate_components(Prop,Components),
158		findall(CList,
159		(member(component(CP,_CompVars),Components),
160		get_conjuncts(CP,CList,undefined)), CCList),
161		flatten_comp(CCList,List,NrConjuncts)
162		),
163		unknown_summary(NrConjuncts,Summary).
164
165		flatten_comp([],[],0).
166		flatten_comp([H|T],['COMPONENT:\n'|Res],NrConjuncts) :-
167		flatten_comp(T,TR,TNr),
168		length(H,LH), NrConjuncts is LH+TNr,
169		append(H,TR,Res).
170
171
172		%:- dynamic conj_nr/1.
173		%conj_nr(1).
174		%get_and_inc_conj_nr(X) :- retract(conj_nr(X)), X1 is X+1, assertz(conj_nr(X1)).
175		%reset_conj_nr :- retractall(conj_nr(_)), assertz(conj_nr(1)).
176
177
178		% check if a summary report is all true
179		check_summary_all_true(L) :-
180	?	member(total_after_expansion/Nr,L), member(true_after_expansion/Nr,L),
181	?	member(false/0,L), member(unknown/0,L), member(timeout/0,L).
182
183		empty_summary([total/0, total_after_expansion/0,
184		true/0, true_after_expansion/0, false/0, false_after_expansion/0,
185		unknown/0, unknown_after_expansion/0, timeout/0, runtime/0, enum_warning/0]).
186		:- use_module(specfile, [current_b_expression/1]).
187		:- use_module(state_space, [current_state_id/1]).
188		get_current_b_expression(S) :-
189		(current_b_expression(S) -> true
190		; current_state_id(root), \+ b_machine_has_constants -> S = []
191		; add_internal_error('Could not get B state for analysis',get_current_b_expression(S)),S=[]
192		).
193		b_analyse_boolean_expression(VAR,Kind,P,L,S) :- var(VAR),!,
194		add_internal_error('Illegal call: ',b_analyse_boolean_expression(VAR,Kind,P,L,S)),
195		S=[unknown/1].
196		b_analyse_boolean_expression(BExpr,Kind,Partition,List,
197		[total/NrTotal, total_after_expansion/NrTotalExpanded,
198		true/NrTrue, true_after_expansion/NrTrueExpanded,
199		false/NrFalse, false_after_expansion/NrFalseExpanded,
200		unknown/NrUnknown, unknown_after_expansion/NrUnknownExpanded,
201		timeout/NrTimeout, runtime/TotalTime, enum_warning/NrEnumWarning]) :-
202		get_current_b_expression(RealCurState),
203		%reset_conj_nr,
204		statistics(walltime,[CurTime,_]), /* get current time in ms */
205		b_analyze_all_sub_conjuncts(Kind,Partition,BExpr, RealCurState, CList),
206		statistics(walltime,[CurTime2,_]), /* get current time in ms */
207		formatsilent('~N=======~NSUMMARY (~w)~N=======~N',[Kind]),
208		new_counter(Counter0),
209	?	l_translate_conjunct_analysis_result(CList,List,none/true,'$_no_model'(none),Counter0,ResCounter),
210		%print_counter(ResCounter),
211		get_counter(total,ResCounter,NrTotal), get_counter(total_after_expansion,ResCounter,NrTotalExpanded),
212		get_counter(true,ResCounter,NrTrue), get_counter(true_after_expansion,ResCounter,NrTrueExpanded),
213		get_counter(false,ResCounter,NrFalse), get_counter(false_after_expansion,ResCounter,NrFalseExpanded),
214		get_counter(unknown,ResCounter,NrUnknown), get_counter(unknown_after_expansion,ResCounter,NrUnknownExpanded),
215		get_counter(timeout,ResCounter,NrTimeout), get_counter(enum_warning,ResCounter,NrEnumWarning),
216		(silent_mode(on),NrFalse==0,NrUnknown==0 -> true
217		; NrTotal=NrTotalExpanded
218		-> format('~p predicates: ~p TRUE, ~p FALSE, ~p UNKNOWN (~p timeouts)~N',[NrTotal,NrTrue,NrFalse,NrUnknown,NrTimeout])
219		; 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])),
220		TotalTime is CurTime2-CurTime,
221		formatsilent('~w ms to analyse ~w~n',[TotalTime,Kind]).
222
223		:- use_module(bsyntaxtree).
224
225		b_analyze_all_sub_conjuncts(Kind,true,BExpr, RealCurState, CList) :- !,
226		bsyntaxtree:predicate_components(BExpr,Components), % Note: does not support list of conjunctions (as generated by b_get_assertions_from_machine)
227		findall(comp_res(CCList,CompVars),
228		(member(component(CompBExpr,CompVars),Components),
229		analyze_all_conjuncts2(Kind,CompBExpr, RealCurState, CCList)),CompRes),
230		flatten_comp_res(CompRes,CList).
231		b_analyze_all_sub_conjuncts(Kind,_Partition,BExpr, RealCurState, CList) :-
232		analyze_all_conjuncts2(Kind,BExpr, RealCurState, CList).
233
234		flatten_comp_res([],[]).
235		flatten_comp_res([comp_res(CCList,Vars)|T],Res) :-
236		flatten_comp_res(T,FT),
237		append([vars(Vars)|CCList],FT,Res).
238
239		analyze_all_conjuncts2(Kind,BExpr, RealCurState, CList) :-
240		findall(conj(Nr,Conjunct,Status,EnumWarning,IsExpanded),
241		(%get_and_inc_conj_nr(Nr), print(analysing_conjunct(Nr)),nl,
242		b_analyse_conjunction(Kind,BExpr,[],RealCurState,Nr,Conjunct,Status,EnumWarning,IsExpanded)
243		),
244		CList).
245
246		%:- use_module(library(codesio)).
247		:- use_module(tools_meta,[translate_term_into_atom/2]).
248		l_translate_conjunct_analysis_result([],[],CurConjNr/CurStatus,_LastModel,Acc,ResAcc) :-
249		flush_cur_status(CurConjNr,CurStatus,Acc,ResAcc).
250		l_translate_conjunct_analysis_result([vars(Vars)|T],Res,CurConjNr/CurStatus,_LastModel,Acc,CRes) :-
251		flush_cur_status(CurConjNr,CurStatus,Acc,Acc1),
252		(Vars=[] -> Res = ['** ISOLATED CONJUNCT **\n'|TT]
253		; Res = [CS,CV,' **\n'|TT], CS = '** CONJUNCTS OVER IDENTIFIERS:'),
254		translate_term_into_atom(Vars,CV),
255	?	l_translate_conjunct_analysis_result(T,TT,none/true,'$_no_model'(none),Acc1,CRes).
256		l_translate_conjunct_analysis_result([conj(NextNr,Conjunct,Status,EnumWarning,IsExpanded)|T],TranslationResult,CurConjNr/CurStatus,LastModel,Acc,CRes) :-
257		translate_conjunct(Conjunct,Status,EnumWarning,CS),
258		inc_counter(total_after_expansion,Acc,AA),
259		(EnumWarning==true -> inc_counter(enum_warning,AA,A1) ; AA=A1),
260		( Status = 'TRUE' -> inc_counter(true_after_expansion,A1,NewAcc)
261		; Status = timeout_true -> inc_counter(true_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc)
262		; Status = false -> inc_counter(false_after_expansion,A1,NewAcc)
263		; Status = timeout_false -> inc_counter(false_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc)
264		; Status = both_true_false -> inc_counter(unknown_after_expansion,A1,NewAcc)
265		; Status = wd_error_true -> inc_counter(unknown_after_expansion,A1,NewAcc)
266		; Status = wd_error_false -> inc_counter(unknown_after_expansion,A1,NewAcc)
267		; inc_counter(unknown_after_expansion,A1,A2),inc_counter(timeout,A2,NewAcc)
268		),
269		(call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, CS) -> true
270		; add_internal_error('Conjunct error hook failed: ',
271		call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, CS))),
272		(CurConjNr==NextNr
273		-> combine_status(CurStatus,Status,NewStatus), NewAcc=NewAcc2 % still the same conjunct; combine status
274		; flush_cur_status(CurConjNr,CurStatus,NewAcc,NewAcc2),
275		convert_status(Status,NewStatus)),
276		((get_rodin_model_name(Conjunct,NewModel), NewModel \= LastModel)
277		-> TranslationResult = [' * MODEL: ',NewModel,'\n',CS|TT] % show from which model the conjuncts come from
278		; NewModel = LastModel, TranslationResult = [CS|TT]),
279	?	l_translate_conjunct_analysis_result(T,TT,NextNr/NewStatus,NewModel,NewAcc2,CRes).
280
281		flush_cur_status(CurConjNr,CurStatus,Acc,NewAcc2) :-
282		(CurConjNr==none -> Acc=NewAcc2
283		; inc_counter(total,Acc,NewAcc1),
284		(CurStatus = true -> inc_counter(true,NewAcc1,NewAcc2)
285		; CurStatus = false -> inc_counter(false,NewAcc1,NewAcc2)
286		; inc_counter(unknown,NewAcc1,NewAcc2)) ).
287
288		combine_status(true,X,R) :- convert_status(X,R).
289		combine_status(false,_,false).
290		combine_status(unknown,false,R) :- !,R=false.
291		combine_status(unknown,_,unknown).
292
293		convert_status('TRUE',true) :- !.
294		convert_status(timeout_true,true) :- !.
295		convert_status(false,false) :- !.
296		convert_status(timeout_false,false) :- !.
297		convert_status(_,unknown).
298
299		:- dynamic conjunct_error_hook_pred/1.
300		conjunct_error_hook_pred(default_hook).
301		call_conjunct_error_hook(Conjunct,Status,EnumWarning,IsExpanded, TranslatedConjunct) :-
302		convert_status(Status,ConvStatus),
303		conjunct_error_hook_pred(Pred),
304		call(Pred,Conjunct,ConvStatus,EnumWarning,IsExpanded, TranslatedConjunct).
305		:- public default_hook/5.
306		default_hook(_,_Status,_,_, _CS).
307		%((Status='TRUE' ; Status = timeout_true) -> print(CS),nl ; true).
308
309		:- use_module(error_manager,[register_error_span/2]).
310		register_span_hook(Conjunct,ConvStatus,_EnumWarning,_IsExpanded, _TranslatedConjunct) :-
311		%print(status(ConvStatus)),nl,
312		(ConvStatus=true -> true ; register_error_span(predicate_evaluator,Conjunct)). % store positions for Tcl/Tk
313
314		reset_conjunct_error_hook :- retractall(conjunct_error_hook_pred(_)), assertz(conjunct_error_hook_pred(default_hook)).
315
316		register_conjunct_error_hook(Pred) :- retractall(conjunct_error_hook_pred(_)), assertz(conjunct_error_hook_pred(Pred)).
317
318		register_conjunct_register_error_span :- register_conjunct_error_hook(register_span_hook).
319
320
321		% some utilities to count occurences of certain things:
322		:- use_module(library(assoc)).
323		new_counter(C) :- empty_assoc(C).
324		%reset_counter(Key,C,NC) :- put_assoc(Key,C,0,NC).
325		inc_counter(Key,C,NC) :- (get_assoc(Key,C,Val) -> NewVal is Val+1 ; NewVal =1),
326		put_assoc(Key,C,NewVal,NC).
327		%cond_inc_counter(true,Key,C,NC) :- !, inc_counter(Key,C,NC).
328		%cond_inc_counter(_,_,C,C).
329		get_counter(Key,C,Val) :- (get_assoc(Key,C,Val) -> true ; Val =0).
330		%print_counter(C) :- portray_assoc(C),nl.
331		%get_counter_list(C,L) :- assoc_to_list(C,L).
332
333		:- use_module(b_interpreter).
334		:- use_module(bsyntaxtree,[is_a_conjunct/3]).
335
336		% conjunct_
337		%b_analyse_conjunction(C, LocalState,State,Conjunct,Status,EnumWarning) :- tools_printing:print_term_summary(C),nl,fail.
338
339		:- use_module(library(lists),[nth1/3]).
340		b_analyse_conjunction(Kind,Conj, LocalState,State,Nr,EvConjunct,Status,EnumWarning,IsExpanded) :-
341		flatten_conjunction(Conj,ConjList,[]),
342	?	nth1(Nr, ConjList, Conjunct),
343	?	b_analyse_conjunction_nr(Kind,Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded).
344
345		flatten_conjunction([]) --> !, [].
346		flatten_conjunction([H|T]) --> !, flatten_conjunction(H),flatten_conjunction(T).
347		flatten_conjunction(C) --> {is_a_conjunct(C,LHS,RHS)},
348	?	{\+ do_not_decompose(C)}, % otherwise the user wants to group it
349		!,
350		flatten_conjunction(LHS), flatten_conjunction(RHS).
351		flatten_conjunction(C) --> [C].
352
353		% maybe provide option to always decompose for precision/performance/forall expansion
354	?	do_not_decompose(C) :- bsyntaxtree:get_texpr_labels(C,_),!. % otherwise the user wants to group it
355		do_not_decompose(C) :- get_texpr_info(C,Infos),
356	?	member(generated_conjunct,Infos). % the conjunct has been generated, e.g., by b_ast_cleanup
357
358		:- use_module(tools_meta,[safe_time_out/3]).
359		analyse_quick_time_out(Call) :-
360		get_time_out_preference_with_factor(0.05,DTimeOut),
361		(DTimeOut > 400 -> TO = 400 ; TO = DTimeOut),
362	?	on_enumeration_warning(
363		safe_time_out(Call,TO,Res),
364		fail), % in case of enumeration warnings: we could not compute all elements of domain
365		\+ is_time_out_result(Res).
366		%analyse_time_out(Call) :-
367		% preferences:get_computed_preference(debug_time_out,DTimeOut),
368		% time_out_with_enum_warning_one_solution(Call,DTimeOut,Res),
369		% \+ is_time_out_result(Res).
370
371
372		:- use_module(b_interpreter,[b_generate_for_all_list_domain_nolwf/8]).
373		:- use_module(kernel_waitflags,[ground_wait_flags/1,init_wait_flags/2]).
374
375		b_analyse_conjunction_nr(Kind,Nr,b(forall(Parameters,LHS,RHS),pred,Info),LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded) :-
376		IsExpanded=true,
377		get_preference(expand_forall_upto,MaxLenForEpxansion),
378		MaxLenForEpxansion>0,
379		% print(generating_for_all_domain(Parameters)),nl,
380	?	analyse_quick_time_out((
381		kernel_waitflags:init_wait_flags_with_call_stack(WF,[prob_command_context(analyse_quick_time_out,Info)]),
382		b_interpreter:b_generate_for_all_list_domain_nolwf(Parameters,LHS,RHS,LocalState,State,AllSols,NewRHS,WF),
383		kernel_waitflags:ground_wait_flags(WF))),
384		length(AllSols,Len), Len>0, Len=<MaxLenForEpxansion,!,
385		(silent_mode(on) -> true ; print('FORALL domain computed: '), translate:print_bexpr(LHS),nl),
386	?	member(ParResult,AllSols),
387		set_up_equality(Parameters,ParResult,EqList),
388		conjunct_predicates(EqList,EqPred),
389		EvConjunct = b(forall(Parameters,EqPred,RHS),pred,Info),
390		(debug_mode(on) -> print('Testing: '), print_bexpr(EvConjunct),nl ; true),
391		set_up_typed_localstate(Parameters,ParResult,_,LocalState,NewLocalState,positive),
392		b_analyse_individual_conjunct(Kind,Nr,NewRHS,NewLocalState,State,_,Status,EnumWarning).
393		b_analyse_conjunction_nr(Kind,Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning,IsExpanded) :-
394		%debug:debug_println(9,analysing_conjunct_in_component(Nr)),
395		IsExpanded=false,
396		b_analyse_individual_conjunct(Kind,Nr,Conjunct,LocalState,State,EvConjunct,Status,EnumWarning).
397
398		set_up_equality([],[],[]).
399		set_up_equality([Identifier|IR],[Val|VR],[b(equal(Identifier,b(value(Val),IDType,[])),pred,[])|TE]) :-
400		get_texpr_type(Identifier,IDType),
401		set_up_equality(IR,VR,TE).
402
403
404
405		:- use_module(tools_printing,[print_goal/1]).
406		:- use_module(tools_meta,[safe_time_out/3,call_residue/2]).
407
408		call_residue_check(Call) :-
409	?	call_residue(Call,Residue),
410		(Residue = [] -> true
411		; add_internal_error('Call had residue: ',residue(Residue)/call(Call)),
412		print_goal(Residue),nl
413		).
414
415		:- use_module(clpfd_interface,[catch_clpfd_overflow_call1/1]).
416		% very similar to time_out_with_enum_warning, adds catch_clpfd_overflow_call1
417		time_out_and_catch_errors(Call,TimeOut,Result) :-
418	?	catch(
419		safe_time_out(catch_clpfd_overflow_call1(call_residue_check(Call)),TimeOut,Result),
420		enumeration_warning(_,_,_,_,_),
421		(print('Treating enumeration warning as TIMEOUT !'),nl,
422		Result=time_out)).
423
424		:- use_module(tools_printing,[print_red/1, print_green/1]).
425		b_analyse_individual_conjunct(Kind,Nr,Conjunct,LocalState,State,Conjunct,Status,EnumWarning) :-
426
427		get_computed_preference(debug_time_out,DTimeOut),
428
429		(silent_mode(on) -> true
430		; nl,print('==> '),translate:print_bexpr(Conjunct),nl),
431		%translate:print_bexpr_with_limit(Conjunct,250),nl,
432		statistics(walltime,[T1,_]),
433		enter_new_error_scope(ScopeID,b_analyse_individual_conjunct),
434	?	(time_out_and_catch_errors(b_test_boolean_expression_cs(Conjunct,LocalState,State,Kind,Nr),
435		DTimeOut,TimeOutRes) ->
436		/* PREDICATE TRUE */
437		statistics(walltime,[T2,_]),check_enum_warning(positive,EnumWarning),
438		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 !!
439		(TimeOutRes=time_out
440		-> print_red('TIMEOUT'),nl,Status=timeout
441		; ErrOcc=true -> (get_preference(strict_raise_warnings,true) -> print('POSSIBLY ') ; true),
442		print_red('NOT-WELL-DEFINED (TRUE)'),nl, Status = wd_error_true
443		; print_true,
444		enter_new_error_scope(NegScopeID,b_analyse_double_evaluation_true),
445		((get_preference(double_evaluation_when_analysing,true),
446		time_out_and_catch_errors(b_not_test_boolean_expression_cs(Conjunct,LocalState,State,Kind,Nr),
447		DTimeOut,TimeOutRes2))
448		-> (TimeOutRes2==time_out -> Status = timeout_true
449		; Status = both_true_false,
450		add_error(predicate_evaluator,'Conjunct is both true and false: ',Conjunct,Conjunct)
451		)
452		; Status = 'TRUE' ),
453		check_enum_warning(_,_NegEnumWarning),
454		exit_error_scope(NegScopeID,_NegTErrorOccurred,b_analyse_double_evaluation_true) % Should we also report those errors ? + NegEnumWarning ?
455		)
456		; /* PREDICATE FALSE */
457		statistics(walltime,[T2,_]), check_enum_warning(negative,EnumWarning),
458		exit_error_scope(ScopeID,ErrOcc,b_analyse_individual_conjunct_false),
459		(ErrOcc=true
460		-> print_red('NOT-WELL-DEFINED (FALSE)'),nl, Status = wd_error_false
461		; (EnumWarning=true -> print_red('UNKNOWN'),nl
462		; print_false),
463		enter_new_error_scope(NegScopeID,b_analyse_double_evaluation_false),
464		((get_preference(double_evaluation_when_analysing,false) ;
465	?	time_out_and_catch_errors(
466		b_not_test_boolean_expression_cs(Conjunct,LocalState,State,Kind,Nr),
467		DTimeOut,TimeOutRes2))
468		-> (TimeOutRes2==time_out -> Status = timeout_false ; Status = false)
469		; Status = unknown),
470		exit_error_scope(NegScopeID,_NegFErrorOccurred,b_analyse_double_evaluation_false) % Should we also report those errors ? + NegEnumWarning ?
471		)
472		),
473		statistics(walltime,[T3,_]),
474		Time1 is T2-T1, Time2 is T3-T2, Time is T3-T1,
475		(silent_mode(on) -> true
476		; format('~w (~w ms + ~w ms = ~w ms)',[Status,Time1,Time2,Time]),
477		(Status = 'TRUE' -> true
478		; translate:translate_span(Conjunct,SpanS), SpanS \= '' -> print(' '),print(SpanS)
479		; true),nl
480		).
481
482		print_true :- silent_mode(on),!.
483		print_true :- print_green('TRUE'),nl.
484		print_false :- silent_mode(on),!.
485		print_false :- print_red('FALSE'),nl.
486
487
488		check_enum_warning(positive,EnumWarning) :- !,
489		(enumeration_warning_occured_in_error_scope
490		-> print('### Enumeration warnings not critical (solution found)'),nl %, error_manager:trace_if_user_wants_it %%
491		; true), EnumWarning = false.
492		check_enum_warning(_,EnumWarning) :-
493		\+ critical_enumeration_warning_occured_in_error_scope,!,
494		EnumWarning = false.
495		check_enum_warning(_,EnumWarning) :-
496		(event_occurred_in_error_scope(enumeration_warning(enumerating(_),_,_,_,_))
497		-> print('### Warning: infinite types were enumerated'),nl, E1=true
498		; true),
499		(event_occurred_in_error_scope(enumeration_warning(checking_finite_closure,_,_,_,_))
500		-> print('### Warning: finiteness of comprehension sets could not be determined'),nl, E2=true
501		; true),
502		(var(E1),var(E2)
503		-> print('### Unknown enumeration warning occurred !')
504		; true),
505		EnumWarning = true.
506
507		translate_conjunct([],_Status,_EnumWarning,'EmptyInvariant') :- !.
508		/* translate_conjunct(Conjunct,true,true) :- !. */ /* do not show true conjuncts */
509		translate_conjunct(Conjunct,Status,EnumWarning,Translation) :-
510		translate_conj_status(Conjunct,Status,EnumWarning,Translation).
511
512
513		get_conjuncts(BoolExpr,Conjuncts,Status) :- findall(C,get_conjunct(BoolExpr,C,Status),Conjuncts).
514		get_conjunct(C,Conjunct,Status) :- is_a_conjunct(C,LHS,RHS),!,
515		(get_conjuncts(LHS,Conjunct,Status) ; get_conjuncts(RHS,Conjunct,Status)).
516		get_conjunct(Conjunct,Translation,Status) :-
517		translate_conj_status(Conjunct,Status,false,Translation).
518
519		translate_conj_status(Conjunct,Status,EnumWarning,Translation) :-
520		translate_bexpression_with_limit(Conjunct,500,TC),
521		(EnumWarning=true ->
522		ajoin([TC,'\n == ',Status,' (#### infinite set expanded ####)\n\n'],Translation)
523		; ajoin([TC,'\n == ',Status,'\n\n'],Translation)).
524