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
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
