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