#397: add FunctionDeclarationKind for BV_ROTATE operations

Author: kfriedberger

src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java

@@ -181,6 +181,24 @@ public enum FunctionDeclarationKind {
   /** Arithmetic right-shift over bitvectors (fill from left with value of first bit). */
   BV_ASHR,
 
+  /** Performs a circular left rotation on the bitvector. */
+  BV_ROTATE_LEFT,
+
+  /** Performs a circular right rotation on the bitvector. */
+  BV_ROTATE_RIGHT,
+
+  /**
+   * Performs a circular left rotation on the bitvector by a specified number of positions,
+   * determined by an integer value.
+   */
+  BV_ROTATE_LEFT_BY_INT,
+
+  /**
+   * Performs a circular right rotation on the bitvector by a specified number of positions,
+   * determined by an integer value.
+   */
+  BV_ROTATE_RIGHT_BY_INT,
+
   /** Cast an unsigned bitvector to a floating-point number. */
   BV_UCASTTO_FP,
 

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java

@@ -305,8 +305,16 @@ private FunctionDeclarationKind getDeclarationKind(Term term) {
       return FunctionDeclarationKind.FP_CASTTO_UBV;
     } else if (kind.equals(Kind.BV_XOR)) {
       return FunctionDeclarationKind.BV_XOR;
+    } else if (kind.equals(Kind.BV_ROL)) {
+      return FunctionDeclarationKind.BV_ROTATE_LEFT;
+    } else if (kind.equals(Kind.BV_ROR)) {
+      return FunctionDeclarationKind.BV_ROTATE_RIGHT;
+    } else if (kind.equals(Kind.BV_ROLI)) {
+      return FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT;
+    } else if (kind.equals(Kind.BV_RORI)) {
+      return FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT;
     }
-    throw new UnsupportedOperationException("Can not discern formula kind " + kind);
+    return FunctionDeclarationKind.OTHER;
   }
 
   @SuppressWarnings("unchecked")

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

@@ -458,6 +458,8 @@ private Expr normalize(Expr operator) {
           .put(Kind.BITVECTOR_SHL, FunctionDeclarationKind.BV_SHL)
           .put(Kind.BITVECTOR_ASHR, FunctionDeclarationKind.BV_ASHR)
           .put(Kind.BITVECTOR_LSHR, FunctionDeclarationKind.BV_LSHR)
+          .put(Kind.BITVECTOR_ROTATE_LEFT, FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT)
+          .put(Kind.BITVECTOR_ROTATE_RIGHT, FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT)
           .put(Kind.BITVECTOR_NOT, FunctionDeclarationKind.BV_NOT)
           .put(Kind.BITVECTOR_NEG, FunctionDeclarationKind.BV_NEG)
           .put(Kind.BITVECTOR_EXTRACT, FunctionDeclarationKind.BV_EXTRACT)

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java

@@ -578,6 +578,8 @@ private Term normalize(Term operator) {
           .put(Kind.BITVECTOR_SHL, FunctionDeclarationKind.BV_SHL)
           .put(Kind.BITVECTOR_ASHR, FunctionDeclarationKind.BV_ASHR)
           .put(Kind.BITVECTOR_LSHR, FunctionDeclarationKind.BV_LSHR)
+          .put(Kind.BITVECTOR_ROTATE_LEFT, FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT)
+          .put(Kind.BITVECTOR_ROTATE_RIGHT, FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT)
           // Floating-point theory
           .put(Kind.TO_INTEGER, FunctionDeclarationKind.FLOOR)
           .put(Kind.TO_REAL, FunctionDeclarationKind.TO_REAL)

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java

@@ -23,6 +23,8 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_NEG;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_NOT;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_OR;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_ROL;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_ROR;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_SDIV;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_SEXT;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_SLE;
@@ -458,6 +460,10 @@ private FunctionDeclarationKind getDeclarationKind(long pF) {
         return FunctionDeclarationKind.BV_SIGN_EXTENSION;
       case MSAT_TAG_BV_ZEXT:
         return FunctionDeclarationKind.BV_ZERO_EXTENSION;
+      case MSAT_TAG_BV_ROL:
+        return FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT;
+      case MSAT_TAG_BV_ROR:
+        return FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT;
 
       case MSAT_TAG_FP_NEG:
         return FunctionDeclarationKind.FP_NEG;

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

@@ -707,6 +707,14 @@ private FunctionDeclarationKind getDeclarationKind(long f) {
         return FunctionDeclarationKind.BV_SIGN_EXTENSION;
       case Z3_OP_ZERO_EXT:
         return FunctionDeclarationKind.BV_ZERO_EXTENSION;
+      case Z3_OP_ROTATE_LEFT:
+        return FunctionDeclarationKind.BV_ROTATE_LEFT_BY_INT;
+      case Z3_OP_ROTATE_RIGHT:
+        return FunctionDeclarationKind.BV_ROTATE_RIGHT_BY_INT;
+      case Z3_OP_EXT_ROTATE_LEFT:
+        return FunctionDeclarationKind.BV_ROTATE_LEFT;
+      case Z3_OP_EXT_ROTATE_RIGHT:
+        return FunctionDeclarationKind.BV_ROTATE_RIGHT;
 
       case Z3_OP_FPA_NEG:
         return FunctionDeclarationKind.FP_NEG;