diff --git a/.idea/ant.xml b/.idea/ant.xml index 3e3b7e7277..52ce37416f 100644 --- a/.idea/ant.xml +++ b/.idea/ant.xml @@ -1,19 +1,8 @@ - - - - + \ No newline at end of file diff --git a/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java index 8d872c554e..46d6e8e629 100644 --- a/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java @@ -61,6 +61,30 @@ ArrayFormula store( ArrayFormula makeArray( String pName, ArrayFormulaType type); + /** Create a new array constant with uninitialized values. */ + , FTE extends FormulaType> + ArrayFormula makeArray(FTI pIndexType, FTE pElementType); + + /** Create a new array constant with uninitialized values. */ + ArrayFormula makeArray( + ArrayFormulaType type); + + /** + * Create a new array constant with values initialized to elseElem. + * + * @param elseElem: The default value of all entries in the array. + */ + , FTE extends FormulaType> + ArrayFormula makeArray(TE elseElem, FTI pIndexType, FTE pElementType); + + /** + * Create a new array constant with values initialized to elseElem. + * + * @param elseElem: The default value of all entries in the array. + */ + ArrayFormula makeArray( + TE elseElem, ArrayFormulaType type); + /** Make a {@link BooleanFormula} that represents the equality of two {@link ArrayFormula}. */ BooleanFormula equivalence( ArrayFormula pArray1, ArrayFormula pArray2); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java index b809e45854..206a6b213f 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java @@ -80,6 +80,56 @@ ArrayFormula makeArray(String pName, FTI pIndexType, FTE pElementType) { protected abstract TFormulaInfo internalMakeArray( String pName, FormulaType pIndexType, FormulaType pElementType); + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(FTI pIndexType, FTE pElementType) { + final TFormulaInfo arrayConst = internalMakeArray(pIndexType, pElementType); + return getFormulaCreator().encapsulateArray(arrayConst, pIndexType, pElementType); + } + + @Override + public ArrayFormula makeArray( + ArrayFormulaType type) { + final TFormulaInfo arrayConst = internalMakeArray(type.getIndexType(), type.getElementType()); + return getFormulaCreator() + .encapsulateArray(arrayConst, type.getIndexType(), type.getElementType()); + } + + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(TE elseElem, FTI pIndexType, FTE pElementType) { + final TFormulaInfo arrayConst = + internalMakeArray(extractInfo(elseElem), pIndexType, pElementType); + return getFormulaCreator().encapsulateArray(arrayConst, pIndexType, pElementType); + } + + @Override + public ArrayFormula makeArray( + TE elseElem, ArrayFormulaType type) { + final TFormulaInfo arrayConst = + internalMakeArray(extractInfo(elseElem), type.getIndexType(), type.getElementType()); + return getFormulaCreator() + .encapsulateArray(arrayConst, type.getIndexType(), type.getElementType()); + } + + protected TFormulaInfo internalMakeArray( + FormulaType pIndexType, FormulaType pElementType) { + throw new UnsupportedOperationException("Array literals are not supported."); + } + + protected TFormulaInfo internalMakeArray( + TFormulaInfo elseElem, FormulaType pIndexType, FormulaType pElementType) { + throw new UnsupportedOperationException("Initialized arrays are not supported."); + } + @Override public FormulaType getIndexType(ArrayFormula pArray) { return getFormulaCreator().getArrayFormulaIndexType(pArray); diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsArrayFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsArrayFormulaManager.java index 227548a9fd..69a6481cb9 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsArrayFormulaManager.java @@ -60,6 +60,42 @@ public ArrayFormula makeArray( return delegate.makeArray(pName, pType); } + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(FTI pIndexType, FTE pElementType) { + stats.arrayOperations.getAndIncrement(); + return delegate.makeArray(pIndexType, pElementType); + } + + @Override + public ArrayFormula makeArray( + ArrayFormulaType type) { + stats.arrayOperations.getAndIncrement(); + return delegate.makeArray(type); + } + + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(TE elseElem, FTI pIndexType, FTE pElementType) { + stats.arrayOperations.getAndIncrement(); + return delegate.makeArray(elseElem, pIndexType, pElementType); + } + + @Override + public ArrayFormula makeArray( + TE elseElem, ArrayFormulaType type) { + stats.arrayOperations.getAndIncrement(); + return delegate.makeArray(elseElem, type); + } + @Override public BooleanFormula equivalence( ArrayFormula pArray1, ArrayFormula pArray2) { diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedArrayFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedArrayFormulaManager.java index bbf99755d2..0a7dcbdc45 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedArrayFormulaManager.java @@ -65,6 +65,46 @@ public ArrayFormula makeArray( } } + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(FTI pIndexType, FTE pElementType) { + synchronized (sync) { + return delegate.makeArray(pIndexType, pElementType); + } + } + + @Override + public ArrayFormula makeArray( + ArrayFormulaType type) { + synchronized (sync) { + return delegate.makeArray(type); + } + } + + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(TE elseElem, FTI pIndexType, FTE pElementType) { + synchronized (sync) { + return delegate.makeArray(elseElem, pIndexType, pElementType); + } + } + + @Override + public ArrayFormula makeArray( + TE elseElem, ArrayFormulaType type) { + synchronized (sync) { + return delegate.makeArray(elseElem, type); + } + } + @Override public BooleanFormula equivalence( ArrayFormula pArray1, ArrayFormula pArray2) { diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java index 7df7207c20..e78c19ce04 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java @@ -46,6 +46,15 @@ protected Term internalMakeArray( return getFormulaCreator().makeVariable(cvc5ArrayType, pName); } + @Override + protected Term internalMakeArray( + Term elseElem, FormulaType pIndexType, FormulaType pElementType) { + final ArrayFormulaType arrayFormulaType = + FormulaType.getArrayType(pIndexType, pElementType); + final Sort cvc5ArrayType = toSolverType(arrayFormulaType); + return solver.mkConstArray(cvc5ArrayType, elseElem); + } + @Override protected Term equivalence(Term pArray1, Term pArray2) { return solver.mkTerm(Kind.EQUAL, pArray1, pArray2); diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5ArrayFormulaManager.java index ab53b1544e..6eac77ee62 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5ArrayFormulaManager.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.solvers.mathsat5; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_array_const; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_array_read; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_array_write; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal; @@ -48,6 +49,15 @@ protected Long internalMakeArray( return getFormulaCreator().makeVariable(mathsatArrayType, pName); } + @Override + protected Long internalMakeArray( + Long elseElem, FormulaType pIndexType, FormulaType pElementType) { + final ArrayFormulaType arrayFormulaType = + FormulaType.getArrayType(pIndexType, pElementType); + final Long mathsatArrayType = toSolverType(arrayFormulaType); + return msat_make_array_const(mathsatEnv, mathsatArrayType, elseElem); + } + @Override protected Long equivalence(Long pArray1, Long pArray2) { return msat_make_equal(mathsatEnv, pArray1, pArray2); diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3ArrayFormulaManager.java index d3bd7b83d7..9b2dbde479 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3ArrayFormulaManager.java @@ -9,6 +9,7 @@ package org.sosy_lab.java_smt.solvers.z3; import com.microsoft.z3.Native; +import java.util.List; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; @@ -45,6 +46,22 @@ protected Long internalMakeArray( return getFormulaCreator().makeVariable(z3ArrayType, pName); } + @Override + protected Long internalMakeArray( + FormulaType pIndexType, FormulaType pElementType) { + long func = + getFormulaCreator() + .declareUFImpl( + "__unnamed_arr", toSolverType(pElementType), List.of(toSolverType(pIndexType))); + return Native.mkAsArray(z3context, func); + } + + @Override + protected Long internalMakeArray( + Long elseElem, FormulaType pIndexType, FormulaType pElementType) { + return Native.mkConstArray(z3context, toSolverType(pIndexType), elseElem); + } + @Override protected Long equivalence(Long pArray1, Long pArray2) { return Native.mkEq(z3context, pArray1, pArray2); diff --git a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java index e82ee0c294..8f7f724059 100644 --- a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java @@ -180,4 +180,155 @@ public void testFloatIndexFloatValue() throws SolverException, InterruptedExcept bmgr.not(fpmgr.equalWithFPSemantics(num2, amgr.select(arr2, num4)))); assertThatFormula(query).isUnsatisfiable(); } + + @Test + public void testArrayConst() throws SolverException, InterruptedException { + requireIntegers(); + requireArraysWithoutDefaultValue(); + + ArrayFormulaType type = + FormulaType.getArrayType(IntegerType, IntegerType); + ArrayFormula arr = amgr.makeArray(type); + + IntegerFormula num2 = imgr.makeNumber(2); + IntegerFormula num4 = imgr.makeNumber(4); + IntegerFormula num5 = imgr.makeNumber(5); + IntegerFormula numM1 = imgr.makeNumber(-1); + + // select(store(arr, i, j)) == j + assertThatFormula(imgr.equal(num4, amgr.select(amgr.store(arr, num2, num4), num2))) + .isTautological(); + // same, but checking whether unnamed arrays work well (i.e., not global) + assertThatFormula(imgr.equal(num5, amgr.select(amgr.store(arr, num2, num5), num2))) + .isTautological(); + // uninit array can read any value + assertThatFormula(imgr.equal(numM1, amgr.select(arr, num2))).isSatisfiable(); + + // name not taken for other types + IntegerFormula intVar = imgr.makeVariable("__unnamed_arr"); + assertThatFormula(imgr.equal(imgr.makeNumber(42), intVar)).isSatisfiable(); + + // name not taken for same-type arrays + ArrayFormula unnamedArrVar = + amgr.makeArray("__unnamed_arr", type); + assertThatFormula(imgr.equal(num4, amgr.select(amgr.store(unnamedArrVar, num2, num4), num2))) + .isTautological(); + } + + @Test + public void testArrayConstBv() throws SolverException, InterruptedException { + requireBitvectors(); + requireArraysWithoutDefaultValue(); + + ArrayFormulaType type = + FormulaType.getArrayType(getBitvectorTypeWithSize(4), getBitvectorTypeWithSize(4)); + ArrayFormula arr = amgr.makeArray(type); + + BitvectorFormula num2 = bvmgr.makeBitvector(4, 2); + BitvectorFormula num4 = bvmgr.makeBitvector(4, 4); + BitvectorFormula num5 = bvmgr.makeBitvector(4, 5); + BitvectorFormula numM1 = bvmgr.makeBitvector(4, -1); + + // select(store(arr, i, j)) == j + assertThatFormula(bvmgr.equal(num4, amgr.select(amgr.store(arr, num2, num4), num2))) + .isTautological(); + // same, but checking whether unnamed arrays work well (i.e., not global) + assertThatFormula(bvmgr.equal(num5, amgr.select(amgr.store(arr, num2, num5), num2))) + .isTautological(); + // uninit array can read any value + assertThatFormula(bvmgr.equal(numM1, amgr.select(arr, num2))).isSatisfiable(); + } + + @Test + public void testArrayConstMixed() throws SolverException, InterruptedException { + requireIntegers(); + requireBitvectors(); + requireArraysWithoutDefaultValue(); + + ArrayFormulaType typeIntInt = + FormulaType.getArrayType(IntegerType, IntegerType); + ArrayFormulaType typeBvInt = + FormulaType.getArrayType(getBitvectorTypeWithSize(4), IntegerType); + ArrayFormulaType typeBvBv = + FormulaType.getArrayType(getBitvectorTypeWithSize(4), getBitvectorTypeWithSize(4)); + ArrayFormulaType typeIntBv = + FormulaType.getArrayType(IntegerType, getBitvectorTypeWithSize(4)); + + ArrayFormula arrIntInt = amgr.makeArray(typeIntInt); + ArrayFormula arrBvInt = amgr.makeArray(typeBvInt); + ArrayFormula arrBvBv = amgr.makeArray(typeBvBv); + ArrayFormula arrIntBv = amgr.makeArray(typeIntBv); + + IntegerFormula num2 = imgr.makeNumber(2); + IntegerFormula num4 = imgr.makeNumber(4); + + BitvectorFormula bv2 = bvmgr.makeBitvector(4, 2); + BitvectorFormula bv4 = bvmgr.makeBitvector(4, 4); + + // select(store(arr, i, j), i) == select(store(arr, k, j), k) + assertThatFormula( + imgr.equal( + amgr.select(amgr.store(arrIntInt, num2, num4), num2), + amgr.select(amgr.store(arrBvInt, bv2, num4), bv2))) + .isTautological(); + + // select(store(arr, i, j), i) == select(store(arr, k, j), k) + assertThatFormula( + bvmgr.equal( + amgr.select(amgr.store(arrIntBv, num2, bv4), num2), + amgr.select(amgr.store(arrBvBv, bv2, bv4), bv2))) + .isTautological(); + } + + @Test + public void testArrayConstWithDefault() throws SolverException, InterruptedException { + requireIntegers(); + requireArraysWithDefaultValue(); + + ArrayFormulaType type = + FormulaType.getArrayType(IntegerType, IntegerType); + IntegerFormula num0 = imgr.makeNumber(0); + ArrayFormula arr = amgr.makeArray(num0, type); + + IntegerFormula num2 = imgr.makeNumber(2); + IntegerFormula num4 = imgr.makeNumber(4); + IntegerFormula num5 = imgr.makeNumber(5); + IntegerFormula numM1 = imgr.makeNumber(-1); + + // select(store(arr, i, j)) == j + assertThatFormula(imgr.equal(num4, amgr.select(amgr.store(arr, num2, num4), num2))) + .isTautological(); + // same, but checking whether unnamed arrays work well (i.e., not global) + assertThatFormula(imgr.equal(num5, amgr.select(amgr.store(arr, num2, num5), num2))) + .isTautological(); + // init array cannot read any value besides default + assertThatFormula(imgr.equal(numM1, amgr.select(arr, num2))).isUnsatisfiable(); + assertThatFormula(imgr.equal(num0, amgr.select(arr, num2))).isTautological(); + } + + @Test + public void testArrayConstBvWithDefault() throws SolverException, InterruptedException { + requireBitvectors(); + requireArraysWithDefaultValue(); + + ArrayFormulaType type = + FormulaType.getArrayType(getBitvectorTypeWithSize(4), getBitvectorTypeWithSize(4)); + BitvectorFormula num0 = bvmgr.makeBitvector(4, 0); + ArrayFormula arr = amgr.makeArray(num0, type); + + BitvectorFormula num2 = bvmgr.makeBitvector(4, 2); + BitvectorFormula num4 = bvmgr.makeBitvector(4, 4); + BitvectorFormula num5 = bvmgr.makeBitvector(4, 5); + BitvectorFormula numM1 = bvmgr.makeBitvector(4, -1); + + // select(store(arr, i, j)) == j + assertThatFormula(bvmgr.equal(num4, amgr.select(amgr.store(arr, num2, num4), num2))) + .isTautological(); + // same, but checking whether unnamed arrays work well (i.e., not global) + assertThatFormula(bvmgr.equal(num5, amgr.select(amgr.store(arr, num2, num5), num2))) + .isTautological(); + // init array cannot read any value besides default + assertThatFormula(bvmgr.equal(numM1, amgr.select(arr, num2))).isUnsatisfiable(); + assertThatFormula(bvmgr.equal(num0, amgr.select(arr, num2))).isTautological(); + } } diff --git a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java index 20fb612d65..444a110938 100644 --- a/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java +++ b/src/org/sosy_lab/java_smt/test/SolverBasedTest0.java @@ -258,6 +258,34 @@ protected final void requireQuantifiers() { .isNotNull(); } + /** Skip test if the solver does not support uninitialized array literals. */ + protected /*final*/ void requireArraysWithoutDefaultValue() { + assume() + .withMessage("Solver %s does not support arrays without default values", solverToUse()) + .that(solverToUse()) + .isNoneOf( + Solvers.OPENSMT, + Solvers.MATHSAT5, + Solvers.SMTINTERPOL, + Solvers.PRINCESS, + Solvers.CVC4, + Solvers.CVC5, + Solvers.BOOLECTOR); + } + + /** Skip test if the solver does not support initialized arrays. */ + protected /*final*/ void requireArraysWithDefaultValue() { + assume() + .withMessage("Solver %s does not support arrays with default values", solverToUse()) + .that(solverToUse()) + .isNoneOf( + Solvers.OPENSMT, + Solvers.SMTINTERPOL, + Solvers.PRINCESS, + Solvers.CVC4, + Solvers.BOOLECTOR); + } + protected final void requireFloats() { assume() .withMessage("Solver %s does not support the theory of floats", solverToUse())