[SMT-LIB] variable arity functions

[Leonardo de Moura]

Hi Christoph,

The theory of integers in SMT-LIB uses the attribute :assoc.
File: http://goedel.cs.uiowa.edu/smtlib/theories/Ints.smt
For example, + is defined as:

(+ Int Int Int :assoc :comm :unit {0})

So, a possibility is to consider that every operator marked as associative can be used as an n-ary operator.

Cheers,
Leonardo

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On Behalf Of Christoph M. Wintersteiger
Sent: Friday, September 08, 2006 1:35 AM
To: smt-lib at cs.nyu.edu
Subject: [SMT-LIB] variable arity functions


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

_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib