Add missing translation taclets for bitwise operations

Some bitwise operations were missing translation taclets for the case
that the parameters are of type `long`. For example, `andJlong` did not
have a definition.

key.core/src/main/resources/de/uka/ilkd/key/proof/rules/binaryAxioms.key

@@ -93,6 +93,16 @@
         \heuristics(simplify_enlarging)
     };
 
+    unsignedShiftRightJlongDef {
+        \schemaVar \term int left, right;
+
+        \find(unsignedshiftrightJlong(left, right))
+        \replacewith(\if(left >= 0) \then(shiftrightJlong(left, right))
+                \else(addJlong(shiftrightJlong(left, right), shiftleftJlong(2, 63 - mod(right, 64)))))
+
+        \heuristics(simplify_enlarging)
+    };
+
     xorJIntDef {
         \schemaVar \term int left, right;
 
@@ -102,6 +112,15 @@
         \heuristics(simplify)
     };
 
+    xorJLongDef {
+        \schemaVar \term int left, right;
+
+        \find(xorJlong(left, right))
+        \replacewith(moduloLong(binaryXOr(left, right)))
+
+        \heuristics(simplify)
+    };
+
     orJIntDef {
         \schemaVar \term int left, right;
 
@@ -111,6 +130,15 @@
         \heuristics(simplify)
     };
 
+    orJLongDef {
+        \schemaVar \term int left, right;
+
+        \find(orJlong(left, right))
+        \replacewith(moduloLong(binaryOr(left, right)))
+
+        \heuristics(simplify)
+    };
+
     andJIntDef {
         \schemaVar \term int left, right;
 
@@ -119,4 +147,13 @@
 
         \heuristics(simplify)
     };
+
+    andJLongDef {
+        \schemaVar \term int left, right;
+
+        \find(andJlong(left, right))
+        \replacewith(moduloLong(binaryAnd(left, right)))
+
+        \heuristics(simplify)
+    };
 }