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