Merge pull request #497 from sosy-lab/z3/version-update-from-4.14.0

Z3/version update from 4.14.0 to 4.15.2

Author: kfriedberger

lib/ivy.xml

@@ -189,7 +189,7 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- Solver Binaries -->
         <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.11-sosy1" conf="runtime-mathsat-x64->solver-mathsat-x64; runtime-mathsat-arm64->solver-mathsat-arm64" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.14.0" conf="runtime-z3-x64->solver-z3-x64; runtime-z3-arm64->solver-z3-arm64; contrib->sources,javadoc" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.15.2" conf="runtime-z3-x64->solver-z3-x64; runtime-z3-arm64->solver-z3-arm64; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.9.0-gef441e1c" conf="runtime-opensmt-x64->solver-opensmt-x64; runtime-opensmt-arm64->solver-opensmt-arm64; contrib->sources,javadoc"/>
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.3-sosy1" conf="runtime-optimathsat->solver-optimathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />

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

@@ -340,7 +340,7 @@ public BitvectorFormula rotateLeft(BitvectorFormula pNumber, BitvectorFormula pT
   protected TFormulaInfo rotateLeft(TFormulaInfo pNumber, TFormulaInfo pToRotate) {
     int length = getLength(wrap(pNumber));
     final TFormulaInfo lengthAsBv = makeBitvectorImpl(length, length);
-    final TFormulaInfo toRotateInRange = smodulo(pToRotate, lengthAsBv);
+    final TFormulaInfo toRotateInRange = remainder(pToRotate, lengthAsBv, false);
     return or(
         shiftLeft(pNumber, toRotateInRange),
         shiftRight(pNumber, subtract(lengthAsBv, toRotateInRange), false));
@@ -373,7 +373,7 @@ public BitvectorFormula rotateRight(BitvectorFormula pNumber, BitvectorFormula p
   protected TFormulaInfo rotateRight(TFormulaInfo pNumber, TFormulaInfo pToRotate) {
     int length = getLength(wrap(pNumber));
     final TFormulaInfo lengthAsBv = makeBitvectorImpl(length, length);
-    final TFormulaInfo toRotateInRange = smodulo(pToRotate, lengthAsBv);
+    final TFormulaInfo toRotateInRange = remainder(pToRotate, lengthAsBv, false);
     return or(
         shiftRight(pNumber, toRotateInRange, false),
         shiftLeft(pNumber, subtract(lengthAsBv, toRotateInRange)));

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

@@ -463,12 +463,20 @@ public void bvRotateByConstant() throws SolverException, InterruptedException {
 
   @Test
   public void bvRotateByBV() throws SolverException, InterruptedException {
-    assume()
-        .withMessage("Princess is too slow for this test")
-        .that(solver)
-        .isNotEqualTo(Solvers.PRINCESS);
+    int[] bitsizes;
+    switch (solverToUse()) {
+      case PRINCESS:
+        bitsizes = new int[] {2, 3}; // Princess is too slow for larger bitvectors
+        break;
+      case Z3:
+        bitsizes = new int[] {2, 3, 4, 8}; // Z3 is too slow for larger bitvectors since v4.15.0
+        break;
+      default:
+        bitsizes = new int[] {2, 3, 4, 8, 13, 25, 31};
+        break;
+    }
 
-    for (int bitsize : new int[] {8, 13, 25, 31}) {
+    for (int bitsize : bitsizes) {
       BitvectorFormula zero = bvmgr.makeBitvector(bitsize, 0);
       BitvectorFormula a = bvmgr.makeVariable(bitsize, "a" + bitsize);
       BitvectorFormula b = bvmgr.makeVariable(bitsize, "b" + bitsize);
@@ -600,6 +608,16 @@ public void bvModulo() throws SolverException, InterruptedException {
     assertThatFormula(bvmgr.equal(bvmgr.smodulo(minusTen, minusThree), minusOne)).isTautological();
   }
 
+  @Test
+  public void bvModulo2() throws SolverException, InterruptedException {
+    BitvectorFormula one = bvmgr.makeBitvector(2, 1);
+    BitvectorFormula two = bvmgr.makeBitvector(2, 2);
+    BitvectorFormula three = bvmgr.makeBitvector(2, 3);
+
+    // check that SMOD works for small bitvectors: 1_2 % 2_2 == 3_2 or 01 % 10 == 11
+    assertThatFormula(bvmgr.equal(bvmgr.smodulo(one, two), three)).isTautological();
+  }
+
   @Test
   public void bvModuloByZero() throws SolverException, InterruptedException {
     BitvectorFormula ten = bvmgr.makeBitvector(8, 10);

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

@@ -51,8 +51,8 @@ public void rotateLeftTest() {
                 FunctionDeclarationKind.ITE,
                 FunctionDeclarationKind.EQ,
                 FunctionDeclarationKind.EQ,
-                FunctionDeclarationKind.BV_SMOD,
-                FunctionDeclarationKind.BV_SMOD,
+                FunctionDeclarationKind.BV_UREM,
+                FunctionDeclarationKind.BV_UREM,
                 FunctionDeclarationKind.BV_LSHR,
                 FunctionDeclarationKind.BV_SUB);
         break;
@@ -62,8 +62,8 @@ public void rotateLeftTest() {
             .containsExactly(
                 FunctionDeclarationKind.BV_OR,
                 FunctionDeclarationKind.BV_SHL,
-                FunctionDeclarationKind.BV_SMOD,
-                FunctionDeclarationKind.BV_SMOD,
+                FunctionDeclarationKind.BV_UREM,
+                FunctionDeclarationKind.BV_UREM,
                 FunctionDeclarationKind.BV_LSHR,
                 FunctionDeclarationKind.BV_SUB);
         break;
@@ -114,8 +114,8 @@ public void rotateRightTest() {
                 FunctionDeclarationKind.ITE,
                 FunctionDeclarationKind.EQ,
                 FunctionDeclarationKind.EQ,
-                FunctionDeclarationKind.BV_SMOD,
-                FunctionDeclarationKind.BV_SMOD,
+                FunctionDeclarationKind.BV_UREM,
+                FunctionDeclarationKind.BV_UREM,
                 FunctionDeclarationKind.BV_SHL,
                 FunctionDeclarationKind.BV_SUB);
         break;
@@ -125,8 +125,8 @@ public void rotateRightTest() {
             .containsExactly(
                 FunctionDeclarationKind.BV_OR,
                 FunctionDeclarationKind.BV_SHL,
-                FunctionDeclarationKind.BV_SMOD,
-                FunctionDeclarationKind.BV_SMOD,
+                FunctionDeclarationKind.BV_UREM,
+                FunctionDeclarationKind.BV_UREM,
                 FunctionDeclarationKind.BV_LSHR,
                 FunctionDeclarationKind.BV_SUB);
         break;