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 | | |