<div dir="ltr"><br><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Sep 21, 2016 at 3:43 PM, Matthias Braun <span dir="ltr"><<a href="mailto:matze@braunis.de" target="_blank">matze@braunis.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">MatzeB added a subscriber: MatzeB.<br>
MatzeB added a comment.<br>
<br>
Without looking at anything in the patch. For the example given, wouldn't it be enough to create some DAGCombine style rules: </blockquote><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<br>
x = PHI(OP(y, c), OP(z, c))<br>
 =><br>
 x = op(PHI(z, z), c)<br>
<br>
?</blockquote><div><br></div><div>There is a set of rewrite rules you can prove cover some of the equivalences, but you can also prove it will not  cover all of them.</div><div>See <a href="https://people.eecs.berkeley.edu/~necula/Papers/gvndet_sas04.pdf">https://people.eecs.berkeley.edu/~necula/Papers/gvndet_sas04.pdf</a> 's discussion of the RKS algorithm.</div><div><br></div><div>(which includes a discussion of this rewrite rule)</div><div><br></div><div><br></div></div></div></div>