log_analyser

analyse_log :- log_file(LF), consult_without_redefine_warning(LF),
    print_message('Initialising'),
    init,
    data_file(F),
    print_message('Generating Table'),
    tell(F),
    (for_gnuplot -> print_normal_table ; print_transposed_excel_table),
    told,
    print_message('Finished Generating Table'),
    (for_gnuplot
    -> script_file(SF),
    tell(SF),
    print_gnuplot_script,
    told,
    print('Now run "gnuplot '), print(SF), print('"'),nl,
    print(' and then open "'),print(F),print('.ps"'),nl % we could execute it also in Prolog
    ; print('Now open "'), print(F), print('" using Excel'),nl
).

analyse_log(F,RowID,ForGnuPlot) :- set_row_identifier(RowID),
    retractall(for_gnuplot),
    (ForGnuPlot=true -> assertz(for_gnuplot) ; true),
    set_log_file_to_analyse(F),
    analyse_log.

assert_group(G) :- group(G) -> true ; assertz(group(G)).

check_log(F) :- consult_without_redefine_warning(F),
    print('File'), print_sep, print('Result'), print_sep,
    print('Loading time'), print_sep, print('(Walltime)'), print_sep,
    print('Checking time'), print_sep, print('(Walltime)'), nl,
    lookup(loading(NOW,Filename,StartTime,StartWTime)),nl,
    get_tail_filename(Filename,Tail),
    print(Tail), print_sep,
    (lookup(error_occurred(NOW,parse_error)) -> print('PARSE ERROR')
    ; lookup(error_occurred(NOW,type_error)) -> print('TYPE ERROR')
    ; lookup(error_occurred(NOW,time_out)) -> print('TIME_OUT')
    ; lookup(error_occurred(NOW,cbc_assertions_time_out)) -> print('TIME_OUT')
    ; lookup(loading_failed(NOW,Filename,_,_)) -> print('OTHER LOAD ERROR')
    ; lookup(error_occurred(NOW,cbc_assertions))
    -> print('** KO **') % print('*** COUNTER EXAMPLE FOUND ***')
    ; lookup(cbc_assertions_finished(NOW,no_counterexample_found,_,_))
    -> print('OK (ENUM WARNING)')
    % TO DO: also register if b_global_sets:unfixed_deferred_set(_) TRUE or not
    % ; lookup(cbc_assertions_finished(NOW,no_counterexample_exists,_,_)
    % \+ b_global_sets:unfixed_deferred_set(_)
    % -> print('PROOF')
    ; print('OK')
    ),
    print_times(NOW,StartTime,StartWTime),
    fail.

check_log(_) :- nl.

consult_without_redefine_warning(File) :-
    current_prolog_flag(redefine_warnings, Old),
    set_prolog_flag(redefine_warnings, off),
    (% load in dynamic mode: so that we can retract later
    my_consult(File)
    -> OK=true ; OK=false),
    set_prolog_flag(redefine_warnings, Old),
    (OK=true -> true ;
    add_error_and_fail(bmachine,'Consulting of File failed: ',File)).

data_file('../log/puzzle.data').

data_file_extension(Ext) :-
    (for_gnuplot -> Ext = '.data' ; Ext = '.csv').

filter_options([],[]).

filter_options([H|T],R) :-
    (interesting_option(H,HH) -> R=[HH|RT] %prob_cli:recognised_option(HH,H),R=[HH|RT]
    ; R=RT),
    filter_options(T,RT).

for_gnuplot.

get_mc_time_for_row_identifier(Benchmark,ID,MCTime) :- use_for_row_identifier(timestamp),
    ID=TimeStamp,
    mc_entry(Benchmark,TimeStamp,MCTime,_Rev).

get_mc_time_for_row_identifier(Benchmark,ID,MCTime) :- use_for_row_identifier(revision),
    ID=Revision,
    mc_entry(Benchmark,_TimeStamp,MCTime,Revision).

init :- retractall(benchmark(_)), print('Benchmarks: '),
    setof(B,Date^Time^mc_entry(B,Date,Time),Bench),
    sort(Bench,SB),
    print(SB),nl,
    member(B1,SB),
    assertz(benchmark(B1)),fail.

init :- retractall(benchmark(_,_,_)),benchmark_group(Group,Benchmark,Name),
    (benchmark(Benchmark) -> true ; print('### No entry for : '), print(Benchmark),nl,fail),
    assertz(benchmark(Benchmark,Group,Name)), assert_group(Group),
    fail.

init :- benchmark(Benchmark), \+ benchmark_group(_,Benchmark,_),
    print('* No group for: '), print(Benchmark),nl,
    assertz(benchmark(Benchmark,unknown,Benchmark)), assert_group(unknown), fail.

init :- retractall(row_identifier(_)),
    use_for_row_identifier(timestamp), print('Timestamps: '),
    setof(D,B^Time^mc_entry(B,D,Time),Dates),
    sort(Dates,SB),
    print(SB),nl,
    member(D1,SB),
    assertz(row_identifier(D1)),fail.

init :- use_for_row_identifier(revision), print('Revisions: '),
    setof(Rev,B^D^Time^mc_entry(B,D,Time,Rev),Revs),
    sort(Revs,SB),
    print(SB),nl,
    member(D1,SB),
    assertz(row_identifier(D1)),fail.

init.

interesting_option(depth_first,df).

interesting_option(breadth_first,bf).

interesting_option(comment(C),C).

interesting_option(set_pref('OPERATION_REUSE',T),op_reuse) :- is_true(T).

interesting_option(set_pref('USE_PO',T),no_po) :- is_false(T).

interesting_option(set_pref('SYMMETRY_MODE',hash),hash).

interesting_option(set_pref('SYMMETRY_MODE',nauty),nauty).

interesting_option(set_pref('SYMMETRY_MODE',flood),flood).

interesting_option(set_pref('SYMBOLIC',T),symbolic) :- is_true(T).

is_false('FALSE'). is_false(false).

is_false('FALSE'). is_false(false).

is_true('TRUE'). is_true(true).

is_true('TRUE'). is_true(true).

log_file('../log/puzzle.log').

lookup(Fact) :- catch(call(Fact), error(existence_error(_,_),_), fail).

mc_entry(BenchT,TIME,MCTime) :- mc_entry(BenchT,TIME,MCTime,_REV).

mc_entry(BenchT,TIME,FullWallTime,rev(REV,FOptions)) :-
    model_check(Now,_,_MCTime,_Res,_TotRun,TotWall),
    loading(Now,B,_StartRun,StartWall),
    FullWallTime is TotWall - StartWall, % assumes nothing else done
    version(Now,_V1,_V2,_V3,_V4,REV,_LASTCHANGED),
    options(Now,Options), filter_options(Options,FOptions),
    %date(Now,datime(Year,Month,Day,_,_)),
    TIME = Now, %is Now // 100,
    get_tail_filename(B,BenchT).

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

p :- init, print_normal_table.

print_benchmark_line(B) :- row_identifier(RowID), print_mc_time_cell(B,RowID),fail.

print_benchmark_line(_) :- nl.

print_cell(X) :- var(X),!,print('_VARIABLE_'), print_sep.

print_cell([H|T]) :- !, print('"'),print_list([H|T]), print('"'), print_sep.

print_cell(X) :- print(X), print_sep.

print_data_file :- data_file(F), print('"'),print(F),print('" ').

print_gnuplot_script :- data_file(F),
    format('set xtics 1,1~Nset style data linespoints~Nset title ""~Nset grid ytics~Nset terminal postscript eps enhanced~Nset output "~p.ps"~N',[F]),
    % set term aqua
    print('plot '),
    findall(BN,benchmark(_B,_,BN),Benchs),
    nth1(Nr,Benchs,BB),
    (Nr>1 -> print(', \\'),nl ; true),
    print_data_file,
    N1 is Nr+1,
    print('using 1:'), print(N1), print(' title "'),print(BB), print('"'),
    fail.

print_gnuplot_script :- nl.

print_header :- for_gnuplot,!,print('# ').

print_header.

print_list([]).

print_list([H|T]) :- print(H), print_list(T).

print_mc_time_cell(B,RowID) :-
    (get_mc_time_for_row_identifier(B,RowID,MCTime) -> print_cell(MCTime) ; print_cell('??')).

print_normal_table :- print_header,
    print_row_identifier_header,
    benchmark(_B,_,BN), print_cell(BN),
    fail.

print_normal_table :- nl,
    row_identifier(D),
    print_row(D),
    fail.

print_normal_table :- nl.

print_row(RowID) :- print_row_identifier(RowID),
    benchmark(B,_,_), print_mc_time_cell(B,RowID),
    fail.

print_row(_) :- nl.

print_row_identifier(rev(ID,Options)) :- use_for_row_identifier(revision),!,
    print_cell(ID),print_cell(Options).

print_row_identifier(TimeStamp) :-
    (date(TimeStamp,datime(Year,Month,Day,Hour,Minutes,Seconds))
    -> RealTime is Seconds + Minutes*60 + Hour*60*60 +
    Day*24*60*60 + Month*31*24*60*60 + (Year-2008)*12*31*24*60*60,
    print_cell(RealTime)
    ; print_cell(TimeStamp), print_error(unknown(TimeStamp))
).

print_row_identifier1(rev(ID,_Options)) :- print_cell(ID),!.

print_row_identifier1(X) :- print_row_identifier(X).

print_row_identifier2(rev(_ID,Options)) :- print_cell(Options),!.

print_row_identifier2(X) :- print_row_identifier(X).

print_row_identifier_header :- use_for_row_identifier(revision),!,
    print_cell('Revision'), print_cell('Options').

print_row_identifier_header :- print_cell('Timestamp').

print_sep :- for_gnuplot,!,print('\t'). % for gnuplot

print_sep :- print(', '). % for Excel CSV

print_time(_Msg,Start,WStart,End,WEnd) :-
    %print(Msg), print_sep,
    T is End-Start, print(T), print(' ms'), print_sep,
    W is WEnd-WStart, print(W), print(' ms').

print_times(NOW,StartTime,StartWTime) :-
    start_animation(NOW,T1,W1),!,
    print_sep,print_time(loading,StartTime,StartWTime,T1,W1),print_sep,
    (lookup(cli_start_initialisation_failed(NOW,T2,W2))
    -> print_time(checking_OK,T1,W1,T2,W2) % no counter-example found
    ; lookup(cbc_assertions_finished(NOW,_,T2,W2))
    -> print_time(checking,T1,W1,T2,W2) % counter-example found
    ; lookup(finished_processing(NOW,T2,W2))
    -> print_time(checking_ERR,T1,W1,T2,W2) % other error
).

print_times(NOW,StartTime,StartWTime) :-
    lookup(loading_failed(NOW,_Filename,T1,W1)),!,
    print_sep,print_time(loading_failure,StartTime,StartWTime,T1,W1).

print_transposed_excel_table :- print_header,
    print_cell('Revision'), row_identifier(D), print_row_identifier1(D),fail.

print_transposed_excel_table :- nl,
    print_cell('Benchmark/Options'), row_identifier(D), print_row_identifier2(D),fail.

print_transposed_excel_table :- nl,
    group(G), print_cell(G),nl,
    print_message(treating_group(G)),
    benchmark(B,G,BN), print_cell(BN),
    print_benchmark_line(B),
    fail.

print_transposed_excel_table :- nl.

script_file('../log/puzzle.plot').

set_log_file_to_analyse(F) :- retractall(log_file(_)), assertz(log_file(F)),
    split_filename(F,Base,_Extension),
    data_file_extension(DExt),
    string_concatenate(Base,DExt,DF),
    print_message(data_file(DF)),
    retractall(data_file(_)), assertz(data_file(DF)),
    string_concatenate(Base,'.plot',PF),
    print_message(script_file(PF)),
    retractall(script_file(_)), assertz(script_file(PF)).

set_row_identifier(ID) :- (ID=timestamp; ID=revision),!,
    retractall(use_for_row_identifier(_)),
    assertz(use_for_row_identifier(ID)).

set_row_identifier(ID) :- add_error(log_analyser,'Illegal Row Identifier: ',ID).

use_for_row_identifier(timestamp).