JavaSMT term transforming: inproper handling of function declarations

[RipplB]

Currently in JavaSMTTermTransformer#transformApp, we are depending on the name of the function declaration to match in the environment variable. I believe (might not be true) that this is not standardized across solvers, for example some names back from mathsat5:

• `not` while we are expecting not
• `<=int` while we are expecting <=

JavaSMT helps however through FunctionDeclaration#getKind which returns a value from FunctionDeclarationKind. We should probably switch from String keys to FunctionDeclarationKind keys in the environment map, and use the getKind as lookup instead of getName.

[leventeBajczi]

You're right, we should not be using the string keys. Can you possibly send in a fix?

[RipplB]

My next PR will include the proposed fix, but won't be perfect - for some of our existing cases I could not find the proper counterpart, and many of their options will be unhandled.

[leventeBajczi]

Please document these cases here, and we'll ask @baierd for some help. Thanks!