[PATCH] D30887: [ScalarEvolution] Predicate implication from operations

[Max Kazantsev via Phabricator via llvm-commits]

mkazantsev created this revision.
Herald added a subscriber: mzolotukhin.

This patch allows SCEV predicate analysis to prove implication of some expression predicates
from predicates related to arguments of those expressions. It introduces three new rules:

For addition:

1. (A > X) && (B > X) && (A >= 0 || B >= 0) ===> (A + B) > X.

For division:

1. (A > X) && (0 < B <= X + 1) ===> (A / B > 0).
2. (A > X) && (-B <= X < 0) ===> (A / B > 0).

Using these rules, SCEV is able to prove facts like "if X > 1 then X / 2 > 0".


https://reviews.llvm.org/D30887

Files:
  include/llvm/Analysis/ScalarEvolution.h
  lib/Analysis/ScalarEvolution.cpp
  test/Analysis/ScalarEvolution/scev-division.ll

-------------- next part --------------
A non-text attachment was scrubbed...
Name: D30887.91543.patch
Type: text/x-patch
Size: 17364 bytes
Desc: not available
URL: <http://lists.llvm.org/pipermail/llvm-commits/attachments/20170313/5c7d2cc2/attachment.bin>