vsavchenko added a comment. In D102696#2774169 <https://reviews.llvm.org/D102696#2774169>, @martong wrote:
> 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. Parent map is more or less trivial for situations like `$x + $y`, where we simply relate `$x` and `$y`. But what should we do for a more general case when `$x` and `$y` are expressions themselves. One simple example here is `$a +$b +$c` as originally constrained and `$a + $c` that got constrained later on. Should we include `$a`, `$b`, $c`, `$a + $b`, `$a + $c`, and `$b + $c` to the parent map to make it work? And again even with parent map, we still need canonicalization. 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
