shiftRightPositiveShiftDef {
\schemaVar \term int left , right ;
\find ( shiftrightPositiveShift ( left , right ))
\replacewith ( div ( left , pow ( 2 , right )))
\heuristics (simplify )
};defined in: binaryAxioms.key Line: 7 Offset :4shiftLeftPositiveShiftDef {
\schemaVar \term int left , right ;
\find ( shiftleftPositiveShift ( left , right ))
\replacewith ( mul ( left , pow ( 2 , right )))
\heuristics (simplify )
};defined in: binaryAxioms.key Line: 16 Offset :4shiftRightDef {
\schemaVar \term int left , right ;
\find ( shiftright ( left , right ))
\replacewith ( \if ( right < 0 )\then ( shiftleftPositiveShift ( left , - right ))\else ( shiftrightPositiveShift ( left , right )))
\heuristics (simplify_enlarging )
};defined in: binaryAxioms.key Line: 26 Offset :4shiftLeftDef {
\schemaVar \term int left , right ;
\find ( shiftleft ( left , right ))
\replacewith ( \if ( right < 0 )\then ( shiftrightPositiveShift ( left , - right ))\else ( shiftleftPositiveShift ( left , right )))
\heuristics (simplify_enlarging )
};defined in: binaryAxioms.key Line: 38 Offset :4javaShiftRightIntDef {
\schemaVar \term int left , right ;
\find ( shiftrightJint ( left , right ))
\replacewith ( moduloInt ( shiftright ( left , mod ( right , 32 ))))
\heuristics (simplify_enlarging )
};defined in: binaryAxioms.key Line: 50 Offset :4javaShiftRightLongDef {
\schemaVar \term int left , right ;
\find ( shiftrightJlong ( left , right ))
\replacewith ( moduloLong ( shiftright ( left , mod ( right , 64 ))))
\heuristics (simplify_enlarging )
};defined in: binaryAxioms.key Line: 59 Offset :4javaShiftLeftIntDef {
\schemaVar \term int left , right ;
\find ( shiftleftJint ( left , right ))
\replacewith ( moduloInt ( shiftleft ( left , mod ( right , 32 ))))
\heuristics (simplify_enlarging )
};defined in: binaryAxioms.key Line: 69 Offset :4javaShiftLeftLongDef {
\schemaVar \term int left , right ;
\find ( shiftleftJlong ( left , right ))
\replacewith ( moduloLong ( shiftleft ( left , mod ( right , 64 ))))
\heuristics (simplify_enlarging )
};defined in: binaryAxioms.key Line: 78 Offset :4unsignedShiftRightJintDef {
\schemaVar \term int left , right ;
\find ( unsignedshiftrightJint ( left , right ))
\replacewith ( \if ( left >= 0 )\then ( shiftrightJint ( left , right ))\else ( addJint ( shiftrightJint ( left , right ), shiftleftJint ( 2 , 31 - mod ( right , 32 )))))
\heuristics (simplify_enlarging )
};defined in: binaryAxioms.key Line: 88 Offset :4xorJIntDef {
\schemaVar \term int left , right ;
\find ( xorJint ( left , right ))
\replacewith ( moduloInt ( binaryXOr ( left , right )))
\heuristics (simplify )
};defined in: binaryAxioms.key Line: 96 Offset :4orJIntDef {
\schemaVar \term int left , right ;
\find ( orJint ( left , right ))
\replacewith ( moduloInt ( binaryOr ( left , right )))
\heuristics (simplify )
};defined in: binaryAxioms.key Line: 105 Offset :4andJIntDef {
\schemaVar \term int left , right ;
\find ( andJint ( left , right ))
\replacewith ( moduloInt ( binaryAnd ( left , right )))
\heuristics (simplify )
};defined in: binaryAxioms.key Line: 114 Offset :4