rnkovacs added a comment. In https://reviews.llvm.org/D45517#1074057, @NoQ wrote:
> > The visitor currently checks states appearing as block edges in the > > exploded graph. The first idea was to filter states based on the shape of > > the exploded graph, by checking the number of successors of the parent > > node, but surprisingly, both `succ_size()` and `pred_size()` seemed to > > return 1 for each node in the graph (except for the root), even if there > > clearly were branchings in the code (and on the `.dot` picture). To my > > understanding, the exploded graph is fully constructed at the stage where > > visitors are run, so I must be missing something. > > Aha, yep, that's probably because visitors are operating on the "trimmed" > exploded graph. You can paint it via the `-trim-egraph` flag or by calling > `ViewGraph(1)` in the debugger. Oh, thanks! That explains a lot. > So, yeah, that's a good optimization that we're not invoking the solver on > every node. But i don't think we should focus on improving this optimization > further; instead, i think the next obvious step here is to implement it in > such a way that we only needed to call the solver //once// for every report. > We could simply collect all constraints from all states along the path and > put them into the solver all together. This will work because symbols are not > mutable and they don't reincarnate. Won't collecting all constraints and solving a ~100ish equations at once take a long time? Maybe the timeout limit for Z3 will need to be slightly increased for refutation then. > Apart from that, the patch seems to be going in the right direction. It > should be possible to split up the `RangeSet` refactoring into a different > review, for easier reviewing and better commit history. Done in https://reviews.llvm.org/D45920. I'll update this patch shortly. https://reviews.llvm.org/D45517 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
