[PATCH] Added InstCombine transform for pattern "(A & B) ^ ((A ^ C) | B) -> (~A)".

suyog suyog.sarda at samsung.com
Fri Aug 8 10:48:53 PDT 2014


Hi Sonam,

I would strongly suggest you to include a link like http://rise4fun.com/Z3/Evslo along with any identities just to verify that no errors are slipping through? It's an easy way to increase confidence in correctness.

Z3 is pretty easy to use and has a good tutorial http://rise4fun.com/Z3/tutorial/guide . You don't need to read all of it, just skip to the "bit vectors" section for the list of operations and just reuse the boilerplate in my link. Basically, if your identity is "foo == bar", then what you ask Z3 to do is check that the statement "foo != bar" is unsatisfiable. The online Z3 "permalink" feature is what gives you a URL like the above.

http://reviews.llvm.org/D4828






More information about the llvm-commits mailing list