Assume an input relaxation $R$, the current unfold processes are:
- A choice between unfold a macro or parse as an edge.
- if $R$ is an individual relax, it triggers relax macro unfold, while if it is a composite relax, it will NOT.
- If unfolding macro fails or is not triggered, it falls back to the default parsing as edge. The input $R$ will be parsed, via a lookup table, to an internal data structure
type edge in edge.ml, that is, {atom_1, edge, atom_2}. For example input [PodWR A] yields a list ERS ([{None, PodWR, None}; {A, Id, A}]). Note that individual annotations are NOT merged with edges nor type check here, e.g. {A, Id, A}, where Id edge indicating annotation. Such list is wrapped in a contractor ERS. This process happens in expand_relax_macros in relax.ml.
- Given the result above under
type relax, the wildcard edge in the ERS(...) will be unfolded further. For example PodW* will be unfold to PodWR and PodWW. Separately, there is a legacy const contractor PPO that are serves as special wildcard based on different architectures. PPO will be unfolded to ERS(...). This happens in expand_relaxs in relax.ml.
- Last, for a candidate cycle of the form
ERS(...), from (1) direct input of diyone7, (2) cartesian product from input of diycross7 and (3) output of the searching algorithms in diy7:
- annotations will be type checked and merged into adjacent edges,
- adjacent edges will be type checked for example a edge ending with read should match with next edge starting from a read. The two processes are in
resolve_edges in edge.ml.
The possible improvement:
- Fix the problem where a composite relax will not go through macro unfold process.
- Unify architecture-agnostic macro unfold and architecture-specific edge wildcard unfold. A better solution is an architecture-specific lookup table to unfold wildcard edges. This means macro and wildcard can be unfold all together.
- Resolve and type check earlier in the process. This means less searching space for
diy7 where the input can be immediate resolved and type checked to filter out invalid inputs prior the searching algorithm.
@fsestini
ref: discussion in #1745
Assume an input relaxation$R$ , the current unfold processes are:
type edgeinedge.ml, that is,{atom_1, edge, atom_2}. For example input[PodWR A]yields a listERS ([{None, PodWR, None}; {A, Id, A}]). Note that individual annotations are NOT merged with edges nor type check here, e.g.{A, Id, A}, whereIdedge indicating annotation. Such list is wrapped in a contractorERS. This process happens inexpand_relax_macrosinrelax.ml.type relax, the wildcard edge in theERS(...)will be unfolded further. For examplePodW*will be unfold toPodWRandPodWW. Separately, there is a legacy const contractorPPOthat are serves as special wildcard based on different architectures.PPOwill be unfolded toERS(...). This happens inexpand_relaxsinrelax.ml.ERS(...), from (1) direct input ofdiyone7, (2) cartesian product from input ofdiycross7and (3) output of the searching algorithms indiy7:resolve_edgesinedge.ml.The possible improvement:
diy7where the input can be immediate resolved and type checked to filter out invalid inputs prior the searching algorithm.@fsestini
ref: discussion in #1745