disprover_test_runner

user:portray_message(informational, _) :- !.

add_info(Info,List,Result) :- member(Info-_,List) -> List=Result ; Result = [Info-0|List].

check_soundness(unknown,_,_) :- !.

check_soundness(Status,unknown,PO_Name) :- !,
    formatsilent('ProB Disprover result ~w improves upon unknown Rodin prover status for ~w!~n',[Status,PO_Name]).

check_soundness(X,X,_) :- !.

check_soundness(Disprover,Prover,PO_Name) :-
    ajoin(['Disprover result ',Disprover, ' incompatible with Rodin proof status ',Prover,' for PO:'],Msg),
    add_error(disprover_unsound,Msg,PO_Name).

disprover_po(unknown,unknown,unknown,unknown,unknown,unknown).

disprover_po_with_info(Name,RodinStatus,ProBStatus,RawResult) :-
    get_disprover_po(Name,_Context,_Goal,_All,_Sel,RodinStatus),
    (disprover_result(Name,ProBStatus,RawResult) -> true ; ProBStatus='not_run', RawResult='not_run').

disprover_result(unknown,unknown,unknown).

disprover_timeout(300).

extra_opts([]).

fix_rodin_name(POName,FixedName) :- atom_codes(POName,Cs),
    exclude(linefeed,Cs,NewCs),
    atom_codes(FixedName,NewCs).

generated(unknown,unknown).

get_disprover_options(L) :- extra_opts(L).

get_disprover_po(FName,Context,Goal,All,Sel,Status) :-
    disprover_po(Name,Context,Goal,All,Sel,Status),
    fix_rodin_name(Name,FName).

get_disprover_result(PO_Name,Result,RawResult) :-
    (disprover_result(PO_Name,R,Raw) -> Result=R,RawResult=Raw
    ; Result = 'not_yet_run', RawResult='not_yet_run').

get_loaded_po_file(File) :- loaded_po_file(File).

linefeed(10).

linefeed(13).

load_po_file(File) :- reset_po_facts,
    % consult_without_redefine_warning
    get_set_optional_prolog_flag(redefine_warnings, Old, off),
    (% load in dynamic mode: so that we can retract later
    my_po_consult(File)
    -> OK=true ; OK=false),
    get_set_optional_prolog_flag(redefine_warnings, _, Old),
    (OK=true -> assertz(loaded_po_file(File)) ;
    add_error_and_fail(disprover_test_runner,'Consulting of File failed: ',File)).

machine_name(unknown).

merge_opts([],Opts,Opts).

merge_opts([Opt/Val|T],Other,[Opt/Val|ResT]) :- !,
    delete(Other,Opt/_,Other2),
    merge_opts(T,Other2,ResT).

merge_opts([Opt|T],Other,[Opt|ResT]) :-
    merge_opts(T,Other,ResT).

my_disprove(PO_Name,Goal,AllHypotheses,SelectedHypotheses,Timeout,OutResult) :-
    get_disprover_default_opts(DOpts),
    Opts = [disprover_option(po_label(PO_Name))|DOpts],
    % interesting extra opts : disprover_option(unsat_core),unsat_core_algorithm/linear
    extra_opts(X), merge_opts(X,Opts,AllOpts),
    % Note: disprover_mode is always set to true
    disprove_with_opts(Goal,AllHypotheses,SelectedHypotheses,Timeout,AllOpts,OutResult).

my_po_consult(File) :-
    catch(
    load_files(File,[compilation_mode(assert_all)]),
    error(existence_error(_,_),_),
    add_error_fail(my_consult,'File does not exist: ',File)).

print_binding(binding(ID,_Val,VS)) :- formatsilent(' ~w = ~w~n',[ID,VS]).

print_disprover_stats :-
    (debug_mode(on) -> print_prover_result_stats ; true), % statistics about various provers
    (disprover_timeout(TO) -> true ; TO = 'UNKNOWN'),
    project_name(N), format('Project ~w~n',[N]),
    generated(_,D),
    machine_name(M), format('Machine ~w (exported ~w)~n',[M,D]),
    print_nr_pos('',_,_),
    print_nr_pos('proven (within Rodin) ',true,_),
    format('ProB Disprover Analysis with timeout ~w ms:~n',[TO]),
    print_nr_pos('proven (by ProB) ',_,true),
    (disprover_result(_,_,contradiction_in_hypotheses)
    -> print_nr_pos('those with contradiction in hypotheses ',_,true,contradiction_in_hypotheses) ; true),
    print_nr_pos('disproven (by ProB) ',_,false),
    print_nr_pos('unproven (by ProB) ',_,unknown),
    (raw_result_exists(failure) -> print_nr_pos('failure (of ProB) ',_,failure) ; true).

