1 % (c) 2009-2026 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(sequence_extension(L)) :- maplist(is_base_expression,L).
140 is_base_expression2(value(_)).
141 is_base_expression2(boolean_true).
142 is_base_expression2(boolean_false).
143 is_base_expression2(empty_set).
144 is_base_expression2(empty_sequence).
145 is_base_expression2(bool_set).
146 is_base_expression2(add(A,B)) :- is_base_expression(A),is_base_expression(B).
147 is_base_expression2(minus(A,B)) :- is_base_expression(A),is_base_expression(B).
148 is_base_expression2(unary_minus(A)) :- is_base_expression(A).
149 is_base_expression2(multiplication(A,B)) :- is_base_expression(A),is_base_expression(B).
150 is_base_expression2(div(A,B)) :- is_base_expression(A),is_base_expression(B).
151 is_base_expression2(floored_div(A,B)) :- is_base_expression(A),is_base_expression(B).
152 is_base_expression2(modulo(A,B)) :- is_base_expression(A),is_base_expression(B).
153 is_base_expression2(power_of(A,B)) :- is_base_expression(A),is_base_expression(B).
154
155
156 undo_kodkod_replacements(Old,New) :-
157 contains_kodkod_call(Old),!,
158 undo_kodkod_replacements2(Old,New).
159 undo_kodkod_replacements(Old,Old).
160 undo_kodkod_replacements2(TOld,TNew) :-
161 get_texpr_expr(TOld,Old),
162 undo_kodkod_replacements3(Old,TOld,TNew).
163 undo_kodkod_replacements3(conjunct(A,B),_TOld,TNew) :-
164 !,create_texpr(conjunct(NewA,NewB),pred,[],TNew),
165 undo_kodkod_replacements2(A,NewA),
166 undo_kodkod_replacements2(B,NewB).
167 undo_kodkod_replacements3(kodkod(Id,_),_TOld,Orig) :-
168 !,get_original_problem(Id,Orig).
169 undo_kodkod_replacements3(_Old,TOld,TOld).
170
171 contains_kodkod_call(TExpr) :-
172 get_texpr_expr(TExpr,Expr),
173 contains_kodkod_call2(Expr),!.
174 contains_kodkod_call2(kodkod(_,_)).
175 contains_kodkod_call2(conjunct(A,_)) :- contains_kodkod_call(A).
176 contains_kodkod_call2(conjunct(_,B)) :- contains_kodkod_call(B).
177
178
179 try_predicate_analysis_with_global_sets(Predicate,Constants,TaggedConstants,TaggedPredicate) :-
180 catch(predicate_analysis_with_global_sets(Predicate,[],Constants,TaggedConstants,TaggedPredicate),
181 failed_analysis(Expr),
182 ( write('kodkod fail: predicate analysis failed on expression '),
183 translate_bexpression_with_limit(Expr,80,Msg),
184 write(Msg),nl,fail)),
185 !.
186 try_predicate_analysis_with_global_sets(_Predicate,_Constants,_TaggedConstants,_TaggedPredicate) :-
187 write('kodkod fail: predicate analysis failed.\n'),
188 fail.
189 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
190
191 :- meta_predicate try_call(-,-,0).
192
193 try_apply_transformation(Predicate,Constants,Index,Result) :-
194 %%print('TRY KODKOD ON: '), translate:print_bexpr(Predicate),nl,
195 Log = log(Predicate,Result,Index,Ints,Bits),
196 try_call( 'applying rewriting rules', Log,
197 apply_rewriting_rules(Predicate,Rewritten)),
198 %%print('REWRITTEN: '), translate:print_bexpr(Rewritten),nl,
199 try_call( 'extracting used types', Log,
200 extract_used_types(Rewritten,Types,Ints,Bits)),
201 try_call( 'creating Kodkod atoms for types', Log,
202 create_atoms_for_types(Types,Ints,Bits,Typemap,Idmap1,_Valuemap)),
203 try_call( 'translate and type Kodkod formula', Log,
204 typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,_Idmap,Rewritten,_KExpr)),
205 finalize_result(Log).
206 try_call(_Msg,log(_Predicate,Result,_Index,_,_),_Call) :-
207 nonvar(Result),!.
208 try_call(Msg,log(Predicate,Result,Index,_,_),Call) :-
209 %%format('Try ~w ~n',[Msg]),
210 ( catch(Call,
211 kodkod(T),
212 ( %%format('Exception: ~w~n',[T]),
213 Result = failure(Index,Predicate,Msg,kodkod_exception(T)))
214 ) -> true
215 ;
216 %%format('Failure for: ~w~n',[Msg]),
217 Result = failure(Index,Predicate,Msg,failed)
218 ).
219 finalize_result(log(Predicate,Result,Index,Ints,Bits)) :-
220 var(Result),!,Result=ok(Index,Predicate,Ints,Bits).
221 finalize_result(_).
222
223
224 typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,Idmap,Rewritten,KExpr) :-
225 % Create the relations for the constants that are actually used
226 restrict_to_used_constants(Constants,Predicate,UsedConstants),
227 create_identifier_relations(UsedConstants,Typemap,Bits,Idmap1,Idmap),
228 % translate the formula in two steps:
229 kodkod_translate(Rewritten,Typemap,Idmap,Formula),
230 kodkod_insert_casts(Formula,Typemap,Idmap,KExpr),
231 !.
232
233 restrict_to_used_constants(Constants,Predicate,UsedConstants) :-
234 find_identifier_uses(Predicate,['$examine_value_was_identifier_info'],UsedIds), % flag says: also get value(_) with was_identifier(_) field
235 include(constant_is_used(UsedIds),Constants,UsedConstants).
236 constant_is_used(UsedIds,C) :-
237 get_texpr_id(C,Id),memberchk(Id,UsedIds).
238
239 try_apply_transformation_l([],_Constants,_,[]).
240 try_apply_transformation_l([Predicate|Prest],Constants,I,[Result|Rrest]) :-
241 try_apply_transformation(Predicate,Constants,I,Result),
242 I2 is I+1,
243 try_apply_transformation_l(Prest,Constants,I2,Rrest).
244
245
246 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
247
248 filter_translatable([],[],[]).
249 filter_translatable([Res|Rrest],ToKodkod,StayProb) :-
250 ( Res = ok(_,P,_,_) -> ToKodkod=[P|Krest], StayProb=Prest
251 ; Res = failure(_,P,_,_) -> ToKodkod=Krest, StayProb=[P|Prest]),
252 filter_translatable(Rrest,Krest,Prest).
253
254 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
255 :- use_module(probsrc(error_manager),[add_warning/3,add_warning/4]).
256 :- use_module(probsrc(debug),[debug_mode/1,silent_mode/1,nls/0,debug_println/2]).
257
258 apply_transformation(AllConstants,PredicateList,Result) :-
259 conjunct_predicates(PredicateList,Predicate1),
260 (debug_mode(on) -> print('TRANSLATING FOR KODKOD: '),nl,translate:print_bexpr_with_limit(Predicate1,1500),nl ; true),
261 apply_transformation2(AllConstants,Predicate1,Result).
262
263 apply_transformation2(AllConstants,Predicate1,Result) :-
264 split_simple_equalities(Predicate1,Equalities,Predicate),
265 (debug_mode(on) -> print('Simple equalities: '), translate:print_bexpr_with_limit(Equalities,1500),nl ; true),
266 translate:print_bexpr(Equalities),nl,nl,
267 translate:print_bexpr(Predicate),nl,
268 (is_truth(Predicate)
269 -> debug_println(19,'Predicate for Kodkod has only simple equalities. Predicate will be solved by ProB.'),
270 Result=Predicate1
271 % we could also fail, but then we would create a kodkod_fail warning
272 ; apply_transformation3(AllConstants,Predicate,Equalities,Result)
273 -> (debug_mode(on) -> print('RESULT: '),nl,translate:print_bexpr_with_limit(Result,1500),nl ; true)
274 ; add_warning(kodkod,'Kodkod Transformation Failed for Predicate over: ',AllConstants),
275 %trace, apply_transformation3(AllConstants,Predicate,Equalities,Result),
276 fail).
277
278 apply_transformation3(AllConstants,Predicate,Equalities,Result) :-
279 restrict_to_used_constants(AllConstants,Predicate,Constants),
280 apply_rewriting_rules(Predicate,Rewritten),
281 extract_used_types(Rewritten,Types,Ints,Bits),
282 create_atoms_for_types(Types,Ints,Bits,Typemap,Idmap1,Valuemap),
283 % check if any types are used, if not Kodkod would exit with an
284 % empty universe exception
285 % (java.lang.IllegalArgumentException: Cannot create an empty universe. or something similar)
286 \+ empty_avl(Typemap),
287 typed_translation(Constants,Predicate,Bits,Typemap,Idmap1,Idmap,Rewritten,KExpr),
288
289 register_problem(Constants,KExpr,Idmap,Typemap,Valuemap,Predicate,ProblemNr),
290 create_texpr(kodkod(ProblemNr,Constants),pred,[],KPred),
291 conjunct_predicates([Equalities,KPred],Result).
292
293 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
294
295 print_results([]).
296 print_results([R|Rrest]) :-
297 print_result(R),nls,
298 print_results(Rrest).
299 print_result(ok(_Ids,Index,P,Ints,Bits)) :-
300 print_result(ok(Index,P,Ints,Bits)).
301 print_result(ok(_Index,P,Ints,Bits)) :-
302 (silent_mode(on) -> true
303 ; write('kodkod ok: '),print_bexpr_with_limit(P,50),
304 write(' ints: '),write(Ints),write(', intatoms: '),write(Bits)
305 ).
306 print_result(failure(_Ids,Index,P,Msg,Reason)) :-
307 print_result(failure(Index,P,Msg,Reason)).
308 print_result(failure(_Index,P,Msg,Reason)) :-
309 write('kodkod fail: '),
310 translate_bexpression_with_limit(P,50,PS), write(PS),
311 write(' , reason: '),write_reason(Reason),write(' while '),write(Msg),nl,
312 (get_preference(kodkod_raise_warnings,false) -> true
313 ; add_warning(kodkod,'Cannot translate predicate for Kodkod: ',PS,P)
314 ).
315 write_reason(kodkod_exception(KE)) :-
316 write_reason2(KE),!.
317 write_reason(E) :- write(E).
318
319 write_reason2(unsupported_type(T)) :-
320 pretty_type(T,PT),
321 write('unsupported type '),write(PT).
322 write_reason2(unsupported_expression(TE)) :-
323 get_texpr_expr(TE,T),
324 functor(T,Functor,Arity),
325 translate_bexpression(TE,PE),
326 format('unsupported expression ~w/~w: ~w',[Functor,Arity,PE]).
327 write_reason2(unsupported_int(Msg)) :-
328 write(Msg).
329 write_reason2(side_condition(Msg,PPExpr,Info)) :-
330 (extract_span_description(Info,Desc)
331 -> format('~w: ~w (~w)',[Msg,PPExpr, Desc])
332 ; format('~w: ~w',[Msg,PPExpr])).
333
334 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
335
336 :- dynamic user:portray/1.
337 :- public pdebug/0.
338 pdebug :-
339 install_b_portray_hook,
340 assertz(( user:portray(X) :- is_avl(X),!,portray_avl(X) )).