1 | % (c) 2014-2019 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 | disprove_predicate/3,disprove_predicate/2]). | |
7 | ||
8 | :- use_module(module_information,[module_info/2]). | |
9 | :- module_info(group,smt_solvers). | |
10 | :- module_info(description,'This module provides an interface to the Atelier-B provers.'). | |
11 | ||
12 | :- use_module(bsyntaxtree,[create_negation/2, | |
13 | conjunct_predicates/2, | |
14 | create_implication/3, | |
15 | conjunction_to_list/2]). | |
16 | :- use_module(translate, [translate_bexpression/2, | |
17 | translate_subst_or_bexpr_in_mode/3, | |
18 | set_print_type_infos/1]). | |
19 | :- use_module(system_call, [system_call/5]). | |
20 | :- use_module(preferences, [get_preference/2, | |
21 | temporary_set_preference/3, | |
22 | reset_temporary_preference/2]). | |
23 | :- use_module(tools, [read_string_from_file/2]). | |
24 | :- use_module(error_manager, [get_error/2, add_error/2, add_error/3]). | |
25 | :- use_module(debug, [debug_println/2]). | |
26 | ||
27 | prove_predicate(L,P,R) :- %debug_println(9,prove_predicate(L,P,R)), | |
28 | (prove_predicate_aux(L,P,Res) | |
29 | -> (get_error(system_call,_) -> R = error ; R = Res) | |
30 | ; add_error(atelierb_provers_interface, | |
31 | 'Call to Atelier-B Provers failed. Be sure to set ATELIERB_KRT_PATH preference correctly.'), | |
32 | fail). | |
33 | prove_predicate_aux(ListOfHypotheses,Predicate,Result) :- | |
34 | set_print_type_infos(all), | |
35 | ||
36 | conjunct_predicates(ListOfHypotheses,ConjunctOfHypotheses), | |
37 | create_implication(ConjunctOfHypotheses,Predicate,Sequent), | |
38 | ||
39 | get_preference(path_to_atb_krt,PathToKrt), | |
40 | debug_println(9,path_to_atb_krt(PathToKrt)), | |
41 | create_temp_file(ml,Sequent,TempFilePathML,ResultFilePathML), | |
42 | debug_println(9,created_temp_file(ResultFilePathML)), | |
43 | call_ml(PathToKrt,TempFilePathML,ResultFilePathML,MLResult), | |
44 | (MLResult = proved | |
45 | -> Result = MLResult | |
46 | ; create_temp_file(pp,Sequent,TempFilePathPP,ResultFilePathPP), | |
47 | call_pp(PathToKrt,TempFilePathPP,ResultFilePathPP,Result)), | |
48 | set_print_type_infos(none). | |
49 | ||
50 | disprove_predicate(Predicate,Result) :- | |
51 | conjunction_to_list(Predicate,Hyps), | |
52 | Falsity = b(equal(b(boolean_true,boolean,[]),b(boolean_false,boolean,[])),pred,[]), | |
53 | prove_predicate(Hyps,Falsity,Result). | |
54 | disprove_predicate(ListOfHypotheses,Predicate,Result) :- | |
55 | create_negation(Predicate,NegPredicate), | |
56 | conjunct_predicates(NegPredicate,Conjunct), | |
57 | prove_predicate(ListOfHypotheses,Conjunct,Result). | |
58 | ||
59 | create_temp_file(ml,Sequent,FileName,OutputFileName) :- | |
60 | % generate identifiers to remove primes, etc. | |
61 | temporary_set_preference(bugly_pp_scrambling,true,Chng), | |
62 | temp_file(S,FileName), | |
63 | format(S,'THEORY Lemma;Unproved IS\n',[]), | |
64 | translate_bexpression(Sequent,PPSequent), | |
65 | format(S,'~w\n',PPSequent), | |
66 | temp_file(STemp,OutputFileName), | |
67 | format(S, 'WHEN Force IS (0;1;2;3) WHEN FileOut IS "~w"\n', [OutputFileName]), | |
68 | format(S, 'WHEN Options IS ? & ? & ? & OK & "" & dummy & KO\nEND\n', []), | |
69 | close(S), | |
70 | close(STemp), | |
71 | reset_temporary_preference(bugly_pp_scrambling,Chng). | |
72 | ||
73 | create_temp_file(pp,Sequent,FileName,OutputFileName) :- | |
74 | % generate identifiers to remove primes, etc. | |
75 | temporary_set_preference(bugly_pp_scrambling,true,Chng), | |
76 | temp_file(S,FileName), | |
77 | temp_file(STemp,OutputFileName), | |
78 | format(S,'Flag(FileOn("~w")) & Set(toto | ',[OutputFileName]), | |
79 | translate_subst_or_bexpr_in_mode(atelierb_pp,Sequent,PPSequent), | |
80 | format(S, '~w )\n', [PPSequent]), | |
81 | close(S), | |
82 | close(STemp), | |
83 | reset_temporary_preference(bugly_pp_scrambling,Chng). | |
84 | ||
85 | temp_file(S,Filename) :- | |
86 | open(temp('atbprovers_temp_file'),write,S,[if_exists(generate_unique_name)]), | |
87 | stream_property(S, file_name(Filename)). | |
88 | ||
89 | call_ml(Krt,TempFilePath,ResultFilePath,Result) :- | |
90 | ml_path(Krt,MLKin), | |
91 | debug_println(9,calling_ml(Krt,MLKin)), | |
92 | system_call(Krt,['-a','m1500000','-p','rmcomm','-b',MLKin,TempFilePath],_,ErrorTextAsCodeList,_), | |
93 | debug_println(9,result_err(ErrorTextAsCodeList)), | |
94 | (ErrorTextAsCodeList = [] | |
95 | -> read_string_from_file(ResultFilePath,String), | |
96 | ml_result(String,Result) | |
97 | ; format('ML Error Result: ~s~n.',[ErrorTextAsCodeList]), | |
98 | Result = error). | |
99 | ||
100 | call_pp(Krt,TempFilePath,ResultFilePath,Result) :- | |
101 | pp_path(Krt,PPKin), | |
102 | debug_println(9,calling_pp(Krt,PPKin)), | |
103 | system_call(Krt,['-p','rmcomm','-b',PPKin,TempFilePath],_,ErrorTextAsCodeList,_), | |
104 | (ErrorTextAsCodeList = [] | |
105 | -> read_string_from_file(ResultFilePath,String), | |
106 | pp_result(String,Result) | |
107 | ; format('PP Error Result: ~s~n',[ErrorTextAsCodeList]), | |
108 | Result = error). | |
109 | ||
110 | ml_result(String,proved) :- | |
111 | append("THEORY Etat IS Proved",_,String), !. | |
112 | ml_result(_,unproved). | |
113 | pp_result(String,proved) :- | |
114 | append("SUCCES",_,String), !. | |
115 | pp_result(_,unproved). | |
116 | ||
117 | ml_path(PathToKrt,PathToML) :- krt_path_to_kin(PathToKrt,"ML.kin",PathToML). | |
118 | pp_path(PathToKrt,PathToML) :- krt_path_to_kin(PathToKrt,"PP.kin",PathToML). | |
119 | ||
120 | krt_path_to_kin(PathToKrt,KINEXT,PathToML) :- | |
121 | atom_codes(PathToKrt,PathString), | |
122 | (append(BasePath,"krt",PathString) | |
123 | -> append(BasePath,KINEXT,MLString), | |
124 | atom_codes(PathToML,MLString) | |
125 | ; add_error(atelierb_provers_interface,'ATELIERB_KRT_PATH does not point to a krt binary: ',PathToKrt), | |
126 | fail). |