[SMT-LIB] Multiarity XOR, IFF

[Cesare Tinelli]

Hi all,

thanks to Timothy for bringing this issue up.


On Nov 6, 2007, at 1:32 PM, Grundy, Jim D wrote:

> 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.

Yes. In the intention of Silvio Ranise and myself (the authors of the  
SMT-LIB standard document) the interpretation of (xor A B ... Z) and  
(iff A B ... Z) is the one
above. This is consistent with the interpretation of, say, (and A  
B ... Z) and (or A B ... Z) other expressions with associative  
connectives.

On reading Timothy's initial message I was surprised to learn that  
the intended intepretation was not clear from the document itself. In  
fact, I realize now that such an interpretation is not explicitly  
stated anywhere in the document's main text. We'll add a  
clarification in this regard in the next version.
Unless, see below.


> Whether it's the most meaningful semantics is certainly debatable

Being this a community-driven effort, if the community thinks that  
the semantics of (xor A B ... Z) and (iff A B ... Z) should be the  
alternative ones guessed by Timothy,
we could switch to that one (and spell that out in the a new version  
of the document). From the point of view of the library, it looks  
like the changes would be minimal or zero, as we do not seem to have  
instances of multiarity XORs or IFFs so far.
But it would require some work for developers of existing SMT solvers  
who would need update their systems to the new semantics.

I'd be good to hear from more people from this list about this  
change. What is your opinion?


> (Personally,
> I'm not sure it really makes sense to have multiarity xor and iff at
> all).
>
Why not?  Would you then say that it does not make sense to have  
multiarity AND and OR connectives either? If not, what would be the  
difference? The current standard treats them all the same by virtue  
of their associativity.



Cesare



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