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		:- module(b_interpreter_components,[
6		reset_component_info/1,
7		b_trace_test_components/3, b_trace_test_components/4,
8		b_trace_test_components_wf/4,
9		unsat_component/2, unsat_component_enumeration_warning/1,
10		unsat_or_unknown_component_exists/0,
11		unsat_component_abort_error/1,
12		unsat_conjunct_inside_component/4,
13		det_solution_for_constant/2, get_det_solution_for_constant_value_kind/2,
14		det_solution_for_constant_was_stored/0, det_solution_for_constant_was_stored/1,
15		b_tracetest_boolean_expression/5,
16		observe_state/3,
17
18		construct_optimized_exists/3, construct_optimized_exists/4,
19		construct_optimized_exists/5,
20		extract_equalities_in_quantifier/4
21		]).
22
23		:- use_module(b_interpreter,[b_test_boolean_expression/6]).
24		:- use_module(preferences).
25		:- use_module(kernel_waitflags).
26		:- use_module(tools).
27		:- use_module(translate).
28		:- use_module(error_manager).
29		:- use_module(library(lists)).
30		:- use_module(b_enumerate, [b_tighter_enumerate_all_values/2, b_tighter_enumerate_values/3]).
31
32		:- use_module(debug,[debug_println/2, debug_mode/1]).
33		:- use_module(tools,[start_ms_timer/1, stop_ms_timer_with_msg/2, stop_ms_timer_with_debug_msg/2]).
34
35		:- use_module(chrsrc(chr_integer_inequality),[attach_chr_integer_inequality_to_wf_store/1]).
36
37
38		:- use_module(module_information,[module_info/2]).
39		:- module_info(group,interpreter).
40		:- module_info(description,'This module can be used to split a predicate into components and solving each component individually (with tracing feedback).').
41
42		/* -------------- */
43		/* dynamic bits */
44		/* -------------- */
45
46		:- dynamic skipped_unsat_conjunct/1, unsat_conjunct_inside_component/4.
47		reset_unsat_conjunct_inside_component_info :-
48		retractall(skipped_unsat_conjunct(_)),
49		retractall(unsat_conjunct_inside_component(_,_,_,_)).
50		reset_tracetest_for_component :- retractall(skipped_unsat_conjunct(_)). % to be called before trace checking a component
51
52		% individual conjuncts which are directly unsatisfiable
53		assert_skipped_failed_conjunct(ComponentNr,BE) :- assert_skipped_unsat_conjunct,
54		assertz(unsat_conjunct_inside_component(ComponentNr,BE,false,'')),
55		(preferences:get_preference(provide_trace_information,false) -> true
56		; add_message(b_interpreter_components,' *** INCONSISTENCY DETECTED, SKIPPING COMPONENT NR: ',ComponentNr, BE),
57		(debug_mode(on) -> print_bexpr_with_limit(BE,500) ; print_bexpr_with_limit(BE,150)), nl
58		).
59		assert_skipped_unknown_conjunct(ComponentNr,BE,Reason) :- assert_skipped_unknown_conjunct,
60		assertz(unsat_conjunct_inside_component(ComponentNr,BE,unknown,Reason)),
61		((Reason=abort_error; Reason=well_definedness_error)
62		-> assert_unsat_component_abort_error(ComponentNr)
63		; true),
64		(preferences:get_preference(provide_trace_information,false) -> true
65		; get_reason_msg(Reason,MSG),format(' *** Skipping predicate due to ~w:',[MSG]),
66		write(' '),print_bexpr_with_limit(BE,150),nl,
67		format('~n *** Predicate is unknown~n *** COMPONENT NUMBER: ~w~n',[ComponentNr])
68		).
69		assert_skipped_unsat_conjunct :-
70		(skipped_unsat_conjunct(false) -> true
71		; retractall(skipped_unsat_conjunct(_)), assertz(skipped_unsat_conjunct(false))).
72		assert_skipped_unknown_conjunct :-
73		(skipped_unsat_conjunct(_) -> true ; assertz(skipped_unsat_conjunct(unknown))).
74
75		get_reason_msg(enumeration_warning,R) :- !, R='ENUMERATION WARNING'.
76		get_reason_msg(M,M).
77
78
79		:- dynamic unsat_component/2, unsat_component_enumeration_warning/1, unsat_component_abort_error/1.
80		reset_unsat_component_info :-
81		retractall(unsat_component(_,_)),
82		retractall(unsat_component_enumeration_warning(_)),
83		retractall(unsat_component_abort_error(_)).
84
85		reset_all_component_infos :-
86		reset_unsat_component_info,
87		reset_unsat_conjunct_inside_component_info,
88		reset_observe_state.
89
90		:- use_module(eventhandling,[register_event_listener/3]).
91		:- register_event_listener(clear_specification,reset_all_component_infos,
92		'Reset b_interpreter_components unsat component info.').
93
94
95		store_unsat_component_nr(X) :- % use if you do not know if it is unknown or unsat
96		%error_manager:print_error_scopes,
97		(critical_enumeration_warning_occured_in_error_scope
98		-> Res = unknown
99		% should we also detect abort_error_occured_in_error_scope ?
100		; Res=false),
101		store_unsat_component_nr(X,Res).
102
103		store_unsat_component_nr(X,FalseOrUnknown) :-
104		debug_println(9,store_unsat_component_nr(X,FalseOrUnknown)),
105		(unsat_component(X,false) -> true
106		; retractall(unsat_component(X,_)),assertz(unsat_component(X,FalseOrUnknown))
107		),
108		(critical_enumeration_warning_occured_in_error_scope,
109		\+ unsat_component_enumeration_warning(X)
110		-> assertz(unsat_component_enumeration_warning(X)),
111		debug_println(19,enumeration_warning_in_component(X))
112		; true),
113		(abort_error_occured_in_error_scope
114		-> assert_unsat_component_abort_error(X)
115		; true).
116		%portray_unsat_components.
117		unsat_component_exists :- unsat_component(_,false),!.
118		unsat_or_unknown_component_exists :- unsat_component(_,_),!.
119
120		% store the fact that an abort or wd error occurred for component
121		assert_unsat_component_abort_error(X) :- \+ unsat_component_abort_error(X),
122		assertz(unsat_component_abort_error(X)),
123		debug_println(19,unsat_component_abort_error(X)).
124
125		% small utility to display status of components
126		:- public portray_unsat_components/0.
127		portray_unsat_components :- format('Unsat components~n',[]),
128		unsat_component(Comp,Status),
129		(unsat_component_abort_error(Comp) -> Abort='abort/well_definedness error' ; Abort=''),
130		(unsat_component_enumeration_warning(Comp) -> EW='enumeration_warning' ; EW=''),
131		format('* component: ~w -> ~w ~w ~w~n',[Comp,Status,Abort,EW]),
132		unsat_conjunct_inside_component(Comp,BE,S,Reason),
133		format(' -> reason for ~w: ~w : ',[S,Reason]), translate:print_bexpr_with_limit(BE,100),nl,
134		fail.
135		portray_unsat_components.
136
137		:- public nr_of_components/1.
138		:- dynamic nr_of_components/1.
139		:- dynamic allow_skipping_over_components/0.
140		reset_component_info(AllowSkip) :- retractall(allow_skipping_over_components),
141		(AllowSkip==true -> assertz(allow_skipping_over_components) ; true),
142		reset_unsat_component_info,
143		reset_unsat_conjunct_inside_component_info.
144
145		% 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 !!
146		% TO DO: keep track of enumeration warnings per component
147
148		/* -------------- */
149
150
151		:- use_module(library(avl)).
152		% You can use the term one as ComponentNr if you don't know the number or it is not relevant
153		b_tracetest_boolean_expression(BE,LS,S,WF,ComponentNr) :- %print(catch(ComponentNr)),nl,
154		empty_avl(Ai),
155	?	catch_enumeration_warning_exceptions_and_wd_failures(
156		b_tracetest_boolean_expression1(BE,LS,S,WF,ComponentNr,Ai,_Ao),
157		% this should not backtrack (without WF0 set); otherwise we may get problems with error blocks nesting
158		assert_skipped_unknown_conjunct(ComponentNr,BE,enumeration_warning),
159		true, % true: add exceptions as event errors
160		assert_skipped_unknown_conjunct(ComponentNr,BE,well_definedness_error), % for WD error
161		component(ComponentNr)). % Source argument for debugging
162
163		b_tracetest_boolean_expression1(b(Expr,_,Infos),LS,S,WF,ComponentNr,Ai,Ao) :-
164	?	b_tracetest_boolean_expression2(Expr,Infos,LS,S,WF,ComponentNr,Ai,Ao).
165
166		:- use_module(bsyntaxtree,[is_a_conjunct_or_neg_disj/3]).
167		b_tracetest_boolean_expression2(Conjunct,Info,LocalState,State,WF,ComponentNr,Ai,Ao) :-
168		is_a_conjunct_or_neg_disj(b(Conjunct,pred,Info),LHS,RHS),
169		% also detects: not(A or B) <=> not(A) & not(B) and not(A=>B) <=> A & not(B)
170		% \+(Info = [try_smt|_]),
171		!,
172		%% print('check lhs of conjunct: '), translate:print_bexpr(LHS),nl,
173		b_tracetest_boolean_expression1(LHS,LocalState,State,WF,ComponentNr,Ai,Aii),
174		%% print('check rhs of conjunct: '), translate:print_bexpr(RHS),nl,
175	?	b_tracetest_boolean_expression1(RHS,LocalState,State,WF,ComponentNr,Aii,Ao).
176		b_tracetest_boolean_expression2(BE,Infos,LS,S,WF,ComponentNr,Ai,Ao) :-
177		(get_preference(provide_trace_information,true)
178		-> format('~n ====> (~w) ',[ComponentNr]),
179		print_bexpr_with_limit(b(BE,pred,Infos),250),nl
180		; true),
181	?	if(safe_b_test_boolean_expression(ComponentNr,b(BE,pred,Infos),LS,S,WF,Ai,Ao),
182		true,
183		(assert_skipped_failed_conjunct(ComponentNr,b(BE,pred,Infos)),
184		Ai=Ao)).
185
186
187		safe_b_test_boolean_expression(ComponentNr,BE,LS,S,WF,Ai,Ao) :- %print(c(_ComponentNr,WF)),nl, translate:print_bexpr(BE),nl,
188		preferences:get_preference(provide_trace_information,false),
189		\+ abort_error_occured_in_error_scope,
190		% avoid setting up new error scope for every conjunct with catch_enumeration_warning
191		% BE is only displayed in TRACE_INFO mode anyway
192		% can be a bottleneck, e.g., for :prob-file ../prob_examples/public_examples/Eval/Sudoku_SAT.eval
193		!,
194	?	if(b_test_boolean_expression(BE,LS,S,WF,Ai,Ao),true,
195		(abort_error_occured_in_error_scope
196		-> assert_unknown(ComponentNr,BE,abort_error,Ai,Ao)
197		; fail)
198		).
199		safe_b_test_boolean_expression(ComponentNr,BE,LS,S,WF,Ai,Ao) :-
200		catch_enumeration_warning_exceptions_and_wd_failures(
201		b_test_boolean_expression(BE,LS,S,WF,Ai,Ao), % this should not backtrack (without WF0 set);
202		% otherwise we may get problems with error blocks nesting
203		assert_unknown(ComponentNr,BE,enumeration_warning,Ai,Ao), % call when exception caught
204		true, % true: add exceptions as event errors
205		assert_unknown(ComponentNr,BE,well_definedness_error,Ai,Ao), % call when wd_error caught
206		component(ComponentNr)). % Source argument for debugging
207
208		% Note: this will only detect enumeration warnings and WD errors in WF0 phase
209
210		assert_unknown(ComponentNr,BE,Reason,Ai,Ao) :- % print(assert_unknown(ComponentNr,Reason)),nl,
211		assert_skipped_unknown_conjunct(ComponentNr,BE,Reason),Ai=Ao.
212
213		:- use_module(bsyntaxtree,[predicate_components_in_scope/3,
214		predicate_identifiers_in_scope/3]).
215		:- use_module(b_enumerate,[extract_do_not_enum_ids_from_predicate/2]).
216
217		get_typedval_id(typedval(_Val,_Type,ID,_),ID).
218		b_trace_test_components(Properties,ConstantsState,TypedVals) :-
219		%format('b_trace_test_components(~w,~w,~w)',[Properties,ConstantsState,TypedVals]),
220		b_trace_test_components(Properties,ConstantsState,TypedVals,all).
221		b_trace_test_components_wf(Properties,ConstantsState,TypedVals,WF) :-
222	?	b_trace_test_components_wf(Properties,ConstantsState,TypedVals,all,[],WF).
223		b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables) :-
224		b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables,[]).
225		% in constract to /3 and /4 b_trace_test_components/5 does not fail if the predicate is unsatisfiable.
226		% instead it returns the unsatisfiable component as the last argument
227		% the other predicates still fail because they expect to find an empty list there
228		b_trace_test_components(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts) :-
229		b_trace_test_components_wf(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts,no_wf_available).
230		b_trace_test_components_wf(Properties,ConstantsState,TypedVals,RelevantVariables,UnsatConjuncts,OuterWF) :-
231		% we now treat all TypedVals as local variables:
232		% ensure that we count them in predicate_components/predicate_identifiers
233		% (in case they clash with global identifiers)!
234		%start_ms_timer(T0),
235		maplist(get_typedval_id,TypedVals,LocalVars),
236		extract_do_not_enum_ids_from_predicate(Properties,DoNotEnumVars),
237		(preferences:get_preference(partition_predicates,true)
238		-> predicate_components_in_scope(Properties,LocalVars,Components),
239		length(Components,Len), print_trace_message(nr_of_components(Len))
240		; predicate_identifiers_in_scope(Properties,LocalVars,PropVars),
241		Components = [component(Properties,PropVars)], Len=1
242		),
243		retractall(nr_of_components(_)),assertz(nr_of_components(Len)),
244		reset_observe_state,
245		%stop_ms_timer_with_debug_msg(T0,b_trace_test_components_preprocessing),
246	?	b_trace_test_components2(Components,ConstantsState,TypedVals,RelevantVariables,DoNotEnumVars,1,WFList,OuterWF),
247	?	get_unsat_component(WFList,Components,UnsatConjuncts).
248
249
250		get_unsat_component(_,Components,UnsatConjuncts) :-
251		unsat_component_exists, !,
252		debug_println(9,unsatisfiable_predicate),
253		unsat_component(UnsatComponentNr,false),!,
254		nth1(UnsatComponentNr,Components,component(UnsatConjuncts,_)).
255		get_unsat_component(WFList,Components,UnsatConjuncts) :-
256	?	get_unsat_component_aux(WFList,Components,UnsatConjuncts).
257
258		get_unsat_component_aux(WFList,Components,UnsatConjuncts) :-
259		print_trace_message(grounding_wait_flags), % Note: for unknown components we continue grounding
260	?	l_ground_wait_flags(WFList),
261		(unsat_component(UnsatComponentNr,Status)
262		-> debug_println(19,unsat_component(UnsatComponentNr,Status)), UnsatConjuncts \== [],
263		nth1(UnsatComponentNr,Components,component(UnsatConjuncts,_))
264		; UnsatConjuncts=[]).
265		get_unsat_component_aux(_,Components,UnsatConjuncts) :-
266		unsat_component(UnsatComponentNr,_),!,
267		nth1(UnsatComponentNr,Components,component(UnsatConjuncts,_)).
268
269
270		:- use_module(b_ast_cleanup,[predicate_level_optimizations/2]).
271		:- use_module(debug,[printsilent_message/1]).
272		print_trace_message(Msg) :-
273		(preference(provide_trace_information,false) -> true
274		; printsilent_message(Msg)).
275		print_trace_message_with_typed_vals(Msg,TypedVals) :-
276		(preference(provide_trace_information,false) -> true
277		; printsilent_message(Msg),
278		maplist(get_typedval_id,TypedVals,IDs),
279		printsilent_message(IDs)
280		).
281
282		b_trace_test_components2([],_ConstantsState,TypedVals,_,_,Nr,ResWF,OuterWF) :-
283		(TypedVals=[]
284		-> print_trace_message(finished_processing_component_predicates),
285		ResWF=[]
286		; print_trace_message_with_typed_vals('Enumerating Identifiers without constraints: ',TypedVals),
287		init_wait_flags(WF0,[b_tighter_enumerate_values]),
288		copy_wait_flag_call_stack_info(OuterWF,WF0,WF),
289		b_tighter_enumerate_all_values(TypedVals,WF), ResWF=[wf_comp(WF,Nr)]).
290		b_trace_test_components2([component(Pred,ComponentVars)|T],ConstantsState,TypedVals,RelevantVariables,DoNotEnumVars,
291		Nr,ResWF,OuterWF) :-
292		N1 is Nr+1,
293		( RelevantVariables\=all, ComponentVars\= all,
294		lists_are_disjoint(RelevantVariables,ComponentVars)
295		-> print_trace_message(skipping_irrelevant_component(Nr,ComponentVars)),
296		b_trace_test_components2(T,ConstantsState,TypedVals,RelevantVariables,DoNotEnumVars,N1,ResWF,OuterWF)
297		; %% print(checking_component_properties(Nr,ComponentVars)),nl, %%
298		%% print(component(Nr)),nl, translate:nested_print_bexpr_as_classicalb(Pred),debug:nl_time,
299		ResWF = [wf_comp(WF,Nr)|TWF],
300		init_wait_flags(WF0,[wf_comp(Nr)]),
301		copy_wait_flag_call_stack_info(OuterWF,WF0,WF),
302		(preferences:preference(use_chr_solver,true) -> attach_chr_integer_inequality_to_wf_store(WF) ; true),
303		(ComponentVars=all -> InTypedVals=TypedVals, OutTypedVals=[], ProjectedState=ConstantsState
304		; project_typed_vals(TypedVals,ComponentVars,InTypedVals,OutTypedVals),
305		project_state(ConstantsState,ComponentVars,ProjectedState) % relevant, e.g., for exists which may wait on state becoming ground
306		),
307		observe_state(InTypedVals,WF,Nr), %%
308		reset_tracetest_for_component,
309		predicate_level_optimizations(Pred,OPred),
310		%%nl,nl,print(component(Nr,ComponentVars,ProjectedState)),nl,nl,translate:print_bexpr(Pred),nl,nl,
311		%%start_ms_timer(T1),
312	?	b_tracetest_boolean_expression(OPred,[],ProjectedState,WF,Nr),
313		% Skipping can only occur in this call above, not in enumeration phase
314		%% stop_ms_timer_with_debug_msg(T1,b_tracetest_boolean_expression(Nr)),
315		%print(done_comp(Nr,WF,ComponentVars)),nl,
316		(skipped_unsat_conjunct(FalseOrUnknown)
317		-> store_unsat_component_nr(Nr,FalseOrUnknown), % can be unknown due to an enumeration warning, cf. test 1390
318		%print('UNSAT: '),translate:nested_print_bexpr(Pred),nl,nl,
319		allow_skipping_over_components % check if we allow skipping over unsat components to
320		% maybe find as many values for constants as possible (partial setup_constants),...
321		% Note: in Disprover mode or solve_predicate (REPL) we can stop and fail straightaway
322		; %print_bt_message(setup_enumerating_constants(Nr)), %%(TypedVals)), %%
323		b_tighter_enumerate_values(InTypedVals,DoNotEnumVars,WF),
324		(preferences:get_preference(disprover_mode,false) -> true
325		; ground_wait_flag0(WF) % ensure that we give each component the chance to run WF0 inconsistency checks
326		%, print(finished_wf0_grounding_in_disprover_mode(Nr)),nl
327		)
328		),
329		% we could ground waitflag 1 (deterministic computations) ?
330	?	b_trace_test_components2(T,ConstantsState,OutTypedVals,RelevantVariables,DoNotEnumVars,N1,TWF,OuterWF)
331		).
332
333
334		l_ground_wait_flags(WF) :-
335	?	l_ground_wait_flags(WF,WFE,Result),
336		(Result=false
337		-> (!,fail) % Cut: to prevent backtracking to find other solutions for earlier components !
338		% 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
339		; grd_ef(WFE)).
340
341		l_ground_wait_flags([],_,true).
342		l_ground_wait_flags([wf_comp(_,ComponentNr)|TWF],WFE,SatResult) :-
343		unsat_component(ComponentNr,_),!, % We now longer try and ground unknown components
344		l_ground_wait_flags(TWF,WFE,SatResult).
345		l_ground_wait_flags([wf_comp(WF,ComponentNr)|TWF],WFE,SatResult) :-
346		(debug_mode(off) -> true ; print(grounding_component(ComponentNr)),nl, start_ms_timer(Timer)),
347		% print_bt_message(grounding_component(ComponentNr)), portray_waitflags(WF),nl, %%
348		% maybe we should set up new error scope ? <--- TO DO
349	?	if(ground_constraintprop_wait_flags(WF),
350		((pending_abort_error(WF) -> assert_unsat_component_abort_error(ComponentNr) ; true),
351		(debug_mode(on) -> (pending_abort_error(WF) -> Msg='PENDING WD/ABORT ERROR'; Msg='true'),
352		stop_ms_timer_with_msg(Timer,component(ComponentNr,Msg))
353		; true),
354		get_enumeration_finished_wait_flag(WF,WFE), % bind enumeration finished to the global outer WFE flag
355	?	l_ground_wait_flags(TWF,WFE,SatResult) % continue with other components
356		),
357		((debug_mode(on) -> print(unsatisfiable_component(ComponentNr)),nl,
358		stop_ms_timer_with_msg(Timer,component(ComponentNr,'false')) ; true),
359		store_unsat_component_nr(ComponentNr),
360		SatResult=false)).
361
362		project_typed_vals([],_,[],[]).
363		project_typed_vals([typedval(Val,Type,VarID,EnumWarningInfos)|Rest],ComponentVars,In,Out) :-
364	?	(member(VarID,ComponentVars)
365		-> In = [typedval(Val,Type,VarID,EnumWarningInfos)|In2], Out2=Out
366		; Out = [typedval(Val,Type,VarID,EnumWarningInfos)|Out2], In2=In
367		), project_typed_vals(Rest,ComponentVars,In2,Out2).
368		project_state([],_,[]).
369		project_state([bind(VarID,Value)|Rest],ComponentVars,Out) :-
370	?	(member(VarID,ComponentVars)
371		-> Out=[bind(VarID,Value)|Out2]
372		; Out=Out2
373		), project_state(Rest,ComponentVars,Out2).
374
375
376		:- use_module(specfile,[get_specification_description/2]).
377		:- use_module(state_packing,[pack_value/2,unpack_value/2]).
378		:- volatile det_solution_for_constant_packed/2.
379		:- dynamic det_solution_for_constant_packed/2.
380		assert_det_solution_for_constant(Var,Val) :-
381		(value_too_large(Val) -> PVal = '$TOO_LARGE' ,debug_println(4,not_storing(Var))
382		; pack_value(Val,PVal)
383		%,translate:translate_bvalue_with_limit(Val,200,VS),format(' STORING ---> ~w = ~w~n',[Var,VS])
384		),
385		assertz(det_solution_for_constant_packed(Var,PVal)).
386
387		det_solution_for_constant(Var,Val) :-
388		if(det_solution_for_constant_packed(Var,PVal),
389		unpack_det_sol(Var,PVal,Val),
390		(get_specification_description(properties,PROPS),
391		ajoin([PROPS, ' are *not* true and no value was found (deterministically) for the following CONSTANT: '], Msg),
392		add_message(det_value_not_found_for_constant,Msg,Var),
393		fail)
394		).
395		unpack_det_sol(Var,PVal,Val) :-
396		(PVal = '$TOO_LARGE'
397		-> ajoin(['The following CONSTANT was not stored due to its size (set preference ALLOW_INCOMPLETE_SETUP_CONSTANTS to TRUE to store all constants found): '], Msg),
398		add_message(det_value_not_stored_for_constant,Msg,Var),
399		fail
400		; unpack_value(PVal,Val)
401		).
402
403		:- use_module(probsrc(translate), [translate_bvalue_kind/2]).
404		get_det_solution_for_constant_value_kind(Var,ValKind) :-
405		det_solution_for_constant_packed(Var,PVal),
406		(PVal = '$TOO_LARGE' -> ValKind='LARGE-VALUE'
407		; unpack_value(PVal,Val),
408		(translate_bvalue_kind(Val,K) -> ValKind=K ; ValKind='UNKNOWN-VALUE')
409		).
410
411		det_solution_for_constant_was_stored :- (det_solution_for_constant_was_stored(_) -> true).
412		det_solution_for_constant_was_stored(Var) :- det_solution_for_constant_packed(Var,_).
413
414		:- use_module(probsrc(bsyntaxtree),[map_over_bexpr/2]).
415		:- use_module(avl_tools,[avl_height_less_than/2]).
416		value_too_large(avl_set(A)) :-
417		preference(allow_incomplete_partial_setup_constants,false), %if true we always store the value
418		(preference(provide_trace_information,false) -> MaxH=7 ; MaxH=9),
419		\+ avl_height_less_than(A,MaxH).
420		% TO DO: it could be a small set but include large subsets !
421		value_too_large((A,B)) :- (value_too_large(A) -> true ; value_too_large(B)).
422		value_too_large(rec(F)) :- member(field(_,FVal),F), value_too_large(FVal).
423		value_too_large(closure(P,T,B)) :-
424		\+ custom_explicit_sets:is_interval_closure(P,T,B,_,_),
425		preference(allow_incomplete_partial_setup_constants,false),
426		uses_large_value(B).
427		% we can have large symbolic closures; cf PlanProGross.mch; see also test 1637
428
429		% assumes values are all ground:
430		uses_large_value_aux(value(V)) :- value_too_large(V).
431
432		uses_large_value(BExpr) :-
433		map_over_bexpr(uses_large_value_aux,BExpr).
434
435
436
437		:- use_module(tools_printing,[print_value_summary/1]).
438		reset_observe_state :- retractall(det_solution_for_constant_packed(_,_)).
439		observe_state(Env,WF,ComponentNr) :-
440		get_wait_flag0(WF,WF0), get_wait_flag1(observe_state,WF,WF1),
441		(preferences:get_preference(provide_trace_information,true)
442		-> when((ground(Env);nonvar(WF0)),print_success(WF0,ComponentNr,Env,WF))
443		%% ,when(nonvar(WF1),(nl, print('Starting Phase 1'),nl, portray_waitflags(WF)))
444		; true),
445		observe_state2(Env,WF0,WF1).
446		%,when(nonvar(WF0),(print(wf0),nl,portray_waitflags(WF))), when(nonvar(WF1),(print(wf1),nl)).
447
448		:- use_module(debug,[debug_format/3]).
449		print_success(WF0,ComponentNr,_,_WF) :- nonvar(WF0),!,
450		debug_format(19,'~n-->> WF0 for component ~w grounded.~n',[ComponentNr]).
451		print_success(_,ComponentNr,Env,_WF) :-
452		(Env=[]
453		->
454		format('~n-->> SUCCESS; processed component ~w (no identifiers)~n',[ComponentNr])
455		; length(Env,NrVal),
456		format('~n-->> SUCCESS; all ~w identifier(s) valued in component ~w~n',[NrVal,ComponentNr])
457		),
458		(debug_mode(on)
459		-> findall(V,member(typedval(_,_,V,_),Env),Vars),
460		statistics(walltime,[W,_]), format('-->> (walltime: ~w ms) : identifiers = ~w~n',[W,Vars])
461		; true),
462		%%,check_for_multiple_solutions(WF,ComponentNr) %% comment in to check for multiple solutions
463		nl.
464
465		observe_state2([],_,_).
466		observe_state2([Binding|T],WF0,WF1) :- get_binding_value(Binding,VarID,Val),
467		observe_variable(VarID,Val,WF0,WF1),observe_state2(T,WF0,WF1).
468
469		get_binding_value(bind(Id,Value),Id,Value).
470		get_binding_value(typedval(Value,_Type,Id,_Trigger),Id,Value).
471
472		% print a warning message if we find multiple solutions *after* all constants have been valued
473		%:- public check_for_multiple_solutions/2.
474		%check_for_multiple_solutions(WF,ComponentNr) :- get_enumeration_finished_wait_flag(WF,EWF),
475		% retractall(solution_found(ComponentNr,_)),
476		% add_solution(EWF,ComponentNr).
477		%:- volatile solution_found/2.
478		%:- dynamic solution_found/2.
479		%:- block add_solution(-,?).
480		%add_solution(_,ComponentNr) :- retract(solution_found(ComponentNr,Nr)),!,
481		% print('*** Multiple solutions found *after valuation* for component '), print(ComponentNr),nl,
482		% N1 is Nr+1,
483		% print('*** Solution: '),print(N1),nl,
484		% assertz(solution_found(ComponentNr,N1)).
485		%add_solution(_,ComponentNr) :-
486		% assertz(solution_found(ComponentNr,1)).
487
488		observe_variable(Var,Val,WF0,_WF1) :- preferences:get_preference(provide_trace_information,false),!,
489		observe_variable_no_trace(Var,Val,WF0).
490		observe_variable(Var,Val,WF0,WF1) :-
491		ground_value_check(Val,GrVal),
492		observe_variable0_block(Var,Val,GrVal,WF0,WF1).
493		:- block observe_variable0_block(?,?,-,-,?).
494		observe_variable0_block(Var,Val,GrVal,WF0,WF1) :-
495		(var(GrVal) -> write(' :?: '), write(Var), write(' '), print_value_summary(Val),
496		observe_variable1(Var,Val,WF1)
497		; (var(WF0) -> write('-->> ')
498		; write('--0-->> ')), % WF0/GrVal grounded at same time probably does not happen (often)
499		write(Var),nl, write(' '),print_value_summary(Val),print_walltime,nl,
500		assert_det_solution_for_constant(Var,Val)
501		).
502		:- use_module(kernel_tools,[ground_value/1,ground_value_check/2]).
503		:- block observe_variable_no_trace(?,-,-).
504		observe_variable_no_trace(Var,Val,WF0) :- nonvar(WF0),!, % important e.g. for test 1368
505		(ground_value(Val) -> assert_det_solution_for_constant(Var,Val) ; true).
506		observe_variable_no_trace(Var,Val,WF0) :- ground_value_check(Val,GV),
507		%tools_printing:print_term_summary(gr_val_check(Var,Val,GV)),nl,
508		observe_variable_no_trace4(Var,GV,Val,WF0).
509		:- block observe_variable_no_trace4(?,-,?,-).
510		observe_variable_no_trace4(_,GV,_,_) :- var(GV),!.
511		observe_variable_no_trace4(Var,_,Val,_) :- assert_det_solution_for_constant(Var,Val). % this could be expensive !?
512
513		print_walltime :- statistics(walltime,[Tot,Delta]),
514		(debug_mode(on) -> print(' '),tools:print_memory_used_wo_gc ; true),
515		format(' ~w ms (Delta ~w ms) ',[Tot,Delta]).
516
517		observe_variable1(Var,Val,WF1) :- ground_value_check(Val,GV),
518		observe_variable1_block(Var,Val,WF1,GV).
519		:- block observe_variable1_block(?,?,-,-).
520		observe_variable1_block(Var,Val,_WF1,GV):-
521		(nonvar(GV)
522		-> write('--1-->> '), write(Var),nl, write(' '),print_value_summary(Val),
523		assert_det_solution_for_constant(Var,Val)
524		; write(' :?1?: '), write(Var), write(' '), print_value_summary(Val)
525		%% , when(ground(Val), (print('--ground-->> '),print(Var),print(' '), print_value_summary(Val))) % comment in to see grounding
526		%% , external_functions:observe_state([bind(Var,Val)]) % comment in to observe values
527		%% , translate:print_bstate([bind(Var,Val)]),nl % comment in to print full value with CLP(FD) info
528		).
529
530
531		% --------------------
532
533		construct_optimized_exists(Parameters,Body,Pred) :-
534		construct_optimized_exists(Parameters,Body,Pred,true,_).
535		construct_optimized_exists(Parameters,Body,Pred,Simplify) :-
536		construct_optimized_exists(Parameters,Body,Pred,Simplify,_).
537
538		% we could also partition inside b_interpreter ?
539		construct_optimized_exists(Parameters,Body,Pred,Simplify,NrComponents) :-
540		% we can actually do more: first project out all conjuncts which do not have any variables in common with Parameters
541		% #x.(P(x) & Q) <=> #x.(P(x)) & Q
542		% 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)
543		get_texpr_ids(Parameters,PIDs),
544		%print(constructing_optimized_exists(PIDs)),nl,
545		LocalVars = PIDs,
546		predicate_components_with_restriction(Body,LocalVars,PIDs,Components), % we focus partition decision on PIDs, not on all identifiers
547		%length(Components,Len), print(nr_of_components_for_exists(Len,Components)),nl,
548		conjunct_components(Components,Parameters,Pred,Simplify,NrComponents).
549		% print('* EXISTS: '),translate:print_bexpr(Pred),nl.
550
551		:- use_module(bsyntaxtree).
552		conjunct_components(C,Parameters,Res,Simplify,NrComponents) :-
553		conjunct_components2(C,Parameters,List,Simplify,0,NrComponents),
554		conjunct_predicates_with_pos_info(List,Res).
555
556		conjunct_components2([],_Parameters,[],_,Nr,Nr). % :- (Parameters=[] -> true ; print(unused_existential_var(Parameters)),nl).
557		conjunct_components2([component(Pred,ComponentVars)|T],Parameters,Res,Simplify,InNr,OutNr) :-
558		augment_ids(ComponentVars,CV), % translate atomic id names into b(identifier(...
559		tools:list_intersection(CV,Parameters,ExistParas), % TO DO: use ordsets
560		(Simplify=true
561		-> create_and_simplify_exists(ExistParas,Pred,EP) % no use in recursively calling construct_optimized_exists
562		; Simplify= no_cleanup_and_simplify
563		-> create_exists(ExistParas,Pred,EP0), % avoid loops when called from ast_cleanup
564		get_texpr_info(EP0,AllInfos0),
565		(nonmember(nodeid(_),AllInfos0),ExistParas=[Par1|_]
566		-> get_texpr_info(Par1,AllInfos1),extract_pos_infos(AllInfos1,PIs) % try and get position from ids
567		; PIs=[]), % we already have a position info
568		add_texpr_infos(EP0,[partitioned_exists|PIs],EP) % add ,removed_typing ??
569		; create_unsimplified_exists(ExistParas,Pred,EP)
570		),
571		(EP=b(truth,pred,[]) % or should we allow _ for Info field ??
572		-> Res=TRes
573		; Res=[EP|TRes]),
574		In1 is InNr+1,
575		conjunct_components2(T,Parameters,TRes,Simplify,In1,OutNr).
576
577
578		% translate a list of atomic ides into ids with the b/3 wrapper
579		augment_ids([],[]).
580		augment_ids([ID|T],[b(identifier(ID),_,_)|TT]) :- augment_ids(T,TT).
581
582		% extract and inline simple equalities to remove quantified variables; useful for exists and forall
583		% TO DO: move to b_quantifier_optimizations.pl or similar
584		extract_equalities_in_quantifier(Parameters,Pred, ReducedParas,OutPred) :-
585		extract_equalities2(Pred,Parameters,ReducedParas,NewPred,[],Subst),
586		%sort(Subst,SortedSubst),
587		%print(extracted(Subst)),nl,
588		apply_subst(Subst,NewPred,OutPred).
589		% apply equality inside expressions: note: this may duplicate expressions !
590		% However, it also works if the equalities contain parameters
591
592		:- use_module(bsyntaxtree,[is_equality/3]).
593
594		extract_equalities2(b(conjunct(A,B),pred,Info),Ids,RemIds,Res) --> !,
595		{Res=b(conjunct(PA,PB),pred,Info)},
596		extract_equalities2(A, Ids,RemIds1,PA),
597		extract_equalities2(B,RemIds1,RemIds,PB).
598		extract_equalities2(TEqual,Ids,RemIds,NewPred,InSubst,OutSubst) :-
599		is_equality(TEqual,ID,E),
600		% TODO: we could try and split equalities if possible; usually this is done by ast_cleanup though?
601		%(bsyntaxtree:split_equality(TEqual,A,B) -> nl,print('COULD BE SPLIT: '),translate:print_bexpr(TEqual),nl ; true),
602		same_id_is_member(ID,Ids,SID,RemIds),
603		%\+ occurs_in_expr(SID,E), % not cyclic; we check it again after applyng InSubst to E below
604		\+ in_subst_dom(SID,InSubst), % ensure we don't already have an equation for the same ID
605		compose_with_subst(InSubst,SID,E,OutSubst), % we can compose with existing substitution without occurs-check problem
606		always_well_defined_or_disprover_mode(E), % otherwise we may move evaluation of E forward !
607		!,
608		NewPred=b(truth,pred,[]).
609		extract_equalities2(X,Ids,Ids,X) --> [].
610
611
612
613		% compose a new binding Var/Expr with existing substitution Subst; where Subst was not yet applied to Expr
614		compose_with_subst(Subst,Var,Expr,[Var/NewExpr|ModSubst]) :-
615		apply_subst(Subst,Expr,NewExpr),
616		\+ occurs_in_expr(Var,NewExpr), % otherwise cyclic
617		apply_binding_to_substitution(Subst,Var,NewExpr,ModSubst).
618		apply_binding_to_substitution([],_,_,[]).
619		apply_binding_to_substitution([TV/TE|T],Var,Expr,[TV/TE2|NT]) :-
620		\+ occurs_in_expr(TV,Expr), % otherwise we get a cyclic substitution --> fail
621		replace_id_by_expr(TE,Var,Expr,TE2),
622		apply_binding_to_substitution(T,Var,Expr,NT).
623
624		apply_subst([],X,X).
625		apply_subst([Var/Expr|T],E,NewE) :-
626		(replace_id_by_expr(E,Var,Expr,E2) % replace identifier Var by expression Expr
627		-> %apply_to_tail(T,Var,Expr,NT), % apply binding to tail of substitution
628		apply_subst(T,E2,NewE)
629		; add_internal_error('Call failed: ',apply_subst([Var/Expr|T],E,NewE)),NewE=E).
630
631
632		in_subst_dom(X,[I/_|T]) :- (X=I -> true ; in_subst_dom(X,T)).
633
634		same_id_is_member(X,[H|T],SID,Rest) :-
635		(same_id(X,H,SID) -> Rest=T ; Rest=[H|TR],same_id_is_member(X,T,SID,TR)).
636
637		% TO DO: investigate what is the exact difference with create_exists_opt; partition into components is only done by construct_optimized_exists/3
638		create_and_simplify_exists(Paras,Pred,ResultingPred) :-
639		extract_equalities_in_quantifier(Paras,Pred,NewParas,NewPred),
640		create_and_simplify_exists2(NewParas,NewPred,ResultingPred).
641
642		%:- use_module(b_interpreter_check,[arithmetic_op/4]). % TODO REFACTOR and move this and code below to separate module
643		create_and_simplify_exists2([],Pred,R) :- !,R=Pred.
644		% simplify #ID.(ID:E1 & ID:E2) <=> E1 /\ E2 /= {} , etc... now done in ast_cleanup
645		% simplify #ID.(ID/:E) <=> E /= FullType also done in ast_cleanup
646		% simplify #SID.(SID > Expr) <=> truth now done in ast_cleanup
647		create_and_simplify_exists2(Parameters,Body,Res) :- create_unsimplified_exists(Parameters,Body,Res).
648		% TO DO: treat nested exists
649
650
651
652		:- use_module(b_ast_cleanup,[clean_up_pred/3]).
653		:- use_module(bsyntaxtree,[add_texpr_info_if_new/3]).
654		create_unsimplified_exists(Parameters,Body,Res) :-
655		maplist(mark_generated_exists,Parameters,Para2), % mark that this is an artificially constructed; we now mark the exists
656		create_exists(Para2,Body,Res1),
657		add_texpr_info_if_new(Res1,removed_typing,Res2), % unconditionally add this info, avoid generating warnings in exists_body_warning, see test 625
658		% and avoid useless_let_message
659		% previously removed_typing was only added for disjuncts or implications
660		clean_up_pred(Res2,[],Res). % also computes used_ids,
661		% and performs some existential quantifier optimisations like replace_exists_by_not_empty
662
663		mark_generated_exists(TID1,TID2) :- add_texpr_info_if_new(TID1,generated_exists_parameter,TID2).