Add support for indexed functions

src/org/sosy_lab/java_smt/api/FunctionDeclaration.java

@@ -29,6 +29,11 @@ public interface FunctionDeclaration<E extends Formula> {
    */
   String getName();
 
+  /**
+   * @return List of indices for the function
+   */
+  ImmutableList<Integer> getIndices();
+
   /**
    * @return Sort of the function output.
    */

src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java

@@ -323,5 +323,147 @@ 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) {
+    return switch (pKind) {
+      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(String.format("Unsupported kind: \"%s\"", pKind));
+    };
+  }
+
+  public static int getNumIndices(FunctionDeclarationKind pKind) {
+    // TODO Add missing kinds
+    return switch (pKind) {
+      case BV_ROTATE_LEFT_BY_INT, BV_ROTATE_RIGHT_BY_INT, BV_SIGN_EXTENSION, BV_ZERO_EXTENSION -> 1;
+      case BV_EXTRACT -> 2;
+      default -> 0;
+    };
+  }
 }

src/org/sosy_lab/java_smt/basicimpl/FunctionDeclarationImpl.java

@@ -23,6 +23,7 @@
 public record FunctionDeclarationImpl<F extends Formula, T>(
     FunctionDeclarationKind getKind,
     String getName,
+    ImmutableList<Integer> getIndices,
     FormulaType<F> getType,
     ImmutableList<FormulaType<?>> getArgumentTypes,
     T getSolverDeclaration)
@@ -31,6 +32,7 @@ public record FunctionDeclarationImpl<F extends Formula, T>(
   public FunctionDeclarationImpl {
     checkNotNull(getKind);
     checkNotNull(getName);
+    checkNotNull(getIndices);
     checkNotNull(getType);
     checkNotNull(getArgumentTypes);
     checkNotNull(getSolverDeclaration);
@@ -39,11 +41,26 @@ public record FunctionDeclarationImpl<F extends Formula, T>(
   public static <F extends Formula, T> FunctionDeclarationImpl<F, T> of(
       String name,
       FunctionDeclarationKind kind,
+      List<Integer> pIndices,
       List<FormulaType<?>> pArgumentTypes,
       FormulaType<F> pReturnType,
       T pDeclaration) {
     return new FunctionDeclarationImpl<>(
-        kind, name, pReturnType, ImmutableList.copyOf(pArgumentTypes), pDeclaration);
+        kind,
+        name,
+        ImmutableList.copyOf(pIndices),
+        pReturnType,
+        ImmutableList.copyOf(pArgumentTypes),
+        pDeclaration);
+  }
+
+  public static <F extends Formula, T> FunctionDeclaration<F> of(
+      String name,
+      FunctionDeclarationKind kind,
+      List<FormulaType<?>> pArgumentTypes,
+      FormulaType<F> pReturnType,
+      T pDeclaration) {
+    return of(name, kind, ImmutableList.of(), pArgumentTypes, pReturnType, pDeclaration);
   }
 
   @Override