[PATCH] Xor reassociation

[Nuno Lopes]

I love this! I'm glad you also picked up on Z3 ;)  And this new Python 
interface is indeed very convenient.
Nuno

-----Original Message-----
From: Sean Silva
Sent: Saturday, March 30, 2013 3:51 AM
Subject: Re: [PATCH] Xor reassociation


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