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