[analyzer][solver] Track symbol disequalities

[analyzer][solver] Track symbol disequalities

Summary:
This commmit adds another relation that we can track separately from
range constraints.  Symbol disequality can help us understand that
two equivalence classes are not equal to each other.  We can generalize
this knowledge to classes because for every a,b,c, and d that
a == b, c == d, and b != c it is true that a != d.

As a result, we can reason about other equalities/disequalities of symbols
that we know nothing else about, i.e. no constraint ranges associated
with them.  However, we also benefit from the knowledge of disequal
symbols by following the rule:
  if a != b and b == C where C is a constant, a != C
This information can refine associated ranges for different classes
and reduce the number of false positives and paths to explore.

Differential Revision: https://reviews.llvm.org/D83286