Skip to content

CIF/BDD: CifBddSpec.getBddVarNames should consider CIF/BDD variable grouping/interleaving

The CIF data-based synthesis allows the BDD variables of CIF variables to be interleaved, by putting them in the same group, using a custom variable ordering. Automatic variable ordering doesn't interleave the BDD variables of different CIF variables. CifBddSpec.getBddVarNames doesn't consider this grouping/interleaving among CIF variables, and therefore produces the wrong result. This means that the saturation transition relation debug output and BddUtils.printDot produce wrong results in such cases.

I found this while adding a test in !1301 (merged), which currently has wrong saturation debug output.