1 | % (c) 2015-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(model_translation, [translate_smt_model_to_b_values/4]). | |
6 | ||
7 | :- use_module(probsrc(module_information),[module_info/2]). | |
8 | :- module_info(group,smt_solvers). | |
9 | :- module_info(description,'This module translates the models found by an SMT-solvers to a ProB state.'). | |
10 | ||
11 | :- use_module(library(lists), [maplist/3,maplist/4, | |
12 | %convlist/3,delete/3, | |
13 | is_list/1]). | |
14 | :- use_module(library(avl)). | |
15 | ||
16 | :- use_module(probsrc(translate), [translate_bvalue/2]). | |
17 | :- use_module(probsrc(tools), [arg_is_number/2, | |
18 | split_atom/3, | |
19 | ajoin/2]). | |
20 | :- use_module(probsrc(tools_strings), [convert_to_number/2]). | |
21 | :- use_module(probsrc(error_manager), [add_error_fail/3]). | |
22 | :- use_module(probsrc(bsyntaxtree), [safe_create_texpr/3, | |
23 | unique_typed_id/3, | |
24 | %conjunct_predicates/2, | |
25 | get_texpr_type/2, | |
26 | get_texpr_id/2, | |
27 | %create_implication/3, | |
28 | %create_negation/2, | |
29 | replace_id_by_expr/4]). | |
30 | :- use_module(probsrc(custom_explicit_sets), [try_expand_custom_set_to_list/4]). | |
31 | :- use_module(probsrc(b_global_sets), [b_type2_set/2]). | |
32 | ||
33 | %:- use_module(probsrc(self_check), [assert_must_succeed/1]). | |
34 | ||
35 | :- use_module(solver_dispatcher). | |
36 | ||
37 | translate_smt_model_to_b_values(Solver,State,Identifiers,Bindings) :- | |
38 | maplist(translate_smt_model_to_b_value(Solver,State),Identifiers,Bindings). | |
39 | ||
40 | translate_smt_model_to_b_value(Solver,State,b(identifier(Id),Type,_Infos),binding(Id,Value,PPValue)) :- | |
41 | member(id(Id,Expr),State), | |
42 | smt_solver_interface_call(Solver,get_string(Expr,String)), !, | |
43 | atom_codes(String,Codes), | |
44 | % format('Result of get_string: ~s~n',[Codes]), | |
45 | % trace, | |
46 | lisp_style_expression(E,Codes,[]), !, | |
47 | (Solver == cvc4 -> translate_cvc4_tree(E,Type,Value) ; | |
48 | Solver == z3 -> translate_z3_tree(Id,E,Type,Value) ; | |
49 | otherwise -> fail), | |
50 | ||
51 | (translate_bvalue(Value,PPValue) -> true ; PPValue='**pretty-print failed**'). | |
52 | ||
53 | translate_z3_tree(Id,Id,Type,Result) :- !, | |
54 | % variable is not assigned (hence z3 returns its name) | |
55 | % just ground it somehow | |
56 | z3_ground_result(Type,Result). | |
57 | translate_z3_tree(Id,EscapedId,Type,Result) :- | |
58 | % the id might have been escaped in z3 (e.g. due to ticks) | |
59 | ajoin(['|',Id,'|'],EscapedId), !, | |
60 | % variable is not assigned (hence z3 returns its name) | |
61 | % just ground it somehow | |
62 | z3_ground_result(Type,Result). | |
63 | translate_z3_tree(_,E,Type,Result) :- | |
64 | translate_z3_tree(E,Type,Result). | |
65 | translate_z3_tree(['-',Number],integer,int(X)) :- !, | |
66 | X is -Number. | |
67 | translate_z3_tree(Number,integer,int(Number)). | |
68 | translate_z3_tree(Number,global(Set),fd(ResNumber,Set)) :- | |
69 | integer(Number), !, | |
70 | ResNumber is Number + 1. | |
71 | translate_z3_tree(Number,global(Set),fd(ResNumber,Set)) :- | |
72 | split_atom(Number,['!'],[Set,val,InternalNumber]), | |
73 | convert_to_number(InternalNumber,Nr), | |
74 | ResNumber is Nr + 1. | |
75 | translate_z3_tree(A,boolean,Res) :- | |
76 | (A == true -> Res = pred_true ; | |
77 | A == false -> Res = pred_false ; | |
78 | otherwise -> fail). | |
79 | translate_z3_tree([couple,A,B],couple(X,Y),(AT,BT)) :- | |
80 | translate_z3_tree(A,X,AT), | |
81 | translate_z3_tree(B,Y,BT). | |
82 | translate_z3_tree(['_','as-array',AuxFunName],set(X),Res) :- | |
83 | % set is represented by aux function | |
84 | % get and parse the full model | |
85 | smt_solver_interface_call(z3,get_full_model_string(FullModel)), | |
86 | % format('z3 full model:~n~w~n',[FullModel]), | |
87 | z3_model_to_avl(FullModel,AVL), !, | |
88 | z3_set_to_b_set(AuxFunName,X,AVL,Res). | |
89 | translate_z3_tree([store,Sub,Entry,true],set(X),ListOut) :- | |
90 | translate_z3_tree(Sub,set(X),SubEntries), | |
91 | translate_z3_tree(Entry,X,BEntry), | |
92 | sort([BEntry|SubEntries],ListOut). | |
93 | translate_z3_tree([[as,const,['Array',_,'Bool']],false],set(_),[]). | |
94 | translate_z3_tree([[as,const,['Array',_,'Bool']],true],set(Type),Res) :- | |
95 | b_type2_set(Type,Res). | |
96 | translate_z3_tree(['record'|Z3Fields],record(Fields),rec(FieldsOut)) :- | |
97 | maplist(translate_z3_record,Fields,Z3Fields,FieldsOut). | |
98 | translate_z3_tree([let,[[Id,Val]],Function],Type,Out) :- | |
99 | z3_replace_let_id_by_value(Id,Val,Function,NewFunction), | |
100 | translate_z3_tree(NewFunction,Type,Out). | |
101 | ||
102 | translate_z3_record(field(Name,BType),CVCVal,field(Name,BVal)) :- | |
103 | translate_z3_tree(CVCVal,BType,BVal). | |
104 | ||
105 | z3_ground_result(integer,int(0)). | |
106 | z3_ground_result(boolean,pred_true). | |
107 | z3_ground_result(couple(X,Y),(XG,YG)) :- | |
108 | z3_ground_result(X,XG), z3_ground_result(Y,YG). | |
109 | z3_ground_result(set(_),[]). | |
110 | z3_ground_result(record(Fields),rec(FieldsOut)) :- | |
111 | maplist(z3_ground_record_fields,Fields,FieldsOut). | |
112 | ||
113 | z3_ground_record_fields(field(Name,BType),field(Name,BVal)) :- | |
114 | z3_ground_result(BType,BVal). | |
115 | ||
116 | :- use_module(probsrc(b_interpreter),[b_compute_expression_nowf/4]). | |
117 | z3_set_to_b_set(FunName,ResType,AVL,ResultOut) :- | |
118 | avl_fetch(FunName,AVL,f([[ParamName,_ParamType]],_ReturnType,Tree)), | |
119 | ||
120 | safe_create_texpr(identifier(ParamName),ResType,IdA), | |
121 | unique_typed_id("tmp",boolean,IdB), | |
122 | z3_function_to_b_pred(Tree,Pred,IdA,IdB,AVL), | |
123 | unique_typed_id("tmp",boolean,IDPredType), | |
124 | safe_create_texpr(equal(IDPredType,Pred),pred,IsEqual), | |
125 | safe_create_texpr(comprehension_set([IdA,IDPredType],IsEqual),set(couple(ResType,boolean)),TheFunction), | |
126 | ||
127 | safe_create_texpr(function(TheFunction,IdA),boolean,FCall), | |
128 | safe_create_texpr(equal(b(boolean_true,boolean,[]),FCall),pred,NewNewPred), | |
129 | safe_create_texpr(comprehension_set([IdA],NewNewPred),set(ResType),CompSet), | |
130 | % translate:set_unicode_mode,translate:print_bexpr(CompSet), | |
131 | b_compute_expression_nowf(CompSet,[],[],Res), | |
132 | (try_expand_custom_set_to_list(Res,ResultOut,true,z3_set_to_b_set) | |
133 | -> true | |
134 | ; ResultOut = Res). | |
135 | z3_set_to_b_set(A,B,_,_) :- | |
136 | add_error_fail(model_translation, 'z3_set_to_b_set failed on fun / result pair', [A,B]). | |
137 | ||
138 | %z3_type_to_b_type('Int',integer). | |
139 | %z3_type_to_b_type('Bool',boolean). | |
140 | ||
141 | z3_function_to_b_pred([ite,[Op,_ParamName,Val],Result|Ifs],Pred,IdParam,IdReturn,AVL) :- !, | |
142 | z3_function_to_b_pred(Ifs,SubPred,IdParam,IdReturn,AVL), | |
143 | get_texpr_type(IdReturn,ReturnType), get_texpr_type(IdParam,ParamType), | |
144 | ||
145 | %translate_z3_tree(Result,ReturnType,Value), | |
146 | %safe_create_texpr(equal(IdReturn,b(value(Value),ReturnType,[])),pred,Then), | |
147 | z3_function_to_b_pred(Result,Then,IdParam,IdReturn,AVL), | |
148 | ||
149 | translate_z3_tree(Val,ParamType,Value2), | |
150 | (Op = '=' -> safe_create_texpr(equal(IdParam,b(value(Value2),ParamType,[])),pred,If) ; | |
151 | Op = '<=' -> safe_create_texpr(less_equal(IdParam,b(value(Value2),ParamType,[])),pred,If) ; | |
152 | Op = '>=' -> safe_create_texpr(greater_equal(IdParam,b(value(Value2),ParamType,[])),pred,If) ; | |
153 | otherwise -> fail), | |
154 | ||
155 | safe_create_texpr(if_then_else(If,Then,SubPred),ReturnType,Pred). | |
156 | z3_function_to_b_pred([let,[[Id,Val]],Function],Pred,IdParam,IdReturn,AVL) :- !, | |
157 | z3_replace_let_id_by_value(Id,Val,Function,NewFunction), | |
158 | z3_function_to_b_pred(NewFunction,Pred,IdParam,IdReturn,AVL). | |
159 | % unwraps lower levels | |
160 | z3_function_to_b_pred([X],Pred,IdParam,IdReturn,AVL) :- !, | |
161 | z3_function_to_b_pred(X,Pred,IdParam,IdReturn,AVL). | |
162 | % function composition | |
163 | z3_function_to_b_pred([X,ParamName],Pred,IdParam,IdReturn,AVL) :- % TODO Id return | |
164 | get_texpr_id(IdParam,ParamName), !, | |
165 | avl_fetch(X,AVL,f([[ParamName,_ParamType]],_ReturnType,XBody)), | |
166 | z3_function_to_b_pred(XBody,Pred,IdParam,IdReturn,AVL). | |
167 | z3_function_to_b_pred(['-',Int],Pred,_IdParam,_IdReturn,_AVL) :- !, | |
168 | translate_z3_tree(Int,integer,int(Value)), | |
169 | MValue is -Value, | |
170 | Pred = b(value(int(MValue)),integer,[]). | |
171 | z3_function_to_b_pred([X|Further],Pred,IdParam,IdReturn,AVL) :- !, | |
172 | get_texpr_type(IdParam,SubParamType), | |
173 | unique_typed_id("tmp",SubParamType,IdB), | |
174 | z3_function_to_b_pred(Further,FurtherPred,IdParam,IdB,AVL), | |
175 | ||
176 | avl_fetch(X,AVL,f([[_XParamName,_ParamType]],_ReturnType,XBody)), | |
177 | z3_function_to_b_pred(XBody,XPred,IdB,IdReturn,AVL), | |
178 | ||
179 | get_texpr_id(IdB,IdToReplace), | |
180 | replace_id_by_expr(XPred,IdToReplace,FurtherPred,Pred). | |
181 | z3_function_to_b_pred(SingleVal,Pred,_,IdReturn,_) :- | |
182 | get_texpr_type(IdReturn,ReturnType), | |
183 | translate_z3_tree(SingleVal,ReturnType,Value), | |
184 | Pred = b(value(Value),ReturnType,[]). | |
185 | ||
186 | z3_replace_let_id_by_value(Id,Val,Function,NewFunction) :- | |
187 | is_list(Function), !, | |
188 | maplist(z3_replace_let_id_by_value(Id,Val),Function,NewFunction). | |
189 | z3_replace_let_id_by_value(Id,Val,Function,NewFunction) :- | |
190 | atomic(Function), !, | |
191 | Id = Function -> NewFunction = Val ; NewFunction = Function. | |
192 | ||
193 | z3_model_to_avl(FullModel,AVL) :- | |
194 | atom_codes(FullModel,Codes), | |
195 | lisp_style_expressions(E,Codes,[]), | |
196 | z3_lisp_to_avl(E,AVL). | |
197 | ||
198 | z3_lisp_to_avl(E,AVL) :- | |
199 | empty_avl(In), | |
200 | z3_lisp_to_avl(E,In,AVL). | |
201 | ||
202 | z3_lisp_to_avl([],A,A). | |
203 | z3_lisp_to_avl([['define-fun',Name,Param,Return,Tree]|T],AIn,AOut) :- | |
204 | avl_store(Name,AIn,f(Param,Return,Tree),ATemp), | |
205 | z3_lisp_to_avl(T,ATemp,AOut). | |
206 | % currently I think I do not need these facts... | |
207 | % as far as I understand they represent enumerated set Elements | |
208 | z3_lisp_to_avl([['declare-fun',_Name,_Params,_Type0]|T],AIn,AOut) :- | |
209 | z3_lisp_to_avl(T,AIn,AOut). | |
210 | % these occur for cardinality constraints | |
211 | z3_lisp_to_avl([['forall',_Vars,_Pred]|T],AIn,AOut) :- | |
212 | z3_lisp_to_avl(T,AIn,AOut). | |
213 | ||
214 | translate_cvc4_tree(['CONST_RATIONAL',Arg],integer,int(Val)) :- | |
215 | arg_is_number(Arg,Val). | |
216 | translate_cvc4_tree(['CONST_BOOLEAN',1],boolean,pred_true). | |
217 | translate_cvc4_tree(['CONST_BOOLEAN',0],boolean,pred_false). | |
218 | translate_cvc4_tree(['CONST_STRING',Content],string,string(Content)). | |
219 | translate_cvc4_tree(['SINGLETON',ValIn],set(X),[ValOut]) :- | |
220 | translate_cvc4_tree(ValIn,X,ValOut). | |
221 | translate_cvc4_tree(['EMPTYSET',emptyset,_Type],set(_),[]). | |
222 | translate_cvc4_tree(['TUPLE',V1,V2],couple(Type1,Type2),(TV1,TV2)) :- | |
223 | translate_cvc4_tree(V1,Type1,TV1), | |
224 | translate_cvc4_tree(V2,Type2,TV2). | |
225 | translate_cvc4_tree(['APPLY_CONSTRUCTOR','__cvc4_tuple_ctor',V1,V2],couple(Type1,Type2),(TV1,TV2)) :- | |
226 | translate_cvc4_tree(V1,Type1,TV1), | |
227 | translate_cvc4_tree(V2,Type2,TV2). | |
228 | translate_cvc4_tree(['UNION',V1,V2],set(X),Val) :- | |
229 | translate_cvc4_tree(V1,set(X),TV1), | |
230 | translate_cvc4_tree(V2,set(X),TV2), | |
231 | append(TV1,TV2,Val). | |
232 | translate_cvc4_tree(['UNINTERPRETED_CONSTANT',C],global(SId),fd(PBCId,SId)) :- | |
233 | atom_codes(C,CCodes), | |
234 | parse_uc(CId,CCodes,[]), | |
235 | PBCId is CId + 1. | |
236 | translate_cvc4_tree(['RECORD',_CVCRecordType|Fields],record(RFields),rec(FieldsOut)) :- | |
237 | maplist(translate_cvc4_record,RFields,Fields,FieldsOut). | |
238 | ||
239 | translate_cvc4_record(field(Name,BType),CVCVal,field(Name,BVal)) :- | |
240 | translate_cvc4_tree(CVCVal,BType,BVal). | |
241 | ||
242 | parse_uc(Id) --> | |
243 | "uc__SORT_TYPE_var_", number(_), | |
244 | "__", number(N), {number_codes(Id,N)}. | |
245 | ||
246 | lisp_style_expressions([E|Es]) --> | |
247 | ws, lisp_style_expression(E), ws, !, | |
248 | lisp_style_expressions(Es). | |
249 | lisp_style_expressions([]) --> ws, []. | |
250 | lisp_style_expressions(_,In,_) :- | |
251 | format("lisp-style parser failed on: ~s~n",[In]),fail. | |
252 | ||
253 | ws --> [W], {W = 32 ; W = 10 ; W = 13}, ws. | |
254 | ws --> ";;", any_but_newline. | |
255 | ws --> []. | |
256 | any_but_newline --> [C], {C \= 10}, any_but_newline ; "\n", ws. | |
257 | ||
258 | lisp_style_expression(A) --> non_empty_symbol(Cs), {atom_codes(A, Cs)}. | |
259 | lisp_style_expression(N) --> number(Cs), {number_codes(N, Cs)}. | |
260 | lisp_style_expression(N) --> "-", number(Cs), {number_codes(N2,Cs), N is -N2}. | |
261 | lisp_style_expression(A) --> string(Codes), {atom_codes(A,Codes)}. | |
262 | lisp_style_expression(List) --> "(", lisp_style_expressions(List), ")". | |
263 | lisp_style_expression(record_type(Fields)) --> | |
264 | "[#", ws, record_type_fields(Fields), ws, "#]". | |
265 | ||
266 | record_type_fields([F|Fields]) --> | |
267 | record_type_field(F), ws, ",", ws, record_type_fields(Fields). | |
268 | record_type_fields([F]) --> record_type_field(F). | |
269 | ||
270 | record_type_field(field(NameA,TypeA)) --> | |
271 | non_empty_symbol(Name), ":(TYPE_CONSTANT ", non_empty_symbol(Type), " type)", | |
272 | {atom_codes(NameA,Name),atom_codes(TypeA,Type)}. | |
273 | ||
274 | number([D|Ds]) --> digit(D), number(Ds). | |
275 | number([D]) --> digit(D). | |
276 | ||
277 | digit(D) --> [D], {48 =< D, D =< 57}. | |
278 | ||
279 | string(Codes) --> "\"", non_empty_symbol(Codes), "\"". | |
280 | ||
281 | non_empty_symbol([A|As]) --> | |
282 | [A], | |
283 | { 65 =< A, A =< 90 | |
284 | ; 97 =< A, A =< 122 | |
285 | % ; 48 =< A, A =< 57 | |
286 | ; A = 124 % "|" | |
287 | ; A = 95 % "_" | |
288 | ; A = 45 % "-" | |
289 | ; A = 39 % "'" | |
290 | ; A = 33 % "!" | |
291 | ; 60 =< A, A =< 62 % "<", "=", ">" | |
292 | }, | |
293 | symbol(As). | |
294 | ||
295 | symbol([A|As]) --> | |
296 | [A], | |
297 | { 65 =< A, A =< 90 | |
298 | ; 97 =< A, A =< 122 | |
299 | ; 48 =< A, A =< 57 | |
300 | ; A = 124 % "|" | |
301 | ; A = 95 % "_" | |
302 | ; A = 45 % "-" | |
303 | ; A = 39 % "'" | |
304 | ; A = 33 % "!" | |
305 | ; 60 =< A, A =< 62 % "<", "=", ">" | |
306 | }, | |
307 | symbol(As). | |
308 | symbol([]) --> "". |