[clang][dataflow] Add function to `WatchedLiteralsSolver` that reports whether the iteration limit has been reached.

[ymandel]

Summary

This change provides a centralized record of whether the solver is
"exhausted". In general, once the solver is exhausted, further uses do not
produce meaningful conclusions. Clients can use this information, for example,
to choose to discard all results based on the solver, instead of trying to
distinguish those reached before the limit was reached. Providing it at in the
solver avoids the need to propagate it from each callsite to the client of the
solver.

clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h

public:
   // `Work` specifies a computational limit on the solver. Units of "work"
   // roughly correspond to attempts to assign a value to a single
   // variable. Since the algorithm is exponential in the number of variables,
   // this is the most direct (abstract) unit to target.
   explicit WatchedLiteralsSolver(std::int64_t WorkLimit)
       : MaxIterations(WorkLimit) {}
 
   Result solve(llvm::ArrayRef<const Formula *> Vals) override;
+
+  // The solver reached its maximum number of iterations.
+  bool reachedLimit() const { return MaxIterations == 0; }
 };
 
 } // namespace dataflow
 } // namespace clang
 
 #endif // LLVM_CLANG_ANALYSIS_FLOWSENSITIVE_WATCHEDLITERALSSOLVER_H

clang/unittests/Analysis/FlowSensitive/SolverTest.cpp

TEST(SolverTest, LowTimeoutResultsInTimedOut) {
 
   // !(Z ^ W) <=> !Z v !W
   auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
 
   // A ^ B
   EXPECT_EQ(solver.solve({A, B}).getStatus(), Solver::Result::Status::TimedOut);
 }
 
+TEST(SolverTest, ReachedLimitsReflectsTimeouts) {
+  WatchedLiteralsSolver solver(10);
+  ConstraintContext Ctx;
+  auto X = Ctx.atom();
+  auto Y = Ctx.atom();
+  auto Z = Ctx.atom();
+  auto W = Ctx.atom();
+
+  // !(X v Y) <=> !X ^ !Y
+  auto A = Ctx.iff(Ctx.neg(Ctx.disj(X, Y)), Ctx.conj(Ctx.neg(X), Ctx.neg(Y)));
+
+  // !(Z ^ W) <=> !Z v !W
+  auto B = Ctx.iff(Ctx.neg(Ctx.conj(Z, W)), Ctx.disj(Ctx.neg(Z), Ctx.neg(W)));
+
+  // A ^ B
+  ASSERT_EQ(solver.solve({A, B}).getStatus(), Solver::Result::Status::TimedOut);
+  EXPECT_TRUE(solver.reachedLimit());
+}
+
 } // namespace