replace_byte_MAX {
\find ( byte_MAX )
\replacewith ( 127 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 48 Offset :4replace_byte_MIN {
\find ( byte_MIN )
\replacewith ( - 128 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 55 Offset :4replace_char_MAX {
\find ( char_MAX )
\replacewith ( 65535 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 62 Offset :4replace_char_MIN {
\find ( char_MIN )
\replacewith ( 0 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 69 Offset :4replace_short_MAX {
\find ( short_MAX )
\replacewith ( 32767 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 76 Offset :4replace_short_MIN {
\find ( short_MIN )
\replacewith ( - 32768 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 83 Offset :4replace_int_MAX {
\find ( int_MAX )
\replacewith ( 2147483647 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 90 Offset :4replace_int_MIN {
\find ( int_MIN )
\replacewith ( - 2147483648 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 97 Offset :4replace_long_MAX {
\find ( long_MAX )
\replacewith ( 9223372036854775807 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 104 Offset :4replace_long_MIN {
\find ( long_MIN )
\replacewith ( - 9223372036854775808 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 111 Offset :4replace_byte_RANGE {
\find ( byte_RANGE )
\replacewith ( 256 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 122 Offset :4replace_byte_HALFRANGE {
\find ( byte_HALFRANGE )
\replacewith ( 128 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 129 Offset :4replace_short_RANGE {
\find ( short_RANGE )
\replacewith ( 65536 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 136 Offset :4replace_short_HALFRANGE {
\find ( short_HALFRANGE )
\replacewith ( 32768 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 143 Offset :4replace_char_RANGE {
\find ( char_RANGE )
\replacewith ( 65536 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 150 Offset :4replace_int_RANGE {
\find ( int_RANGE )
\replacewith ( 4294967296 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 157 Offset :4replace_int_HALFRANGE {
\find ( int_HALFRANGE )
\replacewith ( 2147483648 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 164 Offset :4replace_long_RANGE {
\find ( long_RANGE )
\replacewith ( 18446744073709551616 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 171 Offset :4replace_long_HALFRANGE {
\find ( long_HALFRANGE )
\replacewith ( 9223372036854775808 )
\heuristics (defOps_expandRanges )
};defined in: intRules.key Line: 177 Offset :4expandInRangeByte {
\find ( inRangeByte ( i ))
\replacewith ( leq ( i , byte_MAX )& leq ( byte_MIN , i ))
\heuristics (defOps_expandRanges , delayedExpansion )
};defined in: intRules.key Line: 188 Offset :4expandInRangeChar {
\find ( inRangeChar ( i ))
\replacewith ( leq ( i , char_MAX )& leq ( char_MIN , i ))
\heuristics (defOps_expandRanges , delayedExpansion )
};defined in: intRules.key Line: 194 Offset :4expandInRangeShort {
\find ( inRangeShort ( i ))
\replacewith ( leq ( i , short_MAX )& leq ( short_MIN , i ))
\heuristics (defOps_expandRanges , delayedExpansion )
};defined in: intRules.key Line: 200 Offset :4expandInRangeInt {
\find ( inRangeInt ( i ))
\replacewith ( leq ( i , int_MAX )& leq ( int_MIN , i ))
\heuristics (defOps_expandRanges , delayedExpansion )
};defined in: intRules.key Line: 206 Offset :4expandInRangeLong {
\find ( inRangeLong ( i ))
\replacewith ( leq ( i , long_MAX )& leq ( long_MIN , i ))
\heuristics (defOps_expandRanges , delayedExpansion )
};defined in: intRules.key Line: 212 Offset :4expand_moduloByte {
\find ( moduloByte ( i ))
\replacewith ( add ( byte_MIN , mod ( add ( byte_HALFRANGE , i ), byte_RANGE )))
\heuristics (defOps_expandJNumericOp , delayedExpansion )
};defined in: intRules.key Line: 225 Offset :4expand_moduloShort {
\find ( moduloShort ( i ))
\replacewith ( add ( short_MIN , mod ( add ( short_HALFRANGE , i ), short_RANGE )))
\heuristics (defOps_expandJNumericOp , delayedExpansion )
};defined in: intRules.key Line: 232 Offset :4expand_moduloInteger {
\find ( moduloInt ( i ))
\replacewith ( add ( int_MIN , mod ( add ( int_HALFRANGE , i ), int_RANGE )))
\heuristics (defOps_expandJNumericOp , delayedExpansion )
};defined in: intRules.key Line: 239 Offset :4expand_moduloLong {
\find ( moduloLong ( i ))
\replacewith ( add ( long_MIN , mod ( add ( long_HALFRANGE , i ), long_RANGE )))
\heuristics (defOps_expandJNumericOp , delayedExpansion )
};defined in: intRules.key Line: 246 Offset :4expand_moduloChar {
\find ( moduloChar ( i ))
\replacewith ( mod ( i , char_MAX + 1 ))
\heuristics (defOps_expandJNumericOp , delayedExpansion )
};defined in: intRules.key Line: 252 Offset :4moduloIntFixpoint {
\assumes ( inRangeInt ( i )==> )
\find ( moduloInt ( i ))
\sameUpdateLevel
\replacewith ( i )
\heuristics (simplify )
};defined in: intRules.key Line: 262 Offset :4moduloLongFixpoint {
\assumes ( inRangeLong ( i )==> )
\find ( moduloLong ( i ))
\sameUpdateLevel
\replacewith ( i )
\heuristics (simplify )
};defined in: intRules.key Line: 271 Offset :4moduloShortFixpoint {
\assumes ( inRangeShort ( i )==> )
\find ( moduloShort ( i ))
\sameUpdateLevel
\replacewith ( i )
\heuristics (simplify )
};defined in: intRules.key Line: 280 Offset :4moduloByteFixpoint {
\assumes ( inRangeByte ( i )==> )
\find ( moduloByte ( i ))
\sameUpdateLevel
\replacewith ( i )
\heuristics (simplify )
};defined in: intRules.key Line: 289 Offset :4moduloCharFixpoint {
\assumes ( inRangeChar ( i )==> )
\find ( moduloChar ( i ))
\sameUpdateLevel
\replacewith ( i )
\heuristics (simplify )
};defined in: intRules.key Line: 298 Offset :4moduloIntFixpointInline {
\schemaVar \skolemTerm int moduloT ;
\find ( moduloInt ( i ))
\sameUpdateLevel
\varcond \replacewith ( moduloT ) \add ( \if ( inRangeInt ( i ))\then ( i )\else ( moduloT )= moduloT , moduloInt ( i )= moduloT ==> )
};defined in: intRules.key Line: 307 Offset :4moduloLongFixpointInline {
\schemaVar \skolemTerm int moduloT ;
\find ( moduloLong ( i ))
\sameUpdateLevel
\varcond \replacewith ( moduloT ) \add ( \if ( inRangeLong ( i ))\then ( i )\else ( moduloT )= moduloT , moduloLong ( i )= moduloT ==> )
};defined in: intRules.key Line: 317 Offset :4moduloShortFixpointInline {
\schemaVar \skolemTerm int moduloT ;
\find ( moduloShort ( i ))
\sameUpdateLevel
\varcond \replacewith ( moduloT ) \add ( \if ( inRangeShort ( i ))\then ( i )\else ( moduloT )= moduloT , moduloShort ( i )= moduloT ==> )
};defined in: intRules.key Line: 327 Offset :4moduloByteFixpointInline {
\schemaVar \skolemTerm int moduloT ;
\find ( moduloByte ( i ))
\sameUpdateLevel
\varcond \replacewith ( moduloT ) \add ( \if ( inRangeByte ( i ))\then ( i )\else ( moduloT )= moduloT , moduloByte ( i )= moduloT ==> )
};defined in: intRules.key Line: 337 Offset :4moduloCharFixpointInline {
\schemaVar \skolemTerm int moduloT ;
\find ( moduloChar ( i ))
\sameUpdateLevel
\varcond \replacewith ( moduloT ) \add ( \if ( inRangeChar ( i ))\then ( i )\else ( moduloT )= moduloT , moduloChar ( i )= moduloT ==> )
};defined in: intRules.key Line: 347 Offset :4moduloIntIsInRangeInt {
\find ( inRangeInt ( moduloInt ( i )))
\replacewith ( true )
\heuristics (concrete )
};defined in: intRules.key Line: 361 Offset :4moduloLongIsInRangeLong {
\find ( inRangeLong ( moduloLong ( i )))
\replacewith ( true )
\heuristics (concrete )
};defined in: intRules.key Line: 367 Offset :4moduloShortIsInRangeShort {
\find ( inRangeShort ( moduloShort ( i )))
\replacewith ( true )
\heuristics (concrete )
};defined in: intRules.key Line: 373 Offset :4moduloByteIsInRangeByte {
\find ( inRangeByte ( moduloByte ( i )))
\replacewith ( true )
\heuristics (concrete )
};defined in: intRules.key Line: 379 Offset :4moduloCharIsInRangeChar {
\find ( inRangeChar ( moduloChar ( i )))
\replacewith ( true )
\heuristics (concrete )
};defined in: intRules.key Line: 385 Offset :4