InstCombine: Combine (add (and %a, %b) (or %a, %b)) to (add %a, %b)
authorDavid Majnemer <david.majnemer@gmail.com>
Mon, 11 Aug 2014 22:32:02 +0000 (22:32 +0000)
committerDavid Majnemer <david.majnemer@gmail.com>
Mon, 11 Aug 2014 22:32:02 +0000 (22:32 +0000)
commite8be18e8a32141fa54b37b27889e334ca1653488
tree76d84fcf484b7801392498829e3858c9cf1c2fe8
parent13f4476c55c78e950227e1db39375df8221c9ec8
InstCombine: Combine (add (and %a, %b) (or %a, %b)) to (add %a, %b)

What follows bellow is a correctness proof of the transform using CVC3.

$ < t.cvc
A, B : BITVECTOR(32);

QUERY BVPLUS(32, A & B, A | B) = BVPLUS(32, A, B);

$ cvc3 < t.cvc
Valid.

git-svn-id: https://llvm.org/svn/llvm-project/llvm/trunk@215400 91177308-0d34-0410-b5e6-96231b3b80d8
lib/Transforms/InstCombine/InstCombineAddSub.cpp
test/Transforms/InstCombine/add2.ll