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(atelierb_provers_interface, [prove_predicate/3,
6 %prove_sequent_ml_pp/2,
7 prove_sequent_with_provers/3,
8 disprove_predicate/3,
9 disprove_predicate/2]).
10
11 :- use_module(probsrc(module_information),[module_info/2]).
12 :- module_info(group,smt_solvers).
13 :- module_info(description,'This module provides an interface to the Atelier-B provers.').
14
15 :- use_module(probsrc(bsyntaxtree),[create_negation/2,
16 conjunct_predicates/2,
17 create_implication/3,
18 conjunction_to_list/2]).
19 :- use_module(probsrc(translate), [translate_bexpression/2,
20 translate_subst_or_bexpr_in_mode/3,
21 set_print_type_infos/2,reset_print_type_infos/1]).
22 :- use_module(probsrc(system_call), [system_call/5]).
23 :- use_module(probsrc(preferences), [get_preference/2,
24 temporary_set_preference/3,
25 reset_temporary_preference/2]).
26 :- use_module(probsrc(tools), [read_string_from_file/2]).
27 :- use_module(probsrc(error_manager), [get_error/2, add_error/3]).
28 :- use_module(probsrc(debug), [debug_println/2, debug_format/3]).
29
30 :- set_prolog_flag(double_quotes, codes).
31
32
33 prove_predicate(ListOfHypotheses,Predicate,Result) :-
34 conjunct_predicates(ListOfHypotheses,ConjunctOfHypotheses),
35 create_implication(ConjunctOfHypotheses,Predicate,Sequent),
36 prove_sequent_ml_pp(Sequent,Result).
37
38 prove_sequent_ml_pp(Sequent,Result) :-
39 prove_sequent_with_provers([ml,pp],Sequent,Result).
40
41 prove_sequent_with_provers([],_,unproved).
42 prove_sequent_with_provers([Prover|_],Sequent,FullResult) :-
43 set_print_type_infos(all,CHNG),
44 call_cleanup(call_prover(Prover,Sequent,Result),reset_print_type_infos(CHNG)),
45 Result=proved,!, FullResult=Result.
46 prove_sequent_with_provers([_|T],Sequent,FullResult) :- prove_sequent_with_provers(T,Sequent,FullResult).
47
48
49 call_prover(Prover,Sequent,Result) :-
50 create_temp_file(Prover,Sequent,TempFilePathML,ResultFilePathML),
51 get_preference(path_to_atb_krt,PathToKrt),
52 (call_prover_aux(Prover,PathToKrt,TempFilePathML,ResultFilePathML,PRes)
53 -> (get_error(system_call,_) -> Result = error ; Result = PRes)
54 ; add_error(atelierb_provers_interface,
55 'Call to Atelier-B Provers failed. Be sure to set ATELIERB_KRT_PATH preference correctly, currently:',PathToKrt),
56 Result=error
57 ).
58
59 call_prover_aux(ml,PathToKrt,TempFilePathML,ResultFilePathML,Result) :-
60 call_ml(PathToKrt,TempFilePathML,ResultFilePathML,Result).
61 call_prover_aux(pp,PathToKrt,TempFilePathPP,ResultFilePathPP,Result) :-
62 call_pp(PathToKrt,TempFilePathPP,ResultFilePathPP,Result).
63
64
65 disprove_predicate(Predicate,Result) :-
66 conjunction_to_list(Predicate,Hyps),
67 Falsity = b(equal(b(boolean_true,boolean,[]),b(boolean_false,boolean,[])),pred,[]),
68 prove_predicate(Hyps,Falsity,Result).
69 disprove_predicate(ListOfHypotheses,Predicate,Result) :-
70 create_negation(Predicate,NegPredicate),
71 conjunct_predicates(NegPredicate,Conjunct),
72 prove_predicate(ListOfHypotheses,Conjunct,Result).
73
74 :- use_module(probsrc(bsyntaxtree),[normalise_bexpr_for_ml/2]).
75 % create a THEORY file for ML which contains the sequent
76 create_temp_file(ml,Sequent,FileName,OutputFileName) :-
77 % generate identifiers to remove primes, etc.
78 temporary_set_preference(bugly_pp_scrambling,true,Chng),
79 temp_file(S,FileName),
80 format(S,'THEORY Lemma;Unproved IS\n',[]),
81 % according to chapter 3 of the manuel_reference_prouveur.pdf the formulas need to be normalised
82 normalise_bexpr_for_ml(Sequent,SeqML),
83 translate_subst_or_bexpr_in_mode(atelierb_ml,SeqML,PPSequent),
84 debug_format(19,'Sending sequent to ML: ~w~n',[PPSequent]),
85 format(S,'~w\n',PPSequent),
86 temp_file(STemp,OutputFileName),
87 format(S, 'WHEN Force IS (0;1;2;3) WHEN FileOut IS "~w"\n', [OutputFileName]),
88 format(S, 'WHEN Options IS ? & ? & ? & OK & "" & dummy & KO\nEND\n', []),
89 close(S),
90 close(STemp),
91 reset_temporary_preference(bugly_pp_scrambling,Chng).
92
93 create_temp_file(pp,Sequent,FileName,OutputFileName) :-
94 % generate identifiers to remove primes, etc.
95 temporary_set_preference(bugly_pp_scrambling,true,Chng),
96 temp_file(S,FileName),
97 temp_file(STemp,OutputFileName),
98 format(S,'Flag(FileOn("~w")) & Set(toto | ',[OutputFileName]),
99 translate_subst_or_bexpr_in_mode(atelierb_pp,Sequent,PPSequent),
100 format(S, '~w )\n', [PPSequent]),
101 debug_format(19, 'PP Sequent: ~w~n', [PPSequent]),
102 close(S),
103 close(STemp),
104 reset_temporary_preference(bugly_pp_scrambling,Chng).
105
106 :- use_module(probsrc(tools), [open_temp_file/3]).
107 temp_file(S,Filename) :-
108 open_temp_file(atbprovers_temp_file, Filename, S).
109
110 call_ml(Krt,TempFilePath,ResultFilePath,Result) :-
111 ml_path(Krt,MLKin),
112 debug_println(9,calling_ml(Krt,MLKin,tempfile(TempFilePath))),
113 statistics(walltime,[T1,_]),
114 system_call(Krt,['-a','m1500000','-p','rmcomm','-b',MLKin,TempFilePath],_,ErrorTextAsCodeList,_),
115 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
116 (ErrorTextAsCodeList = []
117 -> read_string_from_file(ResultFilePath,String),
118 statistics(walltime,[T2,_]), WT is T2-T1,
119 debug_format(19,'ml result (after ~w ms): ~s~n',[WT,String]),
120 ml_result(String,Result)
121 ; format('ML Error Result (~w): ~s~n.',[TempFilePath,ErrorTextAsCodeList]),
122 Result = error).
123
124 call_pp(Krt,TempFilePath,ResultFilePath,Result) :-
125 pp_path(Krt,PPKin),
126 debug_println(9,calling_pp(Krt,PPKin)),
127 statistics(walltime,[T1,_]),
128 system_call(Krt,['-p','rmcomm','-b',PPKin,TempFilePath],_,ErrorTextAsCodeList,_),
129 (ErrorTextAsCodeList = []
130 -> read_string_from_file(ResultFilePath,String),
131 statistics(walltime,[T2,_]), WT is T2-T1,
132 debug_format(19,'pp result (after ~w ms): ~s~n',[WT,String]),
133 pp_result(String,Result)
134 ; format('PP Error Result: ~s~n',[ErrorTextAsCodeList]),
135 Result = error).
136
137 ml_result(String,proved) :-
138 append("THEORY Etat IS Proved",_,String), !.
139 ml_result(_,unproved).
140 pp_result(String,proved) :-
141 append("SUCCES",_,String), !.
142 pp_result(_,unproved).
143
144 ml_path(PathToKrt,PathToML) :- krt_path_to_kin(PathToKrt,"ML.kin",PathToML).
145 pp_path(PathToKrt,PathToML) :- krt_path_to_kin(PathToKrt,"PP.kin",PathToML).
146
147 krt_path_to_kin(PathToKrt,KINEXT,PathToML) :-
148 atom_codes(PathToKrt,PathString),
149 (append(BasePath,"krt",PathString)
150 -> append(BasePath,KINEXT,MLString),
151 atom_codes(PathToML,MLString)
152 ; add_error(atelierb_provers_interface,'ATELIERB_KRT_PATH does not point to a krt binary: ',PathToKrt),
153 fail).