[SMT-LIB] Multiarity XOR, IFF

[Aaron Stump]

The conjunctive reading that Jim reports used in DPT seems a bit more
natural than the right-associative reading, particularly if one thinks
of "iff" as similar to "=".  Multi-arity equalities mean that all the
terms involved are equal.  We might then expect multi-arity "iff" to
mean all the propositions are equivalent (which would be the conjunctive
reading).  I do not have any intuition for what the right-associative
reading says, unlike the right-associative reading of multi-arity XOR,
which means parity.

So perhaps the standard should be changed to the DPT reading.  But it is
apparently not a very important point, since tools with different
interpretations report the same results on the current benchmarks.

Aaron

> Fair engough, and indeed Figure 8 of the stanard would appear to say as
> much.  I guess it isn't being used much or we'd be getting the wrong
> answers.
> 
> Jim
> 
> -----Original Message-----
> From: Clark Barrett [mailto:barrett at cs.nyu.edu]=20
> Sent: Tuesday, November 06, 2007 10:29 AM
> To: Grundy, Jim D
> Cc: Timothy Simpson; smt-lib at cs.nyu.edu; Aaron D. Stump
> Subject: Re: [SMT-LIB] Multiarity XOR, IFF
> 
> As Timothy mentioned, according to the standard, we have:
> 
> > (xor A B ... Z) :=3D A xor B xor ... xor Z
> > (iff A B ... Z) :=3D A iff B iff ... iff Z
> 
> This is unambiguous because both xor and iff are associative.  I believe
> this
> is the correct way to interpret these operators according to the
> standard.
> Whether it's the most meaningful semantics is certainly debatable
> (Personally,
> I'm not sure it really makes sense to have multiarity xor and iff at
> all).
> 
> The fact that DPT is getting correct answers on the benchmarks with an
> alternative interpretation suggests to me that there are few, if any,
> benchmarks that exploit these semantics.
> 
> -Clark
> 
> 
> >=20
> > We (the DPT authors) interpreted it to mean
> >=20
> > "xor A B C" is "(A xor B) xor C"
> > "iff A B C" is "(A iff B) and (B iff C)"
> >=20
> > The license terms allow you to inspect the code, the code in question
> > being in the smtlib directory once you download from
> >=20
> > http://sourceforge.net/projects/dpt
> >=20
> > We seem to be getting the right answers on the SMT-LIB benchmarks, so
> > this must be how others are interpreting them too.
> >=20
> > Kind regards
> >=20
> > Jim Grundy
> > =20
> >=20
> > -----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
> >=20
> > Hi,
> >=20
> > 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:
> >=20
> > (xor A B ... Z) :=3D A xor B xor ... xor Z
> > (iff A B ... Z) :=3D A iff B iff ... iff Z
> >=20
> > but this still doesn't seem very clear.
> >=20
> > 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)?
> >=20
> > I've searched throught the mailing list archives and could not find
> > anything on these, so hopefully I haven't asked a redundant question.
> >=20
> > Thanks,
> > Timothy Simpson
> > _______________________________________________
> > SMT-LIB mailing list
> > SMT-LIB at cs.nyu.edu
> > http://www.cs.nyu.edu/mailman/listinfo/smt-lib
> >=20
> > _______________________________________________
> > SMT-LIB mailing list
> > SMT-LIB at cs.nyu.edu
> > http://www.cs.nyu.edu/mailman/listinfo/smt-lib
> >=20