From d5c780075213f01b0c1af7977ca18452d2abf674 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 1 Apr 2024 21:22:10 +0200 Subject: [PATCH 1/4] ArrayFormulaManager: use default methods in the interface to simplify code in the implementation. --- .../java_smt/api/ArrayFormulaManager.java | 19 +++++++++++++------ .../AbstractArrayFormulaManager.java | 7 ------- .../StatisticsArrayFormulaManager.java | 8 -------- .../SynchronizedArrayFormulaManager.java | 9 --------- 4 files changed, 13 insertions(+), 30 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java index 8d872c554e..a520b958b2 100644 --- a/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -48,18 +48,25 @@ ArrayFormula store( * * @param pIndexType The type of the array index * @param pElementType The type of the array elements - * @return Formula that represents the array */ , FTE extends FormulaType> ArrayFormula makeArray(String pName, FTI pIndexType, FTE pElementType); /** - * Declare a new array. + * Declare a new array with exactly the given name. + * + *

Please make sure that the given name is valid in SMT-LIB2. Take a look at {@link + * FormulaManager#isValidName} for further information. + * + *

This method does not quote or unquote the given name, but uses the plain name "AS IS". + * {@link Formula#toString} can return a different String than the given one. * - * @param pName The name of the array variable + * @param type The type of the array, consisting of index type and element type */ - ArrayFormula makeArray( - String pName, ArrayFormulaType type); + default ArrayFormula makeArray( + String pName, ArrayFormulaType type) { + return makeArray(pName, type.getIndexType(), type.getElementType()); + } /** Make a {@link BooleanFormula} that represents the equality of two {@link ArrayFormula}. */ BooleanFormula equivalence( diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java index b809e45854..daaa803384 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java @@ -15,7 +15,6 @@ import org.sosy_lab.java_smt.api.BooleanFormula; 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; @SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"}) public abstract class AbstractArrayFormulaManager @@ -59,12 +58,6 @@ public ArrayFormula store( protected abstract TFormulaInfo store( TFormulaInfo pArray, TFormulaInfo pIndex, TFormulaInfo pValue); - @Override - public ArrayFormula makeArray( - String pName, ArrayFormulaType type) { - return makeArray(pName, type.getIndexType(), type.getElementType()); - } - @Override public < TI extends Formula, 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..494bdbb428 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsArrayFormulaManager.java @@ -15,7 +15,6 @@ import org.sosy_lab.java_smt.api.BooleanFormula; 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; @SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"}) class StatisticsArrayFormulaManager implements ArrayFormulaManager { @@ -53,13 +52,6 @@ ArrayFormula makeArray(String pName, FTI pIndexType, FTE pElementType) { return delegate.makeArray(pName, pIndexType, pElementType); } - @Override - public ArrayFormula makeArray( - String pName, ArrayFormulaType pType) { - stats.arrayOperations.getAndIncrement(); - return delegate.makeArray(pName, pType); - } - @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..a0734299cd 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedArrayFormulaManager.java @@ -15,7 +15,6 @@ import org.sosy_lab.java_smt.api.BooleanFormula; 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; import org.sosy_lab.java_smt.api.SolverContext; @SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"}) @@ -57,14 +56,6 @@ ArrayFormula makeArray(String pName, FTI pIndexType, FTE pElementType) { } } - @Override - public ArrayFormula makeArray( - String pName, ArrayFormulaType pType) { - synchronized (sync) { - return delegate.makeArray(pName, pType); - } - } - @Override public BooleanFormula equivalence( ArrayFormula pArray1, ArrayFormula pArray2) { From 9b440b7a57860a3da8a107a4261497e3b0b79b67 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Mon, 1 Apr 2024 21:40:13 +0200 Subject: [PATCH 2/4] ArrayFormulaManager: add creation of array-literals to API and implement it for several solvers. Additionally, improve visitor for arrays. --- .../java_smt/api/ArrayFormulaManager.java | 18 +++ .../java_smt/api/FunctionDeclarationKind.java | 3 +- .../AbstractArrayFormulaManager.java | 15 +++ .../basicimpl/AbstractFormulaManager.java | 13 +- .../StatisticsArrayFormulaManager.java | 11 ++ .../SynchronizedArrayFormulaManager.java | 12 ++ .../BoolectorArrayFormulaManager.java | 7 ++ .../solvers/cvc4/CVC4ArrayFormulaManager.java | 15 ++- .../solvers/cvc4/CVC4FormulaCreator.java | 18 ++- .../solvers/cvc5/CVC5ArrayFormulaManager.java | 13 +- .../solvers/cvc5/CVC5FormulaCreator.java | 17 ++- .../mathsat5/Mathsat5ArrayFormulaManager.java | 16 ++- .../mathsat5/Mathsat5FormulaCreator.java | 5 +- .../opensmt/OpenSmtArrayFormulaManager.java | 12 +- .../princess/PrincessArrayFormulaManager.java | 15 ++- .../solvers/princess/PrincessEnvironment.java | 19 +++ .../princess/PrincessFormulaCreator.java | 2 + .../SmtInterpolArrayFormulaManager.java | 18 +-- .../SmtInterpolFormulaCreator.java | 4 +- .../solvers/z3/Z3ArrayFormulaManager.java | 14 ++- .../java_smt/solvers/z3/Z3FormulaCreator.java | 4 +- .../test/ArrayFormulaManagerTest.java | 66 ++++++++++ .../java_smt/test/SolverVisitorTest.java | 118 ++++++++++++++++-- 23 files changed, 379 insertions(+), 56 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java index a520b958b2..d2600652a4 100644 --- a/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/api/ArrayFormulaManager.java @@ -68,6 +68,24 @@ default ArrayFormula makeArray( return makeArray(pName, type.getIndexType(), type.getElementType()); } + /** + * 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(FTI pIndexType, FTE pElementType, TE elseElem); + + /** + * Create a new array constant with values initialized to elseElem. + * + * @param elseElem The default value of all entries in the array. + */ + default ArrayFormula makeArray( + ArrayFormulaType type, TE elseElem) { + return makeArray(type.getIndexType(), type.getElementType(), elseElem); + } + /** 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/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index c5932cd2eb..16075fa10f 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -33,9 +33,10 @@ public enum FunctionDeclarationKind { /** Distinct operator for a set of numeric formulas. */ DISTINCT, - /** Store and select on arrays. */ + /** Store and select on arrays, and constant initialization. */ STORE, SELECT, + CONST, // Simple arithmetic, // they work across integers and rationals. diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java index daaa803384..e2a85a78b6 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractArrayFormulaManager.java @@ -70,9 +70,24 @@ ArrayFormula makeArray(String pName, FTI pIndexType, FTE pElementType) { return getFormulaCreator().encapsulateArray(namedArrayFormula, pIndexType, pElementType); } + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(FTI pIndexType, FTE pElementType, TE elseElem) { + final TFormulaInfo arrayConst = + internalMakeArray(pIndexType, pElementType, extractInfo(elseElem)); + return getFormulaCreator().encapsulateArray(arrayConst, pIndexType, pElementType); + } + protected abstract TFormulaInfo internalMakeArray( String pName, FormulaType pIndexType, FormulaType pElementType); + protected abstract TFormulaInfo internalMakeArray( + FormulaType pIndexType, FormulaType pElementType, TFormulaInfo elseElem); + @Override public FormulaType getIndexType(ArrayFormula pArray) { return getFormulaCreator().getArrayFormulaIndexType(pArray); diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java index e131967ee2..5d1d8ba04b 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -17,6 +17,7 @@ import com.google.common.collect.ImmutableBiMap; import com.google.common.collect.ImmutableMap; import com.google.common.collect.ImmutableSet; +import com.google.common.collect.Iterables; import java.util.Arrays; import java.util.List; import java.util.Map; @@ -33,6 +34,7 @@ import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.FunctionDeclarationKind; import org.sosy_lab.java_smt.api.IntegerFormulaManager; import org.sosy_lab.java_smt.api.RationalFormulaManager; import org.sosy_lab.java_smt.api.SLFormulaManager; @@ -445,6 +447,15 @@ public T makeVariable(FormulaType formulaType, String nam @SuppressWarnings("unchecked") public T makeApplication( FunctionDeclaration declaration, List args) { + + if (declaration.getKind() == FunctionDeclarationKind.CONST) { + ArrayFormulaType arrayType = (ArrayFormulaType) declaration.getType(); + Formula elseElem = Iterables.getOnlyElement(args); + return (T) + arrayManager.makeArray( + arrayType.getIndexType(), getFormulaType(elseElem), Iterables.getOnlyElement(args)); + } + return formulaCreator.callFunction(declaration, args); } 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 494bdbb428..ff06c22abb 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsArrayFormulaManager.java @@ -52,6 +52,17 @@ ArrayFormula makeArray(String pName, FTI pIndexType, FTE pElementType) { return delegate.makeArray(pName, pIndexType, pElementType); } + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(FTI pIndexType, FTE pElementType, TE elseElem) { + stats.arrayOperations.getAndIncrement(); + return delegate.makeArray(pIndexType, pElementType, elseElem); + } + @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 a0734299cd..31d4a9506d 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedArrayFormulaManager.java @@ -56,6 +56,18 @@ ArrayFormula makeArray(String pName, FTI pIndexType, FTE pElementType) { } } + @Override + public < + TI extends Formula, + TE extends Formula, + FTI extends FormulaType, + FTE extends FormulaType> + ArrayFormula makeArray(FTI pIndexType, FTE pElementType, TE elseElem) { + synchronized (sync) { + return delegate.makeArray(pIndexType, pElementType, elseElem); + } + } + @Override public BooleanFormula equivalence( ArrayFormula pArray1, ArrayFormula pArray2) { diff --git a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorArrayFormulaManager.java index e09c515251..8215662655 100644 --- a/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/boolector/BoolectorArrayFormulaManager.java @@ -16,6 +16,7 @@ import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; +@SuppressWarnings("MethodTypeParameterName") public class BoolectorArrayFormulaManager extends AbstractArrayFormulaManager { @@ -64,6 +65,12 @@ protected Long internalMakeArray( return array; } + @Override + protected Long internalMakeArray( + FormulaType pIndexType, FormulaType pElementType, Long elseElem) { + throw new UnsupportedOperationException(); + } + @Override protected Long equivalence(Long pArray1, Long pArray2) { return BtorJNI.boolector_eq(btor, pArray1, pArray2); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4ArrayFormulaManager.java index 8d18e0c7ba..579d3788c3 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4ArrayFormulaManager.java @@ -8,15 +8,17 @@ package org.sosy_lab.java_smt.solvers.cvc4; +import edu.stanford.CVC4.ArrayStoreAll; +import edu.stanford.CVC4.ArrayType; import edu.stanford.CVC4.Expr; import edu.stanford.CVC4.ExprManager; import edu.stanford.CVC4.Kind; import edu.stanford.CVC4.Type; 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; import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; +@SuppressWarnings("MethodTypeParameterName") public class CVC4ArrayFormulaManager extends AbstractArrayFormulaManager { @@ -41,12 +43,17 @@ protected Expr store(Expr pArray, Expr pIndex, Expr pValue) { @SuppressWarnings("MethodTypeParameterName") protected Expr internalMakeArray( String pName, FormulaType pIndexType, FormulaType pElementType) { - final ArrayFormulaType arrayFormulaType = - FormulaType.getArrayType(pIndexType, pElementType); - final Type cvc4ArrayType = toSolverType(arrayFormulaType); + final Type cvc4ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); return getFormulaCreator().makeVariable(cvc4ArrayType, pName); } + @Override + protected Expr internalMakeArray( + FormulaType pIndexType, FormulaType pElementType, Expr elseElem) { + final Type cvc4ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); + return exprManager.mkConst(new ArrayStoreAll((ArrayType) cvc4ArrayType, elseElem)); + } + @Override protected Expr equivalence(Expr pArray1, Expr pArray2) { return exprManager.mkExpr(Kind.EQUAL, pArray1, pArray2); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index 6c14be55bd..28a882d106 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -16,6 +16,7 @@ import com.google.common.collect.ImmutableMap; import com.google.common.collect.Iterables; import com.google.common.primitives.Ints; +import edu.stanford.CVC4.ArrayStoreAll; import edu.stanford.CVC4.ArrayType; import edu.stanford.CVC4.BitVectorType; import edu.stanford.CVC4.Expr; @@ -323,6 +324,18 @@ public R visit(FormulaVisitor visitor, Formula formula, final Expr f) { return visitor.visitConstant(formula, f.getConstRoundingMode()); } else if (type.isString()) { return visitor.visitConstant(formula, f.getConstString()); + } else if (type.isArray()) { + ArrayStoreAll storeAll = f.getConstArrayStoreAll(); + Expr constant = storeAll.getExpr(); + return visitor.visitFunction( + formula, + ImmutableList.of(encapsulate(constant)), + FunctionDeclarationImpl.of( + getName(f), + getDeclarationKind(f), + ImmutableList.of(getFormulaTypeFromTermType(constant.getType())), + getFormulaType(f), + f.getKind())); } else { throw new UnsupportedOperationException("Unhandled constant " + f + " with type " + type); } @@ -506,6 +519,9 @@ private Expr normalize(Expr operator) { .put(Kind.REGEXP_INTER, FunctionDeclarationKind.RE_INTERSECT) .put(Kind.REGEXP_COMPLEMENT, FunctionDeclarationKind.RE_COMPLEMENT) .put(Kind.REGEXP_DIFF, FunctionDeclarationKind.RE_DIFFERENCE) + .put(Kind.SELECT, FunctionDeclarationKind.SELECT) + .put(Kind.STORE, FunctionDeclarationKind.STORE) + .put(Kind.STORE_ALL, FunctionDeclarationKind.CONST) .buildOrThrow(); private FunctionDeclarationKind getDeclarationKind(Expr f) { 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..f71e7aad7a 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5ArrayFormulaManager.java @@ -14,9 +14,9 @@ import io.github.cvc5.Term; 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; import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; +@SuppressWarnings("MethodTypeParameterName") public class CVC5ArrayFormulaManager extends AbstractArrayFormulaManager { private final Solver solver; @@ -40,12 +40,17 @@ protected Term store(Term pArray, Term pIndex, Term pValue) { @SuppressWarnings("MethodTypeParameterName") protected Term internalMakeArray( String pName, FormulaType pIndexType, FormulaType pElementType) { - final ArrayFormulaType arrayFormulaType = - FormulaType.getArrayType(pIndexType, pElementType); - final Sort cvc5ArrayType = toSolverType(arrayFormulaType); + final Sort cvc5ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); return getFormulaCreator().makeVariable(cvc5ArrayType, pName); } + @Override + protected Term internalMakeArray( + FormulaType pIndexType, FormulaType pElementType, Term elseElem) { + final Sort cvc5ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); + 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/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index ad9270331e..e90e0a7ef5 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2022 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -408,6 +408,18 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { } else if (f.isRoundingModeValue()) { return visitor.visitConstant(formula, f.getRoundingModeValue()); + } else if (f.isConstArray()) { + Term constant = f.getConstArrayBase(); + return visitor.visitFunction( + formula, + ImmutableList.of(encapsulate(constant)), + FunctionDeclarationImpl.of( + getName(f), + getDeclarationKind(f), + ImmutableList.of(getFormulaTypeFromTermType(constant.getSort())), + getFormulaType(f), + f.getKind())); + } else if (f.getKind() == Kind.VARIABLE) { // BOUND vars are used for all vars that are bound to a quantifier in CVC5. // We resubstitute them back to the original free. @@ -623,6 +635,9 @@ private Term normalize(Term operator) { .put(Kind.REGEXP_INTER, FunctionDeclarationKind.RE_INTERSECT) .put(Kind.REGEXP_COMPLEMENT, FunctionDeclarationKind.RE_COMPLEMENT) .put(Kind.REGEXP_DIFF, FunctionDeclarationKind.RE_DIFFERENCE) + .put(Kind.SELECT, FunctionDeclarationKind.SELECT) + .put(Kind.STORE, FunctionDeclarationKind.STORE) + .put(Kind.CONST_ARRAY, FunctionDeclarationKind.CONST) .build(); private FunctionDeclarationKind getDeclarationKind(Term f) { 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..05e5ffd6aa 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5ArrayFormulaManager.java @@ -8,15 +8,16 @@ 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; 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; import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; +@SuppressWarnings("MethodTypeParameterName") class Mathsat5ArrayFormulaManager extends AbstractArrayFormulaManager { private final long mathsatEnv; @@ -40,14 +41,17 @@ protected Long store(Long pArray, Long pIndex, Long pValue) { @SuppressWarnings("MethodTypeParameterName") protected Long internalMakeArray( String pName, FormulaType pIndexType, FormulaType pElementType) { - // throw new UnsupportedOperationException("Please implement me!"); - final ArrayFormulaType arrayFormulaType = - FormulaType.getArrayType(pIndexType, pElementType); - final Long mathsatArrayType = toSolverType(arrayFormulaType); - + final Long mathsatArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); return getFormulaCreator().makeVariable(mathsatArrayType, pName); } + @Override + protected Long internalMakeArray( + FormulaType pIndexType, FormulaType pElementType, Long elseElem) { + final Long mathsatArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); + 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/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index b5938894ab..6947cdc2d0 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -2,13 +2,14 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 package org.sosy_lab.java_smt.solvers.mathsat5; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_AND; +import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_ARRAY_CONST; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_ARRAY_READ; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_ARRAY_WRITE; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_ADD; @@ -408,6 +409,8 @@ private FunctionDeclarationKind getDeclarationKind(long pF) { return FunctionDeclarationKind.SELECT; case MSAT_TAG_ARRAY_WRITE: return FunctionDeclarationKind.STORE; + case MSAT_TAG_ARRAY_CONST: + return FunctionDeclarationKind.CONST; case MSAT_TAG_BV_EXTRACT: return FunctionDeclarationKind.BV_EXTRACT; diff --git a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtArrayFormulaManager.java index b41909ab13..0a4eee26f5 100644 --- a/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/opensmt/OpenSmtArrayFormulaManager.java @@ -10,13 +10,13 @@ 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; import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; import org.sosy_lab.java_smt.solvers.opensmt.api.Logic; import org.sosy_lab.java_smt.solvers.opensmt.api.PTRef; import org.sosy_lab.java_smt.solvers.opensmt.api.SRef; import org.sosy_lab.java_smt.solvers.opensmt.api.SymRef; +@SuppressWarnings("MethodTypeParameterName") public class OpenSmtArrayFormulaManager extends AbstractArrayFormulaManager { @@ -41,12 +41,16 @@ protected PTRef store(PTRef pArray, PTRef pIndex, PTRef pValue) { @SuppressWarnings("MethodTypeParameterName") protected PTRef internalMakeArray( String pName, FormulaType pIndexType, FormulaType pElementType) { - final ArrayFormulaType arrayFormulaType = - FormulaType.getArrayType(pIndexType, pElementType); - final SRef osmtArrayType = toSolverType(arrayFormulaType); + final SRef osmtArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); return getFormulaCreator().makeVariable(osmtArrayType, pName); } + @Override + protected PTRef internalMakeArray( + FormulaType pIndexType, FormulaType pElementType, PTRef elseElem) { + throw new UnsupportedOperationException(); + } + @Override protected PTRef equivalence(PTRef pArray1, PTRef pArray2) { return logic.mkEq(pArray1, pArray2); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessArrayFormulaManager.java index fbf85d40ea..5840adc98e 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessArrayFormulaManager.java @@ -10,13 +10,14 @@ import ap.parser.IExpression; import ap.parser.ITerm; +import ap.theories.ExtArray.ArraySort; import ap.types.Sort; 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; import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; +@SuppressWarnings("MethodTypeParameterName") class PrincessArrayFormulaManager extends AbstractArrayFormulaManager< IExpression, Sort, PrincessEnvironment, PrincessFunctionDeclaration> { @@ -44,13 +45,17 @@ protected IExpression store(IExpression pArray, IExpression pIndex, IExpression @SuppressWarnings("MethodTypeParameterName") protected IExpression internalMakeArray( String pName, FormulaType pIndexType, FormulaType pElementType) { - final ArrayFormulaType arrayFormulaType = - FormulaType.getArrayType(pIndexType, pElementType); - final Sort arrayType = toSolverType(arrayFormulaType); - + final Sort arrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); return getFormulaCreator().makeVariable(arrayType, pName); } + @Override + protected IExpression internalMakeArray( + FormulaType pIndexType, FormulaType pElementType, IExpression elseElem) { + final Sort arrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); + return env.makeConstArray((ArraySort) arrayType, (ITerm) elseElem); + } + @Override protected IExpression equivalence(IExpression pArray1, IExpression pArray2) { return ap.parser.IExpression.Eq$.MODULE$.apply((ITerm) pArray1, (ITerm) pArray2); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index c005ea4b52..981e9dd5c4 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -29,6 +29,7 @@ import ap.parser.SMTParser2InputAbsy.SMTType; import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; +import ap.theories.ExtArray; import ap.theories.ExtArray.ArraySort; import ap.theories.bitvectors.ModuloArithmetic; import ap.theories.rationals.Fractions.FractionSort$; @@ -47,6 +48,8 @@ import java.io.File; import java.io.IOException; import java.io.StringReader; +import java.lang.reflect.InvocationTargetException; +import java.lang.reflect.Method; import java.nio.file.Path; import java.util.ArrayDeque; import java.util.ArrayList; @@ -608,6 +611,22 @@ public ITerm makeStore(ITerm array, ITerm index, ITerm value) { return new IFunApp(arraySort.theory().store(), toSeq(args)); } + public ITerm makeConstArray(ArraySort arraySort, ITerm elseTerm) { + // return new IFunApp(arraySort.theory().const(), elseTerm); // I love Scala! So simple! ;-) + + // Scala uses keywords that are illegal in Java. Thus, we use reflection to access the method. + // TODO we should contact the developers of Princess and ask for a renaming. + final IFunction constArrayOp; + try { + Method constMethod = ExtArray.class.getMethod("const"); + constArrayOp = (IFunction) constMethod.invoke(arraySort.theory()); + } catch (IllegalAccessException | NoSuchMethodException | InvocationTargetException pE) { + throw new RuntimeException(pE); + } + + return new IFunApp(constArrayOp, toSeq(ImmutableList.of(elseTerm))); + } + public boolean hasArrayType(IExpression exp) { if (exp instanceof ITerm) { final ITerm t = (ITerm) exp; diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 52f6b0d2f8..7565424719 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -427,6 +427,8 @@ private FunctionDeclarationKind getDeclarationKind(IExpression input) { return FunctionDeclarationKind.SELECT; } else if (ExtArray.Store$.MODULE$.unapply(fun).isDefined()) { return FunctionDeclarationKind.STORE; + } else if (ExtArray.Const$.MODULE$.unapply(fun).isDefined()) { + return FunctionDeclarationKind.CONST; } else if (fun == ModuloArithmetic.mod_cast()) { return FunctionDeclarationKind.OTHER; } else if (fun == ModuloArithmetic.int_cast()) { diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolArrayFormulaManager.java index 9a836ccef5..9ac02d0d55 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolArrayFormulaManager.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -14,9 +14,9 @@ import de.uni_freiburg.informatik.ultimate.logic.Term; 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; import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; +@SuppressWarnings("MethodTypeParameterName") class SmtInterpolArrayFormulaManager extends AbstractArrayFormulaManager { @@ -41,14 +41,18 @@ protected Term store(Term pArray, Term pIndex, Term pValue) { @SuppressWarnings("MethodTypeParameterName") protected Term internalMakeArray( String pName, FormulaType pIndexType, FormulaType pElementType) { - - final ArrayFormulaType arrayFormulaType = - FormulaType.getArrayType(pIndexType, pElementType); - final Sort smtInterpolArrayType = toSolverType(arrayFormulaType); - + final Sort smtInterpolArrayType = + toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); return getFormulaCreator().makeVariable(smtInterpolArrayType, pName); } + @Override + protected Term internalMakeArray( + FormulaType pIndexType, FormulaType pElementType, Term elseElem) { + final Sort arraySort = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); + return env.term("const", null, arraySort, elseElem); + } + @Override protected Term equivalence(Term pArray1, Term pArray2) { return env.term("=", pArray1, pArray2); diff --git a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java index b894faef13..fe083eb844 100644 --- a/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolFormulaCreator.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -311,6 +311,8 @@ private FunctionDeclarationKind getDeclarationKind(ApplicationTerm input) { return FunctionDeclarationKind.SELECT; case "store": return FunctionDeclarationKind.STORE; + case "const": + return FunctionDeclarationKind.CONST; case "*": return FunctionDeclarationKind.MUL; case "+": 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..2d3e86b71c 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3ArrayFormulaManager.java @@ -11,9 +11,9 @@ import com.microsoft.z3.Native; 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; import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; +@SuppressWarnings("MethodTypeParameterName") class Z3ArrayFormulaManager extends AbstractArrayFormulaManager { private final long z3context; @@ -37,14 +37,16 @@ protected Long store(Long pArray, Long pIndex, Long pValue) { @SuppressWarnings("MethodTypeParameterName") protected Long internalMakeArray( String pName, FormulaType pIndexType, FormulaType pElementType) { - - final ArrayFormulaType arrayFormulaType = - FormulaType.getArrayType(pIndexType, pElementType); - final Long z3ArrayType = toSolverType(arrayFormulaType); - + final Long z3ArrayType = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); return getFormulaCreator().makeVariable(z3ArrayType, pName); } + @Override + protected Long internalMakeArray( + FormulaType pIndexType, FormulaType pElementType, Long elseElem) { + 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/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index a99072649f..ce0b3708c0 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -629,6 +629,8 @@ private FunctionDeclarationKind getDeclarationKind(long f) { return FunctionDeclarationKind.STORE; case Z3_OP_SELECT: return FunctionDeclarationKind.SELECT; + case Z3_OP_CONST_ARRAY: + return FunctionDeclarationKind.CONST; case Z3_OP_TRUE: case Z3_OP_FALSE: diff --git a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java index e82ee0c294..6d1853e903 100644 --- a/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/ArrayFormulaManagerTest.java @@ -8,6 +8,7 @@ package org.sosy_lab.java_smt.test; +import static com.google.common.truth.TruthJUnit.assume; import static org.sosy_lab.java_smt.api.FormulaType.IntegerType; import static org.sosy_lab.java_smt.api.FormulaType.RationalType; import static org.sosy_lab.java_smt.api.FormulaType.StringType; @@ -16,12 +17,14 @@ import org.junit.Before; import org.junit.Test; +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.BooleanFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; import org.sosy_lab.java_smt.api.SolverException; @@ -180,4 +183,67 @@ public void testFloatIndexFloatValue() throws SolverException, InterruptedExcept bmgr.not(fpmgr.equalWithFPSemantics(num2, amgr.select(arr2, num4)))); assertThatFormula(query).isUnsatisfiable(); } + + @Test + public void testArrayConstWithDefault() throws SolverException, InterruptedException { + requireIntegers(); + assume() + .withMessage("Solver %s does not yet support array initialization", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.OPENSMT); + + for (int elem : new int[] {0, 1, 5, 100, -100}) { + IntegerFormula elseElem = imgr.makeNumber(elem); + IntegerFormula otherElem = imgr.makeNumber(elem + 1); + + ArrayFormula arr = + amgr.makeArray(FormulaType.getArrayType(IntegerType, IntegerType), elseElem); + + for (int i : new int[] {1, 3, 9, 13}) { + IntegerFormula index = imgr.makeNumber(i); + + // select(arr, i) == elseElem, and not otherElem + assertThatFormula(imgr.equal(elseElem, amgr.select(arr, index))).isTautological(); + assertThatFormula(imgr.equal(otherElem, amgr.select(arr, index))).isUnsatisfiable(); + + // select(store(arr, i, j)) == j, and not elseElem + IntegerFormula selectFromStore = amgr.select(amgr.store(arr, index, otherElem), index); + assertThatFormula(imgr.equal(otherElem, selectFromStore)).isTautological(); + assertThatFormula(imgr.equal(elseElem, selectFromStore)).isUnsatisfiable(); + } + } + } + + @Test + public void testArrayConstBvWithDefault() throws SolverException, InterruptedException { + requireBitvectors(); + assume() + .withMessage("Solver %s does not yet support array initialization", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.BOOLECTOR); + + final int size = 8; + + for (int elem : new int[] {0, 1, 5, 100, -100}) { + BitvectorFormula elseElem = bvmgr.makeBitvector(size, elem); + BitvectorFormula otherElem = bvmgr.makeBitvector(size, elem + 1); + + BitvectorType bvType = getBitvectorTypeWithSize(size); + ArrayFormula arr = + amgr.makeArray(FormulaType.getArrayType(bvType, bvType), elseElem); + + for (int i : new int[] {1, 3, 9, 13}) { + BitvectorFormula index = bvmgr.makeBitvector(size, i); + + // select(arr, i) == elseElem, and not otherElem + assertThatFormula(bvmgr.equal(elseElem, amgr.select(arr, index))).isTautological(); + assertThatFormula(bvmgr.equal(otherElem, amgr.select(arr, index))).isUnsatisfiable(); + + // select(store(arr, i, j)) == j, and not elseElem + BitvectorFormula selectFromStore = amgr.select(amgr.store(arr, index, otherElem), index); + assertThatFormula(bvmgr.equal(otherElem, selectFromStore)).isTautological(); + assertThatFormula(bvmgr.equal(elseElem, selectFromStore)).isUnsatisfiable(); + } + } + } } diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 100e0dfdff..38c00eb939 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -32,6 +32,7 @@ import org.junit.Test; import org.sosy_lab.common.rationals.Rational; 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.BooleanFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; @@ -39,6 +40,7 @@ import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; 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; import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; import org.sosy_lab.java_smt.api.FunctionDeclaration; @@ -58,12 +60,13 @@ public class SolverVisitorTest extends SolverBasedTest0.ParameterizedSolverBasedTest0 { /** visit a formula and fail on OTHER, i.e., unexpected function declaration type. */ - private final class FunctionDeclarationVisitorNoOther extends DefaultFormulaVisitor { + private final class FunctionDeclarationVisitorNoOther + extends DefaultFormulaVisitor> { private final List found = new ArrayList<>(); @Override - public Formula visitFunction( + public List visitFunction( Formula f, List args, FunctionDeclaration functionDeclaration) { found.add(functionDeclaration.getKind()); Truth.assert_() @@ -79,18 +82,19 @@ public Formula visitFunction( } @Override - protected Formula visitDefault(Formula pF) { - return pF; + protected List visitDefault(Formula pF) { + return found; } } /** visit a formula and fail on UF, i.e., uninterpreted function declaration type. */ - private final class FunctionDeclarationVisitorNoUF extends DefaultFormulaVisitor { + private final class FunctionDeclarationVisitorNoUF + extends DefaultFormulaVisitor> { private final List found = new ArrayList<>(); @Override - public Formula visitFunction( + public List visitFunction( Formula f, List args, FunctionDeclaration functionDeclaration) { found.add(functionDeclaration.getKind()); Truth.assert_() @@ -106,25 +110,45 @@ public Formula visitFunction( } @Override - protected Formula visitDefault(Formula pF) { - return pF; + protected List visitDefault(Formula pF) { + return found; } } /** visit only constants and ignore other operations. */ - private static final class ConstantsVisitor extends DefaultFormulaVisitor { + private final class ConstantsVisitor extends DefaultFormulaVisitor> { + private final boolean recursive; private final List found = new ArrayList<>(); + ConstantsVisitor(boolean recursive) { + this.recursive = recursive; + } + + ConstantsVisitor() { + this.recursive = false; + } + @Override - public Formula visitConstant(Formula f, Object value) { + public List visitConstant(Formula f, Object value) { found.add(value); return visitDefault(f); } @Override - protected Formula visitDefault(Formula pF) { - return pF; + public List visitFunction( + Formula f, List args, FunctionDeclaration functionDeclaration) { + if (recursive) { + for (Formula arg : args) { + mgr.visit(arg, this); + } + } + return visitDefault(f); + } + + @Override + protected List visitDefault(Formula pF) { + return found; } } @@ -274,6 +298,74 @@ public void rationalConstantVisit() { } } + @Test + public void arrayVisit() { + requireArrays(); + requireIntegers(); + + ArrayFormulaType arrayType = + ArrayFormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType); + IntegerFormula index = imgr.makeNumber(1); + IntegerFormula elem = imgr.makeNumber(123); + + ArrayFormula arr = amgr.makeArray("some_array", arrayType); + IntegerFormula selectedElem = amgr.select(arr, index); + assertThat(mgr.visit(selectedElem, new FunctionDeclarationVisitorNoOther())) + .containsExactly(FunctionDeclarationKind.SELECT); + assertThat(mgr.visit(selectedElem, new ConstantsVisitor(true))) + .containsExactly(BigInteger.valueOf(1)); + + ArrayFormula store = amgr.store(arr, index, elem); + assertThat(mgr.visit(store, new FunctionDeclarationVisitorNoOther())) + .containsExactly(FunctionDeclarationKind.STORE); + assertThat(mgr.visit(store, new ConstantsVisitor(true))) + .containsExactly(BigInteger.valueOf(1), BigInteger.valueOf(123)); + + assume() + .withMessage("Solver %s does not support initialization of arrays", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.OPENSMT); + + ArrayFormula initializedArr = amgr.makeArray(arrayType, elem); + assertThat(mgr.visit(initializedArr, new FunctionDeclarationVisitorNoOther())) + .containsExactly(FunctionDeclarationKind.CONST); + assertThat(mgr.visit(initializedArr, new ConstantsVisitor(true))) + .containsExactly(BigInteger.valueOf(123)); + } + + @Test + public void arrayTransform() throws SolverException, InterruptedException { + requireArrays(); + requireArrays(); + + ArrayFormulaType arrayType = + ArrayFormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType); + IntegerFormula index = imgr.makeNumber(1); + IntegerFormula elem = imgr.makeNumber(123); + IntegerFormula x = imgr.makeVariable("some_var"); + + ArrayFormula arr = amgr.makeArray("some_array", arrayType); + BooleanFormula f = imgr.equal(amgr.select(arr, index), x); + BooleanFormula f2 = mgr.transformRecursively(f, new FormulaTransformationVisitor(mgr) {}); + assertThat(f2).isEqualTo(f); + assertThatFormula(f).isEquivalentTo(f2); + + BooleanFormula f3 = amgr.equivalence(amgr.store(arr, index, elem), arr); + BooleanFormula f4 = mgr.transformRecursively(f3, new FormulaTransformationVisitor(mgr) {}); + assertThat(f4).isEqualTo(f3); + assertThatFormula(f3).isEquivalentTo(f4); + + assume() + .withMessage("Solver %s does not support initialization of arrays", solverToUse()) + .that(solverToUse()) + .isNotEqualTo(Solvers.OPENSMT); + + BooleanFormula f5 = amgr.equivalence(amgr.makeArray(arrayType, elem), arr); + BooleanFormula f6 = mgr.transformRecursively(f5, new FormulaTransformationVisitor(mgr) {}); + assertThat(f6).isEqualTo(f5); + assertThatFormula(f5).isEquivalentTo(f6); + } + @Test public void bitvectorConstantVisit() { requireBitvectors(); From 937097f437435e0073f5d3983e6899bc71b9ebab Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 3 Apr 2024 22:19:49 +0200 Subject: [PATCH 3/4] fix compiler warning about static methods. --- src/org/sosy_lab/java_smt/test/SolverVisitorTest.java | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 38c00eb939..7549c4c690 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -10,6 +10,7 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; +import static org.sosy_lab.java_smt.api.FormulaType.getArrayType; import com.google.common.base.Strings; import com.google.common.collect.ImmutableList; @@ -304,7 +305,7 @@ public void arrayVisit() { requireIntegers(); ArrayFormulaType arrayType = - ArrayFormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType); + getArrayType(FormulaType.IntegerType, FormulaType.IntegerType); IntegerFormula index = imgr.makeNumber(1); IntegerFormula elem = imgr.makeNumber(123); @@ -339,7 +340,7 @@ public void arrayTransform() throws SolverException, InterruptedException { requireArrays(); ArrayFormulaType arrayType = - ArrayFormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType); + getArrayType(FormulaType.IntegerType, FormulaType.IntegerType); IntegerFormula index = imgr.makeNumber(1); IntegerFormula elem = imgr.makeNumber(123); IntegerFormula x = imgr.makeVariable("some_var"); From 5e0339b5e61e53a4420758c66499ad00308b9936 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Wed, 3 Apr 2024 22:32:01 +0200 Subject: [PATCH 4/4] Princess: update Princess to latest version 2024-01-12. --- lib/ivy.xml | 4 ++-- .../solvers/princess/PrincessArrayFormulaManager.java | 2 +- .../solvers/princess/PrincessEnvironment.java | 11 +++++------ .../solvers/princess/PrincessFormulaCreator.java | 2 +- .../java_smt/solvers/princess/PrincessModel.java | 4 ++-- 5 files changed, 11 insertions(+), 12 deletions(-) diff --git a/lib/ivy.xml b/lib/ivy.xml index 0fbfaede56..d24ed0975a 100644 --- a/lib/ivy.xml +++ b/lib/ivy.xml @@ -147,9 +147,9 @@ SPDX-License-Identifier: Apache-2.0 - + - + diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessArrayFormulaManager.java index 5840adc98e..2e4b2490aa 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessArrayFormulaManager.java @@ -10,7 +10,7 @@ import ap.parser.IExpression; import ap.parser.ITerm; -import ap.theories.ExtArray.ArraySort; +import ap.theories.arrays.ExtArray.ArraySort; import ap.types.Sort; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java index 981e9dd5c4..ede3155b8f 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessEnvironment.java @@ -12,6 +12,7 @@ import static scala.collection.JavaConverters.collectionAsScalaIterableConverter; import ap.api.SimpleAPI; +import ap.parameters.GlobalSettings; import ap.parser.BooleanCompactifier; import ap.parser.Environment.EnvironmentException; import ap.parser.IAtom; @@ -26,11 +27,11 @@ import ap.parser.PartialEvaluator; import ap.parser.SMTLineariser; import ap.parser.SMTParser2InputAbsy.SMTFunctionType; -import ap.parser.SMTParser2InputAbsy.SMTType; +import ap.parser.SMTTypes.SMTType; import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; -import ap.theories.ExtArray; -import ap.theories.ExtArray.ArraySort; +import ap.theories.arrays.ExtArray; +import ap.theories.arrays.ExtArray.ArraySort; import ap.theories.bitvectors.ModuloArithmetic; import ap.theories.rationals.Fractions.FractionSort$; import ap.types.Sort; @@ -78,7 +79,6 @@ import scala.Tuple2; import scala.Tuple4; import scala.collection.immutable.Seq; -import scala.collection.immutable.Set$; /** * This is a Wrapper around Princess. This Wrapper allows to set a logfile for all Smt-Queries @@ -219,8 +219,7 @@ private SimpleAPI getNewApi(boolean constructProofs) { SimpleAPI.apply$default$8(), // tightFunctionScopes SimpleAPI.apply$default$9(), // genTotalityAxioms new scala.Some<>(randomSeed), // randomSeed - Set$.MODULE$.empty() // empty Set, no internal logging - ); + GlobalSettings.DEFAULT()); if (constructProofs) { // needed for interpolation and unsat cores newApi.setConstructProofs(true); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java index 7565424719..d8846fbb2b 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -39,7 +39,7 @@ import ap.parser.IVariable; import ap.terfor.conjunctions.Quantifier; import ap.terfor.preds.Predicate; -import ap.theories.ExtArray; +import ap.theories.arrays.ExtArray; import ap.theories.bitvectors.ModuloArithmetic; import ap.theories.nia.GroebnerMultiplication$; import ap.types.Sort; diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java index 5e65b30840..3f47cc959b 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessModel.java @@ -21,8 +21,8 @@ import ap.parser.IFunApp; import ap.parser.ITerm; import ap.terfor.preds.Predicate; -import ap.theories.ExtArray; -import ap.theories.ExtArray.ArraySort; +import ap.theories.arrays.ExtArray; +import ap.theories.arrays.ExtArray.ArraySort; import ap.types.Sort; import ap.types.Sort$; import com.google.common.collect.ArrayListMultimap;