[SMT-LIB] Multiarity XOR, IFF

[Grundy, Jim D]

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] 
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) := A xor B xor ... xor Z
> (iff A B ... Z) := 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


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