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 :4\lemma equalityOfSingleton {
\schemaVar \term Object o1 , o2 ;
\schemaVar \term Field f1 , f2 ;
\find ( singleton ( o1 , f1 )= singleton ( o2 , f2 ))
\replacewith ( o1 = o2 & f1 = f2 )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 862 Offset :4unionWithEmpty {
\schemaVar \term LocSet s ;
\find ( union ( empty , s ))
\replacewith ( s )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 878 Offset :4unionWithAllLocs {
\schemaVar \term LocSet s ;
\find ( union ( allLocs , s ))
\replacewith ( allLocs )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 888 Offset :4intersectWithEmpty {
\schemaVar \term LocSet s ;
\find ( intersect ( empty , s ))
\replacewith ( empty )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 898 Offset :4intersectWithAllLocs {
\schemaVar \term LocSet s ;
\find ( intersect ( allLocs , s ))
\replacewith ( s )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 908 Offset :4unionWithEmptyRight {
\schemaVar \term LocSet s ;
\find ( union ( s , empty ))
\replacewith ( s )
\heuristics (concrete )
\displayname "unionWithEmpty"
};defined in: locSetsRules.key Line: 923 Offset :4unionWithAllLocsRight {
\schemaVar \term LocSet s ;
\find ( union ( s , allLocs ))
\replacewith ( allLocs )
\heuristics (concrete )
\displayname "unionWithAllLocs"
};defined in: locSetsRules.key Line: 934 Offset :4intersectWithEmptyRight {
\schemaVar \term LocSet s ;
\find ( intersect ( s , empty ))
\replacewith ( empty )
\heuristics (concrete )
\displayname "intersectWithEmpty"
};defined in: locSetsRules.key Line: 945 Offset :4intersectWithAllLocsRight {
\schemaVar \term LocSet s ;
\find ( intersect ( s , allLocs ))
\replacewith ( s )
\heuristics (concrete )
\displayname "intersectWithAllLocs"
};defined in: locSetsRules.key Line: 956 Offset :4setMinusWithEmpty1 {
\schemaVar \term LocSet s ;
\find ( setMinus ( s , empty ))
\replacewith ( s )
\heuristics (concrete )
\displayname "setMinusWithEmpty"
};defined in: locSetsRules.key Line: 970 Offset :4setMinusWithEmpty2 {
\schemaVar \term LocSet s ;
\find ( setMinus ( empty , s ))
\replacewith ( empty )
\heuristics (concrete )
\displayname "setMinusWithEmpty"
};defined in: locSetsRules.key Line: 981 Offset :4setMinusWithAllLocs {
\schemaVar \term LocSet s ;
\find ( setMinus ( s , allLocs ))
\replacewith ( empty )
\heuristics (concrete )
\displayname "setMinusWithAllLocs"
};defined in: locSetsRules.key Line: 992 Offset :4subsetWithEmpty {
\schemaVar \term LocSet s ;
\find ( subset ( empty , s ))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1007 Offset :4subsetOfEmpty {
\schemaVar \term LocSet s ;
\find ( subset ( s , empty ))
\replacewith ( s = empty )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1017 Offset :4subsetWithAllLocs {
\schemaVar \term LocSet s ;
\find ( subset ( s , allLocs ))
\replacewith ( true )
\heuristics (concrete )
\displayname "subsetOfAllLocs"
};defined in: locSetsRules.key Line: 1027 Offset :4subsetWithAllLocs2 {
\schemaVar \term LocSet s ;
\find ( subset ( allLocs , s ))
\replacewith ( s = allLocs )
\heuristics (concrete )
\displayname "subsetWithAllLocs"
};defined in: locSetsRules.key Line: 1038 Offset :4disjointWithEmpty {
\schemaVar \term LocSet s ;
\find ( disjoint ( empty , s ))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1052 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: 1062 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: 1073 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: 1084 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: 1093 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: 1103 Offset :4createdInHeapWithEmpty {
\schemaVar \term Heap h ;
\find ( createdInHeap ( empty , h ))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1117 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: 1127 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: 1139 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: 1151 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: 1162 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: 1173 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: 1185 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: 1197 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: 1214 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: 1229 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: 1243 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: 1257 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: 1271 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: 1286 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: 1300 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: 1318 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: 1333 Offset :4referencedObjectIsCreatedRightFinal {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\assumes ( ==> deltaObject :: final ( o , f )= null )
\find ( ==> boolean :: select ( h , deltaObject :: final ( o , f ), java.lang.Object :: )= TRUE )
\replacewith ( ==> boolean :: select ( h , o , java.lang.Object :: )= TRUE | o = null )
\heuristics (simplify_enlarging )
};defined in: locSetsRules.key Line: 1349 Offset :4referencedObjectIsCreatedRighFinalEQ {
\schemaVar \term Heap h ;
\schemaVar \term Object o ;
\schemaVar \term Field f ;
\schemaVar \term Object EQ ;
\assumes ( deltaObject :: final ( o , f )= EQ ==> EQ = null )
\find ( ==> boolean :: select ( h , EQ , java.lang.Object :: )= TRUE )
\add ( ==> boolean :: select ( h , o , java.lang.Object :: )= TRUE | o = null )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1364 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: 1385 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: 1396 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: 1410 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: 1421 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: 1435 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: 1446 Offset :4unionWithItself {
\schemaVar \term LocSet s ;
\find ( union ( s , s ))
\replacewith ( s )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1459 Offset :4intersectWithItself {
\schemaVar \term LocSet s ;
\find ( intersect ( s , s ))
\replacewith ( s )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1469 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: 1480 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: 1490 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: 1500 Offset :4setMinusItself {
\schemaVar \term LocSet s ;
\find ( setMinus ( s , s ))
\replacewith ( empty )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1512 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: 1522 Offset :4intersectionSetMinusItself {
\schemaVar \term LocSet s1 , s2 ;
\find ( intersect ( setMinus ( s1 , s2 ), s2 ))
\replacewith ( empty )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1536 Offset :4intersectionSetMinusItself_2 {
\schemaVar \term LocSet s1 , s2 ;
\find ( intersect ( s2 , setMinus ( s1 , s2 )))
\replacewith ( empty )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1546 Offset :4unionIntersectItself {
\schemaVar \term LocSet s1 , s2 ;
\find ( union ( intersect ( s1 , s2 ), s1 ))
\replacewith ( s1 )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1556 Offset :4unionIntersectItself_2 {
\schemaVar \term LocSet s1 , s2 ;
\find ( union ( intersect ( s2 , s1 ), s1 ))
\replacewith ( s1 )
\heuristics (simplify )
};defined in: locSetsRules.key Line: 1566 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: 1576 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: 1586 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: 1596 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: 1606 Offset :4infiniteUnionUnused {
\schemaVar \variables alpha av ;
\schemaVar \term LocSet s ;
\find ( infiniteUnion { av ; } ( s ))
\varcond \replacewith ( s )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1616 Offset :4subsetOfItself {
\schemaVar \term LocSet s ;
\find ( subset ( s , s ))
\replacewith ( true )
\heuristics (concrete )
};defined in: locSetsRules.key Line: 1628 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: 1639 Offset :4commuteDisjoint {
\schemaVar \term LocSet commLeft , commRight ;
\find ( disjoint ( commLeft , commRight ))
\replacewith ( disjoint ( commRight , commLeft ))
\heuristics (cnf_setComm )
};defined in: locSetsRules.key Line: 1652 Offset :4commuteUnion {
\schemaVar \term LocSet commLeft , commRight ;
\find ( union ( commLeft , commRight ))
\replacewith ( union ( commRight , commLeft ))
\heuristics (cnf_setComm )
};defined in: locSetsRules.key Line: 1661 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: 1671 Offset :4commuteIntersection {
\schemaVar \term LocSet commLeft , commRight ;
\find ( intersect ( commLeft , commRight ))
\replacewith ( intersect ( commRight , commLeft ))
\heuristics (cnf_setComm )
};defined in: locSetsRules.key Line: 1681 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: 1691 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: 1701 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: 1711 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: 1725 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: 1741 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: 1757 Offset :4