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