[PATCH] Xor reassociation

[Shuxin Yang]

Wow, this is really nice. Thank you for sharing!

On 3/29/13 8:51 PM, Sean Silva wrote:
> FYI, it's really easy to use a theorem prover to show these kinds of 
> identities.
>
> Microsoft Research's z3 theorem prover has a convenient web interface 
> that allows creating permalinks that are easy to share as "proof". It 
> is also well documented (see 
> <http://rise4fun.com/Z3Py/tutorial/guide>; the "Bit Tricks" section is 
> especially relevant).
>
> For example, here is a proof of the 4 identities you showed: 
> <http://rise4fun.com/Z3Py/slF3A>.
>
> Also, z3 will give you a counterexample if the identity is not correct.
>
> -- Sean Silva