Revert "Bitwuzla: Patch handling of bitvector rotations in the formula visitor"

daniel-raffler · daniel-raffler · commit 9718a1890743 · 2024-09-21T15:01:36.000+02:00
This reverts commit 328a5ec.
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
@@ -326,10 +326,6 @@ private FunctionDeclarationKind getDeclarationKind(Term term) {
       return FunctionDeclarationKind.FP_CASTTO_UBV;
     } else if (kind.equals(Kind.BV_XOR)) {
       return FunctionDeclarationKind.BV_XOR;
-    } else if (ImmutableList.of(Kind.BV_ROL, Kind.BV_ROLI, Kind.BV_ROR, Kind.BV_RORI)
-        .contains(kind)) {
-      // Rotations are not yet supported by FunctionDeclarationKind
-      return FunctionDeclarationKind.OTHER;
     }
     throw new UnsupportedOperationException("Can not discern formula kind " + kind);
   }

Original file line number	Diff line number	Diff line change
`@@ -326,10 +326,6 @@ private FunctionDeclarationKind getDeclarationKind(Term term) {`
`326`	`326`	`return FunctionDeclarationKind.FP_CASTTO_UBV;`
`327`	`327`	`} else if (kind.equals(Kind.BV_XOR)) {`
`328`	`328`	`return FunctionDeclarationKind.BV_XOR;`
`329`		`- } else if (ImmutableList.of(Kind.BV_ROL, Kind.BV_ROLI, Kind.BV_ROR, Kind.BV_RORI)`
`330`		`- .contains(kind)) {`
`331`		`- // Rotations are not yet supported by FunctionDeclarationKind`
`332`		`- return FunctionDeclarationKind.OTHER;`
`333`	`329`	`}`
`334`	`330`	`throw new UnsupportedOperationException("Can not discern formula kind " + kind);`
`335`	`331`	`}`