1		% (c) 2009-2025 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(store, [ %store_values_for_existing_ids/4,
6		store_value_for_existing_id/4,
7		variable_is_defined/2,
8		store_value/4,
9		store_updates_and_normalise/3,
10		store_intermediate_updates_wf/5,
11		save_updates_in_existing_store/2,
12		%lazy_store_updates_and_normalise/3,
13		merge_updates/3,
14		get_id_value/3,
15		lookup_value/3,
16		lookup_value/4,lookup_value_with_span_wf/6,
17		lookup_value_without_check/4,
18		lookup_value_for_existing_id/3, lookup_value_for_existing_id/4,
19		lookup_value_for_existing_id_wf/4, lookup_value_for_existing_id_wf/5,
20		lookup_and_delete_value/7,
21		no_value_for_variable/2,
22		empty_state/1,
23		add_var_to_localstate/4,
24		set_up_localstate/4,
25		set_up_undefined_localstate/3, set_up_undefined_localstate_with_predefined/4,
26		delete_variables_from_state/3,
27
28		normalise_value_for_var/3, normalise_value_for_var/4,
29		normalise_value/2,
30		l_normalise_values/2,
31		l_expand_and_normalise_values/2, l_expand_and_normalise_values/3,
32		normalise_store/2,
33		normalise_state/2, normalise_states/2,
34		copy_variable_store/4,
35		check_valid_store/2
36		]).
37
38		:- use_module(library(lists)).
39		:- use_module(self_check).
40		:- use_module(debug).
41
42		:- use_module(typechecker).
43		:- use_module(preferences).
44		:- use_module(tools).
45
46		:- use_module(bsyntaxtree).
47
48		:- use_module(error_manager).
49
50		:- use_module(bmachine, [b_is_constant/1, constant_variable_marked_as_expand/1]).
51
52		:- type variable_id +--> (lambda_res(integer) ; atomic).
53		:- type binding +--> bind(variable_id,any).
54		:- type store +--> list(binding).
55
56		:- use_module(tools).
57		:- use_module(module_information).
58		:- module_info(group,interpreter).
59		:- module_info(description,'This module takes care of storing B values in an environment and normalising values.').
60
61		/* --------------------------------------------------------- */
62
63		/* store and lookup of values */
64
65
66
67		variable_is_defined(Var,Store) :- safe_member(bind(Var,_),Store,variable_is_defined).
68
69		store_value(Var,Value,Old,New) :- store_value2(Old,Var,Value,New).
70		store_value2([],Var,Value,[bind(Var,Value)]).
71		store_value2([bind(V,VV)|T],Var,Value,[bind(V,NValue)|UT]) :-
72		( Var=V ->
73		NValue=Value, UT=T
74		;
75		NValue=VV, store_value2(T,Var,Value,UT)).
76
77
78		store_value_for_existing_id(L,ID,V,L2) :- var(ID),!,
79		add_internal_error('VarID is var !!',store_value_for_existing_id(ID,V,L,L2)),fail.
80		store_value_for_existing_id(L,ID,V,L2) :- store_value_for_existing_id_aux(L,ID,V,L2).
81		store_value_for_existing_id_aux([],Var,Value,[bind(Var,Value)]) :-
82		add_error(store_value_for_existing_id,'Variable does not exist in store: ',Var).
83		store_value_for_existing_id_aux([bind(V,VV)|T],Var,Value,[bind(V,VV2)|UT]) :-
84		%we could use: arg(1,BIND,V), arg(2,BIND,VV),
85		(Var=V -> VV2=Value, UT=T
86		; VV2=VV,store_value_for_existing_id_aux(T,Var,Value,UT)).
87
88
89
90
91
92		/* store_intermediate_updates_wf(InState,Updates,OutStates,WF) */
93		/* rewrote it so that it copies state skeleton even if updates are not yet known */
94
95		:- assert_must_succeed((store:store_intermediate_updates_wf([bind(y,1),bind(x,2),bind(a,22)],[bind(x,33)],R,unit_test1,no_wf_available),R==[bind(y,1),bind(x,33),bind(a,22)])).
96		:- assert_must_succeed((store:store_intermediate_updates_wf([bind(Y,1),bind(X,2),bind(A,22)],[bind(x,33)],R,unit_test2,no_wf_available),X=x,A=a,Y=y,R==[bind(y,1),bind(x,33),bind(a,22)])).
97
98
99
100		store_intermediate_updates_wf(InStore,Update,OutStore,PP,WF) :- Update==[], !,
101		copy_store(InStore,OutStore,PP,WF).
102		store_intermediate_updates_wf(InStore,Update,OutStore,PP,WF) :-
103		store_intermediate_updates2(InStore,Update,OutStore,ctxt(PP,InStore,Update),WF).
104
105		:- block store_intermediate_updates2(-,?,?,?,?), store_intermediate_updates2(?,-,?,?,?).
106		store_intermediate_updates2([],Updates,[],PP,_WF) :-
107		store_intermediate_updates3(Updates,PP).
108		store_intermediate_updates2([bind(Var,OldVal)|InT],Updates,[bind(Var,NewVal)|OutT],PP,WF) :-
109		%we could do: arg(1,BIND,Var), arg(2,BIND,OldVal),
110		% TO DO: maybe it would be better to copy Update variables as they come in rather than forcing the order as in the store
111		search_and_delete_value(Var,OldVal,NewVal,Updates,NUpdates),
112		(NUpdates == []
113		-> copy_store(InT,OutT,PP,WF)
114		; store_intermediate_updates2(InT,NUpdates,OutT,PP,WF)
115		).
116
117		:- use_module(kernel_objects,[equal_object_wf/4]).
118		copy_store(In,Out,_,_) :- var(Out),!, Out=In.
119		copy_store(In,Out,PP,_) :- var(In),!, add_warning(store,'In store skeleton not set up:',In,PP), Out=In.
120		copy_store([],[],_PP,_) :- !.
121		copy_store([bind(Var1,InVal)|T1],[bind(Var2,OutVal)|T2],PP,WF) :- !,
122		(Var1=Var2
123		-> equal_object_wf(InVal,OutVal,copy_store,WF)
124		% usually InVal==OutVal, but in test 1043 became false after WF0 was no longer grounded inside SELECT/PRE
125		; add_error(copy_store,'Variable mismatch:',Var1:Var2,PP), fail),
126		copy_store(T1,T2,PP,WF).
127		copy_store(S1,S2,PP,_) :-
128		check_valid_store(S1,PP), check_valid_store(S2,PP),
129		add_error(copy_store,'Illegal stores:',S1:S2,PP),fail.
130
131		:- use_module(library(ordsets),[ord_intersection/3]).
132		:- block store_intermediate_updates3(-,?).
133		store_intermediate_updates3(Updates,PP) :-
134		( Updates = [] -> true
135		%; Updates = [bind(abort__flag__info,_)] -> true
136		; PP = ctxt(SpanInfo,InStore,FullUpdate),
137		% TO DO: determine if illegal assignments, which do not occur in InStore
138		get_ids_from_store(InStore,_,LegalIds),
139		get_ids_from_store(FullUpdate,WrIDs,_WrittenIds),
140		get_ids_from_store(Updates,_,IllegalIds),
141		ord_intersection(IllegalIds,LegalIds,DoubleIds),
142		(DoubleIds \= [] % at least some of the assignments are legal, hence must be double
143		-> add_error(store_intermediate_updates,'Double assignments:',
144		DoubleIds:(illegal_updates(Updates),written_ids(WrIDs)),SpanInfo)
145		% for: get_preference(try_operation_reuse,true/full) we now add term(undefined) for all variables written but not read
146		; add_error(store_intermediate_updates,'Illegal assignments:',
147		IllegalIds:(illegal_updates(Updates),legal_ids(LegalIds),written_ids(WrIDs)),SpanInfo)
148		)
149		).
150
151		get_ids_from_store(Store,Ids,SIds) :- findall(Id,member(bind(Id,_),Store),Ids), sort(Ids,SIds).
152
153		:- assert_pre(store:store_updates_and_normalise(A,B,_C),(type_check(A,store),type_check(B,store))).
154		:- assert_post(store:store_updates_and_normalise(_A,_B,C),(type_check(C,store))).
155
156		% TO DO: optimize; probably better to traverse InState once, rather than for each update binding
157		%:- block store_updates_and_normalise(-,?,?). % block normally not necessary
158		store_updates_and_normalise(Updates,InState,OutState) :- var(Updates), !,
159		add_internal_error('Variable update binding list:',store_updates_and_normalise(Updates,InState,OutState)),
160		when(ground(Updates), store_updates_and_normalise(Updates,InState,OutState)).
161		store_updates_and_normalise(Updates,InState,OutState) :- %print(store_updates_and_normalise),nl,
162		preferences:get_computed_preference(convert_closures_into_explicit_form_for_store,EXPAND),
163		sort(Updates,SUpdates), % only necessary for checking for multiple variables; we could remove this call
164		store_updates_and_normalise1(SUpdates,EXPAND,'$$NONE$$',InState,OutState).
165
166
167
168
169		store_updates_and_normalise1([],_EXPAND,_Last,InState,InState).
170		store_updates_and_normalise1([bind(Var,NewVal)|RestUpdates],EXPAND,LastVar,InState,OutState) :-
171		%NormalisedNewVal=NewVal, % TO DO: do not normalise for operation_cache here
172		normalise_value_for_var(Var,EXPAND,NewVal,NormalisedNewVal),
173		(Var==LastVar % test is in principle no longer necessary
174		-> add_error(store_updates_and_normalise,'Variable has been assigned twice in parallel: ',Var:NewVal)
175		; var(Var)
176		-> add_internal_error('Prolog variable for Var: ',store_updates_and_normalise1([bind(Var,NewVal)|RestUpdates]))
177		; true),
178		store_updates_and_normalise2(Var,EXPAND,NormalisedNewVal,RestUpdates,InState,OutState).
179
180		% no longer necessary; bmachine checks this: (b_is_constant(Var) -> add_error(store_updates_and_normalise,'Assigned value to constant: ',Var) ; true)
181
182		%:- block store_updates_and_normalise2(-,?,?,?,?).
183		store_updates_and_normalise2(Var,EXPAND,NewVal,RestUpdates,[H|T],OutState) :- !,
184		(H=bind(Var,_)
185		-> OutState = [bind(Var,NewVal)|TOut],
186		store_updates_and_normalise1(RestUpdates,EXPAND,Var,T,TOut)
187		; OutState = [H|TOut],
188		store_updates_and_normalise2(Var,EXPAND,NewVal,RestUpdates,T,TOut)).
189		store_updates_and_normalise2(Var,EXPAND,NewVal,RestUpdates,InState,[bind(Var,NewVal)|TOut]) :-
190		add_error(store,'Variable not found in store:',Var),
191		store_updates_and_normalise1(RestUpdates,EXPAND,Var,InState,TOut).
192
193
194
195
196		/* use to merge updates, e.g. for sequential composition LHS ; RHS */
197		:- assert_pre(store:merge_updates(_A,_B,_C),true). % (type_check(_A,store),type_check(_B,store))).
198		:- assert_post(store:merge_updates(_A,_B,_C),true). %(type_check(_C,store))).
199
200		:- assert_must_succeed((store:merge_updates([bind(x,1)],[bind(x,2)],R),R==[bind(x,2)])).
201		:- assert_must_succeed((store:merge_updates([bind(x,1)],[bind(X,2),bind(y,3)],R),X=x,R==[bind(x,2),bind(y,3)])).
202		:- assert_must_succeed((store:merge_updates([bind(x,1)],[bind(X,2),bind(y,3)],R),X=z,R==[bind(z,2),bind(y,3),bind(x,1)])).
203		:- assert_must_succeed((store:merge_updates([bind(y,1),bind(x,1)],[bind(x,2)],R),R==[bind(x,2),bind(y,1)])).
204
205		:- block merge_updates(-,?,?).
206		merge_updates([],RHSUpdates,RHSUpdates).
207		merge_updates([Bind|LHT],RHSUpdates,Rest) :-
208		merge_updates2( Bind,LHT,RHSUpdates,Rest).
209		:- block merge_updates2(?,?,-,?).
210		merge_updates2(bind(Var,NewVal),LHT,RHSUpdates,Rest) :-
211		merge_remove(RHSUpdates,Var,NewVal,RHSUpdates2),
212		merge_updates(LHT,RHSUpdates2,Rest).
213
214		:- block merge_remove(-,?,?,?).
215		merge_remove([],Var,NewVal,[bind(Var,NewVal)]).
216		merge_remove([bind(Var2,Val2)|T2],Var1,Val1,[bind(Var2,Val2)|NewT2]) :-
217		merge_remove_aux(Var2,T2,Var1,Val1,NewT2).
218
219		:- block merge_remove_aux(-,?,?,?,?).
220		merge_remove_aux(Var2,T2,Var1,Val1,NewT2) :-
221		(Var1=Var2
222		-> NewT2=T2 /* binding in second updates overrides first update */
223		; merge_remove(T2,Var1,Val1,NewT2)
224		).
225		/* ----------------------- */
226
227		:- block save_updates_in_existing_store(-,?).
228		save_updates_in_existing_store([],_Store).
229		save_updates_in_existing_store([bind(Var,Value)|Urest],Store) :-
230		save_updates_in_existing_store2(Var,Value,Store),
231		save_updates_in_existing_store(Urest,Store).
232		:- block save_updates_in_existing_store2(-,?,?).
233		save_updates_in_existing_store2(Var,Value,Store) :-
234		lookup_value_for_existing_id(Var,Store,Value).
235
236
237		:- assert_must_succeed(store:l_normalise_values([int(1)],[int(1)])).
238
239		l_normalise_values([],[]).
240		l_normalise_values([H|T],[NH|NT]) :- normalise_value(H,NH), l_normalise_values(T,NT).
241
242		:- block l_expand_and_normalise_values(-,?).
243		l_expand_and_normalise_values([],[]).
244		l_expand_and_normalise_values([H|T],[NH|NT]) :-
245		normalise_value_for_var('$unkown',true,H,NH),
246		l_expand_and_normalise_values(T,NT).
247		:- block l_expand_and_normalise_values(-,?,?).
248		l_expand_and_normalise_values([],[],_).
249		l_expand_and_normalise_values([H|T],[NH|NT],[VarName|VT]) :-
250		%% print(normalising(VarName)),nl, %%
251		normalise_value_for_var(VarName,true,H,NH),
252		l_expand_and_normalise_values(T,NT,VT).
253
254
255
256		:- assert_must_succeed(store:normalise_value(int(1),int(1))).
257		:- assert_must_succeed((store:normalise_value([int(1)],R), R==avl_set(node(int(1),true,0,empty,empty)))).
258		:- assert_must_succeed((store:normalise_value([int(1),int(2)],R1),
259		store:normalise_value([int(2),int(1)],R2),R1==R2)).
260		%:- assert_must_succeed((store:normalise_value(X,[int(1),int(2)]),X=[int(2),int(1)])).
261		:- assert_must_succeed((store:normalise_value(X,_R),X=[Y,Z],
262		Y=[int(2),int(1)],Z=[int(1)])).
263		:- assert_must_succeed(store:normalise_value(_X,[int(1),int(3)])).
264		:- assert_must_succeed((store:normalise_value(X,[int(3),int(1)]),
265		kernel_objects:equal_object(X,[int(1),int(3)]))).
266		:- assert_must_fail(store:normalise_value(int(2),int(1))).
267
268
269		normalise_value_for_var(Var,Val,NormVal) :-
270		preferences:get_computed_preference(convert_closures_into_explicit_form_for_store,EXPAND),
271		normalise_value_for_var(Var,EXPAND,Val,NormVal).
272
273		% EXPAND: can be false, limit(Limit), true, force
274		:- block normalise_value_for_var(?,?,-,-).
275		normalise_value_for_var(Var,EXPAND,Val,NormVal) :-
276		% print(check_var(Var)),nl, b_interpreter:check_value(Val,Var), print(ok(Var)),nl,
277		expand_closure_value_for_normalisation(Val,EXPAND,Var,ENewVal), % also normalises values inside closure if not expanded
278		normalise_value(ENewVal,NormVal). % , tools_printing:print_term_summary(normalised(ENewVal,NormVal)).
279
280		:- block normalise_value(-,-).
281		normalise_value(V,Res) :-
282		(nonvar(V),var(Res) -> normalise2(V,ResR),Res=ResR ; normalise3(V,Res)).
283		% (nonvar(V),var(Res) -> normalise2(V,Res) ; normalise3(V,Res)).
284
285
286
287		:- use_module(b_global_sets,[b_integer_or_real_or_string_set/1,all_elements_of_type/2]).
288		:- use_module(kernel_freetypes,[is_enumerated_set_freetype/1, expand_freetype/3]).
289		:- use_module(library(avl)).
290
291		%:- use_module(debug,[time/1]).
292
293		% a normalise which does not need to call equal_object on the result argument:
294		normalise2([H|T],Res) :- !,
295		normalise_list([H|T],Res).
296		normalise2((A,B),(NA,NB)) :- !, normalise_value(A,NA), normalise_value(B,NB).
297		normalise2(global_set(GS),N) :- !,
298	?	(b_integer_or_real_or_string_set(GS)
299		-> N = global_set(GS) /* can be very large or infinite, so don't expand */
300		; all_elements_of_type(GS,Res),
301		normalise2(Res,N)).
302		normalise2(freetype(ID),N) :- is_enumerated_set_freetype(ID), !, % triggers in test 2439
303		% TODO: also treat freetypes like setX = el1, el23(BOOL)
304		expand_freetype(ID,List,no_wf_available),
305		normalise_value(List,N).
306		normalise2(avl_set(A),R) :- !,
307		(%empty_avl(A)
308		A=empty
309		-> R=[] ;
310		%A = node(_,_,_,empty,_) -> R = avl_set(A) ; % avoid normalising certain one and two element sets; does not seem to bring any improvement
311		avl_to_list(A,L), ord_list_to_avl(L,B), R=avl_set(B)).
312		normalise2(string(S),R) :- !, R=string(S).
313		normalise2(int(S),R) :- !, R=int(S).
314		normalise2(fd(N,T),R) :- !, R=fd(N,T).
315		normalise2(rec(Fields),R) :- !, R=rec(NFields), normalise_fields(Fields,NFields).
316		normalise2(V,V).
317
318		:- block normalise_fields(-,-).
319		normalise_fields([],[]).
320		normalise_fields([field(Name,Val)|T], [field(Name,NVal)|NT]) :- normalise_value(Val,NVal),
321		normalise_fields(T,NT).
322
323		/* version to be called if for some reason second argument already instantiated;
324		e.g. when operation arguments and results are already instantiated */
325		%%normalise3(X,R) :- var(R),var(X),!,R=X. /* just in case the when is unfrozen by hypercall */
326		:- use_module(kernel_objects,[equal_object/3]).
327		%normalise3(R,[H|T]) :- !,kernel_objects:equal_object(R,[H|T]).
328		/* don't insist on normalising if a set is already partially given*/
329		normalise3((A,B),(NA,NB)) :- !, normalise_value(A,NA), normalise_value(B,NB).
330		normalise3(V,Res) :- equal_object(V,Res,normalise3).
331
332
333		:- use_module(custom_explicit_sets,[construct_avl_from_lists/2]).
334		:- use_module(closures,[is_symbolic_closure/1]).
335		:- use_module(kernel_tools,[ground_value_check/2]).
336		normalise_list(List,Res) :-
337		ground_value_check(List,ListGround), % this is slightly slower than ground() for long lists not containing avl_set values
338		normalise_list_aux(ListGround,List,Res).
339		:- block normalise_list_aux(-,?,?).
340		normalise_list_aux(_,[H|T],Res) :- % used to check T==[]; for test 2420 T ist not [] and we get a time-out
341		cannot_be_normalised_in_avl(H),!,
342		% do not expand this; would lead to enumeration warning; cf test 2157,
343		sort([H|T],Sorted),
344		kernel_objects:equal_object(Res,Sorted,normalise_list).
345		normalise_list_aux(_,List,Res) :-
346		% catch enumeration warnings in case infinite set is later in list
347		on_enumeration_warning(
348		construct_avl_from_lists(List,Avl),
349		Avl=List),
350		kernel_objects:equal_object(Res,Avl,normalise_list).
351
352		% check for some values that cannot be normalised within a list
353		cannot_be_normalised_in_avl((A,B)) :- !,
354		(cannot_be_normalised_in_avl(A) -> true ; cannot_be_normalised_in_avl(B) -> true).
355		cannot_be_normalised_in_avl([H|_]) :- cannot_be_normalised_in_avl(H).
356		cannot_be_normalised_in_avl(C) :- is_symbolic_closure(C).
357		cannot_be_normalised_in_avl(rec(Fields)) :- !, member(field(_,A),Fields), cannot_be_normalised_in_avl(A).
358		%cannot_be_normalised_in_avl(C) :- is_infinite_explicit_set(C). % do we need this; we mark them as symbolic before?!
359
360
361
362		expand_closure_value_for_normalisation(Var,_,_,R) :- var(Var),!,R=Var.
363		expand_closure_value_for_normalisation(closure(P,T,B),EXPAND,VarName,ExpandedValue) :- !, %print(expand_closure_value_for_normalisation(P,T,B)),nl,
364		expand_closure_value2(P,T,B,EXPAND,VarName,ExpandedValue).
365		%expand_closure_value_for_normalisation(closure_x(P,T,B,Exp),EXPAND,VarName,ExpandedValue) :- !,
366		% (ground(Exp) -> ExpandedValue=Exp ; expand_closure_value_for_normalisation(closure(P,T,B),EXPAND,VarName,ExpandedValue)).
367		expand_closure_value_for_normalisation(Val,_Expand,_VarName,Val).
368
369		:- use_module(custom_explicit_sets,[dont_expand_this_explicit_set/1,dont_expand_this_explicit_set/2,
370		is_infinite_explicit_set/1, is_infinite_or_very_large_explicit_set/1]).
371		:- use_module(clpfd_interface,[catch_clpfd_overflow_call2/2]).
372		:- use_module(tools_timeout, [time_out_with_factor_call/4]).
373
374		:- block expand_closure_value2(-,?,?,?,?,?), expand_closure_value2(?,-,?,?,?,?), expand_closure_value2(?,?,-,?,?,?).
375		expand_closure_value2(P,T,B,EXPAND,VarName,ExpandedValue) :- !,
376		% print(expand_closure_value2(VarName,EXPAND,P)),debug:nl_time,
377		(dont_expand_for_norm(EXPAND,closure(P,T,B),VarName,B)
378		-> construct_normalised_closure(P,T,B,ExpandedValue) %, print(not_expanding(closure(P))),nl
379		; % format('Expanding closure value of ~w for normalisation (expand:~w)~n',[VarName,EXPAND]),
380		% translate:print_bvalue(closure(P,T,B)),nl,
381		(EXPAND=force,
382		is_symbolic_closure(closure(P,T,B)) % Note: if EXPAND /= force we cannot have symbolic closure
383		-> Factor = 0.1 % more likely that expansion is not possible, user has annotated the closure as symbolic
384		; Factor = 0.3
385		),
386		(EXPAND=force -> Options = []
387		; Options = [max_time_out(120000)]), % Note: TIME_OUT could be very high and 0.3 of it also very high)
388		catch_clpfd_overflow_call2(
389		time_out_with_factor_call(
390		call_with_enumeration_warning( /* ensure we generate enumeration_warning exceptions */
391		store:expand_closure_value3(P,T,B,VarName,ExpandedValue)
392		),
393		Factor, Options,
394		store:time_out_expand_backup(VarName,P,T,B,EXPAND,ExpandedValue))
395		, (format('% CLP(FD) overflow during closure expansion: ~w~n',[VarName]),
396		construct_normalised_closure(P,T,B,ExpandedValue)))
397		%, tools_printing:print_term_summary(expanded(VarName,ExpandedValue)),debug:nl_time
398		).
399
400		:- use_module(kernel_waitflags, [init_wait_flags_with_call_stack/2,ground_wait_flags/1]).
401		expand_closure_value3(P,T,B,VarName,ExpandedValue) :-
402		init_wait_flags_with_call_stack(WF,[prob_command_context(expanding_value_for_normalisation(VarName),unknown)]),
403		custom_explicit_sets:expand_closure_to_avl_or_list(P,T,B,ExpandedValue,no_check,WF),
404		ground_wait_flags(WF).
405
406		:- use_module(performance_messages,[perfmessage/4]).
407		:- use_module(closures,[is_recursive_closure/1]).
408		dont_expand_for_norm(false,_,_,_) :- !.
409		dont_expand_for_norm(limit(Limit),C,_,_) :- !,
410		(dont_normalise_this_explicit_set(C) ;
411		dont_expand_this_explicit_set(C,Limit)).
412		dont_expand_for_norm(_,C,VarName,Span) :-
413		constant_variable_marked_as_expand(VarName),!, % we have a user annotation, e.g., /*@desc expand */
414		% see also b_add_constant_definition for constants in b_interpreter
415		(is_recursive_closure(C)
416		-> add_warning(store,'Cannot expand recursive constant or variable: ',VarName,Span)
417		; is_infinite_explicit_set(C)
418		-> add_warning(store,'Cannot expand infinite constant or variable: ',VarName,Span)
419		).
420		dont_expand_for_norm(true,C,VarName,Span) :-
421	?	(dont_normalise_this_explicit_set(C) -> true
422		; dont_expand_this_explicit_set(C) % detects e.g. symbolic closures or large intervals
423		-> perfmessage(symbolic_set,'Not expanding symbolic value, use FORCE or /*@desc expand */ pragma to override this for: ',VarName,Span) % TODO: maybe not show message for infinite values
424		).
425		dont_expand_for_norm(force,C,_,_) :-
426		(is_recursive_closure(C) -> true ; is_infinite_or_very_large_explicit_set(C)).
427
428		:- use_module(memoization,[is_memoization_closure/4]).
429		% we usually do not want to expand memoized closures when storing in the state !
430	?	dont_normalise_this_explicit_set(closure(P,T,B)) :- is_memoization_closure(P,T,B,_).
431
432		/*
433		:- use_module(custom_explicit_sets,[dont_expand_this_explicit_set/1, is_interval_closure/5]).
434		% maybe systematically expand small intervals and global_set's for normalization purposes ??
435		% (alternatively, we could re-convert certain avl-sets to symbolic form here)
436		dont_expand_closure_value(_,_,_) :-
437		preferences:get_computed_preference(convert_closures_into_explicit_form_for_store,false),!.
438		%dont_expand_closure_value(P,T,B) :-
439		% is_interval_closure(P,T,B,Low,Up), number(Low), number(Up),!,
440		% % interval closures are quite efficient for certain manipulations
441		% Size is Up+1-Low, Size>100. % another magic constant ; which value to choose ??
442		%dont_expand_closure_value(_,_,_) :-
443		% preferences:get_preference(convert_comprehension_sets_into_closures,false),!.
444		% % in the case above: we have already decided not to expand the closure earlier, dont repeat check !? TO DO: check that this is indeed ok; that no closures are constructed otherwise; maybe we should just check for small interval closures ?
445		dont_expand_closure_value(P,T,B) :- dont_expand_this_explicit_set(closure(P,T,B)).
446		*/
447
448		time_out_expand_backup(VarName,P,T,B,EXPAND,ExpandedValue) :-
449		(EXPAND=force
450		-> add_message(expand_closure_value,'Time-out while forcing expansion of symbolic value of: ',VarName,B)
451		; add_message(expand_closure_value,'Time-out while trying to expand symbolic value of: ',VarName,B)
452		),
453		construct_normalised_closure(P,T,B,ExpandedValue).
454
455		construct_normalised_closure(P,T,B1,closure(P,T,NB)) :-
456		%print(normalising(P)),nl,
457		%b_compile(B1,P,[],[],B2,no_wf_available), % probably much more expensive than simple code with can_be_computed below
458		normalise_closure_body(B1,NB).
459		% print(norm),nl,print(B),nl,print(NB),nl,nl.
460
461		% normalise values that are compiled inside closures
462		normalise_closure_body(b(OP,T,I),b(NOP,T,FI)) :-
463		(var(I) -> print(b(OP,T,I)),nl , when(nonvar(OP),(print(b(OP,T,I)),nl)) ; true),
464		filter_info(OP,I,FI),
465		ncb(OP,OP2),
466		(can_be_computed(OP2) % when compiling not all information was available for computation, now it is
467		-> b_interpreter:b_compute_expression_nowf(b(OP,T,I),[],[],Val,'normalising closure body',0),
468		%print(comp(Val)),nl,
469		ncb(value(Val),NOP) % TO DO: better apply the can_be_computed check after ncb, if performance ok
470		; NOP=OP2).
471
472		% should we throw away all infos for certain operators, e.g., for truth (cartesian product closures) or for certain values and member closures?
473		filter_info(truth,_,Res) :- !, % we have a maximal set
474		Res=[]. % we could check preference(provide_trace_information,false)
475		filter_info(falsity,_,Res) :- !, Res=[].
476		filter_info(_,V,R) :- filter_info2(V,R).
477
478		filter_info2(V,R) :- var(V),!,R=V.
479		filter_info2([],[]).
480		filter_info2([H|T],Res) :-
481		(important_info(H) -> Res=[H|TR] ; Res=TR), filter_info2(T,TR).
482
483		important_info(contains_wd_condition).
484		important_info(prob_annotation(_)).
485		important_info(used_ids(_)).
486		important_info(reads(_)). % operation_call_in_expr, modifies(.), non_det_modifies(.) only appear in subst
487		important_info(was(_)).
488		important_info(nodeid(_)).
489		important_info(allow_to_lift_exists).
490
491		:- use_module(kernel_mappings).
492		% ncb stands for normalise closure body
493		ncb(V,R) :- var(V),!, R=V.
494		ncb(bool_set,R) :- !, R=bool_set.
495		ncb(truth,R) :- !, R=truth.
496		ncb(event_b_identity,R) :- !, R=event_b_identity.
497		ncb(falsity,R) :- !, R=falsity.
498		ncb(max_int,R) :- !, R=max_int.
499		ncb(min_int,R) :- !, R=min_int.
500		ncb(value(V),value(NV)) :- !,normalise_value_for_var('$closure_body',V,NV).
501		ncb(integer(X),integer(NX)) :- !, X=NX.
502		ncb(identifier(X),identifier(NX)) :- !, X=NX.
503		ncb(float_set,R) :- !, R=float_set.
504		ncb(real(X),real(NX)) :- !, X=NX.
505		ncb(real_set,R) :- !, R=real_set.
506		ncb(string(X),string(NX)) :- !, X=NX.
507		ncb(string_set,R) :- !, R=string_set.
508		ncb(integer_set(X),integer_set(NX)) :- !, X=NX.
509		ncb(set_extension(X),set_extension(NX)) :- !, X=NX.
510		ncb(partition(S,L),partition(NS,NL)) :- !, normalise_closure_body(S,NS),
511		maplist(normalise_closure_body,L,NL).
512		ncb(general_sum(Ids,Condition,Expression),general_sum(Ids,NC,NE)) :- !,
513		normalise_closure_body(Condition,NC),normalise_closure_body(Expression,NE).
514		ncb(general_product(Ids,Condition,Expression),general_product(Ids,NC,NE)) :- !,
515		normalise_closure_body(Condition,NC),normalise_closure_body(Expression,NE).
516		ncb(sequence_extension(X),sequence_extension(NX)) :- !, X=NX.
517		ncb(external_function_call(F,L),external_function_call(F,LL)) :- !, L=LL.
518		ncb(external_pred_call(F,L),external_pred_call(F,LL)) :- !, L=LL.
519		ncb(equal(A,B),equal(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
520		ncb(couple(A,B),couple(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
521		ncb(interval(A,B),interval(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
522		ncb(function(A,B),function(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
523		ncb(operation_call_in_expr(A,B),operation_call_in_expr(NA,B)) :- !,
524		normalise_closure_body(A,NA).
525		ncb(relations(A,B),relations(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
526		ncb(member(A,B),member(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
527		ncb(not_member(A,B),not_member(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
528		ncb(negation(B),negation(NB)) :- !, normalise_closure_body(B,NB).
529		ncb(conjunct(A,B),conjunct(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
530		ncb(disjunct(A,B),disjunct(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
531		ncb(equivalence(A,B),equivalence(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
532		ncb(if_then_else(A,B,C),if_then_else(NA,NB,NC)) :- !,
533		normalise_closure_body(A,NA), normalise_closure_body(B,NB), normalise_closure_body(C,NC).
534		ncb(implication(A,B),implication(NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
535		ncb(comprehension_set(V,B),comprehension_set(V,NB)) :- !, normalise_closure_body(B,NB).
536		ncb(convert_bool(B),convert_bool(NB)) :- !, normalise_closure_body(B,NB).
537		ncb(convert_real(B),convert_real(NB)) :- !, normalise_closure_body(B,NB).
538		ncb(convert_int_floor(B),convert_int_floor(NB)) :- !, normalise_closure_body(B,NB).
539		ncb(convert_int_ceiling(B),convert_int_ceiling(NB)) :- !, normalise_closure_body(B,NB).
540		ncb(exists(IDs,B),exists(IDs,NB)) :- !, normalise_closure_body(B,NB).
541		ncb(forall(IDs,A,B),forall(IDs,NA,NB)) :- !, normalise_closure_body(A,NA), normalise_closure_body(B,NB).
542		ncb(assertion_expression(Cond,ErrMsg,Expr),assertion_expression(NA,ErrMsg,NB)) :- !,
543		normalise_closure_body(Cond,NA), normalise_closure_body(Expr,NB).
544		ncb(freetype_case(FT,IsCase,Expr),freetype_case(FT,IsCase,NB)) :- !,
545		normalise_closure_body(Expr,NB).
546		ncb(freetype_constructor(Id,Case,Expr),freetype_constructor(Id,Case,NB)) :- !,
547		normalise_closure_body(Expr,NB).
548		ncb(freetype_destructor(Id,Case,Expr),freetype_destructor(Id,Case,NB)) :- !,
549		normalise_closure_body(Expr,NB).
550		ncb(record_field(R,Name),record_field(NR,Name)) :- !,
551		normalise_closure_body(R,NR).
552		ncb(rec(Fields),rec(NFields)) :- !,
553		ncb_fields(Fields,NFields).
554		ncb(recursive_let(ID,R),recursive_let(ID,NR)) :- !,
555		normalise_closure_body(R,NR).
556		ncb(kodkod(Id,Ids),R) :- !, R=kodkod(Id,Ids).
557		ncb(lazy_let_expr(Id,E,Expr),lazy_let_expr(Id,NE,NExpr)) :- !, normalise_closure_body(E,NE),
558		normalise_closure_body(Expr,NExpr).
559		ncb(lazy_let_pred(Id,E,Pred),lazy_let_pred(Id,NE,NPred)) :- !, normalise_closure_body(E,NE),
560		normalise_closure_body(Pred,NPred).
561		% lazy_let_subst should not occur in closure bodies
562		ncb(lazy_lookup_expr(X),lazy_lookup_expr(NX)) :- !, X=NX.
563		ncb(lazy_lookup_pred(X),lazy_lookup_pred(NX)) :- !, X=NX.
564		ncb(let_predicate(Ids,AssignmentExprs,Pred),let_predicate(Ids,AssignmentExprs,NPred)) :- !,
565		normalise_closure_body(Pred,NPred).
566		ncb(let_expression(Ids,AssignmentExprs,Expr),let_expression(Ids,AssignmentExprs,NExpr)) :- !,
567		normalise_closure_body(Expr,NExpr).
568		ncb(let_expression_global(Ids,AssignmentExprs,Expr),let_expression_global(Ids,AssignmentExprs,NExpr)) :- !,
569		normalise_closure_body(Expr,NExpr).
570		ncb(F,NF) :- functor(F,Op,1),
571		(unary_function(Op,_,_) ; unary_in_boolean_type(Op,_)), !,
572		arg(1,F,Arg1), functor(NF,Op,1), arg(1,NF,NormArg1),
573		normalise_closure_body(Arg1,NormArg1).
574		ncb(F,NF) :- functor(F,Op,2),
575		(binary_function(Op,_,_) ; kernel_mappings:binary_boolean_operator(Op,_,_) ; binary_in_boolean_type(Op,_)), !,
576		arg(1,F,Arg1),arg(2,F,Arg2), functor(NF,Op,2), arg(1,NF,NormArg1), arg(2,NF,NormArg2),
577		normalise_closure_body(Arg1,NormArg1),
578		normalise_closure_body(Arg2,NormArg2).
579		ncb(X,X) :- print(ncb(X)),nl.
580
581
582		can_be_computed(domain(X)) :- is_known_set_or_int_value(X).
583		can_be_computed(range(X)) :- is_known_set_or_int_value(X).
584		can_be_computed(plus(X,Y)) :- is_known_set_or_int_value(X),is_known_set_or_int_value(Y).
585		can_be_computed(minus(X,Y)) :- is_known_set_or_int_value(X),is_known_set_or_int_value(Y).
586		can_be_computed(times(X,Y)) :- is_known_set_or_int_value(X),is_known_set_or_int_value(Y).
587		% check for more possible partial evaluations; check for common code with b_compiler, CSE or other parts of ProB
588
589		is_known_set_or_int_value(b(value(V),_,_)) :- is_known_aux(V).
590		is_known_aux(X) :- var(X),!,fail.
591		is_known_aux([]).
592		is_known_aux(avl_set(_)).
593		is_known_aux(int(Nr)) :- number(Nr).
594
595		ncb_fields([],[]).
596		ncb_fields([field(Name,Expr)|T], [field(Name,NExpr)|NT]) :-
597		normalise_closure_body(Expr,NExpr),
598		ncb_fields(T,NT).
599
600		%ncb(set_extension([b(couple(b(add(b(identifier(idx),integer,[nodeid(pos(53,1,11,91,11,93))]),b(integer(1),integer,[nodeid(pos(54,1,11,95,11,95))])),integer,[nodeid(pos(52,1,11,91,11,95))]),b(identifier(bit),integer,[nodeid(pos(55,1,11,101,11,103))])),couple(integer,integer),[nodeid(pos(51,1,11,91,11,103))])]))
601
602		normalise_store(T,NT) :-
603		preferences:get_computed_preference(convert_closures_into_explicit_form_for_store,EXPAND),
604		normalise_store1(T,EXPAND,NT).
605		:- block normalise_store1(-,?,?).
606		normalise_store1([],_Expand,Res) :- !, Res=[].
607		normalise_store1([bind(Var,Val)|T],EXPAND,Res) :- !, Res = [bind(Var,NVal)|NT],
608		%print(normalise(Val)),nl,print(Var),nl,
609		normalise_value_for_var(Var,EXPAND,Val,NVal),
610		normalise_store1(T,EXPAND,NT).
611		normalise_store1(Store,E,Res) :-
612		add_internal_error('Illegal store: ',normalise_store1(Store,E,Res)),
613		Res=Store.
614
615		/* ----------------------- */
616
617		% a utility to also accept const_and_vars states
618		normalise_states([],[]).
619		normalise_states([I|Irest],[O|Orest]) :-
620		normalise_state(I,O),
621		normalise_states(Irest,Orest).
622		normalise_state(I,O) :-
623		extract_vars(I,VI,VO,O),
624		normalise_store(VI,VO).
625		extract_vars(const_and_vars(ConstID,IV),IV,OV,const_and_vars(ConstID,OV)) :- !.
626		extract_vars(IV,IV,OV,OV).
627
628
629		/* ----------------------- */
630
631		:- assert_pre(store:lookup_value_for_existing_id(Id,State,_Val),
632		(type_check(Id,variable_id),list_skeleton(State),type_check(State,store))).
633		:- assert_post(store:lookup_value_for_existing_id(_Id,_State,_Val), true).
634
635		lookup_value_for_existing_id(Id,State,Res) :-
636		(member_bind(Id,Val,State) % safe_member(bind(Id,Val),State,lookup_value_for_existing_id)
637		-> check_val(Val,Id,State),Res=Val
638		; add_internal_error('Call Failed: ',lookup_value_for_existing_id(Id,State,Res)),
639		Res=term(undefined)
640		).
641
642		:- assert_pre(store:lookup_value_for_existing_id(Id,LS,State,_Val),
643		(type_check(Id,variable_id),type_check(LS,store),type_check(State,store),list_skeleton(LS),list_skeleton(State))).
644		:- assert_post(store:lookup_value_for_existing_id(_Id,_LS,_State,_Val), true).
645
646		lookup_value_for_existing_id(Id,LocalState,State,Val) :-
647		(member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value_for_existing_id__4)
648		-> check_val(Val,Id,LocalState)
649		; lookup_value_for_existing_id(Id,State,Val)).
650
651		% pass WF for call_stack info:
652		lookup_value_for_existing_id_wf(Id,LocalState,State,Val,WF) :-
653		(member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value_for_existing_id__4)
654		-> check_val_with_span_wf(Val,Id,LocalState,unknown,WF)
655		; lookup_value_for_existing_id_wf(Id,State,Val,WF)).
656
657		lookup_value_for_existing_id_wf(Id,State,Val,WF) :-
658		(member_bind(Id,Val,State) %safe_member(bind(Id,Val),LocalState,lookup_value_for_existing_id__4)
659		-> check_val_with_span_wf(Val,Id,State,unknown,WF)
660		; add_state_error_wf(lookup_value_for_existing_id_wf,'Cannot find identifier: ',Id,unknown,WF),
661		fail
662		).
663
664		lookup_value(Id,State,Val) :-
665		(member_bind(Id,Val,State) %safe_member(bind(Id,Val),State,lookup_value)
666		-> check_val(Val,Id,State)
667		).
668
669		lookup_value(Id,LocalState,State,Val) :-
670		(member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value__4)
671		-> check_val(Val,Id,LocalState)
672		; member_bind(Id,Val,State) -> check_val(Val,Id,State)).
673
674		lookup_value_with_span_wf(Id,LocalState,State,Val,Span,WF) :-
675		(member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value__4)
676		-> check_val_with_span_wf(Val,Id,LocalState,Span,WF)
677		; member_bind(Id,Val,State) -> check_val_with_span_wf(Val,Id,State,Span,WF)).
678
679		lookup_value_without_check(Id,LocalState,State,Val) :- % does not check if value is undefined
680		(member_bind(Id,Val,LocalState) %safe_member(bind(Id,Val),LocalState,lookup_value__4)
681		-> true
682		; member_bind(Id,Val,State) -> true).
683
684		% a faster version of member(bind(Id,Val),List) with only one solution
685		member_bind(Id,Val,[H|T]) :-
686		arg(1,H,Id) -> arg(2,H,Val) ; member_bind(Id,Val,T).
687
688		get_id_value(Id,State,Val) :- safe_member(bind(Id,Val),State,get_id_value). /* can be backtracked over */
689
690		%safe_member(X,T) :- safe_member(X,T,safe_member).
691		safe_member(_,[],_) :- !,fail.
692		safe_member(X,[H|T],Loc) :- !, (X=H ; safe_member(X,T,Loc)).
693		safe_member(X,T,Loc) :- add_internal_error('Argument not a list: ',safe_member(X,T,Loc)),fail.
694
695		:- use_module(kernel_waitflags,[get_call_stack/2,add_state_error_wf/5]).
696		:- use_module(bmachine,[b_operation_reads_output_variables/3]).
697		check_val_with_span_wf(X,VarName,_State,Span,WF) :-
698		(X==term(undefined) ->
699		(get_preference(allow_operations_to_read_outputs,false),
700		call_stack_contains_operation_call(WF,OpName),
701		b_operation_reads_output_variables(OpName,ReadOutputs,_),
702		member(VarName,ReadOutputs)
703		-> ajoin(['Trying to read output variable of operation ', OpName,
704		' (set ALLOW_OUTPUT_READING to TRUE to allow this): '],Msg)
705		; Msg = 'Trying to read undefined variable: '
706		),
707		add_state_error_wf(reading_undefined_variable,Msg,VarName,Span,WF)
708		% do not fail; otherwise we will look elsewhere and generate another error message, see test 1660
709		; true).
710
711		call_stack_contains_operation_call(WF,Operation) :-
712		get_call_stack(WF,Stack),
713		member(operation_call(Operation,_Args,_Pos),Stack).
714
715		check_val(X,V,_State) :-
716		(X==term(undefined) ->
717		add_state_error_wf(reading_undefined_variable,'Trying to read undefined variable: ',V,unknown,no_wf_available)
718		% do not fail
719		; true).
720
721		:- assert_must_succeed(( store:lookup_and_delete_value(x,X,[bind(y,2),bind(x,3)],R,true,_WF,F),
722		X==3, R==[bind(y,2)],F==true )).
723		:- assert_must_succeed(( store:lookup_and_delete_value(x,X,[bind(y,2)|T],R,true,_WF,F),
724		T = [bind(x,3)],
725		X==3, R==[bind(y,2)],F==true )).
726
727		lookup_and_delete_value(Var,Value,T,UT,ReportError,WF,Finished) :-
728		lookup_and_delete_value1(T,Var,Value,UT,ReportError,WF,Finished).
729		:- use_module(kernel_waitflags,[add_abort_error_span/5]).
730		:- block lookup_and_delete_value1(-,?,?,?,?,?,?).
731		lookup_and_delete_value1([],Var,Value,[],ReportError,WF,Finished) :-
732		(ReportError=report_error(WF)
733		-> add_abort_error_span(missing_assignment_error,'Statement did not assign to variable: ',Var,unknown,WF)
734		/* lookup_and_delete is called only from get_results */
735		; true
736		), no_value_for_variable(Value,Var),
737		Finished=true.
738		lookup_and_delete_value1([bind(Var2,Value2)|T],Var,Value,Res,ReportError,WF,Finished) :-
739		lookup_and_delete_value2(Var2,Value2,T,Var,Value,Res,ReportError,WF,Finished).
740		:- block lookup_and_delete_value2(-,?,?,?,?,?,?,?,?).
741		lookup_and_delete_value2(Var2,Value2,T,Var,Value,Res,ReportError,WF,Finished) :-
742		(Var=Var2
743		-> Value=Value2, T=Res, Finished=true
744		; Res=[bind(Var2,Value2)|UT],
745		lookup_and_delete_value1(T,Var,Value,UT,ReportError,WF,Finished)
746		).
747
748		no_value_for_variable(term(no_value_for(Var)),Var).
749
750		:- assert_must_succeed(( store:search_and_delete_value(x,22,X,[bind(y,2),bind(x,3)],R),
751		X==3, R==[bind(y,2)] )).
752		:- assert_must_succeed(( store:search_and_delete_value(x,22,X,[bind(y,2)],R),
753		X==22, R==[bind(y,2)] )).
754		:- assert_must_succeed(( store:search_and_delete_value(x,22,X,[bind(y,2)|T],R),
755		T = [bind(x,3)],
756		X==3, R==[bind(y,2)] )).
757
758		:- block search_and_delete_value(-,?,?,?,?).
759		search_and_delete_value(Var,OldVal,Value,InStore,OutStore) :-
760		search_and_delete_value2(InStore,Var,OldVal,Value,OutStore).
761
762		:- block search_and_delete_value2(-,?,?,?,?).
763		search_and_delete_value2([],_Var,OldVal,Value,[]) :- eq_obj(Value,OldVal).
764		search_and_delete_value2([BIND|T],Var,OldVal,Value,Res) :- % BIND=bind(Var2,Value2)
765		arg(1,BIND,Var2), arg(2,BIND,Value2),
766		search_and_delete_value3(Var2,Value2,T,Var,OldVal,Value,Res).
767
768		:- block search_and_delete_value3(-,?,?,?,?,?,?).
769		search_and_delete_value3(Var2,Value2,T,Var,OldVal,Value,Res) :-
770		(Var=Var2
771		-> eq_obj(Value,Value2), T=Res
772		; Res=[bind(Var2,Value2)|UT],
773		search_and_delete_value2(T,Var,OldVal,Value,UT)
774		).
775
776		eq_obj(Val1,Val2) :- (var(Val1);var(Val2)),!,Val1=Val2.
777		eq_obj(Val1,Val2) :- equal_object(Val1,Val2,search_and_delete_value).
778
779		empty_state([]).
780		add_var_to_localstate(Var,Val,InState,[bind(Var,Val)|InState]).
781
782		:- assert_pre(store:set_up_localstate(Vars,Vals,In,_),
783		(type_check(Vars,list(variable_id)),type_check(Vals,vlist(any)),type_check(In,store))).
784		:- assert_post(store:set_up_localstate(_,_,_,Out), type_check(Out,store)).
785
786		set_up_localstate([],[],S,S) :- !.
787		set_up_localstate([Var|T],[Val|FT],InS,[bind(VarID,Val)|OutS]) :- !,
788		/* add Var,Val to Local state at the beginning to properly handle nested
789		blocks with same variable names */
790		(Var=b(identifier(Id),_,_) -> %print(typed_identifier_for_set_up_localstate(Var)),nl,
791		VarID = Id
792		; VarID = Var),
793		set_up_localstate(T,FT,InS,OutS).
794		set_up_localstate(Vars,Vals,In,Out) :-
795		add_internal_error('Illegal call: ',set_up_localstate(Vars,Vals,In,Out)), fail.
796
797		set_up_undefined_localstate([],S,S).
798		set_up_undefined_localstate([Var|T],InS,[bind(Id,term(undefined))|OutS]) :-
799		def_get_texpr_id(Var,Id),
800		/* add Var,Val to Local state at the beginning to properly handle nested
801		blocks with same variable names */
802		set_up_undefined_localstate(T,InS,OutS).
803
804		:- use_module(tools_lists,[delete_first/3]).
805		% sets up undefined values for variables, except for a list of predefined variables (all of which must be used)
806		set_up_undefined_localstate_with_predefined([],PredefinedValues,S,S) :-
807		(PredefinedValues=[] -> true
808		; add_internal_error('Unknown predefined values: ',set_up_undefined_localstate_with_predefined([],PredefinedValues,S,S))).
809		set_up_undefined_localstate_with_predefined([Var|T],PredefinedValues,InS,[bind(Id,Val)|OutS]) :-
810		def_get_texpr_id(Var,Id),
811		delete_first(InS,bind(Id,_),InS2), % in case of name clash: remove the old binding from the state
812		(select(bind(Id,Val),PredefinedValues,Rest)
813		-> set_up_undefined_localstate_with_predefined(T,Rest,InS2,OutS)
814		; Val=term(undefined),
815		set_up_undefined_localstate_with_predefined(T,PredefinedValues,InS2,OutS)).
816
817
818		:- assert_pre(store:delete_variables_from_state(Vars,In,_),
819		(type_check(Vars,list(variable_id)),type_check(In,store))).
820		:- assert_post(store:delete_variables_from_state(_,_,Out), type_check(Out,store)).
821
822		delete_variables_from_state([],S,R) :- !, R=S.
823		delete_variables_from_state([Var|T],InState,OutState) :- !,
824		delete_variable(InState, Var, S2),
825		delete_variables_from_state(T,S2,OutState).
826		delete_variables_from_state(Vs,I,O) :-
827		add_internal_error('Illegal call to:',delete_variables_from_state(Vs,I,O)),fail.
828
829		delete_variable([],_,[]).
830		delete_variable([bind(V,Val)|T],Var,Res) :-
831		(Var==V
832		-> Res = T
833		; Res = [bind(V,Val)|DT], delete_variable(T,Var,DT)
834		).
835		/* --------------------------------- */
836
837		% unused at the moment:
838		%:- assert_pre(store:copy_store_template(In,_),
839		% (type_check(In,store))).
840		%:- assert_post(store:copy_store_template(_,Out), type_check(Out,store)).
841		%copy_store_template([],[]).
842		%copy_store_template([bind(Var,_)|T],[bind(Var,_)|CT]) :- copy_store_template(T,CT).
843
844		:- use_module(library(ordsets)).
845		% copy_store_template copies a store and its values except some changing variables
846		% Two new stores are created: constants are not copied into the first new update state, but
847		% to the second new full state
848		copy_variable_store(InState,SortedChanges,Updates,NewFullState) :-
849		(SortedChanges=[] -> Updates = [],NewFullState=InState % Query Operation/Event ,print(no_upd),nl
850		; copy_variable_store2(InState,SortedChanges,Updates,NewFullState)).
851
852		copy_variable_store2([],_,[],[]).
853		copy_variable_store2([bind(Var,Old)|T],SortedChanges,Updates,NewFullState) :-
854		( b_is_constant(Var) ->
855		Updates = CT, NewFullState = [bind(Var,Old)|FT]
856		%; safe_member(Var,SortedChanges,copy_variable_store) ->
857		; ord_member(Var,SortedChanges) ->
858		%; ord_delete(SortedChanges,Var,SortedChanges2) -> % in principle better than ord_member; but seems slightly slower on examples/EventBPrologPackages/Advance_WP2/v6_Sep2014/ex_mch.eventb
859		Updates = [bind(Var,New)|CT], NewFullState = [bind(Var,New)|FT]
860		;
861		Updates = CT, NewFullState = [bind(Var,Old)|FT]
862		), copy_variable_store2(T,SortedChanges,CT,FT).
863
864		%ord_delete([H|T],El,Res) :- El @>= H,
865		% (H==El -> Res=T ; Res = [H|RR], ord_delete(T,El,RR)).
866
867
868		% -------------------------------
869
870		:- assert_must_succeed(store:check_valid_store([bind(x,int(1)), bind(y,int(2))],unit_test)).
871
872		:- block check_valid_store(-,?).
873		check_valid_store([],_PP).
874		check_valid_store([bind(Var,Value)|T],PP) :- member(bind(Var,Val2),T),
875		add_internal_error('Multiple occurences of variable: ',bind(Var,Value,Val2,PP)),
876		fail.
877		check_valid_store([_|T],PP) :- check_valid_store(T,PP).
878
879