[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 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 FinalCNF(NextVar - 1, std::move(CNF.Atomics));
----------------
sammccall wrote:
> the issue is that info only propagates forward (earlier to later clauses, right?)
> 
> so by running this again, and sorting units first, we allow simplifications that propagate info backwards *once*, but we still don't have all simplifications.
> 
> ```
> D
> Av!B
> Bv!C
> Cv!D
> 
> // first simplification pass
> 
> Av!B
> Bv!C
> C // hoist new unit
> 
> // second simplification pass
> 
> Av!B
> B // hoist new unit
> 
> // third simplification pass
> A
> ```
> 
> I think this is worth being explicit about: we're going to find some more simplifications, but we won't find them all, because running this to fixed point is too inefficient.
> 
> Is 2 experimentally determined to be the right number of passes? a guess? or am I misunderstanding :-)
You are right that one could do more work but it is better to leave this to the solver algorithm.

We know empirically that there will be a few unit clauses, so might as well spend *linear time* (in number of unit clauses) to save some work.

This won't be enough to determine whether all formulas are satisfiable, but it catches a few obvious contradictions.

Doing this twice (as opposed to once) catches more formulas that are obvious contradictions in our unit tests and some real sources. I picked two simply because when we obtain unit clauses "later", we had no opportunity to apply them to earlier clauses.

Doing full-blow mutations seems more complicated, esp. given that the Clauses data structure has been written for the actual solver algorithm. I think your concern on optimizing for a certain pattern of input formulas, which may well change in the future, is valid; therefore one should leave the "real" solving work to the solver algorithm, which systematically explores all cases.



Repository:
  rG LLVM Github Monorepo

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

https://reviews.llvm.org/D158407