Use `relnext` and `relprev` for improving data-based synthesis performance
Currently CifBddEdge#apply
uses the BDD operations applyEx
and replaceWith
for determining the set of successor/predecessor states reachable by one forward/backward step of the edge. However, there exist specialized BDD operations, relnext
and relprev
, for computing successor/predecessor states in a single step, which is more efficient than applying applyEx
+replaceWith
as two steps. This improves performance of data-based synthesis as well as reduces the maximum number of used BDD nodes.