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

[Yitzhak Mandelbaum via Phabricator via cfe-commits]

ymandel accepted this revision.
ymandel added inline comments.
This revision is now accepted and ready to land.


================
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;
+};
----------------
Which `Result` is expected if the `Solver` gives up, assuming that's allowed in this API.


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:193
+  // The general strategy of the algorithm implemented below is to map each
+  // sub-values in `Vals` to a unique variable and use these variables in
+  // the resulting CNF expression to avoid exponential blow up. The number of
----------------



================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:373
+
+  Solver::Result solve() && {
+    size_t I = 0;
----------------
Why this constraint?


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:456
+      } else {
+        I++;
+      }
----------------
nit: `++I`, for consistency?


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:529
+      // Assert the invariant that the watched literal is always the first one
+      // in the clause holds.
+      // FIXME: Consider replacing this with a test case that fails if the
----------------



================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:594
+  /// Returns true if and only if all unassigned variables that are forming
+  /// warched literals are active.
+  bool unassignedVarsFormingWatchedLiteralsAreActive() const {
----------------



Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D120289