mirror of
https://github.com/RPCS3/llvm-mirror.git
synced 2024-11-23 11:13:28 +01:00
5a64cc5b28
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. llvm-svn: 215400 |
||
---|---|---|
.. | ||
Analysis | ||
Assembler | ||
Bindings | ||
Bitcode | ||
BugPoint | ||
CodeGen | ||
DebugInfo | ||
ExecutionEngine | ||
Feature | ||
FileCheck | ||
Instrumentation | ||
Integer | ||
JitListener | ||
Linker | ||
LTO | ||
MC | ||
Object | ||
Other | ||
TableGen | ||
tools | ||
Transforms | ||
Unit | ||
Verifier | ||
YAMLParser | ||
.clang-format | ||
CMakeLists.txt | ||
lit.cfg | ||
lit.site.cfg.in | ||
Makefile | ||
Makefile.tests | ||
TestRunner.sh |