[PATCH] D158407: [clang][dataflow] #llvm #flow-analysis Simplify formula at CNF construction time, and short-cut solving of known contradictory formulas.

[Burak Emir via Phabricator via cfe-commits]

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. Assuming K << N, it is negligible. This method
----------------
sammccall wrote:
> I'm confused about this comment: the preprocessing looks like O(N): we process every clause once, and addClauseLiterals() runs in constant time. What am I missing?
> 
I am sorry for the misleading text: I only talked about addClause complexity.

And I estimated the lookup at a conservative O(log(K)) worst case complexity. And this is just completely wrong, since we can expect lookup to be on a hash-table. It would be O(1) average and worst case O(K).
I guess my mind was wandering off thinking about improving worst case lookup complexity.

Changed to O(N).


================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:202
+  ///  All literals in the input that are not `NullLit` must be distinct.
+  void addClause(Literal L1, Literal L2 = NullLit, Literal L3 = NullLit) {
+    // The literals are guaranteed to be distinct from properties of BoolValue
----------------
sammccall wrote:
> if you're going to form an ArrayRef in any case, might as well skip this indirection and have the callsites pass `addClause({L1, L2})` or so?
Thanks, this looks much nicer.

I chose to preserve the assert condition to check that there are <= 3 literals.

I believe the solver way work with clauses that have more literals but I don't know whether any trade-offs were made to focus on 3SAT in the solver.


Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D158407