elementOfEmpty {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( elementOf ( o , f , empty ))
\replacewith ( false )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 14 Offset :4elementOfAllLocs {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( elementOf ( o , f , allLocs ))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 25 Offset :4elementOfSingleton {
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f , f2 ;
\find ( elementOf ( o , f , singleton ( o2 , f2 )))
\replacewith ( o = o2 & f = f2 )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 36 Offset :4elementOfUnion {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term LocSet s , s2 ;
\find ( elementOf ( o , f , union ( s , s2 )))
\replacewith ( elementOf ( o , f , s )| elementOf ( o , f , s2 ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 47 Offset :4elementOfIntersect {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term LocSet s , s2 ;
\find ( elementOf ( o , f , intersect ( s , s2 )))
\replacewith ( elementOf ( o , f , s )& elementOf ( o , f , s2 ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 59 Offset :4elementOfSetMinus {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term LocSet s , s2 ;
\find ( elementOf ( o , f , setMinus ( s , s2 )))
\replacewith ( elementOf ( o , f , s )& ! elementOf ( o , f , s2 ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 71 Offset :4elementOfInfiniteUnion {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \variables alpha av ;
\schemaVar \term LocSet s ;
\find ( elementOf ( o , f , infiniteUnion { av ; } ( s )))
\varcond \replacewith ( \exists av ; elementOf ( o , f , s ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 83 Offset :4elementOfInfiniteUnion2Vars {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \variables alpha av ;
\schemaVar \variables beta bv ;
\schemaVar \term LocSet s ;
\find ( elementOf ( o , f , infiniteUnion { av , bv ; } ( s )))
\varcond \replacewith ( \exists av ; \exists bv ; elementOf ( o , f , s ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 97 Offset :4elementOfAllFields {
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f ;
\find ( elementOf ( o , f , allFields ( o2 )))
\replacewith ( o = o2 )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 112 Offset :4allFieldsEq {
\schemaVar \term Object o1 , o2 ;
\find ( allFields ( o1 )= allFields ( o2 ))
\replacewith ( o1 = o2 )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 123 Offset :4elementOfAllObjects {
\schemaVar \term Object o ;
\schemaVar \term Field f , f2 ;
\find ( elementOf ( o , f , allObjects ( f2 )))
\replacewith ( f = f2 )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 130 Offset :4elementOfArrayRange {
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f ;
\schemaVar \term int lower , upper ;
\schemaVar \variables int iv ;
\find ( elementOf ( o , f , arrayRange ( o2 , lower , upper )))
\varcond \replacewith ( o = o2 & \exists iv ; ( f = arr ( iv )& lower <= iv & iv <= upper ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 142 Offset :4elementOfArrayRangeConcrete {
\schemaVar \term Object o , o2 ;
\schemaVar \term int idx , lower , upper ;
\find ( elementOf ( o , arr ( idx ), arrayRange ( o2 , lower , upper )))
\replacewith ( o = o2 & lower <= idx & idx <= upper )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 157 Offset :4elementOfFreshLocs {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\find ( elementOf ( o , f , freshLocs ( h )))
\replacewith ( o != null & ! boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 168 Offset :4elementOfUnionEQ {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term LocSet s , s2 ;
\schemaVar \term LocSet EQ ;
\assumes ( union ( s , s2 )= EQ ==> )
\find ( elementOf ( o , f , EQ ))
\sameUpdateLevel
\replacewith ( elementOf ( o , f , s )| elementOf ( o , f , s2 ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 183 Offset :4elementOfIntersectEQ {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term LocSet s , s2 ;
\schemaVar \term LocSet EQ ;
\assumes ( intersect ( s , s2 )= EQ ==> )
\find ( elementOf ( o , f , EQ ))
\sameUpdateLevel
\replacewith ( elementOf ( o , f , s )& elementOf ( o , f , s2 ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 198 Offset :4elementOfSetMinusEQ {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term LocSet s , s2 ;
\schemaVar \term LocSet EQ ;
\assumes ( setMinus ( s , s2 )= EQ ==> )
\find ( elementOf ( o , f , EQ ))
\sameUpdateLevel
\replacewith ( elementOf ( o , f , s )& ! elementOf ( o , f , s2 ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 213 Offset :4elementOfInfiniteUnionEQ {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \variables alpha av ;
\schemaVar \term LocSet s ;
\schemaVar \term LocSet EQ ;
\assumes ( infiniteUnion { av ; } ( s )= EQ ==> )
\find ( elementOf ( o , f , EQ ))
\sameUpdateLevel
\varcond \replacewith ( \exists av ; elementOf ( o , f , s ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 228 Offset :4elementOfInfiniteUnion2VarsEQ {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \variables alpha av ;
\schemaVar \variables beta bv ;
\schemaVar \term LocSet s ;
\schemaVar \term LocSet EQ ;
\assumes ( infiniteUnion { av , bv ; } ( s )= EQ ==> )
\find ( elementOf ( o , f , EQ ))
\sameUpdateLevel
\varcond \replacewith ( \exists av ; \exists bv ; elementOf ( o , f , s ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 245 Offset :4elementOfArrayRangeEQ {
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f ;
\schemaVar \term int lower , upper ;
\schemaVar \variables int iv ;
\schemaVar \term LocSet EQ ;
\assumes ( arrayRange ( o2 , lower , upper )= EQ ==> )
\find ( elementOf ( o , f , EQ ))
\sameUpdateLevel
\varcond \replacewith ( o = o2 & \exists iv ; ( f = arr ( iv )& lower <= iv & iv <= upper ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 263 Offset :4equalityToElementOf {
\schemaVar \term LocSet s , s2 ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\find ( s = s2 )
\varcond \replacewith ( \forall ov ; \forall fv ; ( elementOf ( ov , fv , s )<-> elementOf ( ov , fv , s2 )))
\heuristics (semantics_blasting )
};defined in: locSetsRules.key Line: 284 Offset :4equalityToElementOfRight {
\schemaVar \term LocSet s , s2 ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\find ( ==> s = s2 )
\varcond \replacewith ( ==> \forall ov ; \forall fv ; ( elementOf ( ov , fv , s )<-> elementOf ( ov , fv , s2 )))
\heuristics (setEqualityBlastingRight )
};defined in: locSetsRules.key Line: 298 Offset :4emptyEqualsSingleton {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( empty = singleton ( o , f ))
\replacewith ( false )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 311 Offset :4singletonEqualsEmpty {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( singleton ( o , f )= empty )
\replacewith ( false )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 322 Offset :4unionWithSingletonEqualsUnionWithSingleton {
\schemaVar \term LocSet s1 , s2 ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( union ( s1 , singleton ( o , f ))= union ( s2 , singleton ( o , f )))
\replacewith ( setMinus ( s1 , singleton ( o , f ))= setMinus ( s2 , singleton ( o , f )))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 332 Offset :4unionWithSingletonEqualsUnionWithSingleton_2 {
\schemaVar \term LocSet s1 , s2 ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( union ( singleton ( o , f ), s1 )= union ( singleton ( o , f ), s2 ))
\replacewith ( setMinus ( s1 , singleton ( o , f ))= setMinus ( s2 , singleton ( o , f )))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 344 Offset :4subsetToElementOf {
\schemaVar \term LocSet s , s2 ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\find ( subset ( s , s2 ))
\varcond \replacewith ( \forall ov ; \forall fv ; ( elementOf ( ov , fv , s )-> elementOf ( ov , fv , s2 )))
\heuristics (semantics_blasting )
};defined in: locSetsRules.key Line: 356 Offset :4subsetToElementOfRight {
\schemaVar \term LocSet s , s2 ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\find ( ==> subset ( s , s2 ))
\varcond \replacewith ( ==> \forall ov ; \forall fv ; ( elementOf ( ov , fv , s )-> elementOf ( ov , fv , s2 )))
\heuristics (setEqualityBlastingRight )
};defined in: locSetsRules.key Line: 370 Offset :4elementOfSubsetImpliesElementOfSuperset {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( subset ( s , s2 )==> )
\find ( elementOf ( o , f , s )==> )
\add ( elementOf ( o , f , s2 )==> )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 384 Offset :4noElementOfSupersetImpliesNoElementOfSubset {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( subset ( s , s2 )==> )
\find ( ==> elementOf ( o , f , s2 ))
\add ( ==> elementOf ( o , f , s ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 399 Offset :4subsetSingletonLeft {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( subset ( singleton ( o , f ), s ))
\replacewith ( elementOf ( o , f , s ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 412 Offset :4subsetSingletonLeftEQ {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term LocSet EQ ;
\assumes ( singleton ( o , f )= EQ ==> )
\find ( subset ( EQ , s ))
\sameUpdateLevel
\replacewith ( elementOf ( o , f , s ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 425 Offset :4subsetSingletonRight {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( subset ( s , singleton ( o , f )))
\replacewith ( s = empty | s = singleton ( o , f ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 441 Offset :4subsetSingletonRightEQ {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term LocSet EQ ;
\assumes ( singleton ( o , f )= EQ ==> )
\find ( subset ( s , EQ ))
\sameUpdateLevel
\replacewith ( s = empty | s = singleton ( o , f ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 454 Offset :4subsetUnionLeft {
\schemaVar \term LocSet s , s2 , s3 ;
\find ( subset ( union ( s , s2 ), s3 ))
\replacewith ( subset ( s , s3 )& subset ( s2 , s3 ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 470 Offset :4subsetUnionLeftEQ {
\schemaVar \term LocSet s , s2 , s3 ;
\schemaVar \term LocSet EQ ;
\assumes ( union ( s , s2 )= EQ ==> )
\find ( subset ( EQ , s3 ))
\sameUpdateLevel
\replacewith ( subset ( s , s3 )& subset ( s2 , s3 ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 481 Offset :4subsetOfUnionWithItSelf1 {
\schemaVar \term LocSet s , s2 ;
\find ( subset ( s , union ( s , s2 )))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 495 Offset :4subsetOfUnionWithItSelfEQ1 {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term LocSet EQ ;
\assumes ( union ( s , s2 )= EQ ==> )
\find ( subset ( s , EQ ))
\sameUpdateLevel
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 506 Offset :4subsetOfUnionWithItSelf2 {
\schemaVar \term LocSet s , s2 ;
\find ( subset ( s , union ( s2 , s )))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 520 Offset :4subsetOfUnionWithItSelfEQ2 {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term LocSet EQ ;
\assumes ( union ( s2 , s )= EQ ==> )
\find ( subset ( s , EQ ))
\sameUpdateLevel
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 531 Offset :4subsetOfIntersectWithItSelf1 {
\schemaVar \term LocSet s , s2 ;
\find ( subset ( s , intersect ( s , s2 )))
\replacewith ( subset ( s , s2 ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 545 Offset :4subsetOfIntersectWithItSelfEQ1 {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term LocSet EQ ;
\assumes ( intersect ( s , s2 )= EQ ==> )
\find ( subset ( s , EQ ))
\sameUpdateLevel
\replacewith ( subset ( s , s2 ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 556 Offset :4subsetOfIntersectWithItSelf2 {
\schemaVar \term LocSet s , s2 ;
\find ( subset ( s , intersect ( s2 , s )))
\replacewith ( subset ( s , s2 ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 570 Offset :4subsetOfIntersectWithItSelfEQ2 {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term LocSet EQ ;
\assumes ( intersect ( s2 , s )= EQ ==> )
\find ( subset ( s , EQ ))
\sameUpdateLevel
\replacewith ( subset ( s , s2 ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 581 Offset :4allFieldsSubsetOf {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( subset ( allFields ( o ), s )==> )
\find ( elementOf ( o , f , s ))
\sameUpdateLevel
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 595 Offset :4elementOfSubsetOfUnion1 {
\schemaVar \term LocSet s , s2 , s3 ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\assumes ( subset ( s , union ( s2 , s3 )), ==> elementOf ( o , f , s2 ))
\find ( elementOf ( o , f , s ))
\sameUpdateLevel
\add ( elementOf ( o , f , s )<-> elementOf ( o , f , intersect ( s , s3 ))==> )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 610 Offset :4elementOfSubsetOfUnion2 {
\schemaVar \term LocSet s , s2 , s3 ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\assumes ( subset ( s , union ( s2 , s3 )), ==> elementOf ( o , f , s3 ))
\find ( elementOf ( o , f , s ))
\sameUpdateLevel
\add ( elementOf ( o , f , s )<-> elementOf ( o , f , intersect ( s , s2 ))==> )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 627 Offset :4disjointToElementOf {
\schemaVar \term LocSet s , s2 ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\find ( disjoint ( s , s2 ))
\varcond \replacewith ( \forall ov ; \forall fv ; ( ! elementOf ( ov , fv , s )| ! elementOf ( ov , fv , s2 )))
\heuristics (semantics_blasting )
};defined in: locSetsRules.key Line: 643 Offset :4disjointDefinition {
\schemaVar \term LocSet s , s2 ;
\find ( disjoint ( s , s2 ))
\replacewith ( intersect ( s , s2 )= empty )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 657 Offset :4disjointNotInOtherLocset1 {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( intersect ( s , s2 )= empty ==> )
\find ( elementOf ( o , f , s )==> )
\add ( ==> elementOf ( o , f , s2 ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 668 Offset :4disjointNotInOtherLocset2 {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( intersect ( s , s2 )= empty ==> )
\find ( elementOf ( o , f , s2 )==> )
\add ( ==> elementOf ( o , f , s ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 682 Offset :4disjointAndSubset1 {
\schemaVar \term LocSet s , s2 , s3 ;
\assumes ( intersect ( s2 , s3 )= empty ==> )
\find ( subset ( s , s2 )==> )
\add ( intersect ( s , s3 )= empty ==> )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 696 Offset :4disjointAndSubset2 {
\schemaVar \term LocSet s , s2 , s3 ;
\assumes ( intersect ( s2 , s3 )= empty ==> )
\find ( subset ( s , s3 )==> )
\add ( intersect ( s , s2 )= empty ==> )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 708 Offset :4disjointAllFields {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( intersect ( allFields ( o ), s )= empty ==> )
\find ( elementOf ( o , f , s ))
\sameUpdateLevel
\replacewith ( false )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 720 Offset :4disjointAllFields_2 {
\schemaVar \term Object o , o2 ;
\schemaVar \term Field f ;
\find ( intersect ( allFields ( o ), allFields ( o2 ))= empty )
\replacewith ( o != o2 )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 735 Offset :4disjointAllObjects {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( intersect ( allObjects ( f ), s )= empty ==> )
\find ( elementOf ( o , f , s ))
\sameUpdateLevel
\replacewith ( false )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 747 Offset :4disjointInfiniteUnion {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \variables int iv ;
\find ( intersect ( infiniteUnion { iv ; } ( s2 ), s )= empty )
\varcond \replacewith ( \forall iv ; ( intersect ( s2 , s )= empty ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 762 Offset :4disjointInfiniteUnion_2 {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \variables int iv ;
\find ( intersect ( s , infiniteUnion { iv ; } ( s2 ))= empty )
\varcond \replacewith ( \forall iv ; ( intersect ( s , s2 )= empty ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 777 Offset :4intersectAllFieldsFreshLocs {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\find ( intersect ( allFields ( o ), freshLocs ( h ))= empty )
\replacewith ( o = null | boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 792 Offset :4disjointAndSubset_3 {
\schemaVar \term LocSet s1 , s2 , s3 , s4 ;
\assumes ( intersect ( s1 , s2 )= empty ==> )
\find ( subset ( s4 , union ( s2 , s3 ))==> )
\add ( intersect ( s1 , s3 )= empty -> intersect ( s1 , s4 )= empty ==> )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 803 Offset :4disjointAndSubset_4 {
\schemaVar \term LocSet s1 , s2 , s3 , s4 ;
\assumes ( intersect ( s1 , s2 )= empty ==> )
\find ( subset ( s4 , union ( s3 , s2 ))==> )
\add ( intersect ( s1 , s3 )= empty -> intersect ( s1 , s4 )= empty ==> )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 813 Offset :4disjointAndSubset_5 {
\schemaVar \term LocSet s1 , s2 , s3 , s4 ;
\assumes ( intersect ( s2 , s1 )= empty ==> )
\find ( subset ( s4 , union ( s2 , s3 ))==> )
\add ( intersect ( s1 , s3 )= empty -> intersect ( s1 , s4 )= empty ==> )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 823 Offset :4disjointAndSubset_6 {
\schemaVar \term LocSet s1 , s2 , s3 , s4 ;
\assumes ( intersect ( s2 , s1 )= empty ==> )
\find ( subset ( s4 , union ( s3 , s2 ))==> )
\add ( intersect ( s1 , s3 )= empty -> intersect ( s1 , s4 )= empty ==> )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 833 Offset :4createdInHeapToElementOf {
\schemaVar \term LocSet s ;
\schemaVar \term Heap h ;
\schemaVar \variables Object ov ;
\schemaVar \variables Field fv ;
\find ( createdInHeap ( s , h ))
\varcond \replacewith ( \forall ov ; \forall fv ; ( elementOf ( ov , fv , s )-> ov = null | boolean :: select ( h , ov , java.lang.Object :: )= TRUE ))
\heuristics (classAxiom )
};defined in: locSetsRules.key Line: 842 Offset :4unionWithEmpty {
\schemaVar \term LocSet s ;
\find ( union ( empty , s ))
\replacewith ( s )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 861 Offset :4unionWithAllLocs {
\schemaVar \term LocSet s ;
\find ( union ( allLocs , s ))
\replacewith ( allLocs )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 871 Offset :4intersectWithEmpty {
\schemaVar \term LocSet s ;
\find ( intersect ( empty , s ))
\replacewith ( empty )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 881 Offset :4intersectWithAllLocs {
\schemaVar \term LocSet s ;
\find ( intersect ( allLocs , s ))
\replacewith ( s )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 891 Offset :4unionWithEmptyRight {
\schemaVar \term LocSet s ;
\find ( union ( s , empty ))
\replacewith ( s )
\heuristics (concrete )
\displayname "unionWithEmpty"
};defined in: locSetsRules.key Line: 906 Offset :4unionWithAllLocsRight {
\schemaVar \term LocSet s ;
\find ( union ( s , allLocs ))
\replacewith ( allLocs )
\heuristics (concrete )
\displayname "unionWithAllLocs"
};defined in: locSetsRules.key Line: 917 Offset :4intersectWithEmptyRight {
\schemaVar \term LocSet s ;
\find ( intersect ( s , empty ))
\replacewith ( empty )
\heuristics (concrete )
\displayname "intersectWithEmpty"
};defined in: locSetsRules.key Line: 928 Offset :4intersectWithAllLocsRight {
\schemaVar \term LocSet s ;
\find ( intersect ( s , allLocs ))
\replacewith ( s )
\heuristics (concrete )
\displayname "intersectWithAllLocs"
};defined in: locSetsRules.key Line: 939 Offset :4setMinusWithEmpty1 {
\schemaVar \term LocSet s ;
\find ( setMinus ( s , empty ))
\replacewith ( s )
\heuristics (concrete )
\displayname "setMinusWithEmpty"
};defined in: locSetsRules.key Line: 953 Offset :4setMinusWithEmpty2 {
\schemaVar \term LocSet s ;
\find ( setMinus ( empty , s ))
\replacewith ( empty )
\heuristics (concrete )
\displayname "setMinusWithEmpty"
};defined in: locSetsRules.key Line: 964 Offset :4setMinusWithAllLocs {
\schemaVar \term LocSet s ;
\find ( setMinus ( s , allLocs ))
\replacewith ( empty )
\heuristics (concrete )
\displayname "setMinusWithAllLocs"
};defined in: locSetsRules.key Line: 975 Offset :4subsetWithEmpty {
\schemaVar \term LocSet s ;
\find ( subset ( empty , s ))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 990 Offset :4subsetOfEmpty {
\schemaVar \term LocSet s ;
\find ( subset ( s , empty ))
\replacewith ( s = empty )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1000 Offset :4subsetWithAllLocs {
\schemaVar \term LocSet s ;
\find ( subset ( s , allLocs ))
\replacewith ( true )
\heuristics (concrete )
\displayname "subsetOfAllLocs"
};defined in: locSetsRules.key Line: 1010 Offset :4subsetWithAllLocs2 {
\schemaVar \term LocSet s ;
\find ( subset ( allLocs , s ))
\replacewith ( s = allLocs )
\heuristics (concrete )
\displayname "subsetWithAllLocs"
};defined in: locSetsRules.key Line: 1021 Offset :4disjointWithEmpty {
\schemaVar \term LocSet s ;
\find ( disjoint ( empty , s ))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1035 Offset :4\lemma disjointWithSingleton1 {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( intersect ( s , singleton ( o , f ))= empty )
\replacewith ( ! elementOf ( o , f , s ))
\heuristics (simplify )
\displayname "disjointWithSingleton"
};defined in: locSetsRules.key Line: 1045 Offset :4\lemma disjointWithSingleton2 {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( intersect ( singleton ( o , f ), s )= empty )
\replacewith ( ! elementOf ( o , f , s ))
\heuristics (simplify )
\displayname "disjointWithSingleton"
};defined in: locSetsRules.key Line: 1056 Offset :4\lemma disjointArrayRanges {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term int lower1 , upper1 , lower2 , upper2 ;
\find ( intersect ( arrayRange ( o1 , lower1 , upper1 ), arrayRange ( o2 , lower2 , upper2 ))= empty )
\replacewith ( ! ( o1 = o2 & lower1 <= upper1 & lower2 <= upper2 & ( ( lower1 <= lower2 & lower2 <= upper1 )| ( lower2 <= lower1 & lower1 <= upper2 ))))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1067 Offset :4\lemma disjointArrayRangeAllFields1 {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term int lower2 , upper2 ;
\find ( intersect ( allFields ( o1 ), arrayRange ( o2 , lower2 , upper2 ))= empty )
\replacewith ( ! ( o1 = o2 & lower2 <= upper2 ))
\heuristics (simplify )
\displayname "disjointArrayRangeAllFields"
};defined in: locSetsRules.key Line: 1076 Offset :4\lemma disjointArrayRangeAllFields2 {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term int lower1 , upper1 ;
\find ( intersect ( arrayRange ( o1 , lower1 , upper1 ), allFields ( o2 ))= empty )
\replacewith ( ! ( o1 = o2 & lower1 <= upper1 ))
\heuristics (simplify )
\displayname "disjointArrayRangeAllFields"
};defined in: locSetsRules.key Line: 1086 Offset :4createdInHeapWithEmpty {
\schemaVar \term Heap h ;
\find ( createdInHeap ( empty , h ))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1100 Offset :4createdInHeapWithSingleton {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\find ( createdInHeap ( singleton ( o , f ), h ))
\replacewith ( o = null | boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1110 Offset :4createdInHeapWithUnion {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Heap h ;
\find ( ==> createdInHeap ( union ( s , s2 ), h ))
\replacewith ( ==> createdInHeap ( s , h ));
\replacewith ( ==> createdInHeap ( s2 , h ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1122 Offset :4createdInHeapWithSetMinusFreshLocs {
\schemaVar \term LocSet s ;
\schemaVar \term Heap h ;
\find ( createdInHeap ( setMinus ( s , freshLocs ( h )), h ))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1134 Offset :4createdInHeapWithAllFields {
\schemaVar \term Object o ;
\schemaVar \term Heap h ;
\find ( createdInHeap ( allFields ( o ), h ))
\replacewith ( o = null | boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1145 Offset :4createdInHeapWithArrayRange {
\schemaVar \term Object o ;
\schemaVar \term int lower , upper ;
\schemaVar \term Heap h ;
\find ( createdInHeap ( arrayRange ( o , lower , upper ), h ))
\replacewith ( o = null | boolean :: select ( h , o , java.lang.Object :: )= TRUE | upper < lower )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1156 Offset :4createdInHeapWithSelect {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\find ( ==> createdInHeap ( LocSet :: select ( h , o , f ), h ))
\replacewith ( ==> wellFormed ( h ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1168 Offset :4createdInHeapWithObserver {
\schemaVar \term LocSet obs ;
\schemaVar \term Heap h ;
\find ( ==> createdInHeap ( obs , h ))
\varcond \replacewith ( ==> wellFormed ( h ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1180 Offset :4createdInHeapWithSingletonEQ {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\schemaVar \term LocSet EQ ;
\assumes ( singleton ( o , f )= EQ ==> )
\find ( createdInHeap ( EQ , h ))
\sameUpdateLevel
\replacewith ( o = null | boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1197 Offset :4createdInHeapWithUnionEQ {
\schemaVar \term LocSet s , s2 ;
\schemaVar \term Heap h ;
\schemaVar \term LocSet EQ ;
\assumes ( union ( s , s2 )= EQ ==> )
\find ( ==> createdInHeap ( EQ , h ))
\replacewith ( ==> createdInHeap ( s , h ));
\replacewith ( ==> createdInHeap ( s2 , h ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1212 Offset :4createdInHeapWithSetMinusFreshLocsEQ {
\schemaVar \term LocSet s ;
\schemaVar \term Heap h ;
\schemaVar \term LocSet EQ ;
\assumes ( setMinus ( s , freshLocs ( h ))= EQ ==> )
\find ( createdInHeap ( EQ , h ))
\sameUpdateLevel
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1226 Offset :4createdInHeapWithAllFieldsEQ {
\schemaVar \term Object o ;
\schemaVar \term Heap h ;
\schemaVar \term LocSet EQ ;
\assumes ( allFields ( o )= EQ ==> )
\find ( createdInHeap ( EQ , h ))
\sameUpdateLevel
\replacewith ( o = null | boolean :: select ( h , o , java.lang.Object :: )= TRUE )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1240 Offset :4createdInHeapWithArrayRangeEQ {
\schemaVar \term Object o ;
\schemaVar \term int lower , upper ;
\schemaVar \term Heap h ;
\schemaVar \term LocSet EQ ;
\assumes ( arrayRange ( o , lower , upper )= EQ ==> )
\find ( createdInHeap ( EQ , h ))
\sameUpdateLevel
\replacewith ( o = null | boolean :: select ( h , o , java.lang.Object :: )= TRUE | upper < lower )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1254 Offset :4createdInHeapWithSelectEQ {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\schemaVar \term LocSet EQ ;
\assumes ( LocSet :: select ( h , o , f )= EQ ==> )
\find ( ==> createdInHeap ( EQ , h ))
\replacewith ( ==> wellFormed ( h ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1269 Offset :4createdInHeapWithObserverEQ {
\schemaVar \term LocSet obs ;
\schemaVar \term Heap h ;
\schemaVar \term LocSet EQ ;
\assumes ( obs = EQ ==> )
\find ( ==> createdInHeap ( EQ , h ))
\varcond \replacewith ( ==> wellFormed ( h ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1283 Offset :4referencedObjectIsCreatedRight {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( ==> deltaObject :: select ( h , o , f )= null )
\find ( ==> boolean :: select ( h , deltaObject :: select ( h , o , f ), java.lang.Object :: )= TRUE )
\replacewith ( ==> wellFormed ( h ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1301 Offset :4referencedObjectIsCreatedRightEQ {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Object EQ ;
\assumes ( deltaObject :: select ( h , o , f )= EQ ==> EQ = null )
\find ( ==> boolean :: select ( h , EQ , java.lang.Object :: )= TRUE )
\replacewith ( ==> wellFormed ( h ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1316 Offset :4unionEqualsEmpty {
\schemaVar \term LocSet s , s2 , s3 ;
\find ( union ( s , s2 )= empty )
\replacewith ( s = empty & s2 = empty )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1337 Offset :4unionEqualsEmptyEQ {
\schemaVar \term LocSet s , s2 , s3 ;
\schemaVar \term LocSet EQ ;
\assumes ( union ( s , s2 )= EQ ==> )
\find ( EQ = empty )
\sameUpdateLevel
\replacewith ( s = empty & s2 = empty )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1348 Offset :4setMinusOfUnion {
\schemaVar \term LocSet s , s2 , s3 ;
\find ( setMinus ( union ( s , s2 ), s3 ))
\replacewith ( union ( setMinus ( s , s3 ), setMinus ( s2 , s3 )))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1362 Offset :4setMinusOfUnionEQ {
\schemaVar \term LocSet s , s2 , s3 ;
\schemaVar \term LocSet EQ ;
\assumes ( union ( s , s2 )= EQ ==> )
\find ( setMinus ( EQ , s3 ))
\sameUpdateLevel
\replacewith ( union ( setMinus ( s , s3 ), setMinus ( s2 , s3 )))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1373 Offset :4subsetWithSetMinusLeft {
\schemaVar \term LocSet s , s2 , s3 ;
\find ( subset ( setMinus ( s , s2 ), s3 ))
\replacewith ( subset ( s , union ( s2 , s3 )))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1387 Offset :4subsetWithSetMinusLeftEQ {
\schemaVar \term LocSet s , s2 , s3 ;
\schemaVar \term LocSet EQ ;
\assumes ( setMinus ( s , s2 )= EQ ==> )
\find ( subset ( EQ , s3 ))
\sameUpdateLevel
\replacewith ( subset ( s , union ( s2 , s3 )))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1398 Offset :4unionWithItself {
\schemaVar \term LocSet s ;
\find ( union ( s , s ))
\replacewith ( s )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1411 Offset :4intersectWithItself {
\schemaVar \term LocSet s ;
\find ( intersect ( s , s ))
\replacewith ( s )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1421 Offset :4distributeIntersection {
\schemaVar \term LocSet s1 , s2 , s3 ;
\find ( intersect ( s1 , union ( s2 , s3 )))
\replacewith ( union ( intersect ( s1 , s2 ), intersect ( s1 , s3 )))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1432 Offset :4distributeIntersection_2 {
\schemaVar \term LocSet s1 , s2 , s3 ;
\find ( intersect ( union ( s2 , s3 ), s1 ))
\replacewith ( union ( intersect ( s2 , s1 ), intersect ( s3 , s1 )))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1442 Offset :4intersectWithSingleton {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\find ( intersect ( singleton ( o , f ), s ))
\replacewith ( \if ( elementOf ( o , f , s ))\then ( singleton ( o , f ))\else ( empty ))
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1452 Offset :4setMinusItself {
\schemaVar \term LocSet s ;
\find ( setMinus ( s , s ))
\replacewith ( empty )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1464 Offset :4setMinusSingleton {
\schemaVar \term LocSet s ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( ==> elementOf ( o , f , s ))
\find ( setMinus ( s , singleton ( o , f )))
\replacewith ( s )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1474 Offset :4intersectionSetMinusItself {
\schemaVar \term LocSet s1 , s2 ;
\find ( intersect ( setMinus ( s1 , s2 ), s2 ))
\replacewith ( empty )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1488 Offset :4intersectionSetMinusItself_2 {
\schemaVar \term LocSet s1 , s2 ;
\find ( intersect ( s2 , setMinus ( s1 , s2 )))
\replacewith ( empty )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1498 Offset :4unionIntersectItself {
\schemaVar \term LocSet s1 , s2 ;
\find ( union ( intersect ( s1 , s2 ), s1 ))
\replacewith ( s1 )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1508 Offset :4unionIntersectItself_2 {
\schemaVar \term LocSet s1 , s2 ;
\find ( union ( intersect ( s2 , s1 ), s1 ))
\replacewith ( s1 )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1518 Offset :4unionIntersectItself_3 {
\schemaVar \term LocSet s1 , s2 , s ;
\find ( union ( union ( s , intersect ( s1 , s2 )), s1 ))
\replacewith ( union ( s , s1 ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1528 Offset :4unionIntersectItself_4 {
\schemaVar \term LocSet s1 , s2 , s ;
\find ( union ( union ( s , intersect ( s2 , s1 )), s1 ))
\replacewith ( union ( s , s1 ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1538 Offset :4unionIntersectItself_5 {
\schemaVar \term LocSet s1 , s2 , s ;
\find ( union ( union ( intersect ( s1 , s2 ), s ), s1 ))
\replacewith ( union ( s , s1 ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1548 Offset :4unionIntersectItself_6 {
\schemaVar \term LocSet s1 , s2 , s ;
\find ( union ( union ( intersect ( s2 , s1 ), s ), s1 ))
\replacewith ( union ( s , s1 ))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1558 Offset :4infiniteUnionUnused {
\schemaVar \variables alpha av ;
\schemaVar \term LocSet s ;
\find ( infiniteUnion { av ; } ( s ))
\varcond \replacewith ( s )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1568 Offset :4subsetOfItself {
\schemaVar \term LocSet s ;
\find ( subset ( s , s ))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1580 Offset :4elementOfGuardedSet {
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \formula phi ;
\schemaVar \term LocSet s ;
\find ( elementOf ( o , f , \if ( phi )\then ( s )\else ( empty )))
\replacewith ( phi & elementOf ( o , f , s ))
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1591 Offset :4commuteDisjoint {
\schemaVar \term LocSet commLeft , commRight ;
\find ( disjoint ( commLeft , commRight ))
\replacewith ( disjoint ( commRight , commLeft ))
\heuristics (cnf_setComm )
};defined in: locSetsRules.key Line: 1604 Offset :4commuteUnion {
\schemaVar \term LocSet commLeft , commRight ;
\find ( union ( commLeft , commRight ))
\replacewith ( union ( commRight , commLeft ))
\heuristics (cnf_setComm )
};defined in: locSetsRules.key Line: 1613 Offset :4commuteUnion_2 {
\schemaVar \term LocSet commLeft , commRight , s ;
\find ( union ( union ( s , commLeft ), commRight ))
\replacewith ( union ( union ( s , commRight ), commLeft ))
\heuristics (cnf_setComm )
};defined in: locSetsRules.key Line: 1623 Offset :4commuteIntersection {
\schemaVar \term LocSet commLeft , commRight ;
\find ( intersect ( commLeft , commRight ))
\replacewith ( intersect ( commRight , commLeft ))
\heuristics (cnf_setComm )
};defined in: locSetsRules.key Line: 1633 Offset :4commuteIntersection_2 {
\schemaVar \term LocSet commLeft , commRight , s ;
\find ( intersect ( intersect ( s , commLeft ), commRight ))
\replacewith ( intersect ( intersect ( s , commRight ), commLeft ))
\heuristics (cnf_setComm )
};defined in: locSetsRules.key Line: 1643 Offset :4associativeLawUnion {
\schemaVar \term LocSet s1 , s2 , s3 ;
\find ( union ( s1 , union ( s2 , s3 )))
\replacewith ( union ( union ( s1 , s2 ), s3 ))
\heuristics (conjNormalForm )
};defined in: locSetsRules.key Line: 1653 Offset :4associativeLawIntersect {
\schemaVar \term LocSet s1 , s2 , s3 ;
\find ( intersect ( s1 , intersect ( s2 , s3 )))
\replacewith ( intersect ( intersect ( s1 , s2 ), s3 ))
\heuristics (conjNormalForm )
};defined in: locSetsRules.key Line: 1663 Offset :4definitionAllElementsOfArray {
\schemaVar \term Object array ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\schemaVar \variables int j ;
\find ( allElementsOfArray ( h , array , singleton ( o , f )))
\varcond \replacewith ( infiniteUnion { j ; } ( \if ( 0 <= j & j < length ( array ))\then ( singleton ( Object :: select ( h , array , arr ( j )), f ))\else ( empty )))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1677 Offset :4definitionAllElementsOfArray2 {
\schemaVar \term Object array ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\schemaVar \variables int j ;
\find ( allElementsOfArray ( h , array , allFields ( o )))
\varcond \replacewith ( infiniteUnion { j ; } ( \if ( 0 <= j & j < length ( array ))\then ( allFields ( Object :: select ( h , array , arr ( j ))))\else ( empty )))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1693 Offset :4definitionAllElementsOfArrayLocsets {
\schemaVar \term Object array ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Heap h ;
\schemaVar \variables int j ;
\find ( allElementsOfArrayLocsets ( h , array , singleton ( o , f )))
\varcond \replacewith ( infiniteUnion { j ; } ( \if ( 0 <= j & j < length ( array ))\then ( LocSet :: select ( h , Object :: select ( h , array , arr ( j )), f ))\else ( empty )))
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1709 Offset :4