Add rotation operations to BitvectorFormulaManager

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

@@ -98,6 +98,30 @@ protected Expr rotateRightByConstant(Expr number, int toRotate) {
     return exprManager.mkExpr(op, number);
   }
 
+  @Override
+  protected Expr rotateRight(Expr pNumber, Expr toRotate) {
+    // cvc4 does not support non-literal rotation, so we rewrite it to (bvor (bvlshr pNumber
+    // toRotate) (bvshl pNumber (bvsub size toRotate)))
+    final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize();
+    final Expr size = this.makeBitvectorImpl(bitsize, bitsize);
+    final Expr toRotateInRange = exprManager.mkExpr(Kind.BITVECTOR_UREM, toRotate, size);
+    return or(
+        shiftRight(pNumber, toRotateInRange, false),
+        shiftLeft(pNumber, subtract(size, toRotateInRange)));
+  }
+
+  @Override
+  protected Expr rotateLeft(Expr pNumber, Expr toRotate) {
+    // cvc4 does not support non-literal rotation, so we rewrite it to (bvor (bvshl pNumber
+    // toRotate) (bvlshr pNumber (bvsub size toRotate)))
+    final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize();
+    final Expr size = this.makeBitvectorImpl(bitsize, bitsize);
+    final Expr toRotateInRange = exprManager.mkExpr(Kind.BITVECTOR_UREM, toRotate, size);
+    return or(
+        shiftLeft(pNumber, toRotateInRange),
+        shiftRight(pNumber, subtract(size, toRotateInRange), false));
+  }
+
   @Override
   protected Expr not(Expr pParam1) {
     return exprManager.mkExpr(Kind.BITVECTOR_NOT, pParam1);

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

@@ -16,6 +16,7 @@
 import io.github.cvc5.Term;
 import java.math.BigInteger;
 import java.util.List;
+import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
 import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
 
 public class CVC5BitvectorFormulaManager
@@ -147,6 +148,30 @@ protected Term rotateRightByConstant(Term pNumber, int pToRotate) {
     }
   }
 
