<html>
<head>
<meta content="text/html; charset=windows-1252"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">This is truly wonderful tool. I need to
spent some time today to digest this elegant approach. <br>
<br>
> We can do better for rule 3. It simplifies to (~x & c3).<br>
I don't think (~x & c3) is better; it still need two
instructions: one for ~x, the other one for & c3.<br>
On the other hand, the c3 is bound to & expression, instead of
a xor operand, which means the <br>
c3 is not able to directly contribute to the xor simplication.<br>
<br>
In contrast, "(x & c3) ^ c3" may need only one instruction, in
case c3 is "canceled" by XORing <br>
with other constant. <br>
<br>
<br>
On 3/30/13 7:56 AM, Stephen Canon wrote:<br>
</div>
<blockquote
cite="mid:543E7C9B-2AC6-48EA-A9AE-AFF58250A518@apple.com"
type="cite">
<meta http-equiv="Content-Type" content="text/html;
charset=windows-1252">
On Mar 30, 2013, at 10:11 AM, Stephen Canon <<a
moz-do-not-send="true" 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
moz-do-not-send="true"
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
moz-do-not-send="true"
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>
</blockquote>
<br>
</body>
</html>