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