xazax.hun added a comment. In https://reviews.llvm.org/D45517#1116734, @george.karpenkov wrote:
> @xazax.hun (I'll reply here to avoid scattering the conversation across many > subtrees) > > I was thinking about the optimization for not adding redundant constraints > some more, and I've decided I'm still against it --- > we are creating a higher potential for bugs, and we are tightly coupling the > visitor to an internal implementation detail (all formulas are eventually > purged at purge locations), > which creates a more fragile code. > > The proper way to do this would be to have a set of constraints, and then add > all constraints there as we iterate through the states (and through > constraints inside the state). > If we use the hashing function provided by Z3, the simple act of > construction of a set would implicitly drop all redundant constraints. I am not not sure that I got the idea what are you suggesting here. If we have the constraint of for example a symbol s > 10 and later on a path we discover s > 20, will we also deduplicate this that way? (Since the visitor is running backward we will add s > 20 constraint first, but this should be irrelevant for the deduplication I guess.) > @mikhail.ramalho In any case, the discussion here just further highlights > that this optimization should be dropped from the initial patch, and if > anything applied in a subsequent revision. Seams reasonable. https://reviews.llvm.org/D45517 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
