<html><head><meta http-equiv="Content-Type" content="text/html charset=windows-1252"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;">On Mar 30, 2013, at 10:11 AM, Stephen Canon <<a href="mailto:scanon@apple.com">scanon@apple.com</a>> wrote:<br><div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px; word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;"><div>On Mar 29, 2013, at 10:15 PM, Shuxin Yang <<a href="mailto:shuxin.llvm@gmail.com">shuxin.llvm@gmail.com</a>> wrote:</div><div><br class="Apple-interchange-newline"><blockquote type="cite"><div style="letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;">Author: shuxin_yang<br>Date: Fri Mar 29 21:15:01 2013<br>New Revision: 178409<br><br>URL:<span class="Apple-converted-space"> </span><a href="http://llvm.org/viewvc/llvm-project?rev=178409&view=rev">http://llvm.org/viewvc/llvm-project?rev=178409&view=rev</a><br>Log:<br>Implement XOR reassociation. It is based on following rules:<br><br> rule 1: (x | c1) ^ c2 => (x & ~c1) ^ (c1^c2),<br> only useful when c1=c2<br> rule 2: (x & c1) ^ (x & c2) = (x & (c1^c2))<br> rule 3: (x | c1) ^ (x | c2) = (x & c3) ^ c3 where c3 = c1 ^ c2<br> rule 4: (x | c1) ^ (x & c2) => (x & c3) ^ c1, where c3 = ~c1 ^ c2<br></div></blockquote></div><br><div>We can do better for rule 3. It simplifies to (~x & c3).</div></div></blockquote><br></div><div>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.</div><div><br></div><div>A refresher:</div><div><br></div><div>Any expression in boolean algebra can be transformed into a statement in boolean rings as follows:</div><div><br></div><div><span class="Apple-tab-span" style="white-space: pre;"> </span>(a XOR b) ==> a + b</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>(a OR b) ==> a + ab + b</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>(a AND b) ==> ab</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>(NOT a) ==> a + 1</div><div><br></div><div>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:</div><div><br></div><div><span class="Apple-tab-span" style="white-space:pre"> </span>aa = a</div><div><span class="Apple-tab-span" style="white-space:pre"> </span>a + a = 0</div><div><br></div><div>As examples, I’ll give quick proofs of the rules in question:</div><div><br></div><div>Rule 1: (x | c) ^ d ==> x + xc + c + d ==> x(1 + c) + (c + d) ==> (x & ~c) ^ (c ^ d).</div><div>Rule 2: (x & c) ^ (x & d) ==> xc + xd ==> x(c + d) ==> x & (c ^ d).</div><div>Rule 3: (x | c) ^ (x | d) ==> x + xc + c + x + xd + d ==> xc + c + xd + d ==> (x + 1)(c + d) ==> ~x & (c ^ d).</div><div>Rule 4: (x | c) ^ (x & d) ==> x + xc + c + xd ==> x(c + d + 1) + c ==> (x & ~(c ^ d)) ^ c.</div><div><br></div><div>Much cleaner than the usual mess of truth tables or case analysis.</div><div><br></div><div>- Steve</div></body></html>