Efficient rewriting using decision trees #172
Conversation
|
Does that mean that we will not be able to experiment different
heuristics anymore?
Le 03/08/2019 à 12:06, Rodolphe Lepigre a écrit :
…
OK cool. I just pushed the latest changes from the master branch.
There was only one conflict, but I was afraid there would be more.
—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
<#172?email_source=notifications&email_token=ACSZRGMMJGK4A76KBKGGJXTQCVKBJA5CNFSM4GY7ANRKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD3PLURI#issuecomment-517913157>,
or mute the thread
<https://github.com/notifications/unsubscribe-auth/ACSZRGLZ5YUZ4UA6QSKJJS3QCVKBJANCNFSM4GY7ANRA>.
|
|
@fblanqui well, I don't see why we could not play with heuristics now. If anything it should actually be simpler now since the code is a lot easier to follow (it used to be a lot more complicated than it needed to be). Anyway, the mechanisms we removed did not really bring anything in my opinion. It's not like it was a very general mean of configuring heuristics. |
src/tree.ml
Outdated
|
|
||
| (** A pool of (convertibility and free variable) conditions. *) | ||
| type t = | ||
| { nl_partial : int IntMap.t |
There was a problem hiding this comment.
Could you explain what exactly is the idea with this map? I'm not completely sure I follow, and the comment is not very helpful to get an intuition (and looking at the code I'm not sure why this should be correct).
There was a problem hiding this comment.
Since the constraint involve two variables and we inspect one variable at a time, we must memorise which variables have been seen. This mapping allows to remember which variable pointed to which slot in the environment. If the variable inspected points to the same slot as another one in this mapping, then it means it must be convertible with that previous variable
|
@fblanqui to be honest, we were not able to experiment much before (apart from setting not-so-normalised coefficients); as said Rodolphe, the code is much simpler now and is a good basis to decide of the flexibility of the rewrite engine. |
src/tree.ml
Outdated
| try | ||
| (* We obtain the reference slot (if any). *) | ||
| let r_slot = IntMap.find i pool.variables in | ||
| let cond = if r_slot < slot then (r_slot, slot) else (slot, r_slot) in |
There was a problem hiding this comment.
Is it possible that r_slot = slot here? More generally, I'm wondering if we have the right representation for the convertibility constraints. I think we should merge all constraints tied to a particular environment slot. This means that we would map environment indices to sets of slots in the vars array. This way we would avoid potential normalization issues. Are constraints always checked after all filtering has been done on constructors?
src/tree.ml
Outdated
| in the pool [pool]. *) | ||
| let is_contained : tree_cond -> t -> bool = fun cond pool -> | ||
| match cond with | ||
| | CondNL(i,j) -> PSet.mem (if i < j then (i,j) else (j,i)) pool.nl_conds |
There was a problem hiding this comment.
When I talked about normalization in my previous comment, I'm a bit concerned here. For instance, we might have a convertibility constraint between i and j, but we might not have (i,j) nor (j,i) in the set of constraints. We may only have (k,i) and (k,j) for some slot k.
There was a problem hiding this comment.
I don't think we can have this situation ((k, i), (k, j), (i, j)) since the reference slot is given by the pattern in the Patt(Some(s), _, _). Conditions involving slots i, k and j will be added with s as argument (which is unique, otherwise there is no non linearity constraint). First pattern added will create the binding s -> i in pool.variables and other will retrieve the correct slot (here i) using that mapping. Is there something I miss?
|
OK, let's merge. |
The content consists in compiling rewriting rules of a symbol to a decision tree to fasten up choice of the rewriting rule to apply.
The trees are output to
gvfiles that can be interpreted by grapviz usingif invoked with
--write-trees.Features