1		% (c) 2015-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		:- module(model_translation, [translate_smt_model_to_b_values/4,
6		store_explicit_set_unique_id/2,
7		consistent_deferred_set_sizes/0,
8		assert_virtual_deferred_set_id/2,
9		clear_translation_state/0]).
10
11		:- use_module(library(lists), [maplist/3,maplist/4,
12		append/2,select/3,max_member/2]).
13		:- use_module(library(avl)).
14		:- use_module(library(codesio), [read_from_codes/2]).
15
16		:- use_module(probsrc(preferences), [get_preference/2]).
17		:- use_module(probsrc(b_ast_cleanup), [clean_up/3]).
18		:- use_module(probsrc(translate), [translate_bvalue/2]).
19		:- use_module(probsrc(tools), [arg_is_number/2,split_atom/3,atom_to_number/2,ajoin/2]).
20		:- use_module(probsrc(tools_strings), [convert_to_number/2, atom_prefix/2]).
21		:- use_module(probsrc(error_manager),[]).
22		:- use_module(probsrc(tools),[]).
23		:- use_module(probsrc(error_manager), [add_error/3,add_error/4,
24		add_internal_error/2,add_error_fail/3,check_error_occured/2]).
25		:- use_module(probsrc(bsyntaxtree), [safe_create_texpr/3,
26		create_texpr/4,
27		unique_typed_id/3,
28		create_equality/3,
29		conjunction_to_list/2,
30		conjunct_predicates/2,
31		disjunct_predicates/2,
32		get_texpr_type/2,
33		find_identifier_uses/3,
34		create_negation/2]).
35		:- use_module(probsrc(custom_explicit_sets), [try_expand_custom_set_to_list/4]).
36		:- use_module(probsrc(b_global_sets), [b_global_deferred_set/1, b_global_set/1, b_type2_set/2, global_type/2, get_user_defined_scope/4, unfixed_deferred_set/1]).
37		:- use_module(probsrc(b_interpreter),[b_test_boolean_expression_cs/5, b_compute_expression_nowf/6]).
38
39		%:- use_module(probsrc(self_check), [assert_must_succeed/1]).
40
41		:- use_module(solver_dispatcher).
42
43		:- use_module(probsrc(module_information),[module_info/2]).
44		:- module_info(group,smt_solvers).
45		:- module_info(description,'This module translates the models found by an SMT-solvers to a ProB state.').
46
47		:- set_prolog_flag(double_quotes, codes).
48
49		:- dynamic explicit_set_cache/2, fd_var_of_z3/2, virtual_deferred_set_id/2, linecount/1.
50
51		clear_translation_state :-
52		retractall(virtual_deferred_set_id(_,_)),
53		retractall(fd_var_of_z3(_,_)),
54		retractall(explicit_set_cache(_, _)).
55
56		assert_virtual_deferred_set_id(EnumElm, FdVar) :-
57		asserta(virtual_deferred_set_id(EnumElm, FdVar)).
58
59		% Store explicit sets for universally quantified translations to prevent vanishing type information
60		% when translating universal quantifiers from SMT-Lib to B (e.g., for general_intersection).
61		store_explicit_set_unique_id(SetAst, UniqueIdName) :-
62		get_texpr_type(SetAst, Type),
63		unique_typed_id("inner_set", Type, UniqueId),
64		UniqueId = b(identifier(UniqueIdName),_,_),
65		asserta(explicit_set_cache(UniqueIdName, SetAst)).
66
67		%% consistent_deferred_set_sizes.
68		% We collect all global FD variables during the translation of a model found by Z3 to
69		% check if the considered deferred set size (maximum of all global FD variables) is smaller
70		% than the value considered by ProB (preference DEFAULT_SETSIZE).
71		% If such models are refuted, Z3 behaves as ProB.
72		% Otherwise, we might translate a solution using less global FD variables than defined by ProB.
73		consistent_deferred_set_sizes :-
74		findall(DS, (b_global_deferred_set(DS), unfixed_deferred_set(DS)), DeferredSets),
75		consistent_deferred_set_sizes(DeferredSets).
76
77		%% consistent_deferred_set_sizes(DeferredSets).
78		consistent_deferred_set_sizes([]).
79		consistent_deferred_set_sizes([DeferredSet|T]) :-
80		findall(FdVarOfZ3, retract(fd_var_of_z3(DeferredSet,FdVarOfZ3)), FdVarsOfZ3),
81		FdVarsOfZ3 \== [],
82		!,
83		max_member(MaxFdVarOfZ3, FdVarsOfZ3),
84		( get_user_defined_scope(DeferredSet,Low,Up,_Span)
85		-> DeferredSetSize is 1+Up-Low
86		; get_preference(globalsets_fdrange, DeferredSetSize)
87		),
88		% the case for MaxFdVarOfZ3 > DeferredSetSize is already handled in handle_globalsets_fdrange_contradiction
89		MaxFdVarOfZ3 == DeferredSetSize,
90		consistent_deferred_set_sizes(T).
91		consistent_deferred_set_sizes([_|T]) :-
92		% this deferred set is not part of the solution and can be ignored
93		consistent_deferred_set_sizes(T).
94
95		translate_smt_model_to_b_values(Solver,State,Identifiers,Bindings) :-
96	?	get_full_model_as_avl(Solver,AVL), % parse it only once for all identifiers
97	?	maplist(translate_smt_model_to_b_value(Solver,State,AVL),Identifiers,Bindings).
98
99		translate_smt_model_to_b_value(Solver,State,FullModelAVL,
100		b(identifier(Id),Type,_Infos),binding(Id,Value,PPValue)) :-
101	?	member(id(Id,Expr),State),
102		smt_solver_interface_call(Solver,get_model_string(Expr,String)), !,
103		atom_codes(String,Codes),
104		%format('Result of get_model_string:~n~s~n---~n',[Codes]),
105		parse_lisp_style_expressions([E],Codes,[]), !,
106		(Solver == cvc4 -> translate_cvc4_tree(E,Type,Value) ;
107	?	Solver == z3 -> translate_z3_tree_for_id(Id,E,FullModelAVL,Type,Value) ;
108		fail),
109
110		(translate_bvalue(Value,PPValue) -> true ; PPValue='**pretty-print failed**').
111
112		translate_z3_tree_for_id(Id,EscapedId,_,Type,Result) :-
113		% the id might have been escaped in z3 (e.g. due to ticks)
114		ajoin(['|',Id,'|'],EscapedId), !,
115		% variable is not assigned (hence z3 returns its name)
116		% just ground it somehow
117		z3_ground_result(Type,Result).
118		translate_z3_tree_for_id(_,E,FullModelAVL,Type,Result) :-
119	?	translate_z3_tree_and_check(E,FullModelAVL,Type,Result,translate_z3_tree4).
120
121
122		translate_z3_record(Env, field(Name,BType), CVCVal, field(Name,BVal)) :-
123		translate_z3_expr(CVCVal, Env, BType, BVal).
124
125		% -----------------------------
126
127		% performs additional sanity check of computed values:
128		translate_z3_tree_and_check(SingleVal,FullModelAVL,ReturnType,Value,PP) :-
129	?	translate_z3_tree_aux(SingleVal,FullModelAVL,ReturnType,Value),
130		check_value(ReturnType,Value,SingleVal,PP).
131
132		translate_z3_tree_aux(Tree,FullModelAVL,boolean,Res) :-
133		% Z3 might return a quantifier for Boolean values since version 4.12.0
134		!,
135		translate_z3_predicate(Tree,env([],FullModelAVL),BPred),
136		( b_test_boolean_expression_cs(BPred, [], [],'translating Z3 Boolean value',0)
137		-> Res = pred_true
138		; Res = pred_false
139		).
140		translate_z3_tree_aux(Tree,FullModelAVL,Type,Res) :-
141	?	translate_z3_expr(Tree,env([],FullModelAVL),Type,BExpr),
142		b_compute_expression_nowf(BExpr,[],[],Res,'translating Z3 value',0).
143
144		check_value(_,identifier(A),_,_) :- atom(A),!.
145		check_value(integer,I,SV,PP) :- \+ (I=int(Nr), number(Nr)),!,
146		add_internal_error('Illegal Z3 value, not number computed:', PP:SV:I), fail.
147		check_value(boolean,B,SV,PP) :- B \= pred_true , B\= pred_false, !,
148		add_internal_error('Illegal Z3 value, not boolean computed:', PP:SV:B), fail.
149		check_value(_,_,_,_).
150
151		%% get_typing_predicates(+BVars, -TypingPredList).
152		% Create typing predicates for variables either from explicit_set_cache/2
153		% or more generally using generate_typing_predicates/2.
154		get_typing_predicates(BVars, TypingPredList) :-
155		get_typing_predicates(BVars, [], [], TypingPredList).
156
157		get_typing_predicates([], NotCached, Acc, TypingPredList) :-
158		translate:generate_typing_predicates(NotCached, TTypingPredList),
159		append(Acc, TTypingPredList, TypingPredList).
160		get_typing_predicates([BVar|T], NotCached, Acc, TypingPredList) :-
161		BVar = b(identifier(IdName),_,_),
162		explicit_set_cache(IdName, ExplicitSet),
163		!,
164		TypingPred = b(member(BVar,ExplicitSet),pred,[]),
165		get_typing_predicates(T, NotCached, [TypingPred|Acc], TypingPredList).
166		get_typing_predicates([BVar|T], NotCached, Acc, TypingPredList) :-
167		get_typing_predicates(T, [BVar|NotCached], Acc, TypingPredList).
168
169		is_global_type_variable_name(env(Ids,_), VarName, GlobalType) :-
170	?	member(b(identifier(VarName),GlobalType,_), Ids),
171		GlobalType = global(_).
172		is_global_type_variable_name(_, VarName, global(Set)) :-
173		split_atom(VarName, ['!'], [Set,_,_]),
174		b_global_set(Set).
175
176		% enumerated and deferred sets are translated as integers
177		% we have to check for global types to identify integers as such, see e.g. (= 0 c) where c is a global type variable
178		typecheck_for_global_type(Left, _, Env, Type) :-
179		atom(Left),
180		is_global_type_variable_name(Env, Left, GlobalType),
181		!,
182		Type = GlobalType.
183		typecheck_for_global_type(_, Right, Env, Type) :-
184		atom(Right),
185		is_global_type_variable_name(Env, Right, GlobalType),
186		!,
187		Type = GlobalType.
188		typecheck_for_global_type(_, _, _, _). % no global type; use a variable which is set afterwards
189
190		% -------------------------------
191
192		% TODO: do we really need this function anymore:
193		translate_z3_expr_using_full_model(Expr,Type,Result) :-
194		get_full_model_as_avl(z3,AVL),
195		translate_z3_expr(Expr,env([],AVL),Type,Result).
196
197		get_full_model_as_avl(z3,AVL) :- !,
198		% get and parse the full model
199		smt_solver_interface_call(z3,get_full_model_string(FullModel)),
200		%format('z3 full model:~n~w~n',[FullModel]),
201	?	z3_model_to_avl(FullModel,AVL).
202		get_full_model_as_avl(_,AVL) :- empty_avl(AVL).
203
204		map_translate_z3_predicate([], _, Acc, Acc).
205		map_translate_z3_predicate([Z3Pred|T], Env, Acc, Preds) :-
206	?	translate_z3_predicate(Z3Pred, Env, Pred),
207	?	map_translate_z3_predicate(T, Env, [Pred|Acc], Preds).
208
209		translate_z3_quantified_vars([], _, Acc, Acc).
210		translate_z3_quantified_vars([[Name,Type]|T], Env, Acc, Preds) :-
211		z3_type_to_b_type(Type,BType),
212		Id = b(identifier(Name),BType,[]),
213		translate_z3_quantified_vars(T, Env, [Id|Acc], Preds).
214
215		% translate a z3 predicate to a B AST predicate
216		translate_z3_predicate([not,Left], Env, Res) :-
217		!,
218		translate_z3_predicate(Left, Env, TL),
219		create_negation(TL,Res).
220		translate_z3_predicate([ZOP|T], Env, Res) :-
221		z3_connective_to_b(ZOP, BOP),
222		!,
223	?	translate_z3_connective(BOP, T, Env, Res).
224		translate_z3_predicate([let,[[Id,Val]],Function], Env, Res) :-
225		!,
226		z3_replace_let_id_by_value(Id, Val, Function, NewFunction),
227	?	translate_z3_predicate(NewFunction, Env, Res).
228		translate_z3_predicate([let,[[Id,Val]|T],Function], Env, Res) :-
229		!,
230		T \== [],
231		z3_replace_let_id_by_value(Id, Val, Function, NewFunction),
232		translate_z3_predicate([let,T,NewFunction], Env, Res).
233		translate_z3_predicate([=,Left,Right], Env, Res) :-
234		!,
235		typecheck_for_global_type(Left, Right, Env, Type),
236	?	translate_z3_expr(Left, Env, Type, TL),
237	?	translate_z3_expr(Right, Env, Type, TR),
238		create_equality(TL,TR,Res).
239		translate_z3_predicate([ZOP,Left,Right], Env, Res) :-
240		z3_integer_comparison(ZOP, BOP),
241		!,
242		translate_z3_expr(Left, Env, IntegerOrReal, TL),
243		translate_z3_expr(Right, Env, IntegerOrReal, TR),
244		Pred =.. [BOP,TL,TR],
245		safe_create_texpr(Pred,pred,Res).
246		translate_z3_predicate([select,Array,Entry], Env, Res) :-
247		!,
248		translate_z3_expr(Array, Env, _, BSet),
249	?	translate_z3_expr(Entry, Env, _, BEntry),
250		Res = b(member(BEntry,BSet),pred,[]).
251		translate_z3_predicate([exists,Vars,[Body]], Env, Res) :-
252		translate_z3_quantified_vars(Vars, Env, [], BVars),
253		Env = env(Ids,AVL),
254		append(Ids, BVars, NewIds),
255	?	translate_z3_predicate(Body, env(NewIds,AVL), BBody),
256		!,
257		find_identifier_uses(BBody, [], UsedIds),
258		Res = b(exists(BVars,BBody),pred,[used_ids(UsedIds)]).
259		translate_z3_predicate([exists,Vars,Body], Env, Res) :-
260		translate_z3_quantified_vars(Vars, Env, [], BVars),
261		Env = env(Ids,AVL),
262		append(Ids, BVars, NewIds),
263		translate_z3_predicate(Body, env(NewIds,AVL), BBody),
264		!,
265		find_identifier_uses(BBody, [], UsedIds),
266		Res = b(exists(BVars,BBody),pred,[used_ids(UsedIds)]).
267		translate_z3_predicate([forall,Vars,[Body]], Env, Res) :-
268		translate_z3_quantified_vars(Vars, Env, [], BVars),
269		Env = env(Ids,AVL),
270		append(Ids, BVars, NewIds),
271		translate_z3_predicate(Body, env(NewIds,AVL), BBody),
272		!,
273		find_identifier_uses(BBody, [], UsedIds),
274		get_typing_predicates(BVars, TypingPredList),
275		conjunct_predicates(TypingPredList, TypingPred),
276		Res = b(forall(BVars,TypingPred,BBody),pred,[used_ids(UsedIds)]).
277		translate_z3_predicate([forall,Vars,Body], Env, Res) :-
278		translate_z3_quantified_vars(Vars, Env, [], BVars),
279		Env = env(Ids,AVL),
280		append(Ids, BVars, NewIds),
281		translate_z3_predicate(Body, env(NewIds,AVL), BBody),
282		!,
283		find_identifier_uses(BBody, [], UsedIds),
284		get_typing_predicates(BVars, TypingPredList),
285		conjunct_predicates(TypingPredList, TypingPred),
286		Res = b(forall(BVars,TypingPred,BBody),pred,[used_ids(UsedIds)]).
287		translate_z3_predicate([ite, Test, Left, Right], Env, Res) :- !,
288		translate_z3_predicate(Test,Env, BTest),
289	?	translate_z3_predicate(Left, Env, BThen),
290	?	translate_z3_predicate(Right,Env, BElse),
291		safe_create_texpr(convert_bool(BThen),boolean,BThenBool),
292		safe_create_texpr(convert_bool(BElse),boolean,BElseBool),
293		safe_create_texpr(if_then_else(BTest,BThenBool,BElseBool),boolean,TRes),
294		Res = b(equal(TRes,b(boolean_true,boolean,[])),pred,[]).
295		translate_z3_predicate(In, Env, Res) :-
296		translate_z3_expr(In, Env, boolean, TRes),
297		!,
298		% expr to pred
299		Res = b(equal(TRes,b(boolean_true,boolean,[])),pred,[]).
300		translate_z3_predicate(Pred,_,_) :-
301		add_error_fail(translate_z3_predicate, 'Missing translation for Z3 predicate:', Pred).
302
303		% see also smt_id_to_prob_id_preds in smtlib_solver
304		z3_connective_to_b(and, conjunct).
305		z3_connective_to_b(or, disjunct).
306		z3_connective_to_b('=>', implication).
307
308		% see also smt_id_to_prob_id in smtlib_solver
309		z3_integer_comparison(<=, less_equal).
310		z3_integer_comparison(<, less).
311		z3_integer_comparison(>, greater). % not used ?
312		z3_integer_comparison(>=, greater_equal). % not used ?
313
314		%% create_nested_binary_expr(+BOP, +Env, +Type, +TypeA, +TypeB, Args, BExpr).
315		% Z3 model might contain for instance [*,x,x,x] which needs to
316		% be nested using binary operators in B.
317		create_nested_binary_expr(BOP, Env, Type, TA, TB, [Arg1,Arg2|T], Expr) :-
318		translate_z3_expr(Arg1, Env, TA, TArg1),
319		get_texpr_type(TArg1, TA),
320	?	translate_z3_expr(Arg2, Env, TB, TArg2),
321		get_texpr_type(TArg2, TB),
322		TExpr =.. [BOP,TArg1,TArg2],
323		Acc = b(TExpr,Type,[]),
324	?	create_nested_binary_expr(BOP, Env, Type, TA, TB, Acc, T, Expr).
325
326		create_nested_binary_expr(_, _, _, _, _, Acc, [], Acc).
327		create_nested_binary_expr(BOP, Env, Type, _, TB, Acc, [Arg], Expr) :-
328		!,
329		translate_z3_expr(Arg, Env, TB, TArg),
330		TExpr =.. [BOP,Acc,TArg],
331		Expr = b(TExpr,Type,[]).
332		create_nested_binary_expr(BOP, Env, Type, TA, TB, Acc, [Arg|T], Expr) :-
333		translate_z3_expr(Arg, Env, TA, TArg),
334		TExpr =.. [BOP,Acc,TArg],
335		NAcc = b(TExpr,Type,[]),
336		create_nested_binary_expr(BOP, Env, Type, TA, TB, NAcc, T, Expr).
337
338		map_translate_z3_expr([], _, Acc, Acc).
339		map_translate_z3_expr([Z3Pred|T], Env, Acc, Preds) :-
340	?	translate_z3_expr(Z3Pred, Env, _, Pred),
341	?	map_translate_z3_expr(T, Env, [Pred|Acc], Preds).
342
343		handle_globalsets_fdrange_contradiction(Z3sResNumber,Set) :-
344		get_user_defined_scope(Set,Low,Up,Span),!,
345		DeferredSetSize is 1+Up-Low,
346		Z3sResNumber > DeferredSetSize,
347		add_error(translate_z3_expr_globalsets_fdrange,
348		'Z3\'s solution contradicts the size set for the deferred set. Try to increase the set size by adapting the DEFINITION or -card command-line argument.',
349		z3:Z3sResNumber:Set:DeferredSetSize,Span),
350		fail.
351		handle_globalsets_fdrange_contradiction(Z3sResNumber,_Set) :-
352		get_preference(globalsets_fdrange, DeferredSetSize),
353		( Z3sResNumber > DeferredSetSize
354		-> % Z3 does not consider globalsets_fdrange; its solution might contradict ProB's preference
355		add_error_fail(translate_z3_expr_globalsets_fdrange,
356		'Z3\'s solution contradicts ProB\'s preference DEFAULT_SETSIZE. Try to increase the preference.',
357		z3:Z3sResNumber:'DEFAULT_SETSIZE':DeferredSetSize)
358		; % this is any other bug and should not happen
359		fail
360		).
361
362		% translate a z3 expression to a B AST expression
363		%translate_z3_expr(Pred,E,T,_) :- print(translate_z3_expr(Pred,E,T)),nl,fail.
364		translate_z3_expr(['-',Number],_,integer,Res) :-
365		!,
366		Number1 is -Number,
367		Res=b(integer(Number1),integer,[]).
368		translate_z3_expr(Int,_,integer,Res) :- integer(Int),!, Res=b(integer(Int),integer,[]).
369		translate_z3_expr(true,_,boolean,Res) :- !, Res=b(boolean_true,boolean,[]).
370		translate_z3_expr(false,_,boolean,Res) :- !, Res=b(boolean_false,boolean,[]).
371		translate_z3_expr([ZOP|T], Env, boolean, Res) :-
372		z3_connective_to_b(ZOP, BOP),
373		!,
374		translate_z3_connective(BOP, T, Env, PredRes),
375		Res = b(convert_bool(PredRes),boolean,[]).
376		translate_z3_expr(['-',RealAtom], Env, real, Res) :-
377		atom(RealAtom),
378		atom_concat('-', RealAtom, NRealAtom),
379		translate_z3_expr(NRealAtom, Env, real, Res).
380		translate_z3_expr(Atom, _, Type, Res) :-
381		atom(Atom),
382	?	virtual_deferred_set_id(Atom, FdVar),
383		FdVar = fd(_,DefSet),
384		Type = global(DefSet),
385		!,
386		Res = b(value(FdVar),Type,[]).
387		translate_z3_expr(Atom, _, Type, Res) :-
388		atom(Atom),
389		( ( split_atom(Atom,['!'],Splitted),
390		Splitted = [Set,val,InternalNumber]
391		)
392		-> Type = global(Set),
393		!,
394		convert_to_number(InternalNumber,Nr),
395		ResNumber is Nr + 1,
396		Val = fd(ResNumber,Set),
397		asserta(fd_var_of_z3(Set,ResNumber)),
398		( global_type(Val,Set)
399		-> true
400		; handle_globalsets_fdrange_contradiction(ResNumber,Set)
401		),
402		safe_create_texpr(value(Val), global(Set), Res)
403		; % atom could represent a real number
404		Type = real,
405	?	atom_to_number(Atom, Real),
406		float(Real), !,
407		safe_create_texpr(real(Atom), real, Res)
408		).
409		translate_z3_expr(Nr,_,global(GS),Res) :- number(Nr),!, % Z3 represents first element of GS by 0, ...
410		Nr1 is Nr+1, Val = fd(Nr1,GS),
411		asserta(fd_var_of_z3(GS,Nr1)),
412		( global_type(Val,GS)
413		-> true
414		; handle_globalsets_fdrange_contradiction(Nr1,GS)
415		),
416		safe_create_texpr(value(Val), global(GS), Res).
417		translate_z3_expr([Couple,A,B],Env,couple(T1,T2),b(couple(AT,BT),couple(T1,T2),[])) :-
418		atom(Couple),
419	?	get_couple_type_from_atom(Couple, T1, T2),
420	?	translate_z3_expr(A, Env, T1, AT),
421	?	translate_z3_expr(B, Env, T2, BT).
422		translate_z3_expr([CouplePrj,Arg], Env, Type, Res) :-
423		atom(CouplePrj),
424		translate_z3_expr(Arg, Env, _, RArg),
425		get_texpr_type(RArg, CType),
426		( atom_prefix('get_x_couple', CouplePrj),
427		PrjNode = first_of_pair(RArg),
428		CType = couple(ResType,_)
429		; atom_prefix('get_y_couple', CouplePrj),
430		PrjNode = second_of_pair(RArg),
431		CType = couple(_,ResType)
432		),
433		!,
434		Type = ResType,
435		safe_create_texpr(PrjNode, ResType, Res).
436		translate_z3_expr(Id, env(Env,_AVL), Type, Res) :-
437		atom(Id),
438		TId = b(identifier(Id),Type,_),
439	?	member(TId, Env),
440		!,
441		Res = TId.
442		translate_z3_expr(Id, _, Type, Res) :-
443		atom(Id),
444		Type = global(_),
445		% global ids which are not in the environment
446		!,
447		safe_create_texpr(identifier(Id), Type, Res).
448		translate_z3_expr(CstFunc,env(Env,AVL),Type,CompSet) :- atom(CstFunc),
449		Type = set(couple(PType,RType)),
450		avl_fetch(CstFunc,AVL,'z3-define-fun'([[ParamName,ParameterType]],ReturnType,BodyTree)),
451		z3_type_to_b_type(ParameterType,PType), % check if type matches
452		z3_type_to_b_type(ReturnType,RType), % ditto
453		!,
454		PID = b(identifier(ParamName),PType,[]),
455		%print(translate_body(CstFunc,PID)),nl,
456		translate_z3_expr(BodyTree,env([PID|Env],AVL),RType,BodyExpr),
457		%print(body(CstFunc)),translate:print_bexpr(BodyExpr),nl,
458		unique_typed_id("lambda",RType,LambdaID),
459		create_equality(LambdaID,BodyExpr,CPred),
460		% {PID,lambda | lambda = BodyExpr}
461		safe_create_texpr(comprehension_set([PID,LambdaID],CPred), set(couple(PType,RType)), CompSet).
462		translate_z3_expr([CstFunc,Arg],env(Env,AVL),Type,Res) :- % function application
463		avl_fetch(CstFunc,AVL,'z3-define-fun'([[ParamID,ParameterType]],ReturnType,BodyTree)),
464		z3_type_to_b_type(ReturnType,Type), % check if type matches
465		!,
466		( ParamID == Arg % special case if argument and parameter identical
467		-> translate_z3_expr(BodyTree,env(Env,AVL),Type,Res)
468		; z3_type_to_b_type(ParameterType,PType), % TO DO: couple-> ground type; PType could be not ground !
469		translate_z3_expr(CstFunc,env(Env,AVL),set(couple(PType,Type)),TFun),
470		translate_z3_expr(Arg,env(Env,AVL),PType,TArg),
471		create_texpr(function(TFun,TArg),Type,[contains_wd_condition],Res)
472		).
473		translate_z3_expr([let,[[Id,Val]],Function],Env,Type,Res) :- !,
474		z3_replace_let_id_by_value(Id,Val,Function,NewFunction),
475	?	translate_z3_expr(NewFunction,Env,Type,Res).
476		translate_z3_expr([let,[[Id,Val]|T],Function],Env,Type,Res) :-
477		T \== [],
478		z3_replace_let_id_by_value(Id,Val,Function,NewFunction),
479		translate_z3_expr([let,T,NewFunction],Env,Type,Res).
480		translate_z3_expr([ZOP, Left], Env, Type,Res) :-
481		z3_unary_expr_to_b(ZOP, BOP, Type),!,
482		translate_z3_expr(Left, Env, Type, TL),
483		Expr =.. [BOP,TL],
484		safe_create_texpr(Expr, Type, Res).
485		translate_z3_expr([ZOP|Args], Env, Type, Res) :-
486		% operators such as multiplication can have an arbitrary arity like [*,x,x,x]
487	?	z3_binary_expr_to_b(ZOP, BOP, TA, TB, Type), !,
488	?	create_nested_binary_expr(BOP, Env, Type, TA, TB, Args, Res).
489		translate_z3_expr([ite, Test, Left, Right], Env, Type, Res) :- !,
490		translate_z3_predicate(Test,Env, BTest),
491	?	translate_z3_expr(Left, Env, Type, BThen),
492	?	translate_z3_expr(Right,Env, Type, BElse), get_texpr_type(BThen,Type),
493		safe_create_texpr(if_then_else(BTest,BThen,BElse),Type,Res).
494		translate_z3_expr(String,_,string,Res) :-
495		atom(String),
496		!,
497		Res = b(string(String),string,[]).
498		translate_z3_expr(['_','as-array',AuxFunName],_,set(X),Res) :- !,
499		% set is represented by aux function
500		translate_z3_expr_using_full_model(AuxFunName,set(couple(X,boolean)),ChFunSet),
501		% we computed the characteristic function of the set; now convert it to a set
502		% Now we need to compute dom(ChFunSet |> {TRUE}) = ChFunSet~[{TRUE}] = {x|ChFunSet(x)=TRUE}
503		unique_typed_id("el!",X,Element),
504		create_texpr(function(ChFunSet,Element),boolean,[contains_wd_condition],FCall),
505		create_equality(b(boolean_true,boolean,[]),FCall,NewNewPred),
506		safe_create_texpr(comprehension_set([Element],NewNewPred),set(X),CompSet),
507		% translate:print_bexpr(CompSet),nl,
508		compute_bcomp_set(CompSet,Set),
509		Res = b(value(Set),set(X),[]).
510		translate_z3_expr([store,Sub,Entry,TStoreRes],Env,set(Type),Res) :-
511		% TStoreRes can be true, false or a predicate which needs to be evaluated first
512		translate_z3_expr(Sub,Env,set(Type),S1),
513	?	translate_z3_expr(Entry,Env,Type,El2),
514		S2 = b(set_extension([El2]),set(Type),[]),
515		( (TStoreRes = true; TStoreRes = false)
516		-> StoreRes = TStoreRes
517		; translate_z3_predicate(TStoreRes, Env, BStoreRes),
518		( b_test_boolean_expression_cs(BStoreRes, [], [],'translating Z3 value',0)
519		-> StoreRes = true
520		; StoreRes = false
521		)
522		),
523		( StoreRes = true
524		-> Expr = union(S1,S2)
525		; StoreRes = false,
526		Expr = set_subtraction(S1,S2)
527		),
528		!,
529		b_compute_expression_nowf(b(Expr,set(Type),[]), [], [], List,'translating Z3 value',0),
530		Res = b(value(List),set(Type),[]).
531		translate_z3_expr([[as,const,['Array',Z3Type,'Bool']],false],_,Type,b(value([]),Type,[])) :-
532		( (Type = set(BType), z3_type_to_b_type(Z3Type,BType))
533		-> true
534		; add_error(translate_z3_expr,'Unexpected type in Z3 model: ',types(Z3Type,Type))
535		),
536		!.
537		translate_z3_expr([[as,const,['Array',Z3Type,'Bool']],true],_,Type,b(value(Res),Type,[])) :-
538		( (Type = set(BType), z3_type_to_b_type(Z3Type,BType))
539		-> b_type2_set(BType,Res),
540		!
541		; add_error(translate_z3_expr,'Unexpected type in Z3 model: ',types(Z3Type,Type)),
542		fail
543		).
544		translate_z3_expr(['record'|Z3Fields],Env,record(Fields),b(rec(FieldsOut),record(Fields),[])) :-
545		maplist(translate_z3_record(Env),Fields,Z3Fields,FieldsOut).
546		translate_z3_expr([iteration,Rel,Int],Env,set(CoupleType),Res) :-
547		translate_z3_expr(Rel,Env,set(CoupleType),TRel),
548		translate_z3_expr(Int,Env,integer,BInt),
549		Iteration = b(iteration(TRel,BInt),set(CoupleType),[]),
550		( BInt = b(integer(_),_,_)
551		-> compute_bcomp_set(Iteration,Set),
552		Res = b(value(Set),set(CoupleType),[])
553		; Res = Iteration
554		).
555		% Some special cases to improve lambda translations
556		translate_z3_expr([lambda,[[ClosureVar,ClosureVarType]],Body],Env,SetType,Res) :-
557		( ClosureVar = refl_closure_g_u_var
558		-> Functor = reflexive_closure
559		; ClosureVar = closure_g_u_var,
560		Functor = closure
561		),
562		!,
563		z3_type_to_b_type(ClosureVarType,BType),
564		TClosureVar = b(identifier(ClosureVar),BType,[]),
565		% compute closure with ProB if Z3 does not unfold lambda,
566		% the translated model itself (lambda(exists(...))) is too complex so we catch translated closures here
567		Env = env(Ids,B),
568		translate_z3_predicate(Body, env([TClosureVar|Ids],B), TBody),
569		TBody = b(exists(_,ExistsBody),pred,_),
570		conjunction_to_list(ExistsBody, ExistsBodyConj),
571		member(b(exists(_,ExistsBody2),pred,_), ExistsBodyConj),
572		conjunction_to_list(ExistsBody2, ExistsBodyConj2),
573		member(b(equal(b(identifier(_),SetType,_),b(iteration(TRel,_),SetType,_)),pred,[]), ExistsBodyConj2),
574		!,
575		BNode =.. [Functor,TRel],
576		TRes = b(BNode,SetType,[]),
577		clean_up(TRes, [], Res).
578		translate_z3_expr([lambda,Args,Body],env(Ids,_),set(BType),Res) :-
579		% see for instance ':z3-double-check f = %x.(x : INTEGER|x * x * x) & f(f(x)) = y & y = 512'
580		Args = [[ID,Z3Type]],
581		z3_type_to_b_type(Z3Type,BType),
582		TID = b(identifier(ID),BType,[]),
583		Body = [exists|_],
584		translate_z3_predicate(Body,env([TID|Ids],empty),TBody),
585		TBody = b(exists([LambdaID],ExistsBody),pred,_),
586		conjunction_to_list(ExistsBody, ExistsList),
587		select(ExistsBody, ExistsList, RestExistsList),
588		ExistsBody = b(equal(CoupleCst,ExistCouple),pred,_),
589		CoupleCst = b(identifier('_couple_cst'),couple(_,_),_),
590		conjunct_predicates(RestExistsList, RestExistsBody),
591		!,
592		ExistCouple = b(couple(_,ExistsExpr),_,_),
593		safe_create_texpr(lambda([LambdaID],RestExistsBody,ExistsExpr), set(BType), BLambda),
594		clean_up(BLambda, [], CompSet),
595		compute_bcomp_set(CompSet,Set),
596		Res = b(value(Set),set(BType),[]).
597		translate_z3_expr([lambda,Args,Body],env(Ids,B),set(BType),Res) :-
598		Args = [[ID,Z3Type]], % TO DO: more than one argument?
599		z3_type_to_b_type(Z3Type,BType),
600		!,
601		TID = b(identifier(ID),BType,[]),
602	?	translate_z3_predicate(Body,env([TID|Ids],B),TBody),
603		safe_create_texpr(comprehension_set([TID],TBody),set(BType),CompSet),
604		%print('lambda: '),translate:print_bexpr(CompSet),nl, print(CompSet),nl,
605		compute_bcomp_set(CompSet,Set),
606		Res = b(value(Set),set(BType),[]).
607		%
608		translate_z3_expr([['_',map,AndOrTerm]|T], Env, _, Res) :-
609		( AndOrTerm = [AndOr,['Bool','Bool'],'Bool'] % prior version 4.12.2
610		; AndOrTerm = AndOr % since version 4.12.2
611		),
612		( AndOr == and
613		; AndOr == or
614		),
615		!,
616	?	map_translate_z3_expr(T, Env, [], TT),
617		TT = [b(_,SetType,_)|_],
618		( AndOr == and
619		-> unfold_general_intersection(TT, SetType, Res)
620		; unfold_general_union(TT, SetType, Res)
621		).
622		translate_z3_expr([mod,A,B], Env, integer, Res) :-
623		!,
624		translate_z3_expr(A, Env, integer, BA),
625		translate_z3_expr(B, Env, integer, BB),
626		BIsZero = b(equal(BB,b(integer(0),integer,[])),pred,[]),
627		% return 0 if B is zero, otherwise (= (mod x y) (- x (* y (div x y)))) holds
628		ModEq = b(minus(BA,b(multiplication(BB,
629		b(floored_div(BA,BB),integer,[contains_wd_condition])),integer,[contains_wd_condition])),
630		integer,[contains_wd_condition]),
631		safe_create_texpr(if_then_else(BIsZero,b(integer(0),integer,[]),ModEq),integer,TRes),
632		clean_up(TRes, [], Res).
633		translate_z3_expr([rem,A,B], Env, integer, Res) :-
634		!,
635		translate_z3_expr(A, Env, integer, BA),
636		translate_z3_expr(B, Env, integer, BB),
637		BIsZero = b(equal(BB,b(integer(0),integer,[])),pred,[]),
638		BLowerZero = b(less(BB,b(integer(0),integer,[])),pred,[]),
639		% return 0 if B is zero, otherwise (= (rem x y) (ite (< y 0) (* (- x (* y (div x y))) -1) (- x (* y (div x y))))) holds
640		ModEq = b(minus(BA,b(multiplication(BB,
641		b(floored_div(BA,BB),integer,[contains_wd_condition])),integer,[contains_wd_condition])),
642		integer,[contains_wd_condition]),
643		safe_create_texpr(if_then_else(BLowerZero,b(unary_minus(ModEq),integer,[]),ModEq),integer,IfExpr),
644		safe_create_texpr(if_then_else(BIsZero,b(integer(0),integer,[]),IfExpr),integer,TRes),
645		clean_up(TRes, [], Res).
646		translate_z3_expr(Expr,_,Type,_) :-
647		\+ check_error_occured(translate_z3_expr_globalsets_fdrange, _),
648		add_error_fail(translate_z3_expr, 'Missing translation for Z3 expression:', Expr:Type).
649
650		translate_z3_connective(BOP, T, Env, PredRes) :-
651	?	map_translate_z3_predicate(T, Env, [], NT),
652		( BOP == conjunct
653		-> conjunct_predicates(NT, PredRes)
654		; BOP == disjunct
655		-> disjunct_predicates(NT, PredRes)
656		; Pred =.. [BOP|NT],
657		safe_create_texpr(Pred, pred, PredRes)
658		).
659
660		unfold_general_intersection([A], _, A).
661		unfold_general_intersection([A,B|T], SetType, Res) :-
662		!,
663		Acc = b(intersection(A,B),SetType,[]),
664		unfold_general_intersection_acc(T, SetType, Acc, Res).
665
666		unfold_general_intersection_acc([], _, Acc, Acc).
667		unfold_general_intersection_acc([A,B|T], SetType, Acc, Res) :-
668		NewAcc = b(intersection(Acc,b(intersection(A,B),SetType,[])),SetType,[]),
669		unfold_general_intersection_acc(T, SetType, NewAcc, Res).
670
671		unfold_general_union([A], _, A).
672		unfold_general_union([A,B|T], SetType, Res) :-
673		!,
674		Acc = b(union(A,B),SetType,[]),
675		unfold_general_union_acc(T, SetType, Acc, Res).
676
677		unfold_general_union_acc([], _, Acc, Acc).
678		unfold_general_union_acc([A,B|T], SetType, Acc, Res) :-
679		NewAcc = b(union(Acc,b(union(A,B),SetType,[])),SetType,[]),
680		unfold_general_union_acc(T, SetType, NewAcc, Res).
681
682		z3_unary_expr_to_b('-',unary_minus ,integer).
683
684
685		% z3_binary_expr_to_b(Z3Op,BOp,TypeLeftArg,TypeRightArg,TypeOfExpr)
686		z3_binary_expr_to_b('*', multiplication, integer, integer, integer).
687		z3_binary_expr_to_b('+', add, integer, integer, integer).
688		z3_binary_expr_to_b('-', minus, integer, integer, integer).
689		z3_binary_expr_to_b('/', floored_div, integer, integer, integer).
690		z3_binary_expr_to_b('div', floored_div, integer, integer, integer).
691		z3_binary_expr_to_b(Z3Couple, couple, TA, TB, couple(TA,TB)) :-
692		atom(Z3Couple),
693		atom_prefix('couple', Z3Couple).
694
695		% --------------------
696
697		z3_ground_result(real,real(0.0)).
698		z3_ground_result(integer,int(0)).
699		z3_ground_result(boolean,pred_true).
700		z3_ground_result(couple(X,Y),(XG,YG)) :-
701		z3_ground_result(X,XG), z3_ground_result(Y,YG).
702		z3_ground_result(set(_),[]).
703		z3_ground_result(record(Fields),rec(FieldsOut)) :-
704		maplist(z3_ground_record_fields,Fields,FieldsOut).
705
706		z3_ground_record_fields(field(Name,BType),field(Name,BVal)) :-
707		z3_ground_result(BType,BVal).
708
709		% --------------------
710
711		compute_bcomp_set(CompSet,ResultOut) :-
712		% translate:set_unicode_mode,translate:print_bexpr(CompSet),
713		b_compute_expression_nowf(CompSet,[],[],Res,'translating Z3 value',0),
714		(try_expand_custom_set_to_list(Res,ResultOut,true,z3_set_to_b_set)
715		-> true
716		; ResultOut = Res).
717
718		atom_to_term(Atom, Term) :-
719		atom_concat(Atom, '.', AtomWithStop),
720		atom_codes(AtomWithStop, AtomWithStopC),
721		read_from_codes(AtomWithStopC, Term).
722
723		z3_type_to_b_type(record, Type) :- !, Type =.. [record|_]. % record type in SMT-LIB is just 'record'
724		z3_type_to_b_type('String', Type) :- !, Type = string.
725		z3_type_to_b_type('Int', Type) :- !, Type = integer.
726		z3_type_to_b_type('Bool', Type) :- !, Type = boolean.
727		z3_type_to_b_type('Real', Type) :- !, Type = real.
728		z3_type_to_b_type(Z3Couple, BType) :-
729		atom(Z3Couple),
730	?	get_couple_type_from_atom(Z3Couple, CoupleType1, CoupleType2),
731		!,
732		BType = couple(CoupleType1,CoupleType2).
733		z3_type_to_b_type(GlobalSet, BType) :-
734	?	b_global_set(GlobalSet),
735		!,
736		BType = global(GlobalSet).
737		z3_type_to_b_type(['Array',SetType,'Bool'], BType) :-
738		!,
739		z3_type_to_b_type(SetType, BSetType),
740		BType = set(BSetType).
741		z3_type_to_b_type(A, _) :-
742		add_error_fail(z3_type_to_b_type, "Missing translation for Z3 type in model translation.", [A]).
743
744		get_couple_type_from_atom(CoupleAtom, CoupleType1, CoupleType2) :-
745		atom(CoupleAtom),
746		atom_codes(CoupleAtom, Codes),
747	?	get_couple_type_from_codes([TT1,TT2], Codes, []),
748		atom_codes(T1Atom, TT1),
749		atom_to_term(T1Atom, CoupleType1),
750		atom_codes(T2Atom, TT2),
751		atom_to_term(T2Atom, CoupleType2).
752
753		get_couple_type_from_codes([T1,T2]) -->
754		"couple(",
755	?	type_symbol(T1),
756		",",
757	?	type_symbol(T2),
758		")".
759
760		z3_replace_let_id_by_value_maplist([], _, _, Res) :- !, Res=[].
761		z3_replace_let_id_by_value_maplist([let,LetVals|T], Id, _, Out) :-
762		% prevent that the let ids of a nested let expression are mistakenly replaced
763		% I.e., Id is now being overwritten by another let;
764		% TODO: but what if Id is used in RHS of some LetVals? Can that be?
765		member([Id,_], LetVals),
766		!,
767		Out = [let,LetVals|T].
768		z3_replace_let_id_by_value_maplist([H|T], Id, Val, [NH|NT]) :-
769		z3_replace_let_id_by_value(Id, Val, H, NH),
770		z3_replace_let_id_by_value_maplist(T, Id, Val, NT).
771
772
773		z3_replace_let_id_by_value(Id,Val,Function,NewFunction) :-
774		Function = [_|_], % is_list(Function), is_list also does a cyclic check
775		!,
776		z3_replace_let_id_by_value_maplist(Function,Id,Val,NewFunction).
777		z3_replace_let_id_by_value(Id,Val,Function,NewFunction) :-
778		( Id = Function
779		-> NewFunction = Val
780		; %atomic(Function), % do we need this test?
781		NewFunction = Function
782		).
783
784		z3_model_to_avl(FullModel,AVL) :-
785		atom_codes(FullModel,Codes),
786		%format('Full model:~n~s~n',[Codes]),nl,
787		parse_lisp_style_expressions(E,Codes,[]),!,
788	?	z3_lisp_to_avl(E,AVL).
789
790		z3_lisp_to_avl(E,AVL) :-
791		empty_avl(In),
792	?	z3_lisp_to_avl(E,In,AVL).
793
794		z3_lisp_to_avl([],A,A).
795		z3_lisp_to_avl([['define-fun',Name,Param,Return,Tree]|T],AIn,AOut) :-
796		avl_store(Name,AIn,'z3-define-fun'(Param,Return,Tree),ATemp),
797	?	z3_lisp_to_avl(T,ATemp,AOut).
798		% currently I think I do not need these facts...
799		% as far as I understand they represent enumerated set Elements
800		z3_lisp_to_avl([['declare-fun',_Name,_Params,_Type0]|T],AIn,AOut) :-
801	?	z3_lisp_to_avl(T,AIn,AOut).
802		% these occur for cardinality constraints
803		z3_lisp_to_avl([['forall',_Vars,_Pred]|T],AIn,AOut) :-
804	?	z3_lisp_to_avl(T,AIn,AOut).
805
806
807		% -----------------------------
808
809		translate_cvc4_tree(['CONST_RATIONAL',Arg],integer,int(Val)) :-
810		arg_is_number(Arg,Val).
811		translate_cvc4_tree(['CONST_BOOLEAN',1],boolean,pred_true).
812		translate_cvc4_tree(['CONST_BOOLEAN',0],boolean,pred_false).
813		translate_cvc4_tree(['CONST_STRING',Content],string,string(Content)).
814		translate_cvc4_tree(['SINGLETON',ValIn],set(X),[ValOut]) :-
815		translate_cvc4_tree(ValIn,X,ValOut).
816		translate_cvc4_tree(['EMPTYSET',emptyset,_Type],set(_),[]).
817		translate_cvc4_tree(['TUPLE',V1,V2],couple(Type1,Type2),(TV1,TV2)) :-
818		translate_cvc4_tree(V1,Type1,TV1),
819		translate_cvc4_tree(V2,Type2,TV2).
820		translate_cvc4_tree(['APPLY_CONSTRUCTOR','__cvc4_tuple_ctor',V1,V2],couple(Type1,Type2),(TV1,TV2)) :-
821		translate_cvc4_tree(V1,Type1,TV1),
822		translate_cvc4_tree(V2,Type2,TV2).
823		translate_cvc4_tree(['UNION',V1,V2],set(X),Val) :-
824		translate_cvc4_tree(V1,set(X),TV1),
825		translate_cvc4_tree(V2,set(X),TV2),
826		append(TV1,TV2,Val).
827		translate_cvc4_tree(['UNINTERPRETED_CONSTANT',C],global(SId),fd(PBCId,SId)) :-
828		atom_codes(C,CCodes),
829		parse_uc(CId,CCodes,[]),
830		PBCId is CId + 1.
831		translate_cvc4_tree(['RECORD',_CVCRecordType|Fields],record(RFields),rec(FieldsOut)) :-
832		maplist(translate_cvc4_record,RFields,Fields,FieldsOut).
833
834		translate_cvc4_record(field(Name,BType),CVCVal,field(Name,BVal)) :-
835		translate_cvc4_tree(CVCVal,BType,BVal).
836
837		parse_uc(Id) -->
838		"uc__SORT_TYPE_var_", number(_),
839		"__", number(N), {number_codes(Id,N)}.
840
841		parse_lisp_style_expressions(L) -->
842		{reset_line_count},
843		lisp_style_expressions(L),!.
844
845		lisp_style_expressions(Res) --> real_ws,!,
846		lisp_style_expressions(Res).
847		lisp_style_expressions([E|Es]) -->
848		lisp_style_expression(E), !,
849		lisp_style_expressions(Es).
850		lisp_style_expressions([]) --> [].
851		%lisp_style_expressions(_,In,_) :- linecount(Line),
852		% format("lisp-style parser failed on line ~w on: ~s~n",[Line,In]),fail.
853
854
855		closed_lisp_style_expressions(Res) --> real_ws,!,
856		closed_lisp_style_expressions(Res).
857		closed_lisp_style_expressions([]) --> ")",!.
858		closed_lisp_style_expressions([E|Es]) -->
859		lisp_style_expression(E), !,
860		closed_lisp_style_expressions(Es).
861
862		linecount(1).
863		reset_line_count :- retractall(linecount(_)), assertz(linecount(1)).
864		inc_linecount :- retract(linecount(Nr)), N1 is Nr+1, assertz(linecount(N1)).
865
866		% real whitespace
867		real_ws --> "\n", {inc_linecount},!, ws.
868		real_ws --> [W], {W = 32 ; W = 10 ; W = 13}, !, ws.
869		real_ws --> ";;", !, any_but_newline.
870
871		% optional whitespace
872		ws --> real_ws,!.
873		ws --> [].
874		any_but_newline --> [C], {C \= 10}, !, any_but_newline.
875		any_but_newline -->"\n", {inc_linecount},!, ws.
876
877		z3_op([42]) --> [42]. % *
878		z3_op([43]) --> [43]. % +
879		z3_op([45]) --> [45]. % -
880		z3_op([47]) --> [47]. % /
881		% TO DO: support all operators
882
883		lisp_style_expression(Iteration) --> "((_ |iteration_", rel_type_skip, "| 0)", ws,
884		closed_lisp_style_expressions([Arg1,Arg2]), ws, !, {Iteration = [iteration,Arg1,Arg2]}.
885	?	lisp_style_expression(A) --> real(Cs), !, {atom_codes(A, Cs)}.
886		lisp_style_expression(L) --> "!", !, ws, lisp_style_expression(L), ws, ":weight", ws, number(_). % optional term parameter
887		lisp_style_expression(A) --> "/0", !, {A = '/0'}. % weird special case when using reals, e.g., for ':z3 a:REAL & b/=0.0 & a=1.2/b' a function called '/0' is defined
888	?	lisp_style_expression(A) --> z3_op(Cs), !, {atom_codes(A, Cs)}.
889	?	lisp_style_expression(A) --> typed_couple_top_level(Cs), !, {atom_codes(A, Cs)}.
890		lisp_style_expression(A) --> non_empty_symbol(Cs), !, {atom_codes(A, Cs)}.
891	?	lisp_style_expression(N) --> number(Cs), !, {number_codes(N, Cs)}.
892		lisp_style_expression(N) --> "-", number(Cs), !, {number_codes(N2,Cs), N is -N2}.
893	?	lisp_style_expression(A) --> string(Codes), !, {atom_codes(A,Codes)}.
894		lisp_style_expression(List) --> "(", !, closed_lisp_style_expressions(List).
895		lisp_style_expression(record_type(Fields)) -->
896		"[#", !, ws, record_type_fields(Fields),!,
897		ws, expect("#]",record_type).
898		lisp_style_expression(_,In,_) :- In \= [], % not at end of string
899		linecount(Line),
900		format("lisp-style parser failed on line ~w on: ~s~n",[Line,In]),fail.
901
902		expect(L,_) --> L,!.
903		expect(L,Ctxt,In,_) :- linecount(Line),
904		format("lisp-style parser failed on line ~w expecting ~s for ~w on: ~s~n",[Line,L,Ctxt, In]),fail.
905
906		record_type_fields([F|Fields]) -->
907		record_type_field(F), ws, expect(",",record_type_field), !,
908		ws, record_type_fields(Fields).
909		record_type_fields([F]) --> record_type_field(F).
910
911		record_type_field(field(NameA,TypeA)) -->
912		non_empty_symbol(Name), ":(TYPE_CONSTANT ", non_empty_symbol(Type), " type)",
913		{atom_codes(NameA,Name),atom_codes(TypeA,Type)}.
914
915		real(R) -->
916	?	number(I),
917		".",
918	?	number(D),
919		( "?",
920		!
921		; ""
922		),
923		{append([I,[46],D],R)}.
924
925	?	number([D|Ds]) --> digit(D), number(Ds).
926		number([D]) --> digit(D).
927
928		rel_type_skip -->
929		"set(couple(", type_symbol(_), ",", type_symbol(_), "))".
930
931		% top-level couple types are escaped with | in an SMT-Lib model
932		typed_couple_top_level(Cs) -->
933		"|couple(",
934	?	in_couple(Cs1,Cs2),
935		expect(")|", typed_couple_top_level),
936		{append(["couple(",Cs1,",",Cs2,")"], Cs)}.
937
938		typed_couple_inner(Cs) -->
939		"couple(",
940		in_couple(Cs1,Cs2),
941		expect(")", typed_couple_inner),
942		{append(["couple(",Cs1,",",Cs2,")"], Cs)}.
943
944		in_couple(Cs1, Cs2) -->
945	?	type_symbol(Cs1), !,
946		expect(",", in_couple),
947	?	type_symbol(Cs2).
948
949		digit(D) --> [D], {48 =< D, D =< 57}.
950
951	?	string(Codes) --> "\"", string_symbol(Codes), "\"".
952
953		% already escaped
954		type_symbol(Cs) --> typed_couple_inner(Cs).
955		type_symbol(A) --> non_empty_symbol(Global), {Global == "global"}, "('", !,
956		non_empty_symbol(GlobalType), ")", {append([Global,[40,39],GlobalType,[41]], A)}.
957		% the global type has to be escaped for global(_) since it can be capitalised which results in a variable in Prolog
958		type_symbol(A) --> non_empty_symbol(Global), {Global == "global"}, !,
959		"(", non_empty_symbol(GlobalType), ")", {append([Global,[40,39],GlobalType,[39,41]], A)}.
960	?	type_symbol(A) --> non_empty_symbol(A1), type_symbol_term(A2,0), !, {append(A1, A2, A)}.
961		type_symbol(_,In,_) :- linecount(Line),
962		format("lisp-style parser failed on line ~w expecting type_symbol on: ~s~n",[Line, In]),fail.
963
964	?	type_symbol_term([40|A],Lvl) --> "(", {L1 is Lvl+1}, type_symbol_term(A,L1).
965	?	type_symbol_term([41|A],Lvl) --> ")", {Lvl>0, L1 is Lvl-1}, type_symbol_term(A,L1).
966	?	type_symbol_term(A,Lvl) --> non_empty_symbol(A1), type_symbol_term(A2,Lvl), {append(A1, A2, A)}.
967	?	type_symbol_term(A,Lvl) --> typed_couple_inner(A1), !, type_symbol_term(A2,Lvl), {append(A1, A2, A)}.
968		type_symbol_term(A,0) --> non_empty_symbol(A).
969		type_symbol_term([],0) --> "".
970
971		non_empty_symbol([A|As]) -->
972		[A],
973		{ 65 =< A, A =< 90
974		; 97 =< A, A =< 122
975		% ; 48 =< A, A =< 57
976		; 913 =< A, A =< 937 % upper-case greek letters
977		; 945 =< A, A =< 969 % lower-case greek letters
978		; A = 124 % "|"
979		; A = 95 % "_",
980		; A = 45 % "-"
981		; A = 39 % "'"
982		; A = 33 % "!"
983		; 60 =< A, A =< 62 % "<", "=", ">"
984		},!,
985		symbol(As).
986
987		symbol([A|As]) -->
988		[A],
989		{ 65 =< A, A =< 90
990		; 97 =< A, A =< 122
991		; 48 =< A, A =< 57
992		; 913 =< A, A =< 937 % upper-case greek letters
993		; 945 =< A, A =< 969 % lower-case greek letters
994		; A = 124 % "|"
995		; A = 95 % "_",
996		; A = 45 % "-"
997		; A = 39 % "'"
998		; A = 33 % "!"
999		; 60 =< A, A =< 62 % "<", "=", ">"
1000		; A = 8242 % Unicode Prime, should we also allow this as first symbol?
1001		},!,
1002		symbol(As).
1003		symbol([]) --> "".
1004
1005		string_symbol([34|As]) -->
1006		% Z3 escapes double quotes with double quotes while ProB uses \"
1007		[34,34],
1008	?	string_symbol(As).
1009		string_symbol([A|As]) -->
1010		[A],
1011		{ 35 =< A, A =< 126
1012		; A = 33 % "!"
1013		},
1014	?	string_symbol(As).
1015		string_symbol([]) --> "".