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

[Dmitri Gribenko via Phabricator via cfe-commits]

gribozavr2 added inline comments.


================
Comment at: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h:37
+  // measurements like CPU cycles or time to ensure deterministic results.
+  std::int64_t MaxIterations = std::numeric_limits<std::int64_t>::max();
+
----------------
Consider renaming to `RemainingWorkUnits`


================
Comment at: clang/include/clang/Analysis/FlowSensitive/WatchedLiteralsSolver.h:42
+
+  // `Work` specifies a computational limit on the solver. Units of "work"
+  // roughly correspond to attempts to assign a value to a single
----------------



================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:462
+  // Returns the `Result` and the number of iterations "remaining" from
+  // `MaxIterations` (that is, `MaxIterations` - iterations in this call).
+  std::pair<Solver::Result, std::int64_t> solve(std::int64_t MaxIterations) && {
----------------
Why not add a separate getter for the remaining work amount?


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D152732