[clang][dataflow] Support limits on the SAT solver to force timeouts.

This patch allows the client of a `WatchedLiteralsSolver` to specify a
computation limit on the use of the solver. After the limit is exhausted, the
SAT solver times out.

Fixes issues #60265.

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