From afdcd467ca360e9cac08e40f0ffa63f909ae074b Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Thu, 11 Sep 2025 16:58:04 +0200 Subject: [PATCH 1/6] Yices: Add array theory --- .../yices2/Yices2ArrayFormulaManager.java | 77 +++++++++++ .../solvers/yices2/Yices2Formula.java | 25 ++++ .../solvers/yices2/Yices2FormulaCreator.java | 122 +++++++++++++++--- .../solvers/yices2/Yices2FormulaManager.java | 6 +- .../solvers/yices2/Yices2NativeApi.java | 1 + .../solvers/yices2/Yices2SolverContext.java | 4 +- .../java_smt/test/QuantifierManagerTest.java | 5 +- .../java_smt/test/SolverBasedTest0.java | 2 +- .../java_smt/test/SolverTheoriesTest.java | 15 +++ 9 files changed, 235 insertions(+), 22 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java new file mode 100644 index 0000000000..ce306ae7bc --- /dev/null +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java @@ -0,0 +1,77 @@ +/* + * This file is part of JavaSMT, + * an API wrapper for a collection of SMT solvers: + * https://github.com/sosy-lab/java-smt + * + * SPDX-FileCopyrightText: 2025 Dirk Beyer + * + * SPDX-License-Identifier: Apache-2.0 + */ + +package org.sosy_lab.java_smt.solvers.yices2; + +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_application; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_eq; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_function_type; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_lambda; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_variable; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_update; + +import com.google.common.collect.HashBasedTable; +import com.google.common.collect.Table; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; + +public class Yices2ArrayFormulaManager + extends AbstractArrayFormulaManager { + + /** + * Cache with constant array values. + * + *

Used in {@link #internalMakeArray(FormulaType, FormulaType, Integer)} to guarantee that + * existing constant array values are never re-created + */ + private final Table constCache = HashBasedTable.create(); + + public Yices2ArrayFormulaManager(Yices2FormulaCreator pCreator) { + super(pCreator); + } + + @Override + protected Integer select(Integer pArray, Integer pIndex) { + return yices_application(pArray, 1, new int[] {pIndex}); + } + + @Override + protected Integer store(Integer pArray, Integer pIndex, Integer pValue) { + return yices_update(pArray, 1, new int[] {pIndex}, pValue); + } + + @Override + protected Integer internalMakeArray( + String pName, FormulaType pIndexType, FormulaType pElementType) { + var yicesFuncType = + yices_function_type(1, new int[] {toSolverType(pIndexType)}, toSolverType(pElementType)); + return ((Yices2FormulaCreator) getFormulaCreator()).createNamedVariable(yicesFuncType, pName); + } + + @Override + protected Integer internalMakeArray( + FormulaType pIndexType, FormulaType pElementType, Integer defaultElement) { + var arraySort = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); + if (constCache.contains(arraySort, defaultElement)) { + return constCache.get(arraySort, defaultElement); + } else { + var constant = + yices_lambda(1, new int[] {yices_new_variable(toSolverType(pIndexType))}, defaultElement); + constCache.put(arraySort, defaultElement, constant); + return constant; + } + } + + @Override + protected Integer equivalence(Integer pArray1, Integer pArray2) { + return yices_eq(pArray1, pArray2); + } +} diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Formula.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Formula.java index 0848079b42..eb2ed685e4 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Formula.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Formula.java @@ -8,12 +8,15 @@ package org.sosy_lab.java_smt.solvers.yices2; +import static com.google.common.base.Preconditions.checkNotNull; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_to_string; import com.google.errorprone.annotations.Immutable; +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.Formula; +import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; @@ -78,4 +81,26 @@ static final class Yices2BooleanFormula extends Yices2Formula implements Boolean super(pTerm); } } + + @Immutable + static final class Yices2ArrayFormula + extends Yices2Formula implements ArrayFormula { + + private final FormulaType indexType; + private final FormulaType elementType; + + Yices2ArrayFormula(Integer info, FormulaType pIndexType, FormulaType pElementType) { + super(info); + this.indexType = checkNotNull(pIndexType); + this.elementType = checkNotNull(pElementType); + } + + public FormulaType getIndexType() { + return indexType; + } + + public FormulaType getElementType() { + return elementType; + } + } } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java index bd4ddd6621..2ba9d7dedc 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java @@ -15,6 +15,7 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_CONST; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_GE_ATOM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_SUM; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARRAY_EVAL; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BIT_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BOOL_CONST; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BV_ARRAY; @@ -41,12 +42,14 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_IMOD; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_IS_INT_ATOM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ITE_TERM; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_LAMBDA_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_NOT_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_OR_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_POWER_PRODUCT; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_RDIV; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_SELECT_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_UNINTERPRETED_TERM; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_UPDATE_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_VARIABLE; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_XOR_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_abs; @@ -111,16 +114,19 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_bitsize; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_child; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_constructor; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_is_bitvector; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_is_bool; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_is_int; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_is_real; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_num_children; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_to_string; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_true; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_child; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_bitvector; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_bool; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_function; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_int; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_is_real; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_of_term; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_type_to_string; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_update; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_xor; import com.google.common.base.Joiner; @@ -136,24 +142,30 @@ import java.math.BigInteger; import java.util.ArrayList; import java.util.Arrays; +import java.util.HashSet; import java.util.List; +import java.util.Set; import java.util.stream.Collectors; import org.sosy_lab.common.rationals.Rational; +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.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.FloatingPointType; import org.sosy_lab.java_smt.api.FunctionDeclarationKind; import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; import org.sosy_lab.java_smt.basicimpl.FormulaCreator; import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl; +import org.sosy_lab.java_smt.solvers.yices2.Yices2Formula.Yices2ArrayFormula; import org.sosy_lab.java_smt.solvers.yices2.Yices2Formula.Yices2BitvectorFormula; import org.sosy_lab.java_smt.solvers.yices2.Yices2Formula.Yices2BooleanFormula; import org.sosy_lab.java_smt.solvers.yices2.Yices2Formula.Yices2IntegerFormula; import org.sosy_lab.java_smt.solvers.yices2.Yices2Formula.Yices2RationalFormula; +@SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"}) public class Yices2FormulaCreator extends FormulaCreator { private static final ImmutableSet CONSTANT_AND_VARIABLE_CONSTRUCTORS = @@ -170,6 +182,14 @@ public class Yices2FormulaCreator extends FormulaCreator formulaCache = HashBasedTable.create(); + /** + * List of all UF function declarations. + * + *

