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