CIF data-based synthesis could convert all updates in reverse variable order
Currently, we convert the updates in the order as they occur on the linearized edge. Then we add for all variables that are not assigned 'x+ = x' updates, in the reverse order of the variable ordering. The latter uses the reverse variable ordering for better performance (see #580 (closed)).
I was working on a complex model in a research project, that takes a long time to convert the updates to BDDs. I then had an idea that could maybe improve the performance of update conversion. The idea is to change the order we add/convert updates:
- Convert updates for all variables in the reverse variable ordering. So, loop over the variables in the reverse variable order:
- For each variable, add an update to the update relation:
- If there is an explicit update, then convert it.
- Otherwise add a 'x+ = x' update.
- For each variable, add an update to the update relation:
Hopefully, this helps to improve the performance.