1		% (c) 2020-2026 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(well_def_analyser, [analyse_wd_for_machine/3, analyse_wd_for_machine/4,
6		compute_wd/4, compute_all_wd_pos/4,
7		analyse_wd_for_expr/3, analyse_wd_for_expr/4,
8		annotate_wd/2, transform_wd/4,
9		tcltk_get_machine_wd_pos/4,
10		get_hyps_for_top_level_operations/2,
11		prove_sequent/1,
12		prove_sequent/3,
13		prove_sequent/4,
14		analyse_invariants_for_machine/5,
15		find_inconsistent_axiom/3, tcltk_check_for_inconsistent_axiom/1,
16		toplevel_wd_pos/3
17		]).
18
19		:- use_module(probsrc(module_information),[module_info/2]).
20		:- module_info(group,well_def_prover).
21		:- module_info(description,'This module computes WD conditions in AST.').
22
23		:- use_module(probsrc(error_manager)).
24		:- use_module(probsrc(debug)).
25		:- use_module(probsrc(bsyntaxtree)).
26		:- use_module(probsrc(b_ast_cleanup), [has_top_level_wd_condition/1]).
27		:- use_module(probsrc(external_functions),[external_fun_has_wd_condition/1]).
28		:- use_module(probsrc(specfile),[z_or_tla_minor_mode/0, eventb_mode/0]).
29
30		:- use_module(library(ordsets)).
31		:- use_module(library(avl)).
32		:- use_module(wdsrc(well_def_hyps)).
33
34
35		prove_sequent(Goal) :-
36		prove_sequent(proving,Goal,[]).
37		prove_sequent(Context,Goal,Hyps) :-
38		prove_sequent(Context,Goal,Hyps,[push_more_hyps]). % push all hypotheses;
39		% push_more_hyps usually not useful for WD proofs but useful if proof goals have other form than for WD POs
40		prove_sequent(Context,Goal,Hyps,Opts) :-
41		(Context=animation -> Val=true
42		; Context=proving -> Val=false
43		; add_internal_error('Unknown context:',Context),
44		Val=false),
45
46		temporary_set_preference(wd_analysis_for_animation,Val,Chng),
47		call_cleanup(prove_sequent_cur_context(Goal,Hyps,Opts),
48		reset_temporary_preference(wd_analysis_for_animation,Chng)).
49
50
51
52		% utility for disprover
53		prove_sequent_cur_context(_,Hyps,_) :-
54	?	member(Falsity,Hyps), is_falsity(Falsity),!. % TO DO: upon pushing hyps
55		prove_sequent_cur_context(Falsity,Hypotheses,Opts) :-
56		is_falsity(Falsity), % we do not have a good way of detecting inconsistencies in the hyps yet
57		append(NewHyps,[LastHyp],Hypotheses),!,
58		negate_hyp(LastHyp,NewGoal), % pick last hypothesis and try and prove its negation as goal
59		prove_sequent_cur_context(NewGoal,NewHyps,Opts).
60		prove_sequent_cur_context(Goal,Hypotheses,Opts) :-
61		init_hyps_for_goal(Goal,E), % TODO: should we consider also adding typed variables of the Hypotheses?
62		list_to_ord_set([discharge_po|Opts],Options),
63		push_hyps(E,Hypotheses,Options,Hyps),
64		prove_sequent_goal(Goal,Hyps,Options).
65
66		:- use_module(probsrc(bsyntaxtree), [find_typed_identifier_uses/2]).
67		init_hyps_for_goal(Goal,InitialHyps) :-
68		empty_hyps(E),
69		find_typed_identifier_uses(Goal,Identifiers),
70		add_new_hyp_variables(E,Identifiers,InitialHyps).
71
72
73		% process complex sequent goals which arise in Rodin; not generated by our POG
74		prove_sequent_goal(b(Formula,pred,I),Hyps,Options) :- !,
75		process_sequent_aux(Formula,I,Hyps,Options).
76		prove_sequent_goal(Goal,Hyps,Options) :- Goal = b(_,_,_), !,
77		add_internal_error('Goal to prove not a predicate: ',prove_sequent_goal(Goal,Hyps,Options)),fail.
78		prove_sequent_goal(Goal,Hyps,Options) :-
79		add_internal_error('Goal to prove not wrapped: ',prove_sequent_goal(Goal,Hyps,Options)),fail.
80
81	?	process_sequent_aux(negation(b(Pred,pred,_)),I,Hyps,Options) :- cnf_negate(Pred,NegPred),!,
82		(debug_level_inactive_for(19) -> true
83		; print('Pushing negation in sequent goal: '), translate:print_bexpr(b(NegPred,pred,[])),nl),
84		% example :prove x=3 => not( x=3 => x=2)
85		process_sequent_aux(NegPred,I,Hyps,Options).
86		process_sequent_aux(implication(A,B),_,Hyps,Options) :- !,
87		(debug_level_inactive_for(19) -> true ; print('Peeling implication in sequent goal: '), translate:print_bexpr(A),nl),
88		push_hyp(Hyps,A,Options,Hyps1),
89		(prove_sequent_goal(B,Hyps1,Options) -> true
90		; negate_hyp(A,NegA),
91		negate_hyp(B,NegB), push_hyp(Hyps,NegB,Options,Hyps2), % try not(B) => not(A)
92		debug_println(19,trying_to_prove_contrapositive),
93		prove_sequent_goal(NegA,Hyps2,Options)
94		).
95		process_sequent_aux(equivalence(A,B),I,Hyps,Options) :- !,
96		process_sequent_aux(implication(A,B),I,Hyps,Options),
97		process_sequent_aux(implication(B,A),I,Hyps,Options).
98		process_sequent_aux(if_predicate(Test,A,B),I,Hyps,Options) :- !,
99		process_sequent_aux(implication(Test,A),I,Hyps,Options),
100		negate_hyp(Test,NegTest),
101		process_sequent_aux(implication(NegTest,B),I,Hyps,Options).
102		process_sequent_aux(conjunct(A,B),_I,Hyps,Options) :- !,
103		prove_sequent_goal(A,Hyps,Options),
104		prove_sequent_goal(B,Hyps,Options).
105		process_sequent_aux(disjunct(A,B),_I,Hyps,Options) :- !,
106		(negate_hyp(B,NegB),
107		push_hyp(Hyps,NegB,Options,Hyps2), % not(B) => A we have A or B ; OR_R rule from Abrial Event-B Chapter 9.2.2
108		% is a combination of OR_R proof rule and proof by case B, not(B)
109		prove_sequent_goal(A,Hyps2,Options)
110		-> true
111		; % not sure if it will really be often successful to try this branch if the first one failed
112		negate_hyp(A,NegA),
113		push_hyp(Hyps,NegA,Options,Hyps2), % not(A) => B we have A or B
114		prove_sequent_goal(B,Hyps2,Options)).
115		process_sequent_aux(forall(Ids,A,B),I,Hyps,Options) :- !,
116		(debug_level_inactive_for(19) -> true ; print('Peeling forall in sequent goal: '), translate:print_bexpr(A),nl),
117		add_new_hyp_variables(Hyps,Ids,Hyps1),
118		prove_sequent_goal(b(implication(A,B),pred,I),Hyps1,Options).
119		process_sequent_aux(Goal,I,Hyps,Options) :-
120		get_normalized_and_renamed_predicate(b(Goal,pred,I),Hyps,_RenTarget,NT),
121		% print('PROVING: '),translate:print_bexpr(_RenTarget),nl,
122		(get_current_po_label(POLabel,Options) -> true ; POLabel = ''),
123		prove_proof_obligation(POLabel,Goal,NT,Hyps,ProofTree),
124		debug_format(19,'WD PROVER SUCCESSFUL: ~w~n',[ProofTree]).
125
126		:- use_module(probsrc(bsyntaxtree),[create_negation/2]).
127		cnf_negate(implication(A,B),conjunct(A,NotB)) :- create_negation(B,NotB).
128		cnf_negate(equivalence(A,B),conjunct(b(implication(A,NotB),pred,[]),
129		b(implication(NotA,B),pred,[]))) :-
130		% not( A <=> B ) <----> A=> not(B) & not(A) => B
131		create_negation(A,NotA),
132		create_negation(B,NotB).
133		cnf_negate(disjunct(A,B),conjunct(NotA,NotB)) :- create_negation(A,NotA), create_negation(B,NotB).
134		cnf_negate(conjunct(A,B),disjunct(NotA,NotB)) :- create_negation(A,NotA), create_negation(B,NotB).
135		cnf_negate(if_predicate(A,B,C),Res) :- create_negation(A,NA),
136		cnf_negate(conjunct(implication(A,B),implication(NA,C)),Res).
137		cnf_negate(NegA,A) :- negate_op(NegA,A). % deals with negation(A) -> A, truth->falsity, ...
138		%cnf_negate(exists(Ids,Q),forall(Ids,LHS,RHS)) :- ... TODO
139
140		compute_all_wd_pos(TExpr,OriginalHyps,Options,POs) :-
141		findall(PO, compute_wd(TExpr,OriginalHyps,Options,PO), POs).
142
143
144		% analyze and print WD POs for a given typed expression or predicate or subst:
145		analyse_wd_for_expr(TExpr,ResStr,AllDischarged) :-
146		analyse_wd_for_expr(TExpr,ResStr,AllDischarged,silent).
147
148		% MsgLevel = silent, message, warning, error
149		analyse_wd_for_expr(TExpr,_,_,MsgLevel) :-
150		reset_stats,
151		(silent_wd_mode(MsgLevel) -> true ; formatsilent('WD Proof Obligations:~n',[])),
152		%empty_hyps(OriginalHyps),
153		push_properties_invariant_hyps([],OriginalHyps),
154		list_to_ord_set([create_full_po,create_not_discharged_msg(MsgLevel),discharge_po,ignore_wd_infos
155		%,minimize_full_po
156		%,prove_with_z3 % comment in to double-check with Z3
157		],Options),
158	?	compute_wd(TExpr,OriginalHyps,Options,PO),
159		(silent_wd_mode(MsgLevel) -> true ; translate:nested_print_bexpr(PO),nl),
160		fail.
161		analyse_wd_for_expr(TExpr,ResStr,AllDischarged,MsgLevel) :-
162		(silent_wd_mode(MsgLevel) -> true
163		; formatsilent('----~n',[]),
164		print_stats
165		),
166		get_discharged_result(ResStr,_,_,AllDischarged),
167		empty_hyps(OriginalHyps),
168		transform_wd(TExpr,OriginalHyps,[discharge_po],NewTExpr),
169		(silent_wd_mode(MsgLevel) -> true
170		; format('Annotated formula:~n',[]),
171		nested_print_wd_bexpr(NewTExpr)
172		).
173
174		silent_wd_mode(MsgLevel) :- (MsgLevel=silent -> true ; silent_mode(on)).
175
176		nested_print_wd_bexpr(NewTExpr) :-
177		temporary_set_preference(pp_wd_infos,true,Chng),
178		translate:nested_print_bexpr(NewTExpr),nl,
179		reset_temporary_preference(pp_wd_infos,Chng).
180
181		:- use_module(probsrc(translate),[translate_bexpression_with_limit/3]).
182
183		tcltk_get_machine_wd_pos(only_goal,list([Header|POs]),ResStr,AllDischarged) :- !,
184		reset_stats,
185		Header = list(['PO Label','Discharged','Proof Obligation Goal', 'Source']),
186		list_to_ord_set([discharge_po,ignore_wd_infos,reorder_conjuncts],Options),
187		findall(list([POLabel,Discharged,POStr,Source]),
188		(get_machine_wd_po(Options,PO,PO_Name),
189		get_texpr_info(PO,Infos),
190		(member(discharged(D,POLabel),Infos)
191		-> (D=true -> Discharged='yes' ; Discharged='no')
192		; Discharged='UNKNOWN',POLabel=PO_Name),
193		translate:translate_bexpression_with_limit(PO,100,POStr),
194		get_tk_table_position_info(Infos,Source)
195		), POs),
196		get_discharged_result(ResStr,_,_,AllDischarged).
197		tcltk_get_machine_wd_pos(goal_and_hyps,list([Header|POs]),ResStr,AllDischarged) :-
198		reset_stats,
199		get_preference(translation_limit_for_table_commands,Limit),
200		Header = list(['PO Label','Discharged','PO Goal', '(Necessary) Hypotheses', 'Source']),
201		% in case a PO is proven we only show the hyps necessary for the proof
202		list_to_ord_set([discharge_po,ignore_wd_infos,reorder_conjuncts, create_full_po,minimize_full_po],Options),
203		findall(list([POLabel,Discharged,GoalStr,HypsStr,Source]),
204		(get_machine_wd_po(Options,PO,PO_Name),
205		get_texpr_info(PO,Infos),
206		(member(discharged(D,POLabel),Infos)
207		-> (D=true -> Discharged='yes' ; Discharged='no')
208		; Discharged='UNKNOWN',POLabel=PO_Name),
209		decompose_po(PO,Hyps,Goal),
210		translate_bexpression_with_limit(Hyps,Limit,HypsStr),
211		translate_bexpression_with_limit(Goal,Limit,GoalStr),
212		get_tk_table_position_info(Infos,Source)
213		), POs),
214		get_discharged_result(ResStr,_,_,AllDischarged).
215
216		decompose_po(b(implication(Hyps,Goal),pred,_),Hyps,Goal) :- !.
217		decompose_po(Goal,b(truth,pred,[]),Goal).
218
219		% analyse all WD POs for the loaded B machine
220		analyse_wd_for_machine(NrDischarged,NrTot,Discharged) :-
221		Options = [create_not_discharged_msg(warning),discharge_po,ignore_wd_infos,reorder_conjuncts],
222		analyse_wd_for_machine(NrDischarged,NrTot,Discharged,Options).
223		analyse_wd_for_machine_with_double_check(NrDischarged,NrTot,Discharged) :-
224		Options = [create_not_discharged_msg(warning),discharge_po,ignore_wd_infos,reorder_conjuncts,
225		create_full_po, prove_with_z3],
226		analyse_wd_for_machine(NrDischarged,NrTot,Discharged,Options).
227
228		analyse_wd_for_machine(NrDischarged,NrTot,Discharged,UnsortedOptions) :- reset_stats,
229		list_to_ord_set(UnsortedOptions,Options),
230		%list_to_ord_set([discharge_po,reorder_conjuncts],Options),
231		statistics(walltime,[Start,_]),
232	?	( get_machine_wd_po(Options,_PO,_),
233		fail
234		;
235		statistics(walltime,[Stop,_]), Delta is Stop-Start,
236		formatsilent('Analysis walltime: ~w ms~n',[Delta]),
237		print_stats,
238		get_discharged_result(_ResStr,NrDischarged,NrTot,Discharged)
239		).
240
241		:- use_module(probsrc(bmachine), [b_get_properties_from_machine/1, b_get_machine_all_constants/1,
242		b_get_machine_variables/1, b_get_invariant_from_machine/1,
243		b_get_static_assertions_from_machine/1, b_get_dynamic_assertions_from_machine/1,
244		b_get_machine_operation/6, b_get_initialisation_from_machine/2]).
245
246		transl_hyp(Axiom,Str) :-
247		translate:translate_bexpression_with_limit(Axiom,500,Str).
248
249		% if successful: returns a message explaining that an axiom is in contradiction with some other properties
250		tcltk_check_for_inconsistent_axiom(list(['The following predicate from PROPERTIES/axioms:',AxiomStr,
251		'is in contradiction with these predicates:' | TPS])) :-
252		find_inconsistent_axiom([],Axiom,NecHyps),
253		%get_specification_description(properties,PS),
254		translate:translate_bexpression_with_limit(Axiom,500,AxiomStr),
255		maplist(transl_hyp,NecHyps,TPS).
256
257		% try to find inconsistency in properties/axioms:
258		find_inconsistent_axiom(LOpt,Axiom,NecHyps) :-
259		reset_stats,
260		get_fresh_hyps_for_constants(OriginalHyps),
261		b_get_properties_from_machine(Properties),
262		list_to_ord_set([push_more_hyps|LOpt],Options),
263		push_hyp(OriginalHyps,Properties,Options,Hyps1),
264		member_in_conjunction(Axiom,Properties),
265		(debug_mode(on) -> print(' checking for contradiction with ==> '),translate:print_bexpr(Axiom),nl ; true),
266		NegAxiom = b(negation(Axiom),pred,[]),
267		prove_sequent_goal(NegAxiom,Hyps1,Options),
268		print('INCONSISTENCY FOUND, negation of axiom can be proven: '),
269		translate:print_bexpr(Axiom),nl,
270		% ord_member(minimize_full_po,Options),
271		print('Finding NECESSARY Hypotheses:'),nl,
272		minimize_necessary_hyps(Hyps1,NegAxiom,Options,NecHyps),
273		(debug_mode(on) -> translate:nested_print_bexpr(NecHyps),nl ; true).
274		%TODO: optionally take prob-ignore into account (predicate_has_ignore_pragma/1 and get_preference(use_ignore_pragmas,true))
275
276		minimize_necessary_hyps(hyp_rec(AvlNH,_),Goal,Options,NecHyps) :-
277		avl_range(AvlNH,Hyps),
278		minimize_hyps(Hyps,Goal,Options,NecHyps).
279
280
281		get_fresh_hyps_for_constants(OriginalHyps) :-
282		empty_hyps(E),
283		b_get_machine_all_constants(Csts),
284		add_new_hyp_variables(E,Csts,OriginalHyps).
285
286		% get POs for loaded B machine
287		get_machine_wd_po(LOpt,PO,PO_Name) :-
288		reset_stats,
289		list_to_ord_set(LOpt,Options),
290		b_get_properties_from_machine(Properties),
291		% TO DO: move Conjuncts without WD condition to front in first pass
292		get_fresh_hyps_for_constants(OriginalHyps),
293		( PO_Name = 'AXM',
294		debug_format(19,'Checking WD of PROPERTIES~n',[]),
295		ord_add_element(Options,po_label(PO_Name),Opt2),
296	?	compute_wd_with_reordering(Properties,OriginalHyps,Opt2,PO)
297
298		%debug:time(well_def_analyser:transform_wd(Properties,OriginalHyps,Opt2,NewProperties)),nl,fail)
299
300		; % TO DO: for transform: only use assertions if assertion checking is on!?
301
302		push_hyp(OriginalHyps,Properties,Options,Hyps1),
303		b_get_static_assertions_from_machine(StaticAssertions),
304
305		( PO_Name = 'THM-AXM',
306		ord_add_element(Options,po_label(PO_Name),Opt2),
307		conjunct_predicates(StaticAssertions,SAssPred),
308	?	compute_wd(SAssPred,Hyps1,Opt2,PO)
309		;
310		push_hyps(Hyps1,StaticAssertions,Options,Hyps2),
311		%portray_hyps(Hyps2),nl,
312		b_get_machine_variables(Vars),
313		add_new_hyp_variables(Hyps2,Vars,Hyps3),
314		b_get_invariant_from_machine(Invariant),
315		( PO_Name = 'INV',
316		debug_format(19,'Checking WD of INVARIANT~n',[]),
317		ord_add_element(Options,po_label(PO_Name),Opt2),
318	?	compute_wd_with_reordering(Invariant,Hyps3,Opt2,PO)
319		;
320		push_hyp(Hyps3,Invariant,Options,Hyps4),
321		b_get_dynamic_assertions_from_machine(DynAssertions),
322		( PO_Name = 'THM-INV',
323		debug_format(19,'Checking WD of ASSERTIONS~n',[]),
324		ord_add_element(Options,po_label(PO_Name),Opt2),
325		conjunct_predicates(DynAssertions,AssPred),
326	?	compute_wd(AssPred,Hyps4,Opt2,PO)
327		; push_hyps(Hyps4,DynAssertions,Options,Hyps5),
328		(
329		b_get_initialisation_from_machine(Body,_OType),
330		PO_Name = 'INIT',
331		debug_format(19,'Checking WD of INITIALISATION~n',[]),
332		ord_add_element(Options,po_label(PO_Name),Opt2),
333	?	compute_wd(Body,Hyps5,Opt2,PO)
334	?	; b_get_machine_operation(OpName,OpResults,OpFormalParameters,Body,_OType,_TopLevel),
335		PO_Name = OpName,
336		debug_format(19,'Checking WD of OPERATION ~w~n',[OpName]),
337		ord_add_element(Options,po_label(PO_Name),Opt2),
338		add_new_hyp_variables(Hyps5,OpFormalParameters,Hyps6),
339		add_new_hyp_variables(Hyps6,OpResults,Hyps7),
340	?	compute_wd(Body,Hyps7,Opt2,PO)
341		% TODO: optionally transform and store operation
342		)
343		)
344		)
345		)
346		),
347		inc_counter(PO_Name).
348
349
350		% --------------------
351
352		:- use_module(probsrc(tools_strings),[ajoin/2,ajoin_with_sep/3]).
353		% get label of current PO from Options
354		get_current_po_label(POLabel,Options) :-
355		findall(Label,get_label(Label,Options),Labels),
356		Labels \= [],
357		ajoin_with_sep(Labels,'/',POLabel).
358	?	get_label(Label,Options) :- member(po_label(L),Options),
359		(L = [_|_] -> member(Label,L) ; Label=L).
360
361		% --------------------
362
363		:- use_module(well_def_prover,[prove_po/3]).
364		:- use_module(probsrc(tools_lists),[ord_member_nonvar_chk/2]).
365
366		create_po(H,Target,Infos,Options,PO) :- create_po(H,Target,Infos,Options,PO,_).
367
368		create_po(H,Target,Infos,Options,PO,D) :- (var(H) ; H \= hyp_rec(_,_) ; var(Options)),!,
369		add_internal_error('Illegal hypotheses or options: ', create_po(H,Target,Infos,Options,PO,D)),fail.
370		create_po(Hyps,Target,Infos,Options,PO,Discharged) :-
371		get_normalized_and_renamed_predicate(Target,Hyps,RenTarget,NT),
372		(get_current_po_label(POLabel,Options) -> true ; POLabel = ''),
373		(ord_member(print_goal,Options) -> translate:print_bexpr(RenTarget),nl ; true),
374		(ord_member(discharge_po,Options)
375		-> (%nl,add_message(well_def_analyser,'Proving ',Target,Infos),
376		prove_proof_obligation(POLabel,Target,NT,Hyps,ProofTree)
377		-> debug_format(19,'PO ~w discharged: ~w~n',[POLabel,ProofTree]), %debug:nl_time,
378		inc_counter(discharged_po),
379		Discharged=true
380		; inc_counter(not_discharged_po),
381		Discharged=false,
382		(ord_member_nonvar_chk(create_not_discharged_msg(MsgType),Options)
383	?	-> (prove_po(negation(NT),Hyps,_NegProofTree)
384		-> NegProfStatus = ' (goal provably false)'
385		% Negation can be proven; i.e., PO cannot be proven unless there is a contradiction in Hyps
386		; NegProfStatus = ''
387		),
388		(POLabel = '' -> ajoin(['WD-PO not discharged', NegProfStatus, ': '],Msg)
389		; ajoin(['WD-PO [',POLabel,'] not discharged', NegProfStatus, ': '],Msg)
390		),
391		( MsgType=message -> add_message(well_def_analyser,Msg,Target,Infos)
392		; MsgType=warning -> add_warning(well_def_analyser,Msg,Target,Infos)
393		; MsgType=silent -> formatsilent('~w~w~n',[Msg,Target])
394		; add_error(well_def_analyser,Msg,Target,Infos)
395		),
396		debug_format(19,' Normalized Proof Target: ~w~n',[NT])
397		%,(debug_level_active_for(5) -> portray_hyps(Hyps) ; true) % hyps can be shown with create_full_po
398		; true
399		)
400		)
401		; Discharged=false % no discharging of POs
402		),
403		extract_pos_infos(Infos,PosInfos),
404		(ord_member(create_full_po,Options)
405		-> Hyps = hyp_rec(AvlNH,_),
406		avl_range(AvlNH,Hyp),
407		(Discharged=true, ord_member(minimize_full_po,Options)
408		-> minimize_hyps(Hyp,RenTarget,Options,NecHyps) % only show minimum core of hyps necessary for proving
409		; NecHyps=Hyp
410		),
411		%length(NecHyps,Len), print(hyps(Len)),nl,
412		conjunct_predicates(NecHyps,HypC),
413		safe_create_texpr(implication(HypC,RenTarget),pred,[discharged(Discharged,POLabel)|PosInfos],PO),
414		%nl,translate:print_bexpr(PO),nl, prove_po_with_atelierb(POLabel,[ml],PO,_),
415		% terms:term_hash(PO,Hash), print(Hash),nl,
416		%(ord_member(check_ast,Options) -> bsyntaxtree:check_ast(PO) ; true),
417		(ord_member(prove_with_z3,Options)
418		-> prove_po_with_smt(POLabel,z3,PO,Res),double_check(Discharged,z3,Res) ; true),
419		(ord_member(prove_with_ml,Options) -> prove_po_with_atelierb(POLabel,[ml],PO,_) ; true),
420		(ord_member(prove_with_pp,Options) -> prove_po_with_atelierb(POLabel,[pp],PO,_) ; true)
421		; RenTarget = b(POE,POT,POI),
422		append([discharged(Discharged,POLabel)|PosInfos],POI,POInfos),
423		PO = b(POE,POT,POInfos)
424		).
425
426		double_check(true,Solver,solution(S)) :- !,
427		add_error(Solver,'Double check of discharged PO failed, counter-example: ',S).
428		double_check(_,_,_).
429
430		% compute unsat core of hypotheses
431		minimize_hyps(Hyps,Goal,Options,NecHyps) :- minimize_hyps_aux(Hyps,Goal,Options,NecHyps,NecHyps),nl.
432
433		% TO DO: maybe do binary search / divide and conquer
434		% we could also examine which hypotheses were retrieved during the proof
435		% (but not easy; what if access inside a Prolog negation)
436		minimize_hyps_aux([],_,_,_,[]).
437		minimize_hyps_aux([H|T],Goal,Opts,NecessaryHyps,Tail) :-
438		(ord_member(push_more_hyps,Opts) -> ProofOpts = [push_more_hyps] ; ProofOpts=[]),
439		\+ (Tail=T,prove_sequent_cur_context(Goal,NecessaryHyps,ProofOpts)), % we need H to prove Goal
440		!,
441		write('+'),
442		Tail = [H|TT],
443		minimize_hyps_aux(T,Goal,Opts,NecessaryHyps,TT).
444		minimize_hyps_aux([_|T],Goal,Opts,NecessaryHyps,Tail) :-
445		write('-'),
446		minimize_hyps_aux(T,Goal,Opts,NecessaryHyps,Tail).
447
448		:- use_module(probsrc(runtime_profiler),[register_profiler_runtime/5]).
449		:- use_module(extrasrc(atelierb_provers_interface),[prove_sequent_with_provers/3]).
450		prove_po_with_atelierb(POLabel,Provers,PO,ProofRes) :- runtime_profiler:print_runtime_profile,
451		format('Proving PO ~w with ~w~n',[POLabel,Provers]),
452		statistics(walltime,[T1,_]),
453		catch(
454		prove_sequent_with_provers(Provers,PO,ProofRes), % we cannot use time_out as PP/ML/KRT are a separate process
455		user_interrupt_signal,
456		ProofRes = user_interrupt_signal),
457		statistics(walltime,[T2,_]), WT is T2-T1,
458		!,
459		register_profiler_runtime(atelierb(ProofRes),well_def_analyser,POLabel,WT,WT),
460		format('Result of ~w on PO = ~w (walltime ~w ms)~n',[Provers,ProofRes,WT]),
461		(ProofRes=user_interrupt_signal
462		-> write(' Continue? [y/n] => '), flush_output, read(Cont),
463		(Cont='y' -> true ; Cont='yes' -> true ; throw(user_interrupt_signal))
464		; true).
465
466		:- use_module(probsrc(bsyntaxtree),[create_negation/2]).
467		:- use_module(smt_solvers_interface(smt_solvers_interface),[smt_solve_predicate/4]).
468		prove_po_with_smt(POLabel,Solver,PO,ProofRes) :- runtime_profiler:print_runtime_profile,
469		format('Proving PO ~w with ~w~n',[POLabel,Solver]),
470		%translate:print_bexpr(PO),nl,
471		statistics(walltime,[T1,_]),
472		create_negation(PO,NegPO),
473		smt_solve_predicate(Solver,NegPO,_State,ProofRes),!,
474		statistics(walltime,[T2,_]), WT is T2-T1,
475		register_profiler_runtime(smt(Solver,ProofRes),well_def_analyser,POLabel,WT,WT),
476		format('Result of ~w on PO = ~w (walltime ~w ms)~n',[Solver,ProofRes,WT]).
477
478		% a wrapper to prove_po which also checks for obvious POs using type info:
479		prove_proof_obligation(POLabel,Target,_NT,Hyps,ProofTree) :-
480		obvious_po(Target,Kind,Hyps),!,
481		debug_format(19,'Obvious ~w PO (due to typing info): ~w~n',[Kind,POLabel]),
482		register_profiler_runtime(wd_prob_prover(obvious_po),well_def_analyser,POLabel,0,0),
483		ProofTree = obvious_po(Kind).
484		prove_proof_obligation(POLabel,_Target,NT,Hyps,ProofTree) :-
485		statistics(runtime,[RT1,_]),
486		statistics(walltime,[T1,_]),
487	?	(prove_po(NT,Hyps,ProofTree) -> Res=discharged
488		; Res=unknown,ProofTree='' % ,format('~n *********** WD PO UNKNOWN ~w~n~n',[POLabel])
489		),
490		statistics(runtime,[RT2,_]), RT is RT2-RT1,
491		statistics(walltime,[T2,_]), WT is T2-T1,
492		register_profiler_runtime(wd_prob_prover(Res),well_def_analyser,POLabel,RT,WT),
493		(WT>10 -> format('Proof of \'~w\' took ~w ms, result=~w (~w)~n',[POLabel,WT,Res,ProofTree])
494		%, translate:print_bexpr(_Target),nl, assertz(well_def_prover:dt),(prove_po(NT,Hyps,_) -> true ; true), trace
495		; true),
496		Res=discharged.
497
498		%:- use_module(well_def_hyps,[is_finite_type_for_wd/2]).
499		obvious_po(b(finite(Set),pred,_),Kind,Hyps) :- Kind=finite,
500		get_texpr_type(Set,Type), % check this proof rule here, as prove_po has no longer types in the AST
501		is_finite_type_for_wd(Type,Hyps).
502
503		% ------------------------------
504
505		:- dynamic counter/2.
506		reset_stats :- retractall(counter(_,_)),
507		assertz(counter(discharged_po,0)),
508		assertz(counter(not_discharged_po,0)).
509
510		inc_counter(C) :- (retract(counter(C,Nr)) -> N1 is Nr+1 ; N1 = 1),
511		assertz(counter(C,N1)).
512
513		print_stats :- silent_mode(on),!.
514		print_stats :- findall(C/N,counter(C,N),L), format('WD Stats: ~w~n',[L]).
515
516		%tcltk_get_stats(list([list(['Category','Nr'])|Stats])) :-
517		% findall(list([C,N]),counter(C,N),Stats).
518
519		get_discharged_result(ResStr,D,Tot,AllDischarged) :- counter(not_discharged_po,ND),
520		counter(discharged_po,D), Tot is ND+D,
521		ajoin([D,'/',Tot,' DISCHARGED'],ResStr),
522		(ND=0 -> AllDischarged='TRUE' ; AllDischarged='FALSE').
523
524		% ------------------------------
525
526		annotate_wd(TExpr,AnnotatedTExpr) :-
527		reset_stats,
528		%empty_hyps(EH),
529		push_properties_invariant_hyps([],EH),
530		Options = [discharge_po,insert_assertion_expressions],
531		transform_wd(TExpr,EH,Options,AnnotatedTExpr),
532		print_bexpr_with_wd_info(AnnotatedTExpr).
533
534
535		:- use_module(probsrc(preferences),[temporary_set_preference/3, reset_temporary_preference/2, get_preference/2]).
536		print_bexpr_with_wd_info(TExpr) :-
537		temporary_set_preference(pp_wd_infos,true,Chng),
538		call_cleanup(translate:nested_print_bexpr(TExpr),reset_temporary_preference(pp_wd_infos,Chng)),
539		nl.
540
541		% transform an AST by adding annotations about discharged POs
542		transform_wd(b(Expr,Type,Info),Hypotheses,Options,b(NewExpr0,Type,NewInfo0)) :-
543		memberchk(contains_wd_condition,Info),
544		!,
545		syntaxtransformation(Expr,Subs,TNames,NSubs,NewExpr),
546		add_new_hyp_variables(Hypotheses,TNames,Hyps2),
547		(wd_transparent(Expr)
548		-> l_transform_wd(Subs,Hyps2,Options,NSubs), adapt_info(Info,NSubs,NewInfo)
549		; wd_like_conjunction(Expr,Ids,A,B)
550		-> l_transform_conj_wd([A,B],Hyps2,Options,[TA,TB]),
551		check_top_level_wd(conj,Expr,Type,Info,Hyps2,Options, [TA,TB], NewInfo,_),
552		wd_like_conjunction(NewExpr,Ids,TA,TB)
553	?	; transform_special_expr(Expr,Type,Info,Hyps2,Options,NewExpr,NewInfo) -> true
554		; l_transform_wd(Subs,Hyps2,Options,NSubs)
555		->
556		check_top_level_wd(other,Expr,Type,Info,Hyps2,Options, NSubs, NewInfo, PO)
557		),
558		% PO is either a real PO or discharged atom
559		insert_assertions(PO,NewExpr,Type,NewInfo,Options,NewExpr0,NewInfo0).
560		transform_wd(TExpr,_,_,TExpr). % copy entire expression if no contains_wd_condition info
561
562		insert_assertions(discharged,NewExpr,_,NewInfo,_,NewExpr0,NewInfo0) :- !, NewExpr0=NewExpr,NewInfo0=NewInfo.
563		insert_assertions(_,NewExpr,pred,NewInfo,_,NewExpr0,NewInfo0) :- !, NewExpr0=NewExpr,NewInfo0=NewInfo.
564		insert_assertions(_,NewExpr,subst,NewInfo,_,NewExpr0,NewInfo0) :- !, NewExpr0=NewExpr,NewInfo0=NewInfo.
565		insert_assertions(_,NewExpr,_,NewInfo,Options,NewExpr0,NewInfo0) :-
566		nonmember(insert_assertion_expressions,Options), !, NewExpr0=NewExpr,NewInfo0=NewInfo.
567		%insert_assertions(PO,NewExpr,Type,NewInfo,_Options,NewExpr0) :- !,
568		% BOOL_EXPR = b(convert_bool(PO),boolean,NewInfo),
569		% MSG = b(string('WD-ERROR'),string,[]),
570		% % TODO: adapt ASSERT_EXPR to delays & check more strongly than assertion_expression
571		% NewExpr0 = external_function_call('ASSERT_EXPR',[BOOL_EXPR,MSG, b(NewExpr,Type,NewInfo)]).
572		insert_assertions(PO,NewExpr,Type,NewInfo,_Options,NewExpr0,NewInfo0) :-
573		NewInfo0 = [prob_annotation(strong_check_with_delay)|NewInfo], % ensure we really guard the Expression
574		% example usage in repl :wde f = [1,2,3,4,5] & f(x)=6 & x>6
575		% TODO: improve error message, stipulating at least the operator for which the PO is added
576		% also check that we are not adding an assert for an assert
577		NewExpr0 = assertion_expression(PO,'WD-ERROR', b(NewExpr,Type,NewInfo)).
578
579
580		check_top_level_wd(conj,Expr,Type,Info,Hyps,Options, _NSubs, NewInfo, FullPO) :-
581		Discharged=false,
582		findall(PO,create_top_level_wd_po_conj_like(Expr,Type,Info,Hyps,Options,PO,Discharged),POs),
583		POs \= [],
584		!, % PO not proven; keep Info as is
585		%write(-), flush_output, %print(not_discharged(PO)),nl,
586		conjunct_predicates(POs,FullPO),
587		NewInfo=Info.
588		check_top_level_wd(other,Expr,Type,Info,Hyps,Options, _NSubs, NewInfo, FullPO) :-
589		Discharged=false,
590		findall(PO,create_top_level_wd_po(Expr,Type,Info,Hyps,Options,PO,Discharged),POs),
591		POs \= [],
592		!, % PO not proven; keep Info as is
593		%write(-), flush_output, print(not_discharged(PO)),nl,
594		conjunct_predicates(POs,FullPO),
595		NewInfo=Info.
596		check_top_level_wd(_,_Expr,_Type,Info,_Hyps,_Options, NSubs, NewInfo, discharged) :- % no top-level PO or PO proven
597		adapt_info(Info,NSubs,NewInfo).
598
599		%:- use_module(library(lists),[delete/3]).
600		% adapt WD Info depending on result of analysis
601	?	adapt_info(Info,Subs,NewInfo) :- subs_contain_wd_condition(Subs),!,NewInfo=Info.
602		adapt_info(Info,_,[discharged_wd_po|NewInfo]) :-
603		NewInfo=Info, memberchk(contains_wd_condition,Info).
604		%delete(Info,contains_wd_condition,NewInfo).
605
606		subs_contain_wd_condition(Subs) :-
607	?	member(b(_,_,Infos),Subs),
608		(memberchk(contains_wd_condition,Infos) -> nonmember(discharged_wd_po,Infos)).
609
610		% transform independent sub-arguments
611		l_transform_wd([],_Hyps,_Options,[]).
612		l_transform_wd([Sub|T],Hyps,Options,[NSub|NT]) :-
613		transform_wd(Sub,Hyps,Options,NSub),
614		l_transform_wd(T,Hyps,Options,NT).
615
616		% transform conjunction like sub-arguments, with left-to-right adding of hypotheses
617		l_transform_conj_wd([],_Hyps,_Options,[]).
618		l_transform_conj_wd([Sub|T],Hyps,Options,[NSub|NT]) :-
619		transform_wd(Sub,Hyps,Options,NSub),
620		push_hyp(Hyps,Sub,Options,Hyps2),
621		l_transform_conj_wd(T,Hyps2,Options,NT).
622
623		% transform special cases where sub-arguments are not independent nor conjunction-like
624		% TO DO: assign
625		transform_special_expr(disjunct(A,B),_,Info,Hyps,Options,disjunct(TA,TB),NewInfo) :-
626		transform_wd(A,Hyps,Options,TA),
627		negate_hyp(A,NA),
628		push_hyp(Hyps,NA,Options,Hyps2),
629		transform_wd(B,Hyps2,Options,TB),
630		adapt_info(Info,[TA,TB],NewInfo).
631		transform_special_expr(IFTE,_,Info,Hyps,Options,TransformedIFTE,NewInfo) :-
632		is_ifte(IFTE,Functor,A,B,C), is_ifte(TransformedIFTE,Functor,TA,TB,TC),
633		transform_wd(A,Hyps,Options,TA),
634		push_hyp(Hyps,A,Options,Hyps2),
635		transform_wd(B,Hyps2,Options,TB),
636		negate_hyp(A,NA),
637		push_hyp(Hyps,NA,Options,Hyps3),
638		transform_wd(C,Hyps3,Options,TC),
639		adapt_info(Info,[TA,TB,TC],NewInfo).
640		transform_special_expr(recursive_let(ID,B),_,Info,Hyps,Options,recursive_let(ID,TB),NewInfo) :- NewInfo=Info,
641		transform_wd(B,Hyps,Options,TB).
642		transform_special_expr(general_sum(Ids,P,E),_Type,Info,Hyps,Options,general_sum(Ids,TP,TE),NewInfo) :-
643		NewInfo=Info, % Note: we do not try to discharge finite PO; TODO: add
644		transform_wd(P,Hyps,Options,TP),
645		push_hyp(Hyps,P,Options,Hyps2),
646		transform_wd(E,Hyps2,Options,TE).
647		transform_special_expr(general_product(Ids,P,E),_Type,Info,Hyps,Options,general_product(Ids,TP,TE),NewInfo) :-
648		NewInfo=Info, % Note: we do not try to discharge finite PO
649		transform_wd(P,Hyps,Options,TP),
650		push_hyp(Hyps,P,Options,Hyps2),
651		transform_wd(E,Hyps2,Options,TE).
652		transform_special_expr(if(List),_,Info,Hyps,Options,if(TList),NewInfo) :-
653		list_transform_if_elsif_wd(List,Hyps,Options,TList),
654		adapt_info(Info,TList,NewInfo).
655
656		list_transform_if_elsif_wd([],_,_,[]).
657		list_transform_if_elsif_wd([b(if_elsif(A,Body),Type,I) | T], Hyps,Options,Res) :-
658		is_truth(A),!,
659		Res=[b(if_elsif(A,TBody),Type,I) | T],
660		transform_wd(Body,Hyps,Options,TBody).
661		list_transform_if_elsif_wd([b(if_elsif(A,Body),Type,I) | T], Hyps,Options,
662		[b(if_elsif(TA,TBody),Type,I) | TT]) :-
663		transform_wd(A,Hyps,Options,TA),
664		push_hyp(Hyps,A,Options,Hyps2),
665		transform_wd(Body,Hyps2,Options,TBody),
666		negate_hyp(A,NA),
667		push_hyp(Hyps,NA,Options,Hyps3),
668		list_transform_if_elsif_wd(T,Hyps3,Options,TT).
669
670		% ------------------------------
671
672		:- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2]).
673		:- use_module(probsrc(tools),[split_list/4]).
674
675		% process those conjuncts with no WD condition first; this means we have more hypotheses for proving and is safe for ProB
676		% Option 'skip_finite_po' can be used to not generate finite(.) POs.
677		% These POs are, e.g., irrelevant for constraint solving in ProB since the solver would exceed the timeout if finite(.) cannot be proven.
678		compute_wd_with_reordering(TExpr,Hypotheses,Options,PO) :- \+ ord_member(reorder_conjuncts,Options),!,
679		compute_wd(TExpr,Hypotheses,Options,PO).
680		compute_wd_with_reordering(TExpr,Hypotheses,Options,PO) :-
681		conjunction_to_list(TExpr,Conjuncts),
682		split_list(is_well_defined_conjunct,Conjuncts,Conj1,Conj2),
683		Conj2 \= [], % otherwise no WD condition anyway
684		(ord_member(ignore_wd_infos,Options)
685		-> append(Conj1,Conj2,Conj12),
686	?	list_compute_wd(Conj12,Options,Hypotheses,PO)
687		; push_hyps(Hypotheses,Conj1,Options,Hyps2), % push the Hypotheses without WD checking
688		list_compute_wd(Conj2,Options,Hyps2,PO)
689		).
690
691		%is_well_defined_conjunct(TE) :- print('Checking conjunct: '), translate:print_bexpr(TE),nl,fail.
692		is_well_defined_conjunct(b(_,_,Infos)) :- nonmember(contains_wd_condition,Infos),!.
693		%is_well_defined_conjunct(TE) :- print('Not well defined: '), translate:print_bexpr(TE),nl,fail.
694
695		compute_wd(TExpr,Hypotheses,Options,PO) :-
696		syntaxtraversion(TExpr,Expr,Type,Infos,Subs,TNames),
697		(ord_member(ignore_wd_infos,Options) -> true ; memberchk(contains_wd_condition,Infos) -> true),
698		%(print(Expr),nl ; print(backtrack(Expr)),nl,fail),
699	?	(get_info_labels(Infos,Label) -> ord_add_element(Options,po_label(Label),Opt2) ; Opt2=Options),
700	?	compute_wd_aux(Expr,Type,Infos,Subs,TNames,Hypotheses,Opt2,PO),
701		true. %check_if_po_expected(PO,TExpr,Infos).
702
703		check_if_po_expected(PO,TExpr,Infos) :-
704		( memberchk(contains_wd_condition,Infos) -> true
705		; get_texpr_info(PO,POInfo), POInfo=[discharged(true,_)|_] -> true
706		% Note: Sigma currently gets no contains_wd_condition, but has finiteness WD constraint
707		; add_error(well_def_analyser,'Unexpected WD-PO for expression marked to have no WD condition:',PO,TExpr)
708		).
709
710		:- use_module(library(lists),[maplist/3]).
711		% treat assignment substitution
712		% see b_assign_values_or_functions in b_interpreter
713		compute_wd_assign(Hyps,Options,PO,LHS,RHS) :- LHS=b(function(F,X),_,_),
714		!,
715		% special case for f(X) := RHS
716		( compute_wd(F,Hyps,Options,PO) % ?
717		; compute_wd(X,Hyps,Options,PO)
718	?	; compute_wd(RHS,Hyps,Options,PO) ).
719		compute_wd_assign(Hyps,Options,PO,_,RHS) :- % LHS must be an identifier
720	?	compute_wd(RHS,Hyps,Options,PO).
721
722		compute_wd_aux(assign(LHSList,RHSList),_,_,_,[],Hypotheses,Options,PO) :-
723		!,
724	?	maplist(compute_wd_assign(Hypotheses,Options,PO),LHSList,RHSList).
725		compute_wd_aux(Expr,_,_,Subs,TNames,Hypotheses,Options,PO) :-
726		wd_transparent(Expr),!,
727		% cut: only look at WD condition of all sub-arguments
728		add_new_hyp_variables(Hypotheses,TNames,Hyps2),
729	?	member(Sub,Subs),
730	?	compute_wd(Sub,Hyps2,Options,PO).
731		% Now the rules which do not look at all sub-arguments with original Hypotheses:
732		compute_wd_aux(conjunct(A,B),_,_,_,_,Hypotheses,Options,PO) :- !,
733		flatten_conjunct(A,B,List), % avoid re-pushing hyps if A is nested conjunct
734	?	compute_wd_conjuncts(List,Hypotheses,Options,PO).
735		compute_wd_aux(sequence(List),subst,_,_,_,Hypotheses,Options,PO) :- % sequential composition
736		!,
737	?	sequence_compute_wd(List,Options,Hypotheses,PO).
738		compute_wd_aux(while(COND,STMT,INV,VARIANT),_,Infos,_,_,Hypotheses,Options,PO) :- !,
739		(member(modifies(VarsModified),Infos) -> debug_println(9,computed_wd_while(VarsModified))
740		; add_error(well_def_analyser,'While does not contain modifies info:',Infos,Infos),
741		VarsModified=[]
742		),
743		copy_hyp_variables(Hypotheses,VarsModified,Hyps2), % we can no longer make any assumption about the modified vars
744		% this corresponds to a universal quantification
745		( compute_wd(INV,Hyps2,Options,PO) % Invariant must hold before and after WHILE loop
746		;
747		push_hyp(Hyps2,INV,Options,Hyps3), % add INV to the hypotheses now for the other parts of the WHILE
748		(
749		compute_wd(COND,Hyps3,Options,PO)
750		;
751		compute_wd(VARIANT,Hyps3,Options,PO) % NAT proof rule for While must also hold if P is false according to Atelier-B handbook (otherwise we could have pushed COND onto the stack)
752		;
753		push_hyp(Hyps3,COND,Options,Hyps4),
754		compute_wd(STMT,Hyps4,Options,PO) % Statement is only executed if COND is true; INV is checked
755		)
756		).
757		compute_wd_aux(Expr,Type,Infos,Subs,TNames,Hypotheses,Options,PO) :-
758		wd_like_conjunction(Expr,_,A,B),!,
759		add_new_hyp_variables(Hypotheses,TNames,Hyps2),
760		( create_top_level_wd_po_conj_like(Expr,Type,Infos,Hyps2,Options,PO,_Discharged) % e.g., for assertion_expression
761		;
762	?	compute_wd_aux(conjunct(A,B),Type,Infos,Subs,TNames,Hyps2,Options,PO)
763		).
764		compute_wd_aux(if(List),_,_,_,_,Hypotheses,Options,PO) :- !,
765	?	list_compute_if_elsif_wd(List,Hypotheses,Options,PO).
766		compute_wd_aux(disjunct(A,B),_,_,_,_,Hypotheses,Options,PO) :- !,
767	?	(compute_wd(A,Hypotheses,Options,PO)
768		;
769		negate_hyp(A,NA),
770		push_hyp(Hypotheses,NA,Options,NewHyp),
771	?	compute_wd(B,NewHyp,Options,PO)).
772		compute_wd_aux(general_sum(Ids,P,E),Type,Infos,_,_,Hypotheses,Options,PO) :- !, % SIGMA, real or integer
773		( % first the sub arguments
774		add_new_hyp_variables(Hypotheses,Ids,Hyps2),
775		( compute_wd(P,Hyps2,Options,PO)
776		;
777		push_hyp(Hyps2,P,Options,NewHyp),
778	?	compute_wd(E,NewHyp,Options,PO)
779		)
780		; % now the PO of general_sum itself
781		create_top_level_wd_po(general_sum(Ids,P,E),Type,Infos,Hypotheses,Options,PO,_Discharged)
782		).
783		compute_wd_aux(general_product(Ids,P,E),Type,Infos,Subs,TNames,Hypotheses,Options,PO) :- !, % PI
784	?	compute_wd_aux(general_sum(Ids,P,E),Type,Infos,Subs,TNames,Hypotheses,Options,PO).
785		compute_wd_aux(rlevent(_Name,_Sect,_Status,_Params,Guard,Theorems,Actions,VWit,PWit,_Unmod,_AbstractEvents),
786		_,_Infos,_Subs,TNames,Hypotheses,Options,PO) :- !,
787		add_new_hyp_variables(Hypotheses,TNames,Hyps2),
788		% TO DO: treat nested lists VWit,...
789		Act = b(parallel(Actions),subst,[]),
790		append([[Guard],Theorems,VWit,PWit,[Act]],List),
791	?	list_compute_wd(List,Options,Hyps2,PO).
792		compute_wd_aux(recursive_let(_ID,Body),_,_,_,_,Hypotheses,Options,PO) :- !,
793		% the ID does not have to be added to hypothesis stack !
794	?	compute_wd(Body,Hypotheses,Options,PO).
795		compute_wd_aux(IFTE,_,_,_,_,Hypotheses,Options,PO) :- is_ifte(IFTE,_,A,B,C), !,
796	?	(compute_wd(A,Hypotheses,Options,PO)
797		;
798		push_hyp(Hypotheses,A,Options,NewHyp),
799		compute_wd(B,NewHyp,Options,PO)
800		;
801		negate_hyp(A,NA),
802		push_hyp(Hypotheses,NA,Options,NewHyp),
803	?	compute_wd(C,NewHyp,Options,PO)).
804		% ----------------
805		% Now the rules where we also look at the sub-arguments with original Hypotheses:
806		compute_wd_aux(_,_,_,Subs,TNames,Hypotheses,Options,PO) :-
807		add_new_hyp_variables(Hypotheses,TNames,Hyp2),
808		% look at WD condition of all sub-arguments independently
809	?	member(Sub,Subs),
810	?	compute_wd(Sub,Hyp2,Options,PO).
811		% Now the specific rules:
812		compute_wd_aux(Expr,Type,Infos,_,_,Hypotheses,Options,PO) :-
813	?	create_top_level_wd_po(Expr,Type,Infos,Hypotheses,Options,PO,_Discharged).
814
815		% treat a list of conjuncts (after flattening)
816		%compute_wd_conjuncts([],_,_,_) :- fail.
817		compute_wd_conjuncts([A|T],Hypotheses,Options,PO) :-
818	?	(compute_wd(A,Hypotheses,Options,PO)
819		;
820		T \= [],
821		push_hyp(Hypotheses,A,Options,NewHyp),
822	?	compute_wd_conjuncts(T,NewHyp,Options,PO)).
823
824		% flatten conjuncts to avoid re-pushing the same hypotheses
825		flatten_conjunct(ConjA,ConjB,List) :-
826		flatten_conjunct_dl(ConjA,List,[ConjB]). % Tail not flattened; not necessary for performance
827		flatten_conjunct_dl(b(conjunct(A,B),_,_)) --> !, flatten_conjunct_dl(A), flatten_conjunct_dl(B).
828		flatten_conjunct_dl(X) --> [X].
829
830		is_ifte(if_then_else(A,B,C),if_then_else,A,B,C).
831		is_ifte(if_predicate(A,B,C),if_predicate,A,B,C).
832
833		% create top-level WD conditions for conjunction-like operators; not for sub-arguments
834		% conjunction like operators can use the fact that LHS is true to prove WD of RHS
835		% but here we only worry about additional top-level POs by the operator
836		% the predicate must create a single full top-level PO and not succeed upon backtracking
837		create_top_level_wd_po_conj_like(assertion_expression(A,_Msg,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
838		Target = A,
839		ord_add_element(Options,po_label('ASSERT'),Options2),
840		create_po(Hypotheses,Target,Infos,Options2,PO,Discharged).
841
842		% create top-level WD conditions; not for sub-arguments
843		create_top_level_wd_po(function(A,B),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
844		(get_texpr_type(B,TB),
845		safe_create_texpr(domain(A),set(TB),[],DomA),
846		safe_create_texpr(member(B,DomA),pred,[],Target),
847		create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
848		%, tools_printing:print_term_summary(created_function_po(Target,PO))
849		;
850		create_partial_fun_target(A,Target),
851		create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
852		).
853		create_top_level_wd_po(div(_,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
854		create_texpr(integer(0),integer,[],Zero),
855		safe_create_texpr(not_equal(B,Zero),pred,[],Target),
856		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
857		create_top_level_wd_po(div_real(_,B),real,Infos,Hypotheses,Options,PO,Discharged) :- !,
858		create_texpr(real('0.0'),real,[],Zero),
859		safe_create_texpr(not_equal(B,Zero),pred,[],Target),
860		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
861		create_top_level_wd_po(floored_div(_,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
862		create_texpr(integer(0),integer,[],Zero),
863		safe_create_texpr(not_equal(B,Zero),pred,[],Target),
864		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
865		create_top_level_wd_po(modulo(A,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
866		create_texpr(integer(0),integer,[],Zero),
867		( safe_create_texpr(greater(B,Zero),pred,[],Target), % does TLA require this to be positive??
868		create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
869		; \+ z_or_tla_minor_mode,
870		safe_create_texpr(greater_equal(A,Zero),pred,[],Target), % in B A must be positive
871		create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
872		).
873		create_top_level_wd_po(power_of(A,B),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
874		create_texpr(integer(0),integer,[],Zero),
875		( AB=B, % B >= 0 must hold in B and Event-B
876		safe_create_texpr(greater_equal(AB,Zero),pred,[],Target),
877		create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
878		; eventb_mode, % TO DO: what happens in Z and TLA+?
879		AB=A, % A >= 0 must hold in Event-B
880		safe_create_texpr(greater_equal(AB,Zero),pred,[],Target),
881		create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
882		).
883		create_top_level_wd_po(power_of_real(A,B),real,Infos,Hypotheses,Options,PO,Discharged) :- !,
884		% power_of_real has a WD condition, real ** integer has not
885		create_texpr(real('0.0'),real,[],Zero),
886		( % A < 0 => real(floor(B))=B
887		safe_create_texpr(less_real(A,Zero),pred,[],LHS),
888		safe_create_texpr(convert_int_floor(B),integer,[],FloorB),
889		safe_create_texpr(convert_real(FloorB),real,[],BB),
890		safe_create_texpr(equal(B,BB),pred,[],RHS),
891		safe_create_texpr(implication(LHS,RHS),pred,[],Target),
892		create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
893		; % A = 0 => B >= 0
894		safe_create_texpr(equal(A,Zero),pred,[],LHS),
895		safe_create_texpr(less_equal_real(Zero,B),pred,[],RHS),
896		safe_create_texpr(implication(LHS,RHS),pred,[],Target),
897		create_po(Hypotheses,Target,Infos,Options,PO,Discharged)
898		).
899		create_top_level_wd_po(iteration(_Rel,Index),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
900		create_texpr(integer(0),integer,[],Zero),
901		safe_create_texpr(greater_equal(Index,Zero),pred,[],Target),
902		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
903		create_top_level_wd_po(card(S),integer,Infos,Hypotheses,Options,PO,Discharged) :-
904		!,
905		\+ skip_finite_pos(Options),
906		safe_create_texpr(finite(S),pred,[contains_wd_condition],Target),
907		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
908		create_top_level_wd_po(max(S),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
909		get_texpr_type(S,TS),
910		safe_create_texpr(not_equal(S,b(empty_set,TS,[])),pred,[],Target1),
911		( skip_finite_pos(Options)
912		-> Target = Target1
913		; safe_create_texpr(finite(S),pred,[contains_wd_condition],Target2),
914		conjunct_predicates([Target1,Target2],Target) % this is a sufficient condition, not a necessary one
915		),
916		% create a single PO, because of use in check_top_level_wd
917		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
918		create_top_level_wd_po(min(S),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
919		get_texpr_type(S,TS),
920		safe_create_texpr(not_equal(S,b(empty_set,TS,[])),pred,[],Target1),
921		( skip_finite_pos(Options)
922		-> Target = Target1
923		; safe_create_texpr(finite(S),pred,[contains_wd_condition],Target2),
924		conjunct_predicates([Target1,Target2],Target) % this is a sufficient condition, not a necessary one
925		),
926		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
927		create_top_level_wd_po(max_real(S),real,Infos,Hypotheses,Options,PO,Discharged) :- !,
928		create_top_level_wd_po(max(S),integer,Infos,Hypotheses,Options,PO,Discharged). % create same PO as for integer max
929		create_top_level_wd_po(min_real(S),real,Infos,Hypotheses,Options,PO,Discharged) :- !,
930		create_top_level_wd_po(min(S),integer,Infos,Hypotheses,Options,PO,Discharged). % ditto
931		create_top_level_wd_po(general_intersection(A),TA,Infos,Hypotheses,Options,PO,Discharged) :- !, % inter
932		safe_create_texpr(not_equal(A,b(empty_set,set(TA),[])),pred,[],Target),
933		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
934		% Sequence operators:
935		create_top_level_wd_po(size(S),integer,Infos,Hypotheses,Options,PO,Discharged) :- !,
936		% we do not have to create a finite PO: sequences are by construction finite
937		create_sequence_target(S,Target),
938		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
939		create_top_level_wd_po(insert_tail(S,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
940		create_sequence_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
941		create_top_level_wd_po(insert_front(_,S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
942		% page 174 of Abrial's book just requires that S is a partial function NATURAL1 +-> TYPE
943		create_sequence_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
944		create_top_level_wd_po(rev(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
945		create_sequence_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
946		create_top_level_wd_po(concat(S1,S2),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
947		(create_sequence_target(S1,Target) ; create_sequence_target(S2,Target)),
948		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
949		create_top_level_wd_po(general_concat(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
950		create_seq_seq_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
951		create_top_level_wd_po(first(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
952		create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
953		create_top_level_wd_po(last(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
954		create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
955		create_top_level_wd_po(front(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
956		create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
957		create_top_level_wd_po(tail(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
958		create_sequence1_target(S,Target), create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
959		create_top_level_wd_po(restrict_front(S,N),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
960		( create_sequence_target(S,Target) ; create_seq_interval_target(S,N,Target) ),
961		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
962		create_top_level_wd_po(restrict_tail(S,N),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
963		( create_sequence_target(S,Target) ; create_seq_interval_target(S,N,Target) ),
964		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
965		create_top_level_wd_po(mu(S),_,Infos,Hypotheses,Options,PO,Discharged) :- !, % Z MU Operator
966		get_texpr_type(S,TS),
967		safe_create_texpr(not_equal(S,b(empty_set,TS,[])),pred,[],Target1),
968		create_texpr(integer(1),integer,[],One),
969		safe_create_texpr(card(S),integer,[contains_wd_condition],CardS),
970		safe_create_texpr(less_equal(CardS,One),pred,[],Target2),
971		( skip_finite_pos(Options)
972		-> conjunct_predicates([Target1,Target2],Target)
973		; safe_create_texpr(finite(S),pred,[contains_wd_condition],Target3),
974		conjunct_predicates([Target1,Target3,Target2],Target)
975		),
976		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
977		% External Functions:
978		create_top_level_wd_po(external_function_call('MU',[S]),T,Infos,Hypotheses,Options,PO,Discharged) :- !,
979		create_top_level_wd_po(mu(S),T,Infos,Hypotheses,Options,PO,Discharged).
980		create_top_level_wd_po(external_function_call('CHOOSE',[A]),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
981		get_texpr_type(A,TA),
982		safe_create_texpr(not_equal(A,b(empty_set,set(TA),[])),pred,[],Target),
983		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
984		create_top_level_wd_po(external_function_call('SQUASH',[A]),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
985		create_partial_fun_target(A,Target),
986		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
987		create_top_level_wd_po(external_function_call(C,Args),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
988		% external_fun_has_wd_condition is true
989		get_preference(wd_ignore_external_funs,false),
990		create_wd_po_for_external_call(C,Args,Infos,Hypotheses,Options,PO,Discharged).
991		create_top_level_wd_po(external_subst_call(C,_),_,Infos,Hypotheses,Options,PO,Discharged) :- !, % ditto
992		get_preference(wd_ignore_external_funs,false),
993		create_po(Hypotheses,b(unknown_truth_value(C),pred,[]),Infos,Options,PO,Discharged).
994		create_top_level_wd_po(external_pred_call(C,Args),_,Infos,Hypotheses,Options,PO,Discharged) :- !, % ditto
995		get_preference(wd_ignore_external_funs,false),
996		create_wd_po_for_external_call(C,Args,Infos,Hypotheses,Options,PO,Discharged).
997		create_top_level_wd_po(general_product(Ids,P,E),Type,Infos,Hypotheses,Options,PO,Discharged) :- !,
998		create_top_level_wd_po(general_sum(Ids,P,E),Type,Infos,Hypotheses,Options,PO,Discharged).
999		create_top_level_wd_po(general_sum(Ids,P,_E),_,Infos,Hypotheses,Options,PO,Discharged) :- !,
1000		\+ skip_finite_pos(Options),
1001		create_comprehension_set(Ids,P,[],TS),
1002		safe_create_texpr(finite(TS),pred,[contains_wd_condition],Target),
1003		create_po(Hypotheses,Target,Infos,Options,PO,Discharged).
1004		% Unsupported:
1005		create_top_level_wd_po(Expr,T,I,Hypotheses,Options,PO,Discharged) :-
1006		functor(Expr,F,N),
1007		ajoin(['Unsupported expression ',F,'/',N,': '],Msg),
1008		(ord_member_nonvar_chk(create_not_discharged_msg(MsgType),Options)
1009		-> (MsgType=silent -> true ; add_message(well_def_analyser,Msg,Expr,I)) % we create warning below
1010		; known_to_be_unsupported(F,N)
1011		-> add_warning(well_def_analyser,Msg,Expr,I)
1012		; wd_transparent(Expr)
1013		-> add_error(well_def_analyser,Msg,'transparent operator has no top-level WD condition',I)
1014		; (wd_like_conjunction(Expr,_,_,_) ; Expr=disjunct(_,_) ; Expr=if_predicate(_,_,_))
1015		-> add_error(well_def_analyser,Msg,'operator has no top-level WD condition',I)
1016		; add_internal_error(Msg,create_top_level_wd_po(Expr,T,I,_,Options,PO,Discharged))
1017		),
1018		inc_counter(unsupported),
1019		create_po(Hypotheses,b(unknown_truth_value(F),pred,[wd(Expr)]),I,Options,PO,Discharged).
1020
1021		% Note: % if wd_ignore_external_funs is true the WD POs will not be created
1022		% This may be ok for ASSERT, under the assumption that ProB will check those ASSERTS at runtime
1023		% In this way we can instrument a model with ASSERT_TRUE/ASSERT_EXPR and be sure that all WD issues will be detected
1024		create_wd_po_for_external_call('ASSERT_TRUE',[BOOL_EXPR,_ErrString],Infos,Hypotheses,Options,PO,Discharged) :-
1025		extract_assert_predicate(BOOL_EXPR,Pred),!,
1026		create_po(Hypotheses,Pred,Infos,Options,PO,Discharged).
1027		create_wd_po_for_external_call('ASSERT_EXPR',[BOOL_EXPR,_ErrString,_E],Infos,Hypotheses,Options,PO,Discharged) :-
1028		extract_assert_predicate(BOOL_EXPR,Pred),!,
1029		create_po(Hypotheses,Pred,Infos,Options,PO,Discharged).
1030		create_wd_po_for_external_call(C,_Args,Infos,Hypotheses,Options,PO,Discharged) :- !,
1031		create_po(Hypotheses,b(unknown_truth_value(C),pred,[]),Infos,Options,PO,Discharged).
1032
1033		skip_finite_pos(Options) :-
1034		(get_preference(wd_skip_finite_pos,true) -> true
1035		; ord_member(skip_finite_po, Options)).
1036
1037		known_to_be_unsupported(freetype_destructor,3). % has WD condition, see check_freetype_case in b_interpreter
1038		known_to_be_unsupported(lazy_let_expr,3).
1039		known_to_be_unsupported(lazy_let_pred,3).
1040		known_to_be_unsupported(lazy_let_subst,3).
1041		known_to_be_unsupported(quantified_intersection,3).
1042
1043		create_partial_fun_target(A,Target) :-
1044		% see create_function_check in bvisual2
1045		get_texpr_type(A,TA), is_set_type(TA,couple(TDom,TRan)),
1046		create_type_set(TDom,TDT), % we could also use create_maximal_type_set/2
1047		create_type_set(TRan,TRT),
1048		safe_create_texpr(partial_function(TDT,TRT),set(TA),[],PF),
1049		safe_create_texpr(member(A,PF),pred,[],Target).
1050
1051		:- use_module(probsrc(bsyntaxtree),[is_set_type/2]).
1052		% get texpr for set of all sequences:
1053		create_seq_type_expr(Seq,Sequences) :-
1054		get_texpr_type(Seq,ST),
1055		is_set_type(ST,couple(_,TRan)),
1056		create_type_set(TRan,TRT),
1057		safe_create_texpr(seq(TRT),set(ST),[],Sequences).
1058		create_seq1_type_expr(Seq,Sequences) :-
1059		get_texpr_type(Seq,ST),
1060		is_set_type(ST,couple(_,TRan)),
1061		create_type_set(TRan,TRT),
1062		safe_create_texpr(seq1(TRT),set(ST),[],Sequences).
1063		create_seq_seq_type_expr(SeqSeq,SequencesOfSequences) :-
1064		get_texpr_type(SeqSeq,SST),
1065		is_set_type(SST,couple(_,SeqT)), % SeqT = type of the inner sequences
1066		is_set_type(SeqT,couple(_,TRan)), % TRan is type elements in the inner sequence
1067		create_type_set(TRan,TRT1),
1068		safe_create_texpr(seq(TRT1),set(SeqT),[],Sequences),
1069		safe_create_texpr(seq(Sequences),set(SST),[],SequencesOfSequences).
1070
1071		create_type_set(boolean,Res) :- !, Res=b(bool_set,set(boolean),[]). % custom rule not necessary
1072		create_type_set(integer,Res) :- !, Res=b(integer_set('INTEGER'),set(integer),[]).
1073		create_type_set(string,Res) :- !, Res=b(string_set,set(string),[]).
1074		create_type_set(Type,Res) :- create_texpr(typeset,set(Type),[],Res).
1075
1076		create_sequence_target(S,Target) :-
1077		create_seq_type_expr(S,Sequences),
1078		extract_pos_infos(S,PosInfos),
1079		safe_create_texpr(member(S,Sequences),pred,PosInfos,Target).
1080		create_sequence1_target(S,Target) :-
1081		create_seq1_type_expr(S,Sequences),
1082		extract_pos_infos(S,PosInfos),
1083		safe_create_texpr(member(S,Sequences),pred,PosInfos,Target).
1084		create_seq_seq_target(S,Target) :-
1085		create_seq_seq_type_expr(S,SeqSeq),
1086		extract_pos_infos(S,PosInfos),
1087		safe_create_texpr(member(S,SeqSeq),pred,PosInfos,Target).
1088
1089		create_seq_interval_target(S,N,Target) :-
1090		create_texpr(integer(0),integer,[],Zero),
1091		safe_create_texpr(size(S),integer,[contains_wd_condition],MaxIdx),
1092		safe_create_texpr(interval(Zero,MaxIdx),set(integer),[],ValidIdxs),
1093		safe_create_texpr(member(N,ValidIdxs),pred,[],Target).
1094
1095		% compute WD of a conjunction/sequence of formulas
1096		list_compute_wd([A|_],Options,Hyps,PO) :-
1097	?	compute_wd(A,Hyps,Options,PO).
1098		list_compute_wd([A|T],Options,Hyps,PO) :- T \= [],
1099		push_hyp(Hyps,A,Options,Hyps2),
1100	?	list_compute_wd(T,Options,Hyps2,PO).
1101
1102		% compute WD of a list of independent formulas
1103		%list_indep_compute_wd([A|T],Options,Hyps,PO) :-
1104		% (compute_wd(A,Hyps,Options,PO)
1105		% ;
1106		% list_indep_compute_wd(T,Options,Hyps,PO)).
1107
1108		% compute WD of a list of IF-THEN-ELSE cases:
1109		list_compute_if_elsif_wd([b(if_elsif(A,Body),_,_) | T], Hyps,Options,PO) :-
1110		( is_truth(A) -> compute_wd(Body,Hyps,Options,PO)
1111	?	; ( compute_wd(A,Hyps,Options,PO)
1112		;
1113		push_hyp(Hyps,A,Options,NewHyp),
1114	?	compute_wd(Body,NewHyp,Options,PO)
1115		;
1116		T \= [],
1117		negate_hyp(A,NA),
1118		push_hyp(Hyps,NA,Options,NewHyp),
1119		list_compute_if_elsif_wd(T, NewHyp,Options,PO)
1120		)
1121		).
1122
1123		% compute WD of a conjunction/sequence of formulas
1124		sequence_compute_wd([A|_],Options,Hyps,PO) :-
1125	?	compute_wd(A,Hyps,Options,PO).
1126		sequence_compute_wd([A|T],Options,Hyps,PO) :- T \= [],
1127		update_hyp_for_sequence_lhs(Hyps,A,Options,Hyps2),
1128	?	sequence_compute_wd(T,Options,Hyps2,PO).
1129
1130		:- use_module(probsrc(b_read_write_info), [get_accessed_vars/4]).
1131		% update the hypotheses depending on effect of LHS of a sequential composition:
1132		update_hyp_for_sequence_lhs(Hyps,b(LHS,subst,_),Options,Hyps2) :-
1133		process_seq_lhs_aux(LHS,Hyps,Options,Hyps2),
1134		!.
1135		update_hyp_for_sequence_lhs(Hyps,TStmt,_Options,Hyps2) :-
1136		add_modified_vars_to_hyp(Hyps,TStmt,Hyps2).
1137		%add_message(well_def_analyser,'Uncovered substitution in sequential composition: ',TStmt,TStmt).
1138
1139		% add all modified vars as new hyp vars: new hypotheses and goals will thus refer to new version (like priming variables)
1140		add_modified_vars_to_hyp(Hyps,TLHS,Hyps2) :-
1141		(get_accessed_vars(TLHS,[],ModifiedVars,_Read) -> true
1142		; add_error(well_def_analyser,'Could not obtain modified vars:',TLHS,TLHS), ModifiedVars=[]
1143		),
1144		maplist(construct_typed_var(Hyps),ModifiedVars,TModVars),
1145		add_new_hyp_variables(Hyps,TModVars,Hyps2).
1146
1147		construct_typed_var(Hyps,ID,b(identifier(ID),Type,[])) :-
1148		(get_hyp_var_type(ID,Hyps,Type) -> true
1149		; add_internal_error('Unknown identifier in hyps:',ID), Type=any).
1150
1151		rename_expr(Hyps,Expr,RenExpr) :- get_renamed_expression(Expr,Hyps,RenExpr).
1152		:- use_module(probsrc(bsyntaxtree),[get_texpr_id/2]).
1153		construct_equal(TID,RenExpr, b(equal(TID,RenExpr),pred,[])) :- get_texpr_id(TID,_),!.
1154		construct_equal(_,_,b(truth,pred,[])). % TO DO: deal with more complex assignments f(i) := E -> f' = f <+ {i|->E}
1155
1156		process_seq_lhs_aux(assign_single_id(TID,Expr),Hyps,Options,Hyps2) :- !,
1157		get_renamed_expression(Expr,Hyps,RenExpr), % rename in old context; e.g., if we have x:=x+1
1158		add_new_hyp_variables(Hyps,[TID],Hyps1),
1159		get_renamed_expression(TID,Hyps1,RenTID),
1160		Eq = b(equal(RenTID,RenExpr),pred,[]), % print('Add: '), translate:print_bexpr(Eq),nl,
1161		push_hyps_wo_renaming(Hyps1,[Eq],Options,Hyps2). %, portray_hyps(Hyps2).
1162		process_seq_lhs_aux(assign(FTIDs,Exprs),Hyps,Options,Hyps2) :- !,
1163		maplist(rename_expr(Hyps),Exprs,RenExprs),% rename in old context; e.g., if we have x:=x+1
1164		maplist(get_assigned_ids,FTIDs,TIDs),
1165		add_new_hyp_variables(Hyps,TIDs,Hyps1),
1166		maplist(rename_expr(Hyps1),TIDs,RenTIDs),
1167		maplist(well_def_analyser:construct_equal,RenTIDs,RenExprs,Equalities),
1168		push_hyps_wo_renaming(Hyps1,Equalities,Options,Hyps2).
1169
1170		% get assigned ids for things like f(x) := E or r'f := E
1171		get_assigned_ids(b(Expr,_,_),TID) :- get_assigned_id(Expr,F), !,get_assigned_ids(F,TID).
1172		get_assigned_ids(TID,TID).
1173
1174		get_assigned_id(function(F,_),F).
1175		get_assigned_id(record_field(R,_),R).
1176
1177		% wd_like_conjunction(Construct,NewTypedVars,Conjunct1,Conjunct2)
1178		wd_like_conjunction(conjunct(A,B),[],A,B).
1179		wd_like_conjunction(implication(A,B),[],A,B).
1180		wd_like_conjunction(precondition(A,B),[],A,B).
1181		wd_like_conjunction(assertion(A,B),[],A,B).
1182		wd_like_conjunction(witness_then(A,B),[],A,B).
1183		wd_like_conjunction(select_when(A,B),[],A,B).
1184		wd_like_conjunction(assertion_expression(A,_Msg,B),[],A,B). % Note: this has associated WD condition
1185		wd_like_conjunction(any(Ids,A,B),Ids,A,B).
1186		wd_like_conjunction(forall(Ids,A,B),Ids,A,B).
1187		wd_like_conjunction(quantified_union(Ids,A,B),Ids,A,B). % rewritten
1188		wd_like_conjunction(let_predicate(Ids,E,P),Ids,A,P) :- construct_let_eq_pred(Ids,E,A).
1189		wd_like_conjunction(let_expression(Ids,E,P),Ids,A,P) :- construct_let_eq_pred(Ids,E,A).
1190		wd_like_conjunction(let(Ids,E,P),Ids,A,P) :- A=E. % this is already a predicate
1191
1192
1193		:- use_module(library(lists),[maplist/4,append/2]).
1194		construct_let_eq_pred(Ids,E,Pred) :-
1195		(ground(Pred)
1196		-> conjunction_to_list(Pred,Ps), % enable predicate to be used both ways
1197		maplist(deconstruct_eq,Ids,E,Ps)
1198		; maplist(construct_eq,Ids,E,Ps),
1199		conjunct_predicates(Ps,Pred)
1200		),!.
1201		construct_let_eq_pred(Ids,E,Pred) :- add_internal_error('Call failed: ',construct_let_eq_pred(Ids,E,Pred)),fail.
1202
1203		construct_eq(TID,E,EqPred) :- safe_create_texpr(equal(TID,E),pred,EqPred).
1204		deconstruct_eq(TID,E,b(equal(TID,E),pred,_)).
1205
1206		% The constructs which have no WD condition of their own; they just require checking the arguments:
1207		wd_transparent(truth).
1208		wd_transparent(falsity).
1209		wd_transparent(negation(_)).
1210		wd_transparent(equivalence(_,_)).
1211		wd_transparent(equal(_,_)).
1212		wd_transparent(not_equal(_,_)).
1213		wd_transparent(member(_,_)).
1214		wd_transparent(not_member(_,_)).
1215		wd_transparent(subset(_,_)).
1216		wd_transparent(subset_strict(_,_)).
1217		wd_transparent(not_subset(_,_)).
1218		wd_transparent(not_subset_strict(_,_)).
1219		wd_transparent(less_equal(_,_)).
1220		wd_transparent(less(_,_)).
1221		wd_transparent(less_equal_real(_,_)).
1222		wd_transparent(less_real(_,_)).
1223		wd_transparent(greater_equal(_,_)).
1224		wd_transparent(greater(_,_)).
1225		wd_transparent(finite(_)).
1226		wd_transparent(partition(_,_)).
1227		wd_transparent(value(_)).
1228		wd_transparent(boolean_true).
1229		wd_transparent(boolean_false).
1230		wd_transparent(max_int).
1231		wd_transparent(min_int).
1232		wd_transparent(empty_set).
1233		wd_transparent(bool_set).
1234		wd_transparent(float_set).
1235		wd_transparent(real_set).
1236		wd_transparent(string_set).
1237		wd_transparent(convert_bool(_)).
1238		wd_transparent(convert_int_ceiling(_)).
1239		wd_transparent(convert_int_floor(_)).
1240		wd_transparent(convert_real(_)).
1241		wd_transparent(add(_,_)).
1242		wd_transparent(add_real(_,_)).
1243		wd_transparent(minus(_,_)).
1244		wd_transparent(minus_real(_,_)).
1245		wd_transparent(minus_or_set_subtract(_,_)).
1246		wd_transparent(unary_minus(_)).
1247		wd_transparent(unary_minus_real(_)).
1248		wd_transparent(multiplication(_,_)).
1249		wd_transparent(multiplication_real(_,_)).
1250		wd_transparent(mult_or_cart(_,_)).
1251		wd_transparent(cartesian_product(_,_)).
1252		wd_transparent(successor).
1253		wd_transparent(predecessor).
1254		wd_transparent(couple(_,_)).
1255		wd_transparent(pow_subset(_)).
1256		wd_transparent(pow1_subset(_)).
1257		wd_transparent(fin_subset(_)).
1258		wd_transparent(fin1_subset(_)).
1259		wd_transparent(general_union(_)).
1260		wd_transparent(interval(_,_)).
1261		wd_transparent(union(_,_)).
1262		wd_transparent(intersection(_,_)).
1263		wd_transparent(set_subtraction(_,_)).
1264		wd_transparent(relations(_,_)).
1265		wd_transparent(identity(_)).
1266		wd_transparent(event_b_identity).
1267		wd_transparent(reverse(_)).
1268		wd_transparent(first_projection(_,_)).
1269		wd_transparent(first_of_pair(_)).
1270		wd_transparent(event_b_first_projection(_)).
1271		wd_transparent(event_b_first_projection_v2).
1272		wd_transparent(second_projection(_,_)).
1273		wd_transparent(event_b_second_projection(_)).
1274		wd_transparent(event_b_second_projection_v2).
1275		wd_transparent(second_of_pair(_)).
1276		wd_transparent(composition(_,_)).
1277		wd_transparent(ring(_,_)).
1278		wd_transparent(direct_product(_,_)).
1279		wd_transparent(parallel_product(_,_)).
1280		wd_transparent(trans_function(_)).
1281		wd_transparent(trans_relation(_)).
1282		%wd_transparent(iteration(_,_)). % has a WD condition on index of iteration
1283		wd_transparent(reflexive_closure(_)).
1284		wd_transparent(closure(_)).
1285		wd_transparent(domain(_)).
1286		wd_transparent(range(_)).
1287		wd_transparent(image(_,_)).
1288		wd_transparent(domain_restriction(_,_)).
1289		wd_transparent(domain_subtraction(_,_)).
1290		wd_transparent(range_restriction(_,_)).
1291		wd_transparent(range_subtraction(_,_)).
1292		wd_transparent(overwrite(_,_)).
1293		wd_transparent(partial_function(_,_)).
1294		wd_transparent(total_function(_,_)).
1295		wd_transparent(partial_injection(_,_)).
1296		wd_transparent(total_injection(_,_)).
1297		wd_transparent(partial_surjection(_,_)).
1298		wd_transparent(total_surjection(_,_)).
1299		wd_transparent(total_bijection(_,_)).
1300		wd_transparent(partial_bijection(_,_)).
1301		wd_transparent(total_relation(_,_)).
1302		wd_transparent(surjection_relation(_,_)).
1303		wd_transparent(total_surjection_relation(_,_)).
1304		wd_transparent(seq(_)).
1305		wd_transparent(seq1(_)).
1306		wd_transparent(iseq(_)).
1307		wd_transparent(iseq1(_)).
1308		wd_transparent(perm(_)).
1309		wd_transparent(empty_sequence).
1310		wd_transparent(identifier(_)).
1311		wd_transparent(lazy_lookup_expr(_)).
1312		wd_transparent(lazy_lookup_pred(_)).
1313		wd_transparent(integer(_)).
1314		wd_transparent(integer_set(_)).
1315		wd_transparent(real(_)).
1316		wd_transparent(string(_)).
1317		wd_transparent(set_extension(_)).
1318		wd_transparent(sequence_extension(_)).
1319		wd_transparent(struct(_)).
1320		wd_transparent(rec(_)).
1321		wd_transparent(record_field(_,_)).
1322		wd_transparent(typeset).
1323
1324		wd_transparent(external_function_call(F,_)) :- \+ external_fun_has_wd_condition(F).
1325		wd_transparent(external_pred_call(F,_)) :- \+ external_fun_has_wd_condition(F).
1326		wd_transparent(external_subst_call(F,_)) :- \+ external_fun_has_wd_condition(F).
1327
1328		wd_transparent(operation_call_in_expr(_,_)). % the operations will be checked for WD independently
1329		% PRE conditions are not part of WD checking
1330
1331		wd_transparent(freetype_set(_)).
1332		wd_transparent(freetype_constructor(_,_,_)).
1333		wd_transparent(freetype_case(_,_,_)). % predicate to check if we match a given case
1334
1335		% substitutions:
1336		wd_transparent(skip).
1337		wd_transparent(block(_)).
1338		wd_transparent(parallel(_)).
1339		wd_transparent(choice(_)).
1340		wd_transparent(assign(_,_)). % TO DO: f(X) := E ==> f := f <+ {X|->E}, etc,...
1341		wd_transparent(assign_single_id(_,_)).
1342		wd_transparent(select(_)).
1343		wd_transparent(select(_,_)). % TOD: Else only reached if all cases do not apply
1344		wd_transparent(becomes_element_of(_,_)). % in classical B we do not have to check set not empty?
1345		wd_transparent(becomes_such(_,_)). % in classical B we do not have to check satisfiability
1346		wd_transparent(operation_call(_,_,_)). % I.e., we do not see checking PRE condition checking as part of WD checking
1347		wd_transparent(var(_,_)).
1348
1349		wd_transparent(witness(_,_)).
1350
1351		% transparent with new quantified variables
1352		wd_transparent(comprehension_set(_,_)).
1353		wd_transparent(exists(_,_)). % WD must be proven universally for all subexpression
1354
1355
1356		/*
1357		Not yet covered:
1358
1359		syntaxelement(kodkod(PId,Ids), Ids,[],[Ids],PId, pred).
1360
1361		syntaxelement(operation_call_in_expr(Id,As), [Id|As], [], [As], [], expr).
1362
1363		% rewritten:
1364		syntaxelement(event_b_comprehension_set(Ids,E,P),[E,P|Ids], Ids,[Ids], [], expr/only_typecheck).
1365		syntaxelement(lambda(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).
1366
1367		syntaxelement(quantified_intersection(Ids,P,E), [P,E|Ids],Ids,[Ids], [], expr).
1368
1369
1370		TREE operations
1371
1372		syntaxelement(let_expression_global(Ids,As,Expr), Exprs, Ids, [Ids,As], [], expr) :- % version used by b_compiler
1373		append([Ids,As,[Expr]],Exprs).
1374		syntaxelement(lazy_let_expr(TID,A,Expr), Exprs, [TID], [[TID],[A]], [], expr) :-
1375		append([[TID],[A],[Expr]],Exprs).
1376		syntaxelement(lazy_let_pred(TID,A,Expr), Exprs, [TID], [[TID],[A]], [], pred) :-
1377		append([[TID],[A],[Expr]],Exprs).
1378		syntaxelement(lazy_let_subst(TID,A,Expr), Exprs, [TID], [[TID],[A]], [], subst) :-
1379		append([[TID],[A],[Expr]],Exprs).
1380
1381		syntaxelement(compaction(A), [A], [], [], [], expr).
1382		syntaxelement(mu(A), [A], [], [], [], expr).
1383		syntaxelement(bag_items(A), [A], [], [], [], expr).
1384
1385		syntaxelement(freetype_set(Id), [], [], [], Id, expr).
1386		syntaxelement(freetype_case(Type,Case,Expr), [Expr], [], [], [Type,Case], pred).
1387		syntaxelement(freetype_constructor(Type,Case,Expr), [Expr], [], [], [Type,Case], expr).
1388		syntaxelement(freetype_destructor(Type,Case,Expr), [Expr], [], [], [Type,Case], expr).
1389
1390		rlevent(Name,Section,_Status,_Params,Guard,_Theorems,_Actions,_VWitnesses,_PWitnesses,_Unmod,_AbstractEvents),
1391
1392
1393
1394		seval /Users/leuschel/git_root/private_examples/ClearSy/2020/03_Mar/wd_timeout/invalidRef_welldef.mch
1395		:wd
1396		Analysis walltime: 183 ms
1397
1398		Stats: [AXM/1084,THM/104,unsupported/7,not_discharged_po/545,discharged_po/704,caval__rule__1__compute/61]
1399		Stats: [unsupported/2,AXM/1085,THM/104,not_discharged_po/542,discharged_po/708,caval__rule__1__compute/61]
1400
1401		Analysis walltime: 31 ms
1402		Stats: [AXM/1085,THM/104,not_discharged_po/542,discharged_po/708,caval__rule__1__compute/61]
1403		when reordering and not ignoring infos:
1404		Analysis walltime: 17 ms
1405		Stats: [AXM/1085,THM/104,not_discharged_po/540,discharged_po/710,caval__rule__1__compute/61]
1406
1407		Tests:
1408
1409		:wd a>0 & x>0 & x:1..10 & f:1..10-->INTEGER & f(x)=2 & x>1
1410		:wd %x.(x:2..4 | %x.(x:4..8|10/x)(2*x)) = x
1411
1412		:wd x:NATURAL1 & y>=x & x mod y = x/y
1413		-> same PO generated twice
1414
1415		:wd f6 = %x.(x>10 & x<20|100) & res=f6(11)
1416		:wd i5 = %x.(x>10|100+x) & i5(100) = 200
1417		seval /Users/leuschel/git_root/prob_examples/examples/B/ASTD/wetransfer-545a33/Case_Study_Handmade/TRAIN_CONTROL_M6.mch
1418
1419		:wd n:NATURAL & a:1..n --> 1..10 & a /= {} & a(1)=1
1420
1421		-> support for $0 missing
1422		-> support for ; and while (adding condition and invariant to loop body hyps) for transform
1423		-> support for operation all in expression
1424		-> Parallel in classical B: we could propagate guards from first to second subst; CarlaTravelAgency; but Atelier-B considers this to be not well-defined; each parallel construct should be WD on its own; we should make no assumption about order
1425		-> CASE statement: treat cases specially
1426
1427		% Processing file 2/3: /Users/leuschel/git_root/private_examples/ClearSy/2020/01_Jan/logxml_system_error/rule.mch
1428		Proof of AXM took 169 ms, result=discharged ...
1429		*/
1430
1431		% ---------------------------------
1432		% Annotating operations so that we can discharge WD conditions statically
1433
1434		% this can be called once for all operations: it gets the hypotheses that are available for (all) operations
1435		get_hyps_for_top_level_operations(Options,Hyps) :-
1436		push_properties_invariant_hyps(Options,Hyps).
1437
1438		:- public transform_machine_operation/7.
1439
1440		% should call get_hyps_for_top_level_operations
1441		% Note: should be run after global types are pre-compiled; otherwise we do not detect global constants
1442		% TODO: pre-compile global sets before computing operations?
1443		transform_machine_operation(OpName,OpResults,OpFormalParameters,Body,Hyps,Options,NewBody) :-
1444		PO_Name = OpName,
1445		format('Checking WD of OPERATION ~w~n',[OpName]),
1446		ord_add_element(Options,po_label(PO_Name),Opt1),
1447		add_new_hyp_variables(Hyps,OpFormalParameters,Hyps6),
1448		add_new_hyp_variables(Hyps6,OpResults,Hyps7),
1449		ord_add_element(Opt1,discharge_po,Opt2),
1450		ord_add_element(Opt2,reorder_conjuncts,Opt3),
1451		transform_wd(Body,Hyps7,Opt3,NewBody),
1452		print_wd_subst(NewBody).
1453
1454		print_wd_subst(NewTExpr) :-
1455		temporary_set_preference(pp_wd_infos,true,Chng),
1456		translate:print_subst(NewTExpr),nl,
1457		reset_temporary_preference(pp_wd_infos,Chng).
1458
1459		push_properties_invariant_hyps(Options,Hyps4) :-
1460		b_get_properties_from_machine(Properties),
1461		empty_hyps(E),
1462		b_get_machine_all_constants(Csts),
1463		add_new_hyp_variables(E,Csts,OriginalHyps),
1464		push_hyp(OriginalHyps,Properties,Options,Hyps1),
1465		b_get_static_assertions_from_machine(StaticAssertions),
1466		push_hyps(Hyps1,StaticAssertions,Options,Hyps2),
1467		b_get_machine_variables(Vars),
1468		add_new_hyp_variables(Hyps2,Vars,Hyps3),
1469		b_get_invariant_from_machine(Invariant),
1470		push_hyp(Hyps3,Invariant,Options,Hyps4).
1471
1472		% ---------------------------------
1473
1474		:- use_module(probsrc(bsyntaxtree), [def_get_texpr_ids/2]).
1475		:- use_module(probsrc(btypechecker),[prime_identifiers/2]).
1476		:- use_module(extrasrc(before_after_predicates),[prime_bexpr_for_ids/4,
1477		before_after_predicate_for_operation_no_equalities/5]).
1478		% try and prove invariant preservation using BA predicate
1479		prove_invariant_preservation(OpName,TargetInv,Proven,Options) :-
1480		push_properties_invariant_hyps(Options,Hyps),
1481		b_get_invariant_from_machine(Invariant),
1482		conjunction_to_list(Invariant,Invs),
1483		before_after_predicate_for_operation_no_equalities(OpName,Paras,Results,BAPred,TChangedIds),
1484		add_new_hyp_variables(Hyps,Paras,Hyps1),
1485		add_new_hyp_variables(Hyps1,Results,Hyps2),
1486		prime_identifiers(TChangedIds,NewPrimedIds),
1487		add_new_hyp_variables(Hyps2,NewPrimedIds,Hyps3),
1488		push_hyp(Hyps3,BAPred,Options,Hyps4),
1489		formatsilent('~nProving invariant preservation for operation ~w~n',[OpName]),
1490		(silent_mode(on) -> true ; translate:print_bexpr(BAPred),nl),
1491		member(TargetInv,Invs),
1492		def_get_texpr_ids(TChangedIds,ChangedIds),
1493		prime_bexpr_for_ids(TargetInv,ChangedIds,PrimedTargetInv,ChangesPerformed),
1494		(ChangesPerformed=false
1495		-> Proven=unchanged % Invariant unaffected by event
1496		; prove_sequent_goal(PrimedTargetInv,Hyps4,Options)
1497		-> Proven=proven
1498		; Proven=unproven),
1499		(silent_mode(on) -> true
1500		; format(' ~w => ',[Proven]), translate:print_bexpr(PrimedTargetInv),nl).
1501
1502		% well_def_analyser:prove_invariant_preservation(OpName,Target,Proven),fail.
1503
1504		:- use_module(probsrc(tools_lists),[count_occurences/2]).
1505
1506		analyse_invariants_for_machine(UnchangedNr,ProvenNr,UnProvenNr,TotPOsNr,Options) :-
1507		findall(Proven,prove_invariant_preservation(_Op,_,Proven,Options),Ls),
1508		count_occurences(Ls,Res),
1509		(member(proven-ProvenNr,Res) -> true ; ProvenNr=0),
1510		(member(unchanged-UnchangedNr,Res) -> true ; UnchangedNr=0),
1511		(member(unproven-UnProvenNr,Res) -> true ; UnProvenNr=0),
1512		TotPOsNr is UnchangedNr + ProvenNr + UnProvenNr.
1513
1514		% TODO: look at weakest_precondition/3: no need to prime?
1515
1516		% ---------------------------------
1517
1518
1519		%% toplevel_wd_pos(Predicate, Hypotheses, ProofObligations).
1520		%
1521		% Returns a list of proof obligations for the given Ast, but only those relevant
1522		% for the root node.
1523		toplevel_wd_pos(b(Node, _, _), _, []) :-
1524		wd_transparent(Node), !.
1525		toplevel_wd_pos(b(Node, Type, Info), Hyps, WDPOs) :-
1526		wd_like_conjunction(Node, _, _, _), !,
1527		findall(PO, create_top_level_wd_po_conj_like(Node, Type, Info, Hyps, [discharge_po], PO, _), WDPOs).
1528		toplevel_wd_pos(b(Node, Type, Info), Hyps, WDPOs) :-
1529	?	has_top_level_wd_condition(Node), !,
1530		findall(PO, create_top_level_wd_po(Node, Type, Info, Hyps, [discharge_po], PO, _), WDPOs).
1531		toplevel_wd_pos(_, _, []).
1532