We need this in the visitor to tell the difference between functions and arrays. Both are + * modeled internally by function terms. + */ + private final Set ufSymbols = new HashSet<>(); + protected Yices2FormulaCreator() { super(null, yices_bool_type(), yices_int_type(), yices_real_type(), null, null); } @@ -186,7 +206,7 @@ public Integer getFloatingPointType(FloatingPointType pType) { @Override public Integer getArrayType(Integer pIndexType, Integer pElementType) { - throw new UnsupportedOperationException(); + return yices_function_type(1, new int[] {pIndexType}, pElementType); } @Override @@ -199,6 +219,20 @@ public Integer extractInfo(Formula pT) { return Yices2FormulaManager.getYicesTerm(pT); } + @Override + @SuppressWarnings("unchecked") + protected FormulaType getArrayFormulaElementType( + ArrayFormula pArray) { + return ((Yices2ArrayFormula) pArray).getElementType(); + } + + @Override + @SuppressWarnings("unchecked") + protected FormulaType getArrayFormulaIndexType( + ArrayFormula pArray) { + return ((Yices2ArrayFormula) pArray).getIndexType(); + } + @SuppressWarnings("unchecked") @Override public T encapsulate(FormulaType pType, Integer pTerm) { @@ -219,6 +253,10 @@ public T encapsulate(FormulaType pType, Integer pTerm) { return (T) new Yices2RationalFormula(pTerm); } else if (pType.isBitvectorType()) { return (T) new Yices2BitvectorFormula(pTerm); + } else if (pType.isArrayType()) { + var range = ((ArrayFormulaType) pType).getElementType(); + var dom = ((ArrayFormulaType) pType).getIndexType(); + return (T) encapsulateArray(pTerm, dom, range); } throw new IllegalArgumentException("Cannot create formulas of type " + pType + " in Yices"); } @@ -235,12 +273,24 @@ public BitvectorFormula encapsulateBitvector(Integer pTerm) { return new Yices2BitvectorFormula(pTerm); } + @Override + protected ArrayFormula encapsulateArray( + Integer pTerm, FormulaType pIndexType, FormulaType pElementType) { + checkArgument( + getFormulaType(pTerm).equals(FormulaType.getArrayType(pIndexType, pElementType)), + "Array formula has unexpected type: %s", + getFormulaType(pTerm)); + return new Yices2Formula.Yices2ArrayFormula<>(pTerm, pIndexType, pElementType); + } + @SuppressWarnings("unchecked") @Override public FormulaType getFormulaType(T pFormula) { if (pFormula instanceof BitvectorFormula) { int type = yices_type_of_term(extractInfo(pFormula)); return (FormulaType) FormulaType.getBitvectorTypeWithSize(yices_bvtype_size(type)); + } else if (pFormula instanceof ArrayFormula) { + return (FormulaType) convertType(yices_type_of_term(extractInfo(pFormula))); } else { return super.getFormulaType(pFormula); } @@ -248,19 +298,26 @@ public FormulaType getFormulaType(T pFormula) { @Override public FormulaType getFormulaType(Integer pFormula) { - if (yices_term_is_bool(pFormula)) { + return convertType(yices_type_of_term(pFormula)); + } + + /** Convert from Yices2 types to JavaSMT FormulaTypes. */ + private FormulaType convertType(Integer pType) { + if (yices_type_is_bool(pType)) { return FormulaType.BooleanType; - } else if (yices_term_is_int(pFormula)) { + } else if (yices_type_is_int(pType)) { return FormulaType.IntegerType; - } else if (yices_term_is_real(pFormula)) { + } else if (yices_type_is_real(pType)) { return FormulaType.RationalType; - } else if (yices_term_is_bitvector(pFormula)) { - return FormulaType.getBitvectorTypeWithSize(yices_term_bitsize(pFormula)); + } else if (yices_type_is_bitvector(pType)) { + return FormulaType.getBitvectorTypeWithSize(yices_bvtype_size(pType)); + } else if (yices_type_is_function(pType)) { + var domain = yices_type_child(pType, 0); + var range = yices_type_child(pType, 1); + return FormulaType.getArrayType(convertType(domain), convertType(range)); } throw new IllegalArgumentException( - String.format( - "Unknown formula type '%s' for formula '%s'", - yices_type_to_string(yices_type_of_term(pFormula)), yices_term_to_string(pFormula))); + String.format("Unknown formula type '%s'", yices_type_to_string(pType))); } /** Creates a named, free variable. Might retrieve it from the cache if created prior. */ @@ -335,6 +392,17 @@ public R visit(FormulaVisitor pVisitor, Formula pFormula, Integer pF) { return pVisitor.visitConstant(pFormula, convertValue(pF, pF)); case YICES_BV_CONST: return pVisitor.visitConstant(pFormula, convertValue(pF, pF)); + case YICES_LAMBDA_TERM: + // We use lambda terms as array constants + return pVisitor.visitFunction( + pFormula, + ImmutableList.of(encapsulateWithTypeOf(yices_term_child(pF, 1))), + FunctionDeclarationImpl.of( + "const", + FunctionDeclarationKind.CONST, + ImmutableList.of(getFormulaType(yices_term_child(pF, 1))), + getFormulaType(pF), + 0)); case YICES_UNINTERPRETED_TERM: return pVisitor.visitFreeVariable(pFormula, yices_get_term_name(pF)); case YICES_VARIABLE: @@ -398,11 +466,26 @@ private R visitFunctionApplication( functionKind = FunctionDeclarationKind.ITE; break; case YICES_APP_TERM: - functionKind = FunctionDeclarationKind.UF; - functionArgs = getArgs(pF); - functionName = yices_term_to_string(functionArgs.get(0)); - functionDeclaration = functionArgs.get(0); - functionArgs.remove(0); + var fun = yices_term_child(pF, 0); + if (ufSymbols.contains(fun)) { + functionKind = FunctionDeclarationKind.UF; + functionArgs = getArgs(pF); + functionName = yices_get_term_name(functionArgs.get(0)); + functionDeclaration = functionArgs.get(0); + functionArgs.remove(0); + } else { + functionKind = FunctionDeclarationKind.SELECT; + functionArgs = getArgs(pF); + functionName = "select"; + functionDeclaration = -YICES_ARRAY_EVAL; + } + break; + case YICES_UPDATE_TERM: + functionKind = FunctionDeclarationKind.STORE; + functionArgs = + ImmutableList.of( + yices_term_child(pF, 0), yices_term_child(pF, 1), yices_term_child(pF, 2)); + functionDeclaration = -YICES_UPDATE_TERM; break; case YICES_EQ_TERM: functionKind = FunctionDeclarationKind.EQ; // Covers all equivalences @@ -760,6 +843,10 @@ public Integer callFunctionImpl(Integer pDeclaration, List pArgs) { return yices_bvproduct(pArgs.size(), Ints.toArray(pArgs)); case YICES_AND: return yices_and(pArgs.size(), Ints.toArray(pArgs)); + case YICES_ARRAY_EVAL: + return yices_application(pArgs.get(0), 1, new int[] {pArgs.get(1)}); + case YICES_UPDATE_TERM: + return yices_update(pArgs.get(0), 1, new int[] {pArgs.get(1)}, pArgs.get(2)); default: // TODO add more cases // if something bad happens here, @@ -808,6 +895,7 @@ public Integer declareUFImpl(String pName, Integer pReturnType, List pA yicesFuncType = yices_function_type(size, argTypeArray, pReturnType); } int uf = createNamedVariable(yicesFuncType, pName); + ufSymbols.add(uf); return uf; } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java index cb6093e2d2..69b0c8ae82 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaManager.java @@ -39,6 +39,7 @@ public class Yices2FormulaManager extends AbstractFormulaManager Date: Thu, 11 Sep 2025 17:24:49 +0200 Subject: [PATCH 2/6] Yices: Fix Checkstyle issues --- .../java_smt/solvers/yices2/Yices2ArrayFormulaManager.java | 1 + src/org/sosy_lab/java_smt/solvers/yices2/Yices2Formula.java | 1 + 2 files changed, 2 insertions(+) diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java index ce306ae7bc..22e11b7830 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java @@ -23,6 +23,7 @@ import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager; +@SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"}) public class Yices2ArrayFormulaManager extends AbstractArrayFormulaManager { diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Formula.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Formula.java index eb2ed685e4..6b389686ec 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Formula.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Formula.java @@ -82,6 +82,7 @@ static final class Yices2BooleanFormula extends Yices2Formula implements Boolean } } + @SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"}) @Immutable static final class Yices2ArrayFormula extends Yices2Formula implements ArrayFormula { From 2d3ed6379e0678402213171a9ddf4a56420c5d1b Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 13 Sep 2025 13:07:49 +0200 Subject: [PATCH 3/6] Yices2: avoid repeated access to map. --- .../solvers/yices2/Yices2ArrayFormulaManager.java | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java index 22e11b7830..1aa728f6e8 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2ArrayFormulaManager.java @@ -61,14 +61,13 @@ protected Integer internalMakeArray( protected Integer internalMakeArray( FormulaType pIndexType, FormulaType pElementType, Integer defaultElement) { var arraySort = toSolverType(FormulaType.getArrayType(pIndexType, pElementType)); - if (constCache.contains(arraySort, defaultElement)) { - return constCache.get(arraySort, defaultElement); - } else { - var constant = + var constantArray = constCache.get(arraySort, defaultElement); + if (constantArray == null) { + constantArray = yices_lambda(1, new int[] {yices_new_variable(toSolverType(pIndexType))}, defaultElement); - constCache.put(arraySort, defaultElement, constant); - return constant; + constCache.put(arraySort, defaultElement, constantArray); } + return constantArray; } @Override From 07c40f7fdf18df0c38cdc7f1207966ad2a80dcea Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 13 Sep 2025 13:08:41 +0200 Subject: [PATCH 4/6] Yices2: rename constant for function-application or array-select. --- .../java_smt/solvers/yices2/Yices2FormulaCreator.java | 6 +++--- .../sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java index 2ba9d7dedc..0944361ff9 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java @@ -15,7 +15,7 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_CONST; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_GE_ATOM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARITH_SUM; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARRAY_EVAL; +import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_ARRAY_SELECT; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BIT_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BOOL_CONST; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_BV_ARRAY; @@ -477,7 +477,7 @@ private R visitFunctionApplication( functionKind = FunctionDeclarationKind.SELECT; functionArgs = getArgs(pF); functionName = "select"; - functionDeclaration = -YICES_ARRAY_EVAL; + functionDeclaration = -YICES_ARRAY_SELECT; } break; case YICES_UPDATE_TERM: @@ -843,7 +843,7 @@ public Integer callFunctionImpl(Integer pDeclaration, List pArgs) { return yices_bvproduct(pArgs.size(), Ints.toArray(pArgs)); case YICES_AND: return yices_and(pArgs.size(), Ints.toArray(pArgs)); - case YICES_ARRAY_EVAL: + case YICES_ARRAY_SELECT: return yices_application(pArgs.get(0), 1, new int[] {pArgs.get(1)}); case YICES_UPDATE_TERM: return yices_update(pArgs.get(0), 1, new int[] {pArgs.get(1)}, pArgs.get(2)); diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java index eb18443e6c..3848b41c52 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApi.java @@ -89,7 +89,7 @@ private Yices2NativeApi() {} // MAX_INT avoids collisions with existing constants public static final int YICES_AND = Integer.MAX_VALUE - 1; public static final int YICES_BV_MUL = Integer.MAX_VALUE - 2; - public static final int YICES_ARRAY_EVAL = Integer.MAX_VALUE - 3; + public static final int YICES_ARRAY_SELECT = Integer.MAX_VALUE - 3; /* * Yices model tags From 4dfcf13b0bb67bcffdfaa27103d1a2f41dc230c3 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 13 Sep 2025 15:21:51 +0200 Subject: [PATCH 5/6] SolverFormulaIOTest: check declared function symbols, also for arrays. --- .../java_smt/test/SolverFormulaIOTest.java | 98 ++++++++++++++----- 1 file changed, 71 insertions(+), 27 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java index f59932d77e..a3435af37e 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java @@ -14,11 +14,15 @@ import static com.google.common.truth.TruthJUnit.assume; import com.google.common.base.Splitter; -import com.google.common.collect.HashMultiset; +import com.google.common.collect.HashMultimap; +import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; -import com.google.common.collect.Multiset; +import com.google.common.collect.Multimap; import com.google.common.truth.TruthJUnit; +import java.util.Collection; import java.util.function.Supplier; +import java.util.regex.Pattern; +import org.junit.AssumptionViolatedException; import org.junit.Test; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BitvectorFormula; @@ -105,6 +109,10 @@ public class SolverFormulaIOTest extends SolverBasedTest0.ParameterizedSolverBas + "(assert (let (($x35 (and (xor q (= (+ a b) c)) (>= a b)))) (let (($x9 (= a b))) (and" + " (and (or $x35 u) q) (and $x9 $x35)))))"; + private static final Collection ABDE = ImmutableSet.of("a", "b", "d", "e"); + private static final Collection AQBCU = ImmutableSet.of("a", "q", "b", "c", "u"); + private static final Collection QBCU = ImmutableSet.of("q", "b", "c", "u"); + @Test public void logicsParseTest() throws SolverException, InterruptedException { requireParser(); @@ -278,83 +286,83 @@ public void funcsDumpTest() { @Test public void parseMathSatTestParseFirst1() throws SolverException, InterruptedException { requireParser(); - compareParseWithOrgParseFirst(MATHSAT_DUMP1, this::genBoolExpr); + compareParseWithOrgParseFirst(MATHSAT_DUMP1, this::genBoolExpr, ABDE); } @Test public void parseMathSatTestExprFirst1() throws SolverException, InterruptedException { requireParser(); - compareParseWithOrgExprFirst(MATHSAT_DUMP1, this::genBoolExpr); + compareParseWithOrgExprFirst(MATHSAT_DUMP1, this::genBoolExpr, ABDE); } @Test public void parseSmtinterpolTestParseFirst1() throws SolverException, InterruptedException { requireParser(); - compareParseWithOrgParseFirst(SMTINTERPOL_DUMP1, this::genBoolExpr); + compareParseWithOrgParseFirst(SMTINTERPOL_DUMP1, this::genBoolExpr, ABDE); } @Test public void parseSmtinterpolTestExprFirst1() throws SolverException, InterruptedException { requireParser(); - compareParseWithOrgExprFirst(SMTINTERPOL_DUMP1, this::genBoolExpr); + compareParseWithOrgExprFirst(SMTINTERPOL_DUMP1, this::genBoolExpr, ABDE); } @Test public void parseZ3TestParseFirst1() throws SolverException, InterruptedException { requireParser(); - compareParseWithOrgParseFirst(Z3_DUMP1, this::genBoolExpr); + compareParseWithOrgParseFirst(Z3_DUMP1, this::genBoolExpr, ABDE); } @Test public void parseZ3TestExprFirst1() throws SolverException, InterruptedException { requireParser(); - compareParseWithOrgExprFirst(Z3_DUMP1, this::genBoolExpr); + compareParseWithOrgExprFirst(Z3_DUMP1, this::genBoolExpr, ABDE); } @Test public void parseMathSatTestParseFirst2() throws SolverException, InterruptedException { requireParser(); requireIntegers(); - compareParseWithOrgParseFirst(MATHSAT_DUMP2, this::redundancyExprGen); + compareParseWithOrgParseFirst(MATHSAT_DUMP2, this::redundancyExprGen, AQBCU); } @Test public void parseMathSatTestExprFirst2() throws SolverException, InterruptedException { requireParser(); - compareParseWithOrgExprFirst(MATHSAT_DUMP2, this::redundancyExprGen); + compareParseWithOrgExprFirst(MATHSAT_DUMP2, this::redundancyExprGen, AQBCU); } @Test public void parseSmtinterpolSatTestParseFirst2() throws SolverException, InterruptedException { requireParser(); requireIntegers(); - compareParseWithOrgParseFirst(SMTINTERPOL_DUMP2, this::redundancyExprGen); + compareParseWithOrgParseFirst(SMTINTERPOL_DUMP2, this::redundancyExprGen, QBCU); } @Test public void parseSmtinterpolSatTestExprFirst2() throws SolverException, InterruptedException { requireParser(); - compareParseWithOrgExprFirst(SMTINTERPOL_DUMP2, this::redundancyExprGen); + compareParseWithOrgExprFirst(SMTINTERPOL_DUMP2, this::redundancyExprGen, QBCU); } @Test public void parseZ3SatTestParseFirst2() throws SolverException, InterruptedException { requireParser(); requireIntegers(); - compareParseWithOrgParseFirst(Z3_DUMP2, this::redundancyExprGen); + compareParseWithOrgParseFirst(Z3_DUMP2, this::redundancyExprGen, AQBCU); } @Test public void parseZ3SatTestExprFirst2() throws SolverException, InterruptedException { requireParser(); - compareParseWithOrgExprFirst(Z3_DUMP2, this::redundancyExprGen); + compareParseWithOrgExprFirst(Z3_DUMP2, this::redundancyExprGen, AQBCU); } @Test public void parseMathSatTestExprFirst3() throws SolverException, InterruptedException { requireParser(); requireIntegers(); - compareParseWithOrgExprFirst(MATHSAT_DUMP3, this::functionExprGen); + compareParseWithOrgExprFirst(MATHSAT_DUMP3, this::functionExprGen, ImmutableSet.of("fun_b")); } @Test @@ -399,7 +407,7 @@ public void funDeclareTest() { String formDump = mgr.dumpFormula(imgr.equal(calc, int1)).toString(); // check if dumped formula fits our specification - checkThatFunOnlyDeclaredOnce(formDump); + checkThatFunOnlyDeclaredOnce(formDump, ImmutableSet.of("fun_a", "fun_b")); checkThatAssertIsInLastLine(formDump); checkThatDumpIsParseable(formDump); } @@ -419,17 +427,41 @@ public void funDeclareTest2() { String formDump = mgr.dumpFormula(imgr.equal(calc, int1)).toString(); // check if dumped formula fits our specification - checkThatFunOnlyDeclaredOnce(formDump); + checkThatFunOnlyDeclaredOnce(formDump, ImmutableSet.of("fun_a")); + checkThatAssertIsInLastLine(formDump); + checkThatDumpIsParseable(formDump); + } + + @Test + public void funDeclareWithArrayTest() { + requireIntegers(); + requireArrays(); + + IntegerFormula idx = imgr.makeVariable("idx"); + IntegerFormula int1 = imgr.makeNumber(1); + IntegerFormula int2 = imgr.makeNumber(2); + + // assert (((select (store arr idx 2) 1) 2) + var arr = amgr.makeArray("arr", FormulaType.IntegerType, FormulaType.IntegerType); + var store = amgr.store(arr, idx, int2); + var select = amgr.select(store, int1); + var query = imgr.equal(int2, select); + + String formDump = mgr.dumpFormula(query).toString(); + + // check if dumped formula fits our specification + checkThatFunOnlyDeclaredOnce(formDump, ImmutableSet.of("idx", "arr")); checkThatAssertIsInLastLine(formDump); checkThatDumpIsParseable(formDump); } - private void compareParseWithOrgExprFirst(String textToParse, Supplier fun) + private void compareParseWithOrgExprFirst( + String textToParse, Supplier fun, Collection expectedDeclarations) throws SolverException, InterruptedException { // Boolector will fail this anyway since bools are bitvecs for btor TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); // check if input is correct - checkThatFunOnlyDeclaredOnce(textToParse); + checkThatFunOnlyDeclaredOnce(textToParse, expectedDeclarations); checkThatAssertIsInLastLine(textToParse); // actual test @@ -438,12 +470,13 @@ private void compareParseWithOrgExprFirst(String textToParse, Supplier fun) + private void compareParseWithOrgParseFirst( + String textToParse, Supplier fun, Collection expectedDeclarations) throws SolverException, InterruptedException { // Boolector will fail this anyway since bools are bitvecs for btor TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); // check if input is correct - checkThatFunOnlyDeclaredOnce(textToParse); + checkThatFunOnlyDeclaredOnce(textToParse, expectedDeclarations); checkThatAssertIsInLastLine(textToParse); // actual test @@ -452,19 +485,25 @@ private void compareParseWithOrgParseFirst(String textToParse, Supplier expectedDeclarations) { // Boolector will fail this anyway since bools are bitvecs for btor TruthJUnit.assume().that(solver).isNotEqualTo(Solvers.BOOLECTOR); - Multiset funDeclares = HashMultiset.create(); + Multimap funDeclares = HashMultimap.create(); + final Pattern declareFunRegex = Pattern.compile("\\(declare-fun\\s+(?\\S+)\\s*"); for (String line : Splitter.on('\n').split(formDump)) { if (line.startsWith("(declare-fun ")) { - funDeclares.add(line.replaceAll("\\s+", "")); + var matcher = declareFunRegex.matcher(line); + var name = matcher.find() ? matcher.group(1) : line.replaceAll("\\s+", ""); + funDeclares.put(name, line.replaceAll("\\s+", "")); } } + assertThat(funDeclares.keySet()).containsExactlyElementsIn(expectedDeclarations); + // remove non-duplicates - funDeclares.entrySet().removeIf(pStringEntry -> pStringEntry.getCount() <= 1); + funDeclares.keySet().removeIf(pStringEntry -> funDeclares.get(pStringEntry).size() <= 1); assertWithMessage("duplicate function declarations").that(funDeclares).isEmpty(); } @@ -487,8 +526,13 @@ private void checkThatAssertIsInLastLine(String dump) { @SuppressWarnings("CheckReturnValue") private void checkThatDumpIsParseable(String dump) { - requireParser(); - mgr.parse(dump); + try { + requireParser(); + mgr.parse(dump); + } catch (AssumptionViolatedException ave) { + // ignore, i.e., do not report test-case as skipped. + } + ; } private BooleanFormula genBoolExpr() { From c410213a1216550876eaf74ed0222d5a773f8d77 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sat, 13 Sep 2025 15:41:46 +0200 Subject: [PATCH 6/6] SolverFormulaIOTest: remove empty statement / unneeded semicolon. --- src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java index a3435af37e..5bdb9fdcd3 100644 --- a/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverFormulaIOTest.java @@ -532,7 +532,6 @@ private void checkThatDumpIsParseable(String dump) { } catch (AssumptionViolatedException ave) { // ignore, i.e., do not report test-case as skipped. } - ; } private BooleanFormula genBoolExpr() {