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..1aa728f6e8 --- /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; + +@SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"}) +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)); + 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, constantArray); + } + return constantArray; + } + + @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..6b389686ec 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,27 @@ static final class Yices2BooleanFormula extends Yices2Formula implements Boolean super(pTerm); } } + + @SuppressWarnings({"ClassTypeParameterName", "MethodTypeParameterName"}) + @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..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,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_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; @@ -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_SELECT; + } + 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_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)); 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= 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,12 @@ 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() { diff --git a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java index 238e7cad19..6f46fe5d01 100644 --- a/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverTheoriesTest.java @@ -716,6 +716,9 @@ public void testMakeIntArray() { // INFO: OpenSmt changes the order of the terms in the sum assertThat(_b_at_i_plus_1.toString()).isEqualTo("(select b (+ 1 i))"); break; + case YICES2: + assertThat(_b_at_i_plus_1.toString()).isEqualTo("(b (+ 1 i))"); + break; default: assertThat(_b_at_i_plus_1.toString()) .isEqualTo("(select b (+ i 1))"); // Compatibility to all solvers not guaranteed @@ -751,6 +754,9 @@ public void testMakeBitVectorArray() { .that(solver) .isNotEqualTo(Solvers.BOOLECTOR); break; + case YICES2: + assertThat(_b_at_i.toString()).isEqualTo("(b i)"); + break; default: assertThat(_b_at_i.toString()) .isEqualTo("(select b i)"); // Compatibility to all solvers not guaranteed @@ -779,6 +785,9 @@ public void testNestedIntegerArray() { case PRINCESS: assertThat(valueInMulti.toString()).isEqualTo("select(select(multi, i), i)"); break; + case YICES2: + assertThat(valueInMulti.toString()).isEqualTo("((multi i) i)"); + break; default: assertThat(valueInMulti.toString()).isEqualTo("(select (select multi i) i)"); } @@ -807,6 +816,9 @@ public void testNestedRationalArray() { case PRINCESS: assertThat(valueInMulti.toString()).isEqualTo("select(select(multi, i), i)"); break; + case YICES2: + assertThat(valueInMulti.toString()).isEqualTo("((multi i) i)"); + break; default: assertThat(valueInMulti.toString()).isEqualTo("(select (select multi i) i)"); } @@ -838,6 +850,9 @@ public void testNestedBitVectorArray() { assertThat(valueInMulti.toString()) .isEqualTo("(`read_int_T(19)` (`read_int_T(20)` multi " + "i) i)"); break; + case YICES2: + assertThat(valueInMulti.toString()).isEqualTo("((multi i) i)"); + break; default: assertThat(valueInMulti.toString()).isEqualTo("(select (select multi i) i)"); }