Collapse leaf nodes of literals directly into their parent expressions. Dramatically reduces the number of expression nodes allocated, and shortens propagation paths to output nodes. Enabled at level -O 1 and above.
Apply DeMorgan's rules to transform expressions by pushing negations as close each rule's root node as possible. Production rules are restructured into equivalent expressions. Reduces the number of negation expressions, enabling better folding of negated literals. Enabled at level -O 1 and above.