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([]) --> "".