[SMT-LIB] Multiarity XOR, IFF

[Grundy, Jim D]

We (the DPT authors) interpreted it to mean

"xor A B C" is "(A xor B) xor C"
"iff A B C" is "(A iff B) and (B iff C)"

The license terms allow you to inspect the code, the code in question
being in the smtlib directory once you download from

http://sourceforge.net/projects/dpt

We seem to be getting the right answers on the SMT-LIB benchmarks, so
this must be how others are interpreting them too.

Kind regards

Jim Grundy
 

-----Original Message-----
From: smt-lib-bounces at cs.nyu.edu [mailto:smt-lib-bounces at cs.nyu.edu] On
Behalf Of Timothy Simpson
Sent: Thursday, November 01, 2007 12:43 PM
To: smt-lib at cs.nyu.edu
Cc: Aaron D. Stump
Subject: [SMT-LIB] Multiarity XOR, IFF

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
_______________________________________________
SMT-LIB mailing list
SMT-LIB at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/smt-lib