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

[Stephen Canon]

On Mar 30, 2013, at 10:11 AM, Stephen Canon <scanon at apple.com> wrote:

> On Mar 29, 2013, at 10:15 PM, Shuxin Yang <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/fb466e6f/attachment.html>