@@ -30,16 +30,16 @@ predicate hasTupleCount(
3030 float tupleCount
3131) {
3232 inLayer = firstPredicate ( recursive ) and
33- exists ( PipeLineRun run | run = inLayer .getPipelineRuns ( ) .getRun ( iteration ) |
34- ordering = run .getRAReference ( ) and
33+ exists ( PipeLineRun run |
34+ run = inLayer .getPipelineRuns ( ) .getRun ( iteration ) and ordering = run .getRAReference ( )
35+ |
3536 tupleCount = run .getCount ( i )
36- )
37- or
38- exists ( SummaryEvent inLayer0 , float tupleCount0 , PipeLineRun run |
39- run = inLayer .getPipelineRuns ( ) .getRun ( pragma [ only_bind_into ] ( iteration ) ) and
40- successor ( recursive , inLayer0 , inLayer ) and
41- hasTupleCount ( recursive , ordering , inLayer0 , pragma [ only_bind_into ] ( iteration ) , i , tupleCount0 ) and
42- tupleCount = run .getCount ( i ) + tupleCount0
37+ or
38+ exists ( SummaryEvent inLayer0 , float tupleCount0 |
39+ successor ( recursive , inLayer0 , inLayer ) and
40+ hasTupleCount ( recursive , ordering , inLayer0 , pragma [ only_bind_into ] ( iteration ) , i , tupleCount0 ) and
41+ tupleCount = run .getCount ( i ) + tupleCount0
42+ )
4343 )
4444}
4545
@@ -58,57 +58,51 @@ predicate hasDuplication(
5858 ComputeRecursive recursive , string ordering , SummaryEvent inLayer , int iteration , int i ,
5959 float duplication
6060) {
61- inLayer = firstPredicate ( recursive ) and
62- exists ( PipeLineRun run | run = inLayer .getPipelineRuns ( ) .getRun ( iteration ) |
63- ordering = run .getRAReference ( ) and
61+ exists ( PipeLineRun run |
62+ run = inLayer .getPipelineRuns ( ) .getRun ( iteration ) and
63+ ordering = run .getRAReference ( )
64+ |
65+ inLayer = firstPredicate ( recursive ) and
6466 duplication = run .getDuplicationPercentage ( i )
65- )
66- or
67- exists ( SummaryEvent inLayer0 , float duplication0 , PipeLineRun run |
68- run = inLayer . getPipelineRuns ( ) . getRun ( pragma [ only_bind_into ] ( iteration ) ) and
69- successor ( recursive , inLayer0 , inLayer ) and
70- hasDuplication ( recursive , ordering , inLayer0 , pragma [ only_bind_into ] ( iteration ) , i , duplication0 ) and
71- duplication = run . getDuplicationPercentage ( i ) . maximum ( duplication0 )
67+ or
68+ exists ( SummaryEvent inLayer0 , float duplication0 |
69+ successor ( recursive , inLayer0 , inLayer ) and
70+ hasDuplication ( recursive , ordering , inLayer0 , pragma [ only_bind_into ] ( iteration ) , i ,
71+ duplication0 ) and
72+ duplication = run . getDuplicationPercentage ( i ) . maximum ( duplication0 )
73+ )
7274 )
7375}
7476
7577predicate hasDuplication ( ComputeRecursive recursive , string ordering , int i , float duplication ) {
7678 duplication =
77- max ( SummaryEvent inLayer , int iteration , int dup |
78- inLayer = getInLayerOrRecursive ( recursive ) and
79- hasDuplication ( recursive , ordering , inLayer , iteration , i , dup )
80- |
81- dup
82- )
79+ max ( int iteration , int dup | hasDuplication ( recursive , ordering , _, iteration , i , dup ) | dup )
8380}
8481
8582/**
8683 * Holds if the ordering `ordering` has `resultSize` resultSize in the `iteration`'th iteration.
87- *
88- * For example, the "base" ordering in iteration 0 has size 42.
8984 */
9085private predicate hasResultSize (
9186 ComputeRecursive recursive , string ordering , SummaryEvent inLayer , int iteration , float resultSize
9287) {
93- inLayer = firstPredicate ( recursive ) and
94- ordering = inLayer .getPipelineRuns ( ) .getRun ( iteration ) .getRAReference ( ) and
95- resultSize = inLayer .getDeltaSize ( iteration )
96- or
97- exists ( SummaryEvent inLayer0 , int resultSize0 |
98- successor ( recursive , inLayer0 , inLayer ) and
99- hasResultSize ( recursive , ordering , inLayer0 , iteration , resultSize0 ) and
100- resultSize = inLayer .getDeltaSize ( iteration ) + resultSize0
88+ exists ( PipeLineRun run |
89+ run = inLayer .getPipelineRuns ( ) .getRun ( iteration ) and
90+ ordering = run .getRAReference ( )
91+ |
92+ inLayer = firstPredicate ( recursive ) and
93+ resultSize = inLayer .getDeltaSize ( iteration )
94+ or
95+ exists ( SummaryEvent inLayer0 , int resultSize0 |
96+ successor ( recursive , inLayer0 , inLayer ) and
97+ hasResultSize ( recursive , ordering , inLayer0 , iteration , resultSize0 ) and
98+ resultSize = inLayer .getDeltaSize ( iteration ) + resultSize0
99+ )
101100 )
102101}
103102
104103predicate hasResultSize ( ComputeRecursive recursive , string ordering , float resultSize ) {
105104 resultSize =
106- strictsum ( InLayer inLayer , int iteration , float r |
107- inLayer .getComputeRecursiveEvent ( ) = recursive and
108- hasResultSize ( recursive , ordering , inLayer , iteration , r )
109- |
110- r
111- )
105+ strictsum ( int iteration , float r | hasResultSize ( recursive , ordering , _, iteration , r ) | r )
112106}
113107
114108RAParser< PipeLine > :: RAExpr getAnRaOperation ( SummaryEvent inLayer , string ordering ) {
@@ -122,17 +116,20 @@ SummaryEvent getInLayerEventWithName(ComputeRecursive recursive, string predicat
122116
123117bindingset [ predicateName, iteration]
124118int getSize ( ComputeRecursive recursive , string predicateName , int iteration , TDeltaKind kind ) {
125- exists ( int i |
119+ exists ( int i , SummaryEvent event |
126120 kind = TPrevious ( ) and
127121 i = iteration - 1
128122 or
129123 kind = TCurrent ( ) and
130124 i = iteration
131125 |
132- result = getInLayerEventWithName ( recursive , predicateName ) .getDeltaSize ( i )
133- or
134- not exists ( getInLayerEventWithName ( recursive , predicateName ) .getDeltaSize ( i ) ) and
135- result = 0
126+ event = getInLayerEventWithName ( recursive , predicateName ) and
127+ (
128+ result = event .getDeltaSize ( i )
129+ or
130+ not exists ( event .getDeltaSize ( i ) ) and
131+ result = 0
132+ )
136133 )
137134}
138135
@@ -154,36 +151,53 @@ private predicate isDelta(string predicateName, TDeltaKind kind, string withoutS
154151 withoutSuffix = predicateName .regexpCapture ( "(.+)#cur_delta" , 1 )
155152}
156153
154+ bindingset [ iteration]
155+ float getRecursiveDependencySize (
156+ ComputeRecursive recursive , string predicateName , int iteration , SummaryEvent inLayer ,
157+ string ordering , TDeltaKind kind
158+ ) {
159+ result = getSize ( recursive , predicateName , iteration , kind ) and
160+ isDelta ( getAnRaOperation ( inLayer , ordering ) .getARhsPredicate ( ) , kind , predicateName )
161+ }
162+
163+ bindingset [ ordering, iteration]
164+ predicate hasDependentPredicateSizeImpl (
165+ ComputeRecursive recursive , string ordering , float size , string predicateName , int iteration ,
166+ SummaryEvent inLayer
167+ ) {
168+ // We treat the base case as a non-recursive case
169+ if ordering = "base"
170+ then
171+ size =
172+ [
173+ getDependencyWithName ( recursive .getDependencies ( ) , predicateName ) .getResultSize ( ) ,
174+ getRecursiveDependencySize ( recursive , predicateName , iteration , inLayer , ordering ,
175+ TCurrent ( ) )
176+ ]
177+ else
178+ size =
179+ getRecursiveDependencySize ( recursive , predicateName , iteration , inLayer , ordering , TPrevious ( ) )
180+ }
181+
182+ pragma [ nomagic]
157183predicate hasDependentPredicateSize (
158184 ComputeRecursive recursive , string ordering , SummaryEvent inLayer , int iteration ,
159185 string predicateName , float size
160186) {
161- exists ( |
162- inLayer = firstPredicate ( recursive ) and
163- ordering = inLayer .getPipelineRuns ( ) .getRun ( iteration ) .getRAReference ( )
164- |
165- // We treat iteration 0 as a non-recursive case
166- if ordering = "base"
167- then size = getDependencyWithName ( recursive .getDependencies ( ) , predicateName ) .getResultSize ( )
168- else
169- exists ( TDeltaKind kind |
170- size = getSize ( recursive , predicateName , iteration , kind ) and
171- isDelta ( getAnRaOperation ( inLayer , ordering ) .getARhsPredicate ( ) , kind , predicateName )
172- )
173- )
174- or
175- exists ( SummaryEvent inLayer0 , float size0 |
176- successor ( recursive , inLayer0 , inLayer ) and
177- hasDependentPredicateSize ( recursive , ordering , inLayer0 , iteration , predicateName , size0 )
187+ exists ( PipeLineRun run |
188+ run = inLayer .getPipelineRuns ( ) .getRun ( pragma [ only_bind_into ] ( iteration ) ) and
189+ ordering = run .getRAReference ( )
178190 |
179- // We treat iteration 0 as a non-recursive case
180- if ordering = "base"
181- then size = getDependencyWithName ( recursive .getDependencies ( ) , predicateName ) .getResultSize ( )
182- else
183- exists ( TDeltaKind kind |
184- size = getSize ( recursive , predicateName , iteration , kind ) + size0 and
185- isDelta ( getAnRaOperation ( inLayer , ordering ) .getARhsPredicate ( ) , kind , predicateName )
186- )
191+ inLayer = firstPredicate ( recursive ) and
192+ hasDependentPredicateSizeImpl ( recursive , ordering , size , predicateName , iteration , inLayer )
193+ or
194+ exists ( SummaryEvent inLayer0 , float size0 , float size1 |
195+ successor ( recursive , inLayer0 , inLayer ) and
196+ hasDependentPredicateSize ( recursive , ordering , inLayer0 , pragma [ only_bind_into ] ( iteration ) ,
197+ predicateName , size0 ) and
198+ hasDependentPredicateSizeImpl ( recursive , ordering , size1 , predicateName , iteration , inLayer ) and
199+ size = size0 + size1
200+ )
187201 )
188202}
189203
@@ -195,9 +209,8 @@ predicate hasDependentPredicateSize(
195209 ComputeRecursive recursive , string ordering , string predicateName , float size
196210) {
197211 size =
198- strictsum ( SummaryEvent inLayer , int iteration , int s |
199- inLayer = getInLayerOrRecursive ( recursive ) and
200- hasDependentPredicateSize ( recursive , ordering , inLayer , iteration , predicateName , s )
212+ strictsum ( int iteration , float s |
213+ hasDependentPredicateSize ( recursive , ordering , _, iteration , predicateName , s )
201214 |
202215 s
203216 )
0 commit comments