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

[Sam McCall via Phabricator via cfe-commits]

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