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