atelierb_provers_interface

call_ml(Krt,TempFilePath,ResultFilePath,Result) :-
    ml_path(Krt,MLKin),
    debug_println(9,calling_ml(Krt,MLKin,tempfile(TempFilePath))),
    statistics(walltime,[T1,_]),
    system_call(Krt,['-a','m1500000','-p','rmcomm','-b',MLKin,TempFilePath],_,ErrorTextAsCodeList,_),
    debug_format(19,'Calling ~w -a m1500000 -p rmcomm -b ~w ~w~n Result will be written to: ~w~n',[Krt,MLKin,TempFilePath,ResultFilePath]), % ResultFilePath is encoded inside the TempFile
    (ErrorTextAsCodeList = []
    -> read_string_from_file(ResultFilePath,String),
    statistics(walltime,[T2,_]), WT is T2-T1,
    debug_format(19,'ml result (after ~w ms): ~s~n',[WT,String]),
    ml_result(String,Result)
    ; format('ML Error Result (~w): ~s~n.',[TempFilePath,ErrorTextAsCodeList]),
    Result = error).

call_pp(Krt,TempFilePath,ResultFilePath,Result) :-
    pp_path(Krt,PPKin),
    debug_println(9,calling_pp(Krt,PPKin)),
    statistics(walltime,[T1,_]),
    system_call(Krt,['-p','rmcomm','-b',PPKin,TempFilePath],_,ErrorTextAsCodeList,_),
    (ErrorTextAsCodeList = []
    -> read_string_from_file(ResultFilePath,String),
    statistics(walltime,[T2,_]), WT is T2-T1,
    debug_format(19,'pp result (after ~w ms): ~s~n',[WT,String]),
    pp_result(String,Result)
    ; format('PP Error Result: ~s~n',[ErrorTextAsCodeList]),
    Result = error).

call_prover(Prover,Sequent,Result) :-
    create_temp_file(Prover,Sequent,TempFilePathML,ResultFilePathML),
    get_preference(path_to_atb_krt,PathToKrt),
    (call_prover_aux(Prover,PathToKrt,TempFilePathML,ResultFilePathML,PRes)
    -> (get_error(system_call,_) -> Result = error ; Result = PRes)
    ; add_error(atelierb_provers_interface,
    'Call to Atelier-B Provers failed. Be sure to set ATELIERB_KRT_PATH preference correctly, currently:',PathToKrt),
    Result=error
).

call_prover_aux(ml,PathToKrt,TempFilePathML,ResultFilePathML,Result) :-
    call_ml(PathToKrt,TempFilePathML,ResultFilePathML,Result).

call_prover_aux(pp,PathToKrt,TempFilePathPP,ResultFilePathPP,Result) :-
    call_pp(PathToKrt,TempFilePathPP,ResultFilePathPP,Result).

create_temp_file(ml,Sequent,FileName,OutputFileName) :-
    % generate identifiers to remove primes, etc.
    temporary_set_preference(bugly_pp_scrambling,true,Chng),
    temp_file(S,FileName),
    format(S,'THEORY Lemma;Unproved IS\n',[]),
    % according to chapter 3 of the manuel_reference_prouveur.pdf the formulas need to be normalised
    normalise_bexpr_for_ml(Sequent,SeqML),
    translate_subst_or_bexpr_in_mode(atelierb_ml,SeqML,PPSequent),
    debug_format(19,'Sending sequent to ML: ~w~n',[PPSequent]),
    format(S,'~w\n',PPSequent),
    temp_file(STemp,OutputFileName),
    format(S, 'WHEN Force IS (0;1;2;3) WHEN FileOut IS "~w"\n', [OutputFileName]),
    format(S, 'WHEN Options IS ? & ? & ? & OK & "" & dummy & KO\nEND\n', []),
    close(S),
    close(STemp),
    reset_temporary_preference(bugly_pp_scrambling,Chng).

create_temp_file(pp,Sequent,FileName,OutputFileName) :-
    % generate identifiers to remove primes, etc.
    temporary_set_preference(bugly_pp_scrambling,true,Chng),
    temp_file(S,FileName),
    temp_file(STemp,OutputFileName),
    format(S,'Flag(FileOn("~w")) & Set(toto | ',[OutputFileName]),
    translate_subst_or_bexpr_in_mode(atelierb_pp,Sequent,PPSequent),
    format(S, '~w )\n', [PPSequent]),
    debug_format(19, 'PP Sequent: ~w~n', [PPSequent]),
    close(S),
    close(STemp),
    reset_temporary_preference(bugly_pp_scrambling,Chng).

disprove_predicate(Predicate,Result) :-
    conjunction_to_list(Predicate,Hyps),
    Falsity = b(equal(b(boolean_true,boolean,[]),b(boolean_false,boolean,[])),pred,[]),
    prove_predicate(Hyps,Falsity,Result).

disprove_predicate(ListOfHypotheses,Predicate,Result) :-
    create_negation(Predicate,NegPredicate),
    conjunct_predicates(NegPredicate,Conjunct),
    prove_predicate(ListOfHypotheses,Conjunct,Result).

krt_path_to_kin(PathToKrt,KINEXT,PathToML) :-
    atom_codes(PathToKrt,PathString),
    (append(BasePath,"krt",PathString)
    -> append(BasePath,KINEXT,MLString),
    atom_codes(PathToML,MLString)
    ; add_error(atelierb_provers_interface,'ATELIERB_KRT_PATH does not point to a krt binary: ',PathToKrt),
    fail).

ml_path(PathToKrt,PathToML) :- krt_path_to_kin(PathToKrt,"ML.kin",PathToML).

ml_result(String,proved) :-
    append("THEORY Etat IS Proved",_,String), !.

ml_result(_,unproved).

pp_path(PathToKrt,PathToML) :- krt_path_to_kin(PathToKrt,"PP.kin",PathToML).

pp_result(String,proved) :-
    append("SUCCES",_,String), !.

pp_result(_,unproved).

prove_predicate(ListOfHypotheses,Predicate,Result) :-
    conjunct_predicates(ListOfHypotheses,ConjunctOfHypotheses),
    create_implication(ConjunctOfHypotheses,Predicate,Sequent),
    prove_sequent_ml_pp(Sequent,Result).

prove_sequent_ml_pp(Sequent,Result) :-
    prove_sequent_with_provers([ml,pp],Sequent,Result).

prove_sequent_with_provers([],_,unproved).

prove_sequent_with_provers([Prover|_],Sequent,FullResult) :-
    set_print_type_infos(all,CHNG),
    call_cleanup(call_prover(Prover,Sequent,Result),reset_print_type_infos(CHNG)),
    Result=proved,!, FullResult=Result.

prove_sequent_with_provers([_|T],Sequent,FullResult) :- prove_sequent_with_provers(T,Sequent,FullResult).

temp_file(S,Filename) :-
    open_temp_file(atbprovers_temp_file, Filename, S).