[SMT-LIB] variable arity functions

[Christoph M. Wintersteiger]

Hi Leonardo!

That is of course a very good idea, that I didn't think about yet,
because those annotations aren't really in the standard yet. But since
they will very likely make it in there, this seems the way to go. 

Thanks,
Christoph


On Fri, 2006-09-08 at 11:17 -0700, Leonardo de Moura wrote:
> 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