[SMT-LIB] Multiarity XOR, IFF

[Timothy Simpson]

Hi,

I'm working on a CNF conversion method for a class project at that
aims to implement a partial SMT-LIB solver.  We (the professor and I)
are a bit confused by how multiarity XOR and IFF should be
interpreted.  The document describes their expansion as:

(xor A B ... Z) := A xor B xor ... xor Z
(iff A B ... Z) := A iff B iff ... iff Z

but this still doesn't seem very clear.

Would this make multiarity xor a parity check (only true if an odd
number of sub expressions are true) instead of being only true if one
subexpression is true?  Likewise, for iff, would the expression be
interpretted as (((A iff B) iff C) iff Z) or should it be expanded
into (A iff B) and (B iff C) and (C iff D)?

I've searched throught the mailing list archives and could not find
anything on these, so hopefully I haven't asked a redundant question.

Thanks,
Timothy Simpson