@@ -163,15 +163,10 @@ class ClassList extends TClassList {
163
163
int firstIndex ( ClassObjectInternal cls ) { result = this .firstIndex ( cls , 0 ) }
164
164
165
165
/* Helper for firstIndex(cls), getting the first index of `cls` where result >= n */
166
- pragma [ noopt]
167
166
private int firstIndex ( ClassObjectInternal cls , int n ) {
168
167
this .getItem ( n ) = cls and result = n
169
168
or
170
- exists ( int next |
171
- result = this .firstIndex ( cls , next ) and
172
- next = n + 1
173
- ) and
174
- exists ( ClassObjectInternal item | item = this .getItem ( n ) | item != cls )
169
+ this .getItem ( n ) != cls and result = this .firstIndex ( cls , n + 1 )
175
170
}
176
171
177
172
/** Holds if the class at `n` is a duplicate of an earlier position. */
@@ -183,15 +178,10 @@ class ClassList extends TClassList {
183
178
* Gets a class list which is the de-duplicated form of the list containing elements of
184
179
* this list from `n` onwards.
185
180
*/
186
- pragma [ noopt]
187
181
ClassList deduplicate ( int n ) {
188
182
n = this .length ( ) and result = Empty ( )
189
183
or
190
- exists ( int next |
191
- this .duplicate ( n ) and
192
- result = this .deduplicate ( next ) and
193
- next = n + 1
194
- )
184
+ this .duplicate ( n ) and result = this .deduplicate ( n + 1 )
195
185
or
196
186
exists ( ClassObjectInternal cls , ClassList tail |
197
187
this .deduplicateCons ( n , cls , tail ) and
@@ -489,12 +479,10 @@ private predicate needs_reversing(ClassList lst) {
489
479
lst = Empty ( )
490
480
}
491
481
492
- pragma [ noopt]
493
482
private predicate reverse_step ( ClassList lst , ClassList remainder , ClassList reversed ) {
494
483
needs_reversing ( lst ) and remainder = lst and reversed = Empty ( )
495
484
or
496
- exists ( ClassObjectInternal head , ClassList tail , TClassList cons |
497
- reverse_step ( lst , cons , tail ) and
485
+ exists ( ClassObjectInternal head , ClassList tail |
498
486
reversed = Cons ( head , tail ) and
499
487
reverse_stepCons ( lst , remainder , head , tail )
500
488
)
0 commit comments