[llvm] r178409 - Implement XOR reassociation. It is based on following rules:

[Shuxin Yang]

This is truly wonderful tool. I need to spent some time today to digest 
this elegant approach.

 > We can do better for rule 3.  It simplifies to (~x & c3).
I don't think (~x & c3) is better; it still need two instructions: one 
for ~x, the other one for & c3.
On the other hand, the c3 is bound to & expression, instead of a xor 
operand, which means the
c3 is not able to directly contribute to the xor simplication.

In contrast, "(x & c3) ^ c3" may need only one instruction, in case c3 
is "canceled" by XORing
with other constant.


On 3/30/13 7:56 AM, Stephen Canon wrote:
> On Mar 30, 2013, at 10:11 AM, Stephen Canon <scanon at apple.com 
> <mailto:scanon at apple.com>> wrote:
>
>> On Mar 29, 2013, at 10:15 PM, Shuxin Yang <shuxin.llvm at gmail.com 
>> <mailto:shuxin.llvm at gmail.com>> wrote:
>>
>>> Author: shuxin_yang
>>> Date: Fri Mar 29 21:15:01 2013
>>> New Revision: 178409
>>>
>>> URL:http://llvm.org/viewvc/llvm-project?rev=178409&view=rev
>>> Log:
>>> Implement XOR reassociation. It is based on following rules:
>>>
>>>  rule 1: (x | c1) ^ c2 => (x & ~c1) ^ (c1^c2),
>>>     only useful when c1=c2
>>>  rule 2: (x & c1) ^ (x & c2) = (x & (c1^c2))
>>>  rule 3: (x | c1) ^ (x | c2) = (x & c3) ^ c3 where c3 = c1 ^ c2
>>>  rule 4: (x | c1) ^ (x & c2) => (x & c3) ^ c1, where c3 = ~c1 ^ c2
>>
>> We can do better for rule 3.  It simplifies to (~x & c3).
>
> I should also point out that all of these have one-line proofs using 
> only middle-school algebra (no theorem-prover required, though I 
> encourage everyone to use one) if you re-cast them as statements about 
> boolean rings.
>
> A refresher:
>
> Any expression in boolean algebra can be transformed into a statement 
> in boolean rings as follows:
>
> (a XOR b) ==> a + b
> (a OR b) ==> a + ab + b
> (a AND b) ==> ab
> (NOT a) ==> a + 1
>
> This may not seem like an improvement at first glance, but boolean 
> rings are rings, meaning that your favorite properties of 
> multiplication and addition hold, and you can now work with 
> expressions in the same way that you have since you were 10.  Boolean 
> rings also have two additional properties that let you do some 
> simplifications:
>
> aa = a
> a + a = 0
>
> As examples, I’ll give quick proofs of the rules in question:
>
> Rule 1: (x | c) ^ d ==> x + xc + c + d ==> x(1 + c) + (c + d) ==> (x & 
> ~c) ^ (c ^ d).
> Rule 2: (x & c) ^ (x & d) ==> xc + xd ==> x(c + d) ==> x & (c ^ d).
> Rule 3: (x | c) ^ (x | d) ==> x + xc + c + x + xd + d ==> xc + c + xd 
> + d ==> (x + 1)(c + d) ==> ~x & (c ^ d).
> Rule 4: (x | c) ^ (x & d) ==> x + xc + c + xd ==> x(c + d + 1) + c ==> 
> (x & ~(c ^ d)) ^ c.
>
> Much cleaner than the usual mess of truth tables or case analysis.
>
> - Steve

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20130330/b14b1692/attachment.html>