Add support for indexed functions

[daniel-raffler]

Hello,
this PR will add support for indexed functions to the JavaSMT API. In indexed functions take additional arguments that are not terms, but have to be constant. One example is (_ extract i j) for bitvector, which takes two more parameters i and j to specify the range of bits that should be returned. While extract is available in BitvectorFormulaManager and we can create the term in JavaSMT, we've so far lacked a way to access the indices in the visitor.

In this PR we will address the problem by adding a new method ImmutableList<Integer> getIndices() to the FunctionDeclaration API and implementing it for all solvers. In the FormulaVisitor the method can then be used to get the values of the parameters from the function symbol:

new FormulaVisitor<Formula>() {
  @Override
    public Formula visitFunction(
      Formula f,
      List<Formula> args,
      FunctionDeclaration<?> functionDeclaration) {
    List<Integer> params = functionDeclaration.getIndices();
    if (functionDeclaration.getKind().equals(FunctionDeclarationKind.BV_EXTRACT)) {
      // Use the indices to recreate the formula
      return bvmgr.extract((BitvectorFormula) args.get(0), params.get(0), params.get(1));
    }
  }
}

Open issues

• Fix the implementation for Princess

[kfriedberger]

My first thought was that we can actually model all indices as plain IntegerFormula-based arguments and just revert this encoding on usage. Seperating the concept of arguments into "args and indices" while still having methods that allow both, seems weird.

For example, BV_ROTATE_LEFT exists in two versions, one with integer-based shift (modeled as index), one with IntegerFormula-based shift (modeled as argument).

Please give some more reason to model indices separatelly.

[kfriedberger]

Please extend the documentation for this interface method.
Here, we need some strong argument and description for differentiation between args and indices.

[daniel-raffler]

Hello Karlheinz,
thanks a lot for the feedback!

My first thought was that we can actually model all indices as plain IntegerFormula-based arguments and just revert this encoding on usage.

I think this could work too, and in fact this seems to be close to what Princess is doing. There are a few caveats:

• Not all solvers support integers. Specifically Bitwuzla only has Bitvectors and we would have to add use some dummy integer formulas just to store the indices
• If we do use integer fomulas for the indices it would probably break FormulaClassifier and similar classes that check for formula types
• More generally the arity of the symbols changes and formula visitors may have to be rewritten so that they recognize formulas with indices and then treat them separately

These issues can probably be solved, but I think from the user's perspective it would be less disruptive to simply extend FunctionDeclaration with indices. If the indices are not needed they can simply continue using their old code. On the other hand, if they do need to use the indices, the new API shouldn't be too complicated, and it is very close to what SMTLIB (and most solvers) are doing internally. Users would still have to recompile as we're changing FunctionDeclaration and FunctionDeclarationImpl. However, since those are essentially internal classes, their code should not be affected.

Please give some more reason to model indices separatelly.

The difference between indices/parameters and arguments is that arguments can be any formula, while indices need to be constant values. So, for instance, in ((extract i j) a) the type of a would be BitvectorFomula, but indices i, J need to be "numerals", that is positive integer values.

If we treat the indices as regular formulas this might cause issues as visitors would then have to remember that only constant values are allowed in this position.