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