| 1 | | % (c) 2009-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_ast_cleanup, [clean_up/3, clean_up_pred/3, clean_up_pred_or_expr/3, |
| 6 | | clean_up_l_wo_optimizations/4, |
| 7 | | clean_up_l_with_optimizations/4, |
| 8 | | check_used_ids_info/4, recompute_used_ids_info/2, |
| 9 | | definitely_not_empty_and_finite/1, % TO DO: move to another module |
| 10 | | get_unique_id/2, |
| 11 | | predicate_level_optimizations/2]). |
| 12 | | |
| 13 | | :- use_module(module_information,[module_info/2]). |
| 14 | | :- module_info(group,typechecker). |
| 15 | | :- module_info(description,'This module implements transformations/simplifications on the AST.'). |
| 16 | | |
| 17 | | :- use_module(tools, [safe_atom_chars/3,exact_member/2,foldl/4,filter/4]). |
| 18 | | :- use_module(error_manager). |
| 19 | | :- use_module(debug). |
| 20 | | :- use_module(self_check). |
| 21 | | :- use_module(bsyntaxtree). |
| 22 | | :- use_module(translate,[print_bexpr/1]). |
| 23 | | :- use_module(btypechecker, [unify_types_strict/2]). |
| 24 | | :- use_module(preferences,[get_preference/2]). |
| 25 | | :- use_module(custom_explicit_sets,[convert_to_avl/2]). |
| 26 | | :- use_module(prob_rewrite_rules(b_ast_cleanup_rewrite_rules),[rewrite_rule_with_rename/7]). |
| 27 | | |
| 28 | | :- use_module(library(lists)). |
| 29 | | :- use_module(library(ordsets)). |
| 30 | | :- use_module(library(system), [environ/2]). |
| 31 | | |
| 32 | | % entry point for cleaning up predicates; ensures that global, predicate-level optimizations also applied |
| 33 | | clean_up_pred(Expr,NonGroundExceptions,CleanedUpExpr) :- |
| 34 | | clean_up(Expr,NonGroundExceptions,CExpr), |
| 35 | | (get_texpr_type(CExpr,pred) |
| 36 | | -> predicate_level_optimizations(CExpr,CleanedUpExpr) |
| 37 | | ; add_internal_error('Not predicate: ',clean_up_pred(Expr,NonGroundExceptions,CleanedUpExpr)), |
| 38 | | CleanedUpExpr = CExpr). |
| 39 | | |
| 40 | | % Warning: arguments swapped with clean_up for maplist ! |
| 41 | | clean_up_pred_or_expr(NonGroundExceptions,Expr,CleanedUpExpr) :- |
| 42 | | clean_up_pred_or_expr_with_path(NonGroundExceptions,Expr,CleanedUpExpr,[]). |
| 43 | | clean_up_pred_or_expr_with_path(NonGroundExceptions,Expr,CleanedUpExpr,Path) :- |
| 44 | | %print(clean_up_pred_or_expr_with_path(NonGroundExceptions,Expr,CleanedUpExpr,Path)),nl, |
| 45 | | clean_up(Expr,NonGroundExceptions,CExpr,Path), |
| 46 | | (get_texpr_type(CExpr,pred) |
| 47 | | -> predicate_level_optimizations(CExpr,CleanedUpExpr,Path) |
| 48 | | ; CleanedUpExpr = CExpr). |
| 49 | | |
| 50 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 51 | | |
| 52 | | % clean up some code afterwards |
| 53 | | clean_up(Expr,NonGroundExceptions,CExpr) :- |
| 54 | | clean_up_init(Expr,Expr1), |
| 55 | | clean_up(Expr1,NonGroundExceptions,CExpr,[]). |
| 56 | | clean_up(Expr1,NonGroundExceptions,CExpr,Path) :- |
| 57 | | get_texpr_type(Expr1,Type1), |
| 58 | | ground_type_to_any(Type1,NonGroundExceptions), |
| 59 | | (preferences:get_preference(normalize_ast,true) |
| 60 | | -> cleanups(normalize,Expr1,[],Expr2,Path) |
| 61 | | ; Expr2=Expr1), |
| 62 | | cleanups(pre,Expr2,[],TPExpr,Path), |
| 63 | | remove_bt(TPExpr,PExpr,LExpr,TLExpr), |
| 64 | | syntaxtransformation(PExpr,Subs,_,NewSubs,LExpr), |
| 65 | | functor(PExpr,F,N), |
| 66 | | % recursively clean up sub-expressions |
| 67 | | clean_up_l(Subs,NonGroundExceptions,NewSubs,F/N,1,Path), |
| 68 | | cleanups(post,TLExpr,[],CExpr,Path). |
| 69 | | %, tools_printing:print_term_summary(cleaned_up(CExpr)),nl. |
| 70 | | |
| 71 | | clean_up_init(Expr,Expr1) :- |
| 72 | | transform_bexpr(b_ast_cleanup:compute_wd_info,Expr,Expr1). % ensure that WD info is available also for pre phase |
| 73 | | |
| 74 | | :- use_module(bsyntaxtree,[transform_bexpr/3]). |
| 75 | | compute_wd_info(b(E,Type,I),b(E,Type,NInfo)) :- |
| 76 | ? | (nonmember(contains_wd_condition,I),is_possibly_undefined(E) |
| 77 | | -> NInfo = [contains_wd_condition|I] |
| 78 | | ; NInfo = I). |
| 79 | | |
| 80 | | :- use_module(library(ordsets),[ord_nonmember/2, ord_add_element/3]). |
| 81 | | % apply the clean-up rules to an expression until all |
| 82 | | % applicable rules are processed |
| 83 | | % cleanups(Phase,Expr,AppliedRules,Result,Path): |
| 84 | | % Phase: pre or post or normalize |
| 85 | | % Expr: the expression to clean up |
| 86 | | % AppliedRules: a sorted list of clean up rules that have been already applied |
| 87 | | % and must only be apply once ("single" mode) |
| 88 | | % Result: the cleaned-up expression |
| 89 | | % Path: list of outer functors leading to this expression; can be used to decide about applicability of rules |
| 90 | | cleanups(Phase,Expr,AppliedRules,Result,Path) :- |
| 91 | | %% print(cleanups(Phase,Expr,AppliedRules,Result,Path)),nl, |
| 92 | | % set up co-routines that ensure that "Rule" is not applied if |
| 93 | | % is in the list AppliedRules |
| 94 | | assure_single_rules(AppliedRules,Rule), |
| 95 | ? | ( cleanup_phase(Phase,Expr,NExpr,Mode/Rule,Path) -> % try to apply a rule (matching the current phase) |
| 96 | | ( Mode==single -> ord_add_element(AppliedRules,Rule,AppRules) %AppRules = [Rule|AppliedRules] % if the rule is marked as "single", we add to the list of already applied rules |
| 97 | | ; Mode==multi -> AppRules = AppliedRules % if "multi", we do not add it to the list, the rule might be applied more than once |
| 98 | | ; otherwise -> add_error_fail(b_ast_cleanup,'Unexpected rule mode ',Mode)), |
| 99 | | %%% print(fired_rule(Rule,Mode,Phase)),nl, %translate:print_bexpr(Expr), print(' ===> '),nl, translate:print_bexpr(NExpr),nl, print_ast(NExpr),nl, %% COMMENT IN TO SEE applied RULES <--------------- |
| 100 | | %(map_over_typed_bexpr(b_ast_cleanup:check_valid_result,NExpr) -> true ; true), % comment in to check output after every firing of a rule |
| 101 | | cleanups(Phase,NExpr,AppRules,Result,Path) % continue recursively with the new expression |
| 102 | | ; otherwise -> % if no rule matches anymore, |
| 103 | | Result = Expr, % we leave the expression unmodified |
| 104 | | Rule = none). % and unblock the co-routine (see assure_single_rules/2) |
| 105 | | |
| 106 | | %check_valid_result(b(xexists([b(identifier(msgXX),integer,_)|_],_),pred,Infos)) :- nonmember(allow_to_lift_exists,Infos),print(missing_info),nl,trace,fail. |
| 107 | | |
| 108 | | assure_single_rules([],_Rule) :- !. |
| 109 | | assure_single_rules(AppliedRules,Rule) :- |
| 110 | | assure_single_rules2(AppliedRules,Rule). |
| 111 | | :- block assure_single_rules2(?,-). |
| 112 | | assure_single_rules2(_AppliedRules,none) :- !. |
| 113 | | assure_single_rules2(AppliedRules,Rule) :- |
| 114 | | % typically AppliedRules not very long; would also do: \+ member(Rule, AppliedRules). |
| 115 | | ord_nonmember(Rule,AppliedRules). |
| 116 | | |
| 117 | | cleanup_phase(Phase,OTExpr,NTExpr,Mode/Rule,Path) :- |
| 118 | ? | create_texpr(OExpr,OType,OInfo,OTExpr), |
| 119 | ? | check_generated_info(OInfo,entry,Path), |
| 120 | ? | create_texpr(NExpr,NType,NInfo,NTExpr), |
| 121 | ? | cleanup_phase2(Phase,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path), |
| 122 | | check_generated_info(NInfo,Rule,Path). |
| 123 | | cleanup_phase2(normalize,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,_Path) :- |
| 124 | | cleanup_normalize(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule), |
| 125 | | (functor(Mode_Rule,'/',2) -> Mode_Rule = Mode/Rule, |
| 126 | | print('Rewritten: '), translate:print_bexpr(b(OExpr,OType,OInfo)),nl, |
| 127 | | print(' Into: '), translate:print_bexpr(b(NExpr,NType,NInfo)),nl |
| 128 | | ; add_internal_error('Illegal cleanup_normalize rule, missing mode: ',Mode_Rule),fail). |
| 129 | | cleanup_phase2(pre,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path) :- |
| 130 | ? | cleanup_pre_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,Path), |
| 131 | | (functor(Mode_Rule,'/',2) -> Mode_Rule = Mode/Rule |
| 132 | | ; add_internal_error('Illegal cleanup_pre rule, missing mode: ',Mode_Rule),fail). |
| 133 | | cleanup_phase2(post,OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path) :- |
| 134 | ? | cleanup_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,Path), |
| 135 | | (functor(Mode_Rule,'/',2) |
| 136 | | -> Mode_Rule = Mode/Rule %,format(' cleanup_post Rule: ~w/~w~n',[Mode,Rule]) |
| 137 | | ; add_internal_error('Illegal cleanup_post rule, missing mode: ',Mode_Rule),fail). |
| 138 | | |
| 139 | | |
| 140 | | :- if(environ(prob_safe_mode,true)). |
| 141 | | check_generated_info(Info,Rule,Path) :- select(used_ids(_),Info,I1), member(used_ids(_),I1),!, |
| 142 | | format('Illegal used ids generated by ~w within ~w~n Infos=~w~n',[Rule,Path,Info]), |
| 143 | | add_internal_error('Illegal Info generated by rule: ',Rule), |
| 144 | | fail. |
| 145 | | :- endif. |
| 146 | | check_generated_info(_,_,_). |
| 147 | | |
| 148 | | clean_up_l_wo_optimizations(Rest,NonGroundExceptions,CRest,SectionName) :- |
| 149 | | maplist(clean_up_init,Rest,Rest1), |
| 150 | | clean_up_l(Rest1,NonGroundExceptions,CRest,top_level(SectionName),1,[]). |
| 151 | | clean_up_l([],_,[],_Functor,_Nr,_Path). |
| 152 | | clean_up_l([Expr|Rest],NonGroundExceptions,[CExpr|CRest],Functor,ArgNr,Path) :- |
| 153 | | clean_up(Expr,NonGroundExceptions,CExpr,[arg(Functor,ArgNr)|Path]), |
| 154 | | A1 is ArgNr+1, |
| 155 | | clean_up_l(Rest,NonGroundExceptions,CRest,Functor,A1,Path). |
| 156 | | |
| 157 | | |
| 158 | | % MAIN ENTRY POINT for b_machine_construction, bmachine_eventb, proz |
| 159 | | % same as clean_up_l but also applies predicate_level_optimizations |
| 160 | | % Context is just the name of the section/context in which the optimizations are run |
| 161 | | clean_up_l_with_optimizations(Rest,NonGroundExceptions,CRest,Context) :- |
| 162 | | %clean_up_l(Rest,NonGroundExceptions,CRest,top_level,1,[]). |
| 163 | | clean_up_l_with_opt(Rest,NonGroundExceptions,CRest,top_level(Context),1,[]). |
| 164 | | clean_up_l_with_opt([],_,[],_Functor,_Nr,_Path). |
| 165 | | clean_up_l_with_opt([Expr|Rest],NonGroundExceptions,[CExpr|CRest],Functor,ArgNr,Path) :- |
| 166 | | clean_up_init(Expr,Expr1), |
| 167 | | clean_up_pred_or_expr_with_path(NonGroundExceptions,Expr1,CExpr,[arg(Functor,ArgNr)|Path]), |
| 168 | | A1 is ArgNr+1, |
| 169 | | clean_up_l_with_opt(Rest,NonGroundExceptions,CRest,Functor,A1,Path). |
| 170 | | |
| 171 | | :- use_module(typing_tools,[is_infinite_type/1]). |
| 172 | | :- use_module(specfile,[animation_mode/1, animation_minor_mode/1]). |
| 173 | | % cleanup_pre(OldExpr,OldType,OldInfo,NewExpr,NewType,NewInfo,Mode/Rule) |
| 174 | | |
| 175 | | |
| 176 | | % optional normalization rules |
| 177 | | % These rules are now generated using the prob_rule_compiler |
| 178 | | cleanup_normalize(Expr,Type,Info,NewExpr,NewType,NewInfo, multi/apply_normalization_rule(Rule)) :- |
| 179 | | b_ast_cleanup_rewrite_rules:normalization_rule_with_rename(Expr,Type,Info,NewExpr,NewType,NewInfo,Rule), |
| 180 | | (silent_mode(on) -> true |
| 181 | | ; format('Use rewrite_rule_normalize ~w~n',[Rule]), |
| 182 | | translate:print_bexpr(b(NewExpr,NewType,NewInfo)),nl |
| 183 | | ), |
| 184 | | (ground(NewExpr) -> true ; print(not_ground_rewrite(NewExpr)),nl,fail). |
| 185 | | |
| 186 | | never_transform_or_optimise(boolean_false). |
| 187 | | never_transform_or_optimise(boolean_true). |
| 188 | | %never_transform_or_optimise(bool_set). |
| 189 | | never_transform_or_optimise(empty_set). |
| 190 | | never_transform_or_optimise(empty_sequence). |
| 191 | | never_transform_or_optimise(falsity). |
| 192 | | %never_transform_or_optimise(max_int). |
| 193 | | %never_transform_or_optimise(min_int). |
| 194 | | never_transform_or_optimise(truth). |
| 195 | | never_transform_or_optimise(identifier(_)). |
| 196 | | never_transform_or_optimise(integer(_)). |
| 197 | | never_transform_or_optimise(string(_)). |
| 198 | | never_transform_or_optimise(value(_)). |
| 199 | | |
| 200 | | |
| 201 | | |
| 202 | | % first check for a few expressions that never need to be optimised, rewritten: |
| 203 | | cleanup_pre_with_path(E,_,_,_,_,_,_,_) :- never_transform_or_optimise(E),!,fail. |
| 204 | | % TO DO: think about enabling the following clause |
| 205 | | %cleanup_pre_with_path(exists(AllIds,P),pred,I,exists(AllIds,P),pred,NewI,single/annotate_toplevel_exists,Path) :- |
| 206 | | % Path = [H|_], % TODO: also deal with lambda and other quantifications |
| 207 | | % %print(try_mark_exists(H,AllIds)),nl, |
| 208 | | % H=arg(comprehension_set/2,1), |
| 209 | | % print(mark_exists(AllIds)),nl, |
| 210 | | % % TO DO: add some conditions under which we allow to lift |
| 211 | | % add_info_if_new(I,allow_to_lift_exists,NewI). % mark existential quantifier as outermost: no need to delay it in b_interpreter |
| 212 | | cleanup_pre_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule,_) :- |
| 213 | ? | cleanup_pre(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode_Rule). |
| 214 | | |
| 215 | | % Now cleanup_pre rules that do not require path: |
| 216 | | cleanup_pre(block(TS),subst,_,Subst,subst,Info,multi/remove_block) :- |
| 217 | | !,get_texpr_expr(TS,Subst),get_texpr_info(TS,Info). |
| 218 | | % replace finite by truth |
| 219 | | cleanup_pre(finite(S),pred,I,truth,pred,[was(finite(S))|I],multi/remove_finite) :- |
| 220 | | preferences:get_preference(disprover_mode,false), % keep finite in disprover goals |
| 221 | | get_texpr_type(S,Type), |
| 222 | | \+ is_infinite_type(Type),!. |
| 223 | | %!,(is_infinite_type(Type) -> print(keep_finite(Type)),nl,fail ; print(removed_finite(Type)),nl). |
| 224 | | /* |
| 225 | | cleanup_pre(domain(SETC),Type,I, |
| 226 | | comprehension_set(DomainIds,NewPred),Type,I,multi/dom_let_pred) :- |
| 227 | | get_texpr_expr(SETC,comprehension_set(CompIds,CompPred)), |
| 228 | | get_domain_range_ids(CompIds,DomainIds,[RangeId]), |
| 229 | | get_texpr_ids(CompIds,UnsortedIds), sort(UnsortedIds,Blacklist), |
| 230 | | conjunction_to_list(CompPred,Preds), |
| 231 | | select_equality(TId,Preds,Blacklist,Expr,Rest,_UsedIds,check_well_definedness), |
| 232 | | same_id(TId,RangeId,_), |
| 233 | | !, |
| 234 | | LetIds = [RangeId], Exprs = [Expr], |
| 235 | | conjunct_predicates(Rest,RestPred), |
| 236 | | NewPred = b(let_predicate(LetIds,Exprs,RestPred),pred,[generated(domain)]), |
| 237 | | print('Translated dom({...,x|x=E&...}) into: '), |
| 238 | | translate:print_bexpr(b(comprehension_set(DomainIds,NewPred),Type,[])),nl. |
| 239 | | */ |
| 240 | | /* strangely enough: this does not seem to buy anything: |
| 241 | | cleanup_pre(domain(SETC),Type,I, |
| 242 | | let_expression(LetIds,Exprs,NewExpr),Type,[generated(domain)|I],multi/dom_let_expr) :- |
| 243 | | get_texpr_expr(SETC,comprehension_set(CompIds,CompPred)), |
| 244 | | get_domain_range_ids(CompIds,DomainIds,[RangeId]), |
| 245 | | get_texpr_ids(CompIds,UnsortedIds), sort(UnsortedIds,Blacklist), |
| 246 | | conjunction_to_list(CompPred,Preds), |
| 247 | | select_equality(TId,Preds,Blacklist,Expr,Rest,_UsedIds,check_well_definedness), |
| 248 | | same_id(TId,RangeId,_), |
| 249 | | !, |
| 250 | | LetIds = [RangeId], Exprs = [Expr], |
| 251 | | conjunct_predicates(Rest,RestPred), |
| 252 | | get_texpr_info(SETC,CInfo), |
| 253 | | NewExpr = b(comprehension_set(DomainIds,RestPred),Type,CInfo), |
| 254 | | print('Translated dom({...,x|x=E&...}) into: '), translate:print_bexpr(b(let_expression(LetIds,Exprs,NewExpr),Type,[])),nl. |
| 255 | | */ |
| 256 | | % exchange quantified union by generalized union |
| 257 | | cleanup_pre(QUANT,Type,I, |
| 258 | | let_expression(LetIds,Exprs,NewExpr),Type,[generated(QuantOP)|I],multi/quant_union_inter_let) :- |
| 259 | | quantified_set_operator(QUANT,QuantOP,AllIds,Pred,Expr), |
| 260 | | conjunction_to_nontyping_list(Pred,Preds), |
| 261 | | % The ids are needed to build a "black list" |
| 262 | | get_sorted_ids(AllIds,Ids), |
| 263 | | find_one_point_rules(AllIds,Preds,Ids,LetIds,Exprs,RestIds,NewPreds,check_well_definedness), |
| 264 | | %print(find_one_point_rules(AllIds,Preds,Ids,LetIds,Exprs,RestIds,NewPreds)),nl, |
| 265 | | % only succeed if we found at least one id which can be rewritten as let |
| 266 | | LetIds = [_ID1|_], |
| 267 | | !, |
| 268 | | (RestIds=[],NewPreds=[] -> NewExpr=Expr |
| 269 | | % UNION(x).(x=E|Expr) --> LET x BE x=E in Expr END |
| 270 | | ; RestIds = [] -> conjunct_predicates(NewPreds,NewPred), |
| 271 | | % UNION(x).(x=E & NewPred|Expr) --> LET x BE x=E in IF NewPRED THEN Expr ELSE {} END END |
| 272 | | NewExpr = b(if_then_else(NewPred,Expr,b(empty_set,Type,[])),Type,I) |
| 273 | | ; conjunct_predicates(NewPreds,NewPred), |
| 274 | | quantified_set_operator(NewQUANT,QuantOP,RestIds,NewPred,Expr), |
| 275 | | NewExpr = b(NewQUANT,Type,I)), |
| 276 | | (debug_mode(off) -> true |
| 277 | | ; print('Translated UNION/INTER into: '), translate:print_bexpr(b(let_expression(LetIds,Exprs,NewExpr),Type,[])),nl). |
| 278 | | |
| 279 | | cleanup_pre(quantified_union(Ids,Pred,Expr),Type,I,Res,Type,[was(quantified_union)|I],multi/quant_union_symbolic) :- |
| 280 | | memberchk(prob_annotation('SYMBOLIC'),I), |
| 281 | | % UNION(Ids).(Pred|Expr) --> {u| #Ids.(Pred & u:Expr)} |
| 282 | | get_texpr_set_type(Expr,IdType), |
| 283 | | !, |
| 284 | | get_unique_id_inside('__UNION__',Pred,Expr,FRESHID), |
| 285 | | NewTID = b(identifier(FRESHID),IdType,[]), |
| 286 | | safe_create_texpr(member(NewTID,Expr),pred,Member), |
| 287 | | bsyntaxtree:create_exists_opt(Ids,[Pred,Member],Exists), |
| 288 | | Res = comprehension_set([NewTID],Exists), |
| 289 | | (debug_mode(off) -> true ; print('UNION @symbolic: '), translate:print_bexpr(b(Res,Type,I)),nl). |
| 290 | | % exchange quantified union by generalized union |
| 291 | | cleanup_pre(quantified_union(Ids,Pred,Expr),Type,I,Res,Type,I,multi/quant_union) :- |
| 292 | | !, |
| 293 | | ((get_preference(convert_comprehension_sets_into_closures,false), % for test 1101: UNION is a form of let and forces computation at the moment; translating it into a construct without union means that it may be kept symbolic |
| 294 | | singleton_set_extension(Expr,One) %, debug:bisect(Expr,[1,1,1,1,1,1,1])) % [1,1,1,1,1,1,1] slow; 1,1,0 1,1,1,0 fast |
| 295 | | ) |
| 296 | | % UNION(Ids).(Pred|{One}) --> ran( %(Ids).(Pred|One) ) |
| 297 | | -> quantified_set_op(Ids,Pred,One,quantified_intersection,I,TRes), |
| 298 | | get_texpr_expr(TRes,Res), |
| 299 | | (debug_mode(off) -> true ; print('UNION - SINGLETON: '), translate:print_bexpr(TRes),nl) |
| 300 | | ; |
| 301 | | % UNION(Ids).(Pred|Expr) --> union( ran( %(Ids).(Pred|Expr) ) ) |
| 302 | | quantified_set_op(Ids,Pred,Expr,quantified_union,I,Set), |
| 303 | | Res = general_union(Set) |
| 304 | | ). |
| 305 | | %alternate encoding: |
| 306 | | %cleanup_pre(quantified_union(Ids,Pred,Expr),Type,I,Set,Type,I,multi/quant_union) :- |
| 307 | | %poses problem to test 614, 1101 |
| 308 | | % !,quantified_union_op(Ids,Pred,Expr,Type,Set). |
| 309 | | % exchange quantified intersection by generalized intersection |
| 310 | | cleanup_pre(quantified_intersection(Ids,Pred,Expr),Type,I,general_intersection(Set),Type,I,multi/quant_inter) :- |
| 311 | | !,quantified_set_op(Ids,Pred,Expr,quantified_intersection,I,Set). |
| 312 | | % In reply to PROB-240: Check if arguments of Prj1/2 are types only using is_just_type: |
| 313 | | cleanup_pre(function(TProjection,Argument),Type,I,Result,Type,I,multi/projection_call) :- |
| 314 | | get_texpr_expr(TProjection,Projection), |
| 315 | | cleanup_function_projection(Projection,Argument,I,Result), |
| 316 | | %print(prj_fun(Result,I)),nl, |
| 317 | | !. |
| 318 | | cleanup_pre(function(Lambda,Argument),Type,I,assertion_expression(Cond,ErrMsg,Expr),Type,I,multi/lambda_guard1) :- |
| 319 | | get_texpr_expr(Lambda,LambdaExpr), |
| 320 | | is_lambda(LambdaExpr,TId,TPre,TVal), |
| 321 | | get_texpr_id(TId,ID), |
| 322 | | \+ occurs_in_expr(ID,Argument), % otherwise name clash |
| 323 | | !, % TO DO: support for functions of multiple arguments |
| 324 | | get_texpr_id(TId,Id), |
| 325 | | ErrMsg = 'lambda function called outside of domain, condition false: ', |
| 326 | | ~~mnf( replace_id_by_expr(TPre,Id,Argument,Cond) ), |
| 327 | | ~~mnf( replace_id_by_expr(TVal,Id,Argument,Expr) ). |
| 328 | | %print(assertion(expression)),nl,translate:print_bexpr(Cond),nl, translate:print_bexpr(Expr),nl. |
| 329 | | cleanup_pre(first_projection(A,B),Type,I,Set,Type,[was(prj1),prob_annotation('SYMBOLIC')|I],multi/first_projection) :- |
| 330 | | !,create_projection_set(A,B,first,Set). |
| 331 | | cleanup_pre(second_projection(A,B),Type,I,Set,Type,[was(prj2),prob_annotation('SYMBOLIC')|I],multi/second_projection) :- |
| 332 | | !,create_projection_set(A,B,second,Set). |
| 333 | | cleanup_pre(event_b_first_projection(Rel),Type,I,Set,Type,[prob_annotation('SYMBOLIC')|I],multi/ev_first_projection) :- |
| 334 | | !,create_event_b_projection_set(Rel,first,Set). |
| 335 | | cleanup_pre(event_b_second_projection(Rel),Type,I,Set,Type,[prob_annotation('SYMBOLIC')|I],multi/ev_second_projection) :- |
| 336 | | !,create_event_b_projection_set(Rel,second,Set). |
| 337 | | cleanup_pre(event_b_first_projection_v2,Type,I,Set,Type,[prob_annotation('SYMBOLIC')|I],multi/ev2_first_projection) :- |
| 338 | | !,create_event_b_projection_set_v2(Type,first,Set). % TO DO: Daniel, does this work ??? |
| 339 | | cleanup_pre(event_b_second_projection_v2,Type,I,Set,Type,[prob_annotation('SYMBOLIC')|I],multi/ev2_second_projection) :- |
| 340 | | !,create_event_b_projection_set_v2(Type,second,Set). % TO DO: Daniel, does this work ??? |
| 341 | | cleanup_pre(function(Fun,Arg),integer,I,ArithOp,integer,I,multi/succ_pred_optimisation) :- |
| 342 | | get_texpr_expr(Fun,PS), |
| 343 | | ( PS=predecessor -> Op=minus |
| 344 | | ; PS=successor -> Op=add), |
| 345 | | ArithOp =.. [Op,Arg,Integer], |
| 346 | | create_texpr(integer(1),integer,[],Integer). |
| 347 | | /* cleanup_pre(event_b_comprehension_set([ID],ID,Pred),T,I,comprehension_set([Result],NewPred),T, |
| 348 | | [was(event_b_comprehension_set)|I],multi/ev_compset_single_id) :- |
| 349 | | % Event_B_Comprehension with a single ID which is also the expression |
| 350 | | % TO DO: expand for multiple IDs |
| 351 | | !, |
| 352 | | Result = ID, NewPred=Pred. */ |
| 353 | | % Detect if_then_else; also done in cleanup_post (in pre we may be able to detect IF-THEN-ELSE before CSE has inserted lazy_lets |
| 354 | | cleanup_pre(function(IFT,DUMMYARG),Type,Info,if_then_else(IFPRED,THEN,ELSE),Type,Info,multi/function_if_then_else) :- |
| 355 | | is_if_then_else(IFT,DUMMYARG,IFPRED,THEN,ELSE), |
| 356 | | (debug_mode(off) -> true |
| 357 | | ; print('% Recognised if-then-else expression: IF '), translate:print_bexpr(IFPRED), |
| 358 | | print(' THEN '),translate:print_bexpr(THEN), print(' ELSE '),translate:print_bexpr(ELSE),nl |
| 359 | | ). |
| 360 | | cleanup_pre(event_b_comprehension_set(Ids,Expr,Pred),T,I,NewExpression,T, |
| 361 | | [was(event_b_comprehension_set)|I],multi/ev_compset) :- |
| 362 | | rewrite_event_b_comprehension_set(Ids,Expr,Pred, T, NewExpression). |
| 363 | | cleanup_pre(domain_restriction(A,B),T,I,identity(A),T,I,multi/event_b_to_normal_identity1) :- |
| 364 | | /* translate S <| id into id(S) */ |
| 365 | | is_event_b_identity(B). |
| 366 | | cleanup_pre(range_restriction(B,A),T,I,identity(A),T,I,multi/event_b_to_normal_identity2) :- |
| 367 | | /* translate id |> S into id(S) */ |
| 368 | | is_event_b_identity(B). |
| 369 | | % what about translating id(TOTAL TYPE) into event_b_identity ?? |
| 370 | | cleanup_pre(ring(A,B),T,I,composition(B,A),T,I,multi/ring_composition). |
| 371 | | cleanup_pre(minus_or_set_subtract(A,B),integer,I,minus(A,B),integer,I,multi/remove_ambiguous_minus_int). |
| 372 | | cleanup_pre(minus_or_set_subtract(A,B),set(T),I,set_subtraction(A,B),set(T),I,multi/remove_abiguous_minus_set). |
| 373 | | cleanup_pre(minus_or_set_subtract(A,B),seq(T),I,set_subtraction(A,B),seq(T),I,multi/remove_abiguous_minus_seq). |
| 374 | | cleanup_pre(mult_or_cart(A,B),integer,I,multiplication(A,B),integer,I,multi/remove_ambiguous_times_int). |
| 375 | | cleanup_pre(mult_or_cart(A,B),set(T),I,cartesian_product(A,B),set(T),I,multi/remove_ambiguous_times_set). |
| 376 | | cleanup_pre(mult_or_cart(A,B),seq(T),I,cartesian_product(A,B),seq(T),I,multi/remove_ambiguous_times_seq). |
| 377 | | cleanup_pre(E,T,Iin,E,T,Iout,multi/remove_rodinpos) :- % we use multi but can per construction only be applied once |
| 378 | | selectchk(nodeid(rodinpos(_,[],_)),Iin,Iout). % reomve rodinpos information with Name=[] |
| 379 | | cleanup_pre(partition(X,[Set]),pred,I,equal(X,Set),pred,I,multi/remove_partition_one_element) :- |
| 380 | | !, |
| 381 | | % partition(X,Set) <=> X=Set |
| 382 | | (silent_mode(on) -> true ; |
| 383 | | print('Introducing equality for partition: '), |
| 384 | | translate:print_bexpr(X), print(' = '), translate:print_bexpr(Set),nl). |
| 385 | | cleanup_pre(case(Expression,CASES,Else),subst,I,NewSubst,subst,I,single/rewrite_case_to_if_then_else) :- |
| 386 | | % translate CASE E OF EITHER e1 THEN ... ---> LET case_expr BE case_expr=E IN IF case_expr=e1 THEN ... |
| 387 | | get_texpr_type(Expression,EType), get_texpr_info(Expression,EInfo), |
| 388 | | ExprID = b(identifier(EID),EType,EInfo), |
| 389 | | (get_texpr_id(Expression,EID) |
| 390 | | -> NewSubst = if(IFLISTE) % no LET necessary |
| 391 | | ; NewSubst = let([ExprID],Equal,b(if(IFLISTE),subst,I)), |
| 392 | | get_unique_id_inside('case_expr',b(case(Expression,CASES,Else),subst,I),EID), |
| 393 | | safe_create_texpr(equal(ExprID,Expression),pred,Equal) |
| 394 | | ), |
| 395 | | (maplist(gen_if_elsif(ExprID),CASES,IFLIST) |
| 396 | | -> TRUTH = b(truth,pred,[]), get_texpr_info(Else,EI), |
| 397 | | append(IFLIST,[b(if_elsif(TRUTH,Else),subst,EI)],IFLISTE), |
| 398 | | (debug_mode(off) -> true |
| 399 | | ; print('Translating CASE to IF-THEN-ELSE: '), translate:print_bexpr(Expression),nl |
| 400 | | %,translate:print_subst(b(NewSubst,subst,[])),nl |
| 401 | | ) |
| 402 | | ; add_internal_error('Translation of CASE to IF-THEN-ELSE failed: ',CASES),fail |
| 403 | | ). |
| 404 | | cleanup_pre(exists(AllIds,P),pred,I,NewP1,pred,I,single/factor_out) :- |
| 405 | | conjunction_to_nontyping_list(P,Preds), |
| 406 | | % move things which do not depend on AllIds outside |
| 407 | | % transform, e.g., #(x).(y>2 & x=y) --> y>2 & #(x).(x=y) |
| 408 | | bsyntaxtree:create_exists_opt(AllIds,Preds,b(NewP1,pred,_I),Modified), |
| 409 | | %(Modified = true -> print(exists(AllIds)),nl,translate:print_bexpr(b(NewP1,pred,_I)),nl), |
| 410 | | % the rule will fire again on the newly generated sub predicate ! -> fix ? |
| 411 | | Modified=true.% check if anything modified; otherwise don't fire rule |
| 412 | | |
| 413 | | cleanup_pre(exists(AllIds,P),pred,_I,NewP,pred,INew,multi/remove_single_use_equality) :- |
| 414 | | % remove existentially quantified variables which are defined by an equation and are used only once |
| 415 | | % e.g., Z1...Z4 in not(#(X,Y,Z,Z1,Z2,Z3,Z4).(X:INTEGER & X*Y=Z1 & Z1*Z = Z2 & Z*X = Z3 & Z3*Y = Z4 & Z2 /= Z4)) |
| 416 | | conjunction_to_list(P,Preds), |
| 417 | | CheckWellDef=no_check, |
| 418 | ? | select_equality(TId,Preds,[],_,IDEXPR,RestPreds,_,CheckWellDef), |
| 419 | | get_texpr_id(TId,ID), |
| 420 | ? | select(TIdE,AllIds,RestIds), get_texpr_id(TIdE,ID), |
| 421 | | can_be_optimized_away(TIdE), |
| 422 | | \+ occurs_in_expr(ID,IDEXPR), % we cannot inline #x.(x=y+x & ...) |
| 423 | | always_defined_full_check_or_disprover_mode(IDEXPR), % otherwise we may remove WD issue by removing ID if Count=0 or move earlier/later if count=1 |
| 424 | | conjunct_predicates(RestPreds,RestPred), |
| 425 | | single_usage_identifier(ID,RestPred,Count), % we could also remove if Expr is simple |
| 426 | | (Count=0 -> debug_println(19,unused_equality_id(ID)), |
| 427 | | E2=RestPred |
| 428 | | ; % Count should be 1 |
| 429 | | replace_id_by_expr(RestPred,ID,IDEXPR,E2) |
| 430 | | ), |
| 431 | | conjunction_to_list(E2,PL), |
| 432 | | create_exists_opt(RestIds,PL,TNewP), |
| 433 | | (debug_mode(off) -> true |
| 434 | | ; format('Remove existentially quantified identifier with single usage: ~w (count: ~w)~n',[ID,Count]),translate:print_bexpr(IDEXPR),nl), |
| 435 | | TNewP = b(NewP,pred,INew),!. |
| 436 | | cleanup_pre(exists(AllIds,P),pred,I,let_predicate(LetIds,Exprs,NewP),pred,INew,multi/exists_to_let) :- |
| 437 | | % rewrite predicates of the form #x.(x=E & P(x)) into (LET x==E IN P(x)) |
| 438 | | % side condition for #(ids).(id=E & P(ids)): no identifiers of ids occur in E |
| 439 | | conjunction_to_nontyping_list(P,Preds), % TO DO: avoid recomputing again (see line in clause above) |
| 440 | | % The ids are needed to build a "black list" |
| 441 | | get_texpr_ids(AllIds,UnsortedIds), sort(UnsortedIds,Ids), |
| 442 | | find_one_point_rules(AllIds,Preds,Ids,LetIds,Exprs,RestIds,NewPreds,check_well_definedness), % was no_check |
| 443 | | % no_check is not ok in the context of existential quantification and reification: |
| 444 | | % #x.(1:dom(f) & x=f(1) & P) --> LET x=f(1) IN 1:dom(f) & P END |
| 445 | | % it is not ok if the whole predicate gets reified in b_intepreter_check !! Hence we use always_defined_full_check_or_disprover_mode; see Well_def_1.9.0_b5 in private_examples |
| 446 | | % only succeed if we found at least one id which can be rewritten as let |
| 447 | | LetIds = [ID1|_], |
| 448 | | !, |
| 449 | | (atomic(ID1) -> add_internal_error(cleanup_pre,unwrapped_let_identifier(ID1)), INew=I |
| 450 | | ; get_texpr_ids(LetIds,AtomicIDs), |
| 451 | | remove_used_ids_from_info(AtomicIDs,I,INew) |
| 452 | | ), % probably not necessary ?! |
| 453 | | %translate:print_bexpr(b(exists(AllIds,P),pred,[])),nl, |
| 454 | | (member(allow_to_lift_exists,I) -> AddInfos=[allow_to_lift_exists] ; AddInfos=[]), |
| 455 | | create_exists_opt(RestIds,NewPreds,AddInfos,NewP,_Modified), |
| 456 | | % print(generated_let(AtomicIDs,I)),nl, %translate:print_bexpr(P),nl, |
| 457 | | %translate:print_bexpr(b(let_predicate(LetIds,Exprs,NewP),pred,INew)),nl, |
| 458 | | debug_println(19,generated_let(AtomicIDs)). |
| 459 | | % now the same LET extraction but for universal quantification: |
| 460 | | cleanup_pre(forall(AllIds,P,Rhs),pred,I,let_predicate(LetIds,Exprs,NewP),pred,I,multi/forall_to_let) :- |
| 461 | | conjunction_to_nontyping_list(P,Preds), |
| 462 | | % The ids are needed to build a "black list" |
| 463 | | get_texpr_ids(AllIds,UnsortedIds), sort(UnsortedIds,Ids), |
| 464 | | check_forall_lhs(P,I,Ids), |
| 465 | | find_one_point_rules(AllIds,Preds,Ids,LetIds,Exprs,RestIds,NewPreds,check_well_definedness), |
| 466 | | % only succeed if we found at least one id which can be rewritten as let |
| 467 | | LetIds = [ID1|_],!, |
| 468 | | (atomic(ID1) -> add_internal_error(cleanup_pre,unwrapped_let_identifier(ID1)) ; true), |
| 469 | | conjunct_predicates(NewPreds,NewLhs), |
| 470 | | create_implication(NewLhs,Rhs,NewForallBody), |
| 471 | | create_forall(RestIds,NewForallBody,NewP), |
| 472 | | (debug_mode(on) -> print('Introduced let in forall: '), print(LetIds),nl ; true). |
| 473 | | % translate:print_bexpr(b(let_predicate(LetIds,Exprs,NewP),pred,I)),nl. % warning: used_identifier information not yet computed; translate may generate warnings |
| 474 | | cleanup_pre(exists(AllIds,P),pred,I,NewPE,pred,NewI,multi/exists_remove_typing) :- |
| 475 | ? | (is_a_conjunct(P,Typing,Q) ; is_an_implication(P,Typing,Q)), |
| 476 | | % TRUE & Q == TRUE => Q == Q |
| 477 | | is_typing_predicate(Typing), |
| 478 | | % remove typing so that other exists rules can fire |
| 479 | | % we run as cleanup_pre: the other simplifications which remove typing have not run yet |
| 480 | | % such typing conjuncts typicially come from Rodin translations |
| 481 | | create_exists_opt(AllIds,[Q],NewP), |
| 482 | | %print('Remove typing: '), translate:print_bexpr(Typing),nl, translate:print_bexpr(NewP),nl, |
| 483 | | get_texpr_expr(NewP,NewPE), |
| 484 | | add_removed_typing_info(I,NewI). |
| 485 | | cleanup_pre(exists(AllIds,P),pred,I,disjunct(NewP1,NewP2),pred,I,single/partition_exists_implication) :- |
| 486 | | is_a_disjunct_or_implication(P,Type,Q,R), |
| 487 | | /* note that even if R is only well-defined in case Q is false; it is ok to seperate this out |
| 488 | | into two existential quantifiers: #x.(x=0 or 1/x=10) is ok to transform into #x.(x=0) or #x.(1/x=10) */ |
| 489 | | % this slows down test 1452, Cylinders, 'inv3/WD'; TO DO:investigate |
| 490 | | exists_body_warning(P,I,Type), |
| 491 | | %translate:print_bexpr(b(exists(AllIds,P),pred,I)), |
| 492 | | create_exists_opt(AllIds,[Q],NewP1), % print('Q: '),translate:print_bexpr(NewP1),nl, |
| 493 | | create_exists_opt(AllIds,[R],NewP2). %, print('R: '),translate:print_bexpr(NewP2),nl. |
| 494 | | cleanup_pre(forall(AllIds,P,Rhs),pred,I,NewPred,pred,I,multi/forall_to_post_let) :- |
| 495 | | % translate something like !(x,y).(y:1..100 & x=y*y => x<=y) into !(y).(y : 1 .. 100 => (#(x).( (x)=(y * y) & x <= y))) |
| 496 | | post_let_forall(AllIds,P,Rhs,NewPred,modification), |
| 497 | | !, |
| 498 | | (debug_mode(on) -> print('POST LET INTRODUCTION: '),translate:print_bexpr(b(NewPred,pred,[])),nl ; true). |
| 499 | | cleanup_pre(set_extension(List),Type,I, value(AVL),Type,I, single/eval_set_extension) :- % TO DO: ensure we try conversion only once if it fails |
| 500 | | preferences:get_preference(try_kodkod_on_load,false), |
| 501 | | evaluate_set_extension(List,EvaluatedList), |
| 502 | | convert_to_avl(EvaluatedList,AVL), |
| 503 | | % evaluate simple explicit set extensions: avoid storing & traversing position info & AST |
| 504 | | !, |
| 505 | | (debug_mode(on) -> print('EVAL SET EXTENSION: '), translate:print_bvalue(AVL),nl ; true). |
| 506 | | cleanup_pre(sequence_extension(List),Type,I, value(AVL),Type,I, single/eval_set_extension) :- |
| 507 | | preferences:get_preference(try_kodkod_on_load,false), |
| 508 | | evaluate_set_extension(List,EvaluatedList), |
| 509 | | convert_set_to_seq(EvaluatedList,1,ESeq), |
| 510 | | convert_to_avl(ESeq,AVL), |
| 511 | | % evaluate simple explicit set extensions: avoid storing & traversing position info & AST |
| 512 | | !, |
| 513 | | (debug_mode(on) -> print('EVAL SEQUENCE EXTENSION: '), translate:print_bvalue(AVL),nl ; true). |
| 514 | | cleanup_pre(set_extension(List),Type,I, set_extension(NList),Type,I, single/remove_pos) :- |
| 515 | | remove_position_info_from_list(List,I,NList),!. |
| 516 | | cleanup_pre(sequence_extension(List),Type,I, sequence_extension(NList),Type,I, single/remove_pos) :- |
| 517 | | remove_position_info_from_list(List,I,NList),!. |
| 518 | | %cleanup_pre(concat(A,B),string,I,Res,string,I,multi/concat_assoc_reorder) :- |
| 519 | | % A = b(concat(A1,A2),string,I1), |
| 520 | | % !, % reorder STRING concats for better efficiency, can only occur when allow_sequence_operators_on_strings is true |
| 521 | | % % TO DO: extract information I2B from A2 and B |
| 522 | | % Res = concat(A1,b(concat(A2,B),string,I2B)). |
| 523 | | cleanup_pre(typeset,SType,I,Expr,SType,I,multi/remove_typeset) :- !, |
| 524 | | ( ground(SType) -> |
| 525 | | (SType=set(Type),create_type_expression2(Type,Expr) -> true |
| 526 | | ; otherwise -> |
| 527 | | add_error_and_fail(b_ast_cleanup,'Creating type expression for type set failed: ',SType)) |
| 528 | | ; otherwise -> add_error_and_fail(b_ast_cleanup,'Non-ground type for typeset expression: ',SType)). |
| 529 | | cleanup_pre(integer_set(S),Type,I,Expr,Type,[was(integer_set(S))|I],multi/remove_integer_set) :- !, |
| 530 | | translate_integer_set(S,I,Expr), |
| 531 | | (debug_mode(off) -> true |
| 532 | | ; format('Rewrite ~w to: ',[S]), |
| 533 | | translate:print_bexpr(b(Expr,integer,I)),nl). |
| 534 | | % should we move the rewrite_rules to normalize ?? |
| 535 | | cleanup_pre(Expr,Type,Info,NewExpr,NewType,NewInfo, multi/apply_rewrite_rule(Rule)) :- |
| 536 | | rewrite_rule_with_rename(Expr,Type,Info,NewExpr,NewType,NewInfo,Rule), % from b_ast_cleanup_rewrite_rules |
| 537 | | (debug_mode(off) -> true |
| 538 | | ; format('Use rewrite_rule ~w~n',[Rule]), |
| 539 | | translate:print_bexpr(b(NewExpr,NewType,NewInfo)),nl), |
| 540 | | (ground(NewExpr) -> true ; print(not_ground_rewrite(NewExpr)),nl,fail). |
| 541 | | |
| 542 | | translate_integer_set('NAT',I,interval(b(integer(0),integer,I),b(max_int,integer,I))). |
| 543 | | translate_integer_set('NAT1',I,interval(b(integer(1),integer,I),b(max_int,integer,I))). |
| 544 | | translate_integer_set('INT',I,interval(b(min_int,integer,I),b(max_int,integer,I))). |
| 545 | | %translate_integer_set('INTEGER',I,comprehension_set([b(identifier('_zzzz_unary'),integer,I)], |
| 546 | | % b(truth,pred,[prob_annotation('SYMBOLIC')|I]))). |
| 547 | | %translate_integer_set('NATURAL',I,comprehension_set([b(identifier('_zzzz_unary'),integer,I)], |
| 548 | | % b(greater_equal(b(identifier('_zzzz_unary'),integer,I), |
| 549 | | % b(integer(0),integer,I)),pred,[prob_annotation('SYMBOLIC')|I]))). |
| 550 | | %translate_integer_set('NATURAL1',I,comprehension_set([b(identifier('_zzzz_unary'),integer,I)], |
| 551 | | % b(greater_equal(b(identifier('_zzzz_unary'),integer,I), |
| 552 | | % b(integer(1),integer,I)),pred,[prob_annotation('SYMBOLIC')|I]))). |
| 553 | | |
| 554 | | % detect if an expression is equivalent to an integer set, does not check for interval yet |
| 555 | | is_integer_set(integer_set(S),S). |
| 556 | | is_integer_set(comprehension_set([b(identifier(ID),integer,_)],b(B,_,_)),S) :- %print(b(B)),nl, |
| 557 | | is_integer_set_aux(B,ID,S). |
| 558 | | is_integer_set_aux(truth,_,'INTEGER'). |
| 559 | | is_integer_set_aux(Expr,ID,Set) :- |
| 560 | | is_greater_equal(Expr,b(identifier(ID),integer,_),TNr), |
| 561 | | get_integer(TNr,Nr), |
| 562 | | (Nr=0 -> Set='NATURAL' ; Nr=1 -> Set='NATURAL1'). |
| 563 | | is_integer_set_aux(Expr,ID,Set) :- |
| 564 | | is_greater(Expr,b(identifier(ID),integer,_),TNr), |
| 565 | | get_integer(TNr,Nr), |
| 566 | | (Nr = -1 -> Set='NATURAL' ; Nr=0 -> Set='NATURAL1'). |
| 567 | | |
| 568 | | is_greater_equal(greater_equal(A,B),A,B). |
| 569 | | is_greater_equal(less_equal(B,A),A,B). |
| 570 | | is_greater(greater(A,B),A,B). |
| 571 | | is_greater(less(B,A),A,B). |
| 572 | | |
| 573 | | is_inf_integer_set_with_lower_bound(b(X,_,_),Bound) :- is_integer_set(X,N), |
| 574 | | (N='NATURAL' -> Bound=0 ; N='NATURAL1' -> Bound=1). |
| 575 | | |
| 576 | | % TODO: Some types (namely records) are still missing |
| 577 | | create_type_expression(Type,TExpr) :- |
| 578 | | create_texpr(Expr,set(Type),[],TExpr), |
| 579 | | create_type_expression2(Type,Expr). |
| 580 | | create_type_expression2(integer,integer_set('INTEGER')). |
| 581 | | create_type_expression2(boolean,bool_set). |
| 582 | | create_type_expression2(global(G),identifier(G)). |
| 583 | | create_type_expression2(string,string_set). |
| 584 | | create_type_expression2(set(T),pow_subset(Sub)) :- |
| 585 | | create_type_expression(T,Sub). |
| 586 | | create_type_expression2(couple(TA,TB),cartesian_product(A,B)) :- |
| 587 | | create_type_expression(TA,A),create_type_expression(TB,B). |
| 588 | | create_type_expression2(freetype(FT),freetype_set(FT)). |
| 589 | | |
| 590 | | is_subset(subset(A,B),A,B). |
| 591 | | is_subset(member(A,b(pow_subset(B),_,_)),A,B). % x : POW(T) <=> x <: T |
| 592 | | |
| 593 | | % tool to translate CASE values to Test predicates for IF-THEN-ELSE |
| 594 | | gen_if_elsif(CaseID,b(case_or(ListOfValues, Body),_,I), |
| 595 | | b(if_elsif(Test,Body),subst,I)) :- |
| 596 | | get_texpr_type(CaseID,T), |
| 597 | | SEXT = b(set_extension(ListOfValues),set(T),I), |
| 598 | | Test = b(member(CaseID,SEXT),pred,I). |
| 599 | | |
| 600 | | % the case below happens frequently in data validation: |
| 601 | | remove_position_info_from_list(List,I,NList) :- |
| 602 | | member(nodeid(pos(C,FilePos,Line,From,Line,To)),I), |
| 603 | | To-From > 1000, % the entire set/sequence extension is on one large line |
| 604 | | length(List,Len), Len>100, % it has many elements |
| 605 | | % we replace all position infos by the same top-level position info (enabling sharing) |
| 606 | | maplist(remove_position_info(nodeid(pos(C,FilePos,Line,From,Line,To))),List,NList), |
| 607 | | (debug_mode(off) -> true |
| 608 | | ; format('SIMPLIFY POSITION INFO IN SET/SEQUENCE EXTENSION: line # ~w, length ~w~n',[Line,Len])). |
| 609 | | remove_position_info(NI,b(Expr,Type,Infos),b(NExpr,Type,NewInfos)) :- |
| 610 | | syntaxtransformation(Expr,Subs,_Names,NSubs,NExpr), |
| 611 | ? | (select(nodeid(pos(_,_FilePos,_,_,_,_)),Infos,NT) -> NewInfos=[NI|NT] ; NewInfos=Infos), |
| 612 | | maplist(remove_position_info(NI),Subs,NSubs). |
| 613 | | |
| 614 | | % rules for function application of various projection functions |
| 615 | | cleanup_function_projection(first_projection(A,B),Argument,I,Result) :- |
| 616 | | gen_assertion_expression(A,B,Argument,first_of_pair(Argument),first,I,Result). |
| 617 | | cleanup_function_projection(second_projection(A,B),Argument,I,Result) :- |
| 618 | | gen_assertion_expression(A,B,Argument,second_of_pair(Argument),second,I,Result). |
| 619 | | cleanup_function_projection(event_b_second_projection(A),Argument,_I,Result) :- % old style Rodin projection |
| 620 | | check_is_just_type(A),Result = first_of_pair(Argument). |
| 621 | | cleanup_function_projection(event_b_second_projection(A),Argument,_I,Result) :- % old style Rodin projection |
| 622 | | check_is_just_type(A),Result = second_of_pair(Argument). |
| 623 | | cleanup_function_projection(event_b_first_projection_v2,Argument,_I,Result) :- Result = first_of_pair(Argument). |
| 624 | | cleanup_function_projection(event_b_second_projection_v2,Argument,_I,Result) :- Result = second_of_pair(Argument). |
| 625 | | |
| 626 | | check_is_just_type(_A) :- preferences:get_preference(ignore_prj_types,true),!. |
| 627 | | check_is_just_type(A) :- (is_just_type(A) -> true ; debug_println(9,not_type_for_prj(A)),fail). |
| 628 | | |
| 629 | | :- use_module(bsyntaxtree,[get_texpr_set_type/2]). |
| 630 | | gen_assertion_expression(A,B,_Argument,ProjExpr,_ProjType,_I,Result) :- |
| 631 | | check_is_just_type(A),check_is_just_type(B), |
| 632 | | !, |
| 633 | | Result = ProjExpr. |
| 634 | | % TO DO: add simplification rule for couple(x,y) : A*B with A or B being just types |
| 635 | | gen_assertion_expression(A,B,Argument,ProjExpr,ProjType,Info,Result) :- |
| 636 | | create_cartesian_product(A,B,CartAB), |
| 637 | | safe_create_texpr(member(Argument,CartAB),pred,MemCheck), |
| 638 | | ErrMsg = 'projection function called outside of domain: ', % TO DO: provide better user message with Argument result |
| 639 | | (ProjType == first -> get_texpr_set_type(A,TT) ; get_texpr_set_type(B,TT)), %% |
| 640 | | %get_texpr_pos_infos(Argument,Info), % add position infos |
| 641 | | extract_pos_infos(Info,PosInfo), |
| 642 | | safe_create_texpr(ProjExpr,TT,PosInfo,TProjExpr), |
| 643 | | Result = assertion_expression(MemCheck,ErrMsg,TProjExpr). |
| 644 | | :- use_module(bsyntaxtree,[is_set_type/2]). |
| 645 | | create_cartesian_product(A,B,CartAB) :- |
| 646 | | get_texpr_types([A,B],[STA,STB]), |
| 647 | | is_set_type(STA,TypeA), is_set_type(STB,TypeB), |
| 648 | | safe_create_texpr(cartesian_product(A,B),set(couple(TypeA,TypeB)),CartAB). |
| 649 | | |
| 650 | | % TO DO: support for functions of multiple arguments |
| 651 | | is_lambda(lambda([TId],TPred,TValue), TId, TPred,TValue). |
| 652 | | is_lambda(event_b_comprehension_set([TId],Expr,TPred), TId, TPred, TValue) :- |
| 653 | | % rewrite_event_b_comprehension_set does not seem to get called before the function/lambda rule is applied |
| 654 | | % {ID.ID|->Val | PRed} |
| 655 | | Expr = b(couple(LHS,RHS),_,_), |
| 656 | | same_texpr(LHS,TId), |
| 657 | | TValue=RHS. |
| 658 | | |
| 659 | | % rewriting Event-B comprehension sets into classical B style ones |
| 660 | | rewrite_event_b_comprehension_set(IDs,CoupleExpr,Pred, _T, NewExpression) :- |
| 661 | | % detect lambda expressions in classical B style |
| 662 | | nested_couple_to_list(CoupleExpr,List), |
| 663 | | check_ids(IDs,List,Expr),!, |
| 664 | | %print(rewriting_event_b1(IDs,Pred,Expr)),nl, |
| 665 | | NewExpression = lambda(IDs,Pred,Expr). |
| 666 | | rewrite_event_b_comprehension_set(IDList,CoupleExpr,Pred, _T, NewExpression) :- |
| 667 | | % Event_B_Comprehension with a several IDs which are also used as the couple expression |
| 668 | | nested_couple_to_list(CoupleExpr,List), %print(List),nl, |
| 669 | | List = IDList, |
| 670 | | !, |
| 671 | | NewExpression = comprehension_set(IDList,Pred). |
| 672 | | rewrite_event_b_comprehension_set(Ids,Expr,Pred, T, NewExpression) :- |
| 673 | | NewExpression = comprehension_set([Result],NewPred), |
| 674 | | unify_types_strict(T,set(Type)), |
| 675 | | % print(event_b_comprehension_set(Ids,Expr,Pred)),nl, |
| 676 | | (select(Expr,Ids,RestIds) |
| 677 | | -> % the Expr is an identifier which is part of Ids: we can avoid complicated translation below |
| 678 | | % example {f,n•n:INT & f:1..n-->Digit|f} --translated-> {f|#(n).(n:INT & f:1..n-->Digit)} |
| 679 | | % print(remove(Expr,RestIds)),nl, |
| 680 | | ExPred=Pred, Result=Expr |
| 681 | | ; get_unique_id_inside('__comp_result__',Pred,Expr,ResultId), |
| 682 | | create_texpr(identifier(ResultId),Type,[],Result), |
| 683 | | safe_create_texpr(equal(Result,Expr),pred,Equal), |
| 684 | | conjunct_predicates([Equal,Pred],ExPred), |
| 685 | | RestIds=Ids |
| 686 | | ), |
| 687 | | create_exists(RestIds,ExPred,NewPred). %, print(done_rewrite_event_b_comprehension_set),nl, translate:print_bexpr(NewPred),nl. |
| 688 | | |
| 689 | | check_ids([],[CoupleExpr],CoupleExpr). % we terminate with a single expression |
| 690 | | check_ids([ID|T],[CoupleExprID|CT],Rest) :- |
| 691 | | same_id(ID,CoupleExprID,_), |
| 692 | | check_ids(T,CT,Rest). |
| 693 | | |
| 694 | | |
| 695 | | evaluate_set_extension(List,EvaluatedList) :- |
| 696 | | List \= [], |
| 697 | | List = [_|ListT], ListT \= [], % do not do this for singleton sets so as not to prevent triggering of other rules |
| 698 | | preferences:get_preference(try_kodkod_on_load,false), |
| 699 | | maplist(eval_set_extension,List,EvaluatedList). |
| 700 | | |
| 701 | | eval_set_extension(b(E,_,_),EE) :- eval_set_extension_aux(E,EE). |
| 702 | | eval_set_extension_aux(boolean_false,pred_false). |
| 703 | | eval_set_extension_aux(boolean_true,pred_true). |
| 704 | | eval_set_extension_aux(couple(A,B),(EA,EB)) :- eval_set_extension(A,EA), eval_set_extension(B,EB). |
| 705 | | eval_set_extension_aux(integer(I),int(I)). |
| 706 | | eval_set_extension_aux(string(S),string(S)). |
| 707 | | eval_set_extension_aux(unary_minus(b(integer(I),_,_)),int(MI)) :- MI is -I. |
| 708 | | |
| 709 | | |
| 710 | | convert_set_to_seq([],_,[]). |
| 711 | | convert_set_to_seq([H|T],N,[(int(N),H)|CT]) :- N1 is N+1, convert_set_to_seq(T,N1,CT). |
| 712 | | |
| 713 | | |
| 714 | | post_let_forall(AllIds,P,Rhs,NewPred,modification) :- |
| 715 | | %print('try forall: '), translate:print_bexpr(P),nl, |
| 716 | | conjunction_to_list(P,Preds), reverse(Preds,RPreds), |
| 717 | ? | select_equality(TId,RPreds,[],_,Expr,RRest,UsedIds,no_check), |
| 718 | ? | select(TId,AllIds,RestIds), |
| 719 | | get_texpr_id(TId,Id), |
| 720 | | \+ member(Id,UsedIds), % not a recursive equality |
| 721 | | reverse(RRest,Rest), |
| 722 | | conjunct_predicates(Rest,RestPred), |
| 723 | | \+ occurs_in_expr(Id,RestPred), |
| 724 | | !, |
| 725 | | NewRhs = b(let_predicate([TId],[Expr],Rhs),pred,[]), |
| 726 | | post_let_forall(RestIds,RestPred,NewRhs,NewPred,_). |
| 727 | | post_let_forall(AllIds,P,Rhs,NewPred, no_modification) :- |
| 728 | | create_implication(P,Rhs,NewForallBody), |
| 729 | | create_forall(AllIds,NewForallBody,NewP), |
| 730 | | get_texpr_expr(NewP,NewPred). |
| 731 | | |
| 732 | | |
| 733 | | is_interval(b(interval(A,B),_,_),A,B). |
| 734 | | |
| 735 | | % a more flexible version, also detecting singleton set extension |
| 736 | | is_interval_or_singleton(I,A,B) :- is_interval(I,A,B),!. |
| 737 | | is_interval_or_singleton(b(set_extension([A]),set(integer),_),A,A). |
| 738 | | |
| 739 | | is_empty_set(b(ES,_,_)) :- is_empty_set_aux(ES). |
| 740 | | is_empty_set_aux(empty_set). |
| 741 | | is_empty_set_aux(empty_sequence). |
| 742 | | is_empty_set_aux(domain(D)) :- is_empty_set(D). |
| 743 | | is_empty_set_aux(range(D)) :- is_empty_set(D). |
| 744 | | |
| 745 | | % create a lambda expression for a projection |
| 746 | | create_projection_set(A,B,_Switch,Res) :- |
| 747 | | (is_empty_set(A) ; is_empty_set(B)),!, |
| 748 | | Res = empty_set. |
| 749 | | create_projection_set(A,B,Switch,lambda(Ids,SPred,Expr)) :- % generate lambda to be able to use function(lambda) rule |
| 750 | | Ids = [TArg1,TArg2], |
| 751 | | ( Switch==first -> Expr = TArg1 |
| 752 | | ; Switch==second -> Expr = TArg2), |
| 753 | | get_texpr_type(A,TA1), unify_types_strict(TA1,set(Type1)), |
| 754 | | get_texpr_type(B,TB2), unify_types_strict(TB2,set(Type2)), |
| 755 | | (contains_no_ids(A,B) -> Arg1 = '_zzzz_unary', Arg2 = '_zzzz_binary' % avoid generating fresh ids; relevant for test 1313 and ticket PROB-346 |
| 756 | | % TO DO: check whether _zzzz_unary/binary are actually used; we should avoid generating fresh ids whenever possible (otherwise syntactically identical formulas become different) |
| 757 | | ; get_unique_id_inside('_prj_arg1__',A,B,Arg1), |
| 758 | | get_unique_id_inside('_prj_arg2__',A,B,Arg2)), |
| 759 | | create_texpr(identifier(Arg1),Type1,[generated(Switch)],TArg1), |
| 760 | | create_texpr(identifier(Arg2),Type2,[generated(Switch)],TArg2), |
| 761 | | safe_create_texpr(member(TArg1,A),pred,MembA), |
| 762 | | safe_create_texpr(member(TArg2,B),pred,MembB), |
| 763 | | conjunct_predicates([MembA,MembB],Pred), SPred=Pred. |
| 764 | | % bsyntaxtree:mark_bexpr_as_symbolic(Pred,SPred). % TO DO: put mark code into another module; maybe only mark as symbolic if types large enough ?? |
| 765 | | |
| 766 | | contains_no_ids(A,B) :- contains_no_ids(A), contains_no_ids(B). |
| 767 | | contains_no_ids(b(E,_,_)) :- contains_no_ids_aux(E). |
| 768 | | contains_no_ids_aux(bool_set). |
| 769 | | contains_no_ids_aux(X) :- is_integer_set(X,_). % comprehension set may contain ids, but not visible to outside |
| 770 | | contains_no_ids_aux(mult_or_cart(A,B)) :- contains_no_ids(A),contains_no_ids(B). |
| 771 | | contains_no_ids_aux(relations(A,B)) :- contains_no_ids(A),contains_no_ids(B). |
| 772 | | contains_no_ids_aux(pow_subset(A)) :- contains_no_ids(A). |
| 773 | | contains_no_ids_aux(string_set). |
| 774 | | contains_no_ids_aux(interval(A,B)) :- contains_no_ids(A),contains_no_ids(B). |
| 775 | | % TO DO: add more |
| 776 | | |
| 777 | | create_event_b_projection_set(Rel,Switch,lambda(Ids,SPred,Expr)) :- |
| 778 | | Ids = [TArg1,TArg2], |
| 779 | | ( Switch==first -> Expr = TArg1 |
| 780 | | ; Switch==second -> Expr = TArg2), |
| 781 | | get_texpr_type(Rel,RT),unify_types_strict(RT,set(couple(Type1,Type2))), |
| 782 | | get_unique_id_inside('_prj_arg1__',Rel,Arg1), |
| 783 | | get_unique_id_inside('_prj_arg2__',Rel,Arg2), |
| 784 | | create_texpr(identifier(Arg1),Type1,[generated(Switch)],TArg1), |
| 785 | | create_texpr(identifier(Arg2),Type2,[generated(Switch)],TArg2), |
| 786 | | create_texpr(couple(TArg1,TArg2),couple(Type1,Type2),[],Couple), |
| 787 | | safe_create_texpr(member(Couple,Rel),pred,Member), |
| 788 | | SPred=Member. |
| 789 | | %bsyntaxtree:mark_bexpr_as_symbolic(Pred,SPred). |
| 790 | | |
| 791 | | create_event_b_projection_set_v2(RelType,Switch,comprehension_set(Ids,SPred)) :- |
| 792 | | % we are generating {p1,p2,lambda | lambda=p1/p2} |
| 793 | | Ids = [TArg1,TArg2,TArg3], |
| 794 | | ( Switch==first -> ResultExpr = TArg1, Type1 = Type3 |
| 795 | | ; Switch==second -> ResultExpr = TArg2, Type2 = Type3), |
| 796 | | unify_types_strict(RelType,set(couple(couple(Type1,Type2),T3))), |
| 797 | | (T3==Type3 -> true ; add_error(create_event_b_projection_set,'Unexpected return type: ',T3)), |
| 798 | | %print(types(Type1,Type2,Type3)),nl, |
| 799 | | Arg1 = '_zzzz_unary', |
| 800 | | Arg2 = '_zzzz_binary', |
| 801 | | Arg3 = '_lambda_result_', % the comprehension set contains no other expressions: no clash possible |
| 802 | | create_texpr(identifier(Arg1),Type1,[generated(Switch)],TArg1), |
| 803 | | create_texpr(identifier(Arg2),Type2,[generated(Switch)],TArg2), |
| 804 | | create_texpr(identifier(Arg3),Type3,[lambda_result,generated(Switch)],TArg3), |
| 805 | | safe_create_texpr(equal(TArg3,ResultExpr),pred,[lambda_result],Equal), |
| 806 | | conjunct_predicates([Equal],Pred), |
| 807 | | SPred=Pred. |
| 808 | | % bsyntaxtree:mark_bexpr_as_symbolic(Pred,SPred). |
| 809 | | %,print(Pred),nl. |
| 810 | | |
| 811 | | :- use_module(btypechecker,[couplise_list/2,prime_identifiers/2,prime_identifiers0/2, prime_atom0/2]). |
| 812 | | % create a comprehension set for quantified union or intersection UNION(x).(P|E) = ran(%x.(P|E)) |
| 813 | | % TO DO: translate UNION into UNION(x).(P|E) = dom({r,x|P & r:E}) = ran({x,r|P & r:E}) which is considerably faster |
| 814 | | % also works for e.g., UNION(x).(x:1..2|{x+y}) = 12..13 |
| 815 | | %quantified_union_op(Ids,Pred,Expr,SetType,Res) :- is_set_type(SetType,Type), |
| 816 | | % !, |
| 817 | | % Info = [generated(quantified_union)], |
| 818 | | % get_unique_id_inside('_zzzz_unary',Pred,Expr,FRESHID), % also include Expr ! |
| 819 | | % NewID = b(identifier(FRESHID),Type,[]), %fresh |
| 820 | | % append(Ids,[NewID],NewIds), |
| 821 | | % safe_create_texpr(member(NewID,Expr),pred,[],Member), |
| 822 | | % conjunct_predicates([Pred,Member],Body), |
| 823 | | % get_texpr_types(NewIds,Types),couplise_list(Types,TupleType), |
| 824 | | % safe_create_texpr(comprehension_set(NewIds,Body),set(TupleType),Info,ComprSet), |
| 825 | | % Res = range(ComprSet). |
| 826 | | % %safe_create_texpr(range(ComprSet),set(set(Type)),Info,Set),translate:print_bexpr(Set),nl. |
| 827 | | %quantified_union_op(Ids,Pred,Expr,SetType,Set) :- |
| 828 | | % add_internal_error('Could not translate quantified UNION operator: ',quantified_union_op(Ids,Pred,Expr,SetType,Set)), |
| 829 | | % fail. |
| 830 | | |
| 831 | | % create a comprehension set for quantified union or intersection INTER(x).(P|E) = inter(ran(%x.(P|E))) |
| 832 | | % UNION could be treated by quantified_union_op above |
| 833 | | quantified_set_op(Ids,Pred,Expr,Loc,OuterInfos,Set) :- |
| 834 | | create_range_lambda(Ids,Pred,Expr,Loc,OuterInfos,Set), |
| 835 | | !. % , print(quantified),nl,translate:print_bexpr(Set),nl. |
| 836 | | quantified_set_op(Ids,Pred,Expr,Loc,OuterInfos,Set) :- |
| 837 | | add_internal_error('Could not translate quantified set operator: ', |
| 838 | | quantified_set_op(Ids,Pred,Expr,Loc,OuterInfos,Set)), |
| 839 | | fail. |
| 840 | | |
| 841 | | create_range_lambda(Ids,Pred,Expr,Loc,OuterInfos,Set) :- |
| 842 | | Info = [generated(Loc)|OuterInfos], |
| 843 | | get_texpr_types(Ids,Types),couplise_list(Types,ArgType), |
| 844 | | get_texpr_type(Expr,ExprType), |
| 845 | | safe_create_texpr(lambda(Ids,Pred,Expr),set(couple(ArgType,ExprType)),Info,Lambda), |
| 846 | | safe_create_texpr(range(Lambda),set(ExprType),Info,Set). |
| 847 | | |
| 848 | | |
| 849 | | quantified_set_operator(quantified_union(AllIds,Pred,Expr),quantified_union,AllIds,Pred,Expr). |
| 850 | | quantified_set_operator(quantified_intersection(AllIds,Pred,Expr),quantified_intersection,AllIds,Pred,Expr). |
| 851 | | |
| 852 | | :- use_module(tools_strings,[ajoin/2]). |
| 853 | | exists_body_warning(_,_,_) :- preferences:get_preference(disprover_mode,true),!. |
| 854 | | exists_body_warning(_,_,_) :- animation_minor_mode(eventb),!. |
| 855 | | exists_body_warning(_,I,_) :- member(removed_typing,I),!. |
| 856 | | exists_body_warning(P,_,_) :- get_texpr_info(P,PI),member(was(_),PI),!. % it was something else |
| 857 | | exists_body_warning(P,I,Type) :- |
| 858 | | translate:translate_bexpression(P,PS), |
| 859 | | ajoin(['Warning: body of existential quantifier is a ',Type, |
| 860 | | ' (not allowed by Atelier-B): '],Msg), |
| 861 | | (contains_info_pos(I) -> Pos=I ; Pos=P), |
| 862 | | add_warning(b_ast_cleanup,Msg,PS,Pos). |
| 863 | | |
| 864 | | :- use_module(tools_strings,[ajoin_with_sep/3]). |
| 865 | | % we ensure that this check is only done once, for user machines,... not for generated formulas |
| 866 | | check_forall_lhs(_,_,_) :- preferences:get_preference(perform_stricter_static_checks,false),!. |
| 867 | | check_forall_lhs(_,_,_) :- preferences:get_preference(disprover_mode,true),!. |
| 868 | | check_forall_lhs(_,_,_) :- animation_minor_mode(eventb),!. % typing predicates get removed it seems |
| 869 | ? | check_forall_lhs(_,I,_) :- member(removed_typing,I),!. % means that typing was possibly removed |
| 870 | ? | check_forall_lhs(P,_,_) :- member_in_conjunction(PC,P),get_texpr_info(PC,PI),member(II,PI),removed_typing(II),!. % it was something else; does not seem to detect all removed conjunctions, hence we also check I above |
| 871 | | check_forall_lhs(P,I,Ids) :- find_identifier_uses(P,[],LhsUsed), |
| 872 | | ord_subtract(Ids,LhsUsed,NotDefined), |
| 873 | | (NotDefined=[] -> true |
| 874 | | ; ajoin_with_sep(NotDefined,',',S), |
| 875 | | translate:translate_bexpression(P,PS), |
| 876 | | ajoin(['Left-hand-side "', PS, '" of forall does not define identifier(s): '],Msg), |
| 877 | | add_warning(b_ast_cleanup,Msg,S,I)). |
| 878 | | removed_typing(removed_typing). removed_typing(was(_)). |
| 879 | | |
| 880 | | :- use_module(kernel_records,[normalise_record_type/2]). |
| 881 | | :- use_module(library(lists),[last/2]). |
| 882 | | |
| 883 | | % first the rules that require the path: |
| 884 | | cleanup_post_with_path(assign([b(identifier(ID),TYPE,INFO)],[EXPR]),subst,I, |
| 885 | | assign_single_id(b(identifier(ID),TYPE,INFO),EXPR),subst,I,single/assign_single_id,Path) :- |
| 886 | | \+ animation_minor_mode(eventb), % there is no support in the Event-B interpreter for assign_single_id yet |
| 887 | ? | (simple_expression(EXPR) % the assign_single_id is not guarded by a waitflag; EXPR should not be too expensive too calculate |
| 888 | | -> true |
| 889 | | ; % if we are in an unguarded context; then we do not need to guard EXPR by waitflag anyway |
| 890 | ? | maplist(unguarded,Path) |
| 891 | | ), |
| 892 | | !, |
| 893 | | (debug_mode(on) -> print('Single Assignment: '), |
| 894 | | translate:print_subst(b(assign([b(identifier(ID),TYPE,INFO)],[EXPR]),subst,I)),nl |
| 895 | | ; true). |
| 896 | | cleanup_post_with_path(any(Ids,Pred,Subst),subst,Info,any(Ids,Pred,NewSubst),subst,NewInfo,multi/remove_useless_assign,_Path) :- |
| 897 | | get_preference(optimize_ast,true), |
| 898 | ? | member_in_conjunction(b(equal(TID1,TID2),pred,_),Pred), |
| 899 | | get_texpr_id(TID1,ID1), |
| 900 | | get_texpr_id(TID2,ID2), % we have an equality of the form x=x' (as generated by TLA2B) |
| 901 | | delete_assignment(Subst,TID3,TID4,NewSubst), |
| 902 | | get_texpr_id(TID4,ID4), get_texpr_id(TID3,ID3), |
| 903 | | ( c(ID1,ID2) = c(ID3,ID4) ; c(ID1,ID2) = c(ID4,ID3)), % we have an assignment x:=x' or x':=x |
| 904 | | % the cleanup rule recompute_accessed_vars below recomputes the info fields for enclosing operations! get_accessed_vars is currently called before ast_cleanup |
| 905 | | debug_format(19,'Delete useless assignment ~w := ~w~n',[ID3,ID4]), |
| 906 | | (member(removed_useless_assign,Info) -> NewInfo=Info ; NewInfo=[removed_useless_assign|Info]). |
| 907 | | cleanup_post_with_path(operation(TName,Res,Params,TBody),Type,Info, |
| 908 | | operation(TName,Res,Params,NewTBody),Type,NewInfos,single/recompute_accessed_vars,_Path) :- |
| 909 | | TBody=b(Body,subst,BInfos), |
| 910 | | select(removed_useless_assign,BInfos,NewBInfos), |
| 911 | | btypechecker:compute_accessed_vars_infos_for_operation(TName,Res,Params,TBody,Modifies,_,_,NewRWInfos), |
| 912 | | debug_format(19,'Recomputing read/write infos for ~w (~w)~n',[TName,Modifies]), |
| 913 | | update_infos(NewRWInfos,Info,NewInfos), |
| 914 | | NewTBody=b(Body,subst,NewBInfos). |
| 915 | | cleanup_post_with_path(any(Ids,Pred,Subst),subst,I,Result,subst,[generated|I],single/transform_any_into_let,Path) :- |
| 916 | | (last(Path,arg(top_level(_),_)) /* do not remove top-level ANY if show_eventb_any_arguments is true; see, e.g., test 1271 */ |
| 917 | | -> preferences:preference(show_eventb_any_arguments,false) ; true), |
| 918 | | find_lets(Ids,Pred,LetIDs,LetDefs,RestIds,RestPred), |
| 919 | | LetIDs \= [], |
| 920 | | % print(found_lets(LetIDs,RestIds,RestPred)),nl,print(Path),nl, |
| 921 | | conjunct_predicates(LetDefs,LetDefPred), |
| 922 | | (RestIds = [], is_truth(RestPred) % complete ANY can be translated to LET |
| 923 | | -> Result = let(LetIDs,LetDefPred,Body), Body = Subst |
| 924 | | ; split_predicate(RestPred,Ids,RestUsingIds,RestNotUsingIds), |
| 925 | | % print('USING: '),translate:print_bexpr(RestUsingIds),nl, print('NOT USING: '),translate:print_bexpr(RestNotUsingIds),nl, |
| 926 | | (RestIds = [] |
| 927 | | -> (is_truth(RestUsingIds) |
| 928 | | % RestPred does not use the LET identifiers; move outside of the LET ! |
| 929 | | -> Result = select([b(select_when(RestPred,SelectBody),subst,[generated|I])]), |
| 930 | | SelectBody = b(let(LetIDs,LetDefPred,Subst),subst,[generated|I]) |
| 931 | | ; is_truth(RestNotUsingIds) |
| 932 | | % RestPred uses LET identifiers in all conjuncts; move inside LET |
| 933 | | -> Result = let(LetIDs,LetDefPred,LetBody), |
| 934 | | LetBody = b(select([b(select_when(RestPred,Subst),subst,[])]),subst,[generated|I]) |
| 935 | | ; otherwise |
| 936 | | % we would need to generate an outer and inner select; transformation probably not worth it |
| 937 | | -> fail |
| 938 | | ) |
| 939 | | ; is_truth(RestUsingIds) |
| 940 | | % RestPred does not use LET identifiers move outside of LET |
| 941 | | -> Result = any(RestIds,RestPred,SelectBody), |
| 942 | | SelectBody = b(let(LetIDs,LetDefPred,Subst),subst,[generated|I]) |
| 943 | | ; is_truth(RestNotUsingIds) |
| 944 | | % RestPred uses LET identifiers in all conjuncts; move inside LET |
| 945 | | -> Result = let(LetIDs,LetDefPred,LetBody), |
| 946 | | LetBody = b(any(RestIds,RestPred,Subst),subst,I) |
| 947 | | ; otherwise |
| 948 | | % we would need to generate an outer and inner any; transformation probably not worth it |
| 949 | | -> fail |
| 950 | | ) |
| 951 | | ), |
| 952 | | !. %,translate:print_subst(b(Result,subst,[])),nl. |
| 953 | | cleanup_post_with_path(operation(TName,Res,Params,Body),Type,Info, |
| 954 | | operation(TName,Res,Params,NewBody),Type,Info,single/lts_min_guard_splitting,Path) :- |
| 955 | | (get_preference(ltsmin_guard_splitting,true) ; \+ get_preference(pge,off)), % equivalent to pge_algo:is_pge_opt_on), |
| 956 | | Path = [arg(top_level(operation_bodies),_)], % only apply at top-level |
| 957 | | % TO DO: also apply for Event-B models |
| 958 | | get_texpr_id(TName,Name), |
| 959 | | (predicate_debugger:get_operation_propositional_guards(Name,Res,Params,Body,Guards,RestBody) |
| 960 | | -> true |
| 961 | | ; add_warning(ltsmin_guard_splitting,'Cannot extract guard for:',Name),fail), |
| 962 | | Guards \= [], |
| 963 | | conjunct_predicates(Guards,G), |
| 964 | | get_texpr_info(Body,BInfo), |
| 965 | | NewBody = b(precondition(G,RestBody),subst,[prob_annotation('LTSMIN-GUARD')|BInfo]), % a SELECT would be more appropriate |
| 966 | | (debug_mode(off) -> true |
| 967 | | ; format('Extracting LTS Min guard for ~w~n',[Name]),translate:print_subst(NewBody),nl). |
| 968 | | cleanup_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path) :- |
| 969 | | get_preference(optimize_ast,true), |
| 970 | | cleanup_post_ne_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,Path). |
| 971 | | cleanup_post_with_path(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule,_Path) :- |
| 972 | ? | cleanup_post_essential(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule). |
| 973 | | |
| 974 | | % delete an assignment from a substitution |
| 975 | | delete_assignment(b(assign(LHS,RHS),subst,Info),ID,IDRHS,b(RES,subst,Info)) :- |
| 976 | | nth1(Pos,LHS,ID,RestLHS), |
| 977 | | nth1(Pos,RHS,IDRHS,RestRHS), |
| 978 | | (RestLHS = [] -> RES = skip ; RES = assign(RestLHS,RestRHS)). |
| 979 | | % TO DO: also deal with parallel and possibly other constructs assign_single_id,... |
| 980 | | |
| 981 | | %unguarded(arg(sequence/1,1)). % first argument of sequence is not guarded |
| 982 | ? | unguarded(arg(X,_)) :- unguarded_aux(X). |
| 983 | | unguarded_aux(top_level(_)). |
| 984 | | unguarded_aux(operation/4). |
| 985 | | unguarded_aux(parallel/1). |
| 986 | | unguarded_aux(var/2). |
| 987 | | unguarded_aux(let/3). |
| 988 | | % what about choice/2 ?? |
| 989 | | |
| 990 | | :- load_files(library(system), [when(compile_time), imports([environ/2])]). |
| 991 | | |
| 992 | | |
| 993 | | % --------------------- |
| 994 | | |
| 995 | | % now the rules which do not need the Path |
| 996 | | |
| 997 | | % first check for a few expressions that never need to be optimised, rewritten: |
| 998 | | cleanup_post_essential(E,_,_,_,_,_,_) :- never_transform_or_optimise(E),!,fail. |
| 999 | | |
| 1000 | | cleanup_post_essential(Expr,Type,I,Expr,Type,I2,single/remove_erroneous_info_field) :- |
| 1001 | | \+ ground(I),!, |
| 1002 | | functor(Expr,F,_N), |
| 1003 | | add_internal_error('Information field not ground: ',I:F), |
| 1004 | | I2=[]. |
| 1005 | | :- if(environ(prob_safe_mode,true)). |
| 1006 | | cleanup_post_essential(comprehension_set(Ids,E),Type,I,comprehension_set(Ids,E),Type,I,single/sanity_check) :- |
| 1007 | | get_texpr_ids(Ids,UnsortedIds),sort(UnsortedIds,SIds), |
| 1008 | | \+ same_length(UnsortedIds,SIds), |
| 1009 | | add_error(cleanup_post,'Identifier clash in comprehension set: ',UnsortedIds), |
| 1010 | | print(E),nl, |
| 1011 | | fail. |
| 1012 | | :- endif. |
| 1013 | | %cleanup_post(block(TS),subst,_,Subst,subst,Info,multi/remove_block) :- |
| 1014 | | % !,get_texpr_expr(TS,Subst),get_texpr_info(TS,Info). |
| 1015 | | cleanup_post_essential(Expr,Type,I,Expr,NType,I,single/normalise_record_type) :- |
| 1016 | | nonvar(Type),Type=record(Fields), |
| 1017 | | normalise_record_type(record(Fields),NType), |
| 1018 | | NType \== Type, |
| 1019 | | !. |
| 1020 | | |
| 1021 | | cleanup_post_essential(lambda(Ids,Pred,Expr),Type,I, comprehension_set(CompIds,CompPred),Type,NewInfo,multi/remove_lambda) :- !, |
| 1022 | | NewInfo = I, % was NewInfo = [was(lambda)|I], |
| 1023 | | unify_types_strict(Type,set(couple(_ArgType,ResType))), |
| 1024 | | %ResultId = '_lambda_result_', |
| 1025 | | get_unique_id_inside('_lambda_result_',Pred,Expr,ResultId), |
| 1026 | | % get_unique_id('_lambda_result_',ResultId), |
| 1027 | | def_get_texpr_id(Result,ResultId), |
| 1028 | | get_texpr_type(Result,ResType), |
| 1029 | | get_texpr_info(Result,[lambda_result]), |
| 1030 | | append(Ids,[Result],CompIds), |
| 1031 | | get_texpr_expr(Equal,equal(Result,Expr)), |
| 1032 | | get_texpr_type(Equal,pred), |
| 1033 | | extract_important_info_from_subexpression(Expr,EqInfo), % mark equality with wd condition if Expr has wd condition |
| 1034 | | get_texpr_info(Equal,[lambda_result|EqInfo]), |
| 1035 | | conjunct_predicates_with_pos_info(Pred,Equal,CompPred0), |
| 1036 | | add_texpr_infos(CompPred0,[prob_annotation('LAMBDA')],CompPred). |
| 1037 | | |
| 1038 | | cleanup_post_essential(reflexive_closure(Rel),Type,I, UNION,Type,NewInfo,multi/remove_reflexive_closure) :- !, |
| 1039 | | NewInfo = [was(reflexive_closure)|I], |
| 1040 | | safe_create_texpr(closure(Rel),Type,I,CL), |
| 1041 | | UNION = union(b(event_b_identity,Type,IdInfo), CL), % closure(R) = id \/ closure1(R) |
| 1042 | | (is_infinite_type(Type) -> IdInfo = [prob_annotation('SYMBOLIC')|I] ; IdInfo =I), |
| 1043 | | (debug_mode(on) -> print('Rewriting closure to: '), translate:print_bexpr(b(UNION,Type,[])),nl ; true). |
| 1044 | | cleanup_post_essential(evb2_becomes_such(Ids,Pred),subst,I,becomes_such(Ids,Pred2),subst,I,multi/ev2_becomes_such) :- |
| 1045 | | % we translate a Classical-B becomes_such with id -> id$0, id' -> id |
| 1046 | | % classical B: Dec = BEGIN level : (level>=0 & level> level$0-5 & level < level$0) END |
| 1047 | | % Event-B: level'>= 0, level' > level-5 ... |
| 1048 | | !, |
| 1049 | | prime_identifiers(Ids,PIds), |
| 1050 | | maplist(gen_rename,PIds,Ids,RenameList1), % id' -> id |
| 1051 | | prime_identifiers0(Ids,PIds0), |
| 1052 | | maplist(gen_rename,Ids,PIds0,RenameList2), % id -> id$0 |
| 1053 | | append(RenameList1,RenameList2,RenameList), |
| 1054 | | rename_bt(Pred,RenameList,Pred2), |
| 1055 | | (debug_mode(off) -> true |
| 1056 | | ; format('Converting Event-B becomes_such: ',[]),translate:print_bexpr(Pred2),nl). |
| 1057 | | cleanup_post_essential(successor,Type,I,Compset,Type,[was(successor)|I],multi/successor) :- !, |
| 1058 | | % translation of succ |
| 1059 | | pred_succ_compset(add,Compset). |
| 1060 | | cleanup_post_essential(concat(A,B),string,I,ExtFunCall,string,[was(concat)|I],multi/concat_for_string) :- !, |
| 1061 | | % translation of concat (^) for STRINGs, this can only occur when allow_sequence_operators_on_strings is true |
| 1062 | | ExtFunCall = external_function_call('STRING_APPEND',[A,B]). |
| 1063 | | % TO DO: we could translate size(X),string to STRING_LENGTH |
| 1064 | | cleanup_post_essential(predecessor,Type,I,Compset,Type,[was(predecessor)|I],multi/predecessor) :- !, |
| 1065 | | % translation of pred |
| 1066 | | pred_succ_compset(minus,Compset). |
| 1067 | | cleanup_post_essential(becomes_such(Ids1,Pred),subst,I,becomes_such(Ids2,Pred),subst,I,single/becomes_such) :- !, |
| 1068 | | annotate_becomes_such_vars(Ids1,Pred,Ids2). |
| 1069 | | cleanup_post_essential(Expr,Type,I,Expr,Type,[contains_wd_condition|I],multi/possibly_undefined) :- |
| 1070 | | % multi: rule can only be applied once anyway, no need to check |
| 1071 | | nonmember(contains_wd_condition,I), |
| 1072 | | % print(' - CHECK WD: '), translate:print_bexpr(Expr),nl, %% |
| 1073 | | is_possibly_undefined(Expr),!, |
| 1074 | | %% print('CONTAINS WD: '), translate:print_bexpr(Expr),nl, %% |
| 1075 | | %(translate:translate_bexpression(Expr,'{min(xunits)}') -> trace ; true), |
| 1076 | | true. |
| 1077 | | % if a substitution has a sub-expression that is a substitution with that refers to the original |
| 1078 | | % value of a variable, we mark this substitution, too. |
| 1079 | | |
| 1080 | | % If the substitution of an operation contains a while whose invariant contains references x$0 |
| 1081 | | % to the original value of a variable x, we must insert a LET substitution to preserve the original value. |
| 1082 | | cleanup_post_essential(operation(Id,Results,Args,Body),Type,I,operation(Id,Results,Args,NewBody),Type,I,single/refers_to_old_state_let) :- |
| 1083 | | get_texpr_info(Body,BodyInfo), |
| 1084 | | memberchk(refers_to_old_state(References),BodyInfo),!, |
| 1085 | | create_equalities_for_let(References,Ids,Equalities), |
| 1086 | | conjunct_predicates(Equalities,P), |
| 1087 | | insert_let(Body,Ids,P,NewBody). |
| 1088 | | cleanup_post_essential(Subst,subst,I,Subst,subst,NI,single/refers_to_old_state) :- |
| 1089 | | safe_syntaxelement(Subst,Subs,_,_,_), |
| 1090 | | % check if a child contains the refers_to_old_state flag |
| 1091 | | setof(Reference, (member(Sub,Subs), |
| 1092 | | get_texpr_info(Sub,SubInfo), |
| 1093 | | memberchk(refers_to_old_state(References),SubInfo), |
| 1094 | | member(Reference,References)), ReferedIds), |
| 1095 | | !, |
| 1096 | | sort(ReferedIds,SortedIds), |
| 1097 | | NI = [refers_to_old_state(SortedIds)|I]. |
| 1098 | | |
| 1099 | | cleanup_post_essential(let_predicate([],[],TExpr),Type,Iin,Expr,Type,Iout,multi/remove_let_predicate) :- !, |
| 1100 | | % same as above, just for predicates |
| 1101 | | get_texpr_expr(TExpr,Expr), |
| 1102 | | get_texpr_info(TExpr,I), debug_println(9,removed_let_predicate), |
| 1103 | | % The next is done to prevent removing position information (in case of Event-B invariants) |
| 1104 | | ( nonmember(nodeid(_),I), member(nodeid(P),Iin) -> Iout = [nodeid(P)|I] |
| 1105 | | ; otherwise -> Iout = I). |
| 1106 | | |
| 1107 | | |
| 1108 | | cleanup_post_essential(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule) :- |
| 1109 | ? | get_preference(optimize_ast,true), |
| 1110 | ? | cleanup_post(OExpr,OType,OInfo,NExpr,NType,NInfo,Mode/Rule). |
| 1111 | | |
| 1112 | | % moved these rule below the simplifciation rules above to avoid re-computing used_id infos |
| 1113 | | cleanup_post_essential(forall(Ids,Lhs,Rhs),pred,IOld,Res,pred,INew,single/forall_used_identifier) :- |
| 1114 | | construct_inner_forall(Ids,Lhs,Rhs,IOld, b(Res,pred,INew)). |
| 1115 | | cleanup_post_essential(exists(Ids,P),pred,IOld,exists(Ids,NP),pred,ResInfo,single/exists_used_identifier) :- |
| 1116 | | inner_predicate_level_optimizations(P,NP), |
| 1117 | | add_used_identifier_info(Ids,NP,IOld,INew), |
| 1118 | | %print('* POST => '),translate:print_bexpr(b(exists(Ids,NP),pred,INew)),nl, |
| 1119 | | %print(' INFO=> '),print(INew),nl, |
| 1120 | | % TO DO: also compute which identifiers are worth waiting for; do not wait for res in #x.(x:E & ... & res=min(f(x))) |
| 1121 | | add_removed_typing_info(INew,ResInfo). |
| 1122 | | cleanup_post_essential(Construct,Type,I,NewConstruct,Type,I,single/detect_partitions) :- |
| 1123 | | contains_predicate(Construct,Type,Pred,NewConstruct,NewPred),!, % something like a select or other substitution |
| 1124 | | predicate_level_optimizations(Pred,NewPred). |
| 1125 | | cleanup_post_essential(Construct,Type,I,NewConstruct,Type,I,single/detect_partitions2) :- |
| 1126 | | contains_predicates(Construct,Type,Preds,NewConstruct,NewPreds),!, |
| 1127 | | maplist(predicate_level_optimizations,Preds,NewPreds) % TO DO: do CSE together (in some cases) ! |
| 1128 | | . %, (Preds=NewPreds -> true ; print('Found partitions: '), translate:print_subst(b(NewConstruct,Type,I)),nl). |
| 1129 | | |
| 1130 | | % use when in cleanup_post you construct a forall which will not be at the top-level |
| 1131 | | % (meaning that the above essential rules will not run) |
| 1132 | | construct_inner_forall(Ids,LHS,RHS,OldInfo, b(Res,pred,NewInfo)) :- |
| 1133 | | inner_predicate_level_optimizations(LHS,NLhs), |
| 1134 | | inner_predicate_level_optimizations(RHS,NRhs), |
| 1135 | | construct_forall_opt(Ids,NLhs,NRhs,OldInfo, Res,NewInfo). |
| 1136 | | |
| 1137 | | construct_forall_opt(IDs,NLhs,NRhs,Info, Res,NewInfo) :- |
| 1138 | | (is_truth(NRhs) ; is_falsity(NLhs)),!, |
| 1139 | | debug_println(19,removing_useless_forall(IDs)), |
| 1140 | | Res= truth, NewInfo = [was(forall(IDs,NLhs,NRhs))|Info]. |
| 1141 | | % TO DO: is the following rule useful ?: will require adapting test 510 output file |
| 1142 | | % triggers e.g. for test 1447 |
| 1143 | | %construct_forall_opt([TID],LHS,RHS,Info, Res,NewInfo) :- % !x. (x:SetA => x:SetB) ---> SetA <: SetB |
| 1144 | | % is_valid_id_member_check(LHS,TID,SetA), is_valid_id_member_check(RHS,TID,SetB), |
| 1145 | | % !, |
| 1146 | | % (debug_mode(off) -> true |
| 1147 | | % ; format('Replacing forall ~w by subset: ',[TID]), translate:print_bexpr(b(subset(SetA,SetB),pred,Info)),nl |
| 1148 | | % ), |
| 1149 | | % Res = subset(SetA,SetB), NewInfo = [was(forall)|Info]. |
| 1150 | | construct_forall_opt(Ids,NLhs,NRhs,OldInfo, forall(Ids,NLhs,NRhs),ResInfo) :- |
| 1151 | | conjunct_predicates([NLhs,NRhs],P), |
| 1152 | | add_used_identifier_info(Ids,P,OldInfo,Info), |
| 1153 | | add_removed_typing_info(Info,ResInfo). |
| 1154 | | |
| 1155 | | add_removed_typing_info(Info,ResInfo) :- |
| 1156 | | (memberchk(removed_typing,Info) -> ResInfo = Info ; ResInfo = [removed_typing|Info]). |
| 1157 | | |
| 1158 | | disjoint_ids(Ids1,Ids2) :- |
| 1159 | | get_texpr_ids(Ids1,I1), sort(I1,SI1), |
| 1160 | | get_texpr_ids(Ids2,I2), sort(I2,SI2), |
| 1161 | | ord_disjoint(SI1,SI2). |
| 1162 | | % --------------------- |
| 1163 | | |
| 1164 | | % non-essential post cleanup rules; only applied when optimize_ast is TRUE |
| 1165 | | |
| 1166 | | % WITH PATH: |
| 1167 | | |
| 1168 | | cleanup_post_ne_with_path(member(E,b(image(Rel,SONE),TypeImg,InfoImg)),pred,I,member(Couple,Rel),pred,I,multi/replace_image_by_member,Path) :- |
| 1169 | | % x : Rel[{One}] => One|->x : Rel |
| 1170 | | Path \= [arg(forall/3,1)|_], % not LHS of a foral |
| 1171 | | %% do not do this if it is the LHS of a forall: !(aus2).( aus2 : helper[{mm}] => RHS) (as we no longer can apply the optimized set treatment for forall |
| 1172 | | singleton_set_extension(SONE,One), |
| 1173 | | %% Rel \= b(inverse(_),_,_), %% TO DO: maybe exclude this; here user maybe wants to explicitly compute image ? |
| 1174 | | !, |
| 1175 | | create_couple(One,E,Couple), |
| 1176 | | (debug_mode(off) -> true |
| 1177 | | ; print('Member of Image: '),translate:print_bexpr(b(member(E,b(image(Rel,SONE),TypeImg,InfoImg)),pred,I)),nl, |
| 1178 | | print(' replaced by: '),translate:print_bexpr(b(member(Couple,Rel),pred,I)),nl |
| 1179 | | ). |
| 1180 | | |
| 1181 | | |
| 1182 | | % WITHOUT PATH: |
| 1183 | | |
| 1184 | | cleanup_post(conjunct(b(truth,pred,I1),b(B,pred,I2)),pred,I0,B,pred,NewI,multi/remove_truth_conj1) :- !, |
| 1185 | | include_important_info_from_removed_pred(I1,I2,I3), % ensure was,... information propagated |
| 1186 | | add_important_info_from_super_expression(I0,I3,NewI). |
| 1187 | | cleanup_post(conjunct(b(A,pred,I2),b(truth,pred,I1)),pred,I0,A,pred,NewI,multi/remove_truth_conj2) :- !, |
| 1188 | | include_important_info_from_removed_pred(I1,I2,I3), |
| 1189 | | add_important_info_from_super_expression(I0,I3,NewI). |
| 1190 | | cleanup_post(conjunct(b(falsity,pred,I1),b(_,_,I2)),pred,I0,falsity,pred,NewI,multi/simplify_falsity_conj1) :- !, |
| 1191 | | include_important_info_from_removed_pred(I2,I1,I3), |
| 1192 | | add_important_info_from_super_expression(I0,I3,NewI). |
| 1193 | | cleanup_post(conjunct(LHS,b(falsity,pred,I2)),pred,I0,falsity,pred,NewI,multi/simplify_falsity_conj2) :- |
| 1194 | | always_well_defined_or_disprover_mode(LHS), !, % do we need to check WD Implications ; ProB would treat falsity first? |
| 1195 | | get_texpr_info(LHS,I1), |
| 1196 | | include_important_info_from_removed_pred(I1,I2,I3), |
| 1197 | | add_important_info_from_super_expression(I0,I3,NewI). |
| 1198 | | % we use FInfo: in case it has a was(.) field, e.g., for pretty printing and unsat core generation and unsatCore.groovy test |
| 1199 | | cleanup_post(conjunct(AA,BB),pred,I,Res,pred,I,multi/modus_ponens) :- |
| 1200 | | Impl = b(implication(A,B),pred,_), |
| 1201 | ? | ((AA,BB) = (Impl,A2) ; (BB,AA) = (Impl,A2)), |
| 1202 | | same_texpr(A,A2), |
| 1203 | | % arises e.g., for predicates such as IF x:0..3 THEN y=2 ELSE 1=0 END ; works with simplify_falsity_impl3 rule |
| 1204 | | % rewrite (A=>B) & A into (A&B) |
| 1205 | | !, |
| 1206 | | (debug_mode(off) -> true ; print('Modus Ponens: '),translate:print_bexpr(A), print(' => '), translate:print_bexpr(B),nl), |
| 1207 | | Res = conjunct(A,B). |
| 1208 | | %cleanup_post(conjunct(TLHS,P1),pred,_,LHS,pred,Info,multi/duplicate_pred) :- |
| 1209 | | % % TO DO: implement an efficient version of this; currently very slow e.g. for test 293 |
| 1210 | | % b_interpreter:member_conjunct(P2,TLHS,_), |
| 1211 | | % same_texpr(P1,P2), |
| 1212 | | % TLHS = b(LHS,pred,Info), |
| 1213 | | % print('remove_duplicate: '), translate:print_bexpr(P1),nl. |
| 1214 | | cleanup_post(conjunct(LHS,b(Comparison1,pred,_)),pred,I0,Result,pred,RInfo,multi/detect_interval1) :- |
| 1215 | | % X <= UpBound & X >= LowBound <=> X : UpBound .. LowBound (particularly useful when CLPFD FALSE, causes problem with test 1771) |
| 1216 | | % Note: x>18 & y<1024 & x<20 & y>1020 now works, it is bracketed ((()) & y>1020) |
| 1217 | | get_preference(use_clpfd_solver,false), |
| 1218 | | \+ data_validation_mode, % this rule may lead to additional enumerations |
| 1219 | | get_leq_comparison(Comparison1,X,UpBound), %print(leq(X,UpBound)),nl, |
| 1220 | ? | select_conjunct(b(Comparison2,_,_),LHS,Prefix,Suffix), |
| 1221 | | get_geq_comparison(Comparison2,X2,LowBound), %print(x2(X2,LowBound)),nl, |
| 1222 | | same_texpr(X,X2), |
| 1223 | | (always_well_defined_or_disprover_mode(UpBound) |
| 1224 | | -> true |
| 1225 | | ; % as we may move valuation earlier, we have to be careful |
| 1226 | | % we check if Comparison2 is last conjunct; x=7 & x:8..(1/0) raises no WD error in ProB |
| 1227 | | Suffix=[] |
| 1228 | | ), |
| 1229 | | !, |
| 1230 | | create_interval_member(X,LowBound,UpBound,Member), |
| 1231 | | append(Prefix,[Member|Suffix],ResultList), |
| 1232 | | conjunct_predicates(ResultList,TResult), |
| 1233 | | (debug_mode(off) -> true ; print(' Detected interval membership (1): '),translate:print_bexpr(TResult),nl), |
| 1234 | | TResult = b(Result,pred,I1), |
| 1235 | | add_important_info_from_super_expression(I0,I1,RInfo). |
| 1236 | | cleanup_post(conjunct(LHS,b(Comparison1,pred,_)),pred,I0,Result,pred,RInfo,multi/detect_interval2) :- |
| 1237 | | % X >= LowBound & X <= UpBound <=> X : UpBound .. LowBound |
| 1238 | | get_preference(use_clpfd_solver,false), |
| 1239 | | \+ data_validation_mode, % this rule may lead to additional enumerations |
| 1240 | | get_geq_comparison(Comparison1,X,LowBound), |
| 1241 | ? | select_conjunct(b(Comparison2,_,_),LHS,Prefix,Suffix), |
| 1242 | | get_leq_comparison(Comparison2,X2,UpBound), |
| 1243 | | same_texpr(X,X2), |
| 1244 | | (always_well_defined_or_disprover_mode(LowBound) |
| 1245 | | -> true |
| 1246 | | ; % as we may move valuation earlier, we have to be careful |
| 1247 | | % we check if Comparison2 is last conjunct; x=7 & x:8..(1/0) raises no WD error in ProB |
| 1248 | | Suffix=[] |
| 1249 | | ), |
| 1250 | | !, |
| 1251 | | create_interval_member(X,LowBound,UpBound,Member), |
| 1252 | | append(Prefix,[Member|Suffix],ResultList), |
| 1253 | | conjunct_predicates(ResultList,TResult), |
| 1254 | | (debug_mode(off) -> true ; print(' Detected interval membership (2): '),translate:print_bexpr(TResult),nl), |
| 1255 | | TResult = b(Result,pred,I1), |
| 1256 | | add_important_info_from_super_expression(I0,I1,RInfo). |
| 1257 | | |
| 1258 | | cleanup_post(disjunct(b(truth,pred,I1),_),pred,I0,truth,pred,I,multi/simplify_truth_disj1) :- !, |
| 1259 | | add_important_info_from_super_expression(I0,I1,I). |
| 1260 | | %cleanup_post(disjunct(_,b(truth,pred,_)),pred,_,truth,pred,I,multi/simplify_truth_disj2) :- !. % WD Implications ??? |
| 1261 | | cleanup_post(disjunct(b(A,pred,I1),b(falsity,pred,_)),pred,I0,A,pred,I,multi/remove_falsity_disj1) :- !, |
| 1262 | | add_important_info_from_super_expression(I0,I1,I). |
| 1263 | | cleanup_post(disjunct(b(falsity,pred,_),b(B,pred,I1)),pred,I0,B,pred,I,multi/remove_falsity_disj2) :- !, |
| 1264 | | add_important_info_from_super_expression(I0,I1,I). |
| 1265 | | cleanup_post(disjunct(Equality1,Equality2),pred,I,New,pred,I,multi/rewrite_disjunct_to_member) :- |
| 1266 | | identifier_equality(Equality2,ID,_,Expr2), |
| 1267 | | always_well_defined_or_disprover_mode(Expr2), |
| 1268 | | identifier_equality(Equality1,ID,TID,Expr1), |
| 1269 | | % Rewrite (ID = Expr1 or ID = Expr2) into ID: {Expr1,Expr2} ; good if FD information can be extracted for ID |
| 1270 | | % But: can be bad for reification, in particular when set extension cannot be computed fully |
| 1271 | | % TO DO: also deal with ID : {Values} and more general extraction of more complicated disjuncts |
| 1272 | | % TO DO: also apply for implication (e.g., ID /= E1 => ID=E2) |
| 1273 | | !, |
| 1274 | | construct_set_extension(Expr1,Expr2,SetX), |
| 1275 | | New=member(TID,SetX), |
| 1276 | | (debug_mode(off) -> true |
| 1277 | | ; format('Rewrite disjunct ~w: ',[ID]),translate:print_bexpr(SetX),nl). |
| 1278 | | cleanup_post(disjunct(CEquality1,CEquality2),pred,IOld,New,pred,INew,multi/factor_common_pred_in_disjunction) :- |
| 1279 | | % (x=2 & y=3) or (x=2 & y=4) -> x=2 & (y=3 or y=4) to improve constraint propagation |
| 1280 | | factor_disjunct(CEquality1,CEquality2,IOld,New,INew), |
| 1281 | | (debug_mode(off) -> true |
| 1282 | | ; format('Factor disjunct: ',[]),translate:print_bexpr(b(New,pred,INew)),nl). |
| 1283 | | cleanup_post(implication(b(truth,pred,_),b(B,pred,I1)),pred,I0,B,pred,I,multi/remove_truth_impl1) :- !, |
| 1284 | | add_important_info_from_super_expression(I0,I1,I). |
| 1285 | | cleanup_post(implication(b(falsity,pred,I1),_),pred,I0,truth,pred,I,multi/simplify_falsity_impl1) :- !, |
| 1286 | | add_important_info_from_super_expression(I0,I1,I). |
| 1287 | | cleanup_post(implication(_,b(truth,pred,I1)),pred,I0,truth,pred,I,multi/simplify_truth_impl2) :- !, |
| 1288 | | add_important_info_from_super_expression(I0,I1,I). |
| 1289 | | cleanup_post(implication(P,b(falsity,pred,_)),pred,I,NotP,pred,[was(implication)|I],multi/simplify_falsity_impl3) :- !, |
| 1290 | | create_negation(P,TNotP), |
| 1291 | | (debug_mode(off) -> true ; translate:print_bexpr(P), print(' => FALSE simplified'),nl), |
| 1292 | | get_texpr_expr(TNotP,NotP). |
| 1293 | | % TO DO: is the following rule useful ?: |
| 1294 | | %cleanup_post(implication(A,b(implication(B,C),pred,_)),pred,IOld, |
| 1295 | | % implication(AB,C),pred,IOld,single/replace_implication_by_and) :- |
| 1296 | | % % (A => B => C <==> (A & B) => C |
| 1297 | | % conjunct_predicates([A,B],AB), |
| 1298 | | % (debug_mode(off) -> true ; print('Simplifying double implication: '), translate:print_bexpr(b(implication(AB,C),pred,IOld)),nl). |
| 1299 | | cleanup_post(equivalence(b(truth,pred,_),b(B,pred,I1)),pred,I0,B,pred,I,multi/remove_truth_equiv1) :- !, |
| 1300 | | add_important_info_from_super_expression(I0,I1,I). |
| 1301 | | cleanup_post(equivalence(b(A,pred,I),b(truth,pred,I1)),pred,I0,A,pred,I,multi/remove_truth_equiv2) :- !, |
| 1302 | | add_important_info_from_super_expression(I0,I1,I). |
| 1303 | | % TO DO: more rules for implication/equivalence to introduce negations (A <=> FALSITY ---> not(A)) ? |
| 1304 | | % detect certain tautologies/inconsistencies |
| 1305 | | cleanup_post(member(X,B),pred,I,truth,pred,[was(member(X,B))|I],multi/remove_type_member) :- |
| 1306 | | is_just_type(B), |
| 1307 | | nonmember(label(_),I), % the user has explicitly labeled this conjunct |
| 1308 | | !. % print('REMOVE: '),translate:print_bexpr(b(member(X,B),pred,[])),nl, print(I),nl. |
| 1309 | | cleanup_post(not_member(X,B),pred,I,falsity,pred,[was(not_member(X,B))|I],multi/remove_type_not_member) :- |
| 1310 | | is_just_type(B), |
| 1311 | | nonmember(label(_),I), % the user has explicitly labeled this conjunct |
| 1312 | | !. |
| 1313 | | cleanup_post(member(X,TSet),pred,I,equal(X,One),pred,I,multi/remove_member_one_element_set) :- |
| 1314 | | singleton_set_extension(TSet,One), |
| 1315 | | !, |
| 1316 | | % X:{One} <=> X=One |
| 1317 | | true. %,print('Introducing equality: '),translate:print_bexpr(X), print(' = '), translate:print_bexpr(One),nl. |
| 1318 | | cleanup_post(member(X,b(Set,_,_)),pred,I,not_equal(X,One),pred,I,multi/remove_member_setdiff) :- |
| 1319 | | Set = set_subtraction(MaximalSet,SONE), |
| 1320 | | singleton_set_extension(SONE,One), |
| 1321 | | definitely_maximal_set(MaximalSet), |
| 1322 | | !, % x : INTEGER-{One} <=> x/=One |
| 1323 | | (debug_mode(off) -> true |
| 1324 | | ; print('Replacing member of set_subtraction: '), translate:print_bexpr(MaximalSet), print(' - '), translate:print_bexpr(SONE),nl). |
| 1325 | | cleanup_post(not_member(X,TSet),pred,I,not_equal(X,One),pred,I,multi/remove_member_one_element_set) :- |
| 1326 | | singleton_set_extension(TSet,One), |
| 1327 | | !, |
| 1328 | | % X/:{One} <=> X/=One |
| 1329 | | true. %print('Introducing disequality: '),translate:print_bexpr(X), print(' /= '), translate:print_bexpr(One),nl. |
| 1330 | | cleanup_post(member(E,b(fin_subset(E2),_,_)),pred,I,finite(E),pred,I,multi/introduce_finite) :- |
| 1331 | | (same_texpr(E,E2); is_just_type(E2)),!. % print(introduce(finite(E))),nl. |
| 1332 | | /* do we want need this rule ?: |
| 1333 | | clenaup_post(member(b(couple(A,B),couple(TA,TB),IC),ID),pred,I,equal(A,B),pred,I,multi/replace_member_id) :- |
| 1334 | | is_is_event_b_identity(ID), |
| 1335 | | !, |
| 1336 | | print('Replace member of id by equality: '), |
| 1337 | | tranlsate:print_bexpr(b(member(b(couple(A,B),couple(TA,TB),IC),ID),pred,I)),nl. |
| 1338 | | */ |
| 1339 | | cleanup_post(member(b(couple(A,B),couple(TA,TB),IC),b(reverse(Rel),_,_)),pred,I,member(ICouple,Rel),pred,I,multi/remove_reverse) :- !, |
| 1340 | | (debug_mode(off) -> true ; print('Removed inverse (~): '),translate:print_bexpr(Rel),nl), |
| 1341 | | ICouple = b(couple(B,A),couple(TB,TA),IC). |
| 1342 | | cleanup_post(member(LHS,Comprehension),pred,I,Result,pred,I,multi/remove_member_comprehension) :- |
| 1343 | | Comprehension = b(comprehension_set([TID],Body),_,_), |
| 1344 | | % rewrite could duplicate LHS: not an issue in CSE mode; optimization relevant in normalize_ast mode |
| 1345 | ? | (get_preference(normalize_ast,true) |
| 1346 | ? | ; get_preference(use_common_subexpression_elimination,true) ; is_simple_expression(LHS)), |
| 1347 | | get_texpr_id(TID,ID), |
| 1348 | | !, |
| 1349 | | % LHS:{x|P(x)} ==> P(LHS) |
| 1350 | | replace_id_by_expr(Body,ID,LHS,TResult), |
| 1351 | | get_texpr_expr(TResult,Result), |
| 1352 | | (debug_mode(off) -> true ; print('Remove element of comprehension_set: '),translate:print_bexpr(Comprehension),nl, |
| 1353 | | print(' into: '),translate:print_bexpr(TResult),nl). |
| 1354 | | cleanup_post(not_member(LHS,Comprehension),pred,I,Result,pred,I,multi/remove_not_member_comprehension) :- |
| 1355 | | Comprehension = b(comprehension_set([TID],Body),_,_), |
| 1356 | | % rewrite could duplicate LHS: not an issue in CSE mode; optimization relevant in normalize_ast mode |
| 1357 | | (get_preference(normalize_ast,true) |
| 1358 | | ; get_preference(use_common_subexpression_elimination,true) ; is_simple_expression(LHS)), |
| 1359 | | get_texpr_id(TID,ID), |
| 1360 | | !, |
| 1361 | | % LHS/:{x|P(x)} ==> not(P(LHS)) |
| 1362 | | replace_id_by_expr(Body,ID,LHS,TResult), |
| 1363 | | Result = negation(TResult), |
| 1364 | | (debug_mode(off) -> true ; print('Remove not element of comprehension_set: '),translate:print_bexpr(Comprehension),nl, |
| 1365 | | print(' into: not('),translate:print_bexpr(TResult),print(')'),nl). |
| 1366 | | cleanup_post(subset(A,B),pred,I,truth,pred,[was(subset(A,B))|I],multi/remove_type_subset) :- |
| 1367 | | is_just_type(B), |
| 1368 | | nonmember(label(_),I), % the user has explicitly labeled this conjunct |
| 1369 | | !. |
| 1370 | | cleanup_post(not_subset(A,B),pred,I,falsity,pred,[was(subset(A,B))|I],multi/remove_type_not_subset) :- |
| 1371 | | is_just_type(B), |
| 1372 | | nonmember(label(_),I), % the user has explicitly labeled this conjunct |
| 1373 | | !. |
| 1374 | | cleanup_post(SUB,pred,I,NewPred,pred,[generated_conjunct|I],multi/replace_subset_by_element) :- |
| 1375 | | is_subset(SUB,A,B), |
| 1376 | | is_set_extension(A,List), |
| 1377 | | !, % for sequence extension we don't need this as the interpreter knows exactly the cardinality of a sequence_extension ? |
| 1378 | | % applying rule {x1,x2,...} <: B <=> x1:B & x2:B & ... |
| 1379 | | maplist(gen_member_predicates(B),List,Conjuncts), |
| 1380 | | conjunct_predicates(Conjuncts,TNewPred), |
| 1381 | | % print('detected subset-member rule: '),translate:print_bexpr(TNewPred),nl, |
| 1382 | | get_texpr_expr(TNewPred,NewPred). |
| 1383 | | cleanup_post(SUB,pred,I,NewPred,pred,[generated_conjunct|I],multi/replace_union_subset) :- |
| 1384 | | is_subset(SUB,A,B), |
| 1385 | | % mark conjunct as generated: used e.g. by flatten_conjunct in predicate_evaluator |
| 1386 | | get_texpr_expr(A,union(_,_)),!, |
| 1387 | | % applying rule A1 \/ A2 <: B <=> A1 <: B & A2 <: B |
| 1388 | | % could be detrimental if checking that something is an element of B is expensive |
| 1389 | | extract_unions(A,As), |
| 1390 | | findall(Subi,(member(Ai,As),safe_create_texpr(subset(Ai,B),pred,I,Subi)),Conj), % we could try and re-run clean-up ? safe_create_texpr will ensure WD info set |
| 1391 | | conjunct_predicates(Conj,TNewPred), |
| 1392 | | %translate:print_bexpr(TNewPred),nl, |
| 1393 | | get_texpr_expr(TNewPred,NewPred). |
| 1394 | | cleanup_post(Comp,pred,I,SComp,pred,I,multi/simplify_cse_comparison) :- |
| 1395 | | % simplify comparison operations; can result in improved constraint propagation |
| 1396 | | % e.g., ia + CSE1 * 2 > ia + fa <=> CSE1 * 2 > fa for Setlog/prob-ttf/qsee-TransmitMemoryDumpOk21_SP_3.prob |
| 1397 | | comparison(Comp,A,B,SComp,SA,SB), |
| 1398 | | %print(try_simplify(A,B)),nl, |
| 1399 | | simplify_comparison_terms(A,B,SA,SB),!, |
| 1400 | | (debug_mode(off) -> true |
| 1401 | | ; print('Simplified: '),translate:print_bexpr(b(Comp,pred,I)), |
| 1402 | | print(' <=> '),translate:print_bexpr(b(SComp,pred,I)),nl). |
| 1403 | | cleanup_post(equal(A,B),pred,I,truth,pred,[was(equal(A,B))|I],multi/remove_equality) :- |
| 1404 | | same_texpr(A,B),always_well_defined_or_disprover_mode(A),!. % ,print(removed_equal(A,B)),nl. |
| 1405 | | cleanup_post(equal(A,B),pred,I,equal(A2,B2),pred,I,multi/simplify_equality) :- |
| 1406 | | simplify_equality(A,B,A2,B2). |
| 1407 | | cleanup_post(not_equal(A,B),pred,I,not_equal(A2,B2),pred,I,multi/simplify_inequality) :- |
| 1408 | | simplify_equality(A,B,A2,B2). |
| 1409 | | cleanup_post(equal(A,B),pred,I,falsity,pred,[was(equal(A,B))|I],multi/remove_equality_false) :- |
| 1410 | | different_texpr_values(A,B),!. %,print(removed_equal_false(A,B)),nl. |
| 1411 | | cleanup_post(equal(A,B),pred,I,greater(Low,Up),pred,I,multi/remove_equality) :- |
| 1412 | | % Low..Up = {} <=> Low>Up % is also handled by constraint solver; but other simplifications can apply here |
| 1413 | | (is_empty_set(B), is_interval(A,Low,Up) ; |
| 1414 | | is_empty_set(A), is_interval(B,Low,Up)),!, |
| 1415 | | (debug_mode(off) -> true |
| 1416 | | ; print('Simplified: '), translate:print_bexpr(b(equal(A,B),pred,I)), print(' <=> '), |
| 1417 | | translate:print_bexpr(b(greater(Low,Up),pred,I)),nl). |
| 1418 | | % TO DO: card(P) = 0 -> P={} if wd guaranteed |
| 1419 | | cleanup_post(CardGt0Expr,pred,I,not_equal(X,EmptySet),pred,I,multi/remove_cardgt0) :- |
| 1420 | | get_geq_comparison(CardGt0Expr,Card,One), |
| 1421 | | % card(P) > 0 -> P\={} if wd guaranteed ; TODO: card(P) : NATURAL1 |
| 1422 | | Card = b(card(X),integer,_), get_integer(One,1), |
| 1423 | | always_well_defined_or_disprover_mode(Card), |
| 1424 | | get_texpr_type(X,TX), get_texpr_info(One,I0), |
| 1425 | | EmptySet = b(empty_set,TX,I0),!, |
| 1426 | | (debug_mode(off) -> true ; print('Removed card(.) > 0 for set: '), translate:print_bexpr(X), nl). |
| 1427 | | cleanup_post(member(Card,Natural),pred,I,truth,pred,I,multi/remove_card_natural) :- |
| 1428 | | % card(P) : NATURAL -> truth if wd guaranteed |
| 1429 | | Card = b(card(X),integer,_), |
| 1430 | | is_integer_set(Natural,'NATURAL'), |
| 1431 | | always_well_defined_or_disprover_mode(Card), |
| 1432 | | !, |
| 1433 | | (debug_mode(off) -> true ; print('Removed card(.):NATURAL for set: '), translate:print_bexpr(X), nl). |
| 1434 | | cleanup_post(not_equal(A,B),pred,I,less_equal(Low,Up),pred,I,multi/remove_equality) :- |
| 1435 | | % Low..Up \= {} <=> Low<=Up % is also handled by constraint solver; but other simplifications can apply here |
| 1436 | | (is_empty_set(B), is_interval(A,Low,Up) ; |
| 1437 | | is_empty_set(A), is_interval(B,Low,Up)),!, |
| 1438 | | (debug_mode(off) -> true |
| 1439 | | ; print('Simplified: '), translate:print_bexpr(b(equal(A,B),pred,I)), print(' <=> '), |
| 1440 | | translate:print_bexpr(b(less_equal(Low,Up),pred,I)),nl). |
| 1441 | | cleanup_post(equal(A,B),pred,I,equal(A,RLet),pred,I,single/detect_recursion) :- |
| 1442 | | % "A" should be an identifier |
| 1443 | | get_texpr_id(A,ID), |
| 1444 | | % check if some side conditions are fulfilled where the recursion detection can be enabled |
| 1445 | ? | recursion_detection_enabled(A,B,I), |
| 1446 | | % A must be recursively used in B: |
| 1447 | ? | find_recursive_usage(B,ID), |
| 1448 | | % TO DO: also find mutual recursion ! |
| 1449 | | debug_println(9,recursion_detected(ID)), |
| 1450 | | !, % create an recursive_let where the body is annotated to be symbolic |
| 1451 | | get_texpr_type(B,Type), add_texpr_infos(B,[prob_annotation('SYMBOLIC')],B2), |
| 1452 | | mark_recursion(B2,ID,B3), |
| 1453 | | %print(marked_recursion(ID)),nl, |
| 1454 | | safe_create_texpr(recursive_let(A,B3),Type,RLet). |
| 1455 | | cleanup_post(equal(A,B),pred,Info1,ResultExpr,pred,Info3,multi/simplify_bool_true_false) :- |
| 1456 | | % simplify bool(X)=TRUE -> X and bool(X)=FALSE -> not(X) |
| 1457 | ? | ( get_texpr_expr(A,convert_bool(X)), get_texpr_boolean(B,BOOLVAL) |
| 1458 | | ; |
| 1459 | | get_texpr_boolean(A,BOOLVAL),get_texpr_expr(B,convert_bool(X)) |
| 1460 | | ), |
| 1461 | | !, debug_println(9,simplify_bool_equal_TRUE(X)), |
| 1462 | | get_texpr_info(X,Info2), |
| 1463 | | add_important_info_from_super_expression(Info1,Info2,Info3), |
| 1464 | | (BOOLVAL = boolean_true -> get_texpr_expr(X,ResultExpr) ; ResultExpr = negation(X)). |
| 1465 | | %cleanup_post(equal(A,B),pred,Info1,equal(REL,CartProd),pred,Info1,multi/simplify_image) :- |
| 1466 | | % cannot be applied yet; SETS not precompiled yet ! |
| 1467 | | % A = b(image(REL,SetExt),_,_), |
| 1468 | | % % REL[{OneEl}] = B ----> REL = {OneEl}*B if OneEl is the only possible value |
| 1469 | | % % such signature appear in Alloy generated code |
| 1470 | | % SetExt = b(set_extension([_]),set(global(GlobalSetName)),_), |
| 1471 | | % %bmachine:b_get_named_machine_set_calc(GlobalSetName,_,[_]), |
| 1472 | | % b_global_set_cardinality(Type,1), % cannot be called yet; global sets not precompiled |
| 1473 | | % !, |
| 1474 | | % get_texpr_type(REL,RelType), |
| 1475 | | % safe_create_texpr(cartesian_product(SetExt,B),RelType,CartProd), |
| 1476 | | % format('Translating image for singleton set'), translate:print_bexpr(b(equal(REL,CartProd),pred,[])),nl. |
| 1477 | | cleanup_post(not_equal(A,B),pred,I,falsity,pred,[was(not_equal(A,B))|I],multi/remove_disequality) :- |
| 1478 | | same_texpr(A,B),always_well_defined_or_disprover_mode(A),!. % ,print(removed_not_equal(A,B)),nl. |
| 1479 | | % sometimes one uses & TRUE=TRUE to finish off guards, invariants, ... |
| 1480 | | % exchange lambda expressions by a comprehension set |
| 1481 | | % TO DO: also add rule for bool(X)=FALSE -> not(X) |
| 1482 | | cleanup_post(not_equal(A,B),pred,I,truth,pred,[was(not_equal(A,B))|I],multi/remove_disequality_false) :- |
| 1483 | | different_texpr_values(A,B),!. % ,print(removed_not_equal_false(A,B)),nl. |
| 1484 | | cleanup_post(not_equal(A,B),pred,I,NewP,pred,[was(not_equal(A,B))|I],multi/not_disjoint_disequality) :- |
| 1485 | | /* Set1 /\ Set2 /= {} <===> #(zz).(zz:Set1 & zz:Set2) */ |
| 1486 | | preferences:preference(use_smt_mode,true), /* currently this rewriting makes test 1112 fail; TO DO: investigate */ |
| 1487 | | is_empty_set(B), |
| 1488 | | get_texpr_expr(A,intersection(Set1,Set2)),!, |
| 1489 | | get_texpr_type(Set1,Set1Type), unify_types_strict(Set1Type,set(T)), |
| 1490 | | ID = b(identifier('_zzzz_unary'),T,[generated]), |
| 1491 | | ESet1 = b(member(ID,Set1),pred,[]), |
| 1492 | | ESet2 = b(member(ID,Set2),pred,[]), |
| 1493 | | create_exists_opt([ID],[ESet1,ESet2],NewPredicate), |
| 1494 | | (debug_mode(off) -> true |
| 1495 | | ; print('Transformed not disjoint disequality: '),translate:print_bexpr(NewPredicate),nl), |
| 1496 | | get_texpr_expr(NewPredicate,NewP). |
| 1497 | | cleanup_post(equal(b(intersection(A,B),_,_),Empty),pred,I,not_equal(El1,El2),pred,[was(intersection)|I],multi/detect_not_equal) :- |
| 1498 | | % {El1} /\ {El2} = {} --> El1 \= El2 |
| 1499 | | singleton_set_extension(A,El1), |
| 1500 | | singleton_set_extension(B,El2), |
| 1501 | | is_empty_set(Empty). |
| 1502 | | cleanup_post(greater(A,B),pred,I,Res,pred,[was(greater(A,B))|I],multi/eval_greater) :- |
| 1503 | | get_integer(A,IA), get_integer(B,IB), |
| 1504 | | (IA>IB -> Res = truth ; Res=falsity). |
| 1505 | | cleanup_post(less(A,B),pred,I,Res,pred,[was(greater(A,B))|I],multi/eval_less) :- |
| 1506 | | get_integer(A,IA), get_integer(B,IB), |
| 1507 | | (IA<IB -> Res = truth ; Res=falsity). |
| 1508 | | cleanup_post(greater_equal(A,B),pred,I,Res,pred,[was(greater(A,B))|I],multi/eval_greater_equal) :- |
| 1509 | | get_integer(A,IA), get_integer(B,IB), |
| 1510 | | (IA >= IB -> Res = truth ; Res=falsity). |
| 1511 | | cleanup_post(less_equal(A,B),pred,I,Res,pred,[was(greater(A,B))|I],multi/eval_less_equal) :- |
| 1512 | | get_integer(A,IA), get_integer(B,IB), |
| 1513 | | (IA =< IB -> Res = truth ; Res=falsity). |
| 1514 | | cleanup_post(negation(A),pred,I,falsity,pred,[was(negation(A))|I],multi/remove_negation_truth) :- |
| 1515 | | is_truth(A),!. % ,print(negation(A)),nl. |
| 1516 | | cleanup_post(negation(A),pred,I,truth,pred,[was(negation(A))|I],multi/remove_negation_falsity) :- |
| 1517 | | is_falsity(A),!. % ,print(negation(A)),nl. |
| 1518 | | cleanup_post(convert_bool(A),boolean,I,boolean_true,boolean,I,multi/remove_convert_bool) :- |
| 1519 | | is_truth(A),!. % ,print(convert_bool(A)),nl. |
| 1520 | | cleanup_post(convert_bool(A),boolean,I,boolean_false,boolean,I,multi/remove_convert_bool_false) :- |
| 1521 | | is_falsity(A),!. % ,print(convert_bool_false(A)),nl. |
| 1522 | | cleanup_post(assertion_expression(Cond,_ErrMsg,Expr),_T,I0,BE,TE,IE,multi/remove_assertion_expression) :- |
| 1523 | | is_truth(Cond),!, %print(remove_assertion_expression(Cond)),nl, |
| 1524 | | Expr = b(BE,TE,I1), |
| 1525 | | add_important_info_from_super_expression(I0,I1,IE). |
| 1526 | | cleanup_post(cartesian_product(A,B),T,I,Res,T,I,single/cartesian_product_to_pair) :- |
| 1527 | | singleton_set_extension(A,El1), |
| 1528 | | singleton_set_extension(B,El2), % {A}*{B} -> {A|->B} ; happens in Alloy translations a lot |
| 1529 | | !, |
| 1530 | | get_texpr_type(El1,T1), get_texpr_type(El2,T2), |
| 1531 | | safe_create_texpr(couple(El1,El2),couple(T1,T2),Pair), %translate:print_bexpr(Pair),nl, |
| 1532 | | Res = set_extension([Pair]). |
| 1533 | | cleanup_post(union(A,B),T,I,Res,T,[add_element_to_set|I],multi/add_element_to_set) :- % multi: cycle check done in info field |
| 1534 | ? | \+ member(add_element_to_set,I), |
| 1535 | | ( singleton_set_extension(B,_El) -> Res = union(A,B) |
| 1536 | | ; singleton_set_extension(A,_El) -> Res = union(B,A)), |
| 1537 | | !. %,print(detected_add_singleton_element(_El)),nl. |
| 1538 | | cleanup_post(general_union(SetExt),Type,I0,Res,Type,Info,multi/general_union_set_extension) :- % union_generalized |
| 1539 | | SetExt = b(set_extension(LIST),_,I1), |
| 1540 | | add_important_info_from_super_expression(I0,I1,Info), |
| 1541 | | % no need to apply rule if already transformed into avl in cleanup_pre, hence we do not call is_set_extension |
| 1542 | | construct_union_from_list(LIST,Type,Info,TRes), |
| 1543 | | !, |
| 1544 | | (debug_mode(on) -> print('translated_general_union: '), translate:print_bexpr(TRes),nl ; true), |
| 1545 | | get_texpr_expr(TRes,Res). |
| 1546 | | cleanup_post(general_intersection(SetExt),Type,I0,Res,Type,Info,multi/general_inter_set_extension) :- % union_generalized |
| 1547 | | SetExt = b(set_extension(LIST),_,I1), |
| 1548 | | add_important_info_from_super_expression(I0,I1,Info), |
| 1549 | | % no need to apply rule if already transformed into avl in cleanup_pre, hence we do not call is_set_extension |
| 1550 | | construct_inter_from_list(LIST,Type,Info,TRes), |
| 1551 | | !, |
| 1552 | | (debug_mode(on) -> print('translated_general_intersection: '), translate:print_bexpr(TRes),nl ; true), |
| 1553 | | get_texpr_expr(TRes,Res). |
| 1554 | | cleanup_post(SUB,pred,I0,FORALL,pred,FInfo,multi/general_union_subset) :- |
| 1555 | | is_subset(SUB,UNION,T), |
| 1556 | | % union(S) <: T ===> !x.(x:S => x <: T) |
| 1557 | | % currently: subsets of T may be generated, but it does not propagate well to S |
| 1558 | | UNION = b(general_union(S),_,_), |
| 1559 | | !, |
| 1560 | | get_unique_id_inside('_zzzz_unary',S,T,ID), |
| 1561 | | get_texpr_type(S,SType), TID = b(identifier(ID),SType,[generated]), |
| 1562 | | safe_create_texpr(member(TID,S),pred,LHS), |
| 1563 | | safe_create_texpr(subset(TID,T),pred,RHS), |
| 1564 | | create_implication(LHS,RHS,NewForallBody), |
| 1565 | | create_forall([TID],NewForallBody,TFORALL), |
| 1566 | | TFORALL = b(FORALL,pred,I1), |
| 1567 | | add_important_info_from_super_expression(I0,I1,FInfo), |
| 1568 | | % see test 1854, and ProZ ROZ/model.tex |
| 1569 | | (debug_mode(on) -> print('translated_general_union subset: '), translate:print_bexpr(TFORALL),nl ; true). |
| 1570 | | cleanup_post(size(Seq),integer,Info,Res,integer,Info,multi/size_append) :- |
| 1571 | | get_texpr_expr(Seq,concat(A,B)), |
| 1572 | | % size(A^B) = size(A)+size(B) useful e.g. for test 1306 |
| 1573 | | !, |
| 1574 | | Res = add(b(size(A),integer,Info),b(size(B),integer,Info)). |
| 1575 | | cleanup_post(concat(A,B),Type,I0,Seq,Type,[was(concat)|NewInfo],multi/concat_empty) :- |
| 1576 | | (is_empty_set(A) -> b(Seq,_,I1)=B |
| 1577 | | ; is_empty_set(B) -> b(Seq,_,I1)=A),!, |
| 1578 | | add_important_info_from_super_expression(I0,I1,NewInfo). |
| 1579 | | cleanup_post(E,integer,I,Res,integer,[was(Operator)|I],multi/constant_expression) :- |
| 1580 | | pre_compute_static_int_expression(E,Result),!, |
| 1581 | | functor(E,Operator,_), |
| 1582 | | debug_println(9,pre_computed(Operator,Result)), |
| 1583 | | Res = integer(Result). |
| 1584 | | cleanup_post(min(Interval),integer,I0,Res,integer,Info,multi/eval_min_interval) :- |
| 1585 | | is_interval_or_singleton(Interval,Low,Up), |
| 1586 | | get_integer(Low,L), number(L), |
| 1587 | | get_integer(Up,U), number(U), L =< U, % non-empty interval |
| 1588 | | debug_println(5,simplified_min_interval(L,U,L)), |
| 1589 | | Res = integer(L), get_texpr_info(Low,I1), |
| 1590 | | add_important_info_from_super_expression(I0,I1,Info). |
| 1591 | | cleanup_post(max(Interval),integer,I0,Res,integer,Info,multi/eval_max_interval) :- |
| 1592 | | is_interval_or_singleton(Interval,Low,Up), |
| 1593 | | get_integer(Low,L), number(L), |
| 1594 | | get_integer(Up,U), number(U), L =< U, % non-empty interval |
| 1595 | | debug_println(5,simplified_max_interval(L,U,U)), |
| 1596 | | Res = integer(U), get_texpr_info(Low,I1), |
| 1597 | | add_important_info_from_super_expression(I0,I1,Info). |
| 1598 | | cleanup_post(first(Seq),Type,I0,Res,Type,Info,multi/first_seq_extension) :- |
| 1599 | | is_sequence_extension(Seq,List), List = [First|Rest], |
| 1600 | | (Rest == [] -> true ; preferences:get_preference(disprover_mode,true)), % we may remove WD issue otherwise (TO DO: check if Rest contains any problematic elements) |
| 1601 | | !, |
| 1602 | | First = b(Res,Type,I1), |
| 1603 | | add_important_info_from_super_expression(I0,I1,Info). |
| 1604 | | cleanup_post(last(Seq),Type,I0,Res,Type,Info,multi/first_seq_extension) :- |
| 1605 | | is_sequence_extension(Seq,List), List = [First|Rest], |
| 1606 | | (Rest == [] -> true ; preferences:get_preference(disprover_mode,true)), % we may remove WD issue otherwise (TO DO: check if list contains any problematic elements) |
| 1607 | | !, |
| 1608 | | last([First|Rest],b(Res,Type,I1)), |
| 1609 | | add_important_info_from_super_expression(I0,I1,Info). |
| 1610 | | cleanup_post(function(Override,X),Type,I0,Res,Type,Info,multi/function_override) :- |
| 1611 | | preferences:get_preference(disprover_mode,true), % only applied in Disprover mode as it can remove WD problem; TO DO make it also applicable in normal mode |
| 1612 | | get_texpr_expr(Override,overwrite(_F,SEXt)), |
| 1613 | | SEXt = b(set_extension(LIST),_,_), |
| 1614 | | member(b(couple(From,To),_,_),LIST), |
| 1615 | | same_texpr(From,X), |
| 1616 | | % ( F <+ { ... X|->To ...}) (X) ==> To |
| 1617 | | %translate:print_bexpr(b(function(Override,X),Type,_I)), print(' ==> '), translate:print_bexpr(To),nl, |
| 1618 | | !, |
| 1619 | | get_texpr_expr(To,Res), |
| 1620 | | get_texpr_info(To,I1), |
| 1621 | | add_important_info_from_super_expression(I0,I1,Info). |
| 1622 | | cleanup_post(function(Override,X),Type,Info,Res,Type,Info,multi/function_override_ifte) :- |
| 1623 | | preferences:get_preference(disprover_mode,true), % only applied in Disprover mode as it can remove WD |
| 1624 | | % TO DO: should we do this generally? or simply deal with overwrite symbolically always? |
| 1625 | | get_texpr_expr(Override,overwrite(F,SEXt)), |
| 1626 | | SEXt = b(set_extension([Couple]),_,_), |
| 1627 | | Couple = b(couple(From,To),_,_), |
| 1628 | | % f <+ {A|->B}(x) -> if_then_else(x=A,B,f(x)) ; avoids having to explicitly compute f<+{A|->B} |
| 1629 | | Res = if_then_else(EqXFrom,To,FX), |
| 1630 | | safe_create_texpr(equal(X,From),pred,EqXFrom), |
| 1631 | | safe_create_texpr(function(F,X),Type,FX). % , translate:print_bexpr(b(Res,Type,Info)),nl. |
| 1632 | | cleanup_post(function(SEXt,ARG),Type,I0,Res,Type,Info,multi/function_set_extension) :- |
| 1633 | | SEXt = b(set_extension(LIST),_,ListInfos), % TO DO: also support b(value(avl_set(A)),_,_) |
| 1634 | | eval_set_extension(ARG,Value), %nl,print(arg(Value)),nl, |
| 1635 | | select(b(couple(LHS,RHS),_,_),LIST,REST), |
| 1636 | | (member(contains_wd_condition,ListInfos) % then we could remove WD problem, e.g., r = {1|->2, 2|-> 1/0}(1) |
| 1637 | | -> (preferences:preference(find_abort_values,false) ; |
| 1638 | | preferences:get_preference(disprover_mode,true)) |
| 1639 | | ; true), |
| 1640 | | eval_set_extension(LHS,Value), %nl,print(found(RHS)),nl, |
| 1641 | | % WE NEED TO Check that all LHS can be compared against ARG |
| 1642 | | \+ member((b(couple(LHS2,_),_,_),REST),eval_set_extension(LHS2,Value)), % no other potential match |
| 1643 | | \+ member((b(couple(LHS3,_),_,_),LIST), \+ eval_set_extension(LHS3,_)), % all left-hand-sides can be evaluated |
| 1644 | | !, get_texpr_expr(RHS,Res), get_texpr_info(RHS,I1), |
| 1645 | | add_important_info_from_super_expression(I0,I1,Info). |
| 1646 | | % Detect if_then_else in format as printed by pp_expr2(if_then_else( ....)...) or as generated by B2TLA: |
| 1647 | | cleanup_post(function(IFT,DUMMYARG),Type,Info,if_then_else(IFPRED,THEN,ELSE),Type,Info,multi/function_if_then_else) :- |
| 1648 | | is_if_then_else(IFT,DUMMYARG,IFPRED,THEN,ELSE), |
| 1649 | | (debug_mode(off) -> true |
| 1650 | | ; print('% Recognised if-then-else expression: IF '), translate:print_bexpr(IFPRED), |
| 1651 | | print(' THEN '),translate:print_bexpr(THEN), print(' ELSE '),translate:print_bexpr(ELSE),nl |
| 1652 | | ). |
| 1653 | | cleanup_post(function(Composition,X),Type,Info,function(G,FX),Type,Info,multi/function_composition) :- |
| 1654 | ? | (data_validation_mode ; |
| 1655 | | get_preference(convert_comprehension_sets_into_closures,true) % there it can make a big difference in particular since relational composition (rel_composition_wf -> rel_compose_with_inf_fun case) was not fully symbolic; see Systerel data validation examples |
| 1656 | | ), |
| 1657 | | Composition = b(composition(F,G),_,_), |
| 1658 | | % (F;G)(X) --> G(F(X)) |
| 1659 | | get_texpr_type(G,set(couple(TypeFX,_))), |
| 1660 | | safe_create_texpr(function(F,X),TypeFX,Info,FX), |
| 1661 | | (debug_mode(off) -> true |
| 1662 | | ; print('COMPOSITION translated to: '),translate:print_bexpr(b(function(G,FX),Type,Info)),nl). |
| 1663 | | /* |
| 1664 | | cleanup_post(function(Lambda,Argument),Type,I,assertion_expression(Cond,ErrMsg,Expr),Type,I,multi/lambda_guard2) :- |
| 1665 | | get_texpr_info(Lambda,IL), member(was(lambda),IL), |
| 1666 | | print(function(Lambda,Argument)),nl, |
| 1667 | | get_texpr_expr(Lambda,comprehension_set([TId1,TId2,LAMBDARES],TPre,TVal)), |
| 1668 | | Argument=b(couple(Argument1,Argument2),_,_), |
| 1669 | | !, % TO DO: support for functions of multiple arguments |
| 1670 | | get_texpr_id(TId1,Id1), |
| 1671 | | get_texpr_id(TId2,Id2), |
| 1672 | | ErrMsg = 'function called outside of domain: ', |
| 1673 | | ~~mnf( replace_id_by_expr(TPre,Id1,Argument1,Cond1) ), |
| 1674 | | ~~mnf( replace_id_by_expr(TVal,Id1,Argument1,Expr1) ), |
| 1675 | | ~~mnf( replace_id_by_expr(Cond1,Id2,Argument2,Cond) ), |
| 1676 | | ~~mnf( replace_id_by_expr(Expr1,Id2,Argument2,Expr) ). */ |
| 1677 | | cleanup_post(range(SETC),Type,I, comprehension_set(RangeIds2,NewCompPred),Type,I,single/range_setcompr) :- |
| 1678 | | % translate ran({x1,...xn|P}) into {xn| #(x1,...).(P)} ; particularly interesting if x1... contains large datavalues (e.g., C_02_001.mch from test 1131) |
| 1679 | | get_texpr_expr(SETC,comprehension_set(CompIds,CompPred)), |
| 1680 | | get_domain_range_ids(CompIds,DomainIds,RangeIds), % print(range(CompIds,DomainIds,RangeIds)),nl, |
| 1681 | | %\+((member(ID,RangeIds),get_texpr_id(ID,'_lambda_result_'))), % for test 612; maybe disable optimisation if memory consumption of variables small |
| 1682 | | !, % TO DO: also detect patterns such as dom(dom( or ran(ran( ... [Done ??] |
| 1683 | | rename_lambda_result_id(RangeIds,CompPred,RangeIds2,CompPred1), |
| 1684 | | rename_lambda_result_id(DomainIds,CompPred1,DomainIds2,CompPred2), |
| 1685 | | create_outer_exists_for_dom_range(DomainIds2,CompPred2,NewCompPred), % will mark the exists; so that during expansion we will treat it differently for enumeration |
| 1686 | | (debug_mode(off) -> true |
| 1687 | | ; print('Encode range as existential quantification: '), translate:print_bexpr(NewCompPred),nl). |
| 1688 | | cleanup_post(domain(SETC),Type,I, comprehension_set(DomainIds2,NewCompPred),Type,I,single/domain_setcompr) :- |
| 1689 | | % translate dom({x1,...xn|P}) into {x1,..| #(xn).(P)} ; particularly interesting if xn contains large datavalues |
| 1690 | | % used to fail test 306 ; fixed by allow_to_lift_exists annotation |
| 1691 | | get_texpr_expr(SETC,comprehension_set(CompIds,CompPred)), |
| 1692 | | get_domain_range_ids(CompIds,DomainIds,RangeIds), % print(domain(CompIds,DomainIds,RangeIds)),nl, |
| 1693 | | % \+ (member(ID,CompIds),get_texpr_id(ID,'_lambda_result_')), |
| 1694 | | % WE HAVE TO BE CAREFUL if xn = LAMBDA_RESULT ; TO DO rename like above for range |
| 1695 | | % example from test 292: rel(fnc({x,y|x:1..10 & y:1..x})) = {x,y|x:1..10 & y:1..x} |
| 1696 | | !, |
| 1697 | | % TO DO: detect when closure is lambda; e.g., for e.g. dom(pred) = INTEGER in test 292 : split(CompIds,Args,Types), closures:is_lambda_value_domain_closure(Args,Types,B, DomainValue, _),; currently create_exists_opt deals with most of this |
| 1698 | | rename_lambda_result_id(DomainIds,CompPred,DomainIds2,CompPred1), |
| 1699 | | rename_lambda_result_id(RangeIds,CompPred1,RangeIds2,CompPred2), |
| 1700 | | create_outer_exists_for_dom_range(RangeIds2,CompPred2,NewCompPred), |
| 1701 | | (debug_mode(off) -> true |
| 1702 | | ; print('Encode domain as existential quantification: '),translate:print_bexpr(NewCompPred),nl). |
| 1703 | | cleanup_post(domain(SETC),Type,I, comprehension_set(DomainIds,RestPred),Type,I,single/domain_setcompr) :- |
| 1704 | | % translate dom({x1,...xn|P & xn=E}) into {x1,..| P} ; particularly interesting if xn contains large datavalues |
| 1705 | | get_texpr_expr(SETC,comprehension_set(CompIds,CompPred)), |
| 1706 | | get_domain_range_ids(CompIds,DomainIds,RangeIds), % print(domain(CompIds,DomainIds,RangeIds)),nl, |
| 1707 | | \+ (member(ID,CompIds),get_texpr_id(ID,'_lambda_result_')), |
| 1708 | | conjunction_to_list(CompPred,Preds), |
| 1709 | | RangeIds = [TId], |
| 1710 | | get_sorted_ids(RangeIds,Blacklist), |
| 1711 | | select_equality(TId,Preds,Blacklist,_Eq,_Expr,RestPreds,_,check_well_definedness), % We could do check_well_definedness only if preference set |
| 1712 | | conjunct_predicates(RestPreds,RestPred), |
| 1713 | | not_occurs_in_predicate(Blacklist,RestPred), |
| 1714 | | !, |
| 1715 | | % TO DO: use create_optimized exists; also treat inner existential quantification and merge |
| 1716 | | (debug_mode(off) -> true |
| 1717 | | ; print('Encode domain of lambda abstraction: '),translate:print_bexpr(RestPred),nl). |
| 1718 | | cleanup_post(comprehension_set([TID],Pred),Type,I, |
| 1719 | | struct(b(rec(NewFieldSets),record(FieldTypes),I)), |
| 1720 | | Type,I,single/simplify_record) :- |
| 1721 | | % {r|r'a : 1..1000 & r'b : 1..100 & r:struct(a:INTEGER,b:NAT,c:BOOL)} --> struct(a:1..1000,b:1..100,c:BOOL) |
| 1722 | | % these kind of set comprehensions are generated by ProZ, see ROZ example model.tex |
| 1723 | | % TO DO: maybe generalise this optimisation: currently it only works if all predicates can be assimilated into struct expression |
| 1724 | | TID = b(identifier(ID),record(FieldTypes),_), |
| 1725 | | conjunction_to_list(Pred,PL), |
| 1726 | | l_update_record_field_membership(PL,ID,[],FieldSetsOut), |
| 1727 | | maplist(construct_field_sets(FieldSetsOut),FieldTypes,NewFieldSets), |
| 1728 | | print('Detected Record set comprehension: '),translate:print_bexpr(b(struct(b(rec(NewFieldSets),record(FieldTypes),I)),Type,I)),nl. |
| 1729 | | cleanup_post(precondition(TP,TS),subst,I0,S,subst,Info,multi/remove_triv_precondition) :- |
| 1730 | | % remove trivial preconditions |
| 1731 | | get_texpr_expr(TP,truth),!, |
| 1732 | | get_texpr_expr(TS,S),get_texpr_info(TS,I1), |
| 1733 | | add_important_info_from_super_expression(I0,I1,Info). |
| 1734 | | cleanup_post(comprehension_set(Ids1,E),T,I,comprehension_set(Ids2,E2),T,I,single/detect_lambda) :- |
| 1735 | ? | preferences:get_preference(detect_lambdas,true), |
| 1736 | | % creates *** Enumerating lambda result warnings for test 1162 |
| 1737 | ? | E = b(conjunct(LHS,Equality),pred,Info), nonmember(prob_annotation('LAMBDA'),Info), % not already processed |
| 1738 | ? | identifier_equality(Equality,ID,TID1,Expr1), |
| 1739 | ? | last(Ids1,TID), get_texpr_id(TID,ID), |
| 1740 | ? | not_occurs_in_predicate([ID],LHS), |
| 1741 | ? | !, |
| 1742 | ? | get_texpr_info(Equality,EqInfo), |
| 1743 | ? | get_unique_id_inside('_lambda_result_',LHS,Expr1,ResultId), % currently the info field lambda_result is not enough: several parts of the ProB kernel match on the identifier name '_lambda_result_' |
| 1744 | ? | TID1 = b(identifier(_),Type1,Info1), |
| 1745 | ? | add_texpr_infos(b(identifier(ResultId),Type1,Info1),[lambda_result],TID2), |
| 1746 | ? | Equality2 = b(equal(TID2,Expr1),pred,[lambda_result|EqInfo]), |
| 1747 | ? | E2 = b(conjunct(LHS,Equality2),pred,[prob_annotation('LAMBDA')|Info]), |
| 1748 | ? | append(Ids0,[_],Ids1), |
| 1749 | | append(Ids0,[TID2],Ids2), |
| 1750 | | (debug:debug_mode(off) -> true ; format('Lambda using ~w detected: ',[ID]),translate:print_bexpr(E2),nl). |
| 1751 | | % code below is simpler, but has disadvantage of losing position info for equality: |
| 1752 | | %cleanup_post(comprehension_set(Ids1,E),T,I,lambda(Ids2,LHS,Expr),T,I,single/detect_lambda) :- |
| 1753 | | % E = b(conjunct(LHS,Equality),pred,Info), nonmember(prob_annotation('LAMBDA'),Info), % not already processed |
| 1754 | | % identifier_equality(Equality,ID,_,Expr), |
| 1755 | | % last(Ids1,TID), get_texpr_id(TID,ID), |
| 1756 | | % not_occurs_in_predicate([ID],LHS), |
| 1757 | | % append(Ids2,[TID],Ids1), |
| 1758 | | % print('Lambda detected: '),translate:print_bexpr(E),nl,!. |
| 1759 | | % |
| 1760 | | cleanup_post(sequence([S1,b(sequence(S2),subst,_)]),subst,I,sequence([S1|S2]),subst,I, single/flatten_sequence2) :- |
| 1761 | | debug_println(9,flatten_sequence2). % do we need something for longer sequences? |
| 1762 | | cleanup_post(sequence([b(sequence(S1),subst,_)|S2]),subst,I,sequence(NewSeq),subst,I, single/flatten_sequence1) :- |
| 1763 | | append(S1,S2,NewSeq), |
| 1764 | | % avoid maybe calling filter_useless_subst_in_sequence again |
| 1765 | | debug_println(9,flatten_sequence1). |
| 1766 | | cleanup_post(sequence(S1),subst,I,sequence(S2),subst,I, single/remove_useless_subst_in_seuence) :- |
| 1767 | | get_preference(useless_code_elimination,true), |
| 1768 | | filter_useless_subst_in_sequence(S1,Change,S2), debug_println(filter_sequence(9,Change)). |
| 1769 | | cleanup_post(sequence(Statements),subst,I,Result,subst,I, single/sequence_to_multi_assign) :- |
| 1770 | | % merge sequence of assignments if possible |
| 1771 | | merge_assignments(Statements,Merge,New), Merge==merged, |
| 1772 | | construct_sequence(New,Result). |
| 1773 | | % nl,print('Merged: '),translate:print_subst(b(Result,subst,I)),nl,nl. |
| 1774 | | cleanup_post(parallel(Statements),subst,I,Result,subst,I, single/parallel_to_multi_assign) :- |
| 1775 | | % this merges multiple assignments into a single one: advantage: only one waitflag set up |
| 1776 | | % should probably not be done in INITIALISATION |
| 1777 | | % print(parallel(Statements)),nl,trace, |
| 1778 | | extract_assignments(Statements,LHS,RHS,Rest,Nr), % print(extracted(Nr,LHS)),nl, |
| 1779 | | Nr>1,!, |
| 1780 | | (debug_mode(on) -> |
| 1781 | | print('Parallel to Assignment: '), translate:print_subst(b(parallel(Statements),subst,I)),nl |
| 1782 | | ; true), |
| 1783 | | (Rest == [] -> Result = assign(LHS,RHS) |
| 1784 | | ; Result = parallel([b(assign(LHS,RHS),subst,[])|Rest])). |
| 1785 | | %translate:print_subst(b(Result,subst,I)),nl. |
| 1786 | | cleanup_post(select([CHOICE|Rest]),subst,I0,S,subst,Info,single/remove_select) :- |
| 1787 | | Rest = [], % SELECT can have multiple true branches |
| 1788 | | CHOICE=b(select_when(TRUTH,Subst),subst,_), |
| 1789 | | is_truth(TRUTH),!, |
| 1790 | | print('Removing useless SELECT'),nl, |
| 1791 | | get_texpr_expr(Subst,S),get_texpr_info(Subst,I1), |
| 1792 | | add_important_info_from_super_expression(I0,I1,Info). |
| 1793 | | cleanup_post(select([CHOICE|Rest],_ELSE),subst,OldInfo,Res,subst,I,single/remove_select_else) :- |
| 1794 | | CHOICE=b(select_when(TRUTH,Subst),subst,_), |
| 1795 | | is_truth(TRUTH),!, |
| 1796 | | (Rest = [] % completely useless SELECT |
| 1797 | | -> print('Removing useless SELECT'),nl, |
| 1798 | | get_texpr_expr(Subst,Res),get_texpr_info(Subst,I1), |
| 1799 | | add_important_info_from_super_expression(OldInfo,I1,I) |
| 1800 | | ; print('Removing useless SELECT ELSE branch'),nl, |
| 1801 | | Res = select([CHOICE|Rest]), I=OldInfo). |
| 1802 | | cleanup_post(let_expression([],[],TExpr),Type,I0,Expr,Type,I,multi/remove_let_expression) :- !, |
| 1803 | | % remove trivial let expressions without any introduced identifiers |
| 1804 | | % this rule makes only sense in combination with the next rule which removes |
| 1805 | | % simple let identifiers |
| 1806 | | get_texpr_expr(TExpr,Expr), |
| 1807 | | get_texpr_info(TExpr,I1), |
| 1808 | | add_important_info_from_super_expression(I0,I1,I). |
| 1809 | | cleanup_post(let([],Pred,TExpr),Type,I0,Expr,Type,I,multi/remove_let) :- is_truth(Pred),!, |
| 1810 | | % remove trivial let expressions without any introduced identifiers |
| 1811 | | % this rule makes only sense in combination with the next rule which removes |
| 1812 | | % simple let identifiers |
| 1813 | | get_texpr_expr(TExpr,Expr), |
| 1814 | | get_texpr_info(TExpr,I1), |
| 1815 | | add_important_info_from_super_expression(I0,I1,I). |
| 1816 | | cleanup_post(let_expression(Ids,Exprs,Expr),Type,I, |
| 1817 | | let_expression(NIds,NExprs,NExpr),Type,I,multi/remove_let_expression2) :- |
| 1818 | ? | simplify_let(Ids,Exprs,Expr,NIds,NExprs,NExpr),!. |
| 1819 | | cleanup_post(let_predicate(Ids,Exprs,Expr),Type,I, |
| 1820 | | let_predicate(NIds,NExprs,NExpr),Type,I,multi/remove_let_predicate2) :- |
| 1821 | ? | simplify_let(Ids,Exprs,Expr,NIds,NExprs,NExpr),!, |
| 1822 | | true. |
| 1823 | | %print(simplified_let),nl, translate:print_bexpr(b(let_predicate(Ids,Exprs,Expr),pred,I)), print(' INTO : '),nl, translate:print_bexpr(b(let_predicate(NIds,NExprs,NExpr),pred,I)),nl, nl. |
| 1824 | | % was disabled because simplify_let_subst also replaced in RHS of assignments |
| 1825 | | % but now we check that a LET/ANY variable cannot be assigned to statically |
| 1826 | | % so it should be safe now to replace simple equalities: |
| 1827 | | cleanup_post(let(Ids,Pred,Subst),Type,I, |
| 1828 | | let(NIds,NPred,NSubst),Type,I,multi/remove_let_subst2) :- |
| 1829 | | simplify_let_subst(Ids,Pred,Subst,NIds,NPred,NSubst),! , |
| 1830 | | true. % translate:print_subst(b(let(NIds,NPred,NSubst),subst,[])),nl. |
| 1831 | | /* this is not used currently; as the generic code's performance has been improved |
| 1832 | | and better propagation is ensured by b_compute_arith_expression which (partially) instantiates its argument (known to be an integer) |
| 1833 | | cleanup_post(ArithPredicate,pred,Info,ArithPredicate,pred,NewInfo,single/add_arith_pred_info) :- |
| 1834 | | comparison(ArithPredicate,LHS,RHS,_,_,_), |
| 1835 | | \+ clpfd_arith_integer_expression(LHS), |
| 1836 | | \+ clpfd_arith_integer_expression(RHS), |
| 1837 | | !, |
| 1838 | | % store the information that there is no use in doing b_compute_arith_expression special treatment |
| 1839 | | NewInfo = [no_clpfd_arith_integer_expression|Info]. |
| 1840 | | */ |
| 1841 | | |
| 1842 | | cleanup_post(forall([ID],LHS,RHS),pred,IOld,Res,pred,IOld,single/expand_forall_set_extension) :- |
| 1843 | | % expand !x.(x:{a,b,...} => RHS) into conjunction |
| 1844 | | % can be useful e.g. for KODKOD when we pick an element from a set of sets |
| 1845 | | preferences:get_preference(try_kodkod_on_load,true), % at the moment only enable in Kodkod mode |
| 1846 | | % TO DO: enable always; but maybe check that set_extension can be computed (which eval_set_extension will do) to avoid duplicating checks (!y.(y:{v,w} => expensive_pred) + what if v=w |
| 1847 | | nonmember(do_not_optimize_away,IOld), |
| 1848 | | get_texpr_expr(LHS,member(ID2,Set)), |
| 1849 | | same_texpr(ID,ID2), |
| 1850 | | is_set_extension(Set,SList), |
| 1851 | | get_texpr_id(ID,AID), |
| 1852 | | debug_format(19,'Expanding forall ~w ',[AID]), |
| 1853 | | findall(C, (member(SEL,SList),replace_id_by_expr(RHS,AID,SEL,C)),Conjuncts), |
| 1854 | | conjunct_predicates(Conjuncts,ExpandedForAll), |
| 1855 | | (silent_mode(on) -> true ; translate:print_bexpr(ExpandedForAll),nl), |
| 1856 | | get_texpr_expr(ExpandedForAll,Res). |
| 1857 | | cleanup_post(forall(Ids1,LHS,RHS),pred,IOld, |
| 1858 | | forall(Ids,NewLHS,NewRHS),pred,INew,multi/merge_forall) :- |
| 1859 | | is_truth(LHS), |
| 1860 | | RHS = b(forall(Ids2,NewLHS,NewRHS),pred,_), |
| 1861 | | %((member(b(identifier(_),Type,_),Ids1), is_infinite_type(Type)) -> true), % could be useful for tests 1441, 1447 ?? |
| 1862 | | (disjoint_ids(Ids1,Ids2) |
| 1863 | | -> append(Ids1,Ids2,Ids), |
| 1864 | | % !x.(truth => !y.(P=>Q) <==> !(x,y).(P=>Q) |
| 1865 | | (debug_mode(off) -> true ; format('Merging forall ~w: ',[Ids]), translate:print_bexpr(NewLHS),nl), |
| 1866 | | add_removed_typing_info(IOld,INew) |
| 1867 | | ; \+ preferences:get_preference(disprover_mode,true), |
| 1868 | | translate:translate_bexpression(b(forall(Ids1,LHS,RHS),pred,IOld),PS), |
| 1869 | | add_warning(b_ast_cleanup,'Variable clash in nested universal quantification: ',PS,IOld), |
| 1870 | | fail |
| 1871 | | ). |
| 1872 | | cleanup_post(forall(Ids,LHS,RHS),pred,IOld, |
| 1873 | | implication(Outer,FORALL),pred,IOld,single/detect_global_preds_forall1) :- |
| 1874 | | % !x.(P(x) & Q => R(x) <==> Q => !x.(P(x) => R(x)) |
| 1875 | | % TO DO: maybe we should not lift things like printf, ... ? |
| 1876 | | bsyntaxtree:detect_global_predicates(Ids,LHS,Outer,Inner), |
| 1877 | | (debug_mode(off) -> true ; format('Lifting predicate (lhs) of forall ~w: ',[Ids]), translate:print_bexpr(Outer),nl), |
| 1878 | | construct_inner_forall(Ids,Inner,RHS,IOld,FORALL). |
| 1879 | | % TO DO: implement similar lifting rules for exists(Ids,P) |
| 1880 | | cleanup_post(forall(Ids,LHS,RHS),pred,IOld, |
| 1881 | | conjunct(Outer,FORALL),pred,IOld,single/detect_global_preds_forall2) :- |
| 1882 | | is_truth(LHS), |
| 1883 | | % !x.(truth => Q & R(x) <==> Q & !x.(truth => R(x)) |
| 1884 | | bsyntaxtree:detect_global_predicates(Ids,RHS,Outer,Inner), |
| 1885 | | (debug_mode(off) -> true ; format('Lifting predicate (rhs &) of forall ~w: ',[Ids]), translate:print_bexpr(Outer),nl), |
| 1886 | | construct_inner_forall(Ids,LHS,Inner,IOld, FORALL). % translate:print_bexpr(FORALL),nl,nl. |
| 1887 | | cleanup_post(forall(Ids,LHS,RHS),pred,IOld, |
| 1888 | | implication(Outer,FORALL),pred,IOld,single/detect_global_preds_forall3) :- |
| 1889 | | is_truth(LHS), |
| 1890 | | RHS = b(implication(RHS1,RHS2),pred,_), |
| 1891 | | % !x.(truth => (Q & R(x) => S(x)) <==> Q => !x.(truth => R(x) => S(x)) |
| 1892 | | bsyntaxtree:detect_global_predicates(Ids,RHS1,Outer,Inner), |
| 1893 | | create_implication(Inner,RHS2,NewRHS), |
| 1894 | | (debug_mode(off) -> true ; format('Lifting predicate (rhs =>) of forall ~w: ',[Ids]), translate:print_bexpr(Outer),nl), |
| 1895 | | construct_inner_forall(Ids,LHS,NewRHS,IOld, FORALL). |
| 1896 | | cleanup_post(forall([TID1,TID2|OTHER],LHS,RHS),pred,IOld, |
| 1897 | | forall([TID1,TID2|OTHER],NewLHS,RHS),pred,[prob_symmetry(ID1,ID2)|IOld],single/symmetry_detection) :- |
| 1898 | | % DETECT Symmetries such as !(x,y).(x /= y => x=TRUE or y=TRUE) |
| 1899 | | % !(x2,y).(x2 /= y & x2:s & y:s => x2=aa or y=aa) |
| 1900 | | % f:1..n --> 1..(n-1) & !(x,y).(x/=y &x:dom(f) & y:1..n => f(x) /= f(y)) & n=9 (runtime 1 sec -> 0.78 sec) |
| 1901 | | get_texpr_type(TID1,T), get_texpr_type(TID2,T), |
| 1902 | | preferences:get_preference(try_kodkod_on_load,false), % Kodkod cannot properly deal with LEQ_SYM_BREAK, treats it like truth |
| 1903 | | preferences:get_preference(use_static_symmetry_detection,true), |
| 1904 | | sym_break_supported_type(T), % LEQ_SYM_BREAK not yet fully functional with SET types; TO DO: fix |
| 1905 | | get_texpr_id(TID1,ID1), get_texpr_id(TID2,ID2), |
| 1906 | | nonmember(prob_symmetry(ID1,ID2),IOld), |
| 1907 | | rename_bt(LHS,[rename(ID1,ID2),rename(ID2,ID1)],LHS2), |
| 1908 | | same_norm_texpr(LHS,LHS2), |
| 1909 | | %print(lhs_symmetric),nl, |
| 1910 | | rename_bt(RHS,[rename(ID1,ID2),rename(ID2,ID1)],RHS2), |
| 1911 | | same_norm_texpr(RHS,RHS2), |
| 1912 | | %print(rhs_symmetric(ID1,ID2)),nl, |
| 1913 | | construct_sym_break(T,TID1,TID2,LHS,SYMBREAK), |
| 1914 | | conjunct_predicates([LHS,SYMBREAK],NewLHS), |
| 1915 | | (debug_mode(off) -> true |
| 1916 | | ; format('SYMMETRY BREAKING FORALL: !(~w,~w).(',[ID1,ID2]),translate:print_bexpr(NewLHS), |
| 1917 | | print(' => '), translate:print_bexpr(RHS),print(')'),nl). |
| 1918 | | cleanup_post(forall(AllIds,P,Rhs),pred,I,NewPred,pred,INew,multi/forall_splitting) :- |
| 1919 | | AllIds = [TID1|TRestIDs], TRestIDs = [_|_], % TO DO: maybe not require that TID1 is the first id |
| 1920 | | get_preference(use_clpfd_solver,true), % with CLPFD false: maybe more likely to reduce performance |
| 1921 | | % NOTE: we could destroy symmetry reduction detection if TRestIDs = [TID2], but we run after symmetry detection |
| 1922 | | % !(x,y,...).(x:SET & RestPred => Rhs) == !x.(x:SET => !(y,..).(RestPred => Rhs)) |
| 1923 | | conjunction_to_list(P,[MEM|RestPreds]), |
| 1924 | ? | is_membership(MEM,TID,Set,_), |
| 1925 | | same_id(TID1,TID,_ID), |
| 1926 | | \+ known_set(Set), % rewriting makes sense if Set is not fully known and will be instantiated during solving |
| 1927 | | % prevent !(x,y).(x:NATURAL & x<10 & y :1..x => x+y<20), even though it seems to work nonetheless |
| 1928 | | get_sorted_ids(TRestIDs,RestIDs), |
| 1929 | | not_occurs_in_predicate(RestIDs,Set), |
| 1930 | | NewPred = forall([TID1],MEM,InnerForall), |
| 1931 | | conjunct_predicates(RestPreds,InnerForallLhs), |
| 1932 | | construct_inner_forall(TRestIDs,InnerForallLhs,Rhs,I,InnerForall), |
| 1933 | | !, |
| 1934 | | add_removed_typing_info(I,INew), |
| 1935 | | (debug_mode(on) -> print('FORALL SPLITTING for better propagation: '), |
| 1936 | | translate:print_bexpr(b(NewPred,pred,[])),nl |
| 1937 | | ; true). |
| 1938 | | cleanup_post(exists([TID],MemPred),pred,IOld, |
| 1939 | | Res,pred,IOld, single/replace_exists_by_not_empty) :- |
| 1940 | | % simplify #ID.(ID:E) <=> E /= {} |
| 1941 | | % simplify #ID.(ID:E1 & ID:E2) <=> E1 /\ E2 /= {} , etc... |
| 1942 | | % important e.g. for y:20..30000000000 & not(#x.(x:1..10 & x:8..y)) |
| 1943 | ? | is_valid_id_member_check(MemPred,TID,E), |
| 1944 | | !, |
| 1945 | | (definitely_not_empty_set(E) -> Res= truth |
| 1946 | | ; get_texpr_type(E,Type), EmptySet=b(empty_set,Type,[]), |
| 1947 | | Res = not_equal(E,EmptySet)), |
| 1948 | | (debug_mode(off) -> true |
| 1949 | | ; get_texpr_id(TID,ID), |
| 1950 | | format('Removing existential quantifier: ~w~n',[ID]), |
| 1951 | | translate:print_bexpr(b(Res,pred,IOld)),nl). |
| 1952 | | cleanup_post(exists([TID],b(NotMemPred,_,_)),pred,IOld, |
| 1953 | | not_equal(E,TypeExpr),pred,IOld, single/replace_exists_by_not_full) :- |
| 1954 | | % simplify #ID.(ID/:E) <=> E /= FullType |
| 1955 | | % important e.g. for y:7..30000000000 & not(#x.(x /: 1..y)) |
| 1956 | | is_not_member(NotMemPred,MID,E), |
| 1957 | | same_id(TID,MID,SID), |
| 1958 | | % + check that MID does not occur in E |
| 1959 | | \+ occurs_in_expr(SID,E), |
| 1960 | | get_texpr_type(E,SType), |
| 1961 | | bsyntaxtree:is_set_type(SType,Type), |
| 1962 | | translate:set_type_to_maximal_texpr(Type,TypeExpr), % Note: no longer introduces identifiers but value(.) results |
| 1963 | | !, |
| 1964 | | (debug_mode(off) -> true |
| 1965 | | ; format('Removing existential quantifier: ~w~n',[SID]), |
| 1966 | | translate:print_bexpr(b(not_equal(E,TypeExpr),pred,IOld)),nl). |
| 1967 | | cleanup_post(exists([TID],b(Pred,_,_)),pred,IOld, |
| 1968 | | truth,pred,IOld, single/replace_exists_by_truth) :- |
| 1969 | | b_interpreter_check:arithmetic_op(Pred,_Op,X,Y), |
| 1970 | | ( (same_id(TID,X,SID), \+ occurs_in_expr(SID,Y), always_well_defined_or_disprover_mode(Y)) ; |
| 1971 | | (same_id(TID,Y,SID), \+ occurs_in_expr(SID,X), always_well_defined_or_disprover_mode(X)) |
| 1972 | | ), |
| 1973 | | !, % we have a formula of the form #SID.(SID > Expr); provided Expr is well-defined, this is always true |
| 1974 | | %print(simple_comp(SID,_Op,X,Y)), nl, |
| 1975 | | (debug_mode(off) -> true |
| 1976 | | ; format('Removing existential quantifier: ~w~n',[SID]), |
| 1977 | | translate:print_bexpr(b(Pred,pred,[])),nl). |
| 1978 | | cleanup_post(exists([TID1,TID2|OTHER],RHS),pred,IOld, |
| 1979 | | exists([TID1,TID2|OTHER],NewRHS),pred,[prob_symmetry(ID1,ID2)|IOld],single/symmetry_detection) :- |
| 1980 | | % DETECT Symmetries such as #(x,y).(x /= y & (x=TRUE or y=TRUE)) |
| 1981 | | % #(x2,y).(x2 /= y & x2:s & y:s & x2=aa or y=aa) |
| 1982 | | get_texpr_type(TID1,T), get_texpr_type(TID2,T), |
| 1983 | | preferences:get_preference(try_kodkod_on_load,false), |
| 1984 | | preferences:get_preference(use_static_symmetry_detection,true), |
| 1985 | | sym_break_supported_type(T), % LESS not yet fully functional with SET types; TO DO: fix |
| 1986 | | get_texpr_id(TID1,ID1), get_texpr_id(TID2,ID2), |
| 1987 | | nonmember(prob_symmetry(ID1,ID2),IOld), |
| 1988 | | \+(contains_equality(TID1,TID2,RHS)), % IDs are already equal; no use in sym breaking |
| 1989 | | debug_println(try_exists_symmetry(ID1,ID2)), |
| 1990 | | rename_bt(RHS,[rename(ID1,ID2),rename(ID2,ID1)],RHS2), |
| 1991 | | same_norm_texpr(RHS,RHS2), |
| 1992 | | %print(rhs_symmetric(ID1,ID2)),nl, |
| 1993 | | construct_sym_break(T,TID1,TID2,RHS,SYMBREAK), |
| 1994 | | conjunct_predicates([RHS,SYMBREAK],NewRHS), |
| 1995 | | (debug_mode(off) -> true |
| 1996 | | ; format('SYMMETRY BREAKING EXISTS: #(~w,~w).(',[ID1,ID2]),translate:print_bexpr(NewRHS),print(')'),nl). |
| 1997 | | |
| 1998 | | %% COMMENT IN NEXT LINE TO CHECK validity of AST per NODE (helps find bugs) |
| 1999 | | %%cleanup_post(Expr,pred,I,Expr,pred,I,single/checked) :- check_ast(true,b(Expr,pred,I)),fail. |
| 2000 | | %% |
| 2001 | | |
| 2002 | | |
| 2003 | | factor_disjunct(CEquality1,CEquality2,IOld,New,INew) :- |
| 2004 | | % (x=2 & y=3) or (x=2 & y=4) -> x=2 & (y=3 or y=4) to improve constraint propagation |
| 2005 | | Blacklist=[], |
| 2006 | | conjunction_to_list(CEquality1,Preds1), |
| 2007 | | conjunction_to_list(CEquality2,Preds2), |
| 2008 | | %print('TRY: '),nl, translate:nested_print_bexpr(b(disjunct(CEquality1,CEquality2),pred,IOld)),nl, |
| 2009 | ? | select_equality(TId1,Preds1,Blacklist,TEqual,Expr1,RestPreds1,_,check_well_definedness), % also allow other preds, use safe_select(check_well_definedness,TEqual,Preds,Rest), |
| 2010 | | get_texpr_id(TId1,Id), |
| 2011 | | get_texpr_id(TId2,Id), |
| 2012 | ? | select_equality(TId2,Preds2,Blacklist,_,Expr2,RestPreds2,_,check_well_definedness), |
| 2013 | | same_texpr(Expr1,Expr2), |
| 2014 | | conjunct_predicates(RestPreds1,P1), |
| 2015 | | conjunct_predicates(RestPreds2,P2), |
| 2016 | | % TO DO: do not recursively start from scratch in P1, one should start from the right of CEquality1: |
| 2017 | | (fail, % disable recursive looking |
| 2018 | | factor_disjunct(P1,P2,IOld,P12,INew) -> NewDisj = b(P12,pred,INew) |
| 2019 | | ; disjunct_predicates([P1,P2],NewDisj)), |
| 2020 | | conjunct_predicates([TEqual,NewDisj],NewPred), |
| 2021 | | NewPred=b(New,pred,I2), |
| 2022 | | include_important_info_from_removed_pred(IOld,I2,INew). |
| 2023 | | |
| 2024 | | % ------------------------------------------ |
| 2025 | | |
| 2026 | | gen_rename(TID1,TID2,rename(ID1,ID2)) :- def_get_texpr_id(TID1,ID1), def_get_texpr_id(TID2,ID2). |
| 2027 | | |
| 2028 | | is_not_member(not_member(LHS,RHS),LHS,RHS). |
| 2029 | | is_not_member(negation(b(member(LHS,RHS),pred,_)),LHS,RHS). |
| 2030 | | |
| 2031 | | |
| 2032 | | is_valid_id_member_check(b(member(MID,E),_,_),ID,E) :- same_id(ID,MID,SID), |
| 2033 | | % + check that MID does not occur in E |
| 2034 | | \+ occurs_in_expr(SID,E). |
| 2035 | | is_valid_id_member_check(b(truth,_,_),ID,TypeExpr) :- |
| 2036 | | get_texpr_type(ID,SType), |
| 2037 | | translate:set_type_to_maximal_texpr(SType,TypeExpr). % Note: this no longer introduces identifiers, which could clash |
| 2038 | | is_valid_id_member_check(b(conjunct(A,B),_,_),ID,Res) :- |
| 2039 | ? | is_valid_id_member_check(A,ID,EA), |
| 2040 | ? | is_valid_id_member_check(B,ID,EB), |
| 2041 | | get_texpr_type(EA,Type), |
| 2042 | | safe_create_texpr(intersection(EA,EB),Type,Res). |
| 2043 | | |
| 2044 | | contains_equality(TID1,TID2,RHS) :- |
| 2045 | ? | b_interpreter:member_conjunct(b(equal(A,B),pred,_),RHS,_), |
| 2046 | | (same_id(A,TID1,_),same_id(B,TID2,_) ; same_id(A,TID2,_),same_id(B,TID1,_)). |
| 2047 | | |
| 2048 | | simplify_let_subst(Ids,Pred,Subst,NIds,RestPred,NewSubst) :- |
| 2049 | | % remove let identifiers whose definitions are very simple, i.e. identifiers |
| 2050 | | Eq = b(equal(TypID,TExpr),pred,_), |
| 2051 | | can_be_optimized_away(TypID), |
| 2052 | | get_texpr_id(TypID,ToReplace), |
| 2053 | | b_interpreter:member_conjunct(Eq,Pred,RestPred), |
| 2054 | | is_simple_expression(TExpr), |
| 2055 | | nth0(_N,Ids,TI,NIds),get_texpr_id(TI,ToReplace), |
| 2056 | | !, |
| 2057 | | % Intitially there was an issue as we may also replace in the LHS of assignments |
| 2058 | | % see e.g. TestLet = LET cnt BE cnt=1 IN IF cnt=0 THEN ABORT ELSE cnt :: {0,1} END END; in SubstitutionLaws |
| 2059 | | % However, now the static type checker rejects those assignments |
| 2060 | | replace_id_by_expr(Subst,ToReplace,TExpr,NSubst), |
| 2061 | | % TO DO: it seems like cleanup rules are not applied on NSubst, e.g., function for set_extension rules |
| 2062 | | debug_println(9,replaced_let_subst_id(ToReplace)), |
| 2063 | | (Subst==NSubst -> NewSubst=NSubst ; clean_up(NSubst,[],NewSubst)). |
| 2064 | | |
| 2065 | | can_be_optimized_away(b(_,_,I)) :- nonmember(do_not_optimize_away,I). |
| 2066 | | |
| 2067 | | %replace_in_rhs(ID,E,RHS,CleanNewRHS) :- replace_id_by_expr(RHS,ID,E,NewRHS), clean_up(NewRHS,[],CleanNewRHS). |
| 2068 | | |
| 2069 | | can_be_replaced(RHS,_,Ids) :- get_texpr_id(RHS,RHSID),!, |
| 2070 | | \+ (member(TID2,Ids), get_texpr_id(TID2,RHSID)). % ID occurs in Ids, replacing it in Expr will move the scope |
| 2071 | | % example: Z Test (\LET x==1 @ (\LET x==x+1; y==x @ 7*x+y)) = 15 |
| 2072 | | can_be_replaced(_RHS,UsedIds,Ids) :- % TO DO: compute used ids |
| 2073 | | %find_identifier_uses(RHS,[],UsedIds), |
| 2074 | | get_texpr_ids(Ids,AtomicIds), sort(AtomicIds,SortedIds), |
| 2075 | | %print(check(UsedIds,SortedIds)),nl, |
| 2076 | | \+ ord_intersect(UsedIds,SortedIds). |
| 2077 | | |
| 2078 | | |
| 2079 | | simplify_let(Ids,Exprs,Expr,NIds,NExprs,CleanNewExpr) :- |
| 2080 | ? | nth0(N,Ids,TId,NIds), |
| 2081 | | get_texpr_id(TId,Id), |
| 2082 | | can_be_optimized_away(TId), |
| 2083 | | nth0(N,Exprs,LetExpr,NExprs), |
| 2084 | | find_identifier_uses(LetExpr,[],LetExprIds), |
| 2085 | | \+ ord_member(Id,LetExprIds), %\+ occurs_in_expr(Id,LetExpr), % illegal let, e.g., i = i+1; |
| 2086 | | can_be_replaced(LetExpr,LetExprIds,Ids), % moving LetExpr will not produce scoping issues |
| 2087 | | maplist(not_occurs_in_expr(Id),NExprs), % The ID is not used for defining other RHS in the same let |
| 2088 | | simplify_let_aux(TId,Id,LetExpr,Expr,CleanNewExpr). |
| 2089 | | |
| 2090 | | simplify_let_aux(_TId,Id,LetExpr,Expr,CleanNewExpr) :- |
| 2091 | | % remove let identifiers whose definitions are very simple, i.e. identifiers |
| 2092 | | is_simple_expression(LetExpr), |
| 2093 | | % TId = LetExpr |
| 2094 | | % TO DO: do not do this to outer variables which the user cares about !! |
| 2095 | | !, |
| 2096 | | debug_println(9,simple_expression_id(Id)), |
| 2097 | | %maplist(replace_in_rhs(Id,LetExpr),NExprs,NewExprs), |
| 2098 | | replace_id_by_expr(Expr,Id,LetExpr,NExpr), |
| 2099 | | clean_up(NExpr,[],CleanNewExpr). % clean up adjust eg used_ids info; necessary for test 568 in prob_safe_mode |
| 2100 | | simplify_let_aux(TId,Id,LetExpr,Expr,CleanNewExpr) :- |
| 2101 | | % push the let expression down the AST. E.g. "LET a=E IN (4*(a+z*a) + z)" would |
| 2102 | | % be transformed to "4*(LET a=E IN (a+z*a)) + z" |
| 2103 | | % If the final form is like "LET a=E IN a" it will be simplified to E. |
| 2104 | | \+ do_not_to_move_let_inside(Expr), |
| 2105 | | ( identifier_sub_ast(Expr,Id,SubPosition) -> |
| 2106 | | SubPosition = [_|_], % The LET can actually be moved down |
| 2107 | | %tools_printing:print_term_summary(identifier_sub_ast(Id,Expr,SubPosition)),nl, |
| 2108 | | exchange_ast_position(SubPosition,Expr,OldInner,NewInner,NExpr), |
| 2109 | | get_texpr_type(OldInner,Type), |
| 2110 | | ( get_texpr_id(OldInner,Id) -> % There is only one reference to Id, |
| 2111 | | debug_println(9,one_reference(Id)), |
| 2112 | | NewInner = LetExpr % replace it with the expression |
| 2113 | | % We need to check that we are not simply just exchanging lets with each other |
| 2114 | | ; cycle_detection(Id,SubPosition,Expr) -> debug_println(9,cycle(Id)),fail |
| 2115 | | ; Type=pred -> % print(created_let_predicate(N,Id,SubPosition,NIds)),nl, |
| 2116 | | extract_important_info_from_subexpressions(LetExpr,OldInner,NewLetInfo), % maybe no longer necessary because of cleanups call below |
| 2117 | | create_texpr(let_predicate([TId],[LetExpr],OldInner),pred,NewLetInfo,NewInner) |
| 2118 | | ; otherwise -> % print(create_let_expression(TId)),nl, |
| 2119 | | extract_important_info_from_subexpressions(LetExpr,OldInner,NewLetInfo), % maybe no longer necessary because of cleanups call below |
| 2120 | | create_texpr(let_expression([TId],[LetExpr],OldInner),Type,NewLetInfo,NewInner)), |
| 2121 | | clean_up(NExpr,[],CleanNewExpr) % maybe we only need WD post rules ? |
| 2122 | | ; always_well_defined(LetExpr) -> % Id does not occur in the expression -> just remove the LET |
| 2123 | | CleanNewExpr = Expr),!. |
| 2124 | | |
| 2125 | | do_not_to_move_let_inside(b(E,_,_)) :- |
| 2126 | | do_not_to_move_let_inside_aux(E). |
| 2127 | | do_not_to_move_let_inside_aux(forall(_,_,_)). % otherwise we may compute the let multiple times |
| 2128 | | % what about exists ?? |
| 2129 | | do_not_to_move_let_inside_aux(comprehension_set(_,_)). % ditto |
| 2130 | | do_not_to_move_let_inside_aux(lambda(_,_,_)). % ditto |
| 2131 | | do_not_to_move_let_inside_aux(general_sum(_,_,_)). % ditto |
| 2132 | | do_not_to_move_let_inside_aux(general_product(_,_,_)). % ditto |
| 2133 | | do_not_to_move_let_inside_aux(quantified_union(_,_,_)). % ditto |
| 2134 | | do_not_to_move_let_inside_aux(quantified_intersection(_,_,_)). % ditto |
| 2135 | | |
| 2136 | | not_occurs_in_expr(Id,Expr) :- \+ occurs_in_expr(Id,Expr). |
| 2137 | | |
| 2138 | | cycle_detection(Id,SubPosition,Expr) :- |
| 2139 | | get_constructors(SubPosition,Expr,Constructors), |
| 2140 | ? | (member(CC,Constructors), \+ let_constructor(CC) -> fail |
| 2141 | | ; debug_println(9,cycle_let_detection(Id,Constructors)) |
| 2142 | | %,print(cycle_let(Id,Constructors)),nl,translate:print_bexpr(Expr),nl |
| 2143 | | ). |
| 2144 | | % we have a let constructor which can be modified by simplify_let: |
| 2145 | | let_constructor(let_expression). |
| 2146 | | let_constructor(let_predicate). |
| 2147 | | let_constructor(let_substitution). |
| 2148 | | |
| 2149 | | % get a SubPosition path (as produced by identifier_sub_ast) and generate all constructors that are used along the Path |
| 2150 | | get_constructors([],_,[]). |
| 2151 | | get_constructors([Pos|T],OldTExpr,[ConstructorForPos|CT]) :- |
| 2152 | | remove_bt(OldTExpr,OldExpr,NewExpr,_NewTExpr), |
| 2153 | | functor(OldExpr,ConstructorForPos,_), |
| 2154 | | syntaxtransformation(OldExpr,Subs,_Names,_NSubs,NewExpr), |
| 2155 | | nth0(Pos,Subs, OldSelected,_Rest), |
| 2156 | | get_constructors(T,OldSelected,CT). |
| 2157 | | |
| 2158 | | is_simple_expression(TExpr) :- |
| 2159 | | get_texpr_expr(TExpr,Expr), |
| 2160 | | is_simple_expression2(Expr),!. |
| 2161 | | is_simple_expression(TExpr) :- |
| 2162 | | is_just_type(TExpr). |
| 2163 | | is_simple_expression2(identifier(_)). |
| 2164 | | is_simple_expression2(integer(_)). |
| 2165 | | is_simple_expression2(boolean_true). |
| 2166 | | is_simple_expression2(boolean_false). |
| 2167 | | |
| 2168 | | % detect either Event-B identity or id over full type |
| 2169 | | is_event_b_identity(b(X,_,_)) :- is_event_b_identity_aux(X). |
| 2170 | | is_event_b_identity_aux(event_b_identity). |
| 2171 | | is_event_b_identity_aux(identity(T)) :- is_just_type(T). |
| 2172 | | |
| 2173 | | :- use_module(library(avl),[avl_member/2]). |
| 2174 | | % check if we have a set extension and return list of terms |
| 2175 | | is_set_extension(b(S,T,I),L) :- is_set_extension_aux(S,T,I,L). |
| 2176 | | is_set_extension_aux(set_extension(L),_,_,L). |
| 2177 | | % TO DO: detect sequence_extension |
| 2178 | | is_set_extension_aux(value(avl_set(A)),SetType,I,L) :- % computed by eval_set_extension |
| 2179 | | is_set_type(SetType,Type), |
| 2180 | | findall(b(value(M),Type,I),avl_member(M,A),L). |
| 2181 | | |
| 2182 | | is_sequence_extension(b(S,T,I),L) :- is_sequence_extension_aux(S,T,I,L). |
| 2183 | | is_sequence_extension_aux(sequence_extension(L),_,_,L). |
| 2184 | | % TO DO: detect value/set_extensions |
| 2185 | | |
| 2186 | | recursion_detection_enabled(A,B,I) :- |
| 2187 | ? | recursion_detection_enabled_aux(A,B,I). |
| 2188 | | recursion_detection_enabled_aux(A,_B,I) :- |
| 2189 | | animation_mode(b), % in B mode, |
| 2190 | | memberchk(section(properties),I), % the rule should be only applied to properties |
| 2191 | | % and where A is an abstract constant. |
| 2192 | | get_texpr_info(A,AInfo),memberchk(loc(_,_,abstract_constants),AInfo). |
| 2193 | | recursion_detection_enabled_aux(A,_B,_I) :- |
| 2194 | | animation_minor_mode(eventb), % in Event-B, |
| 2195 | | %TODO: Limit application to axioms |
| 2196 | | get_texpr_info(A,AInfo), % A must be a constant |
| 2197 | | memberchk(loc(_,constants),AInfo). |
| 2198 | | recursion_detection_enabled_aux(_A,_B,_I) :- |
| 2199 | | animation_minor_mode(z). % use always in Z |
| 2200 | | |
| 2201 | | |
| 2202 | | construct_union_from_list([X],_,_,Res) :- !, Res=X. |
| 2203 | | construct_union_from_list([X,Y|T],Type,Info,Res) :- |
| 2204 | | construct_union_from_list([Y|T],Type,Info,RHS), |
| 2205 | | Res = b(union(X,RHS),Type,Info). |
| 2206 | | construct_inter_from_list([X],_,_,Res) :- !, Res=X. |
| 2207 | | construct_inter_from_list([X,Y|T],Type,Info,Res) :- |
| 2208 | | construct_inter_from_list([Y|T],Type,Info,RHS), |
| 2209 | | Res = b(intersection(X,RHS),Type,Info). |
| 2210 | | |
| 2211 | | % LEQ_SYM_BREAK does not support all types yet: |
| 2212 | | sym_break_supported_type(integer). |
| 2213 | | sym_break_supported_type(boolean). |
| 2214 | | sym_break_supported_type(string). |
| 2215 | | sym_break_supported_type(global(_)). |
| 2216 | | sym_break_supported_type(couple(A,B)) :- sym_break_supported_type(A), sym_break_supported_type(B). |
| 2217 | | sym_break_supported_type(record(F)) :- maplist(sym_break_supported_field,F). |
| 2218 | | sym_break_supported_field(field(_,T)) :- sym_break_supported_type(T). |
| 2219 | | % example with pairs: !(x,y).(x:s2 & y:s2 & x/=y => prj1(INTEGER,INTEGER)(x)/=prj1(INTEGER,INTEGER)(y)) (with let s2 = {x,y|x:1..10000 & y:{x+1}}); here we get a slow-down; maybe we should check if RHS complicated enough |
| 2220 | | % here it is beneficial: !(x,y).(x:dom(s)&y:dom(s)&x/=y => s(x)+s(y)>0) with let s={x,y,v|x:1..10&y:1..50&v=x+y}; runtime goes down from 9.7 to 6.1 seconds |
| 2221 | | |
| 2222 | ? | construct_sym_break(integer,TID1,TID2,Pred,Res) :- member_in_conjunction(Neq,Pred), is_id_inequality(Neq,TID1,TID2), |
| 2223 | | !, get_texpr_info(TID1,Info1), |
| 2224 | | Res = b(less(TID1,TID2),pred,Info1). % we don't need the external function; we can used < |
| 2225 | | construct_sym_break(integer,TID1,TID2,_Pred,Res) :- !, get_texpr_info(TID1,Info1), |
| 2226 | | Res = b(less_equal(TID1,TID2),pred,Info1). % we don't need the external function; we can used <= ; we could check whether < or <= already in Pred ? occurs in test 1360: #(vv,ww).(vv < ww & ww < vv) |
| 2227 | | construct_sym_break(_,TID1,TID2,_,Res) :- get_texpr_info(TID1,Info1), |
| 2228 | | Res = b(external_pred_call('LEQ_SYM_BREAK',[TID1,TID2]),pred,Info1). |
| 2229 | | |
| 2230 | | % construct {Expr1,Expr2} |
| 2231 | | construct_set_extension(Expr1,Expr2,Res) :- same_texpr(Expr1,Expr2),!, |
| 2232 | | get_texpr_type(Expr1,Type), |
| 2233 | | extract_info(Expr1,Infos), |
| 2234 | | Res = b(set_extension([Expr1]),set(Type),Infos). |
| 2235 | | construct_set_extension(Expr1,Expr2,Res) :- |
| 2236 | | get_texpr_type(Expr1,Type), |
| 2237 | | extract_info(Expr1,Expr2,Infos), |
| 2238 | | (Expr1 @=< Expr2 -> Lst=[Expr1,Expr2] ; Lst=[Expr2,Expr1]), % solves issue with ParserTests; {FALSE,TRUE} |
| 2239 | | Res = b(set_extension(Lst),set(Type),Infos). |
| 2240 | | |
| 2241 | | is_id_inequality(b(not_equal(A,B),pred,_),X,Y) :- |
| 2242 | | (same_texpr(A,X) -> same_texpr(B,Y) ; same_texpr(A,Y), same_texpr(B,X)). |
| 2243 | | |
| 2244 | | |
| 2245 | | is_membership(b(member(TID,Set),pred,Info),TID,Set,Info). |
| 2246 | | is_membership(b(subset(b(set_extension([TID]),_,_),Set),pred,Info),TID,Set,Info). |
| 2247 | | |
| 2248 | | known_set(b(integer_set(_),set(integer),_)). % used for forall splitting; TODO: use is_integer_set ?? |
| 2249 | | known_set(b(interval(_,_),set(integer),_)). |
| 2250 | | |
| 2251 | | % detect if we have an if-then-else function (which is then applied to a dummy argument) |
| 2252 | | is_if_then_else(b(comprehension_set([TDummyID1,ID2],CONJ),_Type,_),_DUMMYARG,IFPRED,THEN,ELSE) :- |
| 2253 | | % we ignore the _DUMMYARG as here we do not check the value of DUMMYARG in the body |
| 2254 | | % TO DO: also allow removal of equalities as in TLA case below |
| 2255 | | % DETECT {Dummy,Res| Test => Res=THEN & not(Test) => Res=ELSE} |
| 2256 | | get_texpr_id(ID2,LambdaID), get_texpr_id(TDummyID1,DummyID), |
| 2257 | | %print(try(LambdaID,DummyID)),nl, translate:print_bexpr(CONJ),nl, |
| 2258 | | is_ifte_case_conjunct(CONJ,IFPRED,EQ1,EQ2), |
| 2259 | | is_equality_conj(EQ1,II1,THEN), get_texpr_id(II1,LambdaID), |
| 2260 | | is_equality_conj(EQ2,II2,ELSE), get_texpr_id(II2,LambdaID), |
| 2261 | | \+ occurs_in_expr(DummyID,IFPRED),\+ occurs_in_expr(LambdaID,IFPRED), |
| 2262 | | \+ occurs_in_expr(DummyID,THEN), \+ occurs_in_expr(LambdaID,THEN), |
| 2263 | | \+ occurs_in_expr(DummyID,ELSE), \+ occurs_in_expr(LambdaID,ELSE). |
| 2264 | | |
| 2265 | | % Recognize B2TLA encodings as well: %((x).(x=0 & PRED|C1)\/%(x).(x=0 & not(PRED)|C2)) (0) |
| 2266 | | %is_if_then_else(IF,_,_,_,_) :- nl,print(IF),nl,nl,fail. |
| 2267 | | is_if_then_else(b(union(COMP1,COMP2),_Type,_),DUMMYARG,IFPRED,THEN,ELSE) :- |
| 2268 | | %print(union(COMP1,COMP2)),nl,tools_printing:trace_print(COMP1),nl, |
| 2269 | | if_then_else_lambda(COMP1,DUMMYARG,IFPRED,THEN), |
| 2270 | | if_then_else_lambda(COMP2,DUMMYARG,NOT_IFPRED,ELSE), |
| 2271 | | is_negation_of(IFPRED,NOT_IFPRED). |
| 2272 | | |
| 2273 | | if_then_else_lambda(b(comprehension_set([TDummyID,TLAMBDAID],CONJ),_,_),DUMMYARG,IFPRED,RESULT) :- |
| 2274 | | conjunction_to_nontyping_list(CONJ,CL), |
| 2275 | | get_texpr_id(TDummyID,DummyID), |
| 2276 | | get_texpr_id(TLAMBDAID,LambdaID), |
| 2277 | ? | (remove_equality(DummyID,DUMMYVAL,CL,ConjList) % look if there is an equality for the DummyID |
| 2278 | | -> same_texpr(DUMMYVAL,DUMMYARG), % TO DO: check that we apply the function with this value |
| 2279 | | \+ occurs_in_expr(LambdaID,DUMMYVAL), % ensure this is really the same value |
| 2280 | | \+ occurs_in_expr(DummyID,DUMMYVAL) |
| 2281 | | ; ConjList=CL), |
| 2282 | | remove_equality(LambdaID,RESULT,ConjList,RestList), |
| 2283 | | \+ occurs_in_expr(LambdaID,RESULT), |
| 2284 | | \+ occurs_in_expr(DummyID,RESULT), % otherwise this is not really a dummy identifier |
| 2285 | | conjunct_predicates(RestList,IFPRED), |
| 2286 | | \+ occurs_in_expr(DummyID,IFPRED). |
| 2287 | | |
| 2288 | | % DETECT (IFPRED => EQ1) & (not(IFPRED) => EQ2) |
| 2289 | | is_ifte_case_conjunct(CONJ,IFPRED,EQ1,EQ2) :- |
| 2290 | | is_a_conjunct(CONJ,IMP1,IMP2), |
| 2291 | | is_an_implication_conj(IMP1,IFPRED,EQ1), |
| 2292 | | is_an_implication_conj(IMP2,NOT_IFPRED,EQ2), |
| 2293 | | is_negation_of(IFPRED,NOT_IFPRED). |
| 2294 | | % TO DO: also deal with lazy_lets wrapped around |
| 2295 | | %is_ifte_case_conjunct(lazy_let_pred(ID,IFPRED,CONJ),IFPRED,EQ1,EQ2) :- |
| 2296 | | % is_a_conjunct(CONJ,IMP1,IMP2), |
| 2297 | | % is_an_implication(IMP1,IFPRED,EQ1), |
| 2298 | | % is_an_implication(IMP2,NOT_IFPRED,EQ2), |
| 2299 | | % is_negation_of(IFPRED,NOT_IFPRED). |
| 2300 | | |
| 2301 | | % just like is_an_implication but allow typing conjuncts (not yet removed in pre-phase) |
| 2302 | | is_an_implication_conj(Pred,LHS,RHS) :- is_an_implication(Pred,LHS,RHS),!. |
| 2303 | | is_an_implication_conj(b(conjunct(A,B),pred,_),LHS,RHS) :- |
| 2304 | | (is_typing_predicate(A) -> is_an_implication_conj(B,LHS,RHS) |
| 2305 | | ; is_typing_predicate(B) -> is_an_implication_conj(A,LHS,RHS)). |
| 2306 | | |
| 2307 | | % just like is_equality but allow typing conjuncts (not yet removed in pre-phase) |
| 2308 | | is_equality_conj(EQ,LHS,RHS) :- is_equality(EQ,LHS,RHS). |
| 2309 | | is_equality_conj(b(conjunct(A,B),pred,_),LHS,RHS) :- |
| 2310 | | (is_typing_predicate(A) -> is_equality_conj(B,LHS,RHS) |
| 2311 | | ; is_typing_predicate(B) -> is_equality_conj(A,LHS,RHS)). |
| 2312 | | |
| 2313 | | % remove a dummy equality from list |
| 2314 | | remove_equality(ID,RHS,ConjList,Rest) :- |
| 2315 | ? | DummyEQ = b(equal(DID,RHS),pred,_), % TO DO: also accept simple typing memberships ? |
| 2316 | ? | get_texpr_id(DID,ID), |
| 2317 | ? | select(DummyEQ,ConjList,Rest). %, print(eq(DID,RHS)),nl. |
| 2318 | | |
| 2319 | | get_texpr_boolean(b(X,_,_),X) :- is_boolan_expr(X). |
| 2320 | | is_boolan_expr(boolean_true). |
| 2321 | | is_boolan_expr(boolean_false). |
| 2322 | | |
| 2323 | | |
| 2324 | | is_typing_conjunct(b(member(_,B),_,_)) :- is_just_type(B). |
| 2325 | | is_typing_predicate(Typing) :- conjunction_to_list(Typing,LT), maplist(is_typing_conjunct,LT). |
| 2326 | | conjunction_to_nontyping_list(Pred,List) :- conjunction_to_list(Pred,TList), exclude(is_typing_conjunct,TList,List). |
| 2327 | | |
| 2328 | | % used e.g. for translating : ran({x1,...xn|P}) --> {xn| #(x1,...).(P)} |
| 2329 | | create_outer_exists_for_dom_range(Ids,CompPred,NewCompPred) :- |
| 2330 | | create_outer_exists_for_dom_range2(Ids,CompPred,NewCompPred1), |
| 2331 | | recompute_used_ids_info(NewCompPred1,NewCompPred). |
| 2332 | | create_outer_exists_for_dom_range2(Ids,b(exists(InnerIds,P),pred,Infos),New) :- |
| 2333 | ? | member(allow_to_lift_exists,Infos), |
| 2334 | | append(Ids,InnerIds,NewIds),!, |
| 2335 | | New = b(exists(NewIds,P),pred,Infos). |
| 2336 | | create_outer_exists_for_dom_range2(Ids,P,N) :- |
| 2337 | | % we could also use create_and_simplify_exists; it does a full partitioning of P |
| 2338 | | conjunction_to_list(P,PL), |
| 2339 | | create_exists_opt(Ids,PL,b(P2,T2,I2)), % create_exists_opt: detects also simple tautologies like #x.(x=E) |
| 2340 | | % + predicates that do not use one of the quantified identifiers are moved outside |
| 2341 | | N=b(P2,T2,[allow_to_lift_exists|I2]). %, check_ast(N). |
| 2342 | | |
| 2343 | | % if _lambda_result_ occurs in list; rename it so that we do not get issues with enumeration |
| 2344 | | rename_lambda_result_id(Ids,CompPred,NewIds,NewCompPred) :- |
| 2345 | ? | select(ID,Ids,Rest), |
| 2346 | | get_texpr_id(ID,'_lambda_result_'), |
| 2347 | | !, |
| 2348 | | get_unique_id_inside('__RANGE_LAMBDA__',CompPred,FRESHID), % if we don't rename then _lambda_result_ will not be enumerated ! TO DO: also check different from Ids if we want to remove __ prefix |
| 2349 | | rename_bt(CompPred,[rename('_lambda_result_',FRESHID)],NewCompPred), |
| 2350 | | get_texpr_type(ID,IDType), get_texpr_info(ID,IDInfo), |
| 2351 | | NewIds = [b(identifier(FRESHID),IDType,IDInfo)|Rest]. |
| 2352 | | rename_lambda_result_id(Ids,CompPred,Ids,CompPred). |
| 2353 | | |
| 2354 | | contains_predicate(convert_bool(Pred),boolean,Pred, |
| 2355 | | convert_bool(NewP),NewP). |
| 2356 | | contains_predicate(comprehension_set(CompIds,Pred),_,Pred, |
| 2357 | | comprehension_set(CompIds,NewP),NewP). |
| 2358 | | contains_predicate(general_sum(Ids,Pred,Expression),integer,Pred, |
| 2359 | | general_sum(Ids,NewP,Expression),NewP). |
| 2360 | | contains_predicate(general_product(Ids,Pred,Expression),integer,Pred, |
| 2361 | | general_product(Ids,NewP,Expression),NewP). |
| 2362 | | contains_predicate(if_then_else(Pred,Then,Else),_,Pred, |
| 2363 | | if_then_else(NewP,Then,Else),NewP). |
| 2364 | | contains_predicate(assertion_expression(Pred,ErrMsg,Expr),_,Pred, |
| 2365 | | assertion_expression(NewP,ErrMsg,Expr),NewP). |
| 2366 | | contains_predicate(precondition(Pred,Body),subst,Pred, |
| 2367 | | precondition(NewP,Body),NewP). |
| 2368 | | contains_predicate(assertion(Pred,Body),subst,Pred, |
| 2369 | | assertion(NewP,Body),NewP). |
| 2370 | | contains_predicate(becomes_such(Vars,Pred),subst,Pred, |
| 2371 | | becomes_such(Vars,NewP),NewP). |
| 2372 | | contains_predicate(any(Parameters,Pred,Body),subst,Pred, |
| 2373 | | any(Parameters,NewP,Body),NewP). |
| 2374 | | contains_predicate(lazy_let_expr(ID,SharedExpr,MainExpr),pred, SharedExpr, |
| 2375 | | lazy_let_expr(ID,NewSharedExpr,MainExpr), NewSharedExpr) :- |
| 2376 | | get_texpr_type(SharedExpr,pred). |
| 2377 | | contains_predicate(lazy_let_subst(ID,SharedExpr,MainExpr),pred, SharedExpr, |
| 2378 | | lazy_let_subst(ID,NewSharedExpr,MainExpr), NewSharedExpr) :- |
| 2379 | | get_texpr_type(SharedExpr,pred). |
| 2380 | | contains_predicate(lazy_let_pred(ID,SharedExpr,MainExpr),pred, MainExpr, |
| 2381 | | lazy_let_pred(ID,SharedExpr,NewMainExpr), NewMainExpr) :- |
| 2382 | | \+ get_texpr_type(SharedExpr,pred). |
| 2383 | | % while(COND,STMT,INV,VARIANT), select, if --> can have multiple predicates !! |
| 2384 | | contains_predicates(while(Cond, Stmt,Invariant,Variant),subst, [Cond,Invariant], |
| 2385 | | while(NewCond,Stmt,NewInv, Variant), [NewCond,NewInv]). |
| 2386 | | contains_predicates(if(Whens),subst,Preds, |
| 2387 | | if(NewWhens),NewPreds) :- |
| 2388 | | get_predicates_from_list_of_cases(Whens,Preds,NewWhens,NewPreds). |
| 2389 | | contains_predicates(select(Whens),subst,Preds, |
| 2390 | | select(NewWhens),NewPreds) :- |
| 2391 | | get_predicates_from_list_of_cases(Whens,Preds,NewWhens,NewPreds). |
| 2392 | | contains_predicates(select(Whens,Else),subst,Preds, |
| 2393 | | select(NewWhens,Else),NewPreds) :- |
| 2394 | | get_predicates_from_list_of_cases(Whens,Preds,NewWhens,NewPreds). |
| 2395 | | contains_predicates(lazy_let_pred(ID,SharedExpr,MainExpr),pred, [SharedExpr,MainExpr], |
| 2396 | | lazy_let_pred(ID,NSharedExpr,NMainExpr), [NSharedExpr,NMainExpr]) :- |
| 2397 | | get_texpr_type(SharedExpr,pred). |
| 2398 | | |
| 2399 | | get_predicates_from_list_of_cases([],[],[],[]). |
| 2400 | | get_predicates_from_list_of_cases([H|T],Preds,[NewH|NewT],NewPreds) :- |
| 2401 | | (get_single_predicate(H,Pred,NH,NewPred) |
| 2402 | | -> NewH=NH, Preds=[Pred|TP], NewPreds = [NewPred|NTP] |
| 2403 | | ; NewH=H, Preds=TP, NewPreds = NTP |
| 2404 | | ), |
| 2405 | | get_predicates_from_list_of_cases(T,TP,NewT,NTP). |
| 2406 | | |
| 2407 | | get_single_predicate(b(E,T,I),Preds,b(NewE,T,I),NewPreds) :- |
| 2408 | | get_single_predicate_aux(E,Preds,NewE,NewPreds). |
| 2409 | | get_single_predicate_aux(select_when(Pred,Body),Pred,select_when(NewPred,Body),NewPred). |
| 2410 | | get_single_predicate_aux(if_elsif(Pred,Body),Pred,if_elsif(NewPred,Body),NewPred). |
| 2411 | | |
| 2412 | | |
| 2413 | | % Detect useless statements in sequential compositions: |
| 2414 | | % useful for LCHIP code, e.g., where dummy code is added for the code generator: i9 : (i9 : BOOL); i9 := TRUE |
| 2415 | | % in test 1660 we remove an assignment that reads an unitialised variable |
| 2416 | | filter_useless_subst_in_sequence([],_,R) :- !, R=[]. |
| 2417 | | filter_useless_subst_in_sequence([S1],_,R) :- !, R=[S1]. |
| 2418 | | filter_useless_subst_in_sequence([S1|S2],change,R) :- useless_subst_in_sequence(S1,S2),!, |
| 2419 | | (debug_mode(off) -> true ; format('Removing useless substitution: ',[]), translate:print_subst(S1),nl), |
| 2420 | | filter_useless_subst_in_sequence(S2,_,R). |
| 2421 | | filter_useless_subst_in_sequence([S1|S2],Change,[S1|RS]) :- filter_useless_subst_in_sequence(S2,Change,RS). |
| 2422 | | |
| 2423 | | useless_subst_in_sequence(b(Subst,subst,Info),Sequence2) :- % print(check(Subst,Sequence2)),nl, |
| 2424 | | useless_code_before_sequence(Subst,Info,Sequence2). |
| 2425 | | |
| 2426 | | useless_code_before_sequence(skip,_,_) :- !. |
| 2427 | | useless_code_before_sequence(Subst,_,SubstList) :- is_non_failing_assignment(Subst,TID), def_get_texpr_id(TID,ID), |
| 2428 | | %print(check(ID,SubstList)), |
| 2429 | | is_dead(ID,SubstList). |
| 2430 | | |
| 2431 | | % first naive version to compute if the variable ID is dead when followed by a list of substitutions |
| 2432 | | is_dead(ID,[b(Subst,subst,Info)|_]) :- % we currently only look at first statement; TO DO: improve |
| 2433 | | is_dead_aux(Subst,Info,ID). |
| 2434 | | is_dead_aux(assign_single_id(TID,RHS),_Info,ID) :- |
| 2435 | | get_texpr_id(TID,ID), % we assign to ID; TO DO: deal with other assignments and assignments to functions f(i) := ... |
| 2436 | | find_identifier_uses(RHS,[],UsedIds), |
| 2437 | | %print(rhs(UsedIds)),nl, |
| 2438 | | \+ ord_member(ID,UsedIds). |
| 2439 | | |
| 2440 | | % non failing assignment without WD condition, note that we may still try and read identifiers that have not been initialised (having term(undefined) as value), see test 1660 |
| 2441 | | is_non_failing_assignment(becomes_such([TID],Pred),TID) :- is_truth(Pred). |
| 2442 | | is_non_failing_assignment(becomes_element_of([TID],Set),TID) :- definitely_not_empty_set(Set). |
| 2443 | | is_non_failing_assignment(assign_single_id(TID,RHS),TID) :- always_well_defined_or_disprover_mode(RHS). |
| 2444 | | is_non_failing_assignment(assign([LHS],[RHS]),TID) :- always_well_defined_or_disprover_mode(RHS), |
| 2445 | | get_lhs_assigned_identifier(LHS,TID). |
| 2446 | | |
| 2447 | | |
| 2448 | | % --------------------------------------------- |
| 2449 | | |
| 2450 | | :- use_module(b_expression_sharing,[cse_optimize_predicate/2]). |
| 2451 | | % these are "global" optimizations at the predicate level |
| 2452 | | % they are only called once a predicate has been completely constructed |
| 2453 | | predicate_level_optimizations(Pred,NewPred) :- |
| 2454 | | predicate_level_optimizations(Pred,NewPred,[]). |
| 2455 | | predicate_level_optimizations(Pred,NewPred,Path) :- |
| 2456 | | inner_predicate_level_optimizations(Pred,Pred1), |
| 2457 | | (get_preference(use_common_subexpression_elimination,true), |
| 2458 | | \+ do_not_optimise_in_context(Path) |
| 2459 | | -> cse_optimize_predicate(Pred1,NewPred) |
| 2460 | | ; NewPred=Pred1 |
| 2461 | | ). %,print_opt_debug_info(Pred,NewPred,Path). |
| 2462 | | /* |
| 2463 | | print_opt_debug_info(Pred,NewPred,Path) :- |
| 2464 | | (Pred==NewPred -> true |
| 2465 | | ; same_texpr(Pred,NewPred) -> true |
| 2466 | | ; format('Optimized pred ~w: ',[Path]), translate:print_bexpr(NewPred),nl |
| 2467 | | % , (Path=[] -> trace ; true) |
| 2468 | | ). |
| 2469 | | */ |
| 2470 | | |
| 2471 | | do_not_optimise_in_context([arg(top_level(invariant),Nr)]) :- |
| 2472 | | get_preference(use_po,true), |
| 2473 | | debug_format(19,'% NOT applying CSE to Invariant Nr ~w (PROOF_INFO = TRUE)~n',[Nr]). |
| 2474 | | |
| 2475 | | :- use_module(partition_detection,[detect_all_partitions_in_predicate/2]). |
| 2476 | | % this predicate is also called for exists, forall, ...: |
| 2477 | | inner_predicate_level_optimizations(Pred,NewPred) :- |
| 2478 | | detect_all_partitions_in_predicate(Pred,NewPred1), |
| 2479 | | (get_preference(remove_implied_constraints,true) |
| 2480 | | -> remove_implied_constraints(NewPred1,NewPred) |
| 2481 | | ; NewPred=NewPred1) |
| 2482 | | . %,(Pred==NewPred -> true ; print('Optimized pred: '), translate:print_bexpr(NewPred),nl). |
| 2483 | | |
| 2484 | | |
| 2485 | | |
| 2486 | | % ---------------------------------- |
| 2487 | | |
| 2488 | | remove_implied_constraints(Predicate,NewPredicate) :- |
| 2489 | | conjunction_to_list(Predicate,PList), |
| 2490 | | remove_implied_constraints(PList,[],PNew), |
| 2491 | | conjunct_predicates(PNew,NewPredicate). |
| 2492 | | |
| 2493 | | % remove constraints which are redundant for ProB |
| 2494 | | % example: |
| 2495 | | % n=1000 & f:1..n --> BOOL & f:1..n +-> BOOL & !x.(x:dom(f) => f(x) = bool(x>50)) & f: 1..n <-> BOOL & dom(f)=1..n |
| 2496 | | % runtime goes from 500 ms down to 300 ms by remove +->, <-> and dom(f) checks |
| 2497 | | % but test 1442 has issue: still unclear how useful this static detection is |
| 2498 | | % it is probably most useful for proving/disproving where we have lots of redundant/derived hypotheses |
| 2499 | | |
| 2500 | | remove_implied_constraints([],_,[]). |
| 2501 | | remove_implied_constraints([Constraint|T],SoFar,Result) :- |
| 2502 | | % print('Checking: '), translate:print_bexpr(Constraint),nl, |
| 2503 | | possible_implied_constraint(Constraint,C1), |
| 2504 | | % print('Checking if implied constraint: '), translate:print_bexpr(Constraint),nl, |
| 2505 | | (member(TC2,T) ; member(TC2,SoFar)), |
| 2506 | | get_texpr_expr(TC2,C2), |
| 2507 | | implied_constraint2(C2,C1), |
| 2508 | | print('Removing implied constraint: '), translate:print_bexpr(Constraint), print(' <=== '), translate:print_bexpr(TC2),nl, |
| 2509 | | !, |
| 2510 | | remove_implied_constraints(T,SoFar,Result). |
| 2511 | | remove_implied_constraints([H|T],SoFar,[H|RT]) :- remove_implied_constraints(T,[H|SoFar],RT). |
| 2512 | | |
| 2513 | | possible_implied_constraint(b(E,T,I),E) :- |
| 2514 | | (possible_implied_constraint2(E,T,I) -> true). |
| 2515 | | possible_implied_constraint2(member(_,b(FUNCTION,_,_)),_,_) :- functor(FUNCTION,F,2), |
| 2516 | | (function_implication2(F,_) -> true ; F = relations). |
| 2517 | | possible_implied_constraint2(equal(b(domain(_),_,_),_),_,_). % TO DO: other way around |
| 2518 | | |
| 2519 | | % f: A --> B ==> f: A +-> B, f: A<->B, dom(f) = A |
| 2520 | | % test 1442: issue with surjection |
| 2521 | | implied_constraint2(member(Fun1,b(FUNCTION1,T,_)), member(Fun2,b(FUNCTION2,T,_))) :- |
| 2522 | | functor(FUNCTION1,F1,2), arg(1,FUNCTION1,X1), arg(2,FUNCTION1,Y1), |
| 2523 | | functor(FUNCTION2,F2,2), arg(1,FUNCTION2,X2), arg(2,FUNCTION2,Y2), |
| 2524 | | function_implication(F1,F2), |
| 2525 | | same_texpr(Fun1,Fun2), |
| 2526 | | same_texpr(X1,X2), |
| 2527 | | same_texpr(Y1,Y2). |
| 2528 | | % f: A --> B ==> dom(f) = A |
| 2529 | | implied_constraint2(member(Fun2,b(FUNCTION2,_,_)), equal(b(domain(Fun1),_,_),Domain)) :- |
| 2530 | | functor(FUNCTION2,F2,2), arg(1,FUNCTION2,Domain2), |
| 2531 | | total_function(F2), |
| 2532 | | same_texpr(Fun1,Fun2), |
| 2533 | | same_texpr(Domain,Domain2). |
| 2534 | | % TODO: f: A -->> B ==> ran(f) = B ? |
| 2535 | | |
| 2536 | | |
| 2537 | | total_function(total_bijection). |
| 2538 | | total_function(total_injection). |
| 2539 | | total_function(total_surjection). |
| 2540 | | total_function(total_function). |
| 2541 | | %total_relation(total_surjection_relation). % not sure if in this case the constraint is maybe not useful after all? |
| 2542 | | %total_relation(total_relation). |
| 2543 | | |
| 2544 | | function_implication(F1,F2) :- function_implication2(F1,F2). |
| 2545 | | function_implication(F1,F2) :- function_implication2(F1,Z), function_implication(Z,F2). |
| 2546 | | |
| 2547 | | function_implication2(total_bijection,total_injection). |
| 2548 | | function_implication2(total_bijection,total_surjection). |
| 2549 | | function_implication2(total_injection,total_function). |
| 2550 | | function_implication2(total_surjection,total_function). |
| 2551 | | function_implication2(total_function,partial_function). |
| 2552 | | function_implication2(partial_function,relations). |
| 2553 | | function_implication2(partial_injection,partial_function). % >+> |
| 2554 | | function_implication2(partial_surjection,partial_function). |
| 2555 | | %function_implication2(partial_bijection,partial_injection). |
| 2556 | | %function_implication2(partial_bijection,partial_surjection). |
| 2557 | | function_implication2(total_relation,relations). |
| 2558 | | function_implication2(surjection_relation,relations). |
| 2559 | | function_implication2(total_surjection_relation,total_relation). |
| 2560 | | function_implication2(total_surjection_relation,surjection_relation). |
| 2561 | | |
| 2562 | | % ------------------ |
| 2563 | | |
| 2564 | | |
| 2565 | | % divide a list of identifiers into domain and range identifiers |
| 2566 | | get_domain_range_ids([D,R],[D],[R]) :- !. |
| 2567 | | get_domain_range_ids([D1,D2|T],[D1|DT],R) :- get_domain_range_ids([D2|T],DT,R). |
| 2568 | | |
| 2569 | | |
| 2570 | | % detect whether there is a pattern of a recursive usage of the identifier: ID(x) or ID[x] or x:ID |
| 2571 | | find_recursive_usage(TExpr,ID) :- |
| 2572 | ? | syntaxtraversion(TExpr,Expr,_,_,Subs,TNames), % print(try_id(ID,Expr,Subs,TNames)),nl, |
| 2573 | ? | ((Expr = function(Fun,_), get_texpr_id(Fun,ID)) -> true |
| 2574 | ? | ; (Expr = image(Rel,_), get_texpr_id(Rel,ID)) -> true |
| 2575 | ? | ; (Expr = member(_,Set), get_texpr_id(Set,ID)) -> true |
| 2576 | ? | ; \+ (member(ID1,TNames),get_texpr_id(ID1,ID)), % new local variable with same name |
| 2577 | ? | member(Sub,Subs), find_recursive_usage(Sub,ID) |
| 2578 | | ). |
| 2579 | | |
| 2580 | | :- use_module(bsyntaxtree,[transform_bexpr/3]). |
| 2581 | | % find comprehension sets and mark them as recursive if they use the recursive ID |
| 2582 | | mark_recursion(TExpr,RecID,NewTExpr) :- |
| 2583 | | (transform_bexpr(b_ast_cleanup:mark_comprehension_set(RecID),TExpr,NewTExpr) |
| 2584 | | -> true |
| 2585 | | ; add_internal_error('Call failed: ',transform_bexpr(b_ast_cleanup:mark_comprehension_set(RecID),TExpr,NewTExpr)), |
| 2586 | | NewTExpr=TExpr). |
| 2587 | | |
| 2588 | | :- public mark_comprehension_set/3. |
| 2589 | | mark_comprehension_set(RecID,b(lambda(Ids,P,Expr),Type,Info), |
| 2590 | | b(lambda(Ids,P,Expr),Type,NInfo)) :- |
| 2591 | | (find_recursive_usage(P,RecID) -> true ; find_recursive_usage(Expr,RecID)), |
| 2592 | | get_texpr_ids(Ids,AtomicIds), |
| 2593 | | (silent_mode(on) -> true |
| 2594 | | ; format('Recursive lambda using ~w detected (name: ~w)~n',[AtomicIds,RecID]), |
| 2595 | | error_manager:print_message_span(Info),nl |
| 2596 | | ), |
| 2597 | | add_texpr_infos(Info,[prob_annotation('SYMBOLIC'),prob_annotation('RECURSIVE')],NInfo). |
| 2598 | | mark_comprehension_set(RecID,b(comprehension_set(Ids,P),Type,Info), |
| 2599 | | b(comprehension_set(Ids,P),Type,NInfo)) :- |
| 2600 | | % DO NOT MARK IT IF IT IS IN RESULT POSITION of recursive function ? |
| 2601 | ? | find_recursive_usage(P,RecID), |
| 2602 | | get_texpr_ids(Ids,AtomicIds), |
| 2603 | | (silent_mode(on) -> true |
| 2604 | | ; format('Recursive comprehension set using ~w detected (name: ~w)~n',[AtomicIds,RecID]), |
| 2605 | | error_manager:print_message_span(Info),nl |
| 2606 | | ), |
| 2607 | | NInfo = [prob_annotation('SYMBOLIC'),prob_annotation('RECURSIVE')|Info]. % TO DO: only add if not already there |
| 2608 | | |
| 2609 | | singleton_set_extension(b(SONE,_,_),El) :- singleton_set_extension_aux(SONE,El). |
| 2610 | | singleton_set_extension_aux(set_extension([El]),El). |
| 2611 | | % singleton_set_extension_aux(value(Set),b(value(El),Type,[])) :- custom_explicit_sets:singleton_set(Set,El). % TO DO: transmit type to be able to construct value |
| 2612 | | %singleton_set_extension_aux(sequence_extension([El]),1 |-> El). % TO DO: |
| 2613 | | |
| 2614 | | % |
| 2615 | | one(b(integer(1),integer,[])). |
| 2616 | | create_interval_member(X,LowBound,UpBound,Member) :- |
| 2617 | | safe_create_texpr(interval(LowBound,UpBound),set(integer),Interval), |
| 2618 | | safe_create_texpr(member(X,Interval),pred,Member). |
| 2619 | | |
| 2620 | | get_leq_comparison(less(A,B),A,B1) :- minus_one(B,BM1), |
| 2621 | | safe_create_texpr(BM1,integer,B1). |
| 2622 | | get_leq_comparison(greater(B,A),A,B1) :- get_leq_comparison(less(A,B),A,B1). |
| 2623 | | get_leq_comparison(less_equal(A,B),A,B). |
| 2624 | | get_leq_comparison(greater_equal(B,A),A,B). |
| 2625 | | |
| 2626 | | minus_one(b(integer(I),integer,_),Res) :- !, I1 is I-1, Res=integer(I1). |
| 2627 | | minus_one(B,minus(B,One)) :- one(One). |
| 2628 | | add_one(b(integer(I),integer,_),Res) :- !, I1 is I+1, Res=integer(I1). |
| 2629 | | add_one(B,add(B,One)) :- one(One). |
| 2630 | | |
| 2631 | | % get_geq_comparison(Expr,LHS,RHS) ; RHS can be shifted by 1 |
| 2632 | | get_geq_comparison(less(B,A),A,B1) :- get_geq_comparison(greater(A,B),A,B1). |
| 2633 | | get_geq_comparison(greater(A,B),A,B1) :- add_one(B,BP1), |
| 2634 | | safe_create_texpr(BP1,integer,B1). |
| 2635 | | get_geq_comparison(less_equal(B,A),A,B). |
| 2636 | | get_geq_comparison(greater_equal(A,B),A,B). |
| 2637 | | get_geq_comparison(member(A,SET),A,b(integer(Bound),integer,[])) :- |
| 2638 | | is_inf_integer_set_with_lower_bound(SET,Bound). |
| 2639 | | % comparison operators: |
| 2640 | | comparison(equal(A,B),A,B,equal(SA,SB),SA,SB). |
| 2641 | | comparison(not_equal(A,B),A,B,not_equal(SA,SB),SA,SB). |
| 2642 | | comparison(greater(A,B),A,B,greater(SA,SB),SA,SB). |
| 2643 | | comparison(less(A,B),A,B,less(SA,SB),SA,SB). |
| 2644 | | comparison(greater_equal(A,B),A,B,greater_equal(SA,SB),SA,SB). |
| 2645 | | comparison(less_equal(A,B),A,B,less_equal(SA,SB),SA,SB). |
| 2646 | | % rules to simplify binary comparison arguments |
| 2647 | | simplify_comparison_terms(b(A,T,_IA),b(B,T,_IB),RA,RB) :- |
| 2648 | | simplify_comparison_terms2(A,B,RA,RB). |
| 2649 | | % TO DO: expand into much better simplifier ! |
| 2650 | | simplify_comparison_terms2(minus(A1,A2),minus(B1,B2),ResA,ResB) :- |
| 2651 | | ( same_texpr(A1,B1) -> ResA=B2, ResB=A2 % X-A2 < X-B2 <=> B2 < A2 |
| 2652 | | ; same_texpr(A2,B2) -> ResA=A1, ResB=B1). % A1-X < B1-X <=> A1 < B1 |
| 2653 | | simplify_comparison_terms2(add(A1,A2),add(B1,B2),ResA,ResB) :- |
| 2654 | | ( same_texpr(A1,B1) -> ResA=A2, ResB=B2 % X+A2 < X+B2 <=> A2 < B2 |
| 2655 | | ; same_texpr(A2,B2) -> ResA=A1, ResB=B1 % A1+X < B1+X <=> A1 < B1 |
| 2656 | | ; same_texpr(A1,B2) -> ResA=A2, ResB=B1 % X+A2 < B1+X <=> A2 < B1 |
| 2657 | | ; same_texpr(A2,B1) -> ResA=A1, ResB=B2). % A1+X < X+B2 <=> A1 < B2 |
| 2658 | | % multiplication: beware of sign, same with division |
| 2659 | | |
| 2660 | | /* not used at the moment: |
| 2661 | | clpfd_arith_integer_expression(b(E,integer,_)) :- clpfd_arith_integer_expression_aux(E). |
| 2662 | | % check if we have an expression that can be dealt with by b_compute_arith_expression |
| 2663 | | clpfd_arith_integer_expression_aux(unary_minus(X)) :- |
| 2664 | | X \= b(integer(_),integer,_). % if it is an explicit integer we can compute it normally |
| 2665 | | clpfd_arith_integer_expression_aux(add(_,_)). |
| 2666 | | clpfd_arith_integer_expression_aux(minus(_,_)). |
| 2667 | | clpfd_arith_integer_expression_aux(multiplication(_,_)). |
| 2668 | | */ |
| 2669 | | |
| 2670 | | % simplify equality/inequality Unifications: |
| 2671 | | simplify_equality(b(A,T,_),b(B,T,_),A2,B2) :- |
| 2672 | | simplify_equality_aux(A,B,A2,B2). |
| 2673 | | simplify_equality_aux(set_extension([A1]),set_extension([B1]),A2,B2) :- |
| 2674 | | (simplify_equality(A1,B1,A2,B2) -> true ; A2=A1, B2=B1). |
| 2675 | | |
| 2676 | | |
| 2677 | | % record field set extraction: |
| 2678 | | construct_field_sets(FieldsSetsOut, field(Name,Type), field(Name,NewSet)) :- |
| 2679 | | (member(field_set(Name,NewSet),FieldsSetsOut) |
| 2680 | | -> true |
| 2681 | | ; translate:set_type_to_maximal_texpr(Type,NewSet) |
| 2682 | | ). |
| 2683 | | |
| 2684 | | % traverse a list of conjuncts and check that they all restrict fields of a record ID |
| 2685 | | % all sets are combined via intersection |
| 2686 | | l_update_record_field_membership([],_) --> []. |
| 2687 | | l_update_record_field_membership([H|T],ID) --> |
| 2688 | | update_record_field_membership(H,ID), l_update_record_field_membership(T,ID). |
| 2689 | | update_record_field_membership(b(member(b(LHS,_,_),TRHS),pred,_),ID) --> update2(LHS,TRHS,ID). |
| 2690 | | update2(record_field(RECID,FieldName),TRHS,ID) --> {get_texpr_id(RECID,ID)},add_field_restriction(FieldName,TRHS). |
| 2691 | | update2(identifier(ID),b(struct(b(rec(FieldSets),_,_)),_,_),ID) --> |
| 2692 | | l_add_field_restriction(FieldSets). |
| 2693 | | |
| 2694 | | l_add_field_restriction([]) --> []. |
| 2695 | | l_add_field_restriction([field(FieldName,TRHS)|T]) --> |
| 2696 | | add_field_restriction(FieldName,TRHS), l_add_field_restriction(T). |
| 2697 | | add_field_restriction(FieldName,TRHS,FieldsIn,FieldsOut) :- %print(add(FieldName,TRHS,FieldsIn)),nl, |
| 2698 | | (select(field_set(FieldName,OldSet),FieldsIn,F2) |
| 2699 | | -> OldSet = b(_,Type,_), |
| 2700 | | safe_create_texpr(intersection(OldSet,TRHS),Type,NewSet), |
| 2701 | | %print(combine(FieldName)),nl,translate:print_bexpr(NewSet),nl, |
| 2702 | | FieldsOut = [field_set(FieldName,NewSet)|F2] |
| 2703 | | ; FieldsOut = [field_set(FieldName,TRHS)|FieldsIn]). |
| 2704 | | % end record field extraction |
| 2705 | | |
| 2706 | | |
| 2707 | | extract_unions(A,R) :- get_texpr_expr(A,union(A1,A2)),!, |
| 2708 | | extract_unions(A1,R1), extract_unions(A2,R2), |
| 2709 | | append(R1,R2,R). |
| 2710 | | extract_unions(A,[A]). |
| 2711 | | |
| 2712 | | gen_member_predicates(B,SEl,TExpr) :- safe_create_texpr(member(SEl,B),pred,TExpr). |
| 2713 | | |
| 2714 | | % when constructing an expression/predicate: important to ripple wd information up |
| 2715 | | extract_important_info_from_subexpression(b(_,_,Info),NewInfo) :- |
| 2716 | | include(important_info,Info,NewInfo). |
| 2717 | | |
| 2718 | | extract_important_info_from_subexpressions(b(_,_,Info1),b(_,_,Info2),NewInfo) :- |
| 2719 | | include(important_info,Info1,II1), |
| 2720 | | (memberchk(contains_wd_condition,Info2), nonmember(contains_wd_condition,II1) |
| 2721 | | -> NewInfo = [contains_wd_condition|II1] |
| 2722 | | ; NewInfo=II1). % TO DO: maybe also import other Infos? merge position info (nodeid(_))? |
| 2723 | | % other important ones: removed_typing ?? |
| 2724 | | |
| 2725 | | % include important info from removed conjunct (note: see also extract_info in bsyntaxtree) |
| 2726 | | % include_important_info(RemovedPredInfo,RemainingPredInfo,NewInfo) |
| 2727 | | include_important_info_from_removed_pred([],Info2,Info2). |
| 2728 | | include_important_info_from_removed_pred([H1|Info1],Info2,NewInfo2) :- |
| 2729 | | (include_del_info(H1,H), nonmember(H,Info2) |
| 2730 | | -> NewInfo2 = [H|NI2], include_important_info_from_removed_pred(Info1,Info2,NI2) |
| 2731 | | ; include_important_info_from_removed_pred(Info1,Info2,NewInfo2)). |
| 2732 | | |
| 2733 | | include_del_info(was(_),removed_typing). |
| 2734 | | include_del_info(removed_typing,removed_typing). |
| 2735 | | |
| 2736 | | important_info(removed_typing). |
| 2737 | | important_info(contains_wd_condition). |
| 2738 | | important_info(prob_annotation(_)). |
| 2739 | | important_info(nodeid(_)). |
| 2740 | | important_info(was(_)). |
| 2741 | | important_info(allow_to_lift_exists). % important but only for exists |
| 2742 | | |
| 2743 | | % add important infos in case an expression gets simplified into a sub-expression, e.g., bool(X)=TRUE -> X |
| 2744 | | add_important_info_from_super_expression(Infos,SubInfos,NewSubInfos) :- |
| 2745 | | include(important_info_from_super_expression,Infos,Important), % print(add_important(Important)),nl, |
| 2746 | | append(Important,SubInfos,NewSubInfos). % TO DO: add allow_to_lift_exists only if new |
| 2747 | | |
| 2748 | | important_info_from_super_expression(label(_)). |
| 2749 | | %add_important_info_to_texpr_from_super(Infos,b(Sub,T,SubInfos),b(Sub,T,NewSubInfos)) :- !, |
| 2750 | | % add_important_info_from_super_expression(Infos,SubInfos,NewSubInfos). |
| 2751 | | |
| 2752 | | |
| 2753 | | % extract all assignments from a list of statements; last arg is the number of assignments extracted |
| 2754 | | extract_assignments([],[],[],[],0). |
| 2755 | | extract_assignments([H|T],ResLHS,ResRHS,Rest,Nr) :- |
| 2756 | | is_ordinary_assignment(H,LHS,RHS,Cnt),!, |
| 2757 | | extract_assignments(T,LT,RT,Rest,N), |
| 2758 | | append(LHS,LT,ResLHS), append(RHS,RT,ResRHS), Nr is N+Cnt. |
| 2759 | | extract_assignments([H|T],LT,RT,[H|Rest],Nr) :- |
| 2760 | | extract_assignments(T,LT,RT,Rest,Nr). |
| 2761 | | % assigned_after(Primed),modifies(Var) |
| 2762 | | |
| 2763 | | % check if we have an ordinary assignment that can be merged, optimised: |
| 2764 | | is_ordinary_assignment(b(S,_,Info),LHS,RHS,Cnt) :- is_ordinary_assignment_aux(S,Info,LHS,RHS,Cnt). |
| 2765 | | is_ordinary_assignment_aux(skip,_Info,[],[],0). |
| 2766 | | is_ordinary_assignment_aux(assign_single_id(LHS,RHS),_Info,[LHS],[RHS],0). % count=0: used for parallel merge: assign_single_id less useful to merge with |
| 2767 | | is_ordinary_assignment_aux(assign(LHS,RHS),Info,LHS,RHS,1) :- |
| 2768 | | \+ member(assigned_after(_),Info), % these assignments are treated in a special way |
| 2769 | | \+ member(modifies(_),Info). |
| 2770 | | |
| 2771 | | % merge assignments in a list of statements to be executed by sequential composition: |
| 2772 | | merge_assignments([S1,S2|T],merged,Res) :- merge_two_assignments(S1,S2,New),!, |
| 2773 | | merge_assignments([New|T],_,Res). |
| 2774 | | merge_assignments([],no_merge,[]). |
| 2775 | | merge_assignments([H|T],Merge,[H|TR]) :- merge_assignments(T,Merge,TR). |
| 2776 | | |
| 2777 | | :- use_module(b_read_write_info,[get_lhs_assigned_identifier/2]). |
| 2778 | | get_lhs_assigned_ids(LHS,SortedIds) :- |
| 2779 | | maplist(get_lhs_assigned_identifier,LHS,TLHSAssign), |
| 2780 | | get_sorted_ids(TLHSAssign,SortedIds). |
| 2781 | | merge_two_assignments(S1,S2,NewAssignment) :- |
| 2782 | | is_ordinary_assignment(S1,LHS1,RHS1,_), %print(assign1(LHS1)),nl, |
| 2783 | | is_ordinary_assignment(S2,LHS2,RHS2,_), %print(assign2(LHS2)),nl, |
| 2784 | | get_lhs_assigned_ids(LHS1,SortedIDs1), |
| 2785 | | get_lhs_assigned_ids(LHS2,SortedIDs2), %print(ids(SortedIDs1,SortedIDs2)),nl, |
| 2786 | | ord_disjoint(SortedIDs1,SortedIDs2), % no race condition |
| 2787 | | maplist(not_occurs_in_predicate(SortedIDs1),RHS2), |
| 2788 | | maplist(not_occurs_in_predicate(SortedIDs1),LHS2), % not used in left-hand side, e.g., f(x+y) := RHS |
| 2789 | | get_texpr_info(S1,I1), get_texpr_info(S2,I2), |
| 2790 | | merge_info(I1,I2,Infos), |
| 2791 | | append(LHS1,LHS2,NewLHS), |
| 2792 | | append(RHS1,RHS2,NewRHS), |
| 2793 | | NewAssignment = b(assign(NewLHS,NewRHS),subst,Infos), |
| 2794 | | (debug_mode(off) -> true ; print('Merged assignments: '),translate:print_subst(NewAssignment),nl). |
| 2795 | | construct_sequence([],skip). |
| 2796 | | construct_sequence([TH],H) :- !, TH=b(H,_,_). |
| 2797 | | construct_sequence(List,sequence(List)). |
| 2798 | | |
| 2799 | | % check if we have a simple expression which will not be complicated to calculate |
| 2800 | ? | simple_expression(b(E,_,_)) :- simple2(E). |
| 2801 | | % (simple2(E) -> true ; print(not_simple(E)),nl). |
| 2802 | | simple2(bool_set). |
| 2803 | | simple2(boolean_false). |
| 2804 | | simple2(boolean_true). |
| 2805 | | simple2(empty_sequence). |
| 2806 | | simple2(empty_set). |
| 2807 | | simple2(identifier(_)). |
| 2808 | | %simple2(integer_set(_)). |
| 2809 | | simple2(X) :- is_integer_set(X,_). |
| 2810 | | simple2(integer(_)). |
| 2811 | | simple2(lazy_lookup_expr(_)). |
| 2812 | | simple2(lazy_let_expr(_,A,B)) :- simple2(B), simple_expr_or_pred(A). |
| 2813 | | simple2(max_int). |
| 2814 | | simple2(min_int). |
| 2815 | | simple2(string_set). |
| 2816 | | simple2(string(_)). |
| 2817 | | simple2(value(_)). |
| 2818 | | simple2(first_of_pair(_)). simple2(second_of_pair(_)). |
| 2819 | | simple2(interval(A,B)) :- simple_expression(A), simple_expression(B). |
| 2820 | ? | simple2(add(A,B)) :- simple_expression(A), simple_expression(B). |
| 2821 | ? | simple2(minus(A,B)) :- simple_expression(A), simple_expression(B). |
| 2822 | | simple2(multiplication(A,B)) :- simple_expression(A), simple_expression(B). |
| 2823 | | simple2(unary_minus(A)) :- simple_expression(A). |
| 2824 | | simple2(convert_bool(A)) :- simple_predicate(A). |
| 2825 | | simple2(sequence_extension(A)) :- maplist(simple_expression,A). |
| 2826 | | simple2(set_extension(A)) :- maplist(simple_expression,A). % a bit more expensive than sequence_extension: elements need to be compared |
| 2827 | | |
| 2828 | | simple_expr_or_pred(b(E,T,_)) :- (T=pred -> simplep2(E) ; simple2(E)). |
| 2829 | | |
| 2830 | | simple_predicate(b(E,_,_)) :- simplep2(E). |
| 2831 | | simplep2(equal(A,B)) :- simple_expression(A), simple_expression(B). % could be slightly more expensive if set type |
| 2832 | | simplep2(not_equal(A,B)) :- simple_expression(A), simple_expression(B). % ditto |
| 2833 | | simplep2(lazy_let_pred(_,A,B)) :- simple_predicate(B), simple_expr_or_pred(A). |
| 2834 | | simplep2(less(A,B)) :- simple_expression(A), simple_expression(B). |
| 2835 | | simplep2(less_equal(A,B)) :- simple_expression(A), simple_expression(B). |
| 2836 | | simplep2(greater(A,B)) :- simple_expression(A), simple_expression(B). |
| 2837 | | simplep2(greater_equal(A,B)) :- simple_expression(A), simple_expression(B). |
| 2838 | | |
| 2839 | | % detect ID = Expr or Expr = ID |
| 2840 | ? | identifier_equality(TExpr,ID,TID,Expr) :- is_equality(TExpr,LHS,RHS), |
| 2841 | ? | ( get_texpr_id(LHS,ID), TID=LHS, Expr = RHS |
| 2842 | | ; get_texpr_id(RHS,ID), TID=RHS, Expr = LHS). |
| 2843 | | |
| 2844 | | :- use_module(self_check). |
| 2845 | | :- assert_must_succeed(b_ast_cleanup:nested_couple_to_list(b(couple(b(couple(a,b),x,[]),c),xx,[]),[a,b,c])). |
| 2846 | | :- assert_must_succeed(b_ast_cleanup:nested_couple_to_list(b(couple(a,c),x,[]),[a,c])). |
| 2847 | | :- assert_must_succeed(b_ast_cleanup:nested_couple_to_list(b(couple(a,b(couple(b,c),x,[])),xx,[]),[a,b(couple(b,c),x,[])])). |
| 2848 | | nested_couple_to_list(NC,L) :- nested_couple_to_list_dcg(NC,L,[]). |
| 2849 | | nested_couple_to_list_dcg(b(couple(A,B),_,_)) --> !, |
| 2850 | | nested_couple_to_list_dcg(A), [B]. |
| 2851 | | nested_couple_to_list_dcg(E) --> [E]. |
| 2852 | | |
| 2853 | | |
| 2854 | | create_equalities_for_let(ORefs,Primed,Equalities) :- |
| 2855 | | maplist(create_equality_for_let,ORefs,Primed,Equalities). |
| 2856 | | create_equality_for_let(oref(PrimedId,OrigId,Type),TPrimed,Equality) :- |
| 2857 | | create_texpr(identifier(OrigId),Type,[],TOrig), |
| 2858 | | create_texpr(identifier(PrimedId),Type,[],TPrimed), |
| 2859 | | safe_create_texpr(equal(TPrimed,TOrig),pred,Equality). |
| 2860 | | |
| 2861 | | % inserts a let statement. If the original statement is a precondition or any, the let is moved |
| 2862 | | % inside the original statement to prevent strange side-effects. This can be used for other, |
| 2863 | | % non-value changing substitutions as well. |
| 2864 | | insert_let(TExpr,Ids,P,NTExpr) :- |
| 2865 | | remove_bt(TExpr,Expr,NewExpr,NTExpr), |
| 2866 | | move_let_inside(Expr,Old,New,NewExpr),!, |
| 2867 | | insert_let(Old,Ids,P,New). |
| 2868 | | insert_let(TExpr,Ids,P,NTExpr) :- |
| 2869 | | create_texpr(let(Ids,P,TExpr),subst,[],NTExpr). |
| 2870 | | move_let_inside(precondition(Cond,Old),Old,New,precondition(Cond,New)). |
| 2871 | | move_let_inside(any(Any,Where,Old),Old,New,any(Any,Where,New)). |
| 2872 | | |
| 2873 | | % find_one_point_rules(+TypedIds,+Blacklist,+Predicates, |
| 2874 | | % -LetIds,-LetExprs,-RemainingIds,-RemainingPredicates, +CheckWellDeff) |
| 2875 | | % TypedIds: The ids that are quantified in the exists clause |
| 2876 | | % Blacklist: All ids that must not be used in the found expression |
| 2877 | | % Predicates: The predicates of the exists (without already used id=E predicates) |
| 2878 | | % LetIds: The ids that can be introduced as LET |
| 2879 | | % LetExprs. For each id (in LetIds) the corresponding expression |
| 2880 | | % RemainingIds: The ids that are not converted into LETs |
| 2881 | | % RemainingPredicates: The predicates after removing the id=E predicates |
| 2882 | | % CheckWellDef: check_well_definedness --> only extract equalities from first pred or if always_well_defined |
| 2883 | | % (e.g., f = {1|->2} & !e.(2:dom(f) & e=f(2) => e>100) should not generate a WD-error) |
| 2884 | | find_one_point_rules([],Preds,_,[],[],[],Preds,_). |
| 2885 | | find_one_point_rules([TId|Irest],Preds,Blacklist,LetIds,Exprs,RestIds,NewPreds,CheckWellDef) :- |
| 2886 | ? | ( select_equality(TId,Preds,Blacklist,_,Expr,RestPred,_,CheckWellDef) -> |
| 2887 | | LetIds = [TId|Lrest], Exprs = [Expr|Erest], |
| 2888 | | RestIds = RestIds2, Preds2 = RestPred |
| 2889 | | ; otherwise -> |
| 2890 | | LetIds = Lrest, Exprs = Erest, |
| 2891 | | RestIds = [TId|RestIds2], Preds2 = Preds), |
| 2892 | | find_one_point_rules(Irest,Preds2,Blacklist,Lrest,Erest,RestIds2,NewPreds,CheckWellDef). |
| 2893 | | % select a predicate from Preds of the form id=Expr (or Expr=id) where Expr does not contain |
| 2894 | | % references to identifiers in Blacklist. Rest is Preds without id=Expr |
| 2895 | | select_equality(TId,Preds,Blacklist,TEqual,Expr,Rest,UsedIds,CheckWellDef) :- |
| 2896 | ? | get_texpr_id(TId,Id), |
| 2897 | ? | is_equality(TEqual,TA,TB), |
| 2898 | ? | safe_select(CheckWellDef,TEqual,Preds,Rest), |
| 2899 | ? | ( get_texpr_id(TA,Id),TB=Expr ; get_texpr_id(TB,Id),TA=Expr ), |
| 2900 | | find_identifier_uses(Expr,[],UsedIds), |
| 2901 | | ord_disjoint(Blacklist,UsedIds). |
| 2902 | | |
| 2903 | | % the ast_cleanup rules have not run yet on the sub-expressions of the exists: detect equalities |
| 2904 | | is_equality(TP,TA,TB) :- get_texpr_expr(TP,P), is_equality_aux(P,TA,TB). |
| 2905 | | :- block is_equality_aux(-,?,?). |
| 2906 | | is_equality_aux(equal(TA,TB),TA,TB). |
| 2907 | | is_equality_aux(partition(TA,[TB]),TA,TB). |
| 2908 | | is_equality_aux(member(TA,TSet),TA,TB) :- singleton_set_extension(TSet,TB). |
| 2909 | | is_equality_aux(negation(b(not_equal(TA,TB),pred,_)),TA,TB). |
| 2910 | | % others not not_member ? |
| 2911 | | |
| 2912 | ? | safe_select(check_well_definedness,Element,[H|T],Rest) :- !, |
| 2913 | ? | (Element=H,Rest=T % either first element |
| 2914 | | ; % or if later element; then it must be well-defined; otherwise H could fail |
| 2915 | ? | select(Element,T,TRest), Rest=[H|TRest], |
| 2916 | | always_defined_full_check_or_disprover_mode(Element) % we cannot use always_well_defined(Element) in cleanup_pre; it is only computed in cleanup_post at the moment; TO DO: we now do compute in pre phase |
| 2917 | | %, print(always_wd(Element)),nl |
| 2918 | | ). |
| 2919 | ? | safe_select(_,Element,List,Rest) :- select(Element,List,Rest). |
| 2920 | | |
| 2921 | | % split predicate into conjuncts using a certain list of ids and those not |
| 2922 | | split_predicate(Pred,Ids,UsingIds,NotUsingIds) :- |
| 2923 | | conjunction_to_list(Pred,LP), |
| 2924 | | get_sorted_ids(Ids,SIds), |
| 2925 | | filter(not_occurs_in_predicate(SIds),LP,NP,UP), |
| 2926 | | conjunct_predicates(NP,NotUsingIds), |
| 2927 | | conjunct_predicates(UP,UsingIds). |
| 2928 | | |
| 2929 | | not_occurs_in_predicate([],_Pred) :- !. |
| 2930 | | not_occurs_in_predicate(SortedIDs,Pred) :- SortedIDs = [ID1|_], |
| 2931 | | (ID1 = b(_,_,_) -> add_internal_error('Wrapped identifiers: ',not_occurs_in_predicate(SortedIDs,Pred)) ; true), |
| 2932 | | find_identifier_uses(Pred,[],UsedIds), |
| 2933 | | ord_disjoint(SortedIDs,UsedIds). |
| 2934 | | get_sorted_ids(Ids,SIds) :- |
| 2935 | | get_texpr_ids(Ids,UnsortedIds),sort(UnsortedIds,SIds). |
| 2936 | | |
| 2937 | | % basically we redo the work in select_equality: to do: cleanup and merge code |
| 2938 | | find_lets(Ids,Pred,[BID|IDT],[EQUALITY|T],RestIds,RestPred) :- Ids \= [], |
| 2939 | | %print(find_lets(Ids)),nl, |
| 2940 | | get_sorted_ids(Ids,SIds), |
| 2941 | ? | b_interpreter:member_conjunct(Eq,Pred,RestPred1), |
| 2942 | ? | id_equality(Eq,ID,RHS), |
| 2943 | ? | select(BID,Ids,RestIds1),get_texpr_id(BID,ID), |
| 2944 | | % Check that RHS does not contain any variable from Ids ! |
| 2945 | | not_occurs_in_predicate(SIds,RHS), |
| 2946 | | !, |
| 2947 | | %print(found_let(ID)),nl, |
| 2948 | | %EQUALITY = b(equal(BID,RHS),pred,[generated_let]), |
| 2949 | | safe_create_texpr(equal(BID,RHS),pred,EQUALITY), |
| 2950 | | find_lets(RestIds1,RestPred1,IDT,T,RestIds,RestPred). |
| 2951 | | find_lets(Ids,Pred,[],[],Ids,Pred). |
| 2952 | | id_equality(Pred,ID,EqExpr) :- |
| 2953 | ? | get_texpr_expr(Pred,equal(LHS,RHS)), |
| 2954 | ? | (get_texpr_id(LHS,ID), EqExpr=RHS |
| 2955 | | ; |
| 2956 | | get_texpr_id(RHS,ID), EqExpr=LHS). |
| 2957 | | |
| 2958 | | pred_succ_compset(Op,comprehension_set([A,B],Pred)) :- |
| 2959 | | %get_unique_id('_a_',AId),get_unique_id('_b_',BId), |
| 2960 | | BId = '_lambda_result_', |
| 2961 | | (Op = add -> AId = '_succ_' ; AId='_pred_'), |
| 2962 | | create_texpr(identifier(AId),integer,[],A), |
| 2963 | | create_texpr(identifier(BId),integer,[],B), |
| 2964 | | create_texpr(integer(1),integer,[],Integer), |
| 2965 | | create_texpr(ArithOp,integer,[],TArithOp), |
| 2966 | | ArithOp =.. [Op,A,Integer], |
| 2967 | | safe_create_texpr(equal(B,TArithOp),pred,Pred). |
| 2968 | | |
| 2969 | | add_used_identifier_info(Ids,P,IOld,[used_ids(FoundIds)|I1]) :- |
| 2970 | | % add used identifiers to information |
| 2971 | | get_sorted_ids(Ids,Ignore), |
| 2972 | | find_identifier_uses(P,Ignore,FoundIds), |
| 2973 | | %print(computed_used_ids(ignore(Ignore),found(FoundIds))),nl, translate:print_bexpr(P),nl, |
| 2974 | ? | (select(used_ids(_),IOld,I1) -> true ; I1=IOld). |
| 2975 | | |
| 2976 | | % can be used to check the validity of the used_ids field, e.g., for existential quantifier |
| 2977 | | check_used_ids_info(Parameters,Predicate,StoredUsedIds,PP) :- |
| 2978 | | % get_global_identifiers(Ignored), and add to Parameters ?? |
| 2979 | | (add_used_identifier_info(Parameters,Predicate,[],[used_ids(UsedIds)]) |
| 2980 | | -> (StoredUsedIds=UsedIds -> true |
| 2981 | | ; ord_subset(UsedIds,StoredUsedIds) |
| 2982 | | -> format('Suboptimal used_ids info: ~w (actual ~w) [origin ~w with ~w]~n',[StoredUsedIds,UsedIds,PP,Parameters]) |
| 2983 | | %, translate:print_bexpr(Predicate),nl |
| 2984 | | ; add_internal_error('Incorrect used_ids info: ', check_used_ids_info(Parameters,Predicate,UsedIds,PP)), |
| 2985 | | translate:print_bexpr(Predicate),nl, |
| 2986 | | (extract_span_description(Predicate,PosMsg) -> format('Location: ~w~n',[PosMsg]) ; true), |
| 2987 | | ord_subtract(UsedIds,StoredUsedIds,Delta), |
| 2988 | | format('Incorrect used_ids info: ~w (actual ~w)~nNot included: ~w~n~n',[StoredUsedIds,UsedIds,Delta]) |
| 2989 | | %, translate:print_bexpr(Predicate),nl |
| 2990 | | ) |
| 2991 | | ; add_internal_error('Could not computed used ids:', |
| 2992 | | add_used_identifier_info(Parameters,Predicate,[],[used_ids(_)])) |
| 2993 | | ). |
| 2994 | | |
| 2995 | | % update used_ids_info for existential and universal quantifier (at top-level only !) |
| 2996 | | recompute_used_ids_info(b(E,pred,Info1),Res) :- |
| 2997 | | recompute_used_ids_info_aux(E,Info1,Info2),!, Res= b(E,pred,Info2). |
| 2998 | | recompute_used_ids_info(TE,TE). |
| 2999 | | |
| 3000 | | recompute_used_ids_info_aux(exists(Parameters,Predicate),Info1,Info2) :- |
| 3001 | | add_used_identifier_info(Parameters,Predicate,Info1,Info2). |
| 3002 | | recompute_used_ids_info_aux(forall(Parameters,Lhs,Rhs),Info1,Info2) :- |
| 3003 | | conjunct_predicates([Lhs,Rhs],Predicate), |
| 3004 | | add_used_identifier_info(Parameters,Predicate,Info1,Info2). |
| 3005 | | % for while loop we could recompute modifies and reads info |
| 3006 | | |
| 3007 | | % generation of unique identifiers |
| 3008 | | :- dynamic unique_id_counter/1. |
| 3009 | | unique_id_counter(1). |
| 3010 | | |
| 3011 | | get_unique_id_inside(Prefix,Pred,ResultId) :- |
| 3012 | | (\+ occurs_in_expr(Prefix,Pred) % first try and see whether we need to append a number |
| 3013 | | -> ResultId = Prefix |
| 3014 | | ; get_unique_id(Prefix,ResultId) |
| 3015 | | ). |
| 3016 | | get_unique_id_inside(Prefix,Pred,Expr,ResultId) :- |
| 3017 | | ((\+ occurs_in_expr(Prefix,Pred), |
| 3018 | | \+ occurs_in_expr(Prefix,Expr)) % first try and see whether we need to append a number |
| 3019 | | -> ResultId = Prefix |
| 3020 | | ; get_unique_id(Prefix,ResultId) |
| 3021 | | ). |
| 3022 | | |
| 3023 | | get_unique_id(Prefix,Id) :- |
| 3024 | | retract(unique_id_counter(Old)), |
| 3025 | | New is Old + 1, |
| 3026 | | assert(unique_id_counter(New)), |
| 3027 | | safe_atom_chars(Prefix,CPrefix,get_unique_id1), |
| 3028 | | number_chars(Old,CNumber), |
| 3029 | | append(CPrefix,CNumber,CId), |
| 3030 | | safe_atom_chars(Id,CId,get_unique_id2). |
| 3031 | | |
| 3032 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 3033 | | % replace all variables in types by "any" |
| 3034 | | |
| 3035 | | ground_type_to_any(T,Exceptions) :- var(T),!, |
| 3036 | | ( exact_member(T,Exceptions) -> ! % any variable exact member in list is not grounded |
| 3037 | | ; otherwise -> T=any). |
| 3038 | | ground_type_to_any(record(Fields),Exceptions) :- !, |
| 3039 | | % treat records separately, we do not want the list of fields to be bound to any; see B/Tickets/RecordPartiallyTyped |
| 3040 | | ground_field_types(Fields,Exceptions). |
| 3041 | | ground_type_to_any(T,_) :- ground(T),!. |
| 3042 | | ground_type_to_any(T,Exceptions) :- |
| 3043 | | functor(T,_,Arity), |
| 3044 | | ground_type_args(Arity,T,Exceptions). |
| 3045 | | ground_type_args(0,_T,_Exceptions) :- !. |
| 3046 | | ground_type_args(N,T,Exceptions) :- |
| 3047 | | arg(N,T,Arg),ground_type_to_any(Arg,Exceptions), |
| 3048 | | N2 is N-1,ground_type_args(N2,T,Exceptions). |
| 3049 | | |
| 3050 | | ground_field_types(T,Exceptions) :- var(T),!, |
| 3051 | | ( exact_member(T,Exceptions) -> ! % any variable exact member in list is not grounded |
| 3052 | | ; otherwise -> print(grounding_open_ended_record),nl, % should we generate a warning here ? |
| 3053 | | T=[] |
| 3054 | | ). |
| 3055 | | ground_field_types([],_) :- !. |
| 3056 | | ground_field_types([field(Name,Type)|T],Exceptions) :- !, |
| 3057 | | (var(Name) |
| 3058 | | -> add_internal_error('Unbound record field name: ',ground_field_types([field(Name,Type)|T],Exceptions)) |
| 3059 | | ; true), |
| 3060 | | ground_type_to_any(Type,Exceptions), |
| 3061 | | ground_field_types(T,Exceptions). |
| 3062 | | ground_field_types(Other,Exceptions) :- |
| 3063 | | add_internal_error('Illegal record field list: ',ground_field_types(Other,Exceptions)). |
| 3064 | | |
| 3065 | | % annote variables of becomes_such with before_substitution infos |
| 3066 | | annotate_becomes_such_vars(Ids1,Pred,Ids2) :- |
| 3067 | | find_used_primed_ids(Pred,Ids1,BeforeAfter), |
| 3068 | | maplist(add_before_after_info(BeforeAfter),Ids1,Ids2). |
| 3069 | | % put optional before/after usage into the information of the identifiers |
| 3070 | | % makes only sense in the context of becomes_such substitutions |
| 3071 | | add_before_after_info(BeforeAfter,TId,TId2) :- |
| 3072 | | def_get_texpr_id(TId,Id), |
| 3073 | | ( member(ba(Id,BeforeId),BeforeAfter) -> |
| 3074 | | get_texpr_type(TId,Type), get_texpr_info(TId,Info), |
| 3075 | | create_texpr(identifier(Id),Type,[before_substitution(Id,BeforeId)|Info],TId2) |
| 3076 | | ; otherwise -> TId = TId2 ). |
| 3077 | | |
| 3078 | | % find all used pairs of before/after variables, e.g. ba(x,'x$0') |
| 3079 | | % see becomes_such substitutions |
| 3080 | | find_used_primed_ids(TExpr,PossibleIds,Uses) :- |
| 3081 | | prime_identifiers0(PossibleIds,TP0), |
| 3082 | | get_sorted_ids(TP0,SP0), % sorted list of primed ids |
| 3083 | | %print(find(SP0,PossibleIds)),nl, translate:print_bexpr(TExpr),nl, |
| 3084 | | find_used_primed_ids2(SP0,TExpr,[],Uses). |
| 3085 | | find_used_primed_ids2(SP0,TExpr,In,Out) :- |
| 3086 | | syntaxtraversion(TExpr,Expr,_,_Infos,Subs,_), |
| 3087 | | ( (Expr = identifier(FullId), |
| 3088 | | %member(before_substitution(Id,FullId),Infos) % this info is not available in Event-B mode |
| 3089 | | ord_member(FullId,SP0), |
| 3090 | | prime_atom0(Id,FullId)) |
| 3091 | | -> ord_add_element(In,ba(Id,FullId),Uses) |
| 3092 | | ; otherwise -> In = Uses ), |
| 3093 | | foldl(find_used_primed_ids2(SP0),Subs,Uses,Out). |
| 3094 | | |
| 3095 | | %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% |
| 3096 | | % find expressions which are possibly not well-defined |
| 3097 | | |
| 3098 | | is_possibly_undefined(Expr) :- |
| 3099 | | safe_syntaxelement(Expr,Subs,_Names,_,_), |
| 3100 | ? | member(Sub,Subs), |
| 3101 | | get_texpr_info(Sub,Info), |
| 3102 | | memberchk(contains_wd_condition,Info),!. |
| 3103 | | is_possibly_undefined(Expr) :- |
| 3104 | ? | functor(Expr,F,_),has_wd_condition(F,Expr). %%,print(wd(F,Expr)),nl. |
| 3105 | | |
| 3106 | | always_defined_full_check_or_disprover_mode(_) :- preferences:get_preference(disprover_mode,true),!. |
| 3107 | | always_defined_full_check_or_disprover_mode(BExpr) :- \+ full_check_is_possibly_undefined(BExpr). |
| 3108 | | |
| 3109 | | % a version which does the full traversal; can be used before contains_wd_condition has been computed |
| 3110 | | full_check_is_possibly_undefined(BExpr) :- get_texpr_expr(BExpr,Expr), |
| 3111 | | full_check_is_possibly_undefined_aux(Expr). |
| 3112 | | full_check_is_possibly_undefined_aux(Expr) :- |
| 3113 | | functor(Expr,F,_),has_wd_condition(F,Expr),!. |
| 3114 | | full_check_is_possibly_undefined_aux(Expr) :- |
| 3115 | | syntaxtraversion(_,Expr,_,_,Subs,_), |
| 3116 | ? | member(Sub,Subs), |
| 3117 | | full_check_is_possibly_undefined(Sub),!. |
| 3118 | | |
| 3119 | | :- use_module(external_functions,[external_fun_has_wd_condition/1]). |
| 3120 | | % determine if an operator has an attached WD condition (used to compute contains_wd_condition) |
| 3121 | | % division and module must not divide by zero |
| 3122 | | has_wd_condition(div,Expr) :- arg(2,Expr,DIV), |
| 3123 | | \+ definitely_not_zero(DIV). |
| 3124 | | has_wd_condition(floored_div,Expr) :- arg(2,Expr,DIV), |
| 3125 | | \+ definitely_not_zero(DIV). |
| 3126 | ? | has_wd_condition(modulo,Expr) :- arg(2,Expr,DIV), |
| 3127 | ? | (\+ definitely_not_zero(DIV) ; |
| 3128 | | \+ definitely_not_negative(DIV) ; |
| 3129 | | arg(1,Expr,A1), \+ definitely_not_negative(A1)). |
| 3130 | | % power_of must have a non-negative exponent (?) |
| 3131 | | has_wd_condition(power_of,Expr) :- arg(2,Expr,EXP), |
| 3132 | | \+ definitely_not_negative(EXP). |
| 3133 | | % min and max need a non-empty set |
| 3134 | | % also Atelier-B manual requires the set to have an upper limit |
| 3135 | | has_wd_condition(max,Expr) :- arg(1,Expr,S), \+ definitely_not_empty_and_finite(S). |
| 3136 | | has_wd_condition(min,Expr) :- arg(1,Expr,S), \+ definitely_not_empty_and_finite(S). |
| 3137 | | % all the sequence operations must not be applied to non-sequence |
| 3138 | | % relations and some must not be applied to empty-sequences |
| 3139 | | has_wd_condition(size,E) :- arg(1,E,S), \+ definitely_sequence(S). |
| 3140 | | has_wd_condition(first,E) :- arg(1,E,S), \+ definitely_not_empty_sequence(S). |
| 3141 | | has_wd_condition(last,E) :- arg(1,E,S), \+ definitely_not_empty_sequence(S). |
| 3142 | | has_wd_condition(front,E) :- arg(1,E,S), \+ definitely_not_empty_sequence(S). |
| 3143 | | has_wd_condition(tail,E) :- arg(1,E,S), \+ definitely_not_empty_sequence(S). |
| 3144 | | has_wd_condition(rev,E) :- arg(1,E,S), \+ definitely_sequence(S). |
| 3145 | | has_wd_condition(concat,_). |
| 3146 | | has_wd_condition(insert_front,_). |
| 3147 | | has_wd_condition(insert_tail,_). |
| 3148 | | has_wd_condition(restrict_front,_). |
| 3149 | | has_wd_condition(restrict_tail,_). |
| 3150 | | has_wd_condition(general_concat,_). |
| 3151 | | % functions must not be applied to values outside their domain |
| 3152 | | has_wd_condition(function,_). |
| 3153 | | % the general intersection must not be applied to an empty set of sets |
| 3154 | | has_wd_condition(general_intersection,_). |
| 3155 | | has_wd_condition(quantified_intersection,_). % gets translated to general_intersection |
| 3156 | | % card must not be applied to infinite sets: |
| 3157 | | has_wd_condition(card,Expr) :- arg(1,Expr,S), \+ definitely_finite(S). |
| 3158 | | has_wd_condition(freetype_destructor,_). |
| 3159 | | has_wd_condition(external_function_call,Expr) :- arg(1,Expr,FunName), |
| 3160 | | external_fun_has_wd_condition(FunName). |
| 3161 | | has_wd_condition(external_pred_call,Expr) :- arg(1,Expr,FunName), |
| 3162 | | external_fun_has_wd_condition(FunName). |
| 3163 | | has_wd_condition(operation_call_in_expr,_). % we now assume all operation calls may have PRE-conditions |
| 3164 | | % or involve recursion, and thus may loop; TO DO: compute this information per operation by a fixpoint algorithm |
| 3165 | | |
| 3166 | | definitely_not_zero(b(integer(X),integer,_)) :- number(X), X \= 0. |
| 3167 | | definitely_not_negative(b(integer(X),integer,_)) :- number(X), X >= 0. |
| 3168 | | % to do add more ?: card(_), ... |
| 3169 | | |
| 3170 | | definitely_not_empty_and_finite(b(S,_,_)) :- definitely_not_empty2(S). |
| 3171 | | definitely_not_empty2(bool_set). |
| 3172 | | definitely_not_empty2(set_extension(_)). |
| 3173 | | definitely_not_empty2(sequence_extension(_)). |
| 3174 | | definitely_not_empty2(cartesian_product(A,B)) :- definitely_not_empty_and_finite(A), definitely_not_empty_and_finite(B). |
| 3175 | | definitely_not_empty2(union(A,B)) :- definitely_not_empty_and_finite(A), definitely_not_empty_and_finite(B). |
| 3176 | | definitely_not_empty2(overwrite(A,B)) :- definitely_not_empty_and_finite(A),definitely_not_empty_and_finite(B). |
| 3177 | | definitely_not_empty2(value(S)) :- % what about closures ? |
| 3178 | | definitely_not_empty_finite_value(S). %kernel_objects:not_empty_set(S). |
| 3179 | | |
| 3180 | | definitely_not_empty_finite_value(S) :- var(S),!,fail. |
| 3181 | | definitely_not_empty_finite_value([_|_]). |
| 3182 | | definitely_not_empty_finite_value(avl_set(_)). |
| 3183 | | %definitely_not_empty_value(closure(P,T,B)) :- |
| 3184 | | |
| 3185 | | definitely_not_empty_sequence(b(S,_,_)) :- definitely_not_empty_sequence2(S). |
| 3186 | | definitely_not_empty_sequence2(sequence_extension(_)). |
| 3187 | | |
| 3188 | | definitely_sequence(b(S,_,_)) :- definitely_sequence2(S). |
| 3189 | | definitely_sequence2(empty_sequence). |
| 3190 | | definitely_sequence2(sequence_extension(_)). |
| 3191 | | |
| 3192 | | definitely_finite(b(S,Type,_)) :- (is_infinite_type(Type) -> definitely_finite2(S) ; true). |
| 3193 | | definitely_finite2(bool_set). |
| 3194 | | definitely_finite2(empty_set). |
| 3195 | | definitely_finite2(empty_sequence). |
| 3196 | | definitely_finite2(set_extension(_)). |
| 3197 | | definitely_finite2(sequence_extension(_)). |
| 3198 | | definitely_finite2(cartesian_product(A,B)) :- definitely_finite(A), definitely_finite(B). |
| 3199 | | definitely_finite2(overwrite(A,B)) :- definitely_finite(A), definitely_finite(B). |
| 3200 | | definitely_finite2(union(A,B)) :- definitely_finite(A), definitely_finite(B). |
| 3201 | | definitely_finite2(intersection(A,B)) :- (definitely_finite(A) -> true ; definitely_finite(B)). |
| 3202 | | definitely_finite2(set_subtraction(A,_)) :- definitely_finite(A). |
| 3203 | | definitely_finite2(interval(_,_)). |
| 3204 | | definitely_finite2(value(S)) :- nonvar(S),(S=[] ; S=avl_set(_)). |
| 3205 | | % TO DO: add other operators : range_restriction,domain_restriction,... |
| 3206 | | |
| 3207 | | :- use_module(custom_explicit_sets,[quick_is_definitely_maximal_set/1]). |
| 3208 | | % should we use is_just_type/1 instead ?? TO DO: check |
| 3209 | | definitely_maximal_set(b(S,_,_)) :- definitely_maximal2(S). |
| 3210 | | definitely_maximal2(integer_set('INTEGER')). |
| 3211 | | definitely_maximal2(bool_set). |
| 3212 | | definitely_maximal2(string_set). |
| 3213 | | definitely_maximal2(comprehension_set(_,b(truth,_,_))). % also covers is_integer_set(X,'INTEGER') |
| 3214 | | definitely_maximal2(value(S)) :- nonvar(S),quick_is_definitely_maximal_set(S). |
| 3215 | | |
| 3216 | | |
| 3217 | | get_integer(b(B,_,_),I) :- get_integer_aux(B,I). |
| 3218 | | get_integer_aux(integer(I),I). |
| 3219 | | get_integer_aux(value(V),I) :- nonvar(V),V=int(I). |
| 3220 | | |
| 3221 | | % ---------------------------------- |
| 3222 | | |
| 3223 | | |
| 3224 | | select_conjunct(Predicate,Conjunction,Prefix,Suffix) :- |
| 3225 | ? | conjunction_to_list(Conjunction,List), |
| 3226 | ? | append(Prefix,[Predicate|Suffix],List). |
| 3227 | | |
| 3228 | | |
| 3229 | | data_validation_mode :- |
| 3230 | | (get_preference(data_validation_mode,true) -> true |
| 3231 | | ; environ(prob_data_validation_mode,true)). |
| 3232 | | |
| 3233 | | % ------------------------ |
| 3234 | | |
| 3235 | | % mini partial evaluation / constant expression evaluation of B expressions |
| 3236 | | % TO DO: unify with b_compile and b_expression_sharing ! |
| 3237 | | % But this one only pre-computes top-level operators; assumes bottom-up traversal |
| 3238 | | |
| 3239 | | :- use_module(kernel_objects,[safe_pown/3]). |
| 3240 | | pre_compute_static_int_expression(add(A,B),Result) :- % plus |
| 3241 | | get_integer(A,IA), get_integer(B,IB), |
| 3242 | | Result is IA+IB. |
| 3243 | | pre_compute_static_int_expression(minus(A,B),Result) :- % plus |
| 3244 | | get_integer(A,IA), get_integer(B,IB), |
| 3245 | | Result is IA-IB. |
| 3246 | | pre_compute_static_int_expression(unary_minus(A),Result) :- % plus |
| 3247 | | get_integer(A,IA), |
| 3248 | | Result is -IA. |
| 3249 | | pre_compute_static_int_expression(multiplication(A,B),Result) :- |
| 3250 | | get_integer(A,IA), get_integer(B,IB), |
| 3251 | | Result is IA*IB. |
| 3252 | | pre_compute_static_int_expression(div(A,B),Result) :- % TO DO: also add floored_div |
| 3253 | | get_integer(B,IB), IB \= 0, |
| 3254 | | get_integer(A,IA), |
| 3255 | | Result is IA//IB. |
| 3256 | | pre_compute_static_int_expression(modulo(A,B),Result) :- |
| 3257 | | get_integer(B,IB), IB > 0, |
| 3258 | | get_integer(A,IA), IA >= 0, |
| 3259 | | Result is IA mod IB. |
| 3260 | | pre_compute_static_int_expression(power_of(A,B),Result) :- |
| 3261 | | get_integer(A,IA), get_integer(B,IB), IB >= 0, |
| 3262 | | safe_pown(IA,IB,Result), number(Result). |
| 3263 | | |
| 3264 | | |