burakemir added inline comments.
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:184
+/// may in turn yield more unit clauses or even a contradiction.
+/// The complexity of this preprocessing is O(log(K)) where K is the number
+/// of unit clauses.
burakemir updated this revision to Diff 555363.
burakemir marked 4 inline comments as done.
burakemir added a comment.
Applied reviewer comments.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D158407/new/
https://reviews.llvm.org/D158407
Files:
burakemir created this revision.
Herald added a reviewer: NoQ.
Herald added a project: All.
burakemir requested review of this revision.
Herald added a project: clang.
Herald added a subscriber: cfe-commits.
In dataflow analysis, SAT solver: simplify formula during CNF construction and
short-cut
burakemir updated this revision to Diff 554040.
burakemir marked 2 inline comments as done.
burakemir added a comment.
Addressing reviewer comments.
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D158407/new/
https://reviews.llvm.org/D158407
Files:
burakemir added a comment.
Thanks for the review. PTAL.
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:426
+ // considered for the simplification of earlier clauses. Do a final
+ // pass to find more opportunities for simplification.
+ CNFFormula
