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 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
