[SMT-LIB] variable arity functions

[Christoph M. Wintersteiger]

Hello everybody!

I've got a problem with the current benchmarks: some of the files in the
QF_LIA set (Averest/parallel_prefix_sum/*), assume a function + with
three arguments in addition to the one that is defined for only two
arguments in Ints.smt.
This poses a problem for me, as I am trying to write a frontend, that
parses the theory, logic and benchmark files and then does typechecking
for all the formulas. Since the 3-argument + function is not defined, I
will of course get an error here.

Now, it is true, that the QF_LIA file states in it's extensions, that
the + function is to be seen as a function with an arbitrary amount of
arguments, but this is only done in natural language, while it would
easily be possible to do so in a formal way, e.g. by extending the
grammar to allow something like (+ INT INT* INT) in function
declarations in theories (and logics?), with * only allowed for the last
argument sort. Otherwise a typechecker for smt lib benchmark files would
have to know about all the existing theories and it's function
extensions and having a parseable theory description file becomes kind
of pointless. 

What's your thoughts about this?

Greetings,
Christoph