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