Add indexed functions to JavaSMT

[daniel-raffler]

Hello,

in Smtlib some functions take additional indices as parameters. An example for this is extract for bitvectors, which takes two additional integers to define the range of bits that should be extracted. In Smtlib this is written as ((_ extract i j) x), where i is the highest bit, and j the lowest bit that will be extracted. More mathematically, the expression could be written as $extract_{i,j}(x)$. Note that indices "belong" to the function symbol, and are not part of the arguments. Unlike real arguments, indices are not formulas, but constant values. Generally this means they are numerals (= positive integers), but since 2.7 symbols (as in (_ round up)) are also allowed

In JavaSmt we can create the above formula with BitvectorFormulaManager.extract(x, i, j). However, there is no way to get the indices back from the formula. This causes problems, for instance when printing formulas with a Visitor, or in the tracing delegate, which needs to rebuild formulas, and has to know the value of the indices

Note that I had already opened a PR here that tries to solve the issue by adding a new method FunctionDeclaration.getIndices that allows access to the indices of a function. However, there might be some other ways to solve the problem, and we can discuss them here:

• We could treat indices just like normal arguments. In that case ((_ extract i j) x) becomes (extract i j x) and there is no need for any new methods. One downside is that users will then have to remember that the first two arguments aren't really arguments and require special treatment. It also changes the arity of the function, and JavaSMT doesn't have a good formula type to wrap the indices that would work on all solvers
• We could encode the indices as part of the function name. In that case ((_ extact i j) x) would be written as (extract_i_j x) and users can simply reconstruct the indices. This means altering the names returned by FunctionDeclaration.getName for most solvers, and introducing our own scheme to encode indices as part of the String. While this doesn't technically change the API, it might still cause problems for users that depend on specific function names

The first option is used in Princess, while MathSat uses the second scheme, so both solutions seem to work in practice