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

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

In D103317#2793797 <https://reviews.llvm.org/D103317#2793797>, @vsavchenko wrote:

> 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?

Are you talking about comparison or assignment? Both assignments can't be valid at the same time, and latter replaces bindings of former. In case of comparisons, they both can be valid.
But we should keep in mind that **assignment** is a //write// operation which replaces and invalidates previous bindings, and comparison a //read// operation. It can add new bindings but can not remove old ones.
This what I haven't dig deep enough yet. Let's do this together how we can handle that.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103317