| 1 | | % (c) 2013-2019 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_expression_sharing, |
| 6 | | [ apply_expression_sharing_to_machine/2 |
| 7 | | , create_initial_expression_cache/1 |
| 8 | | , find_common_subexpressions/4 |
| 9 | | , cse_optimize_predicate/2 |
| 10 | | , cse_optimize_substitution/2 |
| 11 | | , expand_cse_lazy_lets/2 ,expand_cse_lazy_lets_if_cse_enabled/2 |
| 12 | | , is_lazy_let_identifier/1 |
| 13 | | ]). |
| 14 | | |
| 15 | | :- use_module(library(lists)). |
| 16 | | :- use_module(library(ordsets)). |
| 17 | | :- use_module(library(avl)). |
| 18 | | |
| 19 | | :- use_module(tools). |
| 20 | | :- use_module(self_check). |
| 21 | | :- use_module(error_manager). |
| 22 | | :- use_module(debug). |
| 23 | | |
| 24 | | :- use_module(bsyntaxtree). |
| 25 | | :- use_module(bmachine_structure). |
| 26 | | |
| 27 | | :- use_module(preferences,[get_preference/2]). |
| 28 | | |
| 29 | | expression_sharing_enabled :- |
| 30 | | get_preference(use_common_subexpression_elimination,true). |
| 31 | | |
| 32 | | create_subcache(Id,cache(Id,Avl)) :- empty_avl(Avl). |
| 33 | | |
| 34 | | create_initial_expression_cache(A) :- |
| 35 | | expression_sharing_enabled,!, |
| 36 | | A=[Cache],create_subcache(top,Cache). |
| 37 | | create_initial_expression_cache(disabled). |
| 38 | | |
| 39 | | |
| 40 | | apply_expression_sharing_to_machine(InMachine,OutMachine) :- |
| 41 | | change_sections(InMachine,InExprs,OutExprs,OutMachine), |
| 42 | | create_stores(0,EmptyStores), |
| 43 | | remove_implicit_negation_l(InExprs,NormedExprs), |
| 44 | | find_common_subexpressions_l(NormedExprs,EmptyStores,true,machine,1,OutExprs,Stores,_Stripped,_UsedIds,_UsedCSEIds), |
| 45 | | ground_reference_counters(Stores),!. |
| 46 | | |
| 47 | | change_sections(InMachine,InExprs,OutExprs,OutMachine) :- |
| 48 | | change_section2([constraints,properties,invariant, |
| 49 | | assertions,operation_bodies], |
| 50 | | InMachine,InExprs,OutExprs,OutMachine). |
| 51 | | change_section2([],Machine,[],[],Machine). |
| 52 | | change_section2([Sec|Rest],InMachine,InExprs,OutExprs,OutMachine) :- |
| 53 | | select_section_texprs(Sec,LInExprs,LOutExprs,InMachine,InterMachine), |
| 54 | | append(LInExprs,RInExprs,InExprs), |
| 55 | | append(LOutExprs,ROutExprs,OutExprs), |
| 56 | | change_section2(Rest,InterMachine,RInExprs,ROutExprs,OutMachine). |
| 57 | | |
| 58 | | |
| 59 | | |
| 60 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 61 | | |
| 62 | | :- use_module(bsyntaxtree). |
| 63 | | |
| 64 | | % TESTS: x+y >100 & x+y <99 now fails deterministically in REPL with CSE |
| 65 | | |
| 66 | | % (x+y)+(x+y)=(x+y) |
| 67 | | |
| 68 | | % Note: we should detect if we are at the invariant level before calling cse_optimize_predicate: do not mess up Rodin rodinpos proof information or syntactically_relevance info |
| 69 | | |
| 70 | | % new predicate to optimize an operation body; not yet used |
| 71 | | :- public cse_optimize_operation/1. |
| 72 | | :- use_module(bmachine,[b_top_level_operation/1,b_get_machine_operation/4]). |
| 73 | | cse_optimize_operation(OpName) :- |
| 74 | | b_top_level_operation(OpName), |
| 75 | | b_get_machine_operation(OpName,_Results,_Parameters,Body), |
| 76 | | print(optimizing(OpName)),nl, |
| 77 | | cse_optimize_substitution(Body,_Res). |
| 78 | | |
| 79 | | % no difference thus far with cse_optimize_predicate |
| 80 | | cse_optimize_substitution(Subst,Res) :- cse_optimize_predicate(Subst,Res), |
| 81 | | nl,print('FINISHED CSE: '),nl, translate:print_subst(Res),nl. |
| 82 | | |
| 83 | ? | cse_optimize_predicate(Pred,Res) :- already_cse_optimized(Pred), |
| 84 | | !, |
| 85 | | Res=Pred. |
| 86 | | cse_optimize_predicate(Pred,Res) :- |
| 87 | | cse_print_check('Running Common Sub Expressions (CSE) Optimization on ', Pred), |
| 88 | | expand_cse_lazy_lets(Pred,ExpandedPred), % TO DO: see if we can do this more efficiently; do we need it at all ?? |
| 89 | | cse_print_check('Expanded Expression: ', ExpandedPred), |
| 90 | | % Note: we can still have unexpanded lazy-lets hanging around in ExpandedPred from outer scopes |
| 91 | ? | find_maximum_lazy_let_id(ExpandedPred,MaxID), % find maximum ID |
| 92 | | StartNr is MaxID+1, % we will start numbering from there to avoid clashes with existing lazy-lets |
| 93 | ? | find_common_subexpressions(ExpandedPred,StartNr,true,R,_Refs), |
| 94 | | cse_print_check('Found common sub expressions: ',R), |
| 95 | | |
| 96 | | % print('Common: '),nl, translate:nested_print_bexpr_or_subst(R),nl,nl,nl, |
| 97 | | bup_init_acc(InitialAcc), |
| 98 | | reset_let_dependency_info, |
| 99 | | transform_bexpr_with_bup_accs(b_expression_sharing:bup_insert_lazy_lookups,R,R2,InitialAcc,_BUPAcc), |
| 100 | | %portray_avl(BUPAcc),nl, |
| 101 | | %print_bexpr_or_subst(R2),nl,nl, |
| 102 | | % tools_printing:trace_print(R2,6),nl,nl, |
| 103 | | empty_avl(Empty), |
| 104 | | avl_store('$maximum_unregistered_lazy_let_id',Empty,MaxID,TDAcc), |
| 105 | ? | top_down_gen_lazy_lets(R2,TDAcc,OptimizedPred), |
| 106 | | |
| 107 | | %cse_print_check('Optimized Expression Result: ',OptimizedPred), % info fields not yet set |
| 108 | | transform_bexpr(b_expression_sharing:cse_cleanup_infos,OptimizedPred,COPred), |
| 109 | | cse_print_check('Cleaned up Optimized Expression Result: ',COPred), |
| 110 | | |
| 111 | | % nl,print('FINISHED CSE: '),nl, translate:nested_print_bexpr_or_subst(COPred),nl, %portray_avl(LastAcc),nl,nl, |
| 112 | | !, |
| 113 | | mark_as_optimized(COPred,Res). |
| 114 | | cse_optimize_predicate(P,Res) :- |
| 115 | | add_internal_error('CSE FAILED: ',cse_optimize_predicate(P,Res)), |
| 116 | | Res=P. |
| 117 | | |
| 118 | ? | already_cse_optimized(b(_E,_T,I)) :- member(cse_optimized,I). |
| 119 | | mark_as_optimized(b(E,T,I),b(E,T,I2)) :- |
| 120 | | append(I,[cse_optimized],I2). |
| 121 | | |
| 122 | | :- use_module(translate,[print_bexpr_or_subst/1]). |
| 123 | | cse_print_check(Msg,Expr) :- debug:debug_mode(on), %% |
| 124 | | !, |
| 125 | | print(Msg), print_functor(Expr), |
| 126 | | print_bexpr_or_subst(Expr), nl, |
| 127 | | cse_check_ast(Msg,Expr). |
| 128 | | cse_print_check(_,_). |
| 129 | | |
| 130 | | print_functor(b(E,T,_)) :- functor(E,F,A), format('Type: ~w, Functor: ~w/~w~n',[T,F,A]). |
| 131 | | print_functor(E) :- functor(E,F,A), format('Unwrapped, Functor: ~w/~w~n',[F,A]). |
| 132 | | |
| 133 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 134 | | :- if(environ(prob_safe_mode,true)). |
| 135 | | % check the AST (should be removed in production version of ProB): |
| 136 | | cse_check_ast(PP,Pred) :- |
| 137 | | debug_print(4,'Checking AST : '), debug_println(4,PP), % translate:print_bexpr_or_subst(Pred),nl, |
| 138 | | check_ast(true,Pred). |
| 139 | | |
| 140 | | %cse_check_ast_complete(PP,Pred) :- cse_check_ast(PP,Pred), |
| 141 | | % debug_println(20,checking_ast_complete(PP)), |
| 142 | | % % currently will generate spurious warnings when the term to start with has @identifiers introduced by LETs higher up |
| 143 | | % map_over_bexpr_top_down_acc(b_expression_sharing:check_lazy_let_vars,Pred,[]),fail. |
| 144 | | %cse_check_ast_complete(_,_). |
| 145 | | |
| 146 | | %check_lazy_let_vars(X,Acc,R) :- print(t(X,Acc,R)),nl,fail. |
| 147 | | check_lazy_let_vars(lazy_let_expr(TID,_,_),Acc,[ID|Acc]) :- !, get_texpr_id(TID,ID), |
| 148 | | (member(ID,Acc) -> print('multiply defined id: '), print(ID),nl ; true). |
| 149 | | check_lazy_let_vars(lazy_let_pred(TID,_,_),Acc,[ID|Acc]) :- !, get_texpr_id(TID,ID), |
| 150 | | (member(ID,Acc) -> print('multiply defined id: '), print(ID),nl ; true). |
| 151 | | check_lazy_let_vars(lazy_lookup_pred(ID),Acc,Acc) :- !, |
| 152 | | (member(ID,Acc) -> true ; add_internal_error('Lazy lookup pred id not defined: ',ID)). |
| 153 | | check_lazy_let_vars(lazy_lookup_expr(ID),Acc,Acc) :- !, |
| 154 | | (member(ID,Acc) -> true ; add_internal_error('Lazy lookup expr id not defined: ',ID)). |
| 155 | | %check_occurs_in_expr(ID,E) :- |
| 156 | | % (occurs_in_expr(ID,E) -> true |
| 157 | | % ; add_internal_error('Id does not occur in expression: ',ID), |
| 158 | | % print('Expression: '), translate:print_bexpr_or_subst(E),nl). |
| 159 | | :- else. |
| 160 | | cse_check_ast(_PP,_Pred). |
| 161 | | %cse_check_ast_complete(_,_). |
| 162 | | %check_occurs_in_expr(_,_). |
| 163 | | :- endif. |
| 164 | | |
| 165 | | |
| 166 | | % ----------------------------------------------- |
| 167 | | |
| 168 | | % utility to expand lazy let expressions for better CSE if repeatedly applied |
| 169 | | % Note: lazy_lookups could remain if only a partial predicate is passed |
| 170 | | |
| 171 | | expand_cse_lazy_lets_if_cse_enabled(E,EE) :- |
| 172 | | (expression_sharing_enabled -> expand_cse_lazy_lets(E,EE) ; E=EE). |
| 173 | | |
| 174 | | expand_cse_lazy_lets(Expr,ExpandedExpr) :- |
| 175 | | transform_bexpr(b_expression_sharing:expand_lazy_let,Expr,ExpandedExpr). |
| 176 | | |
| 177 | | :- public expand_lazy_let/2. |
| 178 | | %expand_lazy_let(B,R) :- tools_printing:print_term_summary(B),nl,fail. |
| 179 | ? | expand_lazy_let(b(E,Type,Info),Result) :- expand_lazy_let_aux(E,Type,Info,Result). |
| 180 | | expand_lazy_let_aux(lazy_let_expr(TID,SharedExpr,MainExpr),_,_,Result) :- |
| 181 | | get_texpr_id(TID,ID), debug_println(4,expanding(ID)), |
| 182 | | expand_lazy_lookup(ID,SharedExpr,MainExpr,Result). |
| 183 | | expand_lazy_let_aux(lazy_let_pred(TID,SharedExpr,MainExpr),_,_,Result) :- |
| 184 | | get_texpr_id(TID,ID), debug_println(4,expanding(ID)), |
| 185 | | expand_lazy_lookup(ID,SharedExpr,MainExpr,Result). |
| 186 | | expand_lazy_let_aux(lazy_let_subst(TID,SharedExpr,MainExpr),_,_,Result) :- |
| 187 | | get_texpr_id(TID,ID), debug_println(4,expanding(ID)), |
| 188 | | expand_lazy_lookup(ID,SharedExpr,MainExpr,Result). |
| 189 | | expand_lazy_let_aux(E,Type,Info,Result) :- E \= value(_), E \= integer(_), |
| 190 | | compute_static_expression(E,Val), |
| 191 | | %print(computed(E,Val)),nl, |
| 192 | | Result=b(value(Val),Type,Info). |
| 193 | | |
| 194 | | expand_lazy_lookup(ID,SharedExpr,MainExpr,Result) :- \+ atom(ID),!, |
| 195 | | add_internal_error('Illegal call: ',expand_lazy_lookup(ID,SharedExpr,MainExpr,Result)), |
| 196 | | Result=MainExpr. |
| 197 | | expand_lazy_lookup(ID,SharedExpr,MainExpr,Result) :- |
| 198 | | transform_bexpr(b_expression_sharing:replace_lazy_lookup(ID,SharedExpr),MainExpr,Result). |
| 199 | | |
| 200 | | % TO DO: unify with b_compile and ast_cleanup ! |
| 201 | | %compute_static_texpression(b(E,_,_),Result) :- compute_static_expression(E,Result). |
| 202 | | compute_static_int_texpression(b(E,_,_),Result) :- compute_static_expression(E,int(Result)). |
| 203 | | |
| 204 | | :- use_module(kernel_objects,[safe_pown/3]). |
| 205 | | compute_static_expression(add(A,B),int(Result)) :- % plus |
| 206 | | compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB), |
| 207 | | Result is IA+IB. |
| 208 | | compute_static_expression(minus(A,B),int(Result)) :- % plus |
| 209 | | compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB), |
| 210 | | Result is IA-IB. |
| 211 | | compute_static_expression(unary_minus(A),int(Result)) :- % plus |
| 212 | | compute_static_int_texpression(A,IA), |
| 213 | | Result is -IA. |
| 214 | | compute_static_expression(multiplication(A,B),int(Result)) :- |
| 215 | | compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB), |
| 216 | | Result is IA*IB. |
| 217 | | compute_static_expression(div(A,B),int(Result)) :- % TO DO: also add floored_div |
| 218 | | compute_static_int_texpression(B,IB), IB \= 0, |
| 219 | | compute_static_int_texpression(A,IA), |
| 220 | | Result is IA//IB. |
| 221 | | compute_static_expression(power_of(A,B),int(Result)) :- |
| 222 | | compute_static_int_texpression(A,IA), compute_static_int_texpression(B,IB), IB >= 0, |
| 223 | | kernel_objects:safe_pown(IA,IB,Result), number(Result). |
| 224 | | % TO DO: modulo, division, set_extension |
| 225 | | compute_static_expression(integer(I),int(I)). |
| 226 | | compute_static_expression(value(I),I). |
| 227 | | compute_static_expression(equal(A,B),I) :- compute_static_int_texpression(A,SA), compute_static_int_texpression(B,SB), |
| 228 | | (SA==SB -> I = pred_true ; I = pred_false). |
| 229 | | compute_static_expression(not_equal(A,B),I) :- compute_static_int_texpression(A,SA), compute_static_int_texpression(B,SB), |
| 230 | | (SA==SB -> I = pred_false ; I = pred_true). |
| 231 | | |
| 232 | | |
| 233 | | % ----------------------------------------------- |
| 234 | | |
| 235 | | % find maximum id used in lazy lookups; useful to generate new unused identifiers |
| 236 | | find_maximum_lazy_let_id(BExpr,MaxID) :- |
| 237 | ? | reduce_over_bexpr(b_expression_sharing:find_maximum_lazy_let_id_aux,BExpr,-1,MaxID). |
| 238 | | |
| 239 | | :- public find_maximum_lazy_let_id_aux/3. |
| 240 | | find_maximum_lazy_let_id_aux(lazy_lookup_expr(ID),MaxSoFar,NewMax) :- !, |
| 241 | | convert_atom_to_nr(ID,IDNr), |
| 242 | | (IDNr @> MaxSoFar -> NewMax=IDNr ; NewMax=MaxSoFar). |
| 243 | | find_maximum_lazy_let_id_aux(lazy_lookup_pred(ID),MaxSoFar,NewMax) :- |
| 244 | | convert_atom_to_nr(ID,IDNr), |
| 245 | | (IDNr @> MaxSoFar -> NewMax=IDNr ; NewMax=MaxSoFar). |
| 246 | | find_maximum_lazy_let_id_aux(_,V,V). |
| 247 | | |
| 248 | | % ----------------------------------------------- |
| 249 | | |
| 250 | | :- use_module(library(ordsets)). |
| 251 | | :- use_module(library(avl)). |
| 252 | | |
| 253 | | % BUP traversal; replacing shared expressions by lazy_lookup and propagate usage information upwards |
| 254 | | % no introduction of lazy_let yet |
| 255 | | % Accumulator contains list of introduced lazy_lets |
| 256 | | |
| 257 | | % example call ((x+y)+z)*(x+y)+((x+z)+y) + (x+z) = 0 |
| 258 | | |
| 259 | | % the starting accumulator for this traversal: |
| 260 | | % '$used_lazy_lookups': special key to store which lazy_lookups occur below |
| 261 | | bup_init_acc(Acc3) :- empty_avl(E), |
| 262 | | avl_store('$used_lazy_lookups',E,[]-[],Acc1), % used directly and indirectly |
| 263 | | avl_store('$identifier_uses',Acc1,[],Acc2), |
| 264 | | avl_store('$lazy_lookups_directly_used',Acc2,[],Acc3). |
| 265 | | |
| 266 | | :- public bup_insert_lazy_lookups/4. |
| 267 | | bup_insert_lazy_lookups(BE,Res,SubAccs,NewAcc) :- |
| 268 | | BE2=BE, %update_info_field(BE,BE2), % we have just treated sub-expressions and we may insert BE into avl tree of shared expressions; info field is now updated in top-down pass |
| 269 | | % combine all infos about lazy_lets from subexpressions: |
| 270 | | merge_bup_accs(SubAccs,Acc), |
| 271 | | bup_update_identifier_uses(BE,Acc,Acc1), |
| 272 | | bup_insert_lazy_lookup_if_necessary(BE2,Res,Acc1,NewAcc). |
| 273 | | |
| 274 | | % also compute used identifiers bup (ignoring @LazyLookup replacements) |
| 275 | | % a slightly rewritten version of find_typed_identifier_uses2 without recursive calls |
| 276 | | bup_update_identifier_uses(TExpr,Acc,NewAcc) :- |
| 277 | | avl_fetch('$identifier_uses',Acc,UsedIds), |
| 278 | | %bsyntaxtree:syntaxtraversion_fixed(TExpr,Expr,_QSubs,_Subs,TNames), |
| 279 | | get_texpr_expr(TExpr,Expr),safe_syntaxelement(Expr,_Subs,TNames,_,_), |
| 280 | | ( bsyntaxtree:uses_an_identifier(Expr,Id) |
| 281 | | -> ord_add_element(UsedIds,Id,New),avl_store('$identifier_uses',Acc,New,NewAcc) |
| 282 | | ; TNames=[] -> NewAcc=Acc |
| 283 | | ; get_texpr_ids(TNames,Names), % these names are introduced and no longer visible higher up |
| 284 | | sort(Names,SNames), |
| 285 | | ord_subtract(UsedIds,SNames,New), |
| 286 | | avl_store('$identifier_uses',Acc,New,Acc1), |
| 287 | | % now invalidate all lazy_lookups which use an introduced variable name in SNames |
| 288 | | avl_fetch('$used_lazy_lookups',Acc1,All-Intro), |
| 289 | | exclude(filter_lazy_lookup(SNames),All,FAll), |
| 290 | | exclude(filter_lazy_lookup(SNames),Intro,FIntro), |
| 291 | | avl_store('$used_lazy_lookups',Acc1,FAll-FIntro,Acc2), |
| 292 | | avl_fetch('$lazy_lookups_directly_used',Acc2,Direct), |
| 293 | | exclude(filter_lazy_lookup(SNames),Direct,FDirect), |
| 294 | | avl_store('$lazy_lookups_directly_used',Acc2,FDirect,NewAcc) |
| 295 | | %,print(filter(SNames,Intro,FIntro)),nl |
| 296 | | ). |
| 297 | | |
| 298 | | % detect which lazy lookups are no longer valid higher up the AST |
| 299 | | filter_lazy_lookup(SortedNames,LazyLookupID) :- |
| 300 | | lazy_let_to_be_introduced(LazyLookupID,_,_,UsedIds,SharedExpr), |
| 301 | | (ord_intersect(SortedNames,UsedIds) % if any of the introduced names is used: filter out lazy lookup |
| 302 | | -> true |
| 303 | | ; get_texpr_info(SharedExpr,Infos), |
| 304 | | memberchk(contains_wd_condition,Infos) |
| 305 | | %,print(wd_filter(LazyLookupID)),nl, translate:print_bexpr(SharedExpr),nl |
| 306 | | ). |
| 307 | | % TO DO: also filter Expressions with WD-condition attached |
| 308 | | |
| 309 | | % merge accumulators from subexpressions: |
| 310 | | merge_bup_accs([],Res) :- bup_init_acc(Res). |
| 311 | | merge_bup_accs([H],Res) :- !, % only one accumulator/argument: remove all ids marked for introduction |
| 312 | | % they can be introduced in the level below |
| 313 | | avl_delete('$used_lazy_lookups',H,All-_Intro,Acc1), |
| 314 | | avl_store('$used_lazy_lookups',Acc1,All-[],Acc2), % set introduce field to [] |
| 315 | | Res=Acc2. |
| 316 | | merge_bup_accs([H|T],Res) :- avl_fetch('$used_lazy_lookups',H,All1-_), |
| 317 | | avl_store('$used_lazy_lookups',H,All1-[],InitAcc), % set introduction set to empty |
| 318 | | merge_bup_accs_aux(T,InitAcc,Res). |
| 319 | | merge_bup_accs_aux([],R,R). |
| 320 | | merge_bup_accs_aux([H|T],A,R) :- combine_acc(H,A,A2), merge_bup_accs_aux(T,A2,R). |
| 321 | | |
| 322 | | |
| 323 | | combine_acc(Acc1,Acc2,NewAcc) :- |
| 324 | | avl_to_list(Acc1,Acc1List), |
| 325 | | empty_avl(Empty), |
| 326 | | combine_acc_aux(Acc1List,Acc2,Empty,NewAcc). |
| 327 | | |
| 328 | | combine_acc_aux([],_Acc2,Res,Res). |
| 329 | | combine_acc_aux([Field-Value1|T],Acc2,RAcc,Res) :- |
| 330 | | avl_delete(Field,Acc2,Value2,Acc3), |
| 331 | | (field_combinator(Field,Value1,Value2,NewValue) |
| 332 | | -> avl_store(Field,RAcc,NewValue,RAcc2) |
| 333 | | ; RAcc2=Acc2, Acc3=Acc2), |
| 334 | | combine_acc_aux(T,Acc3,RAcc2,Res). |
| 335 | | |
| 336 | | % rules on how to combine the different fields of the accumulators: |
| 337 | | field_combinator('$identifier_uses',Used1,Used2,Used) :- ord_union(Used1,Used2,Used). |
| 338 | | field_combinator('$lazy_lookups_directly_used',Used1,Used2,Used) :- ord_union(Used1,Used2,Used). |
| 339 | | field_combinator('$used_lazy_lookups',All1-_,AccAll-AccIntro,All-Intro) :- |
| 340 | | ord_union(All1,AccAll,All), |
| 341 | | ord_intersection(All1,AccAll,I1), % an @ID that is in this branch and some other branch |
| 342 | | ord_union([I1,AccIntro],Intro). |
| 343 | | |
| 344 | | |
| 345 | | |
| 346 | | |
| 347 | | % check if we need to introduce a lazy_lookup at the current node |
| 348 | | bup_insert_lazy_lookup_if_necessary(BExpr,LAZYLOOKUP,Acc,NewAcc) :- |
| 349 | | BExpr = b(Expr,Type,Info), |
| 350 | ? | select(sharing(ID,TotalCount,_,_),Info,Info2), % this expressions is marked as being shared |
| 351 | | TotalCount > 1, % with at least two occurrences |
| 352 | | !, |
| 353 | | %cse_check_ast(avl_store(ID),BExpr), % infos only re-established in TD phase |
| 354 | | bup_update_info(Info2,Acc,Info3), |
| 355 | | (lazy_let_to_be_introduced(ID,UsedLL,IntroLL,_,_) |
| 356 | | -> true /* let already introduced; ensure we use same Ids/version everywhere */ |
| 357 | | ; get_used_lazy_lookups(Acc,UsedLL,IntroLL), |
| 358 | | avl_fetch('$identifier_uses',Acc,UsedIds), |
| 359 | | % nl, print(lookup(ID,UsedLL,IntroLL)),nl, translate:print_bexpr_or_subst(BExpr), % portray_avl(Acc),nl, |
| 360 | | register_let_id(ID,UsedLL,IntroLL,UsedIds,b(Expr,Type,Info3)) % store that we need to introduce a lazy_let |
| 361 | | ), |
| 362 | | (UsedLL=[] -> true |
| 363 | | ; last(UsedLL,LastLL), |
| 364 | | (ID > LastLL -> true |
| 365 | | ; format('*** LET ~w depends on later id ~w in ~w~n',[ID,LastLL,UsedLL])) |
| 366 | | ), |
| 367 | | ord_union([ID],UsedLL,NewUsedLL), |
| 368 | | ord_union([ID],IntroLL,NewIntroLL), |
| 369 | | avl_store('$lazy_lookups_directly_used',Acc,[ID],Acc1), |
| 370 | | avl_store('$used_lazy_lookups',Acc1,NewUsedLL-NewIntroLL,NewAcc), % to the outside (above) we only see usage of @ID |
| 371 | | bup_update_info(Info2,NewAcc,LazyLookupInfo), |
| 372 | | gen_lazy_lookup(Type,ID,Info2,LazyLookupInfo,LAZYLOOKUP). |
| 373 | | bup_insert_lazy_lookup_if_necessary(b(Expr,Type,Info1),b(Expr,Type,Info2),Acc,Acc) :- |
| 374 | | %nl, print('BUP: '),translate:print_bexpr_or_subst(b(Expr,Type,Info1)), portray_avl(Acc),nl, |
| 375 | | bup_update_info(Info1,Acc,Info2). |
| 376 | | |
| 377 | | bup_update_info(Info0,Acc,Info4) :- |
| 378 | | delete(Info0,sharing(_,_,_,_),Info1), |
| 379 | | delete(Info1,cse_used_ids(_),Info2), |
| 380 | | get_used_lazy_lookups(Acc,_,InterList), |
| 381 | | avl_fetch('$lazy_lookups_directly_used',Acc,DirectlyUsed), |
| 382 | | Info3=Info2, %Info3 = [cse_used_ids(DirectlyUsed)|Info2], |
| 383 | | ord_intersection(InterList,DirectlyUsed,IntroduceHere), % those not directly used will be introduced automatically inside the shared expressions |
| 384 | | (IntroduceHere=[] -> Info4=Info3 |
| 385 | | %,(DirectlyUsed=[] -> true ; print('*** WARNING: directly used not empty: '),print(DirectlyUsed),nl) |
| 386 | | ; Info4 = ['$introduce_lazy_lookups'/IntroduceHere|Info3]). % store info in node for later top-down traversal). |
| 387 | | |
| 388 | | get_used_lazy_lookups(Acc,All,Introduce) :- |
| 389 | | (avl_fetch('$used_lazy_lookups',Acc,A-I) -> All=A,Introduce=I |
| 390 | | ; add_internal_error('Failed: ',get_used_lazy_lookups(Acc,All,Introduce)), |
| 391 | | All=[], Introduce=[]). |
| 392 | | |
| 393 | | |
| 394 | | % ---------------------------------- |
| 395 | | |
| 396 | | % PHASE 2: Top-Down Phase to introduce LETs at latest possible moment: |
| 397 | | |
| 398 | | % top-down traversal to introduce lazy_lets for lazy_lookups we have introduced in bottom-up phase |
| 399 | | top_down_gen_lazy_lets(InExpr,Acc,ResExpr) :- |
| 400 | ? | top_down_gen_lazy_lets1(InExpr,Acc,IntExpr), |
| 401 | | update_info_field(IntExpr,ResExpr). % maybe we should do this only if there was a change |
| 402 | | |
| 403 | | top_down_gen_lazy_lets1(b(LazyLookup,Type,_Info),Acc,NewExpr1) :- |
| 404 | ? | directly_uses_cse_id(LazyLookup,LetID), % check if we have lazy_let_expr/_pred |
| 405 | ? | (lazy_let_to_be_introduced(LetID,UsedInside,IntroduceHere,_,SharedExpression) -> true |
| 406 | | ; avl_fetch('$maximum_unregistered_lazy_let_id',Acc,MaxId), % all ids up until MaxId come from a previous run of CSE |
| 407 | | LetID > MaxId, |
| 408 | | add_internal_error('**** Unregistered let: ',LetID),fail), |
| 409 | ? | \+ avl_fetch(lazy_let_introduced(LetID),Acc,true), |
| 410 | ? | !, |
| 411 | ? | debug_println(9,inlining_single_usage(LetID,UsedInside,IntroduceHere)), |
| 412 | ? | avl_store(lazy_let_inlined(LetID),Acc,true,Acc0), % NOT USED ! |
| 413 | ? | top_down_gen_lazy_lets(SharedExpression,Acc0,NewSharedExpression), |
| 414 | ? | top_down_gen_lazy_lets_for_list(IntroduceHere,Type,Acc0,_,NewExpr1,NewSharedExpression). |
| 415 | | top_down_gen_lazy_lets1(b(Expr,Type,Info),Acc,Res) :- |
| 416 | | %syntaxtraversion(BExpr,Expr,_,_,Subs,_TNames), |
| 417 | ? | select('$introduce_lazy_lookups'/IntroduceHere,Info,Info2), |
| 418 | | % functor(Expr,Fun,Arity),print(intro(IntroduceHere,Fun,Arity)),nl, translate:print_bexpr_or_subst(b(Expr,Type,Info)),nl, |
| 419 | ? | !, |
| 420 | | % the lazy lookups in Inter must now be introduced, if not already done so |
| 421 | ? | top_down_gen_lazy_lets_for_list(IntroduceHere,Type,Acc,NewAcc,Res,InnerRes), |
| 422 | | syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1), |
| 423 | | InnerRes=b(NewExpr1,Type,Info2), |
| 424 | | td_treat_sub_args(Subs,NewAcc,NSubs). |
| 425 | | top_down_gen_lazy_lets1(b(Expr,Type,Info),Acc,b(NewExpr1,Type,Info)) :- |
| 426 | | syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr1), |
| 427 | | td_treat_sub_args(Subs,Acc,NSubs). |
| 428 | | |
| 429 | | % treat sub-arguments of an expression for which we have introduced lets |
| 430 | | td_treat_sub_args([],_Acc,[]). |
| 431 | | td_treat_sub_args([TE|T],Acc,[NTE|NT]) :- |
| 432 | ? | (top_down_gen_lazy_lets(TE,Acc,NTE) |
| 433 | | -> true |
| 434 | | ; add_internal_error('Call failed: ',top_down_gen_lazy_lets(TE,Acc,NTE)), |
| 435 | | NTE=TE ), |
| 436 | | td_treat_sub_args(T,Acc,NT). |
| 437 | | |
| 438 | | |
| 439 | | top_down_gen_lazy_lets_for_list(IntroHere,Type,Acc,NewAcc,Res,InnerRes) :- |
| 440 | | % first collect all lazy_lets we need here: |
| 441 | | %td_collect_lazy_lets_to_introduce_here(Inter,Acc,IntroHere,[]), |
| 442 | | % now update which lazy_lets are now visible |
| 443 | ? | topsort(IntroHere,SortedIntroHere), |
| 444 | | %print(sorted_intro(IntroHere,SortedIntroHere)),nl, |
| 445 | ? | td_introduce_lazy_lets(SortedIntroHere,Type,Acc,NewAcc,Res,InnerRes). |
| 446 | | |
| 447 | | % topological sorting using a naive quadratic algorithm; TO DO: improve |
| 448 | | topsort([],[]). |
| 449 | ? | topsort([H|T],Res) :- select(X,T,TT), let_depends_upon(H,X), !,topsort([X,H|TT],Res). |
| 450 | | topsort([H|T],[H|ST]) :- topsort(T,ST). |
| 451 | | |
| 452 | | :- dynamic let_depends_upon/2, lazy_let_to_be_introduced/5. |
| 453 | | % a fact to store which let depends directly upon which other let |
| 454 | | % UsedLL: Used LazyLet @IDs, IntroduceLL: LazyLet @IDs to be introduced, UsedIds: regular identifiers referenced directly or via other lazy_lookups |
| 455 | | register_let_id(ID,UsedLL,IntroduceLL,UsedIds,SharedExpr) :- |
| 456 | | assert(lazy_let_to_be_introduced(ID,UsedLL,IntroduceLL,UsedIds,SharedExpr)), |
| 457 | | %format('LAZY LET ~w (depends on ~w) [uses ~w ids]~n',[ID,UsedLL,UsedIds]), |
| 458 | ? | member(ID2,UsedLL), |
| 459 | | assert(let_depends_upon(ID,ID2)), |
| 460 | | % now do transitive closure in one direction |
| 461 | | %let_depends_upon(ID0,ID),assert(let_depends_upon(ID0,ID2)), |
| 462 | | fail. |
| 463 | | register_let_id(ID,UsedLL,_,_,_) :- fail, |
| 464 | | % now do transitive closue in other direction |
| 465 | | member(ID2,UsedLL), |
| 466 | | let_depends_upon(ID2,ID3), |
| 467 | | assert(let_depends_upon(ID,ID3)),fail. |
| 468 | | register_let_id(_,_,_,_,_). |
| 469 | | |
| 470 | | reset_let_dependency_info :- retractall(let_depends_upon(_,_)), |
| 471 | | retractall(lazy_let_to_be_introduced(_,_,_,_,_)). |
| 472 | | |
| 473 | | |
| 474 | | % introduce lets in order |
| 475 | | td_introduce_lazy_lets([],_,Acc,Acc,R,R). |
| 476 | | td_introduce_lazy_lets([],Ty,Acc,AccR,T,RT) :- |
| 477 | | add_internal_error('Call failed: ',td_introduce_lazy_lets([],Ty,Acc,AccR,T,RT)),fail. |
| 478 | | td_introduce_lazy_lets([LetID|T],Type,Acc,Acc1,OuterTerm,InnerTerm) :- |
| 479 | ? | avl_fetch(lazy_let_introduced(LetID),Acc,true),!, |
| 480 | | %print(already_introduced(LetID)),nl, |
| 481 | ? | td_introduce_lazy_lets(T,Type,Acc,Acc1,OuterTerm,InnerTerm). |
| 482 | | td_introduce_lazy_lets([LetID|T],Type,Acc,Acc1,OuterTerm,InnerTerm) :- |
| 483 | ? | avl_store(lazy_let_introduced(LetID),Acc,true,Acc0), |
| 484 | ? | td_introduce_lazy_lets(T,Type,Acc0,Acc1,MidTerm,InnerTerm), |
| 485 | | % now introduce let for ID |
| 486 | | lazy_let_to_be_introduced(LetID,_,_,UsedIds,SharedExpression), |
| 487 | | top_down_gen_lazy_lets(SharedExpression,Acc0,NewSharedExpression), % the lazy_lets introduced inside are not visible |
| 488 | | %tools_printing:print_term_summary(gen_lazy_let(Type,LetID,NewSharedExpression,MidTerm,OuterTerm)),nl, |
| 489 | | gen_lazy_let(Type,LetID,UsedIds,NewSharedExpression,MidTerm,OuterTerm). |
| 490 | | |
| 491 | | |
| 492 | | |
| 493 | | % ----------------------------------------------- |
| 494 | | |
| 495 | | |
| 496 | | % copy position information; important e.g. for discharged checks for theorems and invariants |
| 497 | | /* |
| 498 | | copy_position_info(From,b(To,Type,Info1),b(To,Type,Info3)) :- |
| 499 | | get_texpr_pos(From,PositionInfo),!, |
| 500 | | delete(Info1,nodeid(_),Info2), |
| 501 | | Info3 = [nodeid(PositionInfo)|Info2]. |
| 502 | | copy_position_info(_,E,E). |
| 503 | | */ |
| 504 | | |
| 505 | | :- use_module(b_ast_cleanup,[recompute_used_ids_info/2]). |
| 506 | | % update info field of a typed expression after a modification of the expression |
| 507 | | update_info_field(TE,NewTE) :- |
| 508 | | update_wd_condition(TE,TE2), |
| 509 | | recompute_used_ids_info(TE2,NewTE). % inserting lazy_lookups changes used ids for exists/forall |
| 510 | | |
| 511 | | % check if we need to add contains_wd_condition info field |
| 512 | | update_wd_condition(b(E,Type,Info1),Res) :- |
| 513 | | nonmember(contains_wd_condition,Info1), % inlined update_wd_condition_info to just copy E in clause below; not sure this helps memory performance |
| 514 | ? | sub_expression_contains_wd_condition(E), |
| 515 | | !, |
| 516 | | Res = b(E,Type,[contains_wd_condition|Info1]). |
| 517 | | update_wd_condition(E,E). |
| 518 | | |
| 519 | | update_wd_condition_info(E,Info1,Info2) :- |
| 520 | | nonmember(contains_wd_condition,Info1), |
| 521 | | sub_expression_contains_wd_condition(E), |
| 522 | | !, |
| 523 | | Info2 = [contains_wd_condition|Info1]. |
| 524 | | update_wd_condition_info(_,I,I). |
| 525 | | |
| 526 | | |
| 527 | | |
| 528 | | % Remove sharing/4 info from SharedExpression + avoid reusing it for CSE if algorithm applied second time |
| 529 | | %delete_sharing_info(b(E,T,Info),b(E,T,NewInfo)) :- delete(Info,sharing(_,_,_,_),NewInfo). |
| 530 | | |
| 531 | | :- public cse_cleanup_infos/2. |
| 532 | | % Remove info that is no longer necessary once CSE has run to completion: |
| 533 | | cse_cleanup_infos(b(E,T,Info),Res) :- |
| 534 | ? | cse_cleanup_infos1(E,T,Info,Res). |
| 535 | | |
| 536 | | cse_cleanup_infos1(lazy_let_pred(ID,SharedExpr,Body),T,_,Res) :- |
| 537 | | collect_important_info(SharedExpr,Body,Info), |
| 538 | | cse_cleanup_aux(lazy_let_pred(ID,SharedExpr,Body),T,Info,Res). |
| 539 | | cse_cleanup_infos1(lazy_let_expr(ID,SharedExpr,Body),T,_,Res) :- |
| 540 | | collect_important_info(SharedExpr,Body,Info), |
| 541 | | cse_cleanup_aux(lazy_let_expr(ID,SharedExpr,Body),T,Info,Res). |
| 542 | | cse_cleanup_infos1(lazy_let_subst(ID,SharedExpr,Body),T,_,Res) :- |
| 543 | | collect_important_info(SharedExpr,Body,Info), |
| 544 | | cse_cleanup_aux(lazy_let_subst(ID,SharedExpr,Body),T,Info,Res). |
| 545 | | cse_cleanup_infos1(sequence(Seq),T,Info,Res) :- !, % re-flatten sequences that were binarized for CSE sharing analysis |
| 546 | | flatten_sequence(Seq,FSeq,WD), |
| 547 | | ((WD==contains_wd_condition, nonmember(contains_wd_condition,Info)) -> |
| 548 | | Info1 = [contains_wd_condition|Info] ; Info1=Info), |
| 549 | | cse_cleanup_aux(sequence(FSeq),T,Info1,Res). |
| 550 | | cse_cleanup_infos1(E,T,Info,Res) :- cse_cleanup_aux(E,T,Info,Res). |
| 551 | | |
| 552 | | flatten_sequence([H,b(sequence(T),subst,Info)],[H|FT],WD) :- member(cse_generated,Info), |
| 553 | | !, |
| 554 | | % check if this sequence contains a WD condition |
| 555 | | (var(WD),member(contains_wd_condition,Info) -> WD=contains_wd_condition ; true), |
| 556 | | flatten_sequence(T,FT,WD). |
| 557 | | flatten_sequence(X,X,_WD). |
| 558 | | |
| 559 | | |
| 560 | | cse_cleanup_aux(E,T,Info,b(NewE,T,NewInfo)) :- |
| 561 | | delete(Info,cse_used_ids(_),Info2), |
| 562 | | ((nonmember(contains_wd_condition,Info2), % TO DO: allow in DISPROVER_MODE |
| 563 | | post_cse_simplifier(E,SE)) -> NewE = SE, NewInfo=Info2 % Note: maybe some lets no longer necessary now |
| 564 | | ; reorder_lazy_let_expr(E,T,Info2,NewE,NewInfo) -> true |
| 565 | | ; NewE=E,NewInfo=Info2). |
| 566 | | |
| 567 | | % reorder/move lazy lets outside if this leads to better optimizations being applicable |
| 568 | | reorder_lazy_let_expr(Expr,Type,Info,NewExpr,NewInfo) :- |
| 569 | ? | reorder_argument(Expr,FunctorID,Match,TArgToReorder,OtherArgs,_), |
| 570 | | get_texpr_expr(TArgToReorder,ArgToReorder), |
| 571 | | %print(try_reorder(FunctorID,TArgToReorder)),nl, |
| 572 | | is_lazy_let(ArgToReorder,LLType,ID,ShExpr,BodyA), |
| 573 | | get_texpr_expr(BodyA,Match), |
| 574 | | print(reorder_lazy_let_expr(ID,FunctorID)),nl, |
| 575 | | !, |
| 576 | | reorder_argument(NewBinExpr,FunctorID,_,BodyA,OtherArgs,Recur), |
| 577 | | !, % FunctorID ensures only one possible solution for reorder_argument |
| 578 | | ((Recur=recur, % we may have to re-order again |
| 579 | | reorder_lazy_let_expr(NewBinExpr,Type,Info,NewBinExpr2,Info2)) |
| 580 | | -> NewInnerExpr = b(NewBinExpr2,Type,Info2) |
| 581 | | ; NewInnerExpr = b(NewBinExpr,Type,Info)), |
| 582 | | is_lazy_let(NewExpr,LLType,ID,ShExpr,NewInnerExpr), % TYPE MAY HAVE TO CHANGE for CASE ?? TO DO: Check with appropriate B Machine |
| 583 | | % copy important info from InfoA ?? |
| 584 | | update_wd_condition_info(NewExpr,Info,NewInfo). |
| 585 | | % TO DO: add more cases + what if both arguments need reordering --> fixpoint computation ? |
| 586 | | |
| 587 | | is_lazy_let(lazy_let_expr(ID,ShExpr,BodyA),lazy_let_expr,ID,ShExpr,BodyA). |
| 588 | | is_lazy_let(lazy_let_subst(ID,ShExpr,BodyA),lazy_let_subst,ID,ShExpr,BodyA). |
| 589 | | is_lazy_let(lazy_let_pred(ID,ShExpr,BodyA),lazy_let_pred,ID,ShExpr,BodyA). |
| 590 | | |
| 591 | | % reorder argument 1 (i.e., move lazy_let out) in case we match a certain pattern |
| 592 | | % reorder_argument(Expression, ID, MATCH, ARG_TO_REORDER, OtherArgs) |
| 593 | | reorder_argument(function(A,B),function_1,set_extension(_),A,B,do_not_recur). % there is optimized code: b_apply_function_set_extension |
| 594 | | reorder_argument(max(A),max,set_extension(_),A,nil,do_not_recur). % we have optimized code for min({a,b,...}) and max |
| 595 | | reorder_argument(min(A),min,set_extension(_),A,nil,do_not_recur). |
| 596 | | reorder_argument(card(A),card,set_extension(_),A,nil,do_not_recur). |
| 597 | | reorder_argument(image(A,B),image_1,closure(_),A,B,recur). |
| 598 | | reorder_argument(image(B,A),image_2,set_extension(_),A,B,recur). |
| 599 | | % avoid that Lazy Lets stand at illegal places |
| 600 | | % avoid IF THEN LET(... ELSIF P THEN ....) if_elsif term |
| 601 | | reorder_argument(if(IfList),if1,_,A,Rest,recur) :- select(A,IfList,Rest). |
| 602 | | % avoid lazy let in place of a CASE case_or term |
| 603 | | reorder_argument(case(Expr,Cases,Else),case_element,_,A,[Expr,Else|Rest],recur) :- select(A,Cases,Rest). |
| 604 | | % avoid lazy let for a select_when term: |
| 605 | | reorder_argument(select(SelWhenList),select,_,A,Rest,recur) :- select(A,SelWhenList,Rest). % SelWhenList: a list containing select_when/2 terms |
| 606 | | reorder_argument(select(SelWhenList,Else),select_else,_,A,(Rest,Else),recur) :- select(A,SelWhenList,Rest). |
| 607 | | % CSE will sometimes insert a lazy_let_subst where an if_elsif should stand; this not supported by the interpreter |
| 608 | | %reorder_argument(while(COND,TSubst,INV,VARIANT),while_subst,_,TSubst,[COND,INV,VARIANT]). % TO DO: check if lazy_let does not depend on variables modified in loop |
| 609 | | |
| 610 | | % TO DO: bring this in accordance with do_not_share_this rules: |
| 611 | | |
| 612 | | % detect certain obvious inconsistencies / tautologies introduced by CSE |
| 613 | | post_cse_simplifier(equal(A,B),truth) :- same_lazy_lookup(A,B). |
| 614 | | post_cse_simplifier(not_equal(A,B),falsity) :- same_lazy_lookup(A,B). |
| 615 | | post_cse_simplifier(greater(A,B),falsity) :- same_lazy_lookup(A,B). |
| 616 | | post_cse_simplifier(greater_equal(A,B),truth) :- same_lazy_lookup(A,B). |
| 617 | | post_cse_simplifier(less(A,B),falsity) :- same_lazy_lookup(A,B). |
| 618 | | post_cse_simplifier(less_equal(A,B),truth) :- same_lazy_lookup(A,B). |
| 619 | | post_cse_simplifier(subset(A,B),truth) :- same_lazy_lookup(A,B). |
| 620 | | post_cse_simplifier(not_subset(A,B),falsity) :- same_lazy_lookup(A,B). |
| 621 | | post_cse_simplifier(strict_subset(A,B),falsity) :- same_lazy_lookup(A,B). |
| 622 | | post_cse_simplifier(not_strict_subset(A,B),truth) :- same_lazy_lookup(A,B). |
| 623 | | |
| 624 | | /* |
| 625 | | TO DO: |
| 626 | | split up lazy_let_pred; as previously done in gen_lazy_let |
| 627 | | gen_lazy_let(pred,CSEID,_UsedIds,SharedExpr,Body,Result) :- |
| 628 | | true, % TO DO <------------- RENABLE |
| 629 | | % check if we can split off Prefix and/or Suffix of Body not using CSEID |
| 630 | | cse_split_conjunct(Body, CSEID, Prefix, MainBody, Suffix), |
| 631 | | !, |
| 632 | | print(optimizing_let_with_conjunction_body(CSEID)),nl, |
| 633 | | gen_id(CSEID,SharedExpr,ID), |
| 634 | | cse_conjunct_predicates(MainBody,NewBody), |
| 635 | | %get_texpr_info(NewBody,NewInfo), |
| 636 | | collect_important_info(SharedExpr,NewBody,NewInfo), % we could remove ID from cse_used_ids |
| 637 | | LET = b(lazy_let_pred(ID,SharedExpr,NewBody),pred,NewInfo), |
| 638 | | append(Prefix,[LET|Suffix],ConjunctionList), |
| 639 | | cse_conjunct_predicates(ConjunctionList,Result). |
| 640 | | */ |
| 641 | | |
| 642 | | same_lazy_lookup(A,B) :- get_lazy_lookup_id(A,ID), get_lazy_lookup_id(B,ID). |
| 643 | | |
| 644 | | get_lazy_lookup_id(b(E,Type,_),Type,ID) :- get_lazy_lookup_id_aux(E,ID). |
| 645 | | get_lazy_lookup_id(b(E,_,_),ID) :- get_lazy_lookup_id_aux(E,ID). |
| 646 | | get_lazy_lookup_id_aux(lazy_lookup_expr(ID),ID). |
| 647 | | get_lazy_lookup_id_aux(lazy_lookup_pred(ID),ID). |
| 648 | | % there is no lazy_lookup_subst(ID) |
| 649 | | |
| 650 | | %gen_lazy_let_with_check(Type, Identifier, UsedIds,SharedExpression, SubExpressionInsideLet, Result) :- |
| 651 | | % cse_check_ast(before_gen_lazy_let_shared,SharedExpression), |
| 652 | | % cse_check_ast(before_gen_lazy_let_body,SubExpressionInsideLet), |
| 653 | | % (gen_lazy_let(Type, Identifier, UsedIds,SharedExpression, SubExpressionInsideLet, Result) |
| 654 | | % -> cse_check_ast(gen_lazy_let,Result) |
| 655 | | % ; add_internal_error('Call failed: ',gen_lazy_let_with_check(Type, Identifier, UsedIds,SharedExpression, SubExpressionInsideLet, Result)), |
| 656 | | % fail). |
| 657 | | |
| 658 | | % TO DO: maybe check that we are not in a bad context to prevent optimized treatment (e.g. {1|->a,2|->b}(x) ), rather than delegating this to reorder lazy_let code above ? |
| 659 | | % gen_lazy_let(Type, Identifier, UsedIds,SharedExpression, SubExpressionInsideLet, Result) |
| 660 | | gen_lazy_let(pred,A,_UsedIds,SharedExpr,Body,b(R,pred,[])) :- |
| 661 | | % Info field will be set later in cse_cleanup_infos |
| 662 | | !, |
| 663 | | gen_id(A,SharedExpr,ID), debug_println(4,generating_lazy_let_pred(A,ID)), |
| 664 | | R = lazy_let_pred(ID,SharedExpr,Body). |
| 665 | | gen_lazy_let(subst,A,_UsedIds,SharedExpr,Body,b(R,subst,[])) :- |
| 666 | | !, |
| 667 | | gen_id(A,SharedExpr,ID), debug_println(4,generating_lazy_let_subst(A,ID)), |
| 668 | | R = lazy_let_subst(ID,SharedExpr,Body). |
| 669 | | gen_lazy_let(Type,A,_UsedIds,SharedExpr,C,b(lazy_let_expr(ID,SharedExpr,C),Type,[])) :- |
| 670 | | gen_id(A,SharedExpr,ID). |
| 671 | | |
| 672 | | % ---------------------- |
| 673 | | |
| 674 | | |
| 675 | | collect_important_info(SubA,SubB,Info) :- (var(SubA) ; var(SubB)), !, |
| 676 | | add_internal_error('Illegal call: ',collect_important_info(SubA,SubB,Info)),fail. |
| 677 | | collect_important_info(SubA,SubB,Info) :- |
| 678 | | extract_info(SubA,SubB,Info1), % WD info (bsyntaxtree utility) |
| 679 | | % was collect_uses_cse_id([SubA,SubB],IDS), % CSE usage info |
| 680 | | exclude(is_cse_used_ids,Info1,Info2), % is this necessary ?? |
| 681 | | Info=Info2. %Info = [cse_used_ids(IDS)|Info2]. |
| 682 | | |
| 683 | | % ---------------------- |
| 684 | | |
| 685 | | gen_lazy_lookup(pred,A,Infos,LazyLookupInfo,R) :- !, convert_to_atom(A,ID), |
| 686 | ? | (member(negated_cse,Infos) |
| 687 | | -> R = b(negation(b(lazy_lookup_pred(ID),pred,LazyLookupInfo)),pred,OuterInfos), |
| 688 | | delete(LazyLookupInfo,'$introduce_lazy_lookups'/_,OuterInfos) % we do not need to generate the lazy_lookups here; they can be created inside the negation |
| 689 | | %,print(create_neg_lookup(ID,LazyLookupInfo,OuterInfos)),nl |
| 690 | | ; R = b(lazy_lookup_pred(ID),pred,LazyLookupInfo)). |
| 691 | | gen_lazy_lookup(Type,A,_,LazyLookupInfo, |
| 692 | | b(lazy_lookup_expr(ID),Type,LazyLookupInfo)) :- convert_to_atom(A,ID). |
| 693 | | |
| 694 | | % generate atoms: many identifier treating predicates expect atoms |
| 695 | | gen_id(A,B,b(identifier(ID),Type,[])) :- get_texpr_type(B,Type),convert_to_atom(A,ID). |
| 696 | | |
| 697 | | convert_to_atom(A,ID) :- var(A),!, add_internal_error('Illegal call: ', convert_to_atom(A,ID)),fail. |
| 698 | | convert_to_atom(A,ID) :- atom(A),!, ID=A. |
| 699 | | convert_to_atom(Nr,ID) :- number_codes(Nr,C), atom_codes(ID,[64|C]). % 64 = @ |
| 700 | | |
| 701 | | convert_atom_to_nr(Atom,Nr) :- var(Atom),!, add_internal_error('Illegal call: ',convert_atom_to_nr(Atom,Nr)),fail. |
| 702 | | convert_atom_to_nr(Atom,Nr) :- atom_codes(Atom,[64|C]), number_codes(Nr,C). |
| 703 | | |
| 704 | | % check if an identifier is (potentially) a lazy_let ID |
| 705 | | is_lazy_let_identifier(Atom) :- atom(Atom), atom_codes(Atom,[64|_]). |
| 706 | | |
| 707 | | is_cse_used_ids(cse_used_ids(_)). |
| 708 | | |
| 709 | | /* |
| 710 | | collect_uses_cse_id([],[]). |
| 711 | | collect_uses_cse_id([H|T],Res) :- |
| 712 | | get_cse_used_ids_info(H,CSE),!, |
| 713 | | collect_uses_cse_id(T,CSET), |
| 714 | | ord_union(CSE,CSET,Res). |
| 715 | | |
| 716 | | uses_cse_id(ID,Expr) :- get_cse_used_ids_info(Expr,List),!, |
| 717 | | member(ID,List). |
| 718 | | uses_cse_id(_ID,Expr) :- print('Could not extract cse_used_ids info: '), print(Expr),nl, |
| 719 | | true. |
| 720 | | |
| 721 | | % CSE Identifier usage infor either form info field or from direct usage by lazy_lookups |
| 722 | | get_cse_used_ids_info(TExpr,IDList) :- get_texpr_expr(TExpr,E), |
| 723 | | directly_uses_cse_id(E,UsedID),!, |
| 724 | | IDList = [UsedID]. |
| 725 | | get_cse_used_ids_info(TExpr,IDList) :- get_texpr_info(TExpr,Info), |
| 726 | | member(cse_used_ids(IDList),Info),!. |
| 727 | | get_cse_used_ids_info(TE,L) :- print('Could not get cse_used_ids info: '), print(TE), |
| 728 | | L=[]. |
| 729 | | */ |
| 730 | | |
| 731 | | directly_uses_cse_id(E,ID) :- var(E),!, add_internal_error('Illegal call: ',directly_uses_cse_id(E,ID)),fail. |
| 732 | | directly_uses_cse_id(lazy_lookup_pred(AtomID),ID) :- convert_atom_to_nr(AtomID,ID). |
| 733 | | directly_uses_cse_id(lazy_lookup_expr(AtomID),ID) :- convert_atom_to_nr(AtomID,ID). |
| 734 | | % there is no lazy_lookup_subst |
| 735 | | |
| 736 | | :- public print_cse_id_used/1. |
| 737 | | print_cse_id_used(TypedExpr) :- get_texpr_info(TypedExpr,Info), |
| 738 | | member(cse_used_ids(L),Info),!, |
| 739 | | print(L). |
| 740 | | print_cse_id_used(_) :- print(' no cse used id info '). |
| 741 | | |
| 742 | | :- public replace_lazy_lookup/4. |
| 743 | | :- use_module(btypechecker, [unify_types_strict/2]). |
| 744 | | % TO DO: maybe remove cse_used_ids ?? |
| 745 | | %replace_lazy_lookup(_,_,T,_) :- print(T),nl,fail. |
| 746 | | replace_lazy_lookup(ID,SharedExpr,BExpr,SharedExpr) :- |
| 747 | | get_lazy_lookup_id(BExpr,Type,TID), |
| 748 | | !, |
| 749 | | TID=ID, |
| 750 | | get_texpr_type(SharedExpr,SharedType), |
| 751 | | (my_unify_types(SharedType,Type) -> true |
| 752 | | ; add_internal_error('Incompatible type: ',replace_lazy_lookup(ID,'\\='(SharedType,Type),BExpr,SharedExpr))). |
| 753 | | replace_lazy_lookup(_,_,E,Res) :- update_info_field(E,Res). % probably not necessary ?! |
| 754 | | |
| 755 | | :- if(environ(prob_safe_mode,true)). |
| 756 | | my_unify_types(T1,T2) :- (\+ ground(T1) ; \+ ground(T2)), |
| 757 | | format('*** Non-ground type unification: ~w = ~w~n~n',[T1,T2]), |
| 758 | | fail. |
| 759 | | :- endif. |
| 760 | | my_unify_types(T1,T2) :- unify_types_strict(T1,T2). |
| 761 | | |
| 762 | | % ----------------- |
| 763 | | |
| 764 | | |
| 765 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 766 | | % common subexpression detection |
| 767 | | |
| 768 | | :- assert_must_succeed( |
| 769 | | ( find_common_subexpressions(b(identifier(i),integer,[]),0,false,R), |
| 770 | | R == b(identifier(i),integer,[sharing(0,1,top,[]),cse_used_ids([])]) |
| 771 | | )). |
| 772 | | :- assert_must_succeed( |
| 773 | | ( find_common_subexpressions(b(identifier(i),integer,[]),0,true,R), |
| 774 | | R == b(identifier(i),integer,[cse_used_ids([])]) |
| 775 | | )). |
| 776 | | :- assert_must_succeed( |
| 777 | | ( I = b(identifier(i),integer,[]), |
| 778 | | O = b(identifier(i),integer,[sharing(0,2,top,[]),cse_used_ids([])]), |
| 779 | | find_common_subexpressions(b(add(I,I),integer,[]),0,false,R), |
| 780 | | R == b(add(O,O),integer,[sharing(1,1,top,[]),cse_used_ids([0])]) |
| 781 | | )). |
| 782 | | :- assert_must_succeed( |
| 783 | | ( I = b(identifier(i),integer,[]), |
| 784 | | O = b(identifier(i),integer,[cse_used_ids([])]), |
| 785 | | find_common_subexpressions(b(add(I,I),integer,[]),0,true,R), |
| 786 | | R == b(add(O,O),integer,[sharing(0,1,top,[]),cse_used_ids([])]) |
| 787 | | )). |
| 788 | | % two quantifiers with the same variable name must not share |
| 789 | | % expressions that contain the variable, other expressions should be |
| 790 | | % shared |
| 791 | | :- assert_must_succeed( |
| 792 | | ( C = b(identifier(c),integer,[]), |
| 793 | | X = b(identifier(x),integer,[]), |
| 794 | | I = b(identifier(i),set(integer),[]), |
| 795 | | O = b(integer(1),integer,[]), |
| 796 | | % !x.(x:I => x<c+1) |
| 797 | | F = b(forall([X], |
| 798 | | b(member(X,I),pred,[]), |
| 799 | | b(less(X,b(add(C,O),integer,[])),pred,[])),pred,[]), |
| 800 | | % !x.(x:I => x>c+1) |
| 801 | | Fx = b(forall([X], |
| 802 | | b(member(X,I),pred,[]), |
| 803 | | b(greater(X,b(add(C,O),integer,[])),pred,[])),pred,[]), |
| 804 | | C1 = b(identifier(c),integer,[sharing(3,2,top,[]),cse_used_ids([])]), |
| 805 | | X1 = b(identifier(x),integer,[sharing(0,3,7,[]),cse_used_ids([])]), |
| 806 | | I1 = b(identifier(i),set(integer),[sharing(1,2,top,[]),cse_used_ids([])]), |
| 807 | | O1 = b(integer(1),integer,[sharing(4,2,top,[]),cse_used_ids([])]), |
| 808 | | F1 = b(forall([X1], |
| 809 | | b(member(X1,I1),pred,[sharing(2,1,7,[]),cse_used_ids([0,1])]), |
| 810 | | b(less(X1,b(add(C1,O1),integer,[sharing(5,2,top,[]),cse_used_ids([3,4])])), |
| 811 | | pred,[sharing(6,1,7,[]),cse_used_ids([0,3,4,5])])), |
| 812 | | pred,[sharing(7,1,top,[0]),cse_used_ids([0,1,2,3,4,5,6])]), |
| 813 | | % e.g. c+1 should be shared (ref. 5) |
| 814 | | % x and x:I must not be shared, they get a new reference (8 and 9) |
| 815 | | X2 = b(identifier(x),integer,[sharing(8,3,11,[]),cse_used_ids([])]), |
| 816 | | F2 = b(forall([X2], |
| 817 | | b(member(X2,I1),pred,[sharing(9,1,11,[]),cse_used_ids([1,8])]), |
| 818 | | b(greater(X2,b(add(C1,O1),integer,[sharing(5,2,top,[]),cse_used_ids([3,4])])), |
| 819 | | pred,[sharing(10,1,11,[]),cse_used_ids([3,4,5,8])])), |
| 820 | | pred,[sharing(11,1,top,[8]),cse_used_ids([1,3,4,5,8,9,10])]), |
| 821 | | find_common_subexpressions(b(conjunct(F,Fx),pred,[]),0,false,R), |
| 822 | | R == b(conjunct(F1,F2),pred,[sharing(12,1,top,[]),cse_used_ids([0,1,2,3,4,5,6,7,8,9,10,11])]) |
| 823 | | )). |
| 824 | | |
| 825 | | % find_common_subexpressions/4 searches for common subexpressions and adds an |
| 826 | | % information field sharing/4 to each AST node. |
| 827 | | % find_common_subexpressions(+TExpr,+Start,+SkipSimple,-NTExpr): |
| 828 | | % TExpr: the original AST |
| 829 | | % Start: at which number the IDs should start (usually 0) |
| 830 | | % NTExpr: the AST, each node annotated with an sharing(ID,Counter,SubId,References) information field |
| 831 | | % two syntax nodes share the same ID when they should yield always the same |
| 832 | | % value. Counter counts the number of occurrences of the same expression in |
| 833 | | % the given AST. SubId is the unique reference of the quantified expression |
| 834 | | % where a used ID is introduced, top if there is no such quantifier. |
| 835 | | % References is a list of ids that are are sub-expressions of the node which |
| 836 | | % occur more than once and which depend on the newly introduced identifiers |
| 837 | | % (Please note: The declaration of a variable in a quantified expression |
| 838 | | % is an occurrence of its own.) |
| 839 | | % SkipSimple: set to true if expression sharing should not be applied to simple |
| 840 | | % expressions like identifier(_), integer(_), etc. |
| 841 | | find_common_subexpressions(TExpr,Start,SkipSimple,NTExpr) :- |
| 842 | | find_common_subexpressions(TExpr,Start,SkipSimple,NTExpr,_). |
| 843 | | find_common_subexpressions(TExpr,Start,SkipSimple,NTExpr,References) :- |
| 844 | ? | create_stores(Start,EmptyStores), |
| 845 | ? | find_common_subexpressions2(TExpr,EmptyStores,SkipSimple,root/1,NTExpr,Stores,_Stripped,_UsedIds,_UsedCSEIds), |
| 846 | | %print(grounding(Stores)),nl, |
| 847 | | ground_reference_counters(Stores), %print(stores(Stores)),nl, print(NTExpr),nl, |
| 848 | | get_current_references(Stores,References). % needed ?? |
| 849 | | |
| 850 | | :- if(environ(prob_safe_mode,true)). |
| 851 | | add_cse_used_ids_info(Ids,OldInfos,NewInfos) :- (var(Ids) ; \+ ground(OldInfos)),!, |
| 852 | | add_internal_error('Illegal Call: ',add_cse_used_ids_info(Ids,OldInfos,NewInfos)), |
| 853 | | NewInfos = OldInfos. |
| 854 | | :- endif. |
| 855 | | add_cse_used_ids_info(Ids,OldInfos,NewInfos) :- |
| 856 | | exclude(is_cse_used_ids,OldInfos,OldInfos1), |
| 857 | | NewInfos=[cse_used_ids(Ids)|OldInfos1]. |
| 858 | | |
| 859 | | % find_common_subexpressions2(+TExpr,+InStores,+SkipSimple,+OuterFunctor,-NTExpr,-OutStores,-Stripped,-UsedIds,-UsedCSEIds): |
| 860 | | find_common_subexpressions2(TExpr,InStores,SkipSimple,OuterFunctor,NTExpr,OutStores,Stripped,UsedIds,UsedCSEIds) :- |
| 861 | | %print(find(TExpr,InStores,outer(OuterFunctor))),nl, |
| 862 | | % decompose the typed expression into its components (Subs), look up the newly introduced |
| 863 | | % identifiers (NewIds) and create a new typed expression (NTExpr) with the modified components |
| 864 | | % (NSubs) and the new Info field (Info) |
| 865 | ? | fc_parts(TExpr,Expr,Type,Subs,NewQuantifiedIds,InvalidatedIds,NSubs,OldInfos,NewInfos,NTExpr), |
| 866 | | % introduce a map from expression to reference that is only visible to this node |
| 867 | | % and it subnodes if new identifiers (NewIds) are introduced |
| 868 | | % OutStores1 and OutStores contain a pattern such that if OutStores1 is set, |
| 869 | | % OutStores is exactly like OutStores1 but without visibility of the newly introduced |
| 870 | | % identifiers. |
| 871 | ? | append(InvalidatedIds,NewQuantifiedIds,NewIds), |
| 872 | ? | create_substore(NewIds,ID,InStores,SubStores), |
| 873 | | % apply subexpression detection on the subexpressions |
| 874 | ? | functor(Expr,OuterExprFunctor,_), % memorise functor for sub-expressions (allows deciding if sharing makes sense) |
| 875 | ? | find_common_subexpressions_l(Subs,SubStores,SkipSimple,OuterExprFunctor,1, |
| 876 | | NSubs,SubStores1,StrippedSubs,UsedSubIds,SubUsedCSEIds), |
| 877 | | % create a stripped (i.e. no info field, no types) version of the syntax node for look ups |
| 878 | ? | (Type==subst -> Stripped=not_relevant % substitions are never shared (and everything containing a subst is a subst itself) |
| 879 | ? | ; create_stripped(Expr,StrippedSubs,Stripped)), |
| 880 | | %print(stripped(Stripped)),nl, |
| 881 | | LookupKey = cse_lookup_key(Stripped,Type), % we also store the type along with the stripped AST (avoid sharing, e.g., two prj1/2 functions with different types, see test 255 !) |
| 882 | | % merge the used ids of the subnodes with the used ids in this node, |
| 883 | | % subtract newly introduced quantified identifiers because they are not visible from outside |
| 884 | | update_used_ids(Expr,NewQuantifiedIds,UsedSubIds,UsedIds), |
| 885 | | % if a substore was introduced due to newly introduced identifiers, remove it |
| 886 | | %%(OuterExprFunctor=while -> portray_stores(SubStores1) ; true), |
| 887 | | remove_last_substore(NewIds,SubStores1,Stores1,References), |
| 888 | | % try to find the expression in the stores |
| 889 | ? | (do_not_share_this(SkipSimple,Stripped,UsedIds,OuterFunctor,Type,OldInfos) -> |
| 890 | | OutStores = Stores1, |
| 891 | | add_cse_used_ids_info(SubUsedCSEIds,OldInfos,NewInfos), |
| 892 | | UsedCSEIds = SubUsedCSEIds, |
| 893 | | store_expression(LookupKey,UsedIds,Stores1,_,_,ID) /* just ground ID; used for Sub expressions */ |
| 894 | | %, print(not_sharing(ID)) |
| 895 | | ; lookup_cse(Type,LookupKey,UsedIds,Stores1,OutStores,SharingInfo,Negated,ID) -> |
| 896 | | /* it is shared */ |
| 897 | | % print(looked_up(ID,Negated,used(UsedIds,sub(UsedSubIds)),Stores1)),nl, |
| 898 | | (Negated=negated_cse -> NewInfos=[Negated,SharingInfo|OldInfos1] |
| 899 | | ; NewInfos=[SharingInfo|OldInfos1]), |
| 900 | | add_cse_used_ids_info(SubUsedCSEIds,OldInfos,OldInfos1), |
| 901 | | ord_union([ID],SubUsedCSEIds,UsedCSEIds), |
| 902 | | set_references(References,SharingInfo) |
| 903 | | % In this case we do not need to look for sharing in the sub-expressions !! |
| 904 | | %,check_sharing_info(lookup,SharingInfo) |
| 905 | | ; otherwise -> |
| 906 | | % if not found, store the expression: it will be shared if we use it again later |
| 907 | | store_expression(LookupKey,UsedIds,Stores1,OutStores,SharingInfo,ID), |
| 908 | | ord_union([ID],SubUsedCSEIds,UsedCSEIds), |
| 909 | | % print(new_id(ID,UsedIds,SubUsedCSEIds,OutStores)),nl, |
| 910 | | % TO DO: what if later we find out that it is shared after all -> we should remove sub-expression counts |
| 911 | | add_cse_used_ids_info(SubUsedCSEIds,OldInfos,OldInfos1), |
| 912 | | NewInfos=[SharingInfo|OldInfos1], |
| 913 | | set_references(References,SharingInfo) |
| 914 | | %,check_sharing_info(new,SharingInfo) |
| 915 | | ). % print(done_find(NTExpr,OutStores,UsedIds,UsedCSEIds)),nl. |
| 916 | | |
| 917 | | lookup_cse(Type,LookupKey,UsedIds,Stores1,OutStores,SharingInfo,Negated,ID) :- |
| 918 | | (lookup_expression(LookupKey,UsedIds,Stores1,OutStores,SharingInfo,ID) |
| 919 | | -> Negated = normal_cse |
| 920 | | ; Type=pred, negate_lookup_key(LookupKey,NegKey), % try looking up negation |
| 921 | | lookup_expression(NegKey,UsedIds,Stores1,OutStores,SharingInfo,ID), |
| 922 | | Negated = negated_cse). |
| 923 | | |
| 924 | | negate_lookup_key(cse_lookup_key(P,pred),cse_lookup_key(NP,pred)) :- |
| 925 | | negate_norm_strip(P,NP). |
| 926 | | |
| 927 | | %check_sharing_info(_,sharing(Id,_RefCounter,Level,Refs)) :- number(Id), ground(Level), ground(Refs),!. |
| 928 | | %check_sharing_info(PP,SI) :- print(illegal_sharing_info(PP,SI)),nl. |
| 929 | | |
| 930 | | % NewIds = introduced IDs or modified Ids |
| 931 | | fc_parts(TExpr,Expr,Type,Subs,SQuantifiedNewIds,InvalidatedIds,NSubs,OldInfos2,NewInfos,NTExpr) :- |
| 932 | | my_decompose_texpr(TExpr,Expr,Type,OldInfos), |
| 933 | | cse_syntaxtransformation(Expr,Subs,Names,NSubs,NExpr), |
| 934 | | get_texpr_ids(Names,QuantifiedNewIds), list_to_ord_set(QuantifiedNewIds,SQuantifiedNewIds), |
| 935 | | (select(invalidate_ids_for_cse(ModifiedIDs),OldInfos,OldInfos2) |
| 936 | | % we have a stored invalidation info for CSE |
| 937 | | -> InvalidatedIds=ModifiedIDs |
| 938 | | ; InvalidatedIds= [],OldInfos=OldInfos2), |
| 939 | | %functor(Expr,F,A), format('-> ~w/~w : ~w + ~w~n',[F,A,SQuantifiedNewIds,InvalidatedIds]), |
| 940 | | create_texpr(NExpr,Type,NewInfos,NTExpr). |
| 941 | | % TO DO: re-flatten the sequential compositions later |
| 942 | | |
| 943 | | % CSE traversal which ignores certain sub-arguments (mainly LHS of assignments) |
| 944 | | cse_syntaxtransformation(assign(LHS,RHS),RHS,[],NRHS,NExpr) :- !, % print(assign(LHS)),nl, |
| 945 | | same_length(RHS,NRHS), |
| 946 | | NExpr=assign(LHS,NRHS). |
| 947 | | cse_syntaxtransformation(becomes_element_of(LHS,RHS),[RHS],[],[NRHS],NExpr) :- !, |
| 948 | | NExpr=becomes_element_of(LHS,NRHS). |
| 949 | | cse_syntaxtransformation(becomes_such(LHS,RHS),[RHS],[],[NRHS],NExpr) :- !, |
| 950 | | NExpr=becomes_such(LHS,NRHS). |
| 951 | | cse_syntaxtransformation(evb2_becomes_such(LHS,RHS),[RHS],[],[NRHS],NExpr) :- !, |
| 952 | | NExpr=evb2_becomes_such(LHS,NRHS). |
| 953 | | cse_syntaxtransformation(assign_single_id(Id,RHS),[RHS],[],[NRHS],NExpr) :- !, |
| 954 | | NExpr=assign_single_id(Id,NRHS). |
| 955 | | cse_syntaxtransformation(Expr,Subs,Names,NSubs,NExpr) :- syntaxtransformation(Expr,Subs,Names,NSubs,NExpr). |
| 956 | | % TO DO: rlevent(Id,Section,Status,Parameters,Guard,Theorems,Actions,VWitnesses,PWitnesses,_Unmod,Refines) |
| 957 | | |
| 958 | | :- use_module(b_read_write_info, [get_accessed_vars/4]). |
| 959 | | my_decompose_texpr(b(Expr,Type,Infos),Expr2,Type,Infos2) :- my_decompose2(Expr,Expr2,ModifiedIDs), |
| 960 | | add_invalidated_ids_to_infos(Infos,ModifiedIDs,Infos2). |
| 961 | | % decompose sequence into left and right part and store invalidated parts on the right |
| 962 | | my_decompose2(sequence([TSubst|T]),Res,[]) :- !, |
| 963 | | Res=sequence([TSubst|NT]), |
| 964 | | get_accessed_vars(TSubst,[],ModifiedIDs,_), |
| 965 | | print(modified_sequence(ModifiedIDs)),nl, |
| 966 | | construct_seq_tail(T,ModifiedIDs,NT). |
| 967 | | % annotate parts of while loop with variables which are invalidated by loop iteration |
| 968 | | % note the While loop itself also invalidates the same variables, ensures that a substore |
| 969 | | % is already set-up when entering the sub-nodes; TO DO: examine whether we can simplify this by improving the way shared expressions are stored above |
| 970 | | my_decompose2(while(COND,TSubst,INV,VARIANT),while(COND2,TSubst2,INV2,VARIANT2),ModifiedIDs) :- |
| 971 | | get_accessed_vars(TSubst,[],ModifiedIDs,_), |
| 972 | | print(modified_while(ModifiedIDs)),nl, |
| 973 | | add_invalidated_ids(TSubst,ModifiedIDs,TSubst2), |
| 974 | | add_invalidated_ids(COND,ModifiedIDs,COND2), |
| 975 | | add_invalidated_ids(INV,ModifiedIDs,INV2), |
| 976 | | add_invalidated_ids(VARIANT,ModifiedIDs,VARIANT2). |
| 977 | | my_decompose2(X,X,[]). |
| 978 | | |
| 979 | | add_invalidated_ids_to_infos(L,[],R) :- !, R=L. |
| 980 | | add_invalidated_ids_to_infos(L,Ids,[invalidate_ids_for_cse(Ids)|L]). |
| 981 | | |
| 982 | | add_invalidated_ids(b(E,T,I),Ids,b(E,T,[invalidate_ids_for_cse(Ids)|I])). |
| 983 | | |
| 984 | | construct_seq_tail([],_,[]) :- !. |
| 985 | | %construct_seq_tail([X],[X]) :- !. |
| 986 | | construct_seq_tail([H|T],ModifiedIDs,[b(sequence([H|T]),subst,[cse_generated,invalidate_ids_for_cse(ModifiedIDs)])]). % store that modified vars are invalid for CSE in tail |
| 987 | | |
| 988 | | |
| 989 | | |
| 990 | | find_common_subexpressions_l([],Stores,_SkipSimple,_OuterFunctor,_,[],Stores,[],[],[]). |
| 991 | | find_common_subexpressions_l([Expr|Erest],InStores,SkipSimple,OuterFunctor,ArgNr, |
| 992 | | [NExpr|Nrest],OutStores,[Stripped|Srest],UsedIds,UsedCSEIds) :- |
| 993 | ? | find_common_subexpressions2(Expr,InStores,SkipSimple,outer(OuterFunctor,ArgNr),NExpr,InterStores,Stripped,UsedIds1,UsedCSEIds1), |
| 994 | ? | A1 is ArgNr+1, |
| 995 | ? | find_common_subexpressions_l(Erest,InterStores,SkipSimple,OuterFunctor,A1,Nrest,OutStores,Srest,UsedIds2,UsedCSEIds2), |
| 996 | | ord_union(UsedIds1,UsedIds2,UsedIds), % the B identifiers used |
| 997 | | ord_union(UsedCSEIds1,UsedCSEIds2,UsedCSEIds). % the identifiers to CSE used |
| 998 | | |
| 999 | | boolean(boolean_true). |
| 1000 | | boolean(boolean_false). |
| 1001 | | |
| 1002 | | |
| 1003 | | do_not_share_this(_,_,_,_,Type,_) :- \+ ground(Type),!. % it could be that the Type is ground, but the sub-expressions contain non-ground types; see test 1090 size(arr) |
| 1004 | | % nl,print(not_sharing_non_ground_type(Type)),nl,nl. |
| 1005 | | % TO DO: can we maybe still share non-ground type terms if we are careful ? see also tests 402, 403 ? |
| 1006 | | do_not_share_this(_,_,_,_,Type,_) :- do_not_share_type(Type),!. |
| 1007 | | do_not_share_this(_,_Stripped,_,_Functor,_Type,Infos) :- |
| 1008 | | memberchk(contains_wd_condition,Infos), |
| 1009 | | get_preference(use_common_subexpression_wd_only,true), |
| 1010 | | !. % also examine DISPROVER MODE ? |
| 1011 | | do_not_share_this(_,_Stripped,_,_Functor,Type,_Infos) :- Type==pred, |
| 1012 | | get_preference(use_common_subexpression_also_for_predicates,false), |
| 1013 | | !. |
| 1014 | | do_not_share_this(SkipSimple,Stripped,UsedIds,OuterFunctor,_Type,_Infos) :- |
| 1015 | ? | SkipSimple==true, % print(chk(Stripped,OuterFunctor)),nl, |
| 1016 | ? | do_not_share_this_3(Stripped,UsedIds,OuterFunctor). |
| 1017 | | |
| 1018 | | do_not_share_type(subst). |
| 1019 | | do_not_share_type(status). % Event-B Event Status |
| 1020 | | |
| 1021 | | :- use_module(external_functions,[not_declarative/1]). |
| 1022 | | |
| 1023 | | do_not_share_this_3(case_or(_,_),_,_) :- !. % why does this have a pred type ? |
| 1024 | | do_not_share_this_3(if_elsif(_,_),_,_) :- !. |
| 1025 | | do_not_share_this_3(select_when(_,_),_,_) :- !. % has subst type; so will not be shared |
| 1026 | ? | do_not_share_this_3(set_extension(X),_,outer(OuterFunctor,ArgNr)) :- !, |
| 1027 | | %nl,print(sx(X,OuterFunctor/ArgNr)),nl, |
| 1028 | ? | (X = [V], simple_explicit_value(V) ; % singleton set with simple value |
| 1029 | | set_extension_optimized_treatment_available(OuterFunctor,ArgNr)). |
| 1030 | | do_not_share_this_3(comprehension_set(_Id,_),_,M) :- |
| 1031 | | % optimized treatment available; important for test 1079 |
| 1032 | ? | (nmem(M) -> true ; symbolic_set_op(M)). % -> true ; print(share(_Id,M)),nl,nl,fail). |
| 1033 | | do_not_share_this_3(union(_,_),_,M) :- |
| 1034 | | % union often used for composing functions |
| 1035 | | (nmem(M) -> true ; symbolic_set_op(M)). % -> true ; print(share_union(M)),nl,nl,fail). |
| 1036 | | % lambda is already translated into comprehension_set here |
| 1037 | | %do_not_share_this_3(closure(_L),_,outer(OuterFunctor,ArgNr)) :- !, |
| 1038 | | % closure1_optimized_treatment_available(OuterFunctor,ArgNr). |
| 1039 | | %do_not_share_this_3(sequence_extension(_L),_,outer(OuterFunctor,ArgNr)) :- !, % we need to add b_compute_card2 for seq ? |
| 1040 | | /* |
| 1041 | | do_not_share_this_3(X,_,M) :- nmem(M), functor(X,F), |
| 1042 | | (kernel_mappings:symbolic_closure_unary_operator(F) ; |
| 1043 | | kernel_mappings:symbolic_closure_binary_operator(F)). |
| 1044 | | |
| 1045 | | % case for unary_in_boolean_type solutions: |
| 1046 | | */ |
| 1047 | | do_not_share_this_3(pow_subset(X),_,M) :- nmem(M) ; infinite_set(X). |
| 1048 | | do_not_share_this_3(fin_subset(X),_,M) :- nmem(M) ; infinite_set(X). |
| 1049 | | do_not_share_this_3(pow1_subset(X),_,M) :- nmem(M) ; infinite_set(X). |
| 1050 | | do_not_share_this_3(fin1_subset(X),_,M) :- nmem(M) ; infinite_set(X). |
| 1051 | | do_not_share_this_3(struct(_),_,M) :- nmem(M). |
| 1052 | ? | do_not_share_this_3(seq(X),_,M) :- nmem(M) ; infinite_set(X). |
| 1053 | | do_not_share_this_3(iseq(X),_,M) :- nmem(M) ; infinite_set(X). |
| 1054 | ? | do_not_share_this_3(perm(_),_,M) :- nmem(M). |
| 1055 | ? | do_not_share_this_3(domain(_),_,M) :- nmem(M). |
| 1056 | | do_not_share_this_3(seq1(X),_,M) :- nmem(M) ; infinite_set(X). |
| 1057 | | do_not_share_this_3(iseq1(X),_,M) :- nmem(M) ; infinite_set(X). |
| 1058 | | do_not_share_this_3(identity(X),_,M) :- nmem(M) ; infinite_set(X). |
| 1059 | | do_not_share_this_3(closure(_),_,M) :- nmem(M). |
| 1060 | | do_not_share_this_3(external_pred_call(FunName,_Args),_,_) :- not_declarative(FunName). % in principle any element containing this should not be shared (but anyway there are little gurantees about preservation and order of side-effects) |
| 1061 | | do_not_share_this_3(external_function_call(FunName,_Args),_,_) :- not_declarative(FunName). |
| 1062 | | % case for binary_not_in_boolean_type solutions: |
| 1063 | | /* |
| 1064 | | do_not_share_this_3(partial_bijection(_,_),_,M) :- nmem(M). |
| 1065 | | do_not_share_this_3(total_relation(_,_),_,M) :- nmem(M). |
| 1066 | | do_not_share_this_3(surjection_relation(_,_),_,M) :- nmem(M). |
| 1067 | | do_not_share_this_3(total_surjection_relation(_,_),_,M) :- nmem(M). |
| 1068 | | do_not_share_this_3(parallel_product(_,_),_,M) :- nmem(M). |
| 1069 | | % set_subtraction, intersection not covered |
| 1070 | | */ |
| 1071 | ? | do_not_share_this_3(interval(A,B),_,M) :- nmem(M) ; small_interval(A,B). |
| 1072 | ? | do_not_share_this_3(total_function(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). |
| 1073 | | do_not_share_this_3(total_injection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). |
| 1074 | | do_not_share_this_3(total_surjection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). |
| 1075 | | do_not_share_this_3(total_bijection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). |
| 1076 | | do_not_share_this_3(partial_function(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). |
| 1077 | | do_not_share_this_3(partial_injection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). % >+> |
| 1078 | | do_not_share_this_3(partial_surjection(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). |
| 1079 | ? | do_not_share_this_3(relations(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). |
| 1080 | ? | do_not_share_this_3(cartesian_product(A,B),_,M) :- nmem(M) ; infinite_set(A) ; infinite_set(B). |
| 1081 | | %do_not_share_this_3(div(A,B),_,_) :- A=identifier(xx), B=integer(1000000000). % xx / 1000000000 ; purpose: test vesg performance issue |
| 1082 | | %do_not_share_this_3(range(identifier('Block_Id')),_,_). % for vesg performance test in INVARIANT |
| 1083 | | |
| 1084 | | do_not_share_this_3(Stripped,UsedIds,_OuterFunctor) :- too_simple_for_sharing2(Stripped,UsedIds). |
| 1085 | | |
| 1086 | | % check if expression used as second arg of member check: |
| 1087 | | nmem(outer(M,2)) :- mem_op(M). |
| 1088 | ? | nmem(outer(M,_)) :- (M=partial_function ; M=total_function ; M=relations). |
| 1089 | | mem_op(member). |
| 1090 | | mem_op(not_member). |
| 1091 | ? | symbolic_set_op(outer(M,P)) :- (M=union; M=function,P=1). |
| 1092 | | |
| 1093 | | small_interval(integer(A),integer(B)) :- number(A),number(B), B < A+10000000. |
| 1094 | | infinite_set(integer_set(_)). % :- (X='INTEGER' ; X = 'NATURAL' ; X = 'NATURAL1'). |
| 1095 | | infinite_set(string_set). |
| 1096 | | % TO DO : couple |
| 1097 | | simple_explicit_value(integer(_)). |
| 1098 | | simple_explicit_value(string(_)). |
| 1099 | | simple_explicit_value(boolean_true). |
| 1100 | | simple_explicit_value(boolean_false). |
| 1101 | | simple_explicit_value(identifier(_Id)). % :- b_global_sets:is_b_global_constant(_,_,Id). % no guarantee that this is really an enumerated set element because a local variable could overide this; but |
| 1102 | | % TO DO: should any identifier not be ok here: basically, we just gain the lookup when sharing ?? |
| 1103 | | %simple_explicit_value(V) :- print(sev(V)),nl,fail. |
| 1104 | | |
| 1105 | | set_extension_optimized_treatment_available(card,1). |
| 1106 | | set_extension_optimized_treatment_available(min,1). % we have optimized code for min({a,b,...}) and max |
| 1107 | | set_extension_optimized_treatment_available(max,1). |
| 1108 | | set_extension_optimized_treatment_available(function,1). |
| 1109 | | set_extension_optimized_treatment_available(subset,2). % there is a rule in cleanup_post which will rewrite this to member checks {x1,x2,...} <: B <=> x1:B & x2:B & ...; we could also try and ensure that this runs first ! |
| 1110 | | set_extension_optimized_treatment_available(image,2). % ?? |
| 1111 | | |
| 1112 | | %closure1_optimized_treatment_available(image,1). % there is some custom code for: image_for_closure1_wf; but it is also called if we do CSE ??!! |
| 1113 | | |
| 1114 | | :- use_module(external_functions,[performs_io/1]). |
| 1115 | | too_simple_for_sharing2(equal(A,B),_) :- |
| 1116 | | (A = identifier(_Id), boolean(B) ; |
| 1117 | | B = identifier(_Id), boolean(A) ). |
| 1118 | | too_simple_for_sharing2(identifier(Id),[Id]). |
| 1119 | | too_simple_for_sharing2(unary_minus(Int),[]) :- Int = integer(_). |
| 1120 | | too_simple_for_sharing2(integer(_),[]). |
| 1121 | | too_simple_for_sharing2(value(_),[]). |
| 1122 | | too_simple_for_sharing2(boolean_true,[]). |
| 1123 | | too_simple_for_sharing2(boolean_false,[]). |
| 1124 | | too_simple_for_sharing2(integer_set(_),[]). |
| 1125 | | too_simple_for_sharing2(bool_set,[]). |
| 1126 | | too_simple_for_sharing2(string(_),[]). |
| 1127 | | too_simple_for_sharing2(string_set,[]). |
| 1128 | | too_simple_for_sharing2(empty_set,[]). |
| 1129 | | too_simple_for_sharing2(empty_sequence,[]). |
| 1130 | | too_simple_for_sharing2(lazy_lookup_pred(_),_). |
| 1131 | | too_simple_for_sharing2(lazy_lookup_expr(_),_). |
| 1132 | | too_simple_for_sharing2(lazy_let_expr(_,_,_),_). |
| 1133 | | too_simple_for_sharing2(lazy_let_pred(_,_,_),_). |
| 1134 | | too_simple_for_sharing2(lazy_let_subst(_,_,_),_). |
| 1135 | | too_simple_for_sharing2(couple(_,_),_). % maybe could be useful nonetheless ?? |
| 1136 | | |
| 1137 | | %too_simple_for_sharing2(interval(integer(_),integer(_)),_). |
| 1138 | | % TO DO: do not share arithmetic expressions which can be constant folded ?? |
| 1139 | | % or maybe perform constant folding at the same time ?? |
| 1140 | | |
| 1141 | | too_simple_for_sharing2(truth,[]). |
| 1142 | | too_simple_for_sharing2(falsity,[]). |
| 1143 | | |
| 1144 | | % TO DO: completely avoid sharing those expressions ? but usually they should not occur inside predicates/expressions anyway |
| 1145 | | too_simple_for_sharing2(external_pred_call(FunName,_Args),_) :- |
| 1146 | | external_functions:performs_io(FunName). |
| 1147 | | too_simple_for_sharing2(external_function_call(FunName,_Args),_) :- |
| 1148 | | external_functions:performs_io(FunName). |
| 1149 | | |
| 1150 | | |
| 1151 | | |
| 1152 | | set_references(References,sharing(_Id,_RefCounter,_Level,References)). |
| 1153 | | |
| 1154 | | % the stores data type has the following form: |
| 1155 | | % stores(Counter,References,Top,Substores) |
| 1156 | | % - Counter is the next ID for new expressions, the same expressions |
| 1157 | | % share the same id |
| 1158 | | % - References is a mapping from an ID to a term rc(C,R) where C |
| 1159 | | % contains the number of occurrences of the expressions so far and R the |
| 1160 | | % final number of occurrences of this expression. Until the end, R is a variable |
| 1161 | | % that will be unified with the last value of C |
| 1162 | | % - Top is a mapping from a stripped expression to an ID. This mapping is for all |
| 1163 | | % expressions that do not contain references to quantified variables |
| 1164 | | % - Substores is a list of terms substore(Ids,SubStore) where Ids is a list of |
| 1165 | | % introduced identifiers in a qualified expression and Substore is a mapping from |
| 1166 | | % a stripped expression to its ID. The expression contains references to identifiers |
| 1167 | | % in Ids. In case of nested quantified expressions, the inner expression has |
| 1168 | | % a substore entry before the outer expression in the list. |
| 1169 | | create_stores(Start,stores(Start,Empty,Empty,[])) :- |
| 1170 | | empty_avl(Empty). |
| 1171 | | create_substore([],_SubId,Stores,Stores) :- !. |
| 1172 | | create_substore(NewIds,ID,InStores,SubStores) :- |
| 1173 | | force_create_substore(NewIds,ID,InStores,SubStores). |
| 1174 | | force_create_substore(Ids,SubId, |
| 1175 | | stores(Counter,IR,Top, InSubs), |
| 1176 | | stores(Counter,IR,Top, [substore(OrdIds,Empty,SubId,[])|InSubs])) :- |
| 1177 | | list_to_ord_set(Ids,OrdIds), |
| 1178 | | empty_avl(Empty). |
| 1179 | | |
| 1180 | | % remove_last_substore(+Names,+InSubStores,-OutSubStores,-References) |
| 1181 | | remove_last_substore([],Stores,Stores,[]). |
| 1182 | | remove_last_substore([_|_], % new ids have been introduced; local scope / substore was added |
| 1183 | | stores(Counter,IR,Top,[Substore|Subs]), |
| 1184 | | stores(Counter,IR,Top,Subs), |
| 1185 | | References) :- |
| 1186 | | Substore = substore(_Names,_Store,_SubId,References). |
| 1187 | | |
| 1188 | | % try and get references to common sub expression ids + the corresponding expressions |
| 1189 | | get_current_references(stores(_Counter,IR,TopStore,_Subs),References) :- |
| 1190 | | avl_to_list(IR,Refs), |
| 1191 | | convlist(reused_expression(TopStore),Refs,References). |
| 1192 | ? | reused_expression(TopStore,ID-rc(Count,Count),cse(ID,Expr,Count)) :- Count>1, |
| 1193 | ? | avl_member(Expr,TopStore,ID). % reverse lookup; not efficient ! |
| 1194 | | |
| 1195 | | lookup_expression(Stripped,UsedIds,InStores,OutStores,sharing(Id,RefCounter,Level,_References),Id) :- |
| 1196 | | InStores = stores(Counter,InRefCounter, TopStore,OldSubStores), |
| 1197 | | OutStores = stores(Counter,OutRefCounter,TopStore,NewSubStores), |
| 1198 | | lookup_expression2(OldSubStores,TopStore,Stripped,UsedIds,Id,Level,NewSubStores),!, |
| 1199 | | avl_fetch(Id,InRefCounter,rc(OC,RefCounter)), |
| 1200 | | NC is OC+1, |
| 1201 | | avl_store(Id,InRefCounter,rc(NC,RefCounter),OutRefCounter). |
| 1202 | | lookup_expression2([],TopStore,Stripped,_UsedIds,Id,top,[]) :- |
| 1203 | | avl_fetch(Stripped,TopStore,Id). |
| 1204 | | lookup_expression2([substore(Names,Store,SubId,OldRefs)|Rest],_TopStore,Stripped,_UsedIds,Id,SubId, |
| 1205 | | [substore(Names,Store,SubId,NewRefs)|Rest]) :- |
| 1206 | | avl_fetch(Stripped,Store,Id),!, |
| 1207 | | ord_add_element(OldRefs,Id,NewRefs). |
| 1208 | | lookup_expression2([substore(Names,Store,SubId,Refs)|Rest],TopStore,Stripped,UsedIds,Id,Level, |
| 1209 | | [substore(Names,Store,SubId,Refs)|NRest]) :- |
| 1210 | | ord_disjoint(UsedIds,Names), |
| 1211 | | !, |
| 1212 | | lookup_expression2(Rest,TopStore,Stripped,UsedIds,Id,Level,NRest). |
| 1213 | | |
| 1214 | | %lookup_next_id(stores(Id,_,_,_),Id). |
| 1215 | | |
| 1216 | | store_expression(Stripped,UsedIds,InStores,OutStores,sharing(Id,RefCounter,Level,_References),Id) :- |
| 1217 | | InStores = stores(Id,InRefCounter,InTopStore,InSubStores), |
| 1218 | | Counter is Id+1, % Generate a new CSE Identifier |
| 1219 | | OutStores = stores(Counter,OutRefCounter,OutTopStore,OutSubStores), |
| 1220 | | store_expression2(InSubStores,InTopStore,Stripped,UsedIds,Id,OutSubStores,OutTopStore,Level), |
| 1221 | | avl_store(Id,InRefCounter,rc(1,RefCounter),OutRefCounter). |
| 1222 | | store_expression2([],InTopStore,Stripped,_UsedIds,Id,[],OutTopStore,top) :- |
| 1223 | | avl_store(Stripped,InTopStore,Id,OutTopStore). |
| 1224 | | store_expression2([substore(Names,InStore,SubId,Refs) |Srest],TopStore,Stripped,UsedIds,Id, |
| 1225 | | [substore(Names,OutStore,SubId,Refs)|Srest],TopStore,SubId) :- |
| 1226 | | ord_intersect(Names,UsedIds),!, % the Shared Expression makes use of identifiers/names introduced at that level; it cannot be re-used higher up |
| 1227 | | avl_store(Stripped,InStore,Id,OutStore). |
| 1228 | | store_expression2([Substore|ISrest],InTopStore,Stripped,UsedIds,Id, |
| 1229 | | [Substore|OSrest],OutTopStore,Level) :- |
| 1230 | | store_expression2(ISrest,InTopStore,Stripped,UsedIds,Id,OSrest,OutTopStore,Level). |
| 1231 | | |
| 1232 | | :- public portray_stores/1. % for debugging |
| 1233 | | portray_stores(stores(Counter,RefCounter,TopStore,SubStores)) :- |
| 1234 | | format('Store Counter:~w ~n Reference Counts: ',[Counter]), |
| 1235 | | avl:portray_avl(RefCounter),nl, |
| 1236 | | print('Top = '), avl:portray_avl(TopStore),nl, |
| 1237 | | (maplist(portray_substore,SubStores) -> true ; print('Illegal Substores: '),nl). |
| 1238 | | portray_substore(substore(Names,OutStore,_SubId,Refs)) :- |
| 1239 | | format('--> Substore [Names=~w, Refs=~w]~n Store = ',[Names,Refs]), |
| 1240 | | avl:portray_avl(OutStore),nl. |
| 1241 | | |
| 1242 | | update_used_ids(Expr,NewlyIntroducedIds,UsedSubIds,UsedIds) :- |
| 1243 | | update_used_ids2(Expr,UsedSubIds,UsedIds1), |
| 1244 | | ord_subtract(UsedIds1,NewlyIntroducedIds,UsedIds). % remove NewlyIntroducedIds; they are not visible outside |
| 1245 | | update_used_ids2(identifier(Id),UsedSubIds,UsedIds) :- !, % we directly use an identifier |
| 1246 | | ord_add_element(UsedSubIds,Id,UsedIds). |
| 1247 | | update_used_ids2(_Expr,UsedSubIds,UsedIds) :- !, UsedSubIds=UsedIds. |
| 1248 | | |
| 1249 | | % We do not have to use strip_and_norm_ast/2 from bsyntaxtree though |
| 1250 | | % the result should be the same. We already have the stripped versions |
| 1251 | | % of the subexpressions, so we can re-use that information |
| 1252 | | create_stripped(Expr,StrippedSubs,NormStripped) :- |
| 1253 | ? | (cse_syntaxtransformation(Expr,_Subs,_Names,StrippedSubs,Stripped) |
| 1254 | ? | -> norm_strip(Stripped,NormStripped) |
| 1255 | | ; add_internal_error('Illegal Expression: ',create_stripped(Expr,StrippedSubs,NormStripped)), |
| 1256 | | NormStripped = Expr). |
| 1257 | | |
| 1258 | | ground_reference_counters(stores(_Counter,RefCounter,_TopStore,_SubStores)) :- |
| 1259 | | avl_to_list(RefCounter,List), |
| 1260 | | maplist(ground_reference_counter,List). |
| 1261 | | ground_reference_counter(_Id-rc(C,C)). |
| 1262 | | |
| 1263 | | :- use_module(library(samsort)). |
| 1264 | | norm_strip(empty_sequence,R) :- !, R = empty_set. |
| 1265 | | norm_strip(greater_equal(A,B),R) :- !, R = less_equal(B,A). |
| 1266 | | norm_strip(greater(A,B),R) :- !, R = less(B,A). |
| 1267 | | norm_strip(set_extension(SX),R) :- !, |
| 1268 | | sort(SX,SSX), |
| 1269 | | R = set_extension(SSX). |
| 1270 | | norm_strip(negation(A),R) :- negate_norm_strip(A,R). |
| 1271 | | norm_strip(Old,New) :- |
| 1272 | | functor(Old,Functor,2), |
| 1273 | | is_commutative(Functor),!, |
| 1274 | | norm_commutative(Functor,Old,New). |
| 1275 | | norm_strip(Old,Old). |
| 1276 | | |
| 1277 | | negate_norm_strip(equal(A,B),R) :- !, R=not_equal(A,B). |
| 1278 | | negate_norm_strip(not_equal(A,B),R) :- !, R=equal(A,B). |
| 1279 | | negate_norm_strip(less_equal(A,B),R) :- !, R=less(B,A). |
| 1280 | | negate_norm_strip(less(A,B),R) :- !, R=less_equal(B,A). |
| 1281 | | negate_norm_strip(member(A,B),R) :- !, R=not_member(A,B). |
| 1282 | | negate_norm_strip(not_member(A,B),R) :- !, R=member(A,B). |
| 1283 | | negate_norm_strip(subset(A,B),R) :- !, R=not_subset(A,B). |
| 1284 | | negate_norm_strip(not_subset(A,B),R) :- !, R=subset(A,B). |
| 1285 | | negate_norm_strip(subset_strict(A,B),R) :- !, R=not_subset_strict(A,B). |
| 1286 | | negate_norm_strip(not_subset_strict(A,B),R) :- !, R=subset_strict(A,B). |
| 1287 | | negate_norm_strip(conjunct(C),R) :- !, |
| 1288 | | maplist(negate_norm_strip,C,NC), |
| 1289 | | R=disjunct(NC). |
| 1290 | | negate_norm_strip(disjunct(C),R) :- !, |
| 1291 | | maplist(negate_norm_strip,C,NC), |
| 1292 | | R=conjunct(NC). |
| 1293 | | negate_norm_strip(negation(A),R) :- !, R=A. |
| 1294 | | % what about implication, equivalence, exists, forall |
| 1295 | | negate_norm_strip(X,negation(X)). |
| 1296 | | |
| 1297 | | norm_commutative(Functor,Old,New) :- is_associative(Functor), !, |
| 1298 | | functor(Old,Functor,2), arg(1,Old,OA), arg(2,Old,OB), |
| 1299 | | % now collect all args with same functor in left and right: |
| 1300 | | get_top_level_functor_arguments(OA,Functor,LeftArgs), |
| 1301 | | get_top_level_functor_arguments(OB,Functor,RightArgs), |
| 1302 | | append(LeftArgs,RightArgs,Args), |
| 1303 | | samsort(Args,SortedArgs), |
| 1304 | | New =.. [Functor,SortedArgs]. |
| 1305 | | norm_commutative(Functor,Old,New) :- % the functor is not associative (or cannot appear at top-level in OA,OB) |
| 1306 | | functor(Old,Functor,2), arg(1,Old,OA), arg(2,Old,OB), |
| 1307 | | New =.. [Functor,NA,NB], |
| 1308 | | ( OA @>= OB -> OA=NB,OB=NA |
| 1309 | | ; otherwise -> OA=NA,OB=NB). |
| 1310 | | |
| 1311 | | % we could use this instead of samsort |
| 1312 | | % but we get error message e.g. for % (x\/y\/v\/x) /= (v\/x\/y) & x<:BOOL as an expression appears within itself ?! |
| 1313 | | %sort_args(Functor,Args,SortedArgs) :- |
| 1314 | | % (idempotent(Functor) -> sort(Args,SortedArgs) % we can remove duplicates |
| 1315 | | % ; samsort(Args,SortedArgs)). |
| 1316 | | |
| 1317 | | |
| 1318 | | get_top_level_functor_arguments(Top,Functor,Args) :- % must also be associative |
| 1319 | | functor(Top,Functor,N), !, |
| 1320 | | (N=2 -> Top =.. [Functor|Args] % no normalisation applied |
| 1321 | | ; arg(1,Top,Args)). % Note: we do not recurse: we assume normalisation has already been applied fully below |
| 1322 | | get_top_level_functor_arguments(Top,_,[Top]). |
| 1323 | | |
| 1324 | | %is_commutative(_) :- !,fail. |
| 1325 | | is_commutative(conjunct). % commutative only if there are no WD issues ! |
| 1326 | | is_commutative(disjunct). % commutative only if there are no WD issues ! |
| 1327 | | is_commutative(equivalence). |
| 1328 | | is_commutative(equal). |
| 1329 | | is_commutative(not_equal). |
| 1330 | | is_commutative(add). |
| 1331 | | is_commutative(multiplication). |
| 1332 | | is_commutative(union). |
| 1333 | | is_commutative(intersection). |
| 1334 | | |
| 1335 | | |
| 1336 | | %is_associative(_) :- !,fail. |
| 1337 | | is_associative(conjunct). % even if there are WD issues ! |
| 1338 | | is_associative(disjunct). % even if there are WD issues ! |
| 1339 | | is_associative(add). |
| 1340 | | is_associative(multiplication). |
| 1341 | | is_associative(union). |
| 1342 | | is_associative(intersection). |
| 1343 | | is_associative(concat). |
| 1344 | | is_associative(composition). |
| 1345 | | |
| 1346 | | % not used at the moment: |
| 1347 | | :- public idempotent/1. |
| 1348 | | idempotent(conjunct). |
| 1349 | | idempotent(disjunct). |
| 1350 | | idempotent(union). |
| 1351 | | |
| 1352 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 1353 | | % removing implicit negation: |
| 1354 | | % predicates of the form a/=b (resp. a/:b, ...) are |
| 1355 | | % rewritten to not(a=b), (resp. not(a:b), ...) to enable sharing of the |
| 1356 | | % predicate a=b. |
| 1357 | | |
| 1358 | | remove_implicit_negation(TExpr,NTExpr) :- |
| 1359 | | remove_bt(TExpr,Expr,NewExpr,TExpr2), |
| 1360 | | syntaxtransformation(Expr,Subs,_Names,NSubs,NewExpr), |
| 1361 | | remove_implicit_negation_l(Subs,NSubs), |
| 1362 | | remove_implicit_negation2(TExpr2,NTExpr). |
| 1363 | | |
| 1364 | | remove_implicit_negation_l([],[]). |
| 1365 | | remove_implicit_negation_l([OExpr|ORest],[NExpr|NRest]) :- |
| 1366 | | remove_implicit_negation(OExpr,NExpr), |
| 1367 | | remove_implicit_negation_l(ORest,NRest). |
| 1368 | | |
| 1369 | | remove_implicit_negation2(TExpr,NTExpr) :- |
| 1370 | | get_texpr_expr(TExpr,Expr), |
| 1371 | | remove_implicit_negation3(Expr,NTExpr),!. |
| 1372 | | remove_implicit_negation2(TExpr,TExpr). |
| 1373 | | |
| 1374 | | remove_implicit_negation3(negation(P),R) :- |
| 1375 | | get_texpr_expr(P,negation(Q)),!,R=Q. % eliminate double negation |
| 1376 | | remove_implicit_negation3(not_equal(A,B),R) :- negate_bexpr(equal(A,B),A,B,R). |
| 1377 | | remove_implicit_negation3(not_member(A,B),R) :- negate_bexpr(member(A,B),A,B,R). |
| 1378 | | remove_implicit_negation3(not_subset(A,B),R) :- negate_bexpr(subset(A,B),A,B,R). |
| 1379 | | remove_implicit_negation3(not_subset_strict(A,B),R) :- negate_bexpr(subset_strict(A,B),A,B,R). |
| 1380 | | |
| 1381 | | negate_bexpr(Expr,SubA,SubB,R) :- extract_info(SubA,SubB,Info), |
| 1382 | | create_texpr(Expr,pred,Info,P), |
| 1383 | | create_negation(P,R). |
| 1384 | | |
| 1385 | | |
| 1386 | | % TO DO: optimize away unnecessary nested LETs as below: |
| 1387 | | % Optimized pred: |
| 1388 | | % !(sddb1,sddb2).((sddb1 : INTEGER & sddb2 : INTEGER) & (sddb1 |-> sddb2 : dom(SDDBs_Signal) & (Signals_Cap__Name~)(Routes_Cap__Opposite_Signal_ID(route)) : ran(SDDBs_Signal(sddb1 |-> sddb2))) => (LET (@9)==ran(tses) IN (LET (@10)==dom(@9) IN sddb1 /: @10 & sddb2 /: @10))) |
| 1389 | | |
| 1390 | | |
| 1391 | | /* |
| 1392 | | |
| 1393 | | Code currently not used; but possibly to be re-included : |
| 1394 | | |
| 1395 | | |
| 1396 | | % a version of conjunction which recomputes the cse_used_ids INFO |
| 1397 | | cse_conjunct_predicates(L,Res) :- cse_conjunct_predicates2(L,b(E,pred,I)), |
| 1398 | | (collect_uses_cse_id(L,CSEINFO) |
| 1399 | | -> Res = b(E,pred,[cse_used_ids(CSEINFO)|I1]), |
| 1400 | | exclude(is_cse_used_ids,I,I1) %delete(I,cse_used_ids(_),I1) |
| 1401 | | ; print('*** Could not collect uses_cse_id INFO :'), print(L),nl, |
| 1402 | | Res = b(E,pred,I)). |
| 1403 | | |
| 1404 | | % sometimes we get identical conjuncts; TO DO: generalize to longer lists,... (test 351 still leaves redundant conjuncts inside let body) |
| 1405 | | cse_conjunct_predicates2([A,B],R) :- A==B, !, R=A. |
| 1406 | | cse_conjunct_predicates2(L,R) :- conjunct_predicates(L,R). |
| 1407 | | |
| 1408 | | |
| 1409 | | % find prefix list of conjuncts which do not use CSEID: |
| 1410 | | find_prefix_not_using_cse_id([],_CSEID,[],[]). |
| 1411 | | find_prefix_not_using_cse_id([H|T],CSEID,Prefix,Rest) :- |
| 1412 | | (uses_cse_id(CSEID,H) |
| 1413 | | -> Prefix=[], Rest= [H|T] |
| 1414 | | ; % print('NOT USING '), print(CSEID),nl, translate:print_bexpr_or_subst(H),nl, |
| 1415 | | Prefix = [H|TP], |
| 1416 | | find_prefix_not_using_cse_id(T,CSEID,TP,Rest)). |
| 1417 | | |
| 1418 | | % split a conjunct into PREFIX & MAIN & SUFFIX such that PREFIX/SUFFIX do not use CSEID identifier |
| 1419 | | cse_split_conjunct(Conjunct,CSEID, PREFIX,MAIN,SUFFIX) :- |
| 1420 | | is_a_conjunct(Conjunct,_,_), |
| 1421 | | % try removing conjuncts which do not use CSEID by flattening first: |
| 1422 | | conjunction_to_list(Conjunct,List), |
| 1423 | | find_prefix_not_using_cse_id(List,CSEID,PREFIX,Rest1), |
| 1424 | | reverse(Rest1,RevRest1), |
| 1425 | | find_prefix_not_using_cse_id(RevRest1,CSEID,RevSuffix,RevMain), |
| 1426 | | (PREFIX \= [] ; RevSuffix \= []), % only succeed if there is a non-trivial split |
| 1427 | | reverse(RevMain,MAIN), |
| 1428 | | reverse(RevSuffix,SUFFIX). |
| 1429 | | |
| 1430 | | |
| 1431 | | % binders which pose problem for lazy_let introduction in case SharedExpression depends on bound variables |
| 1432 | | non_unary_binder(b(P,_Type,_I),Ids) :- |
| 1433 | | non_unary_binder_aux(P,Ids,_Left,_Right). |
| 1434 | | non_unary_binder_aux(forall(Ids,A,B),Ids,A,B). |
| 1435 | | non_unary_binder_aux(let_predicate(Ids,A,B),Ids,A,B). |
| 1436 | | % expressions |
| 1437 | | non_unary_binder_aux(general_sum(Ids,A,B),Ids,A,B). |
| 1438 | | non_unary_binder_aux(general_product(Ids,A,B),Ids,A,B). |
| 1439 | | non_unary_binder_aux(quantified_union(Ids,A,B),Ids,A,B). |
| 1440 | | non_unary_binder_aux(quantified_intersection(Ids,A,B),Ids,A,B). |
| 1441 | | non_unary_binder_aux(general_product(Ids,A,B),Ids,A,B). |
| 1442 | | non_unary_binder_aux(event_b_comprehension_set(Ids,A,B),Ids,A,B). |
| 1443 | | non_unary_binder_aux(lambda(Ids,A,B),Ids,A,B). |
| 1444 | | non_unary_binder_aux(let_expression(Ids,A,B),Ids,A,B). |
| 1445 | | %subst |
| 1446 | | non_unary_binder_aux(let(Ids,A,B),Ids,A,B). |
| 1447 | | non_unary_binder_aux(any(Ids,A,B),Ids,A,B). |
| 1448 | | % TO DO: add more subst |
| 1449 | | |
| 1450 | | % binders which only have a single sub-expression; here we just have to decide whether to introduce the let inside or outside |
| 1451 | | unary_binder(b(P,_Type,_I),Ids) :- |
| 1452 | | unary_binder_aux(P,Ids,_Left). |
| 1453 | | unary_binder_aux(exists(Ids,A),Ids,A). |
| 1454 | | unary_binder_aux(comprehension_set(Ids,A),Ids,A). |
| 1455 | | |
| 1456 | | |
| 1457 | | */ |