1		% (c) 2009-2019 Lehrstuhl fuer Softwaretechnik und Programmiersprachen,
2		% Heinrich Heine Universitaet Duesseldorf
3		% This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html)
4
5		:- module(b_interpreter_components,[
6		reset_component_info/1,
7		b_trace_test_components/3, b_trace_test_components/4,
8		unsat_component/2, unsat_component_enumeration_warning/1,
9		unsat_or_unknown_component_exists/0,
10		unsat_component_abort_error/1,
11		unsat_conjunct_inside_component/4,
12		det_solution_for_constant/2,
13		b_tracetest_boolean_expression/5,
14		observe_state/3,
15
16		construct_optimized_exists/3, construct_optimized_exists/4
17		]).
18
19		:- use_module(b_interpreter,[b_test_boolean_expression/6]).
20		:- use_module(preferences).
21		:- use_module(kernel_waitflags).
22		:- use_module(tools).
23		:- use_module(translate).
24		:- use_module(error_manager).
25		:- use_module(library(lists)).
26		:- use_module(b_enumerate, [b_trace_tighter_enumerate_values/2]).
27
28		:- load_files(library(system), [when(compile_time), imports([environ/2])]).
29		:- if(\+ environ(disable_chr, true)).
30		:- use_module(chrsrc(chr_integer_inequality),[attach_chr_integer_inequality_to_wf_store/1]).
31		:- else.
32		attach_chr_integer_inequality_to_wf_store(_).
33		:- endif.
34
35		:- use_module(module_information,[module_info/2]).
36		:- module_info(group,interpreter).
37		:- module_info(description,'This module can be used to split a predicate into components and solving each component individually (with tracing feedback).').
38
39		/* -------------- */
40		/* dynamic bits */
41		/* -------------- */
42
43		:- dynamic skipped_unsat_conjunct/1, unsat_conjunct_inside_component/4.
44		reset_unsat_conjunct_inside_component_info :-
45		retractall(skipped_unsat_conjunct(_)),
46		retractall(unsat_conjunct_inside_component(_,_,_,_)).
47		reset_tracetest_for_component :- retractall(skipped_unsat_conjunct(_)). % to be called before trace checking a component
48
49		% individual conjuncts which are directly unsatisfiable
50		assert_skipped_failed_conjunct(ComponentNr,BE) :- assert_skipped_unsat_conjunct,
51		assert(unsat_conjunct_inside_component(ComponentNr,BE,false,'')),
52		(preferences:get_preference(provide_trace_information,false) -> true
53		; print(' *** INCONSISTENCY DETECTED, SKIPPING: '),
54		(debug_mode(on) -> print_bexpr_with_limit(BE,500) ; print_bexpr_with_limit(BE,150)),
55		nl,
56		print(' *** COMPONENT NUMBER: '), print(ComponentNr),nl).
57		assert_skipped_unknown_conjunct(ComponentNr,BE,Reason) :- assert_skipped_unknown_conjunct,
58		assert(unsat_conjunct_inside_component(ComponentNr,BE,unknown,Reason)),
59		(preferences:get_preference(provide_trace_information,false) -> true
60		; get_reason_msg(Reason,MSG),format(' *** Skipping predicate due to ~w:',[MSG]),
61		print_bexpr_with_limit(BE,150),nl,
62		format('~n *** Predicate is unknown~n *** COMPONENT NUMBER: ~w~n',[ComponentNr])
63		).
64		assert_skipped_unsat_conjunct :-
65		(skipped_unsat_conjunct(false) -> true
66		; retractall(skipped_unsat_conjunct(_)), assert(skipped_unsat_conjunct(false))).
67		assert_skipped_unknown_conjunct :-
68		(skipped_unsat_conjunct(_) -> true ; assert(skipped_unsat_conjunct(unknown))).
69
70		get_reason_msg(enumeration_warning,R) :- !, R='ENUMERATION WARNING'.
71		get_reason_msg('prob-ignore',R) :- !, R='prob-ignore pragma'.
72		get_reason_msg(M,M).
73
74
75		:- dynamic unsat_component/2, unsat_component_enumeration_warning/1, unsat_component_abort_error/1.
76		reset_unsat_component_info :-
77		retractall(unsat_component(_,_)),
78		retractall(unsat_component_enumeration_warning(_)),
79		retractall(unsat_component_abort_error(_)).
80
81		:- use_module(eventhandling,[register_event_listener/3]).
82		:- register_event_listener(clear_specification,reset_unsat_component_info,
83		'Reset b_interpreter_components unsat component info.').
84
85		store_unsat_component_nr(X,FalseOrUnknown) :- debug_println(19,store_unsat_component_nr(X,FalseOrUnknown)),
86		(unsat_component(X,false) -> true
87		; retractall(unsat_component(X,_)),assert(unsat_component(X,FalseOrUnknown))
88		),
89		(enumeration_warning_occured_in_error_scope,
90		\+ unsat_component_enumeration_warning(X)
91		-> assert(unsat_component_enumeration_warning(X)),
92		debug_println(19,enumeration_warning_in_component(X))
93		; true),
94		(abort_error_occured_in_error_scope,
95		\+ unsat_component_abort_error(X)
96		-> assert(unsat_component_abort_error(X)), print(abort(X)),nl,
97		debug_println(19,unsat_component_abort_error(X))
98		; true).
99	?	unsat_component_exists :- unsat_component(_,false),!.
100		unsat_or_unknown_component_exists :- unsat_component(_,_),!.
101
102		:- public nr_of_components/1.
103		:- dynamic nr_of_components/1.
104		:- dynamic allow_skipping_over_components/0.
105		reset_component_info(AllowSkip) :- retractall(allow_skipping_over_components),
106		(AllowSkip==true -> assert(allow_skipping_over_components) ; true),
107		reset_unsat_component_info,
108		reset_unsat_conjunct_inside_component_info.
109
110		% in Disprover mode we can stop straightaway; we are not interested in finding values for identifiers in other components; unless we have an enumeration warning !!
111		% TO DO: keep track of enumeration warnings per component
112
113		/* -------------- */
114
115
116		:- use_module(library(avl)).
117		% You can use the term one as ComponentNr if you don't know the number or it is not relevant
118		b_tracetest_boolean_expression(BE,LS,S,WF,ComponentNr) :-
119		empty_avl(Ai),
120		b_tracetest_boolean_expression1(BE,LS,S,WF,ComponentNr,Ai,_Ao).
121
122
123		b_tracetest_boolean_expression1(b(Expr,_,Infos),LS,S,WF,ComponentNr,Ai,Ao) :- !,
124		b_tracetest_boolean_expression2(Expr,Infos,LS,S,WF,ComponentNr,Ai,Ao).
125
126		:- use_module(bsyntaxtree,[info_has_ignore_pragma/1]).
127
128		b_tracetest_boolean_expression2(BE,Infos,_LS,_S,_WF,ComponentNr,Ai,Ao) :-
129		get_preference(use_ignore_pragmas,true),
130		info_has_ignore_pragma(Infos),!,
131		format('~n ==IGNORING==> (~w) ',[ComponentNr]),print_bexpr_with_limit(BE,250),nl,
132		assert_skipped_unknown_conjunct(ComponentNr,b(BE,pred,Infos),'prob-ignore'),
133		Ai=Ao.
134		b_tracetest_boolean_expression2(conjunct(LHS,RHS),_Info,LocalState,State,WF,ComponentNr,Ai,Ao) :-
135		% \+(Info = [try_smt|_]),
136		!,
137		%% print('check lhs of conjunct: '), translate:print_bexpr(LHS),nl,
138		b_tracetest_boolean_expression1(LHS,LocalState,State,WF,ComponentNr,Ai,Aii),
139		%% print('check rhs of conjunct: '), translate:print_bexpr(RHS),nl,
140		b_tracetest_boolean_expression1(RHS,LocalState,State,WF,ComponentNr,Aii,Ao).
141		b_tracetest_boolean_expression2(BE,Infos,LS,S,WF,ComponentNr,Ai,Ao) :-
142		(get_preference(provide_trace_information,true)
143		-> format('~n ====> (~w) ',[ComponentNr]),print_bexpr_with_limit(BE,250),nl
144		; true),
145		if(safe_b_test_boolean_expression(ComponentNr,b(BE,pred,Infos),LS,S,WF,Ai,Ao),true, %% b_det_test_boolean_expression2
146		(assert_skipped_failed_conjunct(ComponentNr,b(BE,pred,Infos)),
147		Ai=Ao)).
148
149		safe_b_test_boolean_expression(ComponentNr,BE,LS,S,WF,Ai,Ao) :-
150		catch_enumeration_warning_exceptions(
151		b_test_boolean_expression(BE,LS,S,WF,Ai,Ao), % this should not backtrack (without WF0 set); otherwise we may get problems with error blocks nesting
152		(assert_skipped_unknown_conjunct(ComponentNr,BE,enumeration_warning),Ai=Ao), true). % true: add exceptions as event errors
153
154		:- use_module(bsyntaxtree,[predicate_components_in_scope/3,
155		predicate_identifiers/2,predicate_identifiers_in_scope/3]).
156
157		get_typedval_id(typedval(_Val,_Type,ID,_),ID).
158		b_trace_test_components(Properties,ConstantsState,TypedVals) :-
159		%format('b_trace_test_components(~w,~w,~w)',[Properties,ConstantsState,TypedVals]),
160	?	b_trace_test_components(Properties,ConstantsState,TypedVals,all).
161		b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables) :-
162	?	b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables,[]).
163		% in constract to /3 and /4 b_trace_test_components/5 does not fail if the predicate is unsatisfiable.
164		% instead it returns the unsatisfiable component as the last argument
165		% the other predicates still fail because they expect to find an empty list there
166		b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts) :-
167		% we now treat all TypedVals as local variables: ensure that we count them in predicate_components/predicate_identifiers (in case they clash with global identifiers)!
168	?	maplist(get_typedval_id,TypedVals,LocalVars),
169	?	(preferences:get_preference(partition_predicates,true)
170		-> predicate_components_in_scope(Properties,LocalVars,Components),
171		length(Components,Len), print_trace_message(nr_of_components(Len))
172		; predicate_identifiers_in_scope(Properties,LocalVars,PropVars),
173		Components = [component(Properties,PropVars)], Len=1
174		),
175	?	retractall(nr_of_components(_)),assert(nr_of_components(Len)),
176	?	reset_observe_state,
177		% print(components(Components)),nl,
178	?	b_trace_test_components2(Components,ConstantsState,TypedVals,RelevantVariables,1,WFList),
179	?	get_unsat_component(WFList,Components,UnsatConjuncts).
180
181
182		get_unsat_component(_,Components,UnsatConjuncts) :-
183		unsat_component_exists, !,
184		debug_println(9,unsatisfiable_predicate),
185	?	unsat_component(UnsatComponentNr,false),!,
186		nth0(UnsatComponentNr,Components,component(UnsatConjuncts,_)).
187		get_unsat_component(WFList,Components,UnsatConjuncts) :-
188	?	get_unsat_component_aux(WFList,Components,UnsatConjuncts).
189
190		get_unsat_component_aux(WFList,Components,UnsatConjuncts) :-
191	?	print_trace_message(grounding_wait_flags), % Note: for unknown components we continue grounding
192	?	l_ground_wait_flags(WFList),
193		(unsat_component(UnsatComponentNr,_)
194		-> print(we_have_unsat(UnsatComponentNr)),nl,
195		nth0(UnsatComponentNr,Components,component(UnsatConjuncts,_))
196		; UnsatConjuncts=[]).
197		get_unsat_component_aux(_,Components,UnsatConjuncts) :-
198		unsat_component(UnsatComponentNr,_),!,
199		nth0(UnsatComponentNr,Components,component(UnsatConjuncts,_)).
200
201
202		:- use_module(b_ast_cleanup,[predicate_level_optimizations/2]).
203		:- use_module(debug,[printsilent_message/1]).
204		print_trace_message(Msg) :-
205		(preference(provide_trace_information,false) -> true
206		; printsilent_message(Msg)).
207		print_trace_message_with_typed_vals(Msg,TypedVals) :-
208		(preference(provide_trace_information,false) -> true
209		; printsilent_message(Msg),
210		maplist(get_typedval_id,TypedVals,IDs),
211		printsilent_message(IDs)
212		).
213
214		b_trace_test_components2([],_ConstantsState,TypedVals,_,Nr,ResWF) :-
215		(TypedVals=[] -> print_trace_message(finished_processing_component_predicates),
216		ResWF=[]
217		; print_trace_message_with_typed_vals('Enumerating Identifiers without constraints: ',TypedVals),
218		init_wait_flags(WF),
219		b_trace_tighter_enumerate_values(TypedVals,WF), ResWF=[wf_comp(WF,Nr)]).
220		b_trace_test_components2([component(Pred,ComponentVars)|T],ConstantsState,TypedVals,RelevantVariables,
221		Nr,ResWF) :-
222		N1 is Nr+1,
223		((RelevantVariables\=all, ComponentVars\= all,
224		lists_are_disjoint(RelevantVariables,ComponentVars))
225		-> print_trace_message(skipping_irrelevant_component(Nr,ComponentVars)),
226		b_trace_test_components2(T,ConstantsState,TypedVals,RelevantVariables,N1,ResWF)
227		; debug_println(9,checking_component_properties(Nr,ComponentVars)), %%
228		%% print(component(Nr)),nl, translate:nested_print_bexpr_as_classicalb(Pred),debug:nl_time,
229		ResWF = [wf_comp(WF,Nr)|TWF],
230		init_wait_flags(WF),
231		attach_chr_integer_inequality_to_wf_store(WF),
232		(ComponentVars=all -> InTypedVals=TypedVals, OutTypedVals=[], ProjectedState=ConstantsState
233		; project_typed_vals(TypedVals,ComponentVars,InTypedVals,OutTypedVals),
234		project_state(ConstantsState,ComponentVars,ProjectedState) % relevant, e.g., for exists which may wait on state becoming ground
235		),
236		observe_state(InTypedVals,WF,Nr), %%
237		reset_tracetest_for_component,
238		predicate_level_optimizations(Pred,OPred),
239		%%nl,nl,print(component(Nr,ComponentVars,ProjectedState)),nl,nl,translate:print_bexpr(Pred),nl,nl,
240		b_tracetest_boolean_expression(OPred,[],ProjectedState,WF,Nr),
241		%print(done_comp(Nr,WF,ComponentVars)),nl,
242		(skipped_unsat_conjunct(false)
243		-> store_unsat_component_nr(Nr,false),
244		allow_skipping_over_components % check if we allow skipping over unsat components to maybe find as many values for constants as possible ,...
245		% Note: in Disprover mode we can stop and fail straightaway
246		; %print_bt_message(setup_enumerating_constants(Nr)), %%(TypedVals)), %%
247		(skipped_unsat_conjunct(_) -> store_unsat_component_nr(Nr,unknown) ; true), % probably due to prob-ignore
248		b_trace_tighter_enumerate_values(InTypedVals,WF),
249		(preferences:get_preference(disprover_mode,false) -> true
250		; ground_wait_flag0(WF) % ensure that we give each component the chance to run WF0 inconsistency checks
251		%, print(finished_wf0_grounding_in_disprover_mode(Nr)),nl
252		)
253		),
254		% we could ground waitflag 1 (deterministic computations) ?
255		b_trace_test_components2(T,ConstantsState,OutTypedVals,RelevantVariables,N1,TWF)
256		).
257
258		:- use_module(debug,[debug_println/2, debug_mode/1]).
259		:- use_module(tools,[start_ms_timer/1, stop_ms_timer_with_msg/2]).
260
261		l_ground_wait_flags(WF) :-
262	?	l_ground_wait_flags(WF,Result),
263		(Result=false
264		-> (!,fail) % Cut: to prevent backtracking to find other solutions for earlier components !
265		% Assumption: each component is independent and finding other solution for earlier component would again lead to failure in last component checked by l_ground_wait_flags/2
266		; true).
267
268		l_ground_wait_flags([],true).
269		l_ground_wait_flags([wf_comp(WF,ComponentNr)|TWF],SatResult) :- %trace,
270	?	(debug_mode(off) -> true ; print(grounding_component(ComponentNr)),nl, start_ms_timer(Timer)),
271		% print_bt_message(grounding_component(ComponentNr)), portray_waitflags(WF),nl, %%
272		% maybe we should set up new error scope ? <--- TO DO
273	?	if(ground_wait_flags(WF),
274		((debug_mode(on) -> stop_ms_timer_with_msg(Timer,component(ComponentNr)) ; true),
275		l_ground_wait_flags(TWF,SatResult) % continue with other components
276		),
277		((debug_mode(on) -> print(unsatisfiable_component(ComponentNr)),nl,
278		stop_ms_timer_with_msg(Timer,component(ComponentNr)) ; true),
279		store_unsat_component_nr(ComponentNr,false),
280		SatResult=false)).
281
282		project_typed_vals([],_,[],[]).
283		project_typed_vals([typedval(Val,Type,VarID,EnumWarning)|Rest],ComponentVars,In,Out) :-
284	?	(member(VarID,ComponentVars)
285		-> In=[typedval(Val,Type,VarID,EnumWarning)|In2], Out2=Out
286		; Out=[typedval(Val,Type,VarID,EnumWarning)|Out2], In2=In
287		), project_typed_vals(Rest,ComponentVars,In2,Out2).
288		project_state([],_,[]).
289		project_state([bind(VarID,Value)|Rest],ComponentVars,Out) :-
290	?	(member(VarID,ComponentVars)
291		-> Out=[bind(VarID,Value)|Out2]
292		; Out=Out2
293		), project_state(Rest,ComponentVars,Out2).
294
295
296		:- use_module(state_packing,[pack_value/2,unpack_value/2]).
297		:- volatile det_solution_for_constant_packed/2.
298		:- dynamic det_solution_for_constant_packed/2.
299		assert_det_solution_for_constant(Var,Val) :- %print(sol(Var)),tools:print_memory_used_wo_gc,nl,nl,
300		(value_too_large(Val) -> PVal = '$TOO_LARGE' ,debug_println(4,not_storing(Var))
301		; pack_value(Val,PVal)),
302		assert(det_solution_for_constant_packed(Var,PVal)).
303		%,tools:print_memory_used_wo_gc,nl.
304	?	det_solution_for_constant(Var,Val) :- det_solution_for_constant_packed(Var,PVal),
305		(PVal = '$TOO_LARGE'
306		-> add_message(no_det_value_stored_for_constant,'Values were found for some constants but not stored. Set ALLOW_INCOMPLETE_SETUP_CONSTANTS to TRUE to store constants found, e.g.: ',Var),
307		fail
308		; unpack_value(PVal,Val)
309		).
310
311		:- use_module(avl_tools,[avl_height_less_than/2]).
312		value_too_large(avl_set(A)) :-
313		preference(allow_incomplete_partial_setup_constants,false), %if true we always store the value
314		\+ avl_height_less_than(A,7).
315		% TO DO: it could be a small set but include large subsets !
316
317		:- use_module(tools_printing,[print_term_summary/1]).
318		reset_observe_state :- retractall(det_solution_for_constant_packed(_,_)).
319		observe_state(Env,WF,ComponentNr) :-
320		get_wait_flag0(WF,WF0), get_wait_flag1(observe_state,WF,WF1),
321		(preferences:get_preference(provide_trace_information,true)
322		-> when((ground(Env);nonvar(WF0)),print_success(WF0,ComponentNr,Env,WF))
323		%% ,when(nonvar(WF1),(nl, print('Starting Phase 1'),nl, portray_waitflags(WF)))
324		; true),
325		observe_state2(Env,WF0,WF1).
326		%,when(nonvar(WF0),(print(wf0),nl,portray_waitflags(WF))), when(nonvar(WF1),(print(wf1),nl)).
327
328		:- use_module(debug,[debug_format/3]).
329		print_success(WF0,ComponentNr,_,_WF) :- nonvar(WF0),!,
330		debug_format(19,'~n-->> WF0 for component ~w grounded.~n',[ComponentNr]).
331		print_success(_,ComponentNr,Env,_WF) :-
332		format('~n-->> SUCCESS; all constants valued in component ~w~n',[ComponentNr]),
333		(debug_mode(on)
334		-> findall(V,member(typedval(_,_,V,_),Env),Vars),
335		statistics(walltime,[W,_]), format('-->> (walltime: ~w ms) : variables = ~w~n',[W,Vars])
336		; true),
337		%%,check_for_multiple_solutions(WF,ComponentNr) %% comment in to check for multiple solutions
338		nl.
339
340		observe_state2([],_,_).
341		observe_state2([typedval(Val,_Type,VarID,_EnumWarning)|T],WF0,WF1) :-
342		observe_variable(VarID,Val,WF0,WF1),observe_state2(T,WF0,WF1).
343		%observe_state2([bind(Var,Val)|T],WF0) :- observe_variable(Var,Val,WF0), observe_state2(T,WF0).
344
345		% print a warning message if we find multiple solutions *after* all constants have been valued
346		%:- public check_for_multiple_solutions/2.
347		%check_for_multiple_solutions(WF,ComponentNr) :- get_enumeration_finished_wait_flag(WF,EWF),
348		% retractall(solution_found(ComponentNr,_)),
349		% add_solution(EWF,ComponentNr).
350		%:- volatile solution_found/2.
351		%:- dynamic solution_found/2.
352		%:- block add_solution(-,?).
353		%add_solution(_,ComponentNr) :- retract(solution_found(ComponentNr,Nr)),!,
354		% print('*** Multiple solutions found *after valuation* for component '), print(ComponentNr),nl,
355		% N1 is Nr+1,
356		% print('*** Solution: '),print(N1),nl,
357		% assert(solution_found(ComponentNr,N1)).
358		%add_solution(_,ComponentNr) :- % print(add_sol(ComponentNr)),nl,
359		% assert(solution_found(ComponentNr,1)).
360
361		observe_variable(Var,Val,WF0,_WF1) :- preferences:get_preference(provide_trace_information,false),!,
362		observe_variable_no_trace(Var,Val,WF0).
363		observe_variable(Var,Val,WF0,WF1) :- ground_value_check(Val,GrVal),
364		when((nonvar(GrVal);nonvar(WF0)),
365		(var(WF0) -> print('-->> '),print(Var), nl,print(' '),print_term_summary(value(Val)),print_walltime,nl,
366		assert_det_solution_for_constant(Var,Val)
367		; print(' :?: '),print(Var),print(' '), print_term_summary(value(Val)),
368		observe_variable1(Var,Val,WF1)
369		)
370		).
371		:- use_module(kernel_tools,[ground_value/1,ground_value_check/2]).
372		:- block observe_variable_no_trace(?,-,-).
373		observe_variable_no_trace(Var,Val,WF0) :- nonvar(WF0),!, % important e.g. for test 1368
374		(ground_value(Val) -> assert_det_solution_for_constant(Var,Val) ; true).
375		observe_variable_no_trace(Var,Val,WF0) :- ground_value_check(Val,GV),
376		%print_term_summary(gr_val_check(Var,Val,GV)),nl,
377		observe_variable_no_trace4(Var,GV,Val,WF0).
378		:- block observe_variable_no_trace4(?,-,?,-).
379		observe_variable_no_trace4(_,GV,_,_) :- var(GV),!.
380		observe_variable_no_trace4(Var,_,Val,_) :- assert_det_solution_for_constant(Var,Val). % this could be expensive !?
381
382		print_walltime :- statistics(walltime,[Tot,Delta]),
383		(debug_mode(on) -> print(' '),tools:print_memory_used_wo_gc ; true),
384		format(' ~w ms (Delta ~w ms) ',[Tot,Delta]).
385
386		observe_variable1(Var,Val,WF1) :- ground_value_check(Val,GV),
387		when((nonvar(GV);nonvar(WF1)),
388		(nonvar(GV) -> print('--1-->> '),print(Var), nl,print(' '),print_term_summary(value(Val)),
389		assert_det_solution_for_constant(Var,Val)
390		; print(' :?1?: '),print(Var),print(' '), print_term_summary(value(Val))
391		%% , when(ground(Val), (print('--ground-->> '),print(Var),print(' '), print_term_summary(value(Val)))) % comment in to see grounding
392		%% , external_functions:observe_state([bind(Var,Val)]) % comment in to observe values
393		%% , translate:print_bstate([bind(Var,Val)]),nl % comment in to print full value with CLP(FD) info
394		) ).
395
396		/*
397		comment back in for finer-grained observation and uncomment call above
398		:- block observe_instantiation(-,?,?).
399		observe_instantiation(X,Var,Val) :-
400		print(bind(X)),nl,translate:print_bstate([bind(Var,Val)]),nl, (debug_mode(on) -> trace ; true),
401		X =.. [_|Args],
402		observe2(Args,Var,Val).
403
404		observe2([],_,_).
405		observe2([H|T],Var,Val) :- (var(H) -> observe_instantiation(H,Var,Val)
406		; H=.. [_|Args], observe2(Args,Var,Val)),
407		observe2(T,Var,Val).
408		*/
409
410		% --------------------
411
412
413		construct_optimized_exists(Parameters,Body,Pred) :-
414		construct_optimized_exists(Parameters,Body,Pred,true).
415
416		% we could also partition inside b_interpreter ?
417		construct_optimized_exists(Parameters,Body,Pred,Simplify) :-
418		% we can actually do more: first project out all conjuncts which do not have any variables in common with Parameters
419		% #x.(P(x) & Q) <=> #x.(P(x)) & Q
420		% we can also use a stronger version of predicate components #(x,y).( P(x,v) & Q(v,y)) <=> #(x).P(x,v) & #(y).Q(v,y)
421		get_texpr_ids(Parameters,PIDs),
422		%print(constructing_optimized_exists(PIDs)),nl,
423		predicate_components_with_restriction(Body,[],PIDs,Components), % should we use LocalVars instead of [] ?
424		%length(Components,Len), print(nr_of_components_for_exists(Len,Components)),nl,
425		conjunct_components(Components,Parameters,Pred,Simplify).
426		% print('* EXISTS: '),translate:print_bexpr(Pred),nl.
427
428		:- use_module(bsyntaxtree).
429		conjunct_components(C,Parameters,Res,Simplify) :- conjunct_components2(C,Parameters,List,Simplify),
430		conjunct_predicates(List,Res).
431
432		conjunct_components2([],_Parameters,[],_). % :- (Parameters=[] -> true ; print(unused_existential_var(Parameters)),nl).
433		conjunct_components2([component(Pred,ComponentVars)|T],Parameters,Res,Simplify) :-
434		augment_ids(ComponentVars,CV), % translate atomic id names into b(identifier(...
435		tools:list_intersection(CV,Parameters,ExistParas),
436		%print(ord_inter(CV,Parameters,ExistParas)),nl,
437		(Simplify=true
438		-> create_and_simplify_exists(ExistParas,Pred,EP)
439		; create_unsimplified_exists(ExistParas,Pred,EP)),
440		(EP=b(truth,pred,[]) % or should we allow _ for Info field ??
441		-> Res=TRes
442		; Res=[EP|TRes]),
443		conjunct_components2(T,Parameters,TRes,Simplify).
444
445		% translate a list of atomic ides into ids with the b/3 wrapper
446		augment_ids([],[]).
447		augment_ids([ID|T],[b(identifier(ID),_,_)|TT]) :- augment_ids(T,TT).
448
449		extract_equalities(Parameters,Pred, ReducedParas,OutPred) :-
450		extract_equalities2(Pred,Parameters,ReducedParas,NewPred,[],Subst),
451		%sort(Subst,SortedSubst),
452		%print(extracted(Subst)),nl,
453		apply_subst(Subst,NewPred,OutPred).
454		% apply equality inside expressions: note: this may duplicate expressions !
455		% However, it also works if the equalities contain parameters
456
457		extract_equalities2(b(conjunct(A,B),pred,Info),Ids,RemIds,Res) --> !,
458		{Res=b(conjunct(PA,PB),pred,Info)},
459		extract_equalities2(A, Ids,RemIds1,PA),
460		extract_equalities2(B,RemIds1,RemIds,PB).
461		extract_equalities2(b(equal(ID,E),pred,_Info),Ids,RemIds,NewPred,InSubst,OutSubst) :-
462		same_id_is_member(ID,Ids,SID,RemIds),
463		%\+ occurs_in_expr(SID,E), % not cyclic; we check it again after applyng InSubst to E below
464		\+ in_subst_dom(SID,InSubst), % ensure we don't already have an equation for the same ID
465		compose_with_subst(InSubst,SID,E,OutSubst), % we can compose with existing substitution without occurs-check problem
466		always_well_defined_or_disprover_mode(E), % otherwise we may move evaluation of E forward !
467		!,
468		NewPred=b(truth,pred,[]).
469		extract_equalities2(X,Ids,Ids,X) --> [].
470
471		% compose a new binding Var/Expr with existing substitution Subst; where Subst was not yet applied to Expr
472		compose_with_subst(Subst,Var,Expr,[Var/NewExpr|ModSubst]) :-
473		apply_subst(Subst,Expr,NewExpr),
474		\+ occurs_in_expr(Var,NewExpr), % otherwise cyclic
475		apply_binding_to_substitution(Subst,Var,NewExpr,ModSubst).
476		apply_binding_to_substitution([],_,_,[]).
477		apply_binding_to_substitution([TV/TE|T],Var,Expr,[TV/TE2|NT]) :-
478		\+ occurs_in_expr(TV,Expr), % otherwise we get a cyclic substitution --> fail
479		replace_id_by_expr(TE,Var,Expr,TE2),
480		apply_binding_to_substitution(T,Var,Expr,NT).
481
482		apply_subst([],X,X).
483		apply_subst([Var/Expr|T],E,NewE) :-
484		(replace_id_by_expr(E,Var,Expr,E2) % replace identifier Var by expression Expr
485		-> %apply_to_tail(T,Var,Expr,NT), % apply binding to tail of substitution
486		apply_subst(T,E2,NewE)
487		; add_internal_error('Call failed: ',apply_subst([Var/Expr|T],E,NewE)),NewE=E).
488
489
490		in_subst_dom(X,[I/_|T]) :- (X=I -> true ; in_subst_dom(X,T)).
491
492		same_id_is_member(X,[H|T],SID,Rest) :-
493		(same_id(X,H,SID) -> Rest=T ; Rest=[H|TR],same_id_is_member(X,T,SID,TR)).
494
495		% TO DO: investigate what is the exact difference with create_exists_opt
496		create_and_simplify_exists(Paras,Pred,ResultingPred) :-
497		% print(exists(Paras)),nl, translate:print_bexpr(Pred),nl,
498		extract_equalities(Paras,Pred,NewParas,NewPred),
499		% translate:print_bexpr(NewPred),nl,
500		%print(create_and_simplify_exists2(NewParas,NewPred)),nl,
501		create_and_simplify_exists2(NewParas,NewPred,ResultingPred).
502
503		%:- use_module(b_interpreter_check,[arithmetic_op/4]). % TODO REFACTOR and move this and code below to separate module
504		create_and_simplify_exists2([],Pred,R) :- !,R=Pred.
505		% simplify #ID.(ID:E1 & ID:E2) <=> E1 /\ E2 /= {} , etc... now done in ast_cleanup
506		% simplify #ID.(ID/:E) <=> E /= FullType also done in ast_cleanup
507		% simplify #SID.(SID > Expr) <=> truth now done in ast_cleanup
508		create_and_simplify_exists2(Parameters,Body,Res) :- create_unsimplified_exists(Parameters,Body,Res).
509		% TO DO: treat nested exists
510
511
512
513		:- use_module(b_ast_cleanup,[clean_up_pred/3]).
514		:- use_module(bsyntaxtree,[add_texpr_info_if_new/3]).
515		create_unsimplified_exists(Parameters,Body,Res) :-
516		% print(create_unsimplified_exists(Parameters,Body)),nl,
517		create_exists(Parameters,Body,Res1),
518		add_texpr_info_if_new(Res1,removed_typing,Res2), % unconditionally add this info, avoid generating warnings in exists_body_warning, see test 625
519		clean_up_pred(Res2,[],Res). % also computes used_ids,
520		% and performs some existential quantifier optimisations like replace_exists_by_not_empty
521		% previously removed_typing was only added for disjuncts or implications:
522		% (bsyntaxtree:is_a_disjunct_or_implication(Body,_,_,_)
523		% -> add_texpr_infos(Res2,[removed_typing],Res3) % avoid generating warnings in exists_body_warning; see, e.g., test 625
524		% ; Res3=Res2),