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 |