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