print_nr_pos(Msg,RodinStatus,ProBStatus) :- print_nr_pos(Msg,RodinStatus,ProBStatus,_).

print_nr_pos(Msg,RodinStatus,ProBStatus,RawResult) :-
    findall(Name,disprover_po_with_info(Name,RodinStatus,ProBStatus,RawResult),L),
    length(L,Len),
    (Len<12
    -> format(' Number of ~wPOs: ~w (~w)~n',[Msg,Len,L])
    ; (L = [First|_],last(L,Last))
    -> format(' Number of ~wPOs: ~w (~w -- ~w)~n',[Msg,Len,First,Last])
    ; format(' Number of ~wPOs: ~w~n',[Msg,Len])
).

print_solution(solution(L)) :-
    formatsilent('Counterexample using all hypotheses:~n',[]), maplist(print_binding,L),!.

print_solution(solution_on_selected_hypotheses(L)) :-
    formatsilent('Counterexample using selected hypotheses:~n',[]), maplist(print_binding,L),!.

print_solution(L) :- (debug_mode(on) -> formatsilent(' ~w~n',[L]) ; true).

project_name(unknown).

raw_result_exists(RawResult) :- disprover_po_with_info(_,_,_,RawResult).

reset_disprover_timeout :- retractall(disprover_timeout(_)), assertz(disprover_timeout(300)).

reset_po_facts :- retractall(loaded_po_file(_)),
    retractall(project_name(_)),
    retractall(machine_name(_)), retractall(generated(_,_)),
    retractall(disprover_po(_,_,_,_,_,_)), retractall(disprover_result(_,_,_)).

run_disprover_on_all_pos(_) :- retractall(disprover_result(_,_,_)), disprover_timeout(TO),run_on_po(_,TO), fail.

run_disprover_on_all_pos(Summary) :- findall(R,disprover_result(_,R,_),L),
    count_occurences(L,Occs),
    format('~nDisprover Run Summary: ~w~n',[Occs]),
    add_info(true,Occs,O1), add_info(false,O1,O2), add_info(unknown,O2,O3),
    add_info(failure,O3,Summary).

run_disprover_on_po(PO) :-
    disprover_timeout(TO),
    run_on_po(PO,TO).

run_on_po(PO_Name,TimeOut) :-
    get_disprover_po(PO_Name,Context,Goal,AllHypotheses,SelectedHypotheses,Status),
    formatsilent('Checking PO ~w (~w in Rodin)~n',[PO_Name,Status]),
    load_event_b_project([],[Context],[],_),
    start_animation,
    debug_println(5,loaded_context),
    (debug_mode(on) -> translate:print_raw_bexpr(Goal),nl ; true),
    statistics(walltime,[T1,_]),
    (my_disprove(PO_Name,Goal,AllHypotheses,SelectedHypotheses,TimeOut,OutResult)
    -> translate_result_for_po(OutResult,ProverResult,Color),
    (silent_mode(on) -> true
    ; statistics(walltime,[T2,_]), WT is T2-T1,
    %format(user_output,'Full result for PO ~w is ~w~n',[PO_Name,OutResult]),
    format(user_output,'Disprover Result (~w ms): PO ~w is ',[WT,PO_Name]),
    format_with_colour_nl(user_output,Color,'~w',[ProverResult])
    ),
    print_solution(OutResult),
    functor(OutResult,RawOutFunctor,_),
    assertz(disprover_result(PO_Name,ProverResult,RawOutFunctor)),
    check_soundness(ProverResult,Status,PO_Name)
    ; add_error(disprover,'Disprover failed: ',(PO_Name:Status)),
    assertz(disprover_result(PO_Name,'failure',unknown))
).

run_on_po(PO_Name,_TimeOut) :- nonvar(PO_Name),
    \+ get_disprover_po(PO_Name,_,_,_,_,_),
    format('PO ~w does not exist !~n',[PO_Name]),
    findall(PO,get_disprover_po(PO,_,_,_,_,_),L),
    format('Available POs: ~w~n',[L]),
    fail.

set_disprover_options(L) :-
    retractall(extra_opts(_)),
    assertz(extra_opts(L)).

set_disprover_timeout(N) :- retractall(disprover_timeout(_)), assertz(disprover_timeout(N)).

translate_result_for_po(solution(_),R,Col) :- !, R=false,Col=[bold,red].

translate_result_for_po(contradiction_found,R,Col) :- !,R=true,Col=[bold,green].

translate_result_for_po(contradiction_in_hypotheses,R,Col) :- !,R=true,Col=[green].

translate_result_for_po(solution_on_selected_hypotheses(_),R,Col) :- !, R=unknown,Col=[bold,red].

translate_result_for_po(_,unknown,[red]).