Improvements to @uninterpreted functions

[elsoroka]

SMT-LIB allows declaring an uninterpreted function with multiple inputs and outputs. We only allow 1 input and 1 output.
What's delaying this?
1, @uNinterpreted is implemented using macros so @uninterpreted(f, Type, Type) declares a callable AbstractExpr f, allowing the syntax f(x) to work. It's hard to write macros that generate f with more inputs.
2. OUTPUT PARSING. Parsing the SMT-LIB solver output for an uninterpreted function requires constructing a function representing the satisfying assignment of f.
3. Lack of test cases for output parsing. Need some examples of satisfiable SMT problems with these functions.

We should be able to present the SMT-LIB representation of the function (its satisfying assignment) to the user. An easy way to do this is to store the representation as a string in f. The complication is in accessing the model in a user-readable way, since during parsing the output of (get-model) is stored as arrays of nested strings.