-
Notifications
You must be signed in to change notification settings - Fork 16
dd_reorder(f,π): (Explicit) Variable (Re)Ordering #407
Copy link
Copy link
Open
Labels
✨ code qualityUncle Bob would be proudUncle Bob would be proud✨ featureNew operation or other featureNew operation or other feature🎓 student programmerWork, work...Work, work...🎓 student projectWork, work... but academic!Work, work... but academic!📁 internalThis is where the ✨magic✨happensThis is where the ✨magic✨happens
Milestone
Description
Metadata
Metadata
Assignees
Labels
✨ code qualityUncle Bob would be proudUncle Bob would be proud✨ featureNew operation or other featureNew operation or other feature🎓 student programmerWork, work...Work, work...🎓 student projectWork, work... but academic!Work, work... but academic!📁 internalThis is where the ✨magic✨happensThis is where the ✨magic✨happens
Currently, Adiar only uses the identity variable ordering, i.e. where xi has level i and so on. We would like to support different variable orderings.
Rename
labeltolevelTo this end, we want the BDD representation to only thinks about levels; these levels are then mapped back to the user's variables elsewhere. Hence, we should replace the variable
labelwith the namelevelwhere appropriate:ptr/uidnoderequestAdd variable ordering file
Then, the BDD's level file or even better a separate shared variable ordering file will translate these back to actual variables.
Resolve mismatching orders in
bdd_applyand other multi-BDD operationsHaving each BDD own its own ordering opens up some interesting opportunities. Yet, it also can create a headache. For example, what should happen if
bdd_and(f,g)is called with anfandgwith mismatching orderings? Here are the following strategies, which should be available for the end user via theexec_policy.Add
dd_reorder(f,π)At this point, we can finally add
dd_reorderwhich is a shallow wrapper arounddd_replace. The main difference fromdd_replaceis that it not only affects the levels but also changes the associated variable ordering.