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

@@ -314,5 +314,123 @@ 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 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;
+    }
+  }
 }

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

@@ -26,11 +26,26 @@ public abstract class FunctionDeclarationImpl<F extends Formula, T>
   public static <F extends Formula, T> FunctionDeclaration<F> of(
       String name,
       FunctionDeclarationKind kind,
+      List<Integer> pIndices,
       List<FormulaType<?>> pArgumentTypes,
       FormulaType<F> 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 <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);
   }
 
   /**

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java

@@ -494,7 +494,12 @@ public <R> R visit(FormulaVisitor<R> 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));
     }
   }
 

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java

@@ -449,6 +449,9 @@ public <R> R visit(FormulaVisitor<R> 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());
@@ -463,7 +466,17 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Term f) {
 
         List<FormulaType<?>> argsTypes = new ArrayList<>();
 
-        // Term operator = normalize(f.getSort());
+        // Collect indices
+        Op operator = f.getOp();
+        ImmutableList.Builder<Integer> 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
@@ -479,10 +492,6 @@ public <R> R visit(FormulaVisitor<R> 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,
@@ -505,7 +514,12 @@ public <R> R visit(FormulaVisitor<R> 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) {

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java

@@ -119,6 +119,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;
@@ -369,6 +370,18 @@ && msat_is_enum_type(environment, msat_term_get_type(f))) {
         return visitor.visitFreeVariable(formula, name);
       }
 
+      // Collect indices: We need to extract them from the term name in MathSAT
+      FunctionDeclarationKind kind = getDeclarationKind(f);
+      List<String> tokens =
+          Splitter.on('_')
+              .splitToList(name.startsWith("`") ? name.substring(1, name.length() - 1) : name);
+
+      ImmutableList.Builder<Integer> 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<Formula> args = ImmutableList.builder();
       ImmutableList.Builder<FormulaType<?>> argTypes = ImmutableList.builder();
       for (int i = 0; i < arity; i++) {
@@ -386,7 +399,8 @@ && msat_is_enum_type(environment, msat_term_get_type(f))) {
           args.build(),
           FunctionDeclarationImpl.of(
               name,
-              getDeclarationKind(f),
+              kind,
+              indices.build(),
               argTypes.build(),
               getFormulaType(f),
               msat_term_get_decl(f)));

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 {