CIF data-based synthesis: allow converting resulting predicates explicitly to only CNF or DNF
Currently, we can have normal
representations, which are either CNF or DNF (the smallest is used). Or we can have nodes
, which encodes the BDDs as directly as possible, with a node array, etc. The normal
representation is most intuitive for users, and the default. But, as noted recently (see #696 (comment 2407034)), there can be performance problems with this, as there are cases where DNF blows up, and synthesis runs out of memory.
I propose to extend the 'BDD output mode' option with explicit 'cnf' and 'dnf' option values. This requires just two option values extra, and some changes to the option class. The use of this is simple, with two extra cases in SynthesisToCifConverter.convertPred(BDD)
. Should be a simple and small change.
This is not a full solution, and requires users to be aware of the problem and this option. Still, it can help in real practical cases. Besides that, we can discuss further in #696 why it blows up, how to prevent that, and in general how to improve the synthesis output.