1		% (c) 20019-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_enumeration_order_analysis, [find_do_not_enumerate_variables/4]).
6
7		:- use_module(module_information,[module_info/2]).
8		:- module_info(group,typechecker).
9		:- module_info(description,'This module computes DO_NOT_ENUMERATE variables.').
10
11		:- use_module(error_manager).
12		:- use_module(debug).
13		:- use_module(self_check).
14		:- use_module(bsyntaxtree).
15
16		:- use_module(library(lists)).
17		:- use_module(library(ordsets)).
18
19		:- use_module(library(ugraphs),[vertices_edges_to_ugraph/3 %, top_sort/2
20		]).
21		:- use_module(tools,[top_sort/3]).
22
23
24		% try and detect variables which do not have to be enumerated:
25		% Example: {x,y,z|z:1..10 & y=z*z & #v.(v:{0,1} & x=y+v)}
26		% Here we want to annotate x and y as DO_NOT_ENUMERATE: y can be computed from z, x can be computed from y and v
27		% Example 2: f<:d & a: 1..100 & b=a+1 & c<:0..b & d<:c & res=b+b
28		% Here a has to be enumerated, b,res do not have to be enumerated, and c,d,f can be delayed in order
29		% VariablesToAnnotate: variables which can be annotated with DO_NOT_ENUMERATE; they should need no enumeration at all
30		% VariablesToDelay: variables whose enumeration can be delayed; they are not used to constrain solutions,...
31		find_do_not_enumerate_variables(TIds,Body,VariablesToAnnotate,VariablesToDelayInOrderOfDelaying) :-
32		TIds = [_,_|_], % we have at least two identifiers to enumerate
33		get_texpr_ids(TIds,Ids),sort(Ids,SIds),
34		% format('Detecting lambda_result / DO_NOT_ENUMERATE ~w : ',[SIds]),translate:print_bexpr(b(comprehension_set(TIds,Body),any,[])),nl,
35		recursive_conjunction_to_list(Body,SIds,LBody),
36		%translate:l_print_bexpr_or_subst(LBody),nl,
37		% first find equalities of the form ID = Expr(UsedIds) with ID not in UsedIds
38		find_lambda_equalities(LBody,SIds,[],Equalities,Rest),
39		nontrivial(Equalities),
40		% find the identifiers used in the the rest predicate
41		% any variable used in the rest cannot be marked as DO_NOT_ENUMERATE
42		find_identifier_uses_l(Rest,[],SortedRestIds),
43		%format('Detecting lambda result over ~w with rest ids = ~w~n',[SIds,SortedRestIds]),
44		remove_illegal_equalities(Equalities,SortedRestIds,RemainingEqualities,ResultUsedIds),
45		nontrivial(RemainingEqualities),
46		findall(Vertice,member(propagator(_,Vertice,_,_),RemainingEqualities),Vs),
47		sort(Vs,SortedVs),
48		findall(Vertice,member(propagator('in-equality',Vertice,_,_),RemainingEqualities),NEqVs),
49		sort(NEqVs,SortedNEqVs), % variables which are not defined by equalities; i.e., may have more than one solution and still require enumeration
50		debug_format(4,'Enumeration analysis: Topological sorting of Vertices = ~w (non-det: ~w), rest ids=~w~n',
51		[SortedVs,SortedNEqVs,ResultUsedIds]),
52		findall(V-W,(member(V,SortedVs),
53		member(propagator(_,W,UsedIds,_),RemainingEqualities),
54		member(V,UsedIds)), Edges),
55		%format('Edges = ~w~n',[Edges]),
56		vertices_edges_to_ugraph(SortedVs,Edges,Graph),
57		topological_sorting(Graph,OrderedVertices),
58		OrderedVertices \= ['_lambda_result_'],
59		!,
60		sort(OrderedVertices,SOV), % vertices were sorted according to enumeration order
61		ord_intersection(SOV,SIds,SOV2), % retain only those ids which are freshly quantified for annotation
62		ord_intersection(SOV2,SortedNEqVs,VariablesToDelay), % Variables which should be delayed; but which still have multiple solutions
63		include(is_ord_mem(VariablesToDelay),OrderedVertices,VariablesToDelayInOrderOfDelaying),
64		ord_subtract(SOV2,VariablesToDelay,VariablesToAnnotate). % Variables which need no enumeration at all
65		find_do_not_enumerate_variables(_,_,[],[]). % return empty list of variables to annotate
66
67		is_ord_mem(SortedIds,Id) :- ord_member(Id,SortedIds).
68
69		nontrivial(Equalities) :-
70		Equalities \= [],
71		Equalities \= [propagator(equality,'_lambda_result_',_,_)].
72		%(member(propagator(equality,_,_,_),Equalities) -> true). % currently we only perform DO_NOT_ENUMERATE analysis
73
74		:- use_module(tools_printing,[format_with_colour_nl/4]).
75		topological_sorting(Graph,OrderedVertices) :-
76		top_sort(Graph,OrderedVertices,UnsortedNr),
77		% allow cycles but do only return the vertices that can be topologically sorted
78		% {x,y,z|z:1..10 & x=z+1 & y=x+1 & x=y-1} -> cycle over x and y
79		% {x,y,r,z|z:1..10 & x=z+1 & y=x+1 & x=y-1 & r=z*z} -> cycle over x and y, but r can be annotated
80		% see also test 1824
81		!,
82		debug_format(4,'Enumeration analysis: Topological Sorting successful = ~w (unsorted due to cycles: ~w)~n',[OrderedVertices,UnsortedNr]).
83		topological_sorting(Graph,_) :-
84		format_with_colour_nl(user_output,[red,bold],'Topological sorting failed for ~w~n',[Graph]),
85		fail.
86
87		% detect assignments of the Form ID = Expr, where ID does not occur in Expr and occurs in SIds
88		is_lambda_equality(_SIds,Equality,ID,UsedIDs) :-
89	?	identifier_equality(Equality,ID,TExpr),
90		%ID \= '_lambda_result_', % include as equality, IDs in TExpr should not count
91		%ord_member(ID,SIds), % if we find lambda equalities for other identifiers not in SIds it is useful to consider them too
92		% Example: {x,y,z|z:1..10 & #(w,v).(x=z+z &w:1..9 & v=card({x,x+x,w}) & y=v+v )}
93		% When analyzing #(w,v) it is also useful to consider the equalities over x and y in the process; otherwise we are not able to detect that v should not be enumerated
94		% example is also identifier NV in operation caval__rule__1__compute in private_examples/ClearSy/2019_Nov/rule_perf4
95		find_identifier_uses(TExpr,[],UsedIDs),
96		\+ ord_member(ID,UsedIDs).
97
98		:- use_module(bsyntaxtree,[is_equality/3]).
99		identifier_equality(b(not_equal(LHS,RHS),pred,_),Id,EqTerm) :- !,
100		% detect boolean inequalities x/=y : ProB will deterministically set the value of x (TRUE/FALSE) when y is known
101		get_texpr_type(LHS,boolean), % type has exactly two values
102		( get_texpr_id(LHS,Id), EqTerm = RHS
103		; get_texpr_id(RHS,Id), EqTerm = LHS).
104		identifier_equality(TExpr,Id,EqTerm) :- is_equality(TExpr,LHS,RHS),
105		( get_texpr_id(LHS,Id), EqTerm = RHS
106		; get_texpr_id(RHS,Id), EqTerm = LHS).
107
108
109		:- use_module(bsyntaxtree, [get_negated_operator_expr/2]).
110
111		% TO DO: also detect other predicates where there is always a solution
112		% Note: will require adapting sort_typed_values
113		% example tf : domain --> ROUTES & tf <: rtbl & OCC1 <: domain & tf[OCC1]<: frm1 & A : OCC1 & A|->R5 /: tf
114		% for public_examples/EventBPrologPackages/Abrial_Train_Ch17/Train_1_beebook_tlc.mch
115		always_satisfiable(b(Pred,pred,_),ID,UsedIDs) :-
116	?	always_satisfiable_aux(Pred,TID,TExprs),
117		get_texpr_id(TID,ID),
118		find_identifier_uses_l(TExprs,[],UsedIDs),
119		\+ ord_member(ID,UsedIDs).
120		always_satisfiable_aux(subset(E,TExpr),TID,[TExpr|Other]) :-
121	?	allows_empty_sol(E,TID,Other). % Solution always E={}
122		always_satisfiable_aux(subset(TExpr,TID),TID,[TExpr]). % Solution TID=TExpr
123		always_satisfiable_aux(not_subset(TExpr,E),TID,[TExpr|Other]) :-
124		allows_empty_sol(E,TID,Other). % Solution always E={}
125		always_satisfiable_aux(not_member(TExpr,E),TID,[TExpr|Other]) :-
126	?	allows_empty_sol(E,TID,Other). % Solution always E={}
127		always_satisfiable_aux(member(TExpr,TID),TID,[TExpr]). % Solution TID={TExpr}
128		always_satisfiable_aux(less(TID,TExpr),TID,[TExpr]).
129		always_satisfiable_aux(less(TExpr,TID),TID,[TExpr]).
130		always_satisfiable_aux(greater(TID,TExpr),TID,[TExpr]).
131		always_satisfiable_aux(greater(TExpr,TID),TID,[TExpr]).
132		always_satisfiable_aux(less_equal(TID,TExpr),TID,[TExpr]).
133		always_satisfiable_aux(less_equal(TExpr,TID),TID,[TExpr]).
134		always_satisfiable_aux(greater_equal(TID,TExpr),TID,[TExpr]).
135		always_satisfiable_aux(greater_equal(TExpr,TID),TID,[TExpr]).
136		always_satisfiable_aux(not_equal(TID,TExpr),TID,[TExpr]) :-
137		expr_type_allows_at_least_two_values(TID). % then we not_equal can be satisfied
138		always_satisfiable_aux(not_equal(TExpr,TID),TID,[TExpr]) :- expr_type_allows_at_least_two_values(TID).
139		always_satisfiable_aux(negation(TExpr),TID,Other) :- get_negated_operator_expr(TExpr,NegExpr),
140		always_satisfiable_aux(NegExpr,TID,Other).
141		% TODO: other constraints which can always be satisfied
142		% less_equal_real, less_real, subset_strict, not_subset_strict
143
144		allows_empty_sol(TID,TID,[]). % Solution: TID={}
145		allows_empty_sol(b(E,_,_),TID,Other) :- allows_empty_sol_aux(E,TID,Other).
146		allows_empty_sol_aux(image(TID,Other),TID,[Other]). % Solution: TID[Other]={} --> TID={}
147		allows_empty_sol_aux(image(Other,TID),TID,[Other]). % Solution: Other[TID]={} --> TID={}
148		allows_empty_sol_aux(intersection(TID,Other),TID,[Other]). % Solution: TID={}
149		allows_empty_sol_aux(intersection(Other,TID),TID,[Other]). % Solution: TID={}
150		allows_empty_sol_aux(set_subtraction(TID,Other),TID,[Other]). % Solution: TID={}
151		allows_empty_sol_aux(set_subtraction(Other,TID),TID,[Other]). % Solution: TID=Other
152
153		:- use_module(typing_tools,[type_has_at_least_two_elements/1]).
154		expr_type_allows_at_least_two_values(b(_,Type,_)) :- type_has_at_least_two_elements(Type).
155		%expr_type_allows_at_least_one_value(b(_,Type,_)) :- non_empty_type(Type).
156
157		% separate predicates into lambda equality candidates ID = Expr and other predicates
158		% find_lambda_equalities(ListOfPreds,QuantifiedIDs,LambdaEqualities,ListOfRest)
159		find_lambda_equalities([],_SIds,_,[],[]).
160		find_lambda_equalities([TPred|Rest],SIds,EqIds,A,B) :-
161	?	(is_lambda_equality(SIds,TPred,ID,UsedIDs),
162		ord_nonmember(ID,EqIds)
163		-> A=[propagator(equality,ID,UsedIDs,TPred)|AR], B=BR,
164		ord_add_element(EqIds,ID,EqIds2)
165		%, format('Equality ~w = Expr(~w)~n',[ID,UsedIDs])
166		; pred_can_be_ignored(TPred)
167		-> A=AR, B=BR, EqIds2=EqIds
168	?	; always_satisfiable(TPred,ID,UsedIDs), % only add if no other constraint already added!
169		ord_nonmember(ID,EqIds) % no guaranteed that together with other constraints it is still always satisfiable
170		-> A=[propagator('in-equality',ID,UsedIDs,TPred)|AR], B=BR,
171		ord_add_element(EqIds,ID,EqIds2)
172		%, format('InEquality ~w = Expr(~w) :: ~w~n',[ID,UsedIDs,EqIds])
173		; A=AR, B=[TPred|BR], EqIds2=EqIds),
174		find_lambda_equalities(Rest,SIds,EqIds2,AR,BR).
175
176		% predicate can be safely ignored for enumeration order analysis:
177		pred_can_be_ignored(b(E,_,_)) :- pred_can_be_ignored_aux(E).
178		pred_can_be_ignored_aux(external_pred_call(EP,_)) :- ext_pred_can_be_ignored(EP).
179		pred_can_be_ignored_aux(external_function_call(EP,_)) :- ext_pred_can_be_ignored(EP).
180		pred_can_be_ignored_aux(equal(A,B)) :-
181		( bool_true(B) -> pred_can_be_ignored(A) % also deal with observe(a)=TRUE, e.g., in REPL
182		; bool_true(A) -> pred_can_be_ignored(B)).
183		ext_pred_can_be_ignored('DO_NOT_ENUMERATE').
184		ext_pred_can_be_ignored('ENUMERATE').
185		ext_pred_can_be_ignored('FORCE').
186		ext_pred_can_be_ignored('printf'). % TO DO: debugging_only fact in external_functions
187		ext_pred_can_be_ignored('fprintf').
188		ext_pred_can_be_ignored('printf1').
189		ext_pred_can_be_ignored('printf_opt_trace').
190		ext_pred_can_be_ignored('iprintf').
191		ext_pred_can_be_ignored('printf_two').
192		ext_pred_can_be_ignored('tprintf').
193		ext_pred_can_be_ignored('printf_nonvar').
194		ext_pred_can_be_ignored('observe').
195		ext_pred_can_be_ignored('observe_silent').
196		ext_pred_can_be_ignored('observe_indent').
197		ext_pred_can_be_ignored('tobserve').
198		ext_pred_can_be_ignored('observe_fun').
199
200		bool_true(b(boolean_true,boolean,_)).
201
202		remove_illegal_equalities(Equalities,RestUsedIds,RemainingEqualities,ResultUsedIds) :-
203	?	select(propagator(Style,ID,UsedIDs,_),Equalities,RestEqualities),
204		ord_member(ID,RestUsedIds),
205		debug_format(5,'Enumeration analysis: Removing ~w over ~w, id used in rest ~w~n',[Style,ID,RestUsedIds]),
206		!,
207		ord_add_element(UsedIDs,ID,UsedIDs2),
208		ord_union(RestUsedIds,UsedIDs2,NewRestUsedIds),
209		remove_illegal_equalities(RestEqualities,NewRestUsedIds,RemainingEqualities,ResultUsedIds).
210		remove_illegal_equalities(Eq,Used,Eq,Used).
211
212		:- use_module(bsyntaxtree,[is_a_conjunct_or_neg_disj/3]).
213
214		% a version of conjunction to list which lifts existential quantifier bodies to the top-level
215		recursive_conjunction_to_list(C,BoundIds,L) :- var(C),!,
216		add_error_fail(conjunction_to_list,'Internal error: var :',conjunction_to_list(C,BoundIds,L)).
217		recursive_conjunction_to_list(C,BoundIds,List) :-
218		rec_conjunction_to_list2(C,BoundIds,List,[]).
219		rec_conjunction_to_list2(X,BoundIds,I,O) :-
220		is_a_conjunct_or_neg_disj(X,LHS,RHS),!,
221		rec_conjunction_to_list2(LHS,BoundIds,I,Inter),
222		rec_conjunction_to_list2(RHS,BoundIds,Inter,O).
223		rec_conjunction_to_list2(X,BoundIds,I,O) :- X=b(E,_,_),
224		( E = truth -> I=O
225		; E = exists(Ids,Body),
226		check_clash(Ids,BoundIds,NewBoundIds)
227		-> rec_conjunction_to_list2(Body,NewBoundIds,I,O)
228		; E = let_predicate(Ids,Exps,Body),
229		check_clash(Ids,BoundIds,NewBoundIds) -> % ditto
230		I = [b(let_predicate(Ids,Exps,b(truth,pred,[])),pred,[]) | Inter],
231		rec_conjunction_to_list2(Body,NewBoundIds,Inter,O)
232		; I = [X|O]).
233
234
235		:- use_module(performance_messages,[perf_format/2]).
236		% check whether the new identifiers clash
237		% Without this check we can get errors: See test 983, 1380 prop_COMPUTE_5, esatrack (detected by check_typed_ids in bsyntaxtree.pl)
238		% TO DO: we could rename the identifiers for the analysis; but complex and is it worth it?
239		check_clash(TIds,BoundIds,NewBoundIds) :- def_get_texpr_ids(TIds,Ids),
240		sort(Ids,SIds),
241		(ord_intersection(SIds,BoundIds,Clash), Clash \= []
242		-> perf_format('Not expanding quantifier for enumeration analysis due to clash with ~w~n',[Clash]),
243		fail
244		; ord_union(SIds,BoundIds,NewBoundIds)). % we could use ord_disjoint_union
245
246		% tests were detection works: 790, 799, 982, 1302, 1303, 1380, 1394, 1492, 1751
247		% 1751 slightly slower
248		% 1307 639
249		% 1935, 1936, 1946, 1950, 1981, 1983
250
251		% TO DO:
252		% can the analysis be counter-productive??
253		% what about {x | #v.(v:1..1000000 & x = bool(v=0))} in CLPFD FALSE mode
254		% here {x | (x=TRUE or x=FALSE) & #v.(v:1..1000000 & x = bool(v=0))} is faster 2 vs 3.5 seconds
255		%
256		% more refined analysis, to detect issue in perf_3264/rule_186.mch
257		% block:dom(ic___OPS_SDS_3264_OTHER_DP_IN_BLOCK |> {FALSE}) is enumerated before
258		% signal : ran(SORT(dom(ic___OPS_SDS_3264_BBS))/|\186)
259		% bad because from signal we can derive block, from the predicate
260		% block : ic___OPS_SDS_3264_BBS(signal)
261
262		% look at do_not_enumerate_binary_boolean_operator in kernel_propagation
263
264
265