1 % (c) 2009-2024 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
6 :- module(kodkod,[replace_by_kodkod/3,
7 current_solver_is_not_incremental/0,
8 kodkod_request/5,
9 %apply_kodkod_to_counterexample_search/5,
10 kodkod_reset/0]).
11
12 :- use_module(library(lists)).
13 :- use_module(library(avl)).
14
15 :- use_module(probsrc(tools)).
16 :- use_module(probsrc(bmachine)).
17 :- use_module(probsrc(self_check)).
18 :- use_module(probsrc(bsyntaxtree)).
19 :- use_module(probsrc(translate)).
20 :- use_module(probsrc(btypechecker)).
21 :- use_module(probsrc(b_global_sets),[b_global_set/1,lookup_global_constant/2]).
22 :- use_module(probsrc(preferences),[get_preference/2]).
23
24 :- use_module(kodkodsrc(predicate_analysis)).
25 :- use_module(kodkodsrc(kodkod_translate)).
26 :- use_module(kodkodsrc(kodkod_tools)).
27 :- use_module(kodkodsrc(kodkod_rewrite)).
28 :- use_module(kodkodsrc(kodkod2)).
29 :- use_module(kodkodsrc(kodkod_typing)).
30 :- use_module(kodkodsrc(kodkod_process)).
31 :- use_module(kodkodsrc(kodkod_annotator)).
32
33 :- use_module(probsrc(module_information),[module_info/2]).
34 :- module_info(group,kodkod).
35 :- module_info(description,'This is the central module of the B to Kodkod translation (still experimental).').
36
37 %:- dynamic kodkod_error/1.
38
39 kodkod_reset :-
40 ( stop_kodkod -> true; true).
41
42 % Signum is either pos (when we want the predicate to succeed) or neg (when we want the predicate to be false)
43 kodkod_request(Id,Signum,LocalState,State,LWF) :-
44 % MaxNrOfSols is the maximum number of solutions found in one go by Kodkod
45 get_max_nr_of_solutions(MaxNrOfSols),
46 kodkod_request(Id,Signum,MaxNrOfSols,LocalState,State,LWF).
47
48 get_max_nr_of_solutions(MaxNrOfSols) :-
49 current_solver_is_not_incremental,!,
50 MaxNrOfSols = 1.
51 get_max_nr_of_solutions(MaxNrOfSols) :-
52 get_preference(kodkod_max_nr_solutions,MaxNrOfSols). % TO DO: we could look at kodkod_for_components and maxNrOfInitialisations preference
53
54 current_solver_is_not_incremental :-
55 get_preference(kodkod_sat_solver,Solver),
56 not_incremental(Solver).
57 not_incremental(lingeling).
58
59 :- use_module(probsrc(error_manager)).
60
61 :- block kodkod_request(?,?,?,?,?,-).
62 kodkod_request(Id,Signum,MaxNrOfSols,LocalState,State,_LWF) :-
63 catch(
64 kodkod_request_intern(Id,Signum,MaxNrOfSols,LocalState,State),
65 error(system_error,system_error(E)), % often SPIO_E_NET_CONNRESET
66 (add_internal_error('System Error while processing Kodkod request: ',E), fail)).
67
68
69 %
70 :- use_module(extrasrc(b_expression_sharing),[expand_cse_lazy_lets/2]).
71 replace_by_kodkod(Constants,Predicate,NewPredicate) :-
72 % Remove any CSE lazy_lets as Kodkod translation cannot deal with them yet
73 (get_preference(use_common_subexpression_elimination,true) ->
74 expand_cse_lazy_lets(Predicate,Predicate0)
75 ; Predicate0=Predicate),
76 % The Predicate may already contain Kodkod calls, replace
77 % them by their original B predicate
78 undo_kodkod_replacements(Predicate0,Predicate1),
79 % first we do a predicate analysis to determine ranges for integers
80 try_predicate_analysis_with_global_sets(Predicate1,Constants,TaggedConstants,TaggedPredicate),
81 replace_by_kodkod2(TaggedConstants,TaggedPredicate,NewPredicate).
82
83 :- use_module(probsrc(preferences),[temporary_set_preference/3,reset_temporary_preference/2]).
84 replace_by_kodkod2(Constants,_Predicate,NewPredicate) :-
85 % If the static analysis states that there is no possible solution for one
86 % of the identifiers, we just say "false"
87 somechk(is_inconsistent_expression,Constants),!,
88 write('kodkod: Static analysis detected inconsistencies, new predicate is "false"'),nl,
89 create_texpr(falsity,pred,[],NewPredicate).
90 replace_by_kodkod2(Constants,Predicate,NewPredicate) :-
91 temporary_set_preference(partition_predicates_inline_equalities,false,CHNG),
92 split_predicates(Predicate,PList), % will split into components if KODKOD_ONLY_FULL = FALSE
93 reset_temporary_preference(partition_predicates_inline_equalities,CHNG),
94 % we try to translate each predicate alone
95 try_apply_transformation_l(PList,Constants,1,Result),
96 print_results(Result),
97 % split the result into two lists: the successfull translatable predicates (ToKodkod)
98 % and those which were not translatable (StayProb)
99 filter_translatable(Result,ToKodkod,StayProb),
100 %%print('Stay ProB: '), conjunct_predicates(StayProb,StayPred), translate:print_bexpr(StayPred),nl,
101 % fail if there are no translatable predicates
102 ToKodkod = [_|_],
103 % now, translate all translatable predicates in one run
104 (StayProb = [_|_] -> add_message(kodkod,'Not translating all components/predicates with Kodkod') ; true ),
105 % with a special preference to force full evaluation we could also abort here and return UNKNOWN
106 apply_transformation(Constants,ToKodkod,KPred),
107 % the new
108 %%print('For Kodkod: '), translate:print_bexpr(KPred),nl,
109 conjunct_predicates([KPred|StayProb],NewPredicate).
110
111
112 split_predicates(Predicate,Parts) :-
113 get_preference(kodkod_for_components,false),!,
114 conjunction_to_list(Predicate,Parts).
115 split_predicates(Predicate,Parts) :-
116 % only translate full components (or component not at all)
117 predicate_components(Predicate,Components),
118 findall(P,member(component(P,_),Components),Parts).
119
120 split_simple_equalities(InPredicate,Equalities,Rest) :-
121 conjunction_to_list(InPredicate,InPredicates),
122 split_list(is_simple_equality,InPredicates,EqualitiesL,RestL),
123 conjunct_predicates(EqualitiesL,Equalities),
124 conjunct_predicates(RestL,Rest).
125
126 is_simple_equality(TExpr) :-
127 get_texpr_expr(TExpr,equal(A,B)),
128 ( get_texpr_id(A,_),is_base_expression(B)
129 ; get_texpr_id(B,_),is_base_expression(A)),!.
130
131 is_base_expression(TExpr) :-
132 get_texpr_expr(TExpr,Expr),
133 is_base_expression2(Expr).
134 is_base_expression2(identifier(Id)) :- b_global_set(Id),!. % a deferred set
135 is_base_expression2(identifier(Id)) :- lookup_global_constant(Id,_). % an enumerated set element
136 is_base_expression2(integer(_)).
137 is_base_expression2(couple(A,B)) :- is_base_expression(A),is_base_expression(B).
138 is_base_expression2(set_extension(L)) :- maplist(is_base_expression,L).
139 is_base_expression2(value(_)).
140 is_base_expression2(boolean_true).
141 is_base_expression2(boolean_false).
142 is_base_expression2(empty_set).
143 is_base_expression2(bool_set).
144 is_base_expression2(add(A,B)) :- is_base_expression(A),is_base_expression(B).
145 is_base_expression2(minus(A,B)) :- is_base_expression(A),is_base_expression(B).
146 is_base_expression2(unary_minus(A)) :- is_base_expression(A).
147 is_base_expression2(multiplication(A,B)) :- is_base_expression(A),is_base_expression(B).
148 is_base_expression2(div(A,B)) :- is_base_expression(A),is_base_expression(B).
149 is_base_expression2(floored_div(A,B)) :- is_base_expression(A),is_base_expression(B).
150 is_base_expression2(modulo(A,B)) :- is_base_expression(A),is_base_expression(B).
151 is_base_expression2(power_of(A,B)) :- is_base_expression(A),is_base_expression(B).
152
153
154 undo_kodkod_replacements(Old,New) :-
155 contains_kodkod_call(Old),!,
156 undo_kodkod_replacements2(Old,New).
157 undo_kodkod_replacements(Old,Old).
158 undo_kodkod_replacements2(TOld,TNew) :-
159 get_texpr_expr(TOld,Old),
160 undo_kodkod_replacements3(Old,TOld,TNew).
161 undo_kodkod_replacements3(conjunct(A,B),_TOld,TNew) :-
162 !,create_texpr(conjunct(NewA,NewB),pred,[],TNew),
163 undo_kodkod_replacements2(A,NewA),
164 undo_kodkod_replacements2(B,NewB).
165 undo_kodkod_replacements3(kodkod(Id,_),_TOld,Orig) :-
166 !,get_original_problem(Id,Orig).
167 undo_kodkod_replacements3(_Old,TOld,TOld).
168
169 contains_kodkod_call(TExpr) :-
170 get_texpr_expr(TExpr,Expr),
171 contains_kodkod_call2(Expr),!.
172 contains_kodkod_call2(kodkod(_,_)).
173 contains_kodkod_call2(conjunct(A,_)) :- contains_kodkod_call(A).
174 contains_kodkod_call2(conjunct(_,B)) :- contains_kodkod_call(B).
175
176
177 try_predicate_analysis_with_global_sets(Predicate,Constants,TaggedConstants,TaggedPredicate) :-
178 catch(predicate_analysis_with_global_sets(Predicate,[],Constants,TaggedConstants,TaggedPredicate),
179 failed_analysis(Expr),
180 ( write('kodkod fail: predicate analysis failed on expression '),
181 translate_bexpression_with_limit(Expr,80,Msg),
182 write(Msg),nl,fail)),
183 !.
184 try_predicate_analysis_with_global_sets(_Predicate,_Constants,_TaggedConstants,_TaggedPredicate) :-
185 write('kodkod fail: predicate analysis failed.\n'),
186 fail.
187 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
188
189 :- meta_predicate try_call(-,-,0).
190
191 try_apply_transformation(Predicate,Constants,Index,Result) :-
192 %%print('TRY KODKOD ON: '), translate:print_bexpr(Predicate),nl,
193 Log = log(Predicate,Result,Index,Ints,Bits),
194 try_call( 'applying rewriting rules', Log,
195 apply_rewriting_rules(Predicate,Rewritten)),
196 %%print('REWRITTEN: '), translate:print_bexpr(Rewritten),nl,
197 try_call( 'extracting used types', Log,
198 extract_used_types(Rewritten,Types,Ints,Bits)),
199 try_call( 'creating Kodkod atoms for types', Log,
200 create_atoms_for_types(Types,Ints,Bits,Typemap,Idmap1,_Valuemap)),
201 try_call( 'translate and type Kodkod formula', Log,
202 typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,_Idmap,Rewritten,_KExpr)),
203 finalize_result(Log).
204 try_call(_Msg,log(_Predicate,Result,_Index,_,_),_Call) :-
205 nonvar(Result),!.
206 try_call(Msg,log(Predicate,Result,Index,_,_),Call) :-
207 %%format('Try ~w ~n',[Msg]),
208 ( catch(Call,
209 kodkod(T),
210 ( %%format('Exception: ~w~n',[T]),
211 Result = failure(Index,Predicate,Msg,kodkod_exception(T)))
212 ) -> true
213 ;
214 %%format('Failure for: ~w~n',[Msg]),
215 Result = failure(Index,Predicate,Msg,failed)
216 ).
217 finalize_result(log(Predicate,Result,Index,Ints,Bits)) :-
218 var(Result),!,Result=ok(Index,Predicate,Ints,Bits).
219 finalize_result(_).
220
221
222 typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,Idmap,Rewritten,KExpr) :-
223 % Create the relations for the constants that are actually used
224 restrict_to_used_constants(Constants,Predicate,UsedConstants),
225 create_identifier_relations(UsedConstants,Typemap,Bits,Idmap1,Idmap),
226 % translate the formula in two steps:
227 kodkod_translate(Rewritten,Typemap,Idmap,Formula),
228 kodkod_insert_casts(Formula,Typemap,Idmap,KExpr),
229 !.
230
231 restrict_to_used_constants(Constants,Predicate,UsedConstants) :-
232 find_identifier_uses(Predicate,['$examine_value_was_identifier_info'],UsedIds), % flag says: also get value(_) with was_identifier(_) field
233 include(constant_is_used(UsedIds),Constants,UsedConstants).
234 constant_is_used(UsedIds,C) :-
235 get_texpr_id(C,Id),memberchk(Id,UsedIds).
236
237 try_apply_transformation_l([],_Constants,_,[]).
238 try_apply_transformation_l([Predicate|Prest],Constants,I,[Result|Rrest]) :-
239 try_apply_transformation(Predicate,Constants,I,Result),
240 I2 is I+1,
241 try_apply_transformation_l(Prest,Constants,I2,Rrest).
242
243
244 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
245
246 filter_translatable([],[],[]).
247 filter_translatable([Res|Rrest],ToKodkod,StayProb) :-
248 ( Res = ok(_,P,_,_) -> ToKodkod=[P|Krest], StayProb=Prest
249 ; Res = failure(_,P,_,_) -> ToKodkod=Krest, StayProb=[P|Prest]),
250 filter_translatable(Rrest,Krest,Prest).
251
252 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
253 :- use_module(probsrc(error_manager),[add_warning/3,add_warning/4]).
254 :- use_module(probsrc(debug),[debug_mode/1,silent_mode/1,nls/0,debug_println/2]).
255
256 apply_transformation(AllConstants,PredicateList,Result) :-
257 conjunct_predicates(PredicateList,Predicate1),
258 (debug_mode(on) -> print('TRANSLATING FOR KODKOD: '),nl,translate:print_bexpr_with_limit(Predicate1,1500),nl ; true),
259 apply_transformation2(AllConstants,Predicate1,Result).
260
261 apply_transformation2(AllConstants,Predicate1,Result) :-
262 split_simple_equalities(Predicate1,Equalities,Predicate),
263 (debug_mode(on) -> print('Equalities: '), translate:print_bexpr_with_limit(Equalities,1500),nl ; true),
264 (is_truth(Predicate)
265 -> debug_println(19,'Predicate for Kodkod has only equalities. Predicate will be solved by ProB.'),
266 Result=Predicate1
267 % we could also fail, but then we would create a kodkod_fail warning
268 ; apply_transformation3(AllConstants,Predicate,Equalities,Result)
269 -> (debug_mode(on) -> print('RESULT: '),nl,translate:print_bexpr_with_limit(Result,1500),nl ; true)
270 ; add_warning(kodkod,'Kodkod Transformation Failed for Predicate over: ',AllConstants),
271 %trace, apply_transformation3(AllConstants,Predicate,Equalities,Result),
272 fail).
273
274 apply_transformation3(AllConstants,Predicate,Equalities,Result) :-
275 restrict_to_used_constants(AllConstants,Predicate,Constants),
276 apply_rewriting_rules(Predicate,Rewritten),
277 extract_used_types(Rewritten,Types,Ints,Bits),
278 create_atoms_for_types(Types,Ints,Bits,Typemap,Idmap1,Valuemap),
279 % check if any types are used, if not Kodkod would exit with an
280 % empty universe exception
281 % (java.lang.IllegalArgumentException: Cannot create an empty universe. or something similar)
282 \+ empty_avl(Typemap),
283 typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,Idmap,Rewritten,KExpr),
284
285 register_problem(Constants,KExpr,Idmap,Typemap,Valuemap,Predicate,ProblemNr),
286 create_texpr(kodkod(ProblemNr,Constants),pred,[],KPred),
287 conjunct_predicates([Equalities,KPred],Result).
288
289 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
290
291 print_results([]).
292 print_results([R|Rrest]) :-
293 print_result(R),nls,
294 print_results(Rrest).
295 print_result(ok(_Ids,Index,P,Ints,Bits)) :-
296 print_result(ok(Index,P,Ints,Bits)).
297 print_result(ok(_Index,P,Ints,Bits)) :-
298 (silent_mode(on) -> true
299 ; write('kodkod ok: '),print_bexpr_with_limit(P,50),
300 write(' ints: '),write(Ints),write(', intatoms: '),write(Bits)
301 ).
302 print_result(failure(_Ids,Index,P,Msg,Reason)) :-
303 print_result(failure(Index,P,Msg,Reason)).
304 print_result(failure(_Index,P,Msg,Reason)) :-
305 write('kodkod fail: '),
306 translate_bexpression_with_limit(P,50,PS), write(PS),
307 write(' , reason: '),write_reason(Reason),write(' while '),write(Msg),nl,
308 (get_preference(kodkod_raise_warnings,false) -> true
309 ; add_warning(kodkod,'Cannot translate predicate for Kodkod: ',PS,P)
310 ).
311 write_reason(kodkod_exception(KE)) :-
312 write_reason2(KE),!.
313 write_reason(E) :- write(E).
314
315 write_reason2(unsupported_type(T)) :-
316 pretty_type(T,PT),
317 write('unsupported type '),write(PT).
318 write_reason2(unsupported_expression(TE)) :-
319 get_texpr_expr(TE,T),
320 functor(T,Functor,Arity),
321 translate_bexpression(TE,PE),
322 format('unsupported expression ~w/~w: ~w',[Functor,Arity,PE]).
323 write_reason2(unsupported_int(Msg)) :-
324 write(Msg).
325 write_reason2(side_condition(Msg,PPExpr,Info)) :-
326 (extract_span_description(Info,Desc)
327 -> format('~w: ~w (~w)',[Msg,PPExpr, Desc])
328 ; format('~w: ~w',[Msg,PPExpr])).
329
330 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
331
332 :- dynamic user:portray/1.
333 :- public pdebug/0.
334 pdebug :-
335 install_b_portray_hook,
336 assertz(( user:portray(X) :- is_avl(X),!,portray_avl(X) )).