1		% (c) 2013-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(disprover, [disprove/5, disprove_with_opts/6, get_disprover_default_opts/1,
6		print_prover_result_stats/0]).
7
8		:- use_module(probsrc(module_information)).
9		:- module_info(group,cbc).
10		:- module_info(description,'Rodin Prover / Disprover').
11
12		% provide access to the Disprover algorithm with all hypotheses, selected hypotheses and goal
13
14		:- use_module(extension('user_signal/user_signal'), [user_interruptable_call_det/2]).
15
16		:- use_module(probsrc(solver_interface), [solve_predicate/5,type_check_in_machine_context/2]).
17		:- use_module(probsrc(preferences), [temporary_set_preference/3, reset_temporary_preference/2,
18		get_preference/2]).
19		:- use_module(probsrc(bsyntaxtree), [conjunct_predicates/2, create_negation/2,
20		find_typed_identifier_uses/3,
21		find_typed_identifier_uses_l/3,
22		get_texpr_types/2]).
23		:- use_module(probsrc(error_manager), [reset_errors/0, add_message/3,
24		add_warning/3, add_internal_error/2, add_error_and_fail/2]).
25		:- use_module(library(lists)).
26		:- use_module(probsrc(tools),[start_ms_timer/1, stop_ms_timer/1,stop_ms_timer_with_debug_msg/2,
27		get_elapsed_timer/2, combiner_timer/3]).
28		:- use_module(probsrc(debug), [debug_println/2,debug_mode/1, debug_format/3]).
29		:- use_module(probsrc(b_global_sets),[contains_unfixed_deferred_set/1]).
30		:- use_module(probsrc(external_functions),[observe_state/1]).
31		:- use_module(extrasrc(unsat_cores),[unsat_core/2]).
32		:- use_module(probsrc(pathes_lib), [unavailable_extension/2]).
33
34		disprove(Goal,AllHypotheses,SelectedHypotheses,Timeout,OutResult) :-
35		get_disprover_default_opts(Opts),
36		% Note: disprover_mode is always set to true
37		disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,Timeout,Opts,OutResult).
38
39		get_disprover_default_opts(Opts) :-
40		(unavailable_extension(chr_extension,_Reason)
41		-> CHR=false, format('Disabling CHR in disprover as extension not available~n',[]) ; CHR=true),
42		% default options:
43		Opts = [use_smt_mode/true,use_clpfd_solver/true,use_chr_solver/CHR].
44
45		% ----------
46
47		disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,Timeout,Opts,OutResult) :-
48		check_options(Opts),
49		temporary_set_preference(disprover_mode,true,DC),
50		temporary_set_preference(time_out,Timeout,TC),
51		start_ms_timer(Timer),
52		user_interruptable_call_det(disprove1(Goal,AllHypotheses,SelectedHypotheses,Opts,Result),InterruptResult),
53		%write(ir(InterruptResult)), nl,
54		(InterruptResult = interrupted -> OutResult = interrupted ; OutResult = Result),
55		%catch_internal_timeout(InterruptResult,Result,OutResult),
56		(debug_mode(on) -> write(disprove_result(OutResult)),nl,stop_ms_timer(Timer),nl ; true),
57		reset_temporary_preference(disprover_mode,DC),
58		reset_temporary_preference(time_out,TC).
59
60		check_options([]) :- !.
61	?	check_options([O|T]) :- !, (valid_option(O) -> true ; add_warning(disprover,'Illegal disprover option: ',O)),
62		check_options(T).
63		check_options(O) :- add_internal_error('Illegal disprover options: ',check_options(O)).
64
65		:- use_module(probsrc(solver_interface), [valid_solver_option/1]).
66		% Valid options
67		valid_option(disprover_option(X)) :- !,valid_disprover_option(X).
68	?	valid_option(X) :- valid_solver_option(X).
69
70		valid_disprover_option(observe_state).
71		valid_disprover_option(unsat_core).
72		valid_disprover_option(unsat_core_as_machine).
73		valid_disprover_option(export_po_as_machine(_)).
74		valid_disprover_option(setlog_prover_timeout(_)).
75		valid_disprover_option(wd_prover_timeout(_)).
76		valid_disprover_option(po_label(_)).
77
78		% ----------
79
80		:- use_module(probsrc(error_manager),[add_all_perrors/3]).
81		disprove1(Goal,AllHypotheses,SelectedHypotheses,Opts,Result) :-
82		catch(
83		(disprove2(Goal,AllHypotheses,SelectedHypotheses,Opts,Result) -> true
84		; add_internal_error('Disprover failed on goal:',Goal),
85		fail),
86		type_errors(E),
87		(add_all_perrors(E,[],disprover), Result=type_error)).
88
89		%catch_internal_timeout(ok,contradiction_found,Out) :-
90		% error_manager:check_warning_occured(warning(_X),Y),
91		% is_time_out_message(Y), % Sebastian: why do we catch this ?? This is not necessarily a problem ??
92		% !, % Might be a problem for proofs, invalidate only if Result = contradiction_found
93		% Out = time_out. % However, this might be old code that is superseded by the enum warnings
94		%catch_internal_timeout(ok,Result,Result).
95
96		% is_time_out_message(Y) :- atom(Y), atom_codes(Y,Codes),
97		% append("TIME-OUT occurred while ProB was expanding", _, Codes).
98
99		% ProverContext: just a name for statistics
100		solve_disprover_predicate(ProverContext,Predicate,Opts,CBCResult) :-
101		TimeoutFactor = 1,
102		exclude(disprover_option,Opts,SOpts),
103		(member(disprover_option(observe_state),Opts) -> observe_state(State) ; true),
104		start_ms_timer(Timer),
105		(solve_predicate(Predicate,State,TimeoutFactor,SOpts,CBCResult)
106		-> register_prover_result(ProverContext,CBCResult,Timer)
107		; register_prover_result(ProverContext,failed,Timer),
108		fail
109		).
110		disprover_option(disprover_option(_)).
111
112
113		:- use_module(wdsrc(well_def_analyser),[prove_sequent/4]).
114		:- use_module(probsrc(tools_meta),[safe_time_out/3]).
115		:- use_module(extrasrc(b2setlog),[prove_using_setlog/5]).
116		prove_using_alternative_prover(setlog_prover,Goal,Hypotheses,Opts,TimeOutMs,Res) :-
117		start_ms_timer(Timer),
118		(prove_using_setlog(Goal,Hypotheses,Opts,TimeOutMs,Res)
119		-> (Res = contradiction_found
120		-> register_prover_result(setlog_prover,contradiction_found,Timer)
121		; register_prover_result(setlog_prover,Res,Timer),
122		fail
123		)
124		; register_prover_result(setlog_prover,failed,Timer),
125		fail
126		).
127		prove_using_alternative_prover(wd_prover,Goal,Hypotheses,Opts,TimeOutMs,contradiction_found) :-
128		% quite often 0 or 1 ms are enough for TimeOutMs
129	?	(member(disprover_option(po_label(Label)),Opts) -> WDOpts=[po_label(Label)] ; WDOpts=[]),
130		debug_format(19,'Starting WD Prover (timeout ~w ms) for \'~w\' ~n',[TimeOutMs,Label]),
131		start_ms_timer(Timer),
132		(safe_time_out(prove_sequent(proving,Goal,Hypotheses,WDOpts),TimeOutMs,TimeOutRes)
133		-> (TimeOutRes=time_out
134		-> format('Timeout in WD Prover (~w ms)~n',[TimeOutMs]),
135		register_prover_result(wd_prover,time_out,Timer), fail
136		; register_prover_result(wd_prover,contradiction_found,Timer))
137		; register_prover_result(wd_prover,failed,Timer),
138		fail
139		).
140
141
142		:- dynamic prover_stats/4.
143
144		% register the result of a prover for statistics / user feedback
145		register_prover_result(Prover,Result,Timer) :-
146		functor(Result,RF,_),
147		(retract(prover_stats(Prover,RF,PrevNr,PrevTime)) -> true ; PrevNr=0, PrevTime=0),
148		NewNr is PrevNr+1,
149		get_elapsed_timer(Timer,DeltaTimer),
150		combiner_timer(PrevTime,DeltaTimer,NewTimer),
151		assert(prover_stats(Prover,RF,NewNr,NewTimer)),
152		stop_ms_timer_with_debug_msg(Timer,prover_result(Prover,RF)).
153
154		print_prover_result_stats :-
155		\+ \+ prover_stats(_,_,_,_), % at least one call made
156		format('* Disprover statistics about individual prover calls and results:~n',[]),
157		format('~w,~w,~w,~w,~w,~w~n',['Prover','Result','Calls','Runtime','TotRuntime','Walltime']),
158		prover_stats(Prover,Result,Nr,timer(Runtime,TotRuntime,Walltime)),
159		format('~w,~w,~w,~w,~w,~w~n',[Prover,Result,Nr,Runtime,TotRuntime,Walltime]),
160		fail.
161		print_prover_result_stats.
162
163		:- public disprove2/5. % it is called by user_interruptable_call_det above; we should also add a meta_predicate annotation
164		:- use_module(probsrc(bsyntaxtree), [predicate_identifiers/2]).
165		disprove2(Goal,AllHypotheses,SelectedHypotheses,Opts,ResultOut) :-
166		(type_check_in_machine_context([Goal|AllHypotheses],[TGoal|TAllHypotheses]) -> true
167		; add_error_and_fail(disprover,'Disprover typechecking goal failed')),
168		(type_check_in_machine_context(SelectedHypotheses,TSelectedHypotheses) -> true
169		; add_error_and_fail(disprover,'Disprover typechecking selected hyps failed')),
170	?	disprove3(TGoal,TAllHypotheses,TSelectedHypotheses,Opts,ResultOut).
171
172
173		disprove3(TGoal,TAllHypotheses,TSelectedHypotheses,Opts,ResultOut) :-
174		% build predicate H1 & H2 .... & not Goal
175		create_negation(TGoal,NegatedGoal),
176		%(debug_mode(on) -> write(NegatedGoal), nl ; true),
177		(debug_mode(on) -> nl,write('Negated Goal:'), nl,
178		translate:nested_print_bexpr_as_classicalb(NegatedGoal),
179		write_hypothesis(TAllHypotheses)
180		; true),
181		conjunct_predicates([NegatedGoal|TAllHypotheses],Predicate),
182		%tools:print_bt_message(solving),
183		ProofInfos = [disprover_result(final,all_and_selected,ResultOut),options(Opts)|PI1],
184		( get_alternate_prover_timeout(Opts,Prover,Timeout),
185		Timeout>0,
186		prove_using_alternative_prover(Prover,TGoal,TAllHypotheses,Opts,Timeout,ResultWithAll)
187		% adds 5 extra PO proven in test 1800, and 4 more in test 1447
188		-> % DISCHARGED by WD Prover
189		(debug_mode(on) -> add_message(disprover,'Discharged by alternate prover: ',Prover:Timeout) ; true),
190		PI1 = [disprover_result(Prover,all,ResultWithAll)|PI2]
191		; solve_disprover_predicate(prob_all_hyps,Predicate,Opts,ResultWithAll),
192		PI1 = [disprover_result(prob,all,ResultWithAll)|PI2]
193		),
194		%tools:print_bt_message(solver_result(CBCResult)),
195		debug_println(10,disprover_result_with_all_hypotheses(ResultWithAll)),
196	?	disprove_double_check(ResultWithAll,NegatedGoal,TAllHypotheses,TSelectedHypotheses,Predicate,Opts,ResultOut,PI2),
197	?	(member(disprover_option(export_po_as_machine(File)),Opts)
198		-> export_po_as_machine(File,TAllHypotheses,TSelectedHypotheses,TGoal,ProofInfos)
199		; true).
200
201		get_alternate_prover_timeout(Opts,Prover,Timeout) :-
202		member(disprover_option(setlog_prover_timeout(TO)),Opts),!,
203		(Prover=wd_prover,member(disprover_option(wd_prover_timeout(Timeout)),Opts) % try WD prover first
204		;
205		Prover=setlog_prover, TO=Timeout).
206		get_alternate_prover_timeout(Opts,wd_prover,Timeout) :-
207		member(disprover_option(wd_prover_timeout(Timeout)),Opts),!.
208		get_alternate_prover_timeout(_,wd_prover,WDTimeout) :-
209		get_preference(time_out,GlobalTO),
210		WDTimeout is 20 + GlobalTO // 100.
211
212		% res <— solve( All Hyp & not G )
213		% if res = solution then
214		% return CounterExample Found, Goal definitely not provable
215		% else if unfixed deferred set used in selected Hypotheses or Goal then
216		% return Unknown // WE COULD TRY and find counter example here in case there was a time-out?
217		% else if res = fail (without time-out & without enumeration warning & no unfixed deferred set in All Hypotheses) then
218		% return Proof Found, Goal proven
219		% else
220		% res <— solve (Selected Hyp & not G) /* maybe use smaller time-out here ?? */
221		% if res = fail (without time-out & without enumeration warning) then
222		% return Proof Found, Goal proven
223		% else if res = solution then
224		% return CounterExample for selected Hypotheses found, Goal not provable from selected Hypotheses (but may be provable with all Hyp)
225		% else
226		% return Unknown
227		% fi
228		% fi
229
230		% we found a solution / counter example to all hyps no need to double check here.
231		% just clear up the resulting state, keeping only variables occuring in the goal.
232		% although: sometimes it is useful to have other IDs as well, at least in the same component as the Goal !
233		disprove_double_check(solution(X),NegatedGoal,_Hypotheses,_SelectedHypotheses,_,_,ResultOut,ProofInfos) :-
234		predicate_identifiers(NegatedGoal,GoalIdentifiers),
235		findall(binding(Id,Value,PP), get_binding_from_solution(X,GoalIdentifiers,0,Id,Value,PP), FilteredState),
236		ResultOut = solution(FilteredState),
237		ProofInfos = ['Counter example to all hypotheses found'].
238		% check if the unfixed deferred sets occur in selected hyps or goal
239		disprove_double_check(no_solution_found(unfixed_deferred_sets),NegatedGoal,_Hypotheses,SelectedHypotheses,_,_,
240		no_solution_found(unfixed_deferred_sets),ProofInfos) :-
241		find_typed_identifier_uses(NegatedGoal,[],GoalIdentifiers),
242		get_texpr_types(GoalIdentifiers,GoalTypes),
243		find_typed_identifier_uses_l(SelectedHypotheses,[],HypIdentifiers),
244		get_texpr_types(HypIdentifiers,HypTypes),
245		append(GoalTypes,HypTypes,Types),
246		% exclude all types that are not unfixed
247		include(contains_unfixed_deferred_set,Types,UnfixedTypes),
248		% see if an unfixed type is left
249		UnfixedTypes = [_|_],
250		!,
251		ProofInfos = ['Goal or selected hypotheses contain unfixed deferred sets', unfixed(UnfixedTypes)],
252		!.
253		% contradiction was found, i.e. there was neither a timeout nor an enumeration warning
254		disprove_double_check(contradiction_found,NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,
255		FinalResult,ProofInfos) :-
256		ProofInfos = ['PO is proven using all hypotheses, no timeout or enumeration warning occured'],
257		%add_hit(po_discharged,prob_all),
258		(get_preference(double_evaluation_when_analysing,true)
259		-> check_negated(NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,FinalResult)
260		; FinalResult = contradiction_found).
261		disprove_double_check(Result,_NegatedGoal,Hypotheses,SelectedHypotheses,_,_Opts,ResultOut,ProofInfos) :-
262		same_conjunction_list(Hypotheses,SelectedHypotheses),!,
263		ProofInfos = ['Selected hypotheses identical to all hypotheses'],
264		Result=ResultOut.
265		% see what solving only selected hypotheses & not G gives us
266		disprove_double_check(_OldResult,NegatedGoal,Hypotheses,SelectedHypotheses,_,Opts,ResultOut,ProofInfos) :-
267		% No proof found with all hypotheses, now try selected ones only
268		% reset existing enumeration warnings,
269		% that might have been generated in a previous run
270		reset_errors,
271		(debug_mode(on)
272		-> nl,write('Trying to use only selected hypotheses.\nNegated Goal:'), nl,
273		translate:nested_print_bexpr_as_classicalb(NegatedGoal),
274		write_hypothesis(SelectedHypotheses)
275		; true),
276		conjunct_predicates([NegatedGoal|SelectedHypotheses],Predicate),
277		%external_functions:observe_state(State),
278		solve_disprover_predicate(prob_selected_hyps,Predicate,Opts,Result),
279		ProofInfos = [disprover_result(prob,selected,Result)],
280		!,
281		disprove_triple_check(Result,NegatedGoal,Hypotheses,SelectedHypotheses,Predicate,Opts,ResultOut).
282
283
284		% we still have a contradiction -> double check it if preference set
285		disprove_triple_check(contradiction_found,NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,FinalResult) :-
286		%add_hit(po_discharged,prob_selected),
287		(get_preference(double_evaluation_when_analysing,true) % preference set by Rodin Disprover
288		-> check_negated(NegatedGoal,Hypotheses,SelectedHypotheses,FullPredicate,Opts,FinalResult)
289		; FinalResult = contradiction_found,
290		compute_unsat_core_if_requested(FullPredicate,Opts)
291		).
292		disprove_triple_check(solution(X),NegatedGoal,_,_,_FullPredicate,_,ResultOut) :-
293		% Counter-Example to Goal for selected Hypotheses found
294		predicate_identifiers(NegatedGoal,GoalIdentifiers),
295		findall(binding(Id,Value,PP), get_binding_from_solution(X,GoalIdentifiers,10,Id,Value,PP), FilteredState),
296		ResultOut = solution_on_selected_hypotheses(FilteredState).
297		disprove_triple_check(time_out,_,_,_,_,_,time_out). % TODO: We could try Kodkod here!
298		disprove_triple_check(no_solution_found(X),_,_,_,_,_,no_solution_found(X)). % Or here?
299
300		:- use_module(library(ordsets),[ord_member/2]).
301		% get bindings from solution; showing all identifiers from goal and a few others as indicated by MaxIndexNonGoal
302		get_binding_from_solution(Solution,GoalIdentifiers,MaxIndexNonGoal,Id,Value,PP) :- MaxIndexNonGoal>=0,
303		sort(GoalIdentifiers,SG),
304	?	nth1(Nr,Solution,binding(Id,Value,PP)),
305		(Nr =< MaxIndexNonGoal -> true ; ord_member(Id,SG)).
306		% TO DO: rather than limiting this way, we could analyse the variables which are in the same component
307		% either by calling predicate_components or by storing component info in
308
309		check_negated(NegatedGoal,Hypotheses,_,FullOrigPredicate,Opts,ResultOut) :-
310		create_negation(NegatedGoal,Goal),
311		conjunct_predicates([Goal|Hypotheses],Predicate),
312		%tools:print_bt_message(check_negated),
313		debug_println(20,'Check whether we can also prove negation of goal'),
314		solve_disprover_predicate(prob_check_negated_goal,Predicate,Opts,Result),
315		%% tools:print_bt_message(solver_double_check_result(Result)),
316		!,
317		(Result = contradiction_found % proven both (H & not G) and (H & G)
318		-> ResultOut = contradiction_in_hypotheses,
319		translate:translate_bexpression_with_limit(NegatedGoal,GS),
320		add_warning(disprover_inconsistent_hypotheses,
321		'Disprover double check result: Contradiction in hypotheses (or Bug) detected for goal: ',
322		GS), %% check_negated(NegatedGoal,Hypotheses))
323		% translate:nested_print_bexpr_as_classicalb(Hypotheses),nl,nl,
324		compute_unsat_core_if_requested(Predicate,Opts)
325		% ; Result=solution(Bindings), format('Solution for negated goal:~n',[]), member(B,Bindings), print_binding(B),fail
326		; ResultOut = contradiction_found,
327		compute_unsat_core_if_requested(FullOrigPredicate,Opts)
328		).
329
330		%print_binding(binding(Var,_,PPV)) :- format(' ~w = ~w~n',[Var,PPV]).
331
332		compute_unsat_core_if_requested(Predicate,Opts) :-
333		(member(disprover_option(unsat_core),Opts) -> compute_unsat_core(Opts,Predicate) ; true).
334		:- use_module(probsrc(preferences),[call_with_preference/3]).
335		:- use_module(probsrc(translate),[translate_predicate_into_machine/3,nested_print_bexpr_as_classicalb/1]).
336		compute_unsat_core(Opts,Predicate) :-
337		(member(unsat_core_algorithm/P,Opts)
338		-> call_with_preference(compute_unsat_core_aux(Predicate,CorePredicate),unsat_core_algorithm,P)
339		; compute_unsat_core_aux(Predicate,CorePredicate)),
340		!,
341		print('UNSAT CORE: '),nl,print('--------'),nl,
342		(member(disprover_option(unsat_core_as_machine),Opts)
343		-> translate_predicate_into_machine(CorePredicate,'UnsatCore',ResultAtom),
344		write(ResultAtom),nl
345		; nested_print_bexpr_as_classicalb(CorePredicate)),
346		nl, print('--------'),nl.
347
348		compute_unsat_core_aux(Predicate,CorePredicate) :-
349		print('Computing UNSAT CORE'),nl,
350		unsat_core(Predicate,CorePredicate). % from unsat_cores
351
352		:- use_module(probsrc(bsyntaxtree),[same_texpr/2]).
353		% check if two lists of conjuncts represent the same conjunction (modulo info fields)
354		same_conjunction_list(List1,List2) :-
355		same_length(List1,List2,_), % avoid possibly expensive comparisons if lists clearly different
356		% we could strip info field and the sort; but here we just want to catch the obvious case where the disprover is called with SelectedHyp = AllHyp
357		maplist(same_texpr,List1,List2).
358
359		:- use_module(probsrc(translate),[nested_print_sequent_as_classicalb/6,nested_print_bexpr_as_classicalb/1]).
360		write_hypothesis([]).
361		write_hypothesis([Hyp|Hyps]) :-
362		write(' & /* Hypothesis: */ '), nl,
363		%(debug_mode(on) -> write(Hyp), nl ; true),
364		nested_print_bexpr_as_classicalb(Hyp),
365		write_hypothesis(Hyps).
366
367		:- use_module(probsrc(tools_io),[safe_intelligent_open_file/3]).
368		export_po_as_machine(Filename,THypothesesList,TSelectedHypothesesList,TGoal,Infos) :-
369		%nested_print_sequent_as_classicalb(Stream,THypothesesList,TGoal,'ProofObligation_AllHyps',Infos),
370		format(user_output,'Exporting selected hypotheses to B machine: ~w~n',[Filename]),
371		safe_intelligent_open_file(Filename,write,Stream),
372		nested_print_sequent_as_classicalb(Stream,TSelectedHypothesesList,TGoal,
373		THypothesesList,'ProofObligation_SelectedHyps',Infos),
374		close(Stream).
375