[PATCH] D83286: [analyzer][solver] Track symbol disequalities

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

In D83286#2138734 <https://reviews.llvm.org/D83286#2138734>, @ASDenysPetrov wrote:

> Did you take into account that e.g. `a > b` also is a disequality.


It is a very good point! I didn't take them into account (yet?) because they make the implementation a bit harder.
Right now we can decide by the look of the assumption (or symbolic expression) if it's an equality/disequality check.  Later on, if we see an expression that looks like equality/disequality, we can try to see what we know about its operands.  So here we have a fairly easy table (2x2) of possible outcomes: if our current knowledge of the equality/disequality matches the current check - it's true, if it's opposite - it's false.

When it comes to things like `a > b`, we can consider it as disequality when we start tracking it because `a > b -> a != b`, but cannot in the second case because `a != b -/-> a > b`.  As the result, this beautiful symmetry that I use is gone and we need to add more data into `EqualityInfo` so we support the one-sidedness of that implication.

It is not a big change, but I would prefer making it separately.


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D83286/new/

https://reviews.llvm.org/D83286