martong added a comment. In D102696#2773340 <https://reviews.llvm.org/D102696#2773340>, @vsavchenko wrote:
> In D102696#2773304 <https://reviews.llvm.org/D102696#2773304>, @martong wrote: > >>> As for the solver, it is something that tormented me for a long time. Is >>> there a way to avoid a full-blown brute force check of all existing >>> constraints and get some knowledge about symbolic expressions by >>> constraints these symbolic expressions are actually part of (right now we >>> can reason about expressions if we know some information about its own >>> parts aka operands)? >> >> Well, it is a hard question. >> I've been thinking about building a "parent" map for the sub-expressions, >> like we do in the AST (see clang::ParentMap). We could use this parent map >> to inject new constraints during the "constant folding" mechanism. >> So, let's say we have `$x + $y = 0` and then when we process `$y = 0` then >> we'd add a new constraint: `$x = 0`. We could add this new constraint by >> knowing that we have to visit `$x + $y` because `$y` is connected to that in >> the parent map. >> What do you think, could it work? > > Yes, this was exactly my line of thinking. Instead of trying to use hard > logic every time we are asked a question, we can try to simplify existing > constraints based on the new bit of information. > The main problem with this is the tree nature of symbolic expressions. If we > have something trivial like `$x + $y` - sure. But something with lot more > nested subexpressions can get tricky really fast. That can be solved if we > have a canonical form for the trees (this will resolve the problem with `$x + > $y` versus `$y + $x` as well). Right now, we have bits of this all around > our codebase, but those are more like workarounds as opposed to one general > approach. OK, I have started working on a constraint manager based prototype implementation with a parent map and a hook in `setConstraint`. The test file in this patch (even the commutativity test) passes with that, so, it looks promising. I hope I can share that next week. Also, I'd like do some performance measurements as well, both on this patch and for the new solver based one. Repository: rG LLVM Github Monorepo CHANGES SINCE LAST ACTION https://reviews.llvm.org/D102696/new/ https://reviews.llvm.org/D102696 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
