TE
TechEcho
Home24h TopNewestBestAskShowJobs
GitHubTwitter
Home

TechEcho

A tech news platform built with Next.js, providing global tech news and discussions.

GitHubTwitter

Home

HomeNewestBestAskShowJobs

Resources

HackerNews APIOriginal HackerNewsNext.js

© 2025 TechEcho. All rights reserved.

Using Z3 theorem prover to prove equivalence of some bizarre alternative to XOR

12 pointsby eatitrawabout 10 years ago

2 comments

zamalekabout 10 years ago
&gt; Beat me to death, but I can&#x27;t understand how it works. But it works.<p>I&#x27;m pretty certain you could figure it out by substituting the mathematical symbols for their circuit counterparts (remember that all binary mathematical ops are merely a sequence of ANDs, ORs, XORs, etc.) and using boolean algebra to simplify - you would probably end up with X XOR Y after the simplification.<p>E.g. A way to square without a square or multiplication op is to: CUBE(X) &#x2F; X, which is really X * X * X &#x2F; X just like the mathematical functions have some underlying binary operations that do involve the XOR that you are not allowed to use.
kbwtabout 10 years ago
Both examples seem rather obvious to me. The first one adds the carries onto the bitwise sum, similar to a carry ripple adder. The second subtracts the carries from the result to retrieve the bitwise sum (XOR).