Improve how MFP handles dual powersets in the monotone framework
I maintainer di solito rispondono entro 1 giorno
@rybern ci sta già lavorando.
Dal 3/9/2019.
Valutazione
Questa issue non è ancora stata valutata.
Descrizione
This is a small issue regarding the monotone framework internals. I'm happy to implement a fix below, but I wanted to get the okay from @VMatthijs in case I'm not understanding something.
I've been adding a simple monotone analysis that uses an intersection as its meet. I found that it fit a dual powerset as included with the monotone framework. I noticed that, because of the way our MFP implementation works, I needed to provide the total set of properties as the lattice bottom in order for intersection to work properly. In my case, this means traversing the whole MIR to find all RHS variables. In the case of lazy expressions, it means traversing to find all expressions. This adds a bit of complexity and computational cost. I see two solutions:
- Instead of using sets as properties directly, use a sum type with sets plus a 'Total' constructor, whose purpose is to be an identity for intersections. As far as I understand it, total sets are currently only required to act as an identity for intersections.
- Change the MFP to take the LUB over all predecessors at a time, rather than the LUB between the current properties of a node and the transfer of each predecessor individually. This is how I've seen the monotone framework and MFP formulated, and how I expected the LUB to be used, but I see that it would require changing the current (efficient looking) implementation.
Number 1 would be easy to do and I'd be happy to implement it. Number 2 would make the framework more intuitive to me, but would probably require re-implementing MFP, which is probably not a good idea.
- Lingua principale
- OCaml
- Stelle
- 162
- Fork
- 60
- Merge medio
- 2g 22h
- PR unite (30g)
- 14
Preparare l'ambiente
- Nessun Dockerfile né file Docker Compose
- Ha un modello di pull request
- Nessuna guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di stan-dev/stanc3
-
optimization performance robustness
Difficoltà 5/5 Più di una settimana Idoneità per principianti 8/100
stan-dev/stanc3#1761 · 6 commenti ·
I maintainer di solito rispondono entro 1 giorno
-
feature
Difficoltà 4/5 1-2 giorni Idoneità per principianti 52/100
stan-dev/stanc3#1757 · 1 commento ·
I maintainer di solito rispondono entro 1 giorno
-
cleanup help wanted
Difficoltà 5/5 Più di una settimana Idoneità per principianti 22/100
I maintainer di solito rispondono entro 1 giorno
-
cpp-codegen feature performance
Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100
stan-dev/stanc3#1722 · 5 commenti ·
I maintainer di solito rispondono entro 1 giorno
-
feature optimization
Difficoltà 5/5 Più di una settimana Idoneità per principianti 30/100
I maintainer di solito rispondono entro 1 giorno