[PATCH] D103317: [Analyzer][engine][solver] Simplify complex constraints

[Valeriy Savchenko via Phabricator via cfe-commits]

vsavchenko added a comment.

In D103317#2793781 <https://reviews.llvm.org/D103317#2793781>, @ASDenysPetrov wrote:

> In D103317#2793658 <https://reviews.llvm.org/D103317#2793658>, @vsavchenko wrote:
>
>> But the problem it is generally not one-to-one relationship, so `x -> y1 + 1`, `x -> y2 + 2`, ... , `x -> yN + N`.
>
> In my approach it can't be more then one binding for one symbol. Like:
> `x = y + z;` produces `$x = $y + $z`, `$y = $x - $z`, `$z = $x - $y`.

Hmm, Okay, but what about situations if you have: `a = a1 + a2` and `a = a3 + a4 + a5` are you going to throw away one of these constraints? And if so, how do you want to select which one?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103317