+  @Override
+  protected Term rotateRight(Term pNumber, Term toRotate) {
+    // cvc5 does not support non-literal rotation, so we rewrite it to (bvor (bvlshr pNumber
+    // toRotate) (bvshl pNumber (bvsub size toRotate)))
+    final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize();
+    final Term size = this.makeBitvectorImpl(bitsize, bitsize);
+    final Term toRotateInRange = solver.mkTerm(Kind.BITVECTOR_UREM, toRotate, size);
+    return or(
+        shiftRight(pNumber, toRotateInRange, false),
+        shiftLeft(pNumber, subtract(size, toRotateInRange)));
+  }
+
+  @Override
+  protected Term rotateLeft(Term pNumber, Term toRotate) {
+    // cvc5 does not support non-literal rotation, so we rewrite it to (bvor (bvshl pNumber
+    // toRotate) (bvlshr pNumber (bvsub size toRotate)))
+    final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize();
+    final Term size = this.makeBitvectorImpl(bitsize, bitsize);
+    final Term toRotateInRange = solver.mkTerm(Kind.BITVECTOR_UREM, toRotate, size);
+    return or(
+        shiftLeft(pNumber, toRotateInRange),
+        shiftRight(pNumber, subtract(size, toRotateInRange), false));
+  }
+
   @Override
   protected Term not(Term pParam1) {
     return solver.mkTerm(Kind.BITVECTOR_NOT, pParam1);

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

@@ -40,6 +40,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_int_to_bv;
 
 import java.math.BigInteger;
+import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
 import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
 
 /** Mathsat Bitvector Theory, build out of Bitvector*Operations. */
@@ -137,6 +138,30 @@ public Long rotateRightByConstant(Long number, int toRotate) {
     return msat_make_bv_ror(mathsatEnv, toRotate, number);
   }
 
+  @Override
+  protected Long rotateRight(Long pNumber, Long toRotate) {
+    // MathSAT5 does not support non-literal rotation, so we rewrite it to (bvor (bvlshr pNumber
+    // toRotate) (bvshl pNumber (bvsub size toRotate)))
+    final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize();
+    final Long size = makeBitvectorImpl(bitsize, bitsize);
+    final Long toRotateInRange = msat_make_bv_urem(mathsatEnv, toRotate, size);
+    return or(
+        shiftRight(pNumber, toRotateInRange, false),
+        shiftLeft(pNumber, subtract(size, toRotateInRange)));
+  }
+
+  @Override
+  protected Long rotateLeft(Long pNumber, Long toRotate) {
+    // MathSAT5 does not support non-literal rotation, so we rewrite it to (bvor (bvshl pNumber
+    // toRotate) (bvlshr pNumber (bvsub size toRotate)))
+    final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize();
+    final Long size = this.makeBitvectorImpl(bitsize, bitsize);
+    final Long toRotateInRange = msat_make_bv_urem(mathsatEnv, toRotate, size);
+    return or(
+        shiftLeft(pNumber, toRotateInRange),
+        shiftRight(pNumber, subtract(size, toRotateInRange), false));
+  }
+
   @Override
   public Long not(Long pBits) {
     return msat_make_bv_not(mathsatEnv, pBits);

src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java

@@ -16,6 +16,7 @@
 import ap.types.Sort$;
 import com.google.common.base.Preconditions;
 import java.math.BigInteger;
+import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
 import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
 import scala.Option;
 
@@ -177,6 +178,32 @@ protected IExpression shiftLeft(IExpression pExtract, IExpression pExtract2) {
     return ModuloArithmetic$.MODULE$.bvshl((ITerm) pExtract, (ITerm) pExtract2);
   }
 
+  @Override
+  protected IExpression rotateRight(IExpression pNumber, IExpression toRotate) {
+    // Princess does not support non-literal rotation, so we rewrite it to (bvor (bvlshr pNumber
+    // toRotate) (bvshl pNumber (bvsub size toRotate)))
+    final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize();
+    final IExpression size = this.makeBitvectorImpl(bitsize, bitsize);
+    final IExpression toRotateInRange =
+        ModuloArithmetic$.MODULE$.bvurem((ITerm) toRotate, (ITerm) size);
+    return or(
+        shiftRight(pNumber, toRotateInRange, false),
+        shiftLeft(pNumber, subtract(size, toRotateInRange)));
+  }
+
+  @Override
+  protected IExpression rotateLeft(IExpression pNumber, IExpression toRotate) {
+    // Princess does not support non-literal rotation, so we rewrite it to (bvor (bvshl pNumber
+    // toRotate) (bvlshr pNumber (bvsub size toRotate)))
+    final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize();
+    final IExpression size = this.makeBitvectorImpl(bitsize, bitsize);
+    final IExpression toRotateInRange =
+        ModuloArithmetic$.MODULE$.bvurem((ITerm) toRotate, (ITerm) size);
+    return or(
+        shiftLeft(pNumber, toRotateInRange),
+        shiftRight(pNumber, subtract(size, toRotateInRange), false));
+  }
+
   @Override
   protected IExpression concat(IExpression number, IExpression pAppend) {
     return ModuloArithmetic$.MODULE$.concat((ITerm) number, (ITerm) pAppend);

src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java

@@ -43,6 +43,7 @@
 import com.google.common.base.Preconditions;
 import com.google.common.base.Strings;
 import java.math.BigInteger;
+import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
 import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
 
 public class Yices2BitvectorFormulaManager
@@ -203,6 +204,30 @@ protected Integer rotateRightByConstant(Integer pNumber, int toRotate) {
     return yices_rotate_right(pNumber, toRotate);
   }
 
+  @Override
+  protected Integer rotateRight(Integer pNumber, Integer toRotate) {
+    // Yices2 does not support non-literal rotation, so we rewrite it to (bvor (bvlshr pNumber
+    // toRotate) (bvshl pNumber (bvsub size toRotate)))
+    final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize();
+    final Integer size = this.makeBitvectorImpl(bitsize, bitsize);
+    final Integer toRotateInRange = yices_bvrem(toRotate, size);
+    return or(
+        shiftRight(pNumber, toRotateInRange, false),
+        shiftLeft(pNumber, subtract(size, toRotateInRange)));
+  }
+
+  @Override
+  protected Integer rotateLeft(Integer pNumber, Integer toRotate) {
+    // Yices2 does not support non-literal rotation, so we rewrite it to (bvor (bvshl pNumber
+    // toRotate) (bvlshr pNumber (bvsub size toRotate)))
+    final int bitsize = ((BitvectorType) formulaCreator.getFormulaType(pNumber)).getSize();
+    final Integer size = this.makeBitvectorImpl(bitsize, bitsize);
+    final Integer toRotateInRange = yices_bvrem(toRotate, size);
+    return or(
+        shiftLeft(pNumber, toRotateInRange),
+        shiftRight(pNumber, subtract(size, toRotateInRange), false));
+  }
+
   @Override
   protected Integer concat(Integer pNumber, Integer pAppend) {
     return yices_bvconcat2(pNumber, pAppend);

src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java

@@ -466,8 +466,10 @@ public void bvRotateByConstant() throws SolverException, InterruptedException {
 
   @Test
   public void bvRotateByBV() throws SolverException, InterruptedException {
-    requireBitvectorRotation();
-
+    assume()
+        .withMessage("Princess seems to be way too slow for this test")
+        .that(solver)
+        .isNotEqualTo(Solvers.PRINCESS);
     for (int bitsize : new int[] {8, 13, 25, 31}) {
       BitvectorFormula zero = bvmgr.makeBitvector(bitsize, 0);
       BitvectorFormula a = bvmgr.makeVariable(bitsize, "a" + bitsize);
@@ -502,8 +504,6 @@ public void bvRotateByBV() throws SolverException, InterruptedException {
 
   @Test
   public void bvIsIdenticalAfterFullRotation() throws SolverException, InterruptedException {
-    requireBitvectorRotation();
-
     for (int bitsize : new int[] {2, 4, 8, 16, 32, 55}) {
       BitvectorFormula number = bvmgr.makeVariable(bitsize, "NUM_ROT_" + bitsize);
       for (int multiplier : new int[] {0, 1, 2, 5, 17, 37, 111, 1111}) {

src/org/sosy_lab/java_smt/test/SolverBasedTest0.java

@@ -233,15 +233,6 @@ protected final void requireBitvectorToInt() {
         .isNotEqualTo(Solvers.YICES2);
   }
 
-  protected final void requireBitvectorRotation() {
-    assume()
-        .withMessage(
-            "Solver %s does not yet support the rotation of bitvectors by arbitrary shift",
-            solverToUse())
-        .that(solverToUse())
-        .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.MATHSAT5, Solvers.PRINCESS, Solvers.YICES2);
-  }
-
   /** Skip test if the solver does not support quantifiers. */
   protected final void requireQuantifiers() {
     assume()