1 | % (c) 2009-2022 Lehrstuhl fuer Softwaretechnik und Programmiersprachen, | |
2 | % Heinrich Heine Universitaet Duesseldorf | |
3 | % This software is licenced under EPL 1.0 (http://www.eclipse.org/org/documents/epl-v10.html) | |
4 | ||
5 | :- module(partition_detection, [detect_partitions/2, detect_all_partitions_in_predicate/2, is_disjoint_pred/4]). | |
6 | ||
7 | :- use_module(module_information,[module_info/2]). | |
8 | :- module_info(group,typechecker). | |
9 | :- module_info(description,'This module detects set partition predicates.'). | |
10 | ||
11 | :- use_module(library(lists)). | |
12 | :- use_module(bsyntaxtree). | |
13 | :- use_module(bmachine_structure,[select_section/5]). | |
14 | ||
15 | detect_partitions(In,Out) :- | |
16 | select_section(properties,Old,New,In,Out), | |
17 | detect_all_partitions_in_predicate(Old,New). | |
18 | ||
19 | % detect all set partition predicates at "top-level", not inside inner predicates (bool(.), comprehension_set,...) | |
20 | % this is assumed to be checked by b_ast_cleanup during bottom-up construction | |
21 | detect_all_partitions_in_predicate(Predicate,NewPredicate) :- | |
22 | conjunction_to_list(Predicate,PList), | |
23 | detect_all_partitions_in_predicates(PList,true,PNew), | |
24 | !, | |
25 | conjunct_predicates(PNew,NewPredicate). | |
26 | detect_all_partitions_in_predicate(Predicate,Predicate). % relevant for e.g., test 1840 to avoid removing labels,... | |
27 | ||
28 | detect_all_partitions_in_predicates(Predicates,Change,NewPredicates) :- | |
29 | %nl,print('detect_partitions: '),translate:l_print_bexpr_or_subst(Predicates),nl, | |
30 | ( detect_partitions_in_predicates(Predicates,P1) -> | |
31 | %print('change: '),translate:l_print_bexpr_or_subst(P1),nl,nl, | |
32 | Change=true, | |
33 | detect_all_partitions_in_predicates(P1,_,NewPredicates) | |
34 | ; | |
35 | Change=false, | |
36 | Predicates=NewPredicates %, print('detected: '),translate:print_bexpr(NewPredicate),nl | |
37 | %detect_partitions_inside_predicate(Predicate,NewPredicate) % now done in b_ast_cleanup | |
38 | ). | |
39 | ||
40 | :- use_module(probsrc(error_manager), [add_message/4]). | |
41 | :- use_module(probsrc(debug), [debug_mode/1]). | |
42 | :- use_module(probsrc(preferences), [get_preference/2]). | |
43 | ||
44 | % detect partitions of set of the type: | |
45 | % x /\ y = {} & x \/ y = z | |
46 | detect_partitions_in_predicates(Predicates,NewPredicates) :- Predicates \= [], | |
47 | ? | find_union(Superset,Partitions,EqualityPred,Predicates,P11,P12), |
48 | create_pairs(Partitions,Pairs), % we need to find inequalities for every pair of elements of Partitions | |
49 | get_texpr_type(Superset,Type), | |
50 | find_all_intersections(Pairs,Type,RestPairs1,P11,P21), | |
51 | find_all_intersections(RestPairs1,Type,RestPairs2,P12,P22), | |
52 | RestPairs2=[], % all pairs are disjoint --> we have found a partition of Superset | |
53 | !, | |
54 | safe_create_texpr(partition(Superset,Partitions),pred,Part), | |
55 | copy_pos_infos(EqualityPred,Part,PartWithInfo), | |
56 | % TO DO: extract_position info from intersections and merge_info | |
57 | % now insert partition predicate at position of union | |
58 | (debug_mode(off),get_preference(performance_monitoring_on,false) -> true | |
59 | ; add_message(partition_detection,'Detected partition predicate for:',Superset,EqualityPred)), | |
60 | append(P21,[PartWithInfo|P22],NewPredicates). | |
61 | ||
62 | :- use_module(bsyntaxtree,[get_texpr_set_type/2]). | |
63 | % should we also find A = {c1,c2,...cn} with all_different(c1,...,cn) ?? | |
64 | find_union(Superset,Partitions,Equal,In,Out1,Out2) :- | |
65 | create_texpr(equal(A,B),pred,_,Equal), | |
66 | get_texpr_set_type(A,Type), | |
67 | get_texpr_set_type(B,Type), | |
68 | append(Out1,[Equal|Out2],In), % select Equal in In Predicates | |
69 | ( is_union(A,Partitions) -> Superset=B | |
70 | ; is_union(B,Partitions) -> Superset=A). | |
71 | ||
72 | is_union(Expr,Partitions) :- | |
73 | get_texpr_expr(Expr,union(_,_)),!, | |
74 | collect_union(Expr,Partitions,[]). | |
75 | is_union(Expr,Partitions) :- | |
76 | % Note: this pattern is rewritten in ast_cleanup, unless optimize_ast is false | |
77 | get_texpr_expr(Expr,general_union(b(set_extension(Partitions),_,_))). | |
78 | ||
79 | collect_union(Expr) --> | |
80 | {get_texpr_expr(Expr,union(A,B)),!}, | |
81 | collect_union(A), | |
82 | collect_union(B). | |
83 | collect_union(Expr) --> [Expr]. | |
84 | ||
85 | create_pairs(Parts,Pairs) :- | |
86 | create_pairs2(Parts,Pairs,[]). | |
87 | create_pairs2([]) --> []. | |
88 | create_pairs2([A|Rest]) --> | |
89 | create_pairs3(Rest,A), | |
90 | create_pairs2(Rest). | |
91 | create_pairs3([],_) --> []. | |
92 | create_pairs3([B|Rest],A) --> | |
93 | [distinct(A,B)], | |
94 | create_pairs3(Rest,A). | |
95 | ||
96 | find_all_intersections(Pairs,Type,RestPairs,In,Out) :- | |
97 | find_all_intersections2(In,Pairs,Type,RestPairs,Out). | |
98 | find_all_intersections2([],Pairs,_,Pairs,[]). | |
99 | find_all_intersections2([Expr|Erest],Pairs,Type,RestPairs,Out) :- | |
100 | is_disjoint_pred(Expr,Type,A,B), | |
101 | remove_pair(A,B,Pairs,InterPairs),!, | |
102 | find_all_intersections2(Erest,InterPairs,Type,RestPairs,Out). | |
103 | find_all_intersections2([Expr|Erest],Pairs,Type,RestPairs,[Expr|Out]) :- | |
104 | find_all_intersections2(Erest,Pairs,Type,RestPairs,Out). | |
105 | ||
106 | is_disjoint_pred(b(Expr,_,_),Type,A,B) :- | |
107 | is_disjoint_pred2(Expr,Type,A,B). | |
108 | is_disjoint_pred2(equal(X,Y),Type,A,B) :- % detect A /\ B = {} or {} = A /\ B | |
109 | ( get_texpr_expr(X,empty_set) -> Inter=Y | |
110 | ; get_texpr_expr(Y,empty_set) -> Inter=X), | |
111 | get_texpr_expr(Inter,intersection(A,B)), get_texpr_type(Inter,Type). | |
112 | is_disjoint_pred2(not_equal(X,Y),set(Type),A,B) :- get_texpr_type(X,Type), | |
113 | A = b(set_extension([X]),set(Type),_), | |
114 | B = b(set_extension([Y]),set(Type),_). | |
115 | is_disjoint_pred2(negation(NE),Type,A,B) :- | |
116 | is_disjoint_neg_pred(NE,Type,A,B). | |
117 | ||
118 | is_disjoint_neg_pred(b(Expr,_,_),Type,A,B) :- | |
119 | is_disjoint_neg_pred2(Expr,Type,A,B). | |
120 | is_disjoint_neg_pred2(not_equal(X,Y),Type,A,B) :- % detect A /\ B /= {} or {} /= A /\ B | |
121 | ( get_texpr_expr(X,empty_set) -> Inter=Y | |
122 | ; get_texpr_expr(Y,empty_set) -> Inter=X), | |
123 | get_texpr_expr(Inter,intersection(A,B)), get_texpr_type(Inter,Type). | |
124 | is_disjoint_neg_pred2(equal(X,Y),set(Type),A,B) :- get_texpr_type(X,Type), | |
125 | A = b(set_extension([X]),set(Type),_), | |
126 | B = b(set_extension([Y]),set(Type),_). | |
127 | is_disjoint_neg_pred2(negation(NE),Type,A,B) :- | |
128 | is_disjoint_pred(NE,Type,A,B). | |
129 | ||
130 | remove_pair(A,B,In,Out) :- | |
131 | remove_all_infos(A,FA), | |
132 | ? | remove_all_infos(B,FB), |
133 | ? | ( select(distinct(FA,FB),In,Out) |
134 | ? | ; select(distinct(FB,FA),In,Out)),!. |