1		% (c) 2009-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
6		:- module(b_compiler,[b_compile/6, b_optimize/6, b_optimize_closure/3]).
7
8		:- use_module(library(lists)).
9
10		:- use_module(self_check).
11		:- use_module(bsyntaxtree).
12		:- use_module(error_manager).
13		:- use_module(debug,[debug_format/3]).
14		:- use_module(btypechecker,[fasttype/2]).
15		:- use_module(bmachine,[b_get_machine_operation_for_animation/6]).
16		:- use_module(b_interpreter).
17		:- use_module(custom_explicit_sets).
18		:- use_module(kernel_waitflags,[add_error_wf/5, add_internal_error_wf/5]).
19		%:- use_module(bmachine,[b_operation_reads_output_variables/3]).
20		:- use_module(probsrc(performance_messages),[performance_monitoring_on/0,perfmessage/3]).
21
22		:- use_module(module_information,[module_info/2]).
23		:- module_info(group,interpreter).
24		:- module_info(description,'This module compiles set comprehensions into closures; making them independent of the state of the B machine.').
25
26		/* compile boolean expression into a closure where the local state and the global
27		state has been incorporated, but any parameter is left in the closure */
28
29		:- public test_bexpr/3, test_bexpr2/3.
30		test_bexpr(Expr,[bind(cc,int(1)),bind(nn,int(2))], [bind(db,[(int(1),int(2))])]) :-
31		fasttype( +conjunct( +conjunct( +member( global('Name')<<identifier(nn), +identifier('Name')),
32		+member( global('Code')<<identifier(cc), +identifier('Code'))),
33		+not_member( global('Name')<<identifier(nn),
34		+domain(set(couple(global('Name'),global('Code')))<<identifier(db)))), Expr).
35
36		test_bexpr2(Expr,[],[]) :-
37		fasttype( +implication( +equal( seq(any)<<identifier(ss), +empty_sequence),
38		+equal( set(any)<<identifier(res), +empty_set)), Expr).
39
40
41
42		b_optimize_closure(closure(P,T,Body),Res,WF) :-
43		b_optimize(Body,P,[],[],CBody,WF),!,
44		Res=closure(P,T,CBody).
45		b_optimize_closure(C,C,_WF).
46
47
48		% difference with b_compile: the states LS, S will not be thrown away by the interpreter
49		% thus: we do not have to compile all accesses, in particular lazy lookups !
50		%b_optimize(TExpr,Parameters,_LS,_S,NTExpr,_WF) :- TExpr=b(_,_,Infos), member(already_optimized,Infos),
51		% !, NTExpr=TExpr.
52		b_optimize(TExpr,Parameters,LS,S,NTExpr,WF) :- %print('OPTIMIZE: '),translate:print_bexpr(TExpr),nl, trace,
53		append(LS,[bind('$optimize_do_not_force_lazy_lookups',pred_true)],NewLS),
54		b_compile(TExpr,Parameters,NewLS,S,NTExpr,WF).
55		%bsyntaxtree:add_texpr_info_if_new(NTExpr,already_optimized,ResTExpr).
56
57		b_compile(TExpr,Parameters,NewLS,S,NTExpr) :-
58	?	b_compile(TExpr,Parameters,NewLS,S,NTExpr,no_wf_available). % for unit tests
59
60		:- assert_must_succeed(( b_compiler:test_bexpr(E,L,S),
61		b_compiler:b_compile(E,[nn],L,S,_R) )).
62		:- assert_must_succeed(( b_compiler:test_bexpr2(E,L,S),
63		b_compiler:b_compile(E,[ss,res],L,S,_R) )).
64		:- assert_must_succeed(( b_compiler:b_compile(b(greater(b(value(int(2)),integer,[]),
65		b(value(int(1)),integer,[])),pred,[]),[],[],[],Res),
66		check_eq(Res,b(truth,pred,_)) )).
67		:- assert_must_succeed(( b_compiler:b_compile(b(greater(b(value(int(2)),integer,[]),
68		b(value(int(3)),integer,[])),pred,[]),[],[],[],Res),
69		check_eq(Res,b(falsity,pred,_)) )).
70		:- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]),
71		b(value(int(_)),integer,[])),pred,[]),
72		b_compiler:b_compile(E,[],[],[],Res),
73		check_eq(Res,E) )).
74		:- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]),
75		b(value(_),integer,[])),pred,[]),
76		b_compiler:b_compile(E,[],[],[],Res),
77		check_eq(Res,E) )).
78		:- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]),
79		b(identifier(x),integer,[])),pred,[]),
80		b_compiler:b_compile(E,[],[bind(x,int(1))],[],Res),
81		check_eq(Res,b(truth,pred,_)) )).
82		:- assert_must_succeed(( E = b(greater(b(value(int(2)),integer,[]),
83		b(identifier(x),integer,[])),pred,[]),
84		b_compiler:b_compile(E,[],[bind(x,int(3))],[],Res),
85		check_eq(Res,b(falsity,pred,_)) )).
86
87		%:- assert_pre(b_compiler:b_compile_boolean_expression(E,Parameters,LS,S,_),
88		% (type_check(E,boolean_expression),type_check(Parameters,list(variable_id)),
89		% type_check(LS,store),type_check(S,store))).
90		%:- assert_post(b_compiler:b_compile_boolean_expression(_,_,_,_,E), type_check(E,boolean_expression)).
91
92		/* probably not worthwhile:
93		b_compile(TExpr,Parameters,LS,S,NTExpr) :- get_texpr_info(TExpr,Info),
94		(memberchk(compiled(Parameters),Info) -> NTExpr = TExpr ,print(already_compiled(Parameters)),nl, translate:print_bexpr(TExpr),nl
95		; b_compile0(TExpr,Parameters,LS,S,b(E,T,I)), translate:print(compiling(Parameters)),nl, translate:print_bexpr(TExpr),nl,
96		NTExpr = b(E,T,[compiled(Parameters)|I])).
97		*/
98		:- use_module(closures,[get_recursive_identifier_of_closure_body/2]).
99		b_compile(TExpr,Parameters,LS,S,NTExpr,WF) :-
100		check_is_id_list(Parameters,Parameters0),
101		(get_recursive_identifier_of_closure_body(TExpr,TRID),
102		def_get_texpr_id(TRID,RID), nonmember(bind(RID,_),LS)
103		-> Parameters1=[RID|Parameters0] % add recursive ID virtually to parameters to avoid error messages
104		; Parameters1=Parameters0),
105		% print('compile : '),translate:print_bexpr(TExpr),nl, statistics(runtime,[Start,_]),%%
106		sort(Parameters1,Parameters2),
107	?	if(b_compile1(TExpr,Parameters2,LS,S,NTExpr0,eval,FullyKnown,WF),
108		(FullyKnown=true
109		-> copy_pos_infos(TExpr,NTExpr0,NTExpr)
110		% ensure position info is not deleted if full expression compiled away, see PROB-412 (test 1677)
111		; NTExpr=NTExpr0),
112		(add_internal_error_wf(b_compiler,'Compilation failed: ',TExpr,TExpr,WF),
113		%b_compile1(TExpr,Parameters1,LS,S,NTExpr0,eval,_FullyKnown,WF),
114		NTExpr = TExpr)
115		).
116		%, bsyntaxtree:check_ast(NTExpr).
117		%, check_infos(TExpr,NTExpr).
118		%, print('compiled: '), translate:print_bexpr(NTExpr), print(' '),statistics(runtime,[Stop,_]), T is Stop-Start, print(T), print(' ms '),nl, bsyntaxtree:check_ast(NTExpr). % , print(NTExpr),nl. check_ast
119
120		/*
121		check_infos(Old,New) :- bsyntaxtree:get_texpr_info(Old,IO),
122		bsyntaxtree:get_texpr_info(New,IN),
123		member(X,IO), \+ member(X,IN),
124		bsyntaxtree:important_info(X),
125		print(check_infos(Old,New)),nl,
126		print('Not copied: '), print(X),fail.
127		check_infos(_,_). */
128
129		:- use_module(bsyntaxtree,[always_well_defined/1]).
130		:- use_module(translate,[translate_bexpression_with_limit/2]).
131		%:- use_module(hit_profiler,[add_profile_hit/1]).
132
133		% Eval=eval means the expression will be needed in a successful branch and we can pre-compute more aggressively
134		% Eval=false means the expression may not be needed (e.g., in a disjunction) and only perform efficient precomputations
135		b_compile1(TExpr,Parameters,LS,S,ResultTExpr,Eval,FullyKnown1,WF) :-
136		TExpr = b(Expr,Type,Infos),
137		NTExpr = b(NewUntypedExpr,Type,NewInfos),
138		%remove_bt(TExpr,Expr,NewUntypedExpr,NTExpr), % remove top-level Type Information
139		%hit_profiler:add_profile_hit(Expr),
140		%functor(Expr,E1,N1), %print(start_compile(E1/N1,Eval,FullyKnown1)),nl,
141	?	b_compile1_infos(Expr,Type,Infos,Parameters,LS,S,NewUntypedExpr,NewInfos,Eval,FullyKnown,WF),
142		%functor(NewUntypedExpr,E2,N2),
143		%format(' compiled ~w/~w -> ~w/~w : ',[E1,N1,E2,N2]),translate:print_bexpr_or_subst(NTExpr),nl,
144		%format(' fully=~w, eval=~w~n',[FullyKnown,Eval]),
145		(NTExpr = b(value(_),_,_)
146		-> FullyKnown1=FullyKnown, ResultTExpr=NTExpr
147		; FullyKnown=true, evaluate_this(Eval,NewUntypedExpr,Type,NewInfos)
148		-> % print('eval : '),translate:print_bexpr(NTExpr),nl, %
149		(nonvar(NewUntypedExpr),
150		% if( would be more prudent !?, also: we used to call b_compute_expression_nowf
151	?	b_interpreter:b_compute_expression(NTExpr,LS,S,ResultValue,WF)
152		-> %print(result(ResultValue)),nl,
153		%remove_bt(TExpr,Expr,value(ResultValue),ResultTExpr)
154		get_texpr_type(TExpr,TT),ResultTExpr = b(value(ResultValue),TT,[]),
155		FullyKnown1 = FullyKnown
156		%, print(compiled_value(ResultTExpr)),nl
157		; add_internal_error_wf(b_compiler,'Undefined value marked for evaluation:',NTExpr,Infos,WF),
158		%trace, b_interpreter:b_compute_expression(NTExpr,LS,S,ResultValue,WF),
159		ResultTExpr=NTExpr, FullyKnown1=false
160		)
161		; % ((FullyKnown=true, NTExpr\=b(value(_),_,_)) -> format('not eval: ~w (~w)~n',[NTExpr,Eval]) ; true),
162		ResultTExpr=NTExpr, FullyKnown1=false
163		).
164
165
166		:- use_module(library(ordsets),[ord_member/2, ord_union/3]).
167		:- use_module(bsyntaxtree,[create_exists_or_let_predicate/3]).
168		:- use_module(tools_lists,[delete_first/3]).
169		add_parameters(SortedIds,NewIds,NewSortedIds) :-
170		sort(NewIds,SNew),
171		ord_union(SortedIds,SNew,NewSortedIds).
172
173		b_compile1_infos(exists(ExistsPara,Pred),_,OldInfos,Parameters,LS,S,NExpr,NewInfos,Eval,FullyKnown,WF) :- !,
174		FullyKnown=false, % predicates never automatically evaluated in b_compile1
175		get_texpr_ids(ExistsPara,AtomicIds),
176		add_parameters(Parameters,AtomicIds,NParameters),
177	?	b_compile1(Pred,NParameters,LS,S,NPred,Eval,_FullyKnown1,WF),
178		(is_falsity(NPred) -> NExpr = falsity, NewInfos = OldInfos
179		; is_truth(NPred) -> NExpr = truth, NewInfos = OldInfos
180		%; Pred==NPred, write(unchanged(Parameters)),nl, member(used_ids(Old),OldInfos), print(used(Old)),nl,nl,fail
181		; create_exists_or_let_predicate(ExistsPara,NPred,b(NExpr,pred,NI)),
182		%print('COMPILED EXISTS: '), translate:print_bexpr(b(NExpr,pred,NI)),nl,
183		(delete_first(OldInfos,used_ids(_),I1),
184	?	member(used_ids(NewUsedIds),NI) -> NewInfos = [used_ids(NewUsedIds)|I1]
185		; %nl,print(missing_used_ids(OldInfos,NI)),nl, % can happen when we construt a let_predicate above
186		update_infos(NExpr,OldInfos,Parameters,NewInfos))
187		).
188		b_compile1_infos(identifier(Id),Type,OldInfos,Parameters,LS,S,NExpr,NewInfos,_Eval,FullyKnown,WF) :- !,
189		( ord_member(Id,Parameters) ->
190		NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos
191		; Id=op(_) ->
192		NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos
193		; b_interpreter:lookup_value_in_store_and_global_sets_wf(Id,Type,LS,S,Value,OldInfos,WF) ->
194		NExpr = value(Value), (known_value(Value) -> FullyKnown=true ; FullyKnown=false),
195		NewInfos = [was_identifier(Id)|OldInfos]
196		; add_internal_error_wf(b_compiler,'Compilation of identifier failed: ',Id,OldInfos,WF),
197		NExpr = identifier(Id), FullyKnown=false, NewInfos = OldInfos
198		).
199		b_compile1_infos(Expr,_,OldInfos,_Parameters,_LS,_S,NewUntypedExpr,NewInfos,_Eval,FullyKnown,_WF) :-
200	?	b_ast_cleanup:is_integer_set(Expr,_Set),!,
201		NewUntypedExpr=Expr, NewInfos=OldInfos,FullyKnown=true.
202		b_compile1_infos(operation_call_in_expr(Operation,OpCallParas),_Type,OldInfos,Parameters,LS,S,
203		Compiled,NewInfos,Eval,FullyKnown,WF) :- !,
204		def_get_texpr_id(Operation,op(OperationName)),
205		FullyKnown = false,
206		b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF),
207		(b_get_operation_normalized_read_write_info(OperationName,ReadVars,Modified) -> true
208		; member(reads(ReadVars),OldInfos), member(modifies(Modified),OldInfos)
209		-> add_message(b_compiler,'Unregistered operation in expression: ',OperationName)
210		% should not happen; but proceed with the locally stored reads/writes info
211		; add_error_wf(b_compiler,'Cannot obtain read/write info for operation:',OperationName,OldInfos,WF),
212		write(OldInfos),nl,nl,
213		ReadVars=[], Modified=[]
214		),
215		%exclude(operation_identifier,Read,ReadVars), % Read used to contain operations used via operation_call_in_expr; TO DO: check if this is ok in other places of source code of ProB; see test 1957
216		(Modified=[] -> true
217		; add_error_wf(b_compiler,'Calling operation that modifies state in expression:',OperationName,OldInfos,WF)),
218		% print(compile_call_op(OperationName,ReadVars,Modified,OpCallParaValues)),nl,
219		(ReadVars=[]
220		-> Compiled = operation_call_in_expr(Operation,OpCallParaValues),
221		NewInfos = OldInfos
222		; maplist(create_value_for_read_variable(LS,S,WF),ReadVars,TRead,TValues),
223		safe_create_texpr(let_expression_global(TRead,TValues,
224		b(operation_call_in_expr(Operation,OpCallParaValues),any,OldInfos)),any,[generated_by_b_compiler],New),
225		New = b(Compiled,_,NewInfos)
226		%NewInfos = [generated_by_b_compiler],
227		%Compiled = let_expression_global(TRead,TValues,
228		% b(operation_call_in_expr(Operation,OpCallParaValues),any,OldInfos))
229		).
230		b_compile1_infos(kodkod(Id,Identifiers),_,OldInfos,Parameters,LS,S,NExpr,NewInfos,_Eval,FullyKnown,WF) :- !,
231		FullyKnown=false, NewInfos=OldInfos,
232		exclude(is_parameter(Parameters),Identifiers,IdsToCompile),
233		(IdsToCompile=[]
234		-> NExpr = kodkod(Id,Identifiers)
235		; maplist(precompile_id(LS,S,WF),IdsToCompile,Values),
236		% as we cannot inspect kodkod problem: wrap it into a let with the values stored:
237		NExpr = let_predicate(IdsToCompile,Values,b(kodkod(Id,Identifiers),pred,OldInfos))
238		).
239		b_compile1_infos(Expr,_,OldInfos,Parameters,LS,S,NewUntypedExpr,NewInfos,Eval,FullyKnown,WF) :-
240	?	b_compile2(Expr,Parameters,LS,S,NewUntypedExpr,Eval,FullyKnown,WF),
241		update_infos(NewUntypedExpr,OldInfos,Parameters,NewInfos).
242
243
244		is_parameter(Parameters,b(identifier(Id),_,_)) :- ord_member(Id,Parameters).
245
246		precompile_id(LS,S,WF,b(identifier(Id),Type,Info),b(value(Value),Type,[])) :-
247		b_interpreter:lookup_value_in_store_and_global_sets_wf(Id,Type,LS,S,Value,Info,WF).
248		% was_identifier is aded in b_compile1_infos
249
250		:- use_module(bmachine,[b_get_operation_normalized_read_write_info/3]).
251
252		%operation_identifier(op(_)).
253		create_value_for_read_variable(LS,S,WF,Variable,TVariable,TValue) :-
254		b_interpreter:lookup_value_in_store_and_global_sets_wf(Variable,_Type,LS,S,Value,unknown,WF),!,
255		% TO DO: try and find type?
256		TVariable = b(identifier(Variable),any,[]),
257		TValue = b(value(Value),any,[]).
258		create_value_for_read_variable(_LS,_S,WF,Variable,TVariable,b(value(term(undefined)),any,[])) :-
259		TVariable = b(identifier(Variable),any,[]),
260		add_internal_error_wf(b_compiler,'Cannot find variable (read) while compiling operation:',Variable,unknown,WF),
261		fail.
262
263		:- use_module(library(ordsets)).
264		update_infos(forall(EParas,LHS,RHS),Infos,Parameters,NewInfos) :-
265		% forall also has used_ids field as it may call exists in negative context
266		conjunct_predicates([LHS,RHS],Cond),
267		update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos),!.
268		update_infos(exists(EParas,Cond),Infos,Parameters,NewInfos) :- % we create_exists_or_let_predicate above, but other transformations may generate an exists below:
269		update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos),!.
270		update_infos(BOP,Infos,_,NewInfos) :- bsyntaxtree:syntaxelement(BOP, [A,B],[], [], [], _),
271		wd_and_efficient(BOP), % should not generate WD errors itself
272	?	(select(contains_wd_condition,Infos,NewInfos) % there is a WD condition attached
273		-> fast_check_wd(A),
274		fast_check_wd(B)
275		),
276		%print(removing_wd_condition(BOP)),nl,
277		!.
278		update_infos(_,I,_,I).
279
280		update_infos_aux(EParas,Cond,Infos,Parameters,NewInfos) :-
281		select_used_ids(UsedIds,Infos,I1,EParas,Cond),
282		UsedIds \= [],!,
283		% remove those used identifiers which will be compiled into the predicate
284		sort(Parameters,SParas),
285		ord_intersection(UsedIds,SParas,NewUsedIds),
286		%print(update(Parameters,UsedIds,I1,new(NewUsedIds))),nl,
287		NewInfos = [used_ids(NewUsedIds)|I1].
288
289		:- use_module(bsyntaxtree,[find_identifier_uses/3]).
290	?	select_used_ids(UsedIds,Infos,I1,_,_) :- select(used_ids(UsedIds),Infos,I1),!.
291		% check_used_ids_info(Parameters,Condition,UsedIds,b_compiler)
292		select_used_ids(UsedIds,Infos,Infos,_Parameters,Condition) :-
293		%add_error(bcompiler,'Expected information of used identifiers in exists operation information : ',Parameters:Infos), %% missing info can happen due to simplifcation rules below !
294		find_identifier_uses(Condition, [], UsedIds). % ,print(used(UsedIds,in_exist(Parameters))),nl.
295		% TO DO: avoid re-computing used-ids; we should refactor b_compile2 to return new Info field
296
297
298
299		evaluate_this(eval,X,Type,Info) :- !, worth_it_type(Type,X,Info).
300		evaluate_this(_,function(A,B),Type,Info) :- !,
301		A=b(value(VA),_,_), nonvar(VA), VA=avl_set(_),
302		B=b(value(_),_,_),
303		worth_it_type(Type,function(A,B),Info). % will check well-definedness
304		evaluate_this(_,X,_Type,_Info) :- wd_and_efficient(X).
305
306
307		% things which are very quick to compute
308		wd_and_efficient(sequence_extension(_)) :- !.
309		wd_and_efficient(set_extension(_)) :- !.
310		wd_and_efficient(integer_set(_)) :- !. % will be converted into value(global_set(_))
311		%% wd_and_efficient(value(_)) :- !. % is already computed
312		% the following will reduce the size of the representation; usually a good thing;
313		% we assume only avl_sets apprear here; inner set comprehensions are never computed into symbolic form by b_compile (see known_value below):
314		%wd_and_efficient(identity(_)) :- !.
315		wd_and_efficient(range(_)) :- !.
316		wd_and_efficient(domain(_)) :- !.
317		wd_and_efficient(domain_restriction(_,_)) :- !.
318		wd_and_efficient(domain_subtraction(_,_)) :- !.
319		wd_and_efficient(range_restriction(_,_)) :- !.
320		wd_and_efficient(range_subtraction(_,_)) :- !.
321		wd_and_efficient(intersection(_,_)) :- !.
322		wd_and_efficient(set_subtraction(_,_)) :- !.
323		wd_and_efficient(image(_,_)) :- !.
324		wd_and_efficient(reverse(_)) :- !. % added for rgen_rgen_Worst_Case_Stopping_distance_NCT_trm13
325		% reverse has n.log(n) complexity, but is always wd and can be beneficial
326		wd_and_efficient(union(A,B)) :- finite_set(A), finite_set(B), !. % has complexity n
327		% usually the union of two avl_sets will be smaller than keeping them separate, what about intervals?
328		wd_and_efficient(interval(_,_)) :- !. % ditto
329		wd_and_efficient(card(S)) :- !, % added for rgen_rgen_Worst_Case_Stopping_distance_NCT_trm13
330		(finite_set(S) -> true % is wd for finite set; has currently linear complexity but reduces size of closure
331		; is_interval(S) -> true). % card is simple to compute
332		wd_and_efficient(min(S)) :- !, % logarithmic for avl_set, see test 1338
333		finite_non_empty_set(S).
334		wd_and_efficient(max(S)) :- !, % logarithmic for avl_set
335		finite_non_empty_set(S).
336		wd_and_efficient(string_set) :- !.
337		% some other efficient operators:
338		% external_function_call CHOOSE (test 1338) ?
339		% first, last, ... need to ensure we have sequence
340		wd_and_efficient(X) :- worth_it_int(X),!.
341		wd_and_efficient(X) :- worth_it_other(X).
342
343		is_interval(b(value(V),set(_),_)) :- nonvar(V), V=closure(P,T,B),
344		is_fixed_interval(P,T,B,_,_).
345
346		finite_set(b(value(V),set(_),_)) :- nonvar(V), finite_set_aux(V).
347		finite_set_aux([]).
348		finite_set_aux(avl_set(_)).
349		finite_non_empty_set(b(value(V),set(_),_)) :- nonvar(V), V=avl_set(_).
350
351		fast_check_wd(b(E,_,Infos)) :-
352		(nonmember(contains_wd_condition,Infos) -> true
353		; nonvar(E), E=value(_)).
354
355		check_wd(NTExpr) :- bsyntaxtree:always_well_defined(NTExpr). % ,print(wd(NTExpr)),nl.
356		%(bsyntaxtree:always_well_defined(NTExpr) -> true ; print(not_guaranteed_wd(NTExpr)),nl).
357
358		% (worth_it_type(Type,X,Info) -> true ; X=value(_) -> true ; print(not_evaluating(X)),nl,fail).
359		worth_it_type(integer,X,Info) :- worth_it_int_wd(X),!, check_wd(b(X,integer,Info)).
360		worth_it_type(T,function(A,B),Info) :- !,
361		(check_wd(b(function(A,B),T,Info)) -> true
362		; fail). %print('not_precompiling_function '),translate:print_bexpr(A), print(' @ '), translate:print_bexpr(B),nl,fail).
363		worth_it_type(integer,X,_) :- worth_it_int(X),!.
364		worth_it_type(T,X,Info) :- worth_it_wd(X),!, check_wd(b(X,T,Info)).
365	?	worth_it_type(set(_),X,_) :- worth_it_set(X),!.
366		worth_it_type(seq(_),X,_) :- worth_it_set(X),!.
367		worth_it_type(_,X,_) :- worth_it_other(X).
368
369		% TO DO: we should use the predicate has_wd_condition from b_ast_cleanup
370
371		% integer operations that could generate WD-errors
372		worth_it_int_wd(div(_,_)).
373		worth_it_int_wd(max(_)).
374		worth_it_int_wd(min(_)).
375		worth_it_int_wd(mod(_,_)).
376		worth_it_int_wd(power_of(_,_)).
377		worth_it_int_wd(card(_)). % has WD condition !!
378		worth_it_int_wd(size(_)).
379
380		% other operations that could generate WD-errors
381		worth_it_wd(first(_)).
382		worth_it_wd(last(_)).
383		worth_it_wd(tail(_)).
384		worth_it_wd(front(_)).
385		worth_it_wd(restrict_front(_,_)).
386		worth_it_wd(restrict_tail(_,_)).
387		worth_it_wd(rel_iterate(_,_)). %% could be expensive
388		worth_it_wd(general_intersection(_)).
389		worth_it_wd(general_concat(_)).
390
391		% to do: check other operators that could be not well-defined !
392
393		worth_it_int(unary_minus(_)).
394		worth_it_int(add(_,_)).
395		worth_it_int(minus(_,_)).
396		worth_it_int(multiplication(_,_)).
397		worth_it_int(max_int).
398		worth_it_int(min_int).
399
400		%worth_it_set(empty_set). % treated below
401		%worth_it_set(empty_sequence). % treated below
402		%worth_it_set(closure(_)). % this is closure1; it is currently always kept symbolic and can be counterproductive to compile; e.g., card(closure1(%x.(x : 1 .. 200|x + 1)))
403		%% ?? need to be more careful here; can be expensive --> need to keep track which parts need definitely to be evaluated
404		worth_it_set(integer_set(_)). % will be converted into value(global_set(_))
405	?	worth_it_set(comprehension_set(A,B)) :- b_ast_cleanup:is_integer_set(comprehension_set(A,B),_).
406		worth_it_set(interval(_,_)).
407		worth_it_set(reflexive_closure(A)) :- \+ symbolic_value(A).
408		worth_it_set(reverse(_)). % function inverse
409		worth_it_set(domain(_)). worth_it_set(range(_)).
410		worth_it_set(union(_,_)). worth_it_set(intersection(_,_)). worth_it_set(set_subtraction(_,_)).
411		worth_it_set(image(_,B)) :- \+ symbolic_value(B).
412		worth_it_set(composition(_,_)).
413		worth_it_set(domain_restriction(_,_)). worth_it_set(domain_subtraction(_,_)).
414		worth_it_set(range_restriction(_,_)). worth_it_set(range_subtraction(_,_)).
415		worth_it_set(direct_product(A,B)) :- \+ symbolic_value(A), \+ symbolic_value(B).
416		worth_it_set(parallel_product(A,B)) :- \+ symbolic_value(A), \+ symbolic_value(B).
417		worth_it_set(iteration(_,_)).
418		worth_it_set(set_extension([H|_])) :- \+ symbolic_value(H). % otherwise we may get an enumeration warning
419		worth_it_set(sequence_extension([H|_])) :- \+ symbolic_value(H). % ditto, TODO: check tail unless expensive
420		worth_it_set(rev(_)). % reverse of sequence
421		worth_it_set(concat(_,_)).
422		worth_it_set(seq(_)). % will be kept symbolic anyway
423		worth_it_set(seq1(_)). % will be kept symbolic anyway; relevant for test 1731
424		% f=%x.(x:iseq(struct(a:seq1(NATURAL),b:BOOL))|x) & f([rec(a:[222],b:TRUE)])=[rec(a:[222],b:xx)] & xx=TRUE
425		% however: value can be put into a set-extension!
426		worth_it_set(iseq(_)). % will be kept symbolic anyway
427		worth_it_set(iseq1(_)). % will be kept symbolic anyway
428		worth_it_set(perm(_)). % will be kept symbolic anyway
429		worth_it_set(pow_subset(_)). % will be kept symbolic anyway
430		worth_it_set(pow1_subset(_)). % will be kept symbolic anyway
431		worth_it_set(fin_subset(_)). % will be kept symbolic anyway
432		worth_it_set(fin1_subset(_)). % will be kept symbolic anyway
433		worth_it_set(general_union(X)) :- \+ symbolic_value(X). % otherwise we can get enumeration warnings
434		worth_it_set(identity(_)).
435		worth_it_set(first_of_pair(_)). % can also produce set
436		worth_it_set(second_of_pair(_)). % can also produce set
437		worth_it_set(cartesian_product(_,_)). % will usually be kept symbolic
438		worth_it_set(string_set). % ensure we have values inside compiled closures, e.g., for custom_explicit_set card computations
439		worth_it_set(bool_set).
440
441		symbolic_value(b(value(Val),_,_)) :- nonvar(Val), symbolic_val_aux(Val).
442		symbolic_val_aux(closure(P,T,B)) :- \+ is_fixed_interval(P,T,B,_,_).
443		symbolic_val_aux(global_set(_)).
444
445		:- use_module(external_functions,[not_declarative/1,external_fun_has_wd_condition/1,
446		expects_unevaluated_args/1]).
447		worth_it_other(boolean_true).
448		worth_it_other(boolean_false).
449		worth_it_other(real(_)).
450		worth_it_other(string(_)).
451		worth_it_other(first_of_pair(_)).
452		worth_it_other(second_of_pair(_)).
453		worth_it_other(couple(_,_)).
454		worth_it_other(record_field(_,_)).
455		worth_it_other(external_function_call(FunName,_)) :-
456		\+ not_declarative(FunName),
457		\+ external_fun_has_wd_condition(FunName). %print(compile(FunName)),nl.
458		% CHOOSE for finite_non_empty_set ?
459		worth_it_other(rec(_)).
460		worth_it_other(struct(_)).
461		%worth_it_other(value(_)). % does not have to be evaluted; already a value
462
463		/*
464		% To do: distinguish which parts definitely need to be evaluated
465		%dont_eval_subexpressions(member). % special membership code can be used
466		%dont_eval_subexpressions(not_member). % special membership code can be used
467		dont_eval_subexpressions(disjunct(_,_)). % it may not be necessary to eval RHS
468		dont_eval_subexpressions(implication(_,_)). % it may not be necessary to eval RHS
469		*/
470
471		:- use_module(bsyntaxtree, [get_negated_operator_expr/2]).
472		:- use_module(kernel_objects,[equal_object/3]).
473		:- use_module(kernel_mappings,[binary_boolean_operator/3]).
474		:- use_module(kernel_tools,[filter_cannot_match/4, get_template_for_filter_cannot_match/2]).
475		b_compile2(Exp,_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,WF) :- var(Exp), !,
476		add_internal_error_wf(b_compiler,'Variable Expression: ',Exp,unknown,WF),
477		NExpr=Exp, FullyKnown=false.
478		b_compile2(truth,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=truth, FullyKnown=false. % predicates never fully known
479		b_compile2(falsity,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=falsity, FullyKnown=false. % predicates never fully known
480		b_compile2(empty_set,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true.
481		b_compile2(empty_sequence,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value([]), FullyKnown=true.
482		b_compile2(boolean_false,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value(pred_false), FullyKnown=true.
483		b_compile2(boolean_true,_,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !, NExpr=value(pred_true), FullyKnown=true.
484		b_compile2(value(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !,
485		NExpr=value(Val),
486		(known_value(Val) -> % ground(Val) -> known_value ?
487		FullyKnown=true ; FullyKnown=false).
488		b_compile2(integer(Val),_Parameters,_LS,_S,NExpr,_Eval,FullyKnown,_WF) :- !,
489		NExpr=value(int(Val)), (number(Val) -> FullyKnown=true ; FullyKnown=false).
490		b_compile2(lazy_lookup_pred(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- !,
491		( ord_member(Id,Parameters) -> %print(lazy_lookup_pred_id_as_parameter(Id,Parameters)),nl,
492		NExpr = lazy_lookup_pred(Id), FullyKnown=false
493		; compute_lazy_lookup(Id,lazy_lookup_pred(Id),LS,S,NExpr,FullyKnown,WF)
494		).
495		b_compile2(lazy_lookup_expr(Id),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :- !,
496		( ord_member(Id,Parameters) -> %print(lazy_lookup_expr_id_as_parameter(Id,Parameters)),nl,
497		NExpr = lazy_lookup_expr(Id), FullyKnown=false
498		; compute_lazy_lookup(Id,lazy_lookup_expr(Id),LS,S,NExpr,FullyKnown,WF)
499		).
500
501		% treat a few common cases, more efficiently than syntaxtransformation
502		b_compile2(equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
503		FullyKnown=false, % predicates never evaluated in b_compile1
504	?	b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
505	?	b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
506		( FullyKnownA=true, FullyKnownB=true,
507		NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_)
508		-> (equal_object(VA,VB,b_compile2_1) -> NExpr = truth ; NExpr = falsity)
509		; generate_equality(NExprA,NExprB,NExpr)
510		).
511		b_compile2(not_equal(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
512		FullyKnown=false, % predicates never evaluated in b_compile1
513		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
514		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
515		( FullyKnownA=true, FullyKnownB=true,
516		NExprA = b(value(VA),_,_), NExprB = b(value(VB),_,_)
517		-> %print(computing_neq(VA,VB)),nl,
518		(kernel_objects:equal_object(VA,VB,b_compile2_2) -> NExpr = falsity ; NExpr = truth)
519		%, print(result(NExpr)),nl
520		; NExpr = not_equal(NExprA,NExprB)
521		).
522		b_compile2(member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
523		FullyKnown=false, % predicates never evaluated in b_compile1
524	?	b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
525		(NExprB = b(value(X),BT,BI)
526		-> (X==[], always_well_defined(A) -> NExpr = falsity
527	?	; b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
528		% check if we can decide membership (e.g., 1:{1})
529	?	(quick_test_membership1(NExprA,X,PRes)
530		-> convert_pred_res(PRes,NExpr)
531		% TO DO: maybe optimize x: {y|P(y)} --> P(x) ; by commenting in code below
532		% However, ensure test 273 succeeds and closure equality correctly detected (e.g., for BV16 = {bt|bt : BIT_VECTOR & bv_size(bt) = 16})
533		% ; (get_texpr_id(NExprA,IDA),
534		% get_comprehension_set(NExprB,IDB,Pred), get_texpr_info(NExprB,Info),
535		% print(rename(IDB,IDA,Info)),nl,
536		% bsyntaxtree:rename_bt(Pred,[rename(IDB,IDA)],PredA)) -> get_texpr_expr(PredA,NExpr)
537		; custom_explicit_sets:singleton_set(X,El) % replace x:{El} -> x=El
538		-> get_texpr_type(NExprA,TA),
539		generate_equality_with_value(NExprA,FullyKnownA,El,FullyKnownB,TA,NExpr)
540		; get_template_for_filter_cannot_match(NExprA,VA)
541		-> filter_cannot_match(X,VA,NewX,Filtered),
542		% (Filtered=false -> true ; print(filtered(NewX,VA,X)),nl),
543		(Filtered=false -> NExpr = member(NExprA,NExprB)
544		; (NewX==[], always_well_defined(A)) -> NExpr = falsity
545		; custom_explicit_sets:singleton_set(NewX,El)
546		-> get_texpr_type(NExprA,TA),
547		%nl,print(create_equal(NExprA,FullyKnownA,El,FullyKnownB,NExprB)),nl,nl,
548		generate_equality_with_value(NExprA,FullyKnownA,El,FullyKnownB,TA,NExpr)
549		; NExpr = member(NExprA, b(value(NewX),BT,BI))
550		)
551		% end fo filtering
552		; NExpr = member(NExprA,NExprB)
553		)
554		% , print('compile: '),print(NExpr),nl
555		)
556		; NExpr = member(NExprA,NExprB),
557		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF)
558		).
559		% TO DO: also optimize things like: (ev1 |-> 0) |-> eg : #221:{((1|->0)|->3),((2|->0)|->0),...,((233|->0)|->218),((234|->0)|->228)}
560
561		b_compile2(not_member(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
562		FullyKnown=false, % predicates never evaluated in b_compile1
563		b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
564		(NExprB = b(value(X),_,_)
565		-> (X==[], always_well_defined(A) -> NExpr = truth
566		; b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
567		(quick_test_membership1(NExprA,X,PRes)
568		-> convert_neg_pred_res(PRes,NExpr)
569		; NExpr = not_member(NExprA,NExprB))
570		)
571		; NExpr = not_member(NExprA,NExprB),
572		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF)
573		).
574		b_compile2(function(Fun,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
575		(is_lazy_extension_function_for_fun_app(Fun)
576		-> Eval1=false % extension function applications treated lazily
577		% TO DO: first evaluate B, if known then only evaluate relevant part of extension function
578		; Eval1=Eval),
579		b_compile1(Fun,Parameters,LS,S,NExprA,Eval1,FullyKnown1,WF),
580		combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown12),
581		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
582		%tools_printing:print_term_summary(compiled_function(FullyKnown1,FullyKnown2,NExprA,NExprB)),nl,
583		(FullyKnown2=true,
584		(NExprA=b(value(_),_,_) -> true % no WD issue can be removed by apply, value already computed
585		; preferences:preference(find_abort_values,false) % in a sequence extension we could remove non-WD elements
586		),
587		% check if we have enough information to apply a partially specified function as a list
588		% e.g. if the function is [(int(1),A),(int(2),B)] and the argument is int(2): we can apply the function without knowing A or B; can have a dramatic importance when expanding unversal quantifiers !
589	?	can_apply_partially_specified_function(NExprA,NExprB,ResultExpr,WF)
590		-> NExpr = ResultExpr,
591		(FullyKnown12=true -> FullyKnown=true
592		; ResultExpr=value(ResultValue),known_value(ResultValue) -> FullyKnown=true
593		; FullyKnown = false)
594		; %tools_printing:print_term_summary(cannot_apply_function(FullyKnown2,NExprA,NExprB)),nl,
595		%translate:print_bexpr(NExprA),nl, translate:print_bexpr(NExprB),nl,
596		NExpr = function(NExprA,NExprB), FullyKnown = FullyKnown12).
597
598		b_compile2(conjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
599		FullyKnown=false, % predicates never automatically evaluated in b_compile1
600	?	b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
601		(is_falsity(NExprA) -> NExpr = falsity
602		;
603		% TO DO: propagate static information from A to B, e.g. if A :: x=10 -> add x=10 to LS/Parameters
604		% also: try and detect unsatisfiable predicates beforehand
605	?	b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
606		(is_falsity(NExprB) -> NExpr = falsity
607		; is_truth(NExprB) -> get_texpr_expr(NExprA,NExpr)
608		; is_truth(NExprA) -> get_texpr_expr(NExprB,NExpr)
609		; NExpr = conjunct(NExprA,NExprB))
610		).
611		b_compile2(disjunct(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
612		FullyKnown=false, % predicates never automatically evaluated in b_compile1
613	?	b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
614		(is_truth(NExprA) -> NExpr = truth
615	?	; b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed
616		(is_truth(NExprB) -> NExpr = truth
617		; is_falsity(NExprA) -> get_texpr_expr(NExprB,NExpr)
618		; is_falsity(NExprB) -> get_texpr_expr(NExprA,NExpr)
619		; NExpr = disjunct(NExprA,NExprB))
620		).
621		b_compile2(implication(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
622		FullyKnown=false, % predicates never automatically evaluated in b_compile1
623		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
624		(is_falsity(NExprA) -> NExpr = truth
625		; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF), get_texpr_expr(NExprB,NExpr)
626		; NExpr = implication(NExprA,NExprB),
627		b_compile1(B,Parameters,LS,S,NExprB,false,_,WF) % B does not have to be executed in a successful branch: set Eval to false to avoid computing expensive expressions which may not be needed
628		% TO DO: add preference to force pre-computation everywhere and pass Eval instead of false to b_compile1; ditto for disjunction
629		).
630		b_compile2(negation(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
631		FullyKnown=false, % predicates never automatically evaluated in b_compile1
632		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
633		( get_negated_operator_expr(NExprA,NegatedA) -> NExpr = NegatedA
634		; NExpr = negation(NExprA)
635		).
636		b_compile2(if_then_else(A,B,C),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
637		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
638		(is_falsity(NExprA) -> b_compile1(C,Parameters,LS,S,NExprC,Eval,FullyKnown,WF), get_texpr_expr(NExprC,NExpr)
639		; is_truth(NExprA) -> b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown,WF), get_texpr_expr(NExprB,NExpr)
640		; NExpr = if_then_else(NExprA,NExprB,NExprC), FullyKnown=false,
641		b_compile1(B,Parameters,LS,S,NExprB,false,_,WF), % set Eval to false as we do not know if B will be needed
642		b_compile1(C,Parameters,LS,S,NExprC,false,_,WF) % ditto for C
643		).
644		/* b_compile2(comprehension_set(CParas,Body),Parameters,LS,S,NExpr,_Eval,FullyKnown,WF) :-
645		sort(Parameters,SParas),
646		b_ast_cleanup:not_occurs_in_predicate(SParas,Body), %can only be applied if Body does not reference Parameters
647		!,
648		b_generate_inner_closure_if_necessary(Parameters,CParas,Body,LS,S,Result), % will itself call b_compile
649		NExpr = value(Result),
650		(ground(Result) -> FullyKnown=true ; FullyKnown=false). */
651		b_compile2(forall(ForallPara,A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
652		FullyKnown=false, % predicates never automatically evaluated in b_compile1
653		get_texpr_ids(ForallPara,AtomicIds),
654		add_parameters(Parameters,AtomicIds,NParameters),
655		b_compile1(A,NParameters,LS,S,NA,Eval,_FullyKnownA,WF),
656		(is_falsity(NA) -> NExpr = truth
657		; b_compile1(B,NParameters,LS,S,NB,Eval,_FullyKnownB,WF),
658		(is_truth(NB) -> NExpr = truth
659		; NExpr = forall(ForallPara,NA,NB)
660		% TO DO ??: if we have an equality -> replace Body by value and remove quantifier
661		%,print('COMPIlED: '),translate:print_bexpr(b(NExpr,pred,[])),nl
662		)
663		).
664		% some special cases to avoid calling syntaxtransformation
665		b_compile2(record_field(A,FieldName),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
666		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
667		% First: we can try compute even if value not fully known !, we just need record field list
668		(get_record_field(NExprA,FieldName,NExpr,FullyKnown) -> true
669		; NExpr = record_field(NExprA,FieldName), FullyKnown=FullyKnownA).
670		b_compile2(couple(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
671		%NExpr = couple(NExprA,NExprB),
672		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
673		combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
674		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
675		(FullyKnown \== true, % evaluation will already combine the result
676		NExprA=b(value(VA),_,_),NExprB=b(value(VB),_,_)
677		-> NExpr = value((VA,VB))
678		; NExpr = couple(NExprA,NExprB)).
679		b_compile2(image(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
680		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
681		combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
682		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
683		(FullyKnown \= true, NExprA=b(value(VA),BT,BI),
684		NExprB=b(value(VB),_,_), nonvar(VB),
685		custom_explicit_sets:singleton_set(VB,VBX)
686		-> filter_cannot_match(VA,(VBX,_),NewVA,_Filtered), %nl,print(filtered_image(VBX,VA,NewVA)),nl,
687		NExpr = image(b(value(NewVA),BT,BI),NExprB)
688		% TO DO: add case where VB==[] or VA==[] are the empty set
689		; NExpr = image(NExprA,NExprB)
690		). %, print('compile image: '),translate:print_bexpr(NExpr),nl.
691		% TO DO: do something like can_apply_partially_specified_function; or filter_can_match
692		b_compile2(composition(A,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
693		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
694		combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
695		NExpr = composition(NExprA,NExprB),
696		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown2,WF),
697		(FullyKnown=false, Eval=eval, performance_monitoring_on,
698		( FullyKnown1=true, NExprB=b(value(_),_,Info), large_known_value(NExprA,2)
699		-> true %translate:nested_print_bexpr(NExprB),nl
700		; FullyKnown2=true, NExprA=b(value(_),_,Info), large_known_value(NExprB,2)
701		-> true %translate:nested_print_bexpr(NExprA),nl
702		)
703		-> perfmessage(b_compiler,'Cannot compile relational composition (try lift it out of quantification)',Info)
704		; true).
705		b_compile2(assertion_expression(A,Msg,B),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
706		b_compile1(A,Parameters,LS,S,NExprA,Eval,_,WF),
707		(is_truth(NExprA) -> % the ASSERT EXPR is redundant
708		%print(removed_assert),nl, translate:print_bexpr(B),nl,
709		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnown,WF),
710		get_texpr_expr(NExprB,NExpr)
711		; b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF),
712		FullyKnown=false, % we cannot get rid of WD condition
713		NExpr = assertion_expression(NExprA,Msg,NExprB)
714		).
715		b_compile2(domain(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
716		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
717		(FullyKnown1=false,get_texpr_expr(NExprA,NA),evaluate_domain(NA,Domain) % try and compute domain even if not fully known
718		-> FullyKnown = true, NExpr = value(Domain)
719		; FullyKnown = FullyKnown1, NExpr = domain(NExprA)).
720		b_compile2(range(A),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
721		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown1,WF),
722		(FullyKnown1=false,evaluate_range(NExprA,Range) % try and compute range even if not fully known
723		-> FullyKnown = true, NExpr = value(Range)
724		; FullyKnown = FullyKnown1, NExpr = range(NExprA)).
725		b_compile2(assign(LHS_List,RHS_List),Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- !,
726		NExpr = assign(New_LHS_List,NewRHS_List), FullyKnown = false,
727		maplist(b_compile_lhs(Parameters,LS,S,Eval,WF),LHS_List,New_LHS_List),
728		b_compile_l(RHS_List,Parameters,LS,S,NewRHS_List,Eval,_FullyKnown2,WF).
729		b_compile2(assign_single_id(ID,B),Parameters,LS,S,assign_single_id(ID,NExprB),Eval,FullyKnown,WF) :- !,
730		FullyKnown = false,
731		b_compile1(B,Parameters,LS,S,NExprB,Eval,_,WF).
732		b_compile2(operation_call(Operation,OpCallResults,OpCallParas),Parameters,LS,S,InlinedOpCall,Eval,FullyKnown,WF) :-
733		% TO DO: evaluate if we should also use the let_expression_global approach used for operation_call_in_expr
734		!,
735		def_get_texpr_id(Operation,op(OperationName)),
736		FullyKnown = false,
737		b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF),
738		TopLevel=false,
739		b_get_machine_operation_for_animation(OperationName,OpResults,OpFormalParameters,Body,_OType,TopLevel),
740		bsyntaxtree:replace_ids_by_exprs(Body,OpResults,OpCallResults,Body2),
741		get_texpr_ids(OpFormalParameters,OpIds),
742		add_parameters(Parameters,OpIds,InnerParas),
743		b_compile1(Body2,InnerParas,[],S,NBody,Eval,FullyKnown,WF), % do not pass local state: this may override constants,... from the called machine
744		% Note: global state S should be valid for all machines in currently loaded specification
745		get_texpr_ids(OpCallResults,OpRIds),
746		add_parameters(Parameters,OpRIds,LocalKnownParas),
747		simplify_assignment(OpFormalParameters,OpCallParaValues,LHSFormalParas,RHSCallVals), %%
748		split_formal_parameters(LHSFormalParas,RHSCallVals,LocalKnownParas,
749		FreshOpParas,FreshCallVals,
750		ClashOpParas, ClashCallVals), % only set up VAR for fresh Paras
751		% print(split(LHSFormalParas,LocalKnownParas,fresh(FreshOpParas),clash(ClashOpParas))),nl,
752		(FreshOpParas=[] -> get_texpr_expr(NBody,Let1)
753		; create_equality_for_let(FreshOpParas,FreshCallVals,Equality1),
754		Let1 = let(FreshOpParas,Equality1,NBody)),
755		(ClashOpParas = []
756		-> InlinedOpCall = Let1
757		; %nl,print(clash(ClashOpParas)),nl,
758		maplist(create_fresh_id,ClashOpParas,FreshCopy),
759		create_equality_for_let(ClashOpParas,FreshCopy,Equality2), % copy Values from Fresh Ids
760		create_equality_for_let(FreshCopy,ClashCallVals,Equality3), % assign Parameter Vals to Fresh Ids
761		get_texpr_pos(Body,BodyPos), BodyPosInfo = [nodeid(BodyPos)],
762		Let2 = let(ClashOpParas,Equality2,b(Let1,subst,[BodyPosInfo])),
763		InlinedOpCall = let(FreshCopy,Equality3,b(Let2,subst,[BodyPosInfo]))
764		).
765		%, print('Compiled operation call: '), translate:print_subst(b(InlinedOpCall,subst,BodyPosInfo)),nl,nl.
766		% Maybe this version is faster when no OpCallResults:
767		%b_compile2(operation_call(Operation,OpCallResults,OpCallParas),Parameters,LS,S,InlinedOpCall,Eval,FullyKnown,WF) :-
768		% OpCallResults=[],
769		% !,
770		% def_get_texpr_id(Operation,op(OperationName)),
771		% FullyKnown = false,
772		%% b_compile_l(Results,Parameters,LS,S,NResults,Eval,_,WF),
773		% b_compile_l(OpCallParas,Parameters,LS,S,OpCallParaValues,Eval,_,WF),
774		% TopLevel=false,
775		% b_get_machine_operation_for_animation(OperationName,OpResults,OpParameters,Body,_OType,TopLevel),
776		% % Note: input parameters cannot be assigned to: so replace ids is ok
777		% % However, we cannot replace output parameters: these can be assigned to and we can have aliasing
778		% % Note: no aliasing is allowed in OpCallResults (cf Atelier-B handbook x,x <-- op not allowed)
779		% bsyntaxtree:replace_ids_by_exprs(Body,OpParameters,OpCallParaValues,Body2),
780		% get_texpr_ids(OpResults,OpIds),
781		% append(OpIds,Parameters,InnerParas),
782		% b_compile1(Body2,InnerParas,LS,S,NBody,Eval,FullyKnown,WF),
783		% FinalBody = NBody.
784		b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
785		functor(Expr,BOP,2),
786		binary_boolean_operator(BOP,_,_),!, % from kernel_mappings, slightly more efficient than syntaxtransformation
787		arg(1,Expr,A),
788		FullyKnown=false, % predicates never evaluated in b_compile1
789		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
790		arg(2,Expr,B),
791		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
792		(eval_binary_bool(FullyKnownA,NExprA,FullyKnownB,NExprB,BOP,Result)
793		-> NExpr = Result
794		; functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB)
795		).
796		b_compile2(external_function_call(ExtFun,Args),_Parameters,LS,_S,NExpr,_Eval,FullyKnown,_WF) :-
797		expects_unevaluated_args(ExtFun),
798		memberchk(bind('$optimize_do_not_force_lazy_lookups',_),LS), % this is an optimize call
799		!,
800		debug_format(9,'Not compiling external function call to ~w~n',[ExtFun]),
801		NExpr=external_function_call(ExtFun,Args),
802		FullyKnown=false.
803		b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
804		functor(Expr,BOP,2),
805		kernel_mappings:binary_function(BOP,_,_),!, % slightly more efficient than syntaxtransformation
806		arg(1,Expr,A),
807	?	b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnownA,WF),
808		combine_fully_known(FullyKnownA,FullyKnownB,FullyKnown),
809		arg(2,Expr,B),
810		b_compile1(B,Parameters,LS,S,NExprB,Eval,FullyKnownB,WF),
811		functor(NExpr,BOP,2), arg(1,NExpr,NExprA), arg(2,NExpr,NExprB).
812		b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :-
813		functor(Expr,UOP,1),
814		kernel_mappings:unary_function(UOP,_,_),!, % slightly more efficient than syntaxtransformation
815		arg(1,Expr,A),
816		b_compile1(A,Parameters,LS,S,NExprA,Eval,FullyKnown,WF),
817		functor(NExpr,UOP,1), arg(1,NExpr,NExprA).
818		b_compile2(Expr,Parameters,LS,S,NExpr,Eval,FullyKnown,WF) :- % GENERAL CASE
819		%hit_profiler:add_profile_hit(Expr),
820	?	syntaxtransformation(Expr,Subs,Names,NSubs,NExpr),
821		get_texpr_ids(Names,Ids),
822		add_parameters(Parameters,Ids,NParameters),
823	?	b_compile_l(Subs,NParameters,LS,S,NSubs,Eval,FullyKnown,WF).
824
825		b_compile_l([],_,_,_,[],_Eval,true,_WF).
826		b_compile_l([Expr|ExprRest],P,LS,S,[NExpr|NExprRest],Eval,FullyKnown,WF) :-
827	?	b_compile1(Expr,P,LS,S,NExpr,Eval,FullyKnown1,WF),
828		combine_fully_known(FullyKnown1,FullyKnown2,FullyKnown),
829		b_compile_l(ExprRest,P,LS,S,NExprRest,Eval,FullyKnown2,WF).
830
831		% detecth when a parameter clashes with existing known ids
832		id_clash(LocalKnownParas,TID) :- def_get_texpr_id(TID,ID), member(ID,LocalKnownParas).
833
834		/* comment in if we want to compile inner comprehension sets:
835		:- use_module(bsyntaxtree,[split_names_and_types/3]).
836		:- use_module(closures,[construct_closure_if_necessary/4]).
837		b_generate_inner_closure_if_necessary(OuterParameters,ClosureParas,Condition,LocalState,State,Result) :-
838		split_names_and_types(ClosureParas,Names,Types),
839		add_parameters(OuterParameters,Names,FullNames),
840		b_compile(Condition,FullNames,LocalState,State,ClosurePred),
841		print('INNER COMPILE: '), translate:print_bexpr(ClosurePred),nl,
842		construct_closure_if_necessary(Names,Types,ClosurePred,Result).
843		*/
844
845
846		% the LHS contains l-values which should not be looked up in the environment
847		% however, we need to deal with things like f(i) := RHS and compile i
848		b_compile_lhs(Parameters,LS,S,Eval,WF,TExpr,NewTExpr) :-
849		TExpr = b(Expr,Type,Info), NewTExpr = b(NewExpr,Type,Info),
850		b_compile_lhs_aux(Expr,Parameters,LS,S,NewExpr,Eval,WF).
851
852		b_compile_lhs_aux(function(A,B),Parameters,LS,S,function(NewA,NewB),Eval,WF) :- !,
853		b_compile_lhs(Parameters,LS,S,Eval,WF,A,NewA), % we can have nexted function calls f(e)(g) :=
854		b_compile1(B,Parameters,LS,S,NewB,Eval,_,WF).
855		b_compile_lhs_aux(E,_,_,_,E,_,_WF). % other LHS should be identifier -> just copy
856
857		get_record_field(b(value(Val),_,_),FieldName,value(Field),FullyKnown) :- !,
858		nonvar(Val), Val=rec(Fields),
859		safe_get_field(Fields,FieldName,Field),
860		known_value(Field,FullyKnown).
861		get_record_field(b(function(FUN,ARG),_Type,_Info),FieldName,function(ReducedFUN,ARG),false) :-
862		% {1|->rec(a:1,b:2),...}(x)'b --> {1|->2,...}(x)
863		%nl,print(get_field(FUN,ARG,FieldName)),nl,
864		% TO DO: also allow nested functions calls {1|->rec(a:1,b:2),...}(x)(y)'b or other reduction operators
865		get_field_in_range(FUN,FieldName,ReducedFUN).
866		safe_get_field(V,FN,_) :- (var(V) ; var(FN)),!,fail.
867		safe_get_field([field(N,V)|T],FieldName,Result) :- nonvar(N),
868		(N=FieldName -> Result=V ; safe_get_field(T,FieldName,Result)).
869
870		:- use_module(probsrc(custom_explicit_sets),[expand_custom_set_to_list/4, convert_to_avl/2]).
871		:- use_module(probsrc(avl_tools),[avl_height_less_than/2]).
872		get_field_in_range(b(value(OldVal),set(couple(Dom,OldRange)),Info),FieldName,
873		b(value(NewVal),set(couple(Dom,NewRange)),Info)) :-
874		nonvar(OldVal), OldVal=avl_set(AVL),
875		avl_height_less_than(AVL,10),
876		OldRange = record(Fields),
877		member(field(FieldName,NewRange),Fields),!,
878		expand_custom_set_to_list(avl_set(AVL),List,_,get_field_in_range),
879		maplist(safe_get_range_field(FieldName),List,NewList),
880		convert_to_avl(NewList,NewVal).
881
882		% compute the field access for the range elements:
883		safe_get_range_field(FieldName,(Dom,rec(Fields)),(Dom,Field)) :- safe_get_field(Fields,FieldName,Field).
884
885
886		eval_binary_bool(true,b(value(ValA),_,_),true,b(value(ValB),_,_),BOP,Result) :-
887		ground(ValA),
888		ground(ValB),
889		eval_binary_aux(BOP,ValA,ValB,Result).
890
891		eval_binary_aux(less,int(A),int(B),Result) :-
892		(A < B -> Result = truth ; Result = falsity).
893		eval_binary_aux(greater,int(A),int(B),Result) :-
894		(A > B -> Result = truth ; Result = falsity).
895		eval_binary_aux(less_equal,int(A),int(B),Result) :-
896		(A =< B -> Result = truth ; Result = falsity).
897		eval_binary_aux(greater_equal,int(A),int(B),Result) :-
898		(A >= B -> Result = truth ; Result = falsity).
899		eval_binary_aux(subset,avl_set(A1),avl_set(A2),Result) :-
900		(custom_explicit_sets:check_avl_subset(A1,A2) -> Result = truth ; Result = falsity).
901		eval_binary_aux(subset,[],_,Result) :- Result=truth.
902		%eval_binary_aux(less_real,real(A),real(B),Result) :- % TO DO
903		% (A < B -> Result = truth ; Result = falsity).
904		% TO DO: other operators are not_subset, strict_subset, ... intervals for subset,...
905
906
907
908		:- use_module(store,[lookup_value_for_existing_id_wf/5]).
909		compute_lazy_lookup(Id,Expr,LS,S,NExpr,FullyKnown,WF) :-
910		lookup_value_for_existing_id_wf(Id,LS,S,(Evaluated,Value),WF),
911		% the lazy expression has already been registered, but maybe not yet evaluated
912		!,
913		known_value(Value,FullyKnown), % compute if value fully known
914		(Evaluated==pred_true -> NExpr = value(Value)
915		; FullyKnown==true -> NExpr = value(Value)
916		; memberchk(bind('$optimize_do_not_force_lazy_lookups',_),LS)
917		-> NExpr = Expr % we do not force lookup: there could be WD issues !
918		% TO DO: examine Infos for wd_condition; we could also return NExpr = lazy_value(Id,Evaluated,Value)
919		; if(Evaluated = pred_true,
920		% will force evaluation ! Note: this means shared expression inside a compiled expression must be well-defined
921		NExpr = value(Value),
922		(add_internal_error_wf(b_compiler,'Compilation failed: ', Id, unknown,WF),
923		fail))
924		).
925		compute_lazy_lookup(Id,_E,_LS,_S,_LazyValue,_,WF) :-
926		add_internal_error_wf(b_compiler,'Compilation failed, illegal lazy_lookup_value: ',Id,unknown,WF),
927		fail.
928
929		combine_fully_known(true,A,A).
930		combine_fully_known(false,_,false).
931
932		:- use_module(tools_lists,[length_greater/2]).
933		% is an extension function with at least two elements, but not too long
934		% (for long set extensions it is much better to compile them to avl once; see private_examples/ClearSy/2019_Sep/rule_dummy)
935		% extension functions are treated lazily in b_interpreter for function application under the condition:
936		% memberchk(contains_wd_condition,FInfo) ; preferences:preference(use_clpfd_solver,false) ; ground_value(ArgValue)
937		is_lazy_extension_function_for_fun_app(b(A,_,FInfo)) :-
938		preferences:preference(data_validation_mode,false),
939		(memberchk(contains_wd_condition,FInfo) -> Lim=98 ; Lim = 23),
940		is_extension_function_aux(A,Lim).
941		is_extension_function_aux(set_extension([_A,_|T]),Lim) :- \+ length_greater(T,Lim).
942		is_extension_function_aux(sequence_extension([_,_|T]),Lim) :- \+ length_greater(T,Lim).
943
944		:- use_module(bsyntaxtree,[is_set_type/2]).
945		% check if we can apply an argument to a partially specified function (as a list and now also as AVL)
946		%can_apply_partially_specified_function(Fun,X,_,_) :- print(fun(Fun)),nl,print(val(X)),nl,fail.
947		can_apply_partially_specified_function(b(Expr,TYPE,_), b(value(X),TA,_),ResultExpr,WF) :-
948	?	can_apply_aux(Expr,TYPE,X,TA,ResultExpr,WF).
949
950		can_apply_aux(value(VAL),TYPE,X,TA,value(ResultValue),WF) :-
951		is_set_type(TYPE,couple(TA,_TB)),
952	?	lookup_result(VAL,X,ResultValue,WF).
953		can_apply_aux(sequence_extension(List),_,X,integer,ResultExpr,_WF) :-
954		% important, e.g., for solving test 1551: {b|[a,b,c](2)=333} =res & a : res & b:res
955		nonvar(X), X=int(Index), number(Index),
956		% this will prevent computing rest of sequence extension: can hide WD issues !
957		% print(apply_seq_extension(Index,List)),nl,
958		nth1(Index,List,b(ResultExpr,_,_)).
959
960		:- use_module(kernel_equality,[equality_objects_wf/4, equality_can_be_decided_by_unification/1]).
961		%lookup_result(VAR,ArgValue,Result,WF) :- var(VAR),!,kernel_mappings:kernel_call_apply_to(VAR,ArgValue,Result,unknown,unknown,WF).
962		% the clause above is unsound; as apply_to CAN RAISE WD ERRORS !! what if we have IF 1:dom(f) THEN f(1) ELSE f(0) END; we do not want to compute f(1) ! it can also instantiate unbound variables !
963		% the idea was to avoid that we wait on the full function, before compiled closure can be evaluated; test 1552
964		% important for e.g. a = {(1, {([]|->2)} ), (2, const(1, [a(1)]))}
965		% or: a = {1 |-> {[] |-> 2}, 2 |-> (dom({pi,ff,p|((pi : seq(INTEGER) & ff : INTEGER) & p : seq(INTEGER)) & (p |-> ff : [a(1)](1) & pi = 1 -> p)}) \/ {[] |-> 1})}
966		% test 1552 is currently skipped
967		% TO DO: think whether there are other deterministic computations that can be done in b_compile: prj1,prj2, record-field access ? this would ensure that closures,... can be computed earlier
968		lookup_result(VAR,_,_,_WF) :- var(VAR),!,fail.
969		lookup_result(avl_set(A),X,Result,_WF) :-
970	?	(custom_explicit_sets:try_apply_to_avl_set(X,Result,A)
971		-> true % precompiled function application
972		; debug_format(19,'Function application in b_compiler for avl_set is not well-defined for: ~w~n',[X]),
973		% We could transform the function application into a construct that raises a WD error
974		fail).
975		lookup_result(closure(_P,_T,_B),_X,_Result,_WF) :- !,
976		fail. % TODO: should we replace parameters by values in body? if domain is full type?
977		lookup_result(List,X,Result,WF) :- List = [_|_],equality_can_be_decided_by_unification(X),!,
978		% this is relevant for long lists,
979		% see public_examples/B/ExternalFunctions/Satsolver/QueensBoardVersionTF_Satsolver.mch
980		fast_lookup_result(List,X,Result,WF).
981		lookup_result(List,X,Result,WF) :-
982		regular_lookup_result_in_list(List,X,Result,WF).
983
984		regular_lookup_result_in_list([],X,_Result,_WF) :-
985		debug_format(19,'Function application in b_compiler for list is not well-defined for: ~w~n',[X]), % ditto
986		fail.
987		regular_lookup_result_in_list([(HFrom,HTo)|T],X,Result,WF) :-
988		equality_objects_wf(HFrom,X,PredRes,WF),
989		%kernel_equality:equality_objects1(HFrom,X,PredRes,WF), % this could be called if X is guaranteed nonvar
990		nonvar(PredRes), % only proceed if we have enough information to determine the result of the comparison
991		(PredRes = pred_true -> Result = HTo % we have found the value; we assume there is no other value later
992		% TO DO: if find_abort_values=true: look later in the list if for all other HFrom PredRes=pred_false
993		; regular_lookup_result_in_list(T,X,Result,WF)).
994
995		% a faster version which does not use equality_objects_wf
996		fast_lookup_result([(HFrom,HTo)|T],X,Result,WF) :-
997		equality_can_be_decided_by_unification(HFrom), !,
998		(HFrom=X -> Result = HTo
999		; fast_lookup_result(T,X,Result,WF)
1000		).
1001		fast_lookup_result(List,X,Result,WF) :-
1002		regular_lookup_result_in_list(List,X,Result,WF).
1003
1004
1005		% get_comprehension_set(b(SET,_,_),ID,PRED) :- get_comprehension_set_aux(SET,ID,PRED).
1006		% get_comprehension_set_aux(comprehension_set([TID],PRED),ID,PRED) :-
1007		% get_texpr_id(TID,ID).
1008		% get_comprehension_set_aux(value(V),ID,PRED) :- nonvar(V), V = closure([ID],_,PRED).
1009
1010
1011
1012
1013		quick_test_membership1(b(value(VA),_,_),VB,Result) :-
1014	?	quick_test_membership_aux(VB,VA,Result).
1015		quick_test_membership_aux(VAR,_,_) :- var(VAR),!,fail.
1016		quick_test_membership_aux([],_,pred_false).
1017		quick_test_membership_aux(avl_set(AVL),X,Result) :-
1018		custom_explicit_sets:quick_test_avl_membership(AVL,X,Result). % we could also check that in case X is not ground but partially instantiated, whether there is a possible match in AVL (if not Result = pred_false)
1019		quick_test_membership_aux(global_set(GS),X,Result) :- nonvar(X), X=int(IX), nonvar(IX),
1020		custom_explicit_sets:membership_global_set(GS,X,R,_WF),
1021		nonvar(R), Result=R.
1022		quick_test_membership_aux(closure(P,T,B),X,Result) :- nonvar(X), X=int(IX), nonvar(IX),
1023		is_fixed_interval(P,T,B,LOW,UP),
1024		kernel_equality:in_nat_range_test(X,int(LOW),int(UP),R),
1025		nonvar(R), Result=R.
1026		quick_test_membership_aux(closure(P,T,B),X,Result) :- X==[], % check {} : POW(_) / FIN(_) and {} : POW1(_) / FIN1(_)
1027	?	custom_explicit_sets:is_powerset_closure(closure(P,T,B),Kind,_),
1028		(contains_empty_set(Kind) -> Result = pred_true ; Result=pred_false).
1029
1030		is_fixed_interval(P,T,B,LOW,UP) :-
1031		custom_explicit_sets:is_interval_closure(P,T,B,LOW,UP), integer(LOW),integer(UP).
1032
1033		contains_empty_set(pow).
1034		contains_empty_set(fin).
1035
1036		convert_pred_res(pred_false,falsity).
1037		convert_pred_res(pred_true,truth).
1038		convert_neg_pred_res(pred_true,falsity).
1039		convert_neg_pred_res(pred_false,truth).
1040
1041		generate_equality(b(A,_,_),b(B,_,_),Res) :-
1042		( generate_equality_aux(A,B,Res) ;
1043		generate_equality_aux(B,A,Res) ),
1044		!.
1045		generate_equality(A,B,equal(A,B)).
1046
1047		generate_equality_aux(convert_bool(AA),value(PT),Res) :-
1048		PT==pred_true,
1049		get_texpr_expr(AA,TA),
1050		!,
1051		Res = TA.
1052		generate_equality_aux(convert_bool(AA),value(PF),Res) :-
1053		PF==pred_false,!,
1054		Res = negation(AA).
1055
1056		% generate an equal(_,_) node where the second one is a Value
1057		generate_equality_with_value(b(value(ValA),_,_),true,ValB,true,_TA,NExpr) :-
1058		% both are FullyKnown
1059		simple_value(ValA), % we should avoid closures
1060		!,
1061		kernel_equality:equality_objects(ValA,ValB,PRes),
1062		convert_pred_res(PRes,NExpr).
1063		generate_equality_with_value(NExprA,_,Value,_,TA,equal(NExprA,b(value(Value),TA,[]))).
1064
1065		% similar to custom_explicit_sets:simple_value
1066		% values where we can decide equality easily
1067		simple_value(fd(_,_)).
1068		simple_value(pred_true /* bool_true */).
1069		simple_value(pred_false /* bool_false */).
1070		simple_value(int(_)).
1071		simple_value((A,B)) :- simple_value(A), simple_value(B).
1072		simple_value(rec(Fields)) :- maplist(simple_field,Fields).
1073		simple_value(string(_)).
1074
1075		simple_field(field(_,Val)) :- simple_value(Val).
1076
1077		known_value(X,FullyKnown) :- (known_value(X) -> FullyKnown=true ; FullyKnown=false).
1078		known_value(X) :- nonvar(X), known_value2(X).
1079		known_value2(global_set(GS)) :- nonvar(GS).
1080		known_value2(freetype(GS)) :- nonvar(GS).
1081		known_value2(closure(P,T,B)) :- known_closure(P,T,B).
1082		%Note: for other closures: they still may have to be computed; some of the computations in wd_and_efficient could be expensive for closures
1083		known_value2(avl_set(_)). % already fully normalised
1084		known_value2((X,Y)) :- known_value(X),known_value(Y).
1085		known_value2(fd(A,B)) :- number(A),atomic(B).
1086		known_value2(int(N)) :- number(N).
1087		known_value2([]).
1088		known_value2(pred_true).
1089		known_value2(pred_false).
1090		known_value2(string(S)) :- atomic(S).
1091		known_value2([H|T]) :- known_value(H), known_value(T).
1092		%known_value2(record(Fields)) :- known_fields(Fields).
1093		known_value2(rec(Fields)) :- known_fields(Fields).
1094
1095		:- use_module(avl_tools,[avl_height_less_than/2]).
1096		% large known avl_set value; for issueing perfmessage warnings
1097		large_known_value(b(value(V),_,_),Lim) :- nonvar(V), large_known_aux(V,Lim).
1098		large_known_aux(avl_set(A),Lim) :-
1099		\+ avl_height_less_than(A,Lim).
1100
1101		% something we could do:
1102		%optimize_known_value([H|T],Res) :- (convert_to_avl([H|T],CS) -> Res=CS ; print(failed_to_convert_known_list),nl,fail).
1103		% try_convert_to_avl
1104
1105		known_closure(P,T,B) :- custom_explicit_sets:is_interval_closure(P,T,B,Low,Up), !,
1106		number(Low), number(Up),
1107		Up < Low+1000.
1108		known_closure(P,T,B) :-
1109		is_cartesian_product_closure(closure(P,T,B),A1,A2),
1110		!,% we could call is_cartesian_product_closure_aux(P,T,B,A1,A2)
1111		known_value(A1), known_value(A2).
1112
1113		known_fields(X) :- var(X),!,fail.
1114		known_fields([]).
1115		known_fields([field(N,V)|T]) :- ground(N),known_value(V),known_fields(T).
1116
1117		%b_evaluate1(TExpr,Parameters,LS,S,ResultTExpr,FullyKnown) :-
1118
1119		check_is_id_list([],[]).
1120		check_is_id_list([H|T],Res) :-
1121		(H=b(identifier(_),_,_)
1122		-> add_internal_error('Typed id list as argument: ',check_is_id_list([H|T],Res)), % use get_texpr_ids or maplist(def_get_texpr_id,P,PIDs)
1123		maplist(def_get_texpr_id,[H|T],Res)
1124		; Res=[H|T]).
1125
1126		:- use_module(kernel_frozen_info,[kfi_domain/2]).
1127
1128		:- use_module(custom_explicit_sets,[construct_interval_closure/3]).
1129		% try and evaluate domain of a list (avl_set already dealt with separately)
1130		%evaluate_domain(X,_) :- print(dom(X)),nl,fail.
1131		evaluate_domain(sequence_extension(L),Domain) :- length(L,Len),
1132		% this will prevent computing range of sequence extension: can hide WD issues ! TO DO: check wd info and/or preference
1133		construct_interval_closure(1,Len,Domain).
1134		% TO DO: set_extension when possible ?
1135		evaluate_domain(value(L),Domain) :-
1136		get_domain(L,Domain).
1137
1138		get_domain(V,Dom) :- var(V),!,kfi_domain(V,Dom). % try infer domain from attached co-routines
1139		get_domain([],[]).
1140		get_domain([V|VT],Result) :- nonvar(V), V=(D,_),
1141		known_value(D),get_list_domain(VT,DT),
1142		%length(DT,Len),print(got_list_domain(D,Len)),nl,
1143		(custom_explicit_sets:try_convert_to_avl([D|DT],Res) -> Result=Res
1144		; write(could_not_convert_domain_to_avl(D)),nl, Result=[D|DT]). %sort([D|DT],Result)?
1145		% we could also do this:
1146		%get_domain(closure(Par,Typ,Body),Result) :-
1147		% is_lambda_value_domain_closure(Par,Typ,Body, DomainValue,Expr), check_wd(Expr),
1148		% Result=DomainValue.
1149		get_list_domain(V,_) :- var(V),!,fail.
1150		get_list_domain([],[]).
1151		get_list_domain([V|VT],[D|DT]) :- nonvar(V), V=(D,_),
1152		known_value(D),get_list_domain(VT,DT).
1153
1154
1155		:- use_module(kernel_frozen_info,[kfi_range/2]).
1156
1157		% try and evaluate range of a list (avl_set already dealt with separately)
1158		evaluate_range(b(value(L),_T,_),Range) :-
1159		get_range(L,Range).
1160		get_range(V,Dom) :- var(V),!,kfi_range(V,Dom). % try infer range from attached co-routines
1161		get_range([],[]).
1162		get_range([V|VT],Result) :- nonvar(V), V=(_,D),
1163		known_value(D),
1164		get_list_range(VT,DT),
1165		sort([D|DT],Result).
1166
1167		get_list_range(V,_) :- var(V),!,fail.
1168		get_list_range([],[]).
1169		get_list_range([V|VT],[D|DT]) :-
1170		nonvar(V), V=(_,D),
1171		known_value(D),
1172		get_list_range(VT,DT).
1173
1174		create_equality_for_let(LHS,RHS,Conj) :-
1175		maplist(create_eq,LHS,RHS,CL),
1176		conjunct_predicates(CL,Conj).
1177		create_eq(Id,Expr,TPred) :- safe_create_texpr(equal(Id,Expr),pred,TPred).
1178
1179		% split formal operation call parameters into those which clash and those that do not:
1180		split_formal_parameters([],[],_,[],[],[],[]).
1181		split_formal_parameters([Formal1|FormalT],[Val1|VT],LocalKnownParas,Fresh,FV,Clash,CV) :-
1182		(id_clash(LocalKnownParas,Formal1)
1183		-> Fresh = FreshT, FV=FVT, Clash = [Formal1|ClashT], CV = [Val1|CVT]
1184		; Fresh = [Formal1|FreshT], FV = [Val1|FVT], Clash = ClashT, CV = CVT
1185		), split_formal_parameters(FormalT,VT,LocalKnownParas,FreshT,FVT,ClashT,CVT).
1186
1187		:- use_module(gensym,[gensym/2]).
1188		create_fresh_id(b(identifier(_),T,I),b(identifier(FRESHID),T,I)) :-
1189		gensym('__COMPILED_ID__',FRESHID).
1190
1191		:- use_module(bsyntaxtree, [get_texpr_pos/2,same_id/3]).
1192		% compute which assignments are really necessary, remove skip assignments x := x
1193		simplify_assignment([],[],[],[]).
1194		simplify_assignment([ID1|T1],[ID2|T2],Res1,Res2) :-
1195		(same_id(ID1,ID2,_) -> Res1=TR1, Res2=TR2 ; Res1=[ID1|TR1], Res2=[ID2|TR2]),
1196		simplify_assignment(T1,T2,TR1,TR2).
1197
1198
1199		/*
1200		% check if an AST term is a total lambda without WD condition:
1201		% NExprA=value(closure([x,...,'_lambda_result_'],b(equal())), NExprB=couple(,,,,) -> replace x by parameters
1202		% possibly better to do this via contains_wd_condition or similar Info field?!
1203
1204
1205		is_total_lambda(b(value(V),_,_),OtherIDs,LambdaExpr) :- nonvar(V),
1206		V=closure(Args,_Types,Body),
1207		is_total_lambda_closure(Args,Body, OtherIDs, LambdaExpr).
1208
1209		:- use_module(probsrc(bsyntaxtree),[conjunction_to_list/2,occurs_in_expr/2]).
1210		is_total_lambda_closure(Args,b(equal(TLambda,LambdaExpr),pred,_),OtherIDs,LambdaExpr) :-
1211		get_texpr_id(TLambda,LambdaID),
1212		append(OtherIDs,[LambdaID],Args),
1213		\+ occurs_in_expr(LambdaID,LambdaExpr).
1214
1215		% try and get arguments from expression
1216		get_actual_arguments([_],Expr,Args) :- !,
1217		% print('arg1: '),tools_printing:print_term_summary(Expr),nl,
1218		check_simple(Expr),
1219		Args= [Expr].
1220		get_actual_arguments([_|T],b(Couple,_,_),[Arg1|TArgs]) :-
1221		get_couple(Couple,Arg1,Arg2), print('arg: '),tools_printing:print_term_summary(Arg1),nl,
1222		check_simple(Arg1),
1223		get_actual_arguments(T,Arg2,TArgs).
1224
1225		check_simple(b(V,_,_)) :- simple2(V).
1226		simple2(value(_)).
1227		simple2(identifier(_)).
1228		simple2(integer(_)).
1229
1230		get_couple(couple(A,B),A,B).
1231		%get_couple(value(V),A,B) :- nonvar(V), V=(V1,V2), ... % TODO
1232
1233
1234		Code for bcompile2(function(...))
1235
1236
1237		% ; is_total_lambda(NExprA,Ids,Expr) ,
1238		% get_actual_arguments(Ids,NExprB,Args) %, print(ok),nl, translate:l_print_bexpr_or_subst(Args),nl
1239		% ->
1240		% bsyntaxtree:replace_ids_by_exprs(Expr,Ids,Args,Result),
1241		% % only ok if we do not replicate expressions !! we could repeatedly re-apply rule / compilation on result
1242		% print(' replaced: '),translate:print_bexpr(Result),nl,
1243		% Result = b(NExpr,_,_), FullyKnown = FullyKnown12
1244
1245		*/