[SMT-LIB] Multiarity XOR, IFF

[Radu Grigore]

Given the booleans b1, ..., bn out of which exactly m are true we can read
  (xor b1 ... bn) as meaning odd(m)
and
  (iff b1 ... bn) as meaning odd(m)=odd(n)

Both "meanings" are easy to remember. Having "iff" interpreted as a
conjunction would be quite confusing to people who use its
associativity.

Here is a naive way to "use the associativity." If we know (iff a b c)
and (iff d e f g) and we can unify (a,b) with (d,f) using the
substitution s then we can conclude (iff s(c) s(e) s(g)). The
processing pattern is quite simple and one can imagine a small tool
based on it. (Of course, the keyword "imagine" is important.)

I'm sure the following tautology must appear in the book by Gries,
which was mentioned, but I'll still write it since it is cute :) and
illustrates another place where associativity is "used":
  (iff (and A B) (or A B) A B)

-- 
regards,
 radu
http://rgrig.blogspot.com/