1 % (c) 2014-2022 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/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),
44 call_cleanup(call_prover(Prover,Sequent,Result),set_print_type_infos(none)),
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 create_temp_file(ml,Sequent,FileName,OutputFileName) :-
75 % generate identifiers to remove primes, etc.
76 temporary_set_preference(bugly_pp_scrambling,true,Chng),
77 temp_file(S,FileName),
78 format(S,'THEORY Lemma;Unproved IS\n',[]),
79 translate_bexpression(Sequent,PPSequent),
80 %translate_subst_or_bexpr_in_mode(atelierb_ml,Sequent,PPSequent),
81 format(S,'~w\n',PPSequent),
82 temp_file(STemp,OutputFileName),
83 format(S, 'WHEN Force IS (0;1;2;3) WHEN FileOut IS "~w"\n', [OutputFileName]),
84 format(S, 'WHEN Options IS ? & ? & ? & OK & "" & dummy & KO\nEND\n', []),
85 close(S),
86 close(STemp),
87 reset_temporary_preference(bugly_pp_scrambling,Chng).
88
89 create_temp_file(pp,Sequent,FileName,OutputFileName) :-
90 % generate identifiers to remove primes, etc.
91 temporary_set_preference(bugly_pp_scrambling,true,Chng),
92 temp_file(S,FileName),
93 temp_file(STemp,OutputFileName),
94 format(S,'Flag(FileOn("~w")) & Set(toto | ',[OutputFileName]),
95 translate_subst_or_bexpr_in_mode(atelierb_pp,Sequent,PPSequent),
96 format(S, '~w )\n', [PPSequent]),
97 debug_format(19, 'PP Sequent: ~w~n', [PPSequent]),
98 close(S),
99 close(STemp),
100 reset_temporary_preference(bugly_pp_scrambling,Chng).
101
102 :- use_module(probsrc(tools), [open_temp_file/3]).
103 temp_file(S,Filename) :-
104 open_temp_file(atbprovers_temp_file, Filename, S).
105
106 call_ml(Krt,TempFilePath,ResultFilePath,Result) :-
107 ml_path(Krt,MLKin),
108 debug_println(9,calling_ml(Krt,MLKin)),
109 statistics(walltime,[T1,_]),
110 system_call(Krt,['-a','m1500000','-p','rmcomm','-b',MLKin,TempFilePath],_,ErrorTextAsCodeList,_),
111 (ErrorTextAsCodeList = []
112 -> read_string_from_file(ResultFilePath,String),
113 statistics(walltime,[T2,_]), WT is T2-T1,
114 debug_format(19,'ml result (after ~w ms): ~s~n',[WT,String]),
115 ml_result(String,Result)
116 ; format('ML Error Result (~w): ~s~n.',[TempFilePath,ErrorTextAsCodeList]),
117 Result = error).
118
119 call_pp(Krt,TempFilePath,ResultFilePath,Result) :-
120 pp_path(Krt,PPKin),
121 debug_println(9,calling_pp(Krt,PPKin)),
122 statistics(walltime,[T1,_]),
123 system_call(Krt,['-p','rmcomm','-b',PPKin,TempFilePath],_,ErrorTextAsCodeList,_),
124 (ErrorTextAsCodeList = []
125 -> read_string_from_file(ResultFilePath,String),
126 statistics(walltime,[T2,_]), WT is T2-T1,
127 debug_format(19,'pp result (after ~w ms): ~s~n',[WT,String]),
128 pp_result(String,Result)
129 ; format('PP Error Result: ~s~n',[ErrorTextAsCodeList]),
130 Result = error).
131
132 ml_result(String,proved) :-
133 append("THEORY Etat IS Proved",_,String), !.
134 ml_result(_,unproved).
135 pp_result(String,proved) :-
136 append("SUCCES",_,String), !.
137 pp_result(_,unproved).
138
139 ml_path(PathToKrt,PathToML) :- krt_path_to_kin(PathToKrt,"ML.kin",PathToML).
140 pp_path(PathToKrt,PathToML) :- krt_path_to_kin(PathToKrt,"PP.kin",PathToML).
141
142 krt_path_to_kin(PathToKrt,KINEXT,PathToML) :-
143 atom_codes(PathToKrt,PathString),
144 (append(BasePath,"krt",PathString)
145 -> append(BasePath,KINEXT,MLString),
146 atom_codes(PathToML,MLString)
147 ; add_error(atelierb_provers_interface,'ATELIERB_KRT_PATH does not point to a krt binary: ',PathToKrt),
148 fail).