1 % (c) 2017 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 :- module(symmetry_reduction,[get_preliminary_symmetry_reduction_constraint/4,
5 get_post_symmetry_reduction_constraint/5]).
6
7 :- use_module(probsrc(module_information),[module_info/2]).
8 :- module_info(group,synthesis).
9 :- module_info(description,'Symmetry reduction for synthesis').
10
11 :- use_module(library(lists)).
12 :- use_module(library(sets),[subtract/3]).
13 :- use_module(probsrc(bsyntaxtree)).
14
15 % Symmetry reduction when searching for another semantically different program. That means, we are given a solution for the location variables.
16 % The preliminary symmetry reduction is to weak when we are already given a solution, especially to prevent symmetric changes between
17 % equivalent components.
18 get_post_symmetry_reduction_constraint(Components,Solution,LocationVarsIn,LocationVarsOut,SymmetryReduction) :-
19 get_symmetric_components(Components,SymmetricComponents) ,
20 (SymmetricComponents = []
21 -> ! , SymmetryReduction = b(truth,pred,[])
22 ; get_post_symmetry_reduction_constraint_aux(SymmetricComponents,Solution,LocationVarsIn,LocationVarsOut,SymmetryReduction)).
23
24 get_post_symmetry_reduction_constraint_aux(SymmetricComponents,Solution,LocationVarsIn,LocationVarsOut,SymmetryReduction) :-
25 get_single_operator_post_symmetry_reduction(SymmetricComponents,Solution,LocationVarsIn,LocationVarsOut,SingleOperatorReduction) ,
26 get_equivalent_operators_post_symmetry_reduction(Solution,SymmetricComponents,LocationVarsOut,EquivalentOperatorsReduction) ,
27 create_texpr(conjunct(SingleOperatorReduction,EquivalentOperatorsReduction),pred,[],SymmetryReduction).
28
29 get_equivalent_operators_post_symmetry_reduction(Solution,SymmetricComponents,LocationVarsOut,EquivalentOperatorsReduction) :-
30 split_equivalent_components(SymmetricComponents,[],EquivalentComponents) ,
31 maplist(get_equivalent_operators_post_symmetry_reduction_aux(Solution,LocationVarsOut),EquivalentComponents,EquivalentOperatorsReductions) ,
32 conjunct_predicates(EquivalentOperatorsReductions,EquivalentOperatorsReduction).
33
34 get_equivalent_operators_post_symmetry_reduction_aux(Solution,LocationVarsOut,EquivalentComponents,EquivalentOperatorsReductions) :-
35 findall((C1,C2),(member(C1,EquivalentComponents) , member(C2,EquivalentComponents) , C1 \= C2),EquivalentComponentPairs) ,
36 get_equivalent_operators_post_symmetry_reduction_aux2(Solution,LocationVarsOut,EquivalentComponentPairs,EquivalentOperatorsReductions).
37
38 get_equivalent_operators_post_symmetry_reduction_aux2(Solution,LocationVarsOut,[EquivalentComponentPair|T],EquivalentOperatorsReductions) :-
39 get_operators_post_symmetry_reduction_for_pair(EquivalentComponentPair,Solution,LocationVarsOut,PairReduction) ,
40 get_equivalent_operators_post_symmetry_reduction_aux2(Solution,LocationVarsOut,T,PairReduction,EquivalentOperatorsReductions).
41
42 get_equivalent_operators_post_symmetry_reduction_aux2(_,_,[],Acc,Acc).
43 get_equivalent_operators_post_symmetry_reduction_aux2(Solution,LocationVarsOut,[EquivalentComponentPair|T],Acc,EquivalentOperatorsReductions) :-
44 get_operators_post_symmetry_reduction_for_pair(EquivalentComponentPair,Solution,LocationVarsOut,PairReduction) ,
45 create_texpr(conjunct(PairReduction,Acc),pred,[],NewAcc) ,
46 get_equivalent_operators_post_symmetry_reduction_aux2(Solution,LocationVarsOut,T,NewAcc,EquivalentOperatorsReductions).
47
48 get_operators_post_symmetry_reduction_for_pair((ComponentName1,ComponentName2),Solution,LocationVarsOut,PairReduction) :-
49 % get the output location variables that are mapped to left and right input of the component
50 % the components are symmetric and thus have two inputs
51 get_location_var_from_list(ComponentName1,left_input,LocationVarsOut,b(identifier(C1LeftLocationVarName),_,_)) ,
52 get_mapped_output_location(C1LeftLocationVarName,Solution,C1LeftMappedOutputLocationName) ,
53 get_location_var_from_list(ComponentName1,right_input,LocationVarsOut,b(identifier(C1RightLocationVarName),_,_)) ,
54 get_mapped_output_location(C1RightLocationVarName,Solution,C1RightMappedOutputLocationName) ,
55 C1LeftMappedOutputLocationName \= C1RightMappedOutputLocationName , % not the same operator mapped to both locations, otherwise we may loose solutions
56 % create inequality with the input locations of the equivalent symmetric component
57 get_location_var_from_list(ComponentName2,left_input,LocationVarsOut,C2LeftLocationVar) ,
58 get_location_var_from_list(ComponentName2,right_input,LocationVarsOut,C2RightLocationVar) ,
59 create_texpr(not_equal(b(identifier(C1LeftMappedOutputLocationName),integer,[]),C2RightLocationVar),pred,[],C1LOutC2RInReduction) ,
60 create_texpr(not_equal(b(identifier(C1RightMappedOutputLocationName),integer,[]),C2LeftLocationVar),pred,[],C1ROutC2LInReduction) ,
61 create_texpr(conjunct(C1LOutC2RInReduction,C1ROutC2LInReduction),pred,[],PairReduction).
62 get_operators_post_symmetry_reduction_for_pair(_,_,_,b(truth,pred,[])).
63
64 get_single_operator_post_symmetry_reduction([(_,InternalName)|T],Solution,LocationVarsIn,LocationVarsOut,SingleOperatorReductionConj) :-
65 get_single_operator_post_symmetry_reduction_aux(InternalName,Solution,LocationVarsIn,LocationVarsOut,SingleOperatorReduction) ,
66 get_single_operator_post_symmetry_reduction(T,Solution,LocationVarsIn,LocationVarsOut,SingleOperatorReduction,SingleOperatorReductionConj).
67
68 get_single_operator_post_symmetry_reduction([],_,_,_,Acc,Acc).
69 get_single_operator_post_symmetry_reduction([(_,InternalName)|T],Solution,LocationVarsIn,LocationVarsOut,Acc,SingleOperatorReductionConj) :-
70 get_single_operator_post_symmetry_reduction_aux(InternalName,Solution,LocationVarsIn,LocationVarsOut,SingleOperatorReduction) ,
71 create_texpr(conjunct(Acc,SingleOperatorReduction),pred,[],NewAcc) ,
72 get_single_operator_post_symmetry_reduction(T,Solution,LocationVarsIn,LocationVarsOut,NewAcc,SingleOperatorReductionConj).
73
74 % All symmetric components have two inputs. We have to exclude left right and vice versa since we refer to explicit location values, i.e.,
75 % the locations of the mapped outputs.
76 get_single_operator_post_symmetry_reduction_aux(InternalName,Solution,LocationVarsIn,_LocationVarsOut,SingleOperatorReduction) :-
77 get_single_operator_post_symmetry_reduction_aux2(left_input,right_input,InternalName,Solution,LocationVarsIn,LRReduction) ,
78 get_single_operator_post_symmetry_reduction_aux2(right_input,left_input,InternalName,Solution,LocationVarsIn,RLReduction) ,
79 create_texpr(conjunct(LRReduction,RLReduction),pred,[],SingleOperatorReduction).
80
81 get_single_operator_post_symmetry_reduction_aux2(I1,I2,InternalName,Solution,LocationVarsIn,Reduction) :-
82 get_location_var_from_list(InternalName,I1,LocationVarsIn,Input1LocationVar) ,
83 Input1LocationVar = b(identifier(Input1LocationName),_,_) ,
84 get_mapped_output_location(Input1LocationName,Solution,MappedOutputLocationName) ,
85 get_location_var_from_list(InternalName,I2,LocationVarsIn,Input2LocationVar) ,
86 create_texpr(not_equal(b(identifier(MappedOutputLocationName),integer,[]),Input2LocationVar),pred,[],Reduction).
87
88 get_mapped_output_location(InputLocation,Solution,OutputLocation) :-
89 member(binding(InputLocation,_,InputLocationValue),Solution) ,
90 get_mapped_output_location_by_value(InputLocationValue,Solution,OutputLocation).
91
92 get_mapped_output_location_by_value(InputLocationValue,Solution,OutputLocation) :-
93 member(binding(OutputLocation,_,InputLocationValue),Solution) ,
94 (atom_concat(lo,_,OutputLocation) ; atom_concat(linput,_,OutputLocation)).
95
96 % Exclude symmetric changes.
97 % These are the restrictions we can make without a given previous solution for the location variables.
98 % Components are tuples of raw component name and internal component name like (add,add1).
99 get_preliminary_symmetry_reduction_constraint(Components,LocationVarsIn,LocationVarsOut,SymmetryReduction) :-
100 get_symmetric_components(Components,SymmetricComponents) ,
101 maplist(get_single_operand_symmetry_reduction(LocationVarsIn),SymmetricComponents,OperandExclusionList) ,
102 get_operator_symmetry_reduction(Components,LocationVarsOut,OperatorReductionPredicate) ,
103 conjunct_predicates([OperatorReductionPredicate|OperandExclusionList],SymmetryReduction).
104
105 get_symmetric_components(Components,SymmetricComponents) :-
106 get_symmetric_components(Components,[],SymmetricComponents).
107
108 get_symmetric_components([],Acc,Acc).
109 get_symmetric_components([(Name,InternalName)|T],Acc,SymmetricComponents) :-
110 Name \= constant-_ ,
111 is_symmetric(Name) ,
112 get_symmetric_components(T,[(Name,InternalName)|Acc],SymmetricComponents).
113 get_symmetric_components([_|T],Acc,SymmetricComponents) :-
114 get_symmetric_components(T,Acc,SymmetricComponents).
115
116 % Exclude symmetric changes within a component by asserting L(i1) < L(i2).
117 get_single_operand_symmetry_reduction(LocationVarsIn,Expression,SymmetryReduction) :-
118 Expression = (_,InternalName) ,
119 get_location_var_from_list(InternalName,left_input,LocationVarsIn,LeftLocationVarIn) ,
120 get_location_var_from_list(InternalName,right_input,LocationVarsIn,RightLocationVarIn) ,
121 SymmetryReduction = b(less_equal(LeftLocationVarIn,RightLocationVarIn),pred,[]).
122
123 % Exclude symmetric changes of operands (components). E.g., given three additions add1,add2,add3 we assert
124 % L(add1) < L(add2) < L(add3) to hold, where L(add_) is the corresponding output location of the component.
125 get_operator_symmetry_reduction(Components,LocationVarsOut,SymmetryReduction) :-
126 split_equivalent_components(Components,[],EquivalentComponents) ,
127 maplist(get_operator_symmetry_reduction_aux(LocationVarsOut,[]),EquivalentComponents,SymmetryExclusionList) ,
128 conjunct_predicates(SymmetryExclusionList,SymmetryReduction).
129
130 get_operator_symmetry_reduction_aux(_,Acc,[],SymmetryReduction) :-
131 conjunct_predicates(Acc,SymmetryReduction).
132 get_operator_symmetry_reduction_aux(LocationVarsOut,Acc,[Components|T],SymmetryReduction) :-
133 % skip single components
134 length(Components,Length) ,
135 Length > 1 , !,
136 get_operator_symmetry_reduction_aux2(Components,LocationVarsOut,[],OperatorReduction) ,
137 get_operator_symmetry_reduction_aux(LocationVarsOut,[OperatorReduction|Acc],T,SymmetryReduction).
138 get_operator_symmetry_reduction_aux(LocationVarsOut,Acc,[_|T],SymmetryReduction) :-
139 get_operator_symmetry_reduction_aux(LocationVarsOut,Acc,T,SymmetryReduction).
140
141 % Components are all equivalent like [add1,add2,add3] and the list has a minimum length of 2.
142 % For just one component we don't need symmetry reduction on the level of operators.
143 get_operator_symmetry_reduction_aux2([_],_,Acc,OperatorReduction) :-
144 conjunct_predicates(Acc,OperatorReduction).
145 get_operator_symmetry_reduction_aux2([(_,InternalName1),(Name,InternalName2)|T],LocationVarsOut,Acc,OperatorReduction) :-
146 get_location_var_from_list(InternalName1,output,LocationVarsOut,LocationVarOutComp1) ,
147 get_location_var_from_list(InternalName2,output,LocationVarsOut,LocationVarOutComp2) ,
148 NewAcc = [b(less_equal(LocationVarOutComp1,LocationVarOutComp2),pred,[])|Acc] ,
149 get_operator_symmetry_reduction_aux2([(Name,InternalName2)|T],LocationVarsOut,NewAcc,OperatorReduction).
150
151 % Find all equivalent components like [add1,add2,add3].
152 split_equivalent_components([],Acc,Acc).
153 split_equivalent_components([(Name,InternalName)|T],Acc,EquivalentComponentsList) :-
154 Name \= constant-_ ,
155 findall(EquiInternalName,(member((_,EquiInternalName),T) , EquiInternalName = InternalName),EquivalentComponents) ,
156 subtract(T,EquivalentComponents,NT) ,
157 split_equivalent_components(NT,[(Name,InternalName)|Acc],EquivalentComponentsList).
158 split_equivalent_components([_|T],Acc,EquivalentComponentsList) :-
159 split_equivalent_components(T,Acc,EquivalentComponentsList).
160
161 % Search a location variable for a given tuple of component name and internal name (like add1)
162 % and a component type (i.e., one of [left_input, right_input, output]).
163 get_location_var_from_list(InternalName,ComponentType,LocationVars,LocationVar) :-
164 member(LocationVar,LocationVars) ,
165 get_texpr_info(LocationVar,Info) ,
166 member(synthesis(InternalName,ComponentType),Info).
167
168 is_symmetric(not_equal).
169 is_symmetric(equal).
170 is_symmetric(conjunct).
171 is_symmetric(disjunct).
172 is_symmetric(equivalence).
173 is_symmetric(add).
174 is_symmetric(multiplication).
175 is_symmetric(union).
176 is_symmetric(intersection).