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). |