mirror of
https://github.com/RPCS3/llvm.git
synced 2024-12-28 07:05:03 +00:00
e8be18e8a3
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 |
||
---|---|---|
.. | ||
Hello | ||
InstCombine | ||
Instrumentation | ||
IPO | ||
ObjCARC | ||
Scalar | ||
Utils | ||
Vectorize | ||
CMakeLists.txt | ||
LLVMBuild.txt | ||
Makefile |