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)),!.