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, print_green_checkmark/1, print_red_cross/1]).
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		(ProverResult=true -> print_green_checkmark(user_output) ; print_red_cross(user_output)),
109		format(user_output,' Disprover Result (~w ms): PO ~w is ',[WT,PO_Name]),
110		format_with_colour_nl(user_output,Color,'~w',[ProverResult])
111		),
112		print_solution(OutResult),
113		functor(OutResult,RawOutFunctor,_),
114		assertz(disprover_result(PO_Name,ProverResult,RawOutFunctor)),
115		check_soundness(ProverResult,Status,PO_Name)
116		; add_error(disprover,'Disprover failed: ',(PO_Name:Status)),
117		assertz(disprover_result(PO_Name,'failure',unknown))
118		).
119		run_on_po(PO_Name,_TimeOut) :- nonvar(PO_Name),
120		\+ get_disprover_po(PO_Name,_,_,_,_,_),
121		format('PO ~w does not exist !~n',[PO_Name]),
122		findall(PO,get_disprover_po(PO,_,_,_,_,_),L),
123		format('Available POs: ~w~n',[L]),
124		fail.
125
126		:- use_module(library(lists), [maplist/2]).
127		print_solution(solution(L)) :-
128		formatsilent('Counterexample using all hypotheses:~n',[]), maplist(print_binding,L),!.
129		print_solution(solution_on_selected_hypotheses(L)) :-
130		formatsilent('Counterexample using selected hypotheses:~n',[]), maplist(print_binding,L),!.
131		print_solution(L) :- (debug_mode(on) -> formatsilent(' ~w~n',[L]) ; true).
132		print_binding(binding(ID,_Val,VS)) :- formatsilent(' ~w = ~w~n',[ID,VS]).
133
134		translate_result_for_po(solution(_),R,Col) :- !, R=false,Col=[bold,red].
135		translate_result_for_po(contradiction_found,R,Col) :- !,R=true,Col=[bold,green].
136		translate_result_for_po(contradiction_in_hypotheses,R,Col) :- !,R=true,Col=[green].
137		translate_result_for_po(solution_on_selected_hypotheses(_),R,Col) :- !, R=unknown,Col=[bold,red].
138		translate_result_for_po(_,unknown,[red]).
139
140		check_soundness(unknown,_,_) :- !.
141		check_soundness(Status,unknown,PO_Name) :- !,
142		formatsilent('ProB Disprover result ~w improves upon unknown Rodin prover status for ~w!~n',[Status,PO_Name]).
143		check_soundness(X,X,_) :- !.
144		check_soundness(Disprover,Prover,PO_Name) :-
145		ajoin(['Disprover result ',Disprover, ' incompatible with Rodin proof status ',Prover,' for PO:'],Msg),
146		add_error(disprover_unsound,Msg,PO_Name).
147
148
149		:- dynamic extra_opts/1.
150		extra_opts([]).
151		get_disprover_options(L) :- extra_opts(L).
152		set_disprover_options(L) :-
153		retractall(extra_opts(_)),
154		assertz(extra_opts(L)).
155
156		my_disprove(PO_Name,Goal,AllHypotheses,SelectedHypotheses,Timeout,OutResult) :-
157		get_disprover_default_opts(DOpts),
158		Opts = [disprover_option(po_label(PO_Name))|DOpts],
159		% interesting extra opts : disprover_option(unsat_core),unsat_core_algorithm/linear
160		extra_opts(X), merge_opts(X,Opts,AllOpts),
161		% Note: disprover_mode is always set to true
162		disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,Timeout,AllOpts,OutResult).
163
164		merge_opts([],Opts,Opts).
165		merge_opts([Opt/Val|T],Other,[Opt/Val|ResT]) :- !,
166		delete(Other,Opt/_,Other2),
167		merge_opts(T,Other2,ResT).
168		merge_opts([Opt|T],Other,[Opt|ResT]) :-
169		merge_opts(T,Other,ResT).
170
171		get_disprover_po(FName,Context,Goal,All,Sel,Status) :-
172		disprover_po(Name,Context,Goal,All,Sel,Status),
173		fix_rodin_name(Name,FName).
174
175		linefeed(10).
176		linefeed(13).
177		% sometimes Rodin POs have a newline before the slash; we remove this (see e.g., test 2023)
178		fix_rodin_name(POName,FixedName) :- atom_codes(POName,Cs),
179		exclude(linefeed,Cs,NewCs),
180		atom_codes(FixedName,NewCs).
181
182		:- dynamic project_name/1.
183		:- dynamic machine_name/1.
184		:- dynamic generated/2.
185		:- dynamic disprover_po/6.
186		:- dynamic disprover_result/3.
187		project_name(unknown).
188		machine_name(unknown).
189		generated(unknown,unknown).
190		disprover_po(unknown,unknown,unknown,unknown,unknown,unknown).
191		disprover_result(unknown,unknown,unknown).
192
193		reset_po_facts :- retractall(loaded_po_file(_)),
194		retractall(project_name(_)),
195		retractall(machine_name(_)), retractall(generated(_,_)),
196		retractall(disprover_po(_,_,_,_,_,_)), retractall(disprover_result(_,_,_)).
197
198		get_disprover_result(PO_Name,Result,RawResult) :-
199		(disprover_result(PO_Name,R,Raw) -> Result=R,RawResult=Raw
200		; Result = 'not_yet_run', RawResult='not_yet_run').
201
202		:- dynamic loaded_po_file/1.
203		get_loaded_po_file(File) :- loaded_po_file(File).
204		load_po_file(File) :- reset_po_facts,
205		% consult_without_redefine_warning
206		get_set_optional_prolog_flag(redefine_warnings, Old, off),
207		(% load in dynamic mode: so that we can retract later
208		my_po_consult(File)
209		-> OK=true ; OK=false),
210		get_set_optional_prolog_flag(redefine_warnings, _, Old),
211		(OK=true -> assertz(loaded_po_file(File)) ;
212		add_error_and_fail(disprover_test_runner,'Consulting of File failed: ',File)).
213
214		my_po_consult(File) :-
215		catch(
216		load_files(File,[compilation_mode(assert_all)]),
217		error(existence_error(_,_),_),
218		add_error_fail(my_consult,'File does not exist: ',File)).