From 0cbf059c543292364ef3a7abfe7ba8b4d982df18 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 25 Aug 2025 20:07:00 +0200 Subject: [PATCH 01/12] Indices: Extend the API to support indexed function symbols, such as like "extract" for bitvectors --- .../java_smt/api/FunctionDeclaration.java | 5 + .../java_smt/api/FunctionDeclarationKind.java | 127 +++++++++++++++++- .../basicimpl/FunctionDeclarationImpl.java | 17 ++- 3 files changed, 147 insertions(+), 2 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java b/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java index d697fddb34..873508bcf6 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclaration.java @@ -29,6 +29,11 @@ public interface FunctionDeclaration { */ String getName(); + /** + * @return List of indices for the function + */ + ImmutableList getIndices(); + /** * @return Sort of the function output. */ diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index a203fa1f2d..69f7d9a7bd 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -320,5 +320,130 @@ public enum FunctionDeclarationKind { * Solvers support a lot of different built-in theories. We enforce standardization only across a * small subset. */ - OTHER + OTHER; + + public static int getArity(FunctionDeclarationKind pKind) { + // TODO Add missing kinds + switch (pKind) { + case AND: + case OR: + case IFF: + case XOR: + case IMPLIES: + case DISTINCT: + case SUB: + case ADD: + case DIV: + case MUL: + case LT: + case LTE: + case GT: + case GTE: + case EQ: + case BV_CONCAT: + case BV_OR: + case BV_AND: + case BV_XOR: + case BV_SUB: + case BV_ADD: + case BV_MUL: + return -1; + + case FP_ROUND_EVEN: + case FP_ROUND_AWAY: + case FP_ROUND_POSITIVE: + case FP_ROUND_NEGATIVE: + case FP_ROUND_ZERO: + return 0; + + case NOT: + case UMINUS: + case EQ_ZERO: + case GTE_ZERO: + case FLOOR: + case TO_REAL: + case CONST: + case BV_EXTRACT: + case BV_SIGN_EXTENSION: + case BV_ZERO_EXTENSION: + case BV_NOT: + case BV_NEG: + case BV_ROTATE_LEFT_BY_INT: + case BV_ROTATE_RIGHT_BY_INT: + case FP_NEG: + case FP_ABS: + case FP_IS_NAN: + case FP_IS_INF: + case FP_IS_ZERO: + case FP_IS_NEGATIVE: + case FP_IS_SUBNORMAL: + case FP_IS_NORMAL: + case FP_AS_IEEEBV: + case FP_FROM_IEEEBV: + return 1; + + case SELECT: + case MODULO: + case BV_SDIV: + case BV_UDIV: + case BV_SREM: + case BV_UREM: + case BV_SMOD: + case BV_ULT: + case BV_SLT: + case BV_ULE: + case BV_SLE: + case BV_UGT: + case BV_SGT: + case BV_UGE: + case BV_SGE: + case BV_SHL: + case BV_LSHR: + case BV_ASHR: + case BV_ROTATE_LEFT: + case BV_ROTATE_RIGHT: + case BV_UCASTTO_FP: + case BV_SCASTTO_FP: + case FP_MAX: + case FP_MIN: + case FP_SQRT: + case FP_REM: + case FP_LT: + case FP_LE: + case FP_GE: + case FP_GT: + case FP_EQ: + case FP_ROUND_TO_INTEGRAL: + case FP_CASTTO_FP: + case FP_CASTTO_SBV: + case FP_CASTTO_UBV: + return 2; + + case ITE: + case STORE: + case FP_SUB: + case FP_ADD: + case FP_DIV: + case FP_MUL: + return 3; + + default: + throw new IllegalArgumentException(String.format("Unsupported kind: \"%s\"", pKind)); + } + } + + public static int getNumIndices(FunctionDeclarationKind pKind) { + // TODO Add missing kinds + switch (pKind) { + case BV_ROTATE_LEFT_BY_INT: + case BV_ROTATE_RIGHT_BY_INT: + case BV_SIGN_EXTENSION: + case BV_ZERO_EXTENSION: + return 1; + case BV_EXTRACT: + return 2; + default: + return 0; + } + } } diff --git a/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java b/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java index 5b276cfa64..5ccb34d291 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java +++ b/src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java @@ -26,11 +26,26 @@ public abstract class FunctionDeclarationImpl public static FunctionDeclaration of( String name, FunctionDeclarationKind kind, + List pIndices, List> pArgumentTypes, FormulaType pReturnType, T pDeclaration) { return new AutoValue_FunctionDeclarationImpl<>( - kind, name, pReturnType, ImmutableList.copyOf(pArgumentTypes), pDeclaration); + kind, + name, + ImmutableList.copyOf(pIndices), + pReturnType, + ImmutableList.copyOf(pArgumentTypes), + pDeclaration); + } + + public static FunctionDeclaration of( + String name, + FunctionDeclarationKind kind, + List> pArgumentTypes, + FormulaType pReturnType, + T pDeclaration) { + return of(name, kind, ImmutableList.of(), pArgumentTypes, pReturnType, pDeclaration); } /** From ded588893efa21ecbc5bc96e6acc41c4a7390c9d Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Mon, 25 Aug 2025 20:07:54 +0200 Subject: [PATCH 02/12] Indices: Add support for indexed functions symbols to the solver backends for Bitwuzla, CVC5, MathSAT, Princess and Z3 --- .../bitwuzla/BitwuzlaFormulaCreator.java | 7 +++- .../solvers/cvc5/CVC5FormulaCreator.java | 23 ++++++++--- .../mathsat5/Mathsat5FormulaCreator.java | 16 +++++++- .../princess/PrincessFormulaCreator.java | 40 ++++++++++++++----- .../java_smt/solvers/z3/Z3FormulaCreator.java | 13 +++++- 5 files changed, 79 insertions(+), 20 deletions(-) diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java index f946331319..2c524373d0 100644 --- a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java @@ -484,7 +484,12 @@ public R visit(FormulaVisitor visitor, Formula formula, Term f) formula, arguments.build(), FunctionDeclarationImpl.of( - name, getDeclarationKind(f), argumentTypes.build(), getFormulaType(f), decl)); + name, + getDeclarationKind(f), + ImmutableList.copyOf(f.indices()), + argumentTypes.build(), + getFormulaType(f), + decl)); } } 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 946b6be069..7a26cf71e3 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -452,7 +452,17 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { List> argsTypes = new ArrayList<>(); - // Term operator = normalize(f.getSort()); + // Collect indices + Op operator = f.getOp(); + ImmutableList.Builder indexBuilder = ImmutableList.builder(); + for (int p = 0; p < operator.getNumIndices(); p++) { + Term index = operator.get(p); + if (index.isIntegerValue()) { + indexBuilder.add(index.getIntegerValue().intValueExact()); + } + } + + // Collect arguments Kind kind = f.getKind(); if (sort.isFunction() || kind == Kind.APPLY_UF) { // The arguments are all children except the first one @@ -468,10 +478,6 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { } } - // TODO some operations (BV_SIGN_EXTEND, BV_ZERO_EXTEND, maybe more) encode information as - // part of the operator itself, thus the arity is one too small and there might be no - // possibility to access the information from user side. Should we encode such information - // as additional parameters? We do so for some methods of Princess. if (sort.isFunction()) { return visitor.visitFunction( formula, @@ -494,7 +500,12 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { formula, argsBuilder.build(), FunctionDeclarationImpl.of( - getName(f), getDeclarationKind(f), argsTypes, getFormulaType(f), normalize(f))); + getName(f), + getDeclarationKind(f), + indexBuilder.build(), + argsTypes, + getFormulaType(f), + normalize(f))); } } } catch (CVC5ApiException e) { 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 ff35694c4a..85b5c9c6dd 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -112,6 +112,7 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_repr; import com.google.common.base.Preconditions; +import com.google.common.base.Splitter; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import com.google.common.primitives.Longs; @@ -348,6 +349,18 @@ public R visit(FormulaVisitor visitor, Formula formula, final Long f) { return visitor.visitFreeVariable(formula, name); } + // Collect indices: We need to extract them from the term name in MathSAT + FunctionDeclarationKind kind = getDeclarationKind(f); + List tokens = + Splitter.on('_') + .splitToList(name.startsWith("`") ? name.substring(1, name.length() - 1) : name); + + ImmutableList.Builder indices = ImmutableList.builder(); + for (int p = 1; p <= FunctionDeclarationKind.getNumIndices(kind); p++) { + indices.add(Integer.valueOf(tokens.get(p))); + } + + // Now collect the arguments ImmutableList.Builder args = ImmutableList.builder(); ImmutableList.Builder> argTypes = ImmutableList.builder(); for (int i = 0; i < arity; i++) { @@ -365,7 +378,8 @@ public R visit(FormulaVisitor visitor, Formula formula, final Long f) { args.build(), FunctionDeclarationImpl.of( name, - getDeclarationKind(f), + kind, + indices.build(), argTypes.build(), getFormulaType(f), msat_term_get_decl(f))); 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 9de0d34811..d10b67df5a 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -488,16 +488,13 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression } } - ImmutableList.Builder args = ImmutableList.builder(); - ImmutableList.Builder> argTypes = ImmutableList.builder(); - int arity = input.length(); - int arityStart = 0; + int numSortParameters = getNumSortParameters(kind); + int numIndices = FunctionDeclarationKind.getNumIndices(kind); PrincessFunctionDeclaration solverDeclaration; - if (isBitvectorOperationWithAdditionalArgument(kind)) { + if (numSortParameters > 0) { // the first argument is the bitsize, and it is not relevant for the user. // we do not want type/sort information as arguments. - arityStart = 1; if (input instanceof IAtom) { solverDeclaration = new PrincessBitvectorToBooleanDeclaration(((IAtom) input).pred()); } else if (input instanceof IFunApp) { @@ -518,7 +515,17 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression solverDeclaration = new PrincessByExampleDeclaration(input); } - for (int i = arityStart; i < arity; i++) { + ImmutableList.Builder indices = ImmutableList.builder(); + + for (int i = numSortParameters; i < numSortParameters + numIndices; i++) { + IExpression term = input.apply(i); + indices.add(((IIntLit) term).value().intValue()); + } + + ImmutableList.Builder args = ImmutableList.builder(); + ImmutableList.Builder> argTypes = ImmutableList.builder(); + + for (int i = numSortParameters + numIndices; i < input.length(); i++) { IExpression arg = input.apply(i); FormulaType argumentType = getFormulaType(arg); args.add(encapsulate(argumentType, arg)); @@ -529,7 +536,12 @@ public R visit(FormulaVisitor visitor, final Formula f, final IExpression f, args.build(), FunctionDeclarationImpl.of( - getName(input), kind, argTypes.build(), getFormulaType(f), solverDeclaration)); + getName(input), + kind, + indices.build(), + argTypes.build(), + getFormulaType(f), + solverDeclaration)); } private R visitQuantifier(FormulaVisitor visitor, BooleanFormula f, IQuantified input) { @@ -569,7 +581,8 @@ private String getFreshVariableNameForBody(IFormula body) { body, k -> "__JAVASMT__BOUND_VARIABLE_" + boundVariableNames.size()); } - private boolean isBitvectorOperationWithAdditionalArgument(FunctionDeclarationKind kind) { + private int getNumSortParameters(FunctionDeclarationKind kind) { + // TODO Check that his is still right switch (kind) { case BV_NOT: case BV_NEG: @@ -593,9 +606,14 @@ private boolean isBitvectorOperationWithAdditionalArgument(FunctionDeclarationKi case BV_UGE: case BV_SGE: case BV_EQ: - return true; + case BV_LSHR: + case BV_ASHR: + case BV_SHL: + return 1; + case BV_CONCAT: + return 2; default: - return false; + return 0; } } 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 bde94b3e5f..6256909317 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -22,6 +22,7 @@ import com.microsoft.z3.Z3Exception; import com.microsoft.z3.enumerations.Z3_ast_kind; import com.microsoft.z3.enumerations.Z3_decl_kind; +import com.microsoft.z3.enumerations.Z3_param_kind; import com.microsoft.z3.enumerations.Z3_sort_kind; import com.microsoft.z3.enumerations.Z3_symbol_kind; import java.lang.ref.PhantomReference; @@ -492,7 +493,8 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long return visitor.visitConstant(formula, convertValue(f)); case Z3_APP_AST: int arity = Native.getAppNumArgs(environment, f); - int declKind = Native.getDeclKind(environment, Native.getAppDecl(environment, f)); + long decl = Native.getAppDecl(environment, f); + int declKind = Native.getDeclKind(environment, decl); if (arity == 0) { // constants @@ -538,6 +540,14 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long } } + ImmutableList.Builder indexBuilder = ImmutableList.builder(); + for (int p = 0; p < Native.getDeclNumParameters(environment, decl); p++) { + int kind = Native.getDeclParameterKind(environment, decl, p); + if (kind == Z3_param_kind.Z3_PK_UINT.toInt()) { + indexBuilder.add(Native.getDeclIntParameter(environment, decl, p)); + } + } + // Function application with zero or more parameters ImmutableList.Builder args = ImmutableList.builder(); ImmutableList.Builder> argTypes = ImmutableList.builder(); @@ -553,6 +563,7 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long FunctionDeclarationImpl.of( getAppName(f), getDeclarationKind(f), + indexBuilder.build(), argTypes.build(), getFormulaType(f), Native.getAppDecl(environment, f))); From ad9d94520356be2e012e2ac35613210bc1d905d8 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 2 Dec 2025 16:29:43 +0100 Subject: [PATCH 03/12] Fix merge --- src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java | 7 ------- 1 file changed, 7 deletions(-) diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java index dadf55aeeb..8d176adde3 100644 --- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java +++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java @@ -343,13 +343,6 @@ public static int getArity(FunctionDeclarationKind pKind) { case BV_MUL: return -1; - case FP_ROUND_EVEN: - case FP_ROUND_AWAY: - case FP_ROUND_POSITIVE: - case FP_ROUND_NEGATIVE: - case FP_ROUND_ZERO: - return 0; - case NOT: case UMINUS: case EQ_ZERO: From 38655e6f36c70e72209908777944c2989afddf5f Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 2 Dec 2025 19:34:24 +0100 Subject: [PATCH 04/12] Indices: Fix handling of bv_extract and bv_concat in Princess --- .../solvers/princess/PrincessEnvironment.java | 14 +++++++ .../princess/PrincessFormulaCreator.java | 38 +++++++++++++++++++ .../princess/PrincessFunctionDeclaration.java | 28 ++++++++++++++ 3 files changed, 80 insertions(+) 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 40aeaecb00..ac4539f504 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.basetypes.IdealInt; import ap.parameters.GlobalSettings; import ap.parser.BooleanCompactifier; import ap.parser.Environment.EnvironmentException; @@ -22,6 +23,7 @@ import ap.parser.IFunApp; import ap.parser.IFunction; import ap.parser.IIntFormula; +import ap.parser.IIntLit; import ap.parser.IPlus; import ap.parser.ITerm; import ap.parser.ITermITE; @@ -581,6 +583,18 @@ static FormulaType getFormulaType(IExpression pFormula) { FormulaType t1 = getFormulaType(plus.left()); FormulaType t2 = getFormulaType(plus.right()); return mergeFormulaTypes(t1, t2); + } else if (pFormula instanceof IFunApp + && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_extract())) { + IIntLit upper = (IIntLit) pFormula.apply(0); + IIntLit lower = (IIntLit) pFormula.apply(1); + IdealInt bwResult = upper.value().$minus(lower.value()); + return FormulaType.getBitvectorTypeWithSize(bwResult.intValue()); + } else if (pFormula instanceof IFunApp + && ((IFunApp) pFormula).fun().equals(ModuloArithmetic.bv_concat())) { + IIntLit upper = (IIntLit) pFormula.apply(0); + IIntLit lower = (IIntLit) pFormula.apply(1); + IdealInt bwResult = upper.value().$plus(lower.value()); + return FormulaType.getBitvectorTypeWithSize(bwResult.intValue()); } else { final Sort sort = Sort$.MODULE$.sortOf((ITerm) pFormula); try { 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 2d28758ecf..5827f0a5c2 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFormulaCreator.java @@ -396,6 +396,44 @@ private static boolean isValue(IExpression input) { public R visit(FormulaVisitor visitor, final Formula f, final IExpression input) { if (isValue(input)) { return visitor.visitConstant(f, convertValue(input)); + } else if (input instanceof IFunApp + && ((IFunApp) input).fun().equals(ModuloArithmetic.bv_extract())) { + var kind = FunctionDeclarationKind.BV_EXTRACT; + var upper = ((IIntLit) input.apply(0)).value().intValue(); + var lower = ((IIntLit) input.apply(1)).value().intValue(); + var arg = input.apply(2); + var argType = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg); + + return visitor.visitFunction( + f, + ImmutableList.of(encapsulateWithTypeOf(arg)), + FunctionDeclarationImpl.of( + kind.toString(), + kind, + ImmutableList.of(upper, lower), + ImmutableList.of(argType), + FormulaType.getBitvectorTypeWithSize(upper - lower), + new PrincessFunctionDeclaration.PrincessBitvectorExtractDeclaration(upper, lower))); + + } else if (input instanceof IFunApp + && ((IFunApp) input).fun().equals(ModuloArithmetic.bv_concat())) { + var kind = FunctionDeclarationKind.BV_CONCAT; + var size1 = ((IIntLit) input.apply(0)).value().intValue(); + var size2 = ((IIntLit) input.apply(1)).value().intValue(); + var arg1 = input.apply(2); + var arg2 = input.apply(3); + var arg1Type = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg1); + var arg2Type = (FormulaType.BitvectorType) PrincessEnvironment.getFormulaType(arg2); + + return visitor.visitFunction( + f, + ImmutableList.of(encapsulateWithTypeOf(arg1), encapsulateWithTypeOf(arg2)), + FunctionDeclarationImpl.of( + kind.toString(), + kind, + ImmutableList.of(arg1Type, arg2Type), + FormulaType.getBitvectorTypeWithSize(size1 + size2), + new PrincessFunctionDeclaration.PrincessBitvectorConcatDeclaration())); } else if (input instanceof IQuantified) { return visitQuantifier(visitor, (BooleanFormula) f, (IQuantified) input); diff --git a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java index 670d2f1521..d33dae2d7c 100644 --- a/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java +++ b/src/org/sosy_lab/java_smt/solvers/princess/PrincessFunctionDeclaration.java @@ -24,6 +24,7 @@ import ap.parser.ITermITE; import ap.terfor.ConstantTerm; import ap.terfor.preds.Predicate; +import ap.theories.bitvectors.ModuloArithmetic$; import ap.theories.nia.GroebnerMultiplication; import ap.types.MonoSortedIFunction; import ap.types.Sort; @@ -236,4 +237,31 @@ public IExpression makeApp(PrincessEnvironment env, List args) { return GroebnerMultiplication.mult((ITerm) args.get(0), (ITerm) args.get(1)); } } + + static class PrincessBitvectorExtractDeclaration extends PrincessFunctionDeclaration { + private final int upper; + private final int lower; + + PrincessBitvectorExtractDeclaration(int pUpper, int pLower) { + upper = pUpper; + lower = pLower; + } + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 1); + return ModuloArithmetic$.MODULE$.extract(upper, lower, (ITerm) args.get(0)); + } + } + + static class PrincessBitvectorConcatDeclaration extends PrincessFunctionDeclaration { + + PrincessBitvectorConcatDeclaration() {} + + @Override + public IExpression makeApp(PrincessEnvironment env, List args) { + checkArgument(args.size() == 2); + return ModuloArithmetic$.MODULE$.concat((ITerm) args.get(0), (ITerm) args.get(1)); + } + } } From 25335f33fe9066d1c2acb5cdb6016515a18e133c Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 2 Dec 2025 20:02:42 +0100 Subject: [PATCH 05/12] Indices: Fix CVC5 visitor for sep.nil --- src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java | 3 +++ 1 file changed, 3 insertions(+) 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 a2c4d18ef5..f2833dc817 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -449,6 +449,9 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { } else if (f.getKind() == Kind.CONSTANT) { return visitor.visitFreeVariable(formula, dequote(f.toString())); + } else if (f.getKind() == Kind.SEP_NIL) { + return visitor.visitConstant(formula, null); + } else if (f.getKind() == Kind.APPLY_CONSTRUCTOR) { Preconditions.checkState( f.getNumChildren() == 1, "Unexpected formula '%s' with sort '%s'", f, f.getSort()); From 1c900421421d21335d24ec8fed5dfa6373e8ada5 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 27 Feb 2026 23:06:21 +0100 Subject: [PATCH 06/12] Indices: Add support for new solver "Z3 with interpolation" --- .../solvers/z3legacy/Z3LegacyFormulaCreator.java | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java index 2dc6da4ddf..d36242bd53 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3legacy/Z3LegacyFormulaCreator.java @@ -26,6 +26,7 @@ import com.microsoft.z3legacy.Z3Exception; import com.microsoft.z3legacy.enumerations.Z3_ast_kind; import com.microsoft.z3legacy.enumerations.Z3_decl_kind; +import com.microsoft.z3legacy.enumerations.Z3_param_kind; import com.microsoft.z3legacy.enumerations.Z3_sort_kind; import com.microsoft.z3legacy.enumerations.Z3_symbol_kind; import java.lang.ref.PhantomReference; @@ -536,7 +537,8 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long return visitor.visitConstant(formula, convertValue(f)); case Z3_APP_AST: int arity = Native.getAppNumArgs(environment, f); - int declKind = Native.getDeclKind(environment, Native.getAppDecl(environment, f)); + long decl = Native.getAppDecl(environment, f); + int declKind = Native.getDeclKind(environment, decl); if (arity == 0) { // constants @@ -582,6 +584,14 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long } } + ImmutableList.Builder indexBuilder = ImmutableList.builder(); + for (int p = 0; p < Native.getDeclNumParameters(environment, decl); p++) { + int kind = Native.getDeclParameterKind(environment, decl, p); + if (kind == Z3_param_kind.Z3_PK_UINT.toInt()) { + indexBuilder.add(Native.getDeclIntParameter(environment, decl, p)); + } + } + // Function application with zero or more parameters ImmutableList.Builder args = ImmutableList.builder(); ImmutableList.Builder> argTypes = ImmutableList.builder(); @@ -597,6 +607,7 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long FunctionDeclarationImpl.of( getAppName(f), getDeclarationKind(f), + indexBuilder.build(), argTypes.build(), getFormulaType(f), Native.getAppDecl(environment, f))); From a0fdbc1650cc621fe90ae2fad71ae28d856116d8 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Fri, 27 Feb 2026 23:05:41 +0100 Subject: [PATCH 07/12] Indices: Add tests for visiting indexed functions --- .../java_smt/test/SolverVisitorTest.java | 51 +++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index f93e4ebf3c..aabd08742d 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -640,6 +640,57 @@ protected Void visitDefault(Formula f) { } } + private static class CheckIndexed extends DefaultFormulaVisitor { + private final FunctionDeclarationKind kind; + private final List index; + + private CheckIndexed(FunctionDeclarationKind pKind, List pIndex) { + kind = pKind; + index = pIndex; + } + + @Override + protected Void visitDefault(Formula f) { + return null; + } + + @Override + public Void visitFunction( + Formula f, List args, FunctionDeclaration functionDeclaration) { + assertThat(functionDeclaration.getKind()).isEqualTo(kind); + assertThat(functionDeclaration.getIndices()).isEqualTo(index); + return visitDefault(f); + } + } + + @Test + public void bvExtractVisit() { + requireBitvectors(); + assume() + .withMessage("Visiting indexed functions not fully supported on %") + .that(solver) + .isNoneOf(Solvers.CVC4, Solvers.YICES2); + + var x = bvmgr.makeVariable(8, "x"); + var f = bvmgr.extract(x, 3, 0); + + mgr.visit(f, new CheckIndexed(FunctionDeclarationKind.BV_EXTRACT, ImmutableList.of(3, 0))); + } + + @Test + public void bvExtendVisit() { + requireBitvectors(); + assume() + .withMessage("Visiting indexed functions not fully supported on %") + .that(solver) + .isNoneOf(Solvers.CVC4, Solvers.YICES2, Solvers.PRINCESS); + + var x = bvmgr.makeVariable(8, "x"); + var f = bvmgr.extend(x, 8, false); + + mgr.visit(f, new CheckIndexed(FunctionDeclarationKind.BV_ZERO_EXTENSION, ImmutableList.of(8))); + } + @Test public void bvVisit() throws SolverException, InterruptedException { requireBitvectors(); From 493cd9443596ec92c949e98b97bba0982913a7a5 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 28 Mar 2026 14:21:46 +0100 Subject: [PATCH 08/12] Indices: Fix indices in CVC5 visitor We need to check `hasOp` before getting the operator of a term to extract the indices. Otherwise, it will crash for SEP_EMP, which has no operator --- .../solvers/cvc5/CVC5FormulaCreator.java | 36 ++++++++++--------- 1 file changed, 20 insertions(+), 16 deletions(-) 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 6aaa43f476..c6906d551d 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -470,34 +470,34 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { } else { // Term expressions like uninterpreted function calls (Kind.APPLY_UF) or operators (e.g. // Kind.AND). - // These are all treated like operators, so we can get the declaration by f.getOperator()! - - ImmutableList.Builder argsBuilder = ImmutableList.builder(); - - List> argsTypes = new ArrayList<>(); + Kind kind = f.getKind(); // Collect indices - Op operator = f.getOp(); ImmutableList.Builder indexBuilder = ImmutableList.builder(); - for (int p = 0; p < operator.getNumIndices(); p++) { - Term index = operator.get(p); - if (index.isIntegerValue()) { - indexBuilder.add(index.getIntegerValue().intValueExact()); + if (f.hasOp()) { + Op operator = f.getOp(); + for (int p = 0; p < operator.getNumIndices(); p++) { + Term index = operator.get(p); + if (index.isIntegerValue()) { + indexBuilder.add(index.getIntegerValue().intValueExact()); + } } } // Collect arguments - Kind kind = f.getKind(); + ImmutableList.Builder argsBuilder = ImmutableList.builder(); + ImmutableList.Builder> argTypesBuilder = ImmutableList.builder(); + if (sort.isFunction() || kind == Kind.APPLY_UF) { // The arguments are all children except the first one for (int i = 1; i < f.getNumChildren(); i++) { - argsTypes.add(getFormulaTypeFromTermType(f.getChild(i).getSort())); + argTypesBuilder.add(getFormulaTypeFromTermType(f.getChild(i).getSort())); // CVC5s first argument in a function/Uf is the declaration, we don't need that here argsBuilder.add(encapsulate(f.getChild(i))); } } else { for (Term arg : f) { - argsTypes.add(getFormulaType(arg)); + argTypesBuilder.add(getFormulaType(arg)); argsBuilder.add(encapsulate(arg)); } } @@ -507,7 +507,11 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { formula, argsBuilder.build(), FunctionDeclarationImpl.of( - getName(f), getDeclarationKind(f), argsTypes, getFormulaType(f), normalize(f))); + getName(f), + getDeclarationKind(f), + argTypesBuilder.build(), + getFormulaType(f), + normalize(f))); } else if (kind == Kind.APPLY_UF) { return visitor.visitFunction( formula, @@ -515,7 +519,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { FunctionDeclarationImpl.of( getName(f), getDeclarationKind(f), - argsTypes, + argTypesBuilder.build(), getFormulaType(f), normalize(f.getChild(0)))); } else { @@ -527,7 +531,7 @@ public R visit(FormulaVisitor visitor, Formula formula, final Term f) { getName(f), getDeclarationKind(f), indexBuilder.build(), - argsTypes, + argTypesBuilder.build(), getFormulaType(f), normalize(f))); } From b5406d7c145949550b6a163f78941dc6115eaf65 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 28 Mar 2026 21:51:10 +0100 Subject: [PATCH 09/12] Indices: Add support for indexed functions in the tracer --- .../delegate/trace/TraceFormulaManager.java | 51 +++++++++++++++---- 1 file changed, 40 insertions(+), 11 deletions(-) diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java index 9001747dd6..390cfa7d5c 100644 --- a/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java @@ -10,6 +10,7 @@ package org.sosy_lab.java_smt.delegate.trace; +import static com.google.common.base.Preconditions.checkArgument; import static org.sosy_lab.common.collect.Collections3.transformedImmutableListCopy; import static org.sosy_lab.common.collect.Collections3.transformedImmutableSetCopy; @@ -567,17 +568,38 @@ public T makeApplication( } else { return (T) getRationalFormulaManager().floor((NumeralFormula) args.get(0)); } - // FIXME Requires indexed functions - // case INT_TO_BV: - // case BV_EXTRACT: + case INT_TO_BV: + checkArgument(declaration.getIndices().size() == 1); + return (T) + getBitvectorFormulaManager() + .makeBitvector(declaration.getIndices().get(0), (IntegerFormula) args.get(0)); + case BV_EXTRACT: + return (T) + getBitvectorFormulaManager() + .extract( + (BitvectorFormula) args.get(0), + declaration.getIndices().get(0), + declaration.getIndices().get(1)); case BV_CONCAT: - Preconditions.checkArgument(args.size() == 2); + checkArgument(!args.isEmpty(), "Expected at least one argument"); + var concat = (T) args.get(0); + for (var p = 1; p < args.size(); p++) { + concat = + (T) + getBitvectorFormulaManager() + .concat((BitvectorFormula) concat, (BitvectorFormula) args.get(p)); + } + return concat; + case BV_SIGN_EXTENSION: + checkArgument(declaration.getIndices().size() == 1); return (T) getBitvectorFormulaManager() - .concat((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); - // FIXME Requires indexed functions - // case BV_SIGN_EXTENSION: - // case BV_ZERO_EXTENSION: + .extend((BitvectorFormula) args.get(0), declaration.getIndices().get(0), true); + case BV_ZERO_EXTENSION: + checkArgument(declaration.getIndices().size() == 1); + return (T) + getBitvectorFormulaManager() + .extend((BitvectorFormula) args.get(0), declaration.getIndices().get(0), false); case BV_NOT: return (T) getBitvectorFormulaManager().not((BitvectorFormula) args.get(0)); case BV_NEG: @@ -696,9 +718,16 @@ public T makeApplication( return (T) getBitvectorFormulaManager() .rotateRight((BitvectorFormula) args.get(0), (BitvectorFormula) args.get(1)); - // FIXME Requires indexed functions - // case BV_ROTATE_LEFT_BY_INT: - // case BV_ROTATE_RIGHT_BY_INT: + case BV_ROTATE_LEFT_BY_INT: + checkArgument(declaration.getIndices().size() == 1); + return (T) + getBitvectorFormulaManager() + .rotateLeft((BitvectorFormula) args.get(0), declaration.getIndices().get(0)); + case BV_ROTATE_RIGHT_BY_INT: + checkArgument(declaration.getIndices().size() == 1); + return (T) + getBitvectorFormulaManager() + .rotateRight((BitvectorFormula) args.get(0), declaration.getIndices().get(0)); case BV_UCASTTO_FP: return (T) getFloatingPointFormulaManager() From 8a5f5d3c35d9cf1af80369a8eda4cff74b04bded Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sat, 28 Mar 2026 23:23:50 +0100 Subject: [PATCH 10/12] Indices: Add support for indices in Yices, and update the tests --- .../solvers/yices2/Yices2FormulaCreator.java | 7 +- .../java_smt/test/SolverVisitorTest.java | 81 ++++++++++++++----- 2 files changed, 65 insertions(+), 23 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 cead1976d0..9bfccf544c 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2FormulaCreator.java @@ -555,7 +555,12 @@ private R visitFunctionApplication( pFormula, args, FunctionDeclarationImpl.of( - functionName, functionKind, argTypes, getFormulaType(pF), functionDeclaration)); + functionName, + functionKind, + functionIndex, + argTypes, + getFormulaType(pF), + functionDeclaration)); } private int buildDeclaration( diff --git a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java index 923f518734..3bb23593d8 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -640,27 +640,41 @@ protected Void visitDefault(Formula f) { } } - private static class CheckIndexed extends DefaultFormulaVisitor { - private final FunctionDeclarationKind kind; - private final List index; + private void checkIndexedSymbol( + FunctionDeclarationKind pExpectedKind, List pExpectedIndex, Formula pTerm) { + mgr.visit( + pTerm, + new DefaultFormulaVisitor() { + @Override + public Void visitFunction( + Formula f, List args, FunctionDeclaration functionDeclaration) { + assertThat(functionDeclaration.getKind()).isEqualTo(pExpectedKind); + assertThat(functionDeclaration.getIndices()).isEqualTo(pExpectedIndex); + return null; + } - private CheckIndexed(FunctionDeclarationKind pKind, List pIndex) { - kind = pKind; - index = pIndex; - } + @Override + protected Void visitDefault(Formula f) { + throw new AssertionError(); + } + }); + } - @Override - protected Void visitDefault(Formula f) { - return null; - } + private List getArgs(Formula pFormula) { + return mgr.visit( + pFormula, + new DefaultFormulaVisitor<>() { + @Override + public List visitFunction( + Formula f, List args, FunctionDeclaration functionDeclaration) { + return args; + } - @Override - public Void visitFunction( - Formula f, List args, FunctionDeclaration functionDeclaration) { - assertThat(functionDeclaration.getKind()).isEqualTo(kind); - assertThat(functionDeclaration.getIndices()).isEqualTo(index); - return visitDefault(f); - } + @Override + protected List visitDefault(Formula f) { + throw new AssertionError(); + } + }); } @Test @@ -669,12 +683,22 @@ public void bvExtractVisit() { assume() .withMessage("Visiting indexed functions not fully supported on %") .that(solver) - .isNoneOf(Solvers.CVC4, Solvers.YICES2); + .isNotEqualTo(Solvers.CVC4); var x = bvmgr.makeVariable(8, "x"); var f = bvmgr.extract(x, 3, 0); - mgr.visit(f, new CheckIndexed(FunctionDeclarationKind.BV_EXTRACT, ImmutableList.of(3, 0))); + if (solver == Solvers.YICES2) { + // Yices2 will rewrite to (bv-array (bit x 3) (bit x 2) (bit x 1) (bit x 0)) + var args = getArgs(f); + assertThat(args.size()).isEqualTo(4); + for (var p = 0; p < args.size(); p++) { + checkIndexedSymbol( + FunctionDeclarationKind.BV_EXTRACT, ImmutableList.of(3 - p, 3 - p), args.get(p)); + } + } else { + checkIndexedSymbol(FunctionDeclarationKind.BV_EXTRACT, ImmutableList.of(3, 0), f); + } } @Test @@ -683,12 +707,25 @@ public void bvExtendVisit() { assume() .withMessage("Visiting indexed functions not fully supported on %") .that(solver) - .isNoneOf(Solvers.CVC4, Solvers.YICES2, Solvers.PRINCESS); + .isNoneOf(Solvers.CVC4, Solvers.PRINCESS); var x = bvmgr.makeVariable(8, "x"); var f = bvmgr.extend(x, 8, false); - mgr.visit(f, new CheckIndexed(FunctionDeclarationKind.BV_ZERO_EXTENSION, ImmutableList.of(8))); + if (solver == Solvers.YICES2) { + // Yices2 will rewrite to (bv-array #b0 ... #b0 (bit x 7) ... (bit x 0) + var terms = getArgs(f); + assertThat(terms.size()).isEqualTo(16); + for (var p = 0; p < terms.size(); p++) { + if (p < 8) { + assertThat(terms.get(p)).isEqualTo(bvmgr.makeBitvector(1, 0)); + } else { + assertThat(terms.get(p)).isEqualTo(bvmgr.extract(f, 15 - p, 15 - p)); + } + } + } else { + checkIndexedSymbol(FunctionDeclarationKind.BV_ZERO_EXTENSION, ImmutableList.of(8), f); + } } @Test From 0e184c2394deda380659d354dbea20edfeb54768 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 29 Mar 2026 03:25:23 +0200 Subject: [PATCH 11/12] Indices: Remove duplicate code --- .../delegate/trace/TraceFormulaManager.java | 133 +----------------- 1 file changed, 1 insertion(+), 132 deletions(-) diff --git a/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java b/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java index 098e26f907..8031ab6f70 100644 --- a/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java +++ b/src/org/sosy_lab/java_smt/delegate/trace/TraceFormulaManager.java @@ -271,138 +271,7 @@ public T makeVariable(FormulaType formulaType, String nam } private int getArity(FunctionDeclaration pDeclaration) { - return switch (pDeclaration.getKind()) { - case AND, - OR, - IFF, - XOR, - IMPLIES, - DISTINCT, - SUB, - ADD, - DIV, - MUL, - LT, - LTE, - GT, - GTE, - EQ, - BV_CONCAT, - BV_OR, - BV_AND, - BV_XOR, - BV_SUB, - BV_ADD, - BV_MUL, - STR_CONCAT, - STR_LT, - STR_LE, - RE_CONCAT, - RE_DIFFERENCE, - RE_UNION, - RE_INTERSECT -> - -1; - case RE_NONE, SEP_NIL -> 0; - case INT_TO_BV, - NOT, - UMINUS, - EQ_ZERO, - GTE_ZERO, - FLOOR, - TO_REAL, - CONST, - BV_EXTRACT, - BV_SIGN_EXTENSION, - BV_ZERO_EXTENSION, - BV_NOT, - BV_NEG, - BV_ROTATE_LEFT_BY_INT, - BV_ROTATE_RIGHT_BY_INT, - UBV_TO_INT, - SBV_TO_INT, - FP_NEG, - FP_ABS, - FP_IS_NAN, - FP_IS_INF, - FP_IS_ZERO, - FP_IS_NEGATIVE, - FP_IS_SUBNORMAL, - FP_IS_NORMAL, - FP_AS_IEEEBV, - FP_FROM_IEEEBV, - RE_PLUS, - RE_STAR, - INT_TO_STR, - STR_FROM_CODE, - STR_TO_CODE, - STR_LENGTH, - STR_TO_INT, - STR_TO_RE, - RE_COMPLEMENT, - RE_OPTIONAL -> - 1; - case SELECT, - MODULO, - BV_SDIV, - BV_UDIV, - BV_SREM, - BV_UREM, - BV_SMOD, - BV_ULT, - BV_SLT, - BV_ULE, - BV_SLE, - BV_UGT, - BV_SGT, - BV_UGE, - BV_SGE, - BV_SHL, - BV_LSHR, - BV_ASHR, - BV_ROTATE_LEFT, - BV_ROTATE_RIGHT, - BV_UCASTTO_FP, - BV_SCASTTO_FP, - FP_MAX, - FP_MIN, - FP_SQRT, - FP_REM, - FP_LT, - FP_LE, - FP_GE, - FP_GT, - FP_EQ, - FP_ROUND_TO_INTEGRAL, - FP_CASTTO_FP, - FP_CASTTO_SBV, - FP_CASTTO_UBV, - STR_CHAR_AT, - STR_CONTAINS, - STR_IN_RE, - STR_PREFIX, - STR_SUFFIX, - RE_RANGE, - SEP_PTO, - SEP_EMP, - SEP_STAR, - SEP_WAND -> - 2; - case ITE, - STORE, - FP_SUB, - FP_ADD, - FP_DIV, - FP_MUL, - STR_INDEX_OF, - STR_REPLACE, - STR_REPLACE_ALL, - STR_SUBSTRING -> - 3; - default -> - throw new IllegalArgumentException( - "Unsupported kind: \"%s\" (%s)" - .formatted(pDeclaration.getName(), pDeclaration.getKind())); - }; + return FunctionDeclarationKind.getArity(pDeclaration.getKind()); } @SuppressWarnings({"unchecked", "rawtypes"}) From bbae8f0640047223fb2df1307baa11aaefe65b05 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Sun, 29 Mar 2026 03:54:38 +0200 Subject: [PATCH 12/12] Apply refaster patch --- src/org/sosy_lab/java_smt/test/SolverVisitorTest.java | 4 ++-- 1 file changed, 2 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 13a751a676..68c9d28976 100644 --- a/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverVisitorTest.java @@ -691,7 +691,7 @@ public void bvExtractVisit() { if (solver == Solvers.YICES2) { // Yices2 will rewrite to (bv-array (bit x 3) (bit x 2) (bit x 1) (bit x 0)) var args = getArgs(f); - assertThat(args.size()).isEqualTo(4); + assertThat(args).hasSize(4); for (var p = 0; p < args.size(); p++) { checkIndexedSymbol( FunctionDeclarationKind.BV_EXTRACT, ImmutableList.of(3 - p, 3 - p), args.get(p)); @@ -715,7 +715,7 @@ public void bvExtendVisit() { if (solver == Solvers.YICES2) { // Yices2 will rewrite to (bv-array #b0 ... #b0 (bit x 7) ... (bit x 0) var terms = getArgs(f); - assertThat(terms.size()).isEqualTo(16); + assertThat(terms).hasSize(16); for (var p = 0; p < terms.size(); p++) { if (p < 8) { assertThat(terms.get(p)).isEqualTo(bvmgr.makeBitvector(1, 0));