[clang][dataflow] Refactor function that queries the solver for satisfiability checking.

[clang][dataflow] Refactor function that queries the solver for satisfiability checking.

Given a set of `Constraints`, `querySolver` adds common background information across queries (`TrueVal` is always true and `FalseVal` is always false) and passes the query to the solver.

`checkUnsatisfiable` is a simple wrapper around `querySolver` for checking that the solver returns an unsatisfiable result.

Depends On D128519

Reviewed By: gribozavr2, xazax.hun

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