[PATCH] D120289: [clang][dataflow] Add SAT solver interface and implementation

[Stanislav Gatev via Phabricator via cfe-commits]

sgatev added inline comments.


================
Comment at: clang/include/clang/Analysis/FlowSensitive/Solver.h:39
+  ///  All elements in `Vals` must be non-null.
+  virtual Result solve(llvm::DenseSet<BoolValue *> Vals) = 0;
+};
----------------
ymandel wrote:
> Which `Result` is expected if the `Solver` gives up, assuming that's allowed in this API.
Added a `TimedOut` result for such cases.


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:373
+
+  Solver::Result solve() && {
+    size_t I = 0;
----------------
ymandel wrote:
> Why this constraint?
That's because `solve` must be called at most once for `WatchedLiteralsSolverImpl` - it initializes its data structures in the constructor and then mutates them in `solve`.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D120289