1		% (c) 2014-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_test_runner, [run_disprover_on_po/1, run_disprover_on_all_pos/1,
6		get_loaded_po_file/1, load_po_file/1,
7		set_disprover_timeout/1, reset_disprover_timeout/0,
8		get_disprover_options/1, set_disprover_options/1,
9		get_disprover_po/6, get_disprover_result/3,
10		print_disprover_stats/0]).
11
12		:- use_module(probsrc(prob_startup), [startup_prob/0]).
13		%:- use_module(pathes,[set_search_pathes/0]). % imported first to set_compile_time_search_pathes, now loaded by prob_startup
14
15		:- multifile user:portray_message/2.
16		user:portray_message(informational, _) :- !.
17
18		:- use_module(probsrc(module_information)).
19		:- module_info(group,cbc).
20		:- module_info(description,'Rodin Prover / Disprover').
21
22
23		:- use_module(disprover).
24		:- use_module(probsrc(error_manager)).
25		:- use_module(probsrc(tools)).
26		:- use_module(probsrc(debug)).
27
28		:- use_module(library(system)).
29		:- use_module(library(lists)).
30
31
32
33		%:- use_module(eventhandling, [announce_event/1]).
34
35		print_disprover_stats :-
36		(debug_mode(on) -> print_prover_result_stats ; true), % statistics about various provers
37		(disprover_timeout(TO) -> true ; TO = 'UNKNOWN'),
38		project_name(N), format('Project ~w~n',[N]),
39		generated(_,D),
40		machine_name(M), format('Machine ~w (exported ~w)~n',[M,D]),
41		print_nr_pos('',_,_),
42		print_nr_pos('proven (within Rodin) ',true,_),
43		format('ProB Disprover Analysis with timeout ~w ms:~n',[TO]),
44		print_nr_pos('proven (by ProB) ',_,true),
45		(disprover_result(_,_,contradiction_in_hypotheses)
46		-> print_nr_pos('those with contradiction in hypotheses ',_,true,contradiction_in_hypotheses) ; true),
47		print_nr_pos('disproven (by ProB) ',_,false),
48		print_nr_pos('unproven (by ProB) ',_,unknown),
49		(raw_result_exists(failure) -> print_nr_pos('failure (of ProB) ',_,failure) ; true).
50
51		raw_result_exists(RawResult) :- disprover_po_with_info(_,_,_,RawResult).
52		print_nr_pos(Msg,RodinStatus,ProBStatus) :- print_nr_pos(Msg,RodinStatus,ProBStatus,_).
53		print_nr_pos(Msg,RodinStatus,ProBStatus,RawResult) :-
54		findall(Name,disprover_po_with_info(Name,RodinStatus,ProBStatus,RawResult),L),
55		length(L,Len),
56		(Len<12
57		-> format(' Number of ~wPOs: ~w (~w)~n',[Msg,Len,L])
58		; (L = [First|_],last(L,Last))
59		-> format(' Number of ~wPOs: ~w (~w -- ~w)~n',[Msg,Len,First,Last])
60		; format(' Number of ~wPOs: ~w~n',[Msg,Len])
61		).
62
63		disprover_po_with_info(Name,RodinStatus,ProBStatus,RawResult) :-
64	?	get_disprover_po(Name,_Context,_Goal,_All,_Sel,RodinStatus),
65		(disprover_result(Name,ProBStatus,RawResult) -> true ; ProBStatus='not_run', RawResult='not_run').
66
67		:- dynamic disprover_timeout/1.
68		:- if(current_prolog_flag(dialect, swi)).
69		disprover_timeout(1000).
70		:- else.
71		disprover_timeout(300).
72		:- endif.
73		set_disprover_timeout(N) :- retractall(disprover_timeout(_)), assertz(disprover_timeout(N)).
74		reset_disprover_timeout :- retractall(disprover_timeout(_)), assertz(disprover_timeout(300)).
75
76		:- use_module(probsrc(tools_lists),[count_occurences/2]).
77
78		run_disprover_on_po(PO) :-
79		disprover_timeout(TO),
80		run_on_po(PO,TO).
81
82	?	run_disprover_on_all_pos(_) :- retractall(disprover_result(_,_,_)), disprover_timeout(TO),run_on_po(_,TO), fail.
83		run_disprover_on_all_pos(Summary) :- findall(R,disprover_result(_,R,_),L),
84		count_occurences(L,Occs),
85		format('~nDisprover Run Summary: ~w~n',[Occs]),
86		add_info(true,Occs,O1), add_info(false,O1,O2), add_info(unknown,O2,O3),
87		add_info(failure,O3,Summary).
88
89	?	add_info(Info,List,Result) :- member(Info-_,List) -> List=Result ; Result = [Info-0|List].
90
91
92		:- use_module(probsrc(tools_printing),[format_with_colour_nl/4]).
93		:- use_module(probsrc(prob2_interface), [start_animation/0, load_event_b_project/4]).
94
95		run_on_po(PO_Name,TimeOut) :-
96	?	get_disprover_po(PO_Name,Context,Goal,AllHypotheses,SelectedHypotheses,Status),
97		formatsilent('Checking PO ~w (~w in Rodin)~n',[PO_Name,Status]),
98		load_event_b_project([],[Context],[],_),
99		start_animation,
100		debug_println(5,loaded_context),
101		(debug_mode(on) -> translate:print_raw_bexpr(Goal),nl ; true),
102		statistics(walltime,[T1,_]),
103		(my_disprove(PO_Name,Goal,AllHypotheses,SelectedHypotheses,TimeOut,OutResult)
104		-> translate_result_for_po(OutResult,ProverResult,Color),
105		(silent_mode(on) -> true
106		; statistics(walltime,[T2,_]), WT is T2-T1,
107		%format(user_output,'Full result for PO ~w is ~w~n',[PO_Name,OutResult]),
108		format(user_output,'Disprover Result (~w ms): PO ~w is ',[WT,PO_Name]),
109		format_with_colour_nl(user_output,Color,'~w',[ProverResult])
110		),
111		print_solution(OutResult),
112		functor(OutResult,RawOutFunctor,_),
113		assertz(disprover_result(PO_Name,ProverResult,RawOutFunctor)),
114		check_soundness(ProverResult,Status,PO_Name)
115		; add_error(disprover,'Disprover failed: ',(PO_Name:Status)),
116		assertz(disprover_result(PO_Name,'failure',unknown))
117		).
118		run_on_po(PO_Name,_TimeOut) :- nonvar(PO_Name),
119		\+ get_disprover_po(PO_Name,_,_,_,_,_),
120		format('PO ~w does not exist !~n',[PO_Name]),
121		findall(PO,get_disprover_po(PO,_,_,_,_,_),L),
122		format('Available POs: ~w~n',[L]),
123		fail.
124
125		:- use_module(library(lists), [maplist/2]).
126		print_solution(solution(L)) :-
127		formatsilent('Counterexample using all hypotheses:~n',[]), maplist(print_binding,L),!.
128		print_solution(solution_on_selected_hypotheses(L)) :-
129		formatsilent('Counterexample using selected hypotheses:~n',[]), maplist(print_binding,L),!.
130		print_solution(L) :- (debug_mode(on) -> formatsilent(' ~w~n',[L]) ; true).
131		print_binding(binding(ID,_Val,VS)) :- formatsilent(' ~w = ~w~n',[ID,VS]).
132
133		translate_result_for_po(solution(_),R,Col) :- !, R=false,Col=[bold,red].
134		translate_result_for_po(contradiction_found,R,Col) :- !,R=true,Col=[bold,green].
135		translate_result_for_po(contradiction_in_hypotheses,R,Col) :- !,R=true,Col=[green].
136		translate_result_for_po(solution_on_selected_hypotheses(_),R,Col) :- !, R=unknown,Col=[bold,red].
137		translate_result_for_po(_,unknown,[red]).
138
139		check_soundness(unknown,_,_) :- !.
140		check_soundness(Status,unknown,PO_Name) :- !,
141		formatsilent('ProB Disprover result ~w improves upon unknown Rodin prover status for ~w!~n',[Status,PO_Name]).
142		check_soundness(X,X,_) :- !.
143		check_soundness(Disprover,Prover,PO_Name) :-
144		ajoin(['Disprover result ',Disprover, ' incompatible with Rodin proof status ',Prover,' for PO:'],Msg),
145		add_error(disprover_unsound,Msg,PO_Name).
146
147
148		:- dynamic extra_opts/1.
149		extra_opts([]).
150		get_disprover_options(L) :- extra_opts(L).
151		set_disprover_options(L) :-
152		retractall(extra_opts(_)),
153		assertz(extra_opts(L)).
154
155		my_disprove(PO_Name,Goal,AllHypotheses,SelectedHypotheses,Timeout,OutResult) :-
156		get_disprover_default_opts(DOpts),
157		Opts = [disprover_option(po_label(PO_Name))|DOpts],
158		% interesting extra opts : disprover_option(unsat_core),unsat_core_algorithm/linear
159		extra_opts(X), merge_opts(X,Opts,AllOpts),
160		% Note: disprover_mode is always set to true
161		disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,Timeout,AllOpts,OutResult).
162
163		merge_opts([],Opts,Opts).
164		merge_opts([Opt/Val|T],Other,[Opt/Val|ResT]) :- !,
165		delete(Other,Opt/_,Other2),
166		merge_opts(T,Other2,ResT).
167		merge_opts([Opt|T],Other,[Opt|ResT]) :-
168		merge_opts(T,Other,ResT).
169
170		get_disprover_po(FName,Context,Goal,All,Sel,Status) :-
171	?	disprover_po(Name,Context,Goal,All,Sel,Status),
172		fix_rodin_name(Name,FName).
173
174		linefeed(10).
175		linefeed(13).
176		% sometimes Rodin POs have a newline before the slash; we remove this (see e.g., test 2023)
177		fix_rodin_name(POName,FixedName) :- atom_codes(POName,Cs),
178		exclude(linefeed,Cs,NewCs),
179		atom_codes(FixedName,NewCs).
180
181		:- dynamic project_name/1.
182		:- dynamic machine_name/1.
183		:- dynamic generated/2.
184		:- dynamic disprover_po/6.
185		:- dynamic disprover_result/3.
186		project_name(unknown).
187		machine_name(unknown).
188		generated(unknown,unknown).
189		disprover_po(unknown,unknown,unknown,unknown,unknown,unknown).
190		disprover_result(unknown,unknown,unknown).
191
192		reset_po_facts :- retractall(loaded_po_file(_)),
193		retractall(project_name(_)),
194		retractall(machine_name(_)), retractall(generated(_,_)),
195		retractall(disprover_po(_,_,_,_,_,_)), retractall(disprover_result(_,_,_)).
196
197		get_disprover_result(PO_Name,Result,RawResult) :-
198		(disprover_result(PO_Name,R,Raw) -> Result=R,RawResult=Raw
199		; Result = 'not_yet_run', RawResult='not_yet_run').
200
201		:- dynamic loaded_po_file/1.
202		get_loaded_po_file(File) :- loaded_po_file(File).
203		load_po_file(File) :- reset_po_facts,
204		% consult_without_redefine_warning
205		get_set_optional_prolog_flag(redefine_warnings, Old, off),
206		(% load in dynamic mode: so that we can retract later
207		my_po_consult(File)
208		-> OK=true ; OK=false),
209		get_set_optional_prolog_flag(redefine_warnings, _, Old),
210		(OK=true -> assertz(loaded_po_file(File)) ;
211		add_error_and_fail(disprover_test_runner,'Consulting of File failed: ',File)).
212
213		my_po_consult(File) :-
214		catch(
215		load_files(File,[compilation_mode(assert_all)]),
216		error(existence_error(_,_),_),
217		add_error_fail(my_consult,'File does not exist: ',File)).