Abstract datatype of (untyped) partial maps.
Map;defined in: map.key Line: 13 Offset :4Return a value from the given Map.
If value is undefined, mapUndef is used.
inDomainImpliesCreated (Map ); defined in: map.key Line: 40 Offset :4getOfMapForeach {
\find ( mapGet ( mapForeach { v ; } ( b , y ), x ))
\sameUpdateLevel
\replacewith ( \if ( inDomain ( mapForeach { v ; } ( b , y ), x ))\then ( {\subst v ; alpha :: cast ( x )} y )\else ( mapUndef ))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 74 Offset :4defMapEmpty {
\find ( mapEmpty )
\replacewith ( mapForeach { vy ; } ( FALSE , mapUndef ))
};defined in: map.key Line: 87 Offset :4defMapOverride {
\find ( mapOverride ( m0 , m1 ))
\varcond \replacewith ( mapForeach { vy ; } ( \if ( inDomain ( m0 , vy )| inDomain ( m1 , vy ))\then ( TRUE )\else ( FALSE ), \if ( inDomain ( m1 , vy ))\then ( mapGet ( m1 , vy ))\else ( mapGet ( m0 , vy ))))
};defined in: map.key Line: 100 Offset :4defSeq2Map {
\schemaVar \term Seq s ;
\schemaVar \variables int ix ;
\find ( seq2map ( s ))
\varcond \replacewith ( mapForeach { ix ; } ( \if ( 0 <= ix & ix < seqLen ( s ))\then ( TRUE )\else ( FALSE ), any :: seqGet ( s , ix )))
};defined in: map.key Line: 110 Offset :4defInDomainImpliesCreated {
\schemaVar \variables Object o ;
\find ( inDomainImpliesCreated ( m ))
\varcond \replacewith ( \forall o ; ( inDomain ( m , o )-> boolean :: select ( heap , o , java.lang.Object :: )= TRUE ))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 148 Offset :4mapEqualityRight {
\find ( ==> m0 = m1 )
\varcond \replacewith ( ==> \forall vy ; ( ( inDomain ( m0 , vy )<-> inDomain ( m1 , vy ))& ( inDomain ( m0 , vy )-> mapGet ( m0 , vy )= mapGet ( m1 , vy ))))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 162 Offset :4mapUpdateUnchanged {
\find ( m = mapUpdate ( m , key , value ))
\replacewith ( inDomain ( m , key )& mapGet ( m , key )= value )
\heuristics (simplify_enlarging )
};defined in: map.key Line: 171 Offset :4mapUpdateUnchanged2 {
\find ( mapUpdate ( m , key , value )= m )
\replacewith ( inDomain ( m , key )& mapGet ( m , key )= value )
\heuristics (simplify_enlarging )
};defined in: map.key Line: 178 Offset :4mapRemoveUnchanged {
\find ( m = mapRemove ( m , key ))
\replacewith ( ! inDomain ( m , key ))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 185 Offset :4mapRemoveUnchanged2 {
\find ( mapRemove ( m , key )= m )
\replacewith ( ! inDomain ( m , key ))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 192 Offset :4inDomainOfMapEmpty {
\find ( inDomain ( mapEmpty , x ))
\replacewith ( false )
\heuristics (concrete )
};defined in: map.key Line: 202 Offset :4inDomainOfMapSingleton {
\find ( inDomain ( mapSingleton ( x , y ), z ))
\replacewith ( x = z )
\heuristics (simplify )
};defined in: map.key Line: 208 Offset :4inDomainOfMapOverride {
\find ( inDomain ( mapOverride ( m0 , m1 ), x ))
\replacewith ( inDomain ( m0 , x )| inDomain ( m1 , x ))
\heuristics (simplify )
};defined in: map.key Line: 214 Offset :4inDomainOfMapUpdate {
\find ( inDomain ( mapUpdate ( m , key , value ), x ))
\replacewith ( inDomain ( m , x )| ( x = key ))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 229 Offset :4inDomainOfMapRemove {
\find ( inDomain ( mapRemove ( m , key ), x ))
\replacewith ( inDomain ( m , x )& ( x != key ))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 236 Offset :4notInDomain {
\find ( ==> inDomain ( m , x ))
\add ( mapGet ( m , x )= mapUndef ==> )
\heuristics (inReachableStateImplication )
};defined in: map.key Line: 243 Offset :4inDomainConcrete {
\assumes ( ==> mapUndef = y )
\find ( mapGet ( m , x )= y ==> )
\add ( inDomain ( m , x )==> )
\heuristics (inReachableStateImplication )
};defined in: map.key Line: 249 Offset :4getOfMapEmpty {
\find ( mapGet ( mapEmpty , x ))
\sameUpdateLevel
\replacewith ( mapUndef )
\heuristics (simplify )
};defined in: map.key Line: 261 Offset :4getOfMapSingleton {
\find ( mapGet ( mapSingleton ( x , y ), z ))
\sameUpdateLevel
\replacewith ( \if ( x = z )\then ( y )\else ( mapUndef ))
\heuristics (simplify )
};defined in: map.key Line: 268 Offset :4getOfMapOverride {
\find ( mapGet ( mapOverride ( m0 , m1 ), x ))
\sameUpdateLevel
\replacewith ( \if ( inDomain ( m1 , x ))\then ( mapGet ( m1 , x ))\else ( mapGet ( m0 , x )))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 275 Offset :4getOfSeq2Map {
\schemaVar \term Seq s ;
\find ( mapGet ( seq2map ( s ), x ))
\sameUpdateLevel
\replacewith ( \if ( int :: instance ( x )= TRUE & 0 <= int :: cast ( x )& int :: cast ( x )< seqLen ( s ))\then ( any :: seqGet ( s , int :: cast ( x )))\else ( mapUndef ))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 283 Offset :4getOfMapUpdate {
\find ( mapGet ( mapUpdate ( m , key , value ), x ))
\sameUpdateLevel
\replacewith ( \if ( x = key )\then ( value )\else ( mapGet ( m , x )))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 293 Offset :4getOfMapRemove {
\find ( mapGet ( mapRemove ( m , key ), x ))
\sameUpdateLevel
\replacewith ( \if ( x = key )\then ( mapUndef )\else ( mapGet ( m , x )))
\heuristics (simplify_enlarging )
};defined in: map.key Line: 301 Offset :4