sammccall accepted this revision.
sammccall added inline comments.
This revision is now accepted and ready to land.
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:153
/// 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 Formula
- // and the construction in `buildCNF`.
- assert(L1 != NullLit && L1 != L2 && L1 != L3 &&
- (L2 != L3 || L2 == NullLit));
+ void addClause(ArrayRef<Literal> lits) {
+ assert(!lits.empty());
----------------
lits => Lits
================
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
----------------
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?
================
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
----------------
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?
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:221
+ llvm::SmallVector<Literal> Simplified;
+ for (auto literal : Literals) {
+ auto v = var(literal);
----------------
literal => L or so
================
Comment at: clang/lib/Analysis/FlowSensitive/WatchedLiteralsSolver.cpp:259
+ /// In this case then the formula is already known to be unsatisfiable.
+ bool IsKnownContradictory() { return Formula.KnownContradictory; }
+
----------------
IsKnownContradictory => isKnownContradictory
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
