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

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

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`.
Then if `z = a;`, all above should be invalidated (removed), because we can't rely on those expressions any more. And new ones should be added `$z = $a` and `$a = $z`.

> As you can see, this is BRUTE FORCE.

I would say this is a `linked list` with stop-markers, not blindly passing through all the bindings. And I don't talk about implementation details. For now we just need to elaborate an approach.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103317