Use partial transition relations for improving data-based synthesis performance
Currently data-based synthesis performs symbolic reachability using full transition relations, in the sense that CifToBddConverter#convertUpdates
generates 'unchanged state predicates' for every variable that's not written to by the edge update.
However, such unchanged state predicates are not needed for symbolically computing reachable states, as one could also quantify over only the BDD variables that are updated by an edge, when applying CifBddEdge#apply
. Moreover, the BDD operations relnext
and relprev
, as proposed in #865 (closed), are implemented to be able to handle partial transition relations. Not having to generate/consider unchanged state predicates further improves the performance and memory usage of data-based synthesis with respect to #865 (closed).