wd_LocSet_AllFields {
\find ( wd ( allFields ( o )))
\varcond \replacewith ( wd ( o ))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 17 Offset :4wd_LocSet_AllFieldsArr {
\find ( wd ( allFields ( o )))
\varcond \replacewith ( wd ( o )& o != null )
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 31 Offset :4wd_LocSet_AllObjects {
\find ( wd ( allObjects ( f )))
\replacewith ( wd ( f ))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 45 Offset :4wd_LocSet_FreshLocs {
\find ( wd ( freshLocs ( h )))
\replacewith ( wd ( h )& wellFormed ( h ))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 56 Offset :4wd_LocSet_Singleton {
\find ( wd ( singleton ( o , f )))
\varcond \replacewith ( wd ( o )& wd ( f )& o != null )
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 67 Offset :4wd_LocSet_Singleton_Static {
\find ( wd ( singleton ( o , f )))
\varcond \replacewith ( wd ( o )& wd ( f )& o = null )
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 82 Offset :4wd_LocSet_Singleton_Arr {
\find ( wd ( singleton ( o , arr ( i ))))
\varcond \replacewith ( wd ( o )& wd ( i )& o != null & leq ( 0 , i )& lt ( i , length ( o )))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 97 Offset :4wd_LocSet_Singleton_Quant {
\find ( \forall c ; wd ( singleton ( o , f )))
\varcond \replacewith ( \forall c ; ( wd ( o )& wd ( f )))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 111 Offset :4wd_LocSet_Union {
\find ( wd ( union ( l , s )))
\replacewith ( wd ( l )& wd ( s ))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 125 Offset :4wd_LocSet_Intersect {
\find ( wd ( intersect ( l , s )))
\replacewith ( wd ( l )& wd ( s ))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 136 Offset :4wd_LocSet_Diff {
\find ( wd ( setMinus ( l , s )))
\replacewith ( wd ( l )& wd ( s ))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 146 Offset :4wd_LocSet_ArrRange {
\find ( wd ( arrayRange ( o , i , j )))
\varcond \replacewith ( wd ( o )& wd ( i )& wd ( j )& o != null & leq ( 0 , i )& leq ( i , j )& lt ( j , length ( o )))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 157 Offset :4wd_LocSet_AllElemsArr {
\find ( wd ( allElementsOfArray ( h , o , l )))
\varcond \replacewith ( wd ( h )& wd ( o )& wd ( l )& wellFormed ( h )& o != null & boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 171 Offset :4wd_LocSet_AllElemsArrLocsets {
\find ( wd ( allElementsOfArrayLocsets ( h , o , l )))
\varcond \replacewith ( wd ( h )& wd ( o )& wd ( l )& wellFormed ( h )& o != null & boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 186 Offset :4wd_LocSet_InfiniteUnion {
\find ( wd ( infiniteUnion { a ; } ( l )))
\replacewith ( \forall a ; wd ( l ))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 201 Offset :4wd_LocSet_InfiniteUnion2 {
\find ( wd ( infiniteUnion { a , b ; } ( l )))
\replacewith ( \forall a ; ( \forall b ; wd ( l )))
\heuristics (simplify )
\displayname "wd_LocSet_InfiniteUnion"
};defined in: wdLocSetRules.key Line: 212 Offset :4wd_LocSet_Pred_ElementOf {
\find ( WD ( elementOf ( o , f , l )))
\varcond \replacewith ( wd ( o )& wd ( f )& wd ( l )& o != null )
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 224 Offset :4wd_LocSet_Pred_ElementOf_Static {
\find ( WD ( elementOf ( o , f , l )))
\varcond \replacewith ( wd ( o )& wd ( f )& wd ( l )& o = null )
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 238 Offset :4wd_LocSet_Pred_Subset {
\find ( WD ( subset ( l , s )))
\replacewith ( wd ( l )& wd ( s ))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 252 Offset :4wd_LocSet_Pred_Disjoint {
\find ( WD ( disjoint ( l , s )))
\replacewith ( wd ( l )& wd ( s ))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 263 Offset :4wd_LocSet_Pred_InHeap {
\find ( WD ( createdInHeap ( l , h )))
\replacewith ( wd ( l )& wd ( h )& wellFormed ( h ))
\heuristics (simplify )
};defined in: wdLocSetRules.key Line: 273 Offset :4