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

[Denys Petrov via Phabricator via cfe-commits]

ASDenysPetrov added a comment.

@vsavchenko

I appologize for my immaturity and for the audacity of my infantile assumptions. I admit any constructive criticism. Thank you for referencing the theory. I will thoroughly study the domain in all.

As for the **assignments** and why I brought them up, that's because I just tried to look at the problem from another angle. Consider two snippets:

  void f(int a, int b, int c, int x, int y){
    a = b;
    x = y;
    c = a;
    // What can you say about a, x, c?
    // `a` equals to `b` and 'c'
    // `x` equals to `y`
    // `c` equals to `a` and `b`
  }

and

  void f(int a, int b, int c, int x, int y){
    if(a == b) {
      if(x == y) {
        if(c == a) {
          // What can you say about a, x, c?
          // `a` equals to `b` and 'c'
          // `x` equals to `y`
          // `c` equals to `a` and `b`
        }
      }
    }
  }

They both generates the same relationship between the variables. **Assignment** seemed to me as just a special case in a //true// branch of `==` operator and can be substituted with it in calculations. So, I decided to make some assumptions in this way. Digging more, it opened a lot of gaps and lacks for me.
Next time I will investigate deeper to present a finalized solution and not wasting your time explaining me the basics.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D103317