Utility methods on FunctionDeclarationKind

[PhilippWendler]

FunctionDeclarationKind is an enum with quite a lot of cases that belong to different categories. When using this enum, e.g., in a visitor, it is likely common that one wants to handle related cases together in the same or a similar way. But there is no way to do this instead of hard-coding lists of related cases. I think it would be quite useful if the enum would have methods that one can use to distinguish categories such as the following:

• arity, i.e., is the function unary, binary, ternary, n-ary
• related theory, i.e., is the function valid (only) for bitvectors, floats, numeric, boolean, array, string, etc. parameters,
• semantics, e.g., is it a comparison operation or even an (in-)equality.

[shivammm21]

Helo team,
I’d like to work on this. I’ll add support for rotateLeft and rotateRight in BitvectorFormulaManager, and implement them for supported solvers like Z3. Could you please assign it to me?
Thanks.

[kfriedberger]

There are some cases where arity is not sufficient: PLUS, EQ, DISTINCT typically have an arity of 2, however can be used with more operands as well, such as 3 or more.
Some solvers do not distinguish between different theories when classifying operators like EQ or PLUS.

We can add some additional flags or utility methods for operators. A user of JavaSMT could also do this directly in the application. I do not expect a larger benefit from that, except an extended API.

@shivammm21 :
Why do you want to implement rotateLeft/rotateRight. It should already be available:
https://github.com/sosy-lab/java-smt/blob/master/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java#L335-L369

[PhilippWendler]

There are some cases where arity is not sufficient: PLUS, EQ, DISTINCT typically have an arity of 2, however can be used with more operands as well, such as 3 or more.

Well, then they can be classified as n-ary.

This actually shows that it would be good for JavaSMT to expose this information, because I would have assumed EQ to be binary, not n-ary.

We can add some additional flags or utility methods for operators. A user of JavaSMT could also do this directly in the application.

Sure, but then users of JavaSMT have to repeat this instead of it being done only once, and as we can see users of JavaSMT are more likely to implement this incorrectly than the JavaSMT developers.