diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java index 9a24432e8d..2e8a3e1419 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4BitvectorFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java index 04674ca107..1e72646d88 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5BitvectorFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java index c2dfb0d6d5..bc52b33e22 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5BitvectorFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java index dfb1f2ed30..a4649fed7e 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessBitvectorFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java index 3117bd8de7..84724174ed 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2BitvectorFormulaManager.java +++ b/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); diff --git a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java index 6c857fcc8f..02badbc804 100644 --- a/src/org/sosy_lab/java_smt/test/BitvectorFormulaManagerTest.java +++ b/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}) { diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 20fb612d65..d57494e017 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/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()