[SMT-LIB] Multiarity XOR, IFF

[Clark Barrett]

> > (Personally,
> > I'm not sure it really makes sense to have multiarity xor and iff at
> > all).
> >
> Why not?  Would you then say that it does not make sense to have  
> multiarity AND and OR connectives either? If not, what would be the  
> difference? The current standard treats them all the same by virtue  
> of their associativity.

I have no problem with multiarity AND and OR.  These come up in real
applications and are (I believe) well-understood.  The reason I am less
comfortable with multiarity XOR and IFF is that I've never seen them come
up in practice and (as evidenced by this discussion) I believe there is little
or no intuition behind their current meanings.

That said, I think that changing the semantics would be even more confusing: if
(iff a b c) really means (and (iff a b) (iff b c)) then I'd rather see it
spelled out than hidden behind a multiarity iff.

To summarize, here is what I would suggest (in order of preference):

1. Restrict XOR and IFF to be binary operators
2. Leave the semantics as they are but add some clarification in the standard
3. Change the semantics

-Clark