adding tests for Arrays with BV-elements.
Previous versions of Princess did not yet support to create Arrays with BV elements.
We should check whether there was an improvement.
This check is a first (failing) step towards that.
If Princess can not handle this part, we can disable the tests.
@@ -10,6 +10,7 @@ package org.sosy_lab.java_smt.test;
import static com.google.common.truth.Truth.assertThat;
import static com.google.common.truth.Truth.assertWithMessage;
+import static com.google.common.truth.TruthJUnit.assume;
import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
import java.math.BigInteger;
@@ -22,6 +23,7 @@ import org.junit.runners.Parameterized;
import org.junit.runners.Parameterized.Parameter;
import org.junit.runners.Parameterized.Parameters;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
+import org.sosy_lab.java_smt.api.ArrayFormula;
import org.sosy_lab.java_smt.api.BitvectorFormula;
import org.sosy_lab.java_smt.api.FormulaType;
import org.sosy_lab.java_smt.api.FormulaType.BitvectorType;
@@ -38,6 +40,8 @@ import org.sosy_lab.java_smt.api.SolverException;
@RunWith(Parameterized.class)
public class BitvectorFormulaManagerTest extends SolverBasedTest0 {
+ private static final BitvectorType bvType4 = FormulaType.getBitvectorTypeWithSize(4);
+
@Parameters(name = "{0}")
public static Object[] getAllSolvers() {
return Solvers.values();
@@ -358,4 +362,34 @@ public class BitvectorFormulaManagerTest extends SolverBasedTest0 {
BitvectorFormula bv = bvmgr.makeBitvector(2, 4);
bvmgr.extend(bv, -1, true);
}
+
+ @Test
+ public void bvIntArray() {
+ requireArrays();
+ assume()
+ .withMessage("Solver %s does not support arrays with integer index", solverToUse())
+ .that(solverToUse())
+ .isNotEqualTo(Solvers.BOOLECTOR);
+
+ BitvectorFormula bv = bvmgr.makeBitvector(4, 3);
+ ArrayFormula<IntegerFormula, BitvectorFormula> arr =
+ amgr.makeArray("arr", FormulaType.IntegerType, bvType4);
+ IntegerFormula index = imgr.makeNumber(12);
+ arr = amgr.store(arr, index, bv);
+
+ assertThat(mgr.getFormulaType(arr))
+ .isEqualTo(FormulaType.getArrayType(FormulaType.IntegerType, bvType4));
+ }
+
+ @Test
+ public void bvBvArray() {
+ requireArrays();
+
+ BitvectorFormula bv = bvmgr.makeBitvector(4, 3);
+ ArrayFormula<BitvectorFormula, BitvectorFormula> arr = amgr.makeArray("arr", bvType4, bvType4);
+ BitvectorFormula index = bvmgr.makeBitvector(4, 2);
+ arr = amgr.store(arr, index, bv);
+
+ assertThat(mgr.getFormulaType(arr)).isEqualTo(FormulaType.getArrayType(bvType4, bvType4));
+ }
}
