Add rotation operations to BitvectorFormulaManager

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

@@ -266,6 +266,18 @@ BooleanFormula greaterOrEquals(
    */
   BitvectorFormula shiftLeft(BitvectorFormula number, BitvectorFormula toShift);
 
+  /**
+   * This method returns a term representing the right rotation of number by toRotate. The result
+   * has the same length as the given number.
+   */
+  BitvectorFormula rotateRight(BitvectorFormula number, BitvectorFormula toRotate);
+
+  /**
+   * This method returns a term representing the left shift of number by toRotate. The result has
+   * the same length as the given number.
+   */
+  BitvectorFormula rotateLeft(BitvectorFormula number, BitvectorFormula toRotate);
+
   /** Concatenate two bitvectors. */
   BitvectorFormula concat(BitvectorFormula prefix, BitvectorFormula suffix);
 

src/org/sosy_lab/java_smt/basicimpl/AbstractBitvectorFormulaManager.java

@@ -314,6 +314,28 @@ public BitvectorFormula shiftLeft(BitvectorFormula pNumber, BitvectorFormula toS
 
   protected abstract TFormulaInfo shiftLeft(TFormulaInfo pExtract, TFormulaInfo pExtract2);
 
+  /** Return a term representing the right rotation of number by toRotate. */
+  @Override
+  public BitvectorFormula rotateRight(BitvectorFormula pNumber, BitvectorFormula toRotate) {
+    TFormulaInfo param1 = extractInfo(pNumber);
+    TFormulaInfo param2 = extractInfo(toRotate);
+
+    return wrap(rotateRight(param1, param2));
+  }
+
+  protected abstract TFormulaInfo rotateRight(TFormulaInfo pNumber, TFormulaInfo toRotate);
+
+  /** Return a term representing the left rotation of number by toRotate. */
+  @Override
+  public BitvectorFormula rotateLeft(BitvectorFormula pNumber, BitvectorFormula toRotate) {
+    TFormulaInfo param1 = extractInfo(pNumber);
+    TFormulaInfo param2 = extractInfo(toRotate);
+
+    return wrap(rotateLeft(param1, param2));
+  }
+
+  protected abstract TFormulaInfo rotateLeft(TFormulaInfo pNumber, TFormulaInfo toRotate);
+
   @Override
   public final BitvectorFormula concat(BitvectorFormula pNumber, BitvectorFormula pAppend) {
     TFormulaInfo param1 = extractInfo(pNumber);

src/org/sosy_lab/java_smt/delegate/statistics/StatisticsBitvectorFormulaManager.java

@@ -178,6 +178,18 @@ public BitvectorFormula shiftLeft(BitvectorFormula pNumber, BitvectorFormula pTo
     return delegate.shiftLeft(pNumber, pToShift);
   }
 
+  @Override
+  public BitvectorFormula rotateRight(BitvectorFormula pNumber, BitvectorFormula pToRotate) {
+    stats.bvOperations.getAndIncrement();
+    return delegate.rotateRight(pNumber, pToRotate);
+  }
+
+  @Override
+  public BitvectorFormula rotateLeft(BitvectorFormula pNumber, BitvectorFormula pToRotate) {
+    stats.bvOperations.getAndIncrement();
+    return delegate.rotateLeft(pNumber, pToRotate);
+  }
+
   @Override
   public BitvectorFormula concat(BitvectorFormula pNumber, BitvectorFormula pAppend) {
     stats.bvOperations.getAndIncrement();

src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedBitvectorFormulaManager.java

@@ -204,6 +204,20 @@ public BitvectorFormula shiftLeft(BitvectorFormula pNumber, BitvectorFormula pTo
     }
   }
 
+  @Override
+  public BitvectorFormula rotateRight(BitvectorFormula pNumber, BitvectorFormula pToRotate) {
+    synchronized (sync) {
+      return delegate.rotateRight(pNumber, pToRotate);
+    }
+  }
+
+  @Override
+  public BitvectorFormula rotateLeft(BitvectorFormula pNumber, BitvectorFormula pToRotate) {
+    synchronized (sync) {
+      return delegate.rotateLeft(pNumber, pToRotate);
+    }
+  }
+
   @Override
   public BitvectorFormula concat(BitvectorFormula pNumber, BitvectorFormula pAppend) {
     synchronized (sync) {

src/org/sosy_lab/java_smt/solvers/boolector/BoolectorBitvectorFormulaManager.java

@@ -16,6 +16,8 @@
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_neg;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_not;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_or;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_rol;
+import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_ror;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sdiv;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sext;
 import static org.sosy_lab.java_smt.solvers.boolector.BtorJNI.boolector_sgt;
@@ -187,6 +189,16 @@ public Long shiftLeft(Long bitVec, Long toShift) {
     return boolector_sll(btor, bitVec, toShift);
   }
 
+  @Override
+  protected Long rotateRight(Long pNumber, Long toRotate) {
+    return boolector_ror(btor, pNumber, toRotate);
+  }
+
+  @Override
+  protected Long rotateLeft(Long pNumber, Long toRotate) {
+    return boolector_rol(btor, pNumber, toRotate);
+  }
+
   @Override
   public Long concat(Long bitVec, Long bitVecAppend) {
     return boolector_concat(btor, bitVec, bitVecAppend);

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

@@ -84,6 +84,24 @@ protected Expr shiftLeft(Expr pParam1, Expr pParam2) {
     return exprManager.mkExpr(Kind.BITVECTOR_SHL, pParam1, pParam2);
   }
 
+  @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);
+    return or(shiftRight(pNumber, toRotate, false), shiftLeft(pNumber, subtract(size, toRotate)));
+  }
+
+  @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);
+    return or(shiftLeft(pNumber, toRotate), shiftRight(pNumber, subtract(size, toRotate), 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
@@ -125,6 +126,24 @@ protected Term shiftLeft(Term pParam1, Term pParam2) {
     return solver.mkTerm(Kind.BITVECTOR_SHL, pParam1, pParam2);
   }
 
+  @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);
+    return or(shiftRight(pNumber, toRotate, false), shiftLeft(pNumber, subtract(size, toRotate)));
+  }
+
+  @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);
+    return or(shiftLeft(pNumber, toRotate), shiftRight(pNumber, subtract(size, toRotate), false));
+  }
+
   @Override
   protected Term not(Term pParam1) {
     return solver.mkTerm(Kind.BITVECTOR_NOT, pParam1);

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

@@ -38,6 +38,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. */
@@ -125,6 +126,24 @@ public Long shiftLeft(Long number, Long toShift) {
     return msat_make_bv_lshl(mathsatEnv, number, toShift);
   }
 
+  @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 = this.makeBitvectorImpl(bitsize, bitsize);
+    return or(shiftRight(pNumber, toRotate, false), shiftLeft(pNumber, subtract(size, toRotate)));
+  }
+
+  @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);
+    return or(shiftLeft(pNumber, toRotate), shiftRight(pNumber, subtract(size, toRotate), 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,24 @@ 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);
+    return or(shiftRight(pNumber, toRotate, false), shiftLeft(pNumber, subtract(size, toRotate)));
+  }
+
+  @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);
+    return or(shiftLeft(pNumber, toRotate), shiftRight(pNumber, subtract(size, toRotate), 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

@@ -41,6 +41,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
@@ -191,6 +192,24 @@ protected Integer shiftLeft(Integer pNumber, Integer pToShift) {
     return yices_bvshl(pNumber, pToShift);
   }
 
+  @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);
+    return or(shiftRight(pNumber, toRotate, false), shiftLeft(pNumber, subtract(size, toRotate)));
+  }
+
+  @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);
+    return or(shiftLeft(pNumber, toRotate), shiftRight(pNumber, subtract(size, toRotate), false));
+  }
+
   @Override
   protected Integer concat(Integer pNumber, Integer pAppend) {
     return yices_bvconcat2(pNumber, pAppend);

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

@@ -82,6 +82,16 @@ public Long shiftLeft(Long number, Long toShift) {
     return Native.mkBvshl(z3context, number, toShift);
   }
 
+  @Override
+  protected Long rotateRight(Long pNumber, Long toRotate) {
+    return Native.mkExtRotateRight(z3context, pNumber, toRotate);
+  }
+
+  @Override
+  protected Long rotateLeft(Long pNumber, Long toRotate) {
+    return Native.mkExtRotateLeft(z3context, pNumber, toRotate);
+  }
+
   @Override
   public Long not(Long pBits) {
     return Native.mkBvnot(z3context, pBits);

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

@@ -397,4 +397,29 @@ public void bvVarDistinct() throws SolverException, InterruptedException {
     assertThatFormula(bvmgr.distinct(List.of(a, a))).isUnsatisfiable();
     assertThatFormula(bvmgr.distinct(List.of(num3, num3))).isUnsatisfiable();
   }
+
+  @Test
+  public void bvRotateLeft() throws SolverException, InterruptedException {
+    // (ROL 0001 0010) == 0100
+    // (ROL 0100 0010) == 0001
+    BitvectorFormula bf1 = bvmgr.makeBitvector(4, BigInteger.ONE);
+    BitvectorFormula bf2 = bvmgr.makeBitvector(4, BigInteger.TWO);
+    BitvectorFormula bf3 = bvmgr.makeBitvector(4, BigInteger.valueOf(4));
+
+    assertThatFormula(bvmgr.equal(bvmgr.rotateLeft(bf1, bf2), bf3)).isTautological();
+    assertThatFormula(bvmgr.equal(bvmgr.rotateLeft(bf3, bf2), bf1)).isTautological();
+  }
+
+  @Test
+  public void bvRotateRight() throws SolverException, InterruptedException {
+    // (ROR 0001 0011) == 0010
+    // (ROR 0010 0011) == 0100
+    BitvectorFormula bf1 = bvmgr.makeBitvector(4, BigInteger.ONE);
+    BitvectorFormula bf2 = bvmgr.makeBitvector(4, BigInteger.valueOf(3));
+    BitvectorFormula bf3 = bvmgr.makeBitvector(4, BigInteger.TWO);
+    BitvectorFormula bf4 = bvmgr.makeBitvector(4, BigInteger.valueOf(4));
+
+    assertThatFormula(bvmgr.equal(bvmgr.rotateRight(bf1, bf2), bf3)).isTautological();
+    assertThatFormula(bvmgr.equal(bvmgr.rotateRight(bf3, bf2), bf4)).isTautological();
+  }
 }