Currently the way we implement conversion from CNF to DNF works by building up a tree in place, something like this:

input: (a0+a1).(b0+b1).(c0+c1)

take the first conjunct:
(a0) + (a1)

multiply by the next conjunct:
(a0.b0) +
(a0.b1) +
(a1.b0) +
(a1.b1)

multiply by the next conjunct
(a0.b0.c0) + (a0.b0.c1) +
(a0.b1.c0) + (a0.b1.c1) +
(a1.b0.c0) + (a1.b0.c1) +
(a1.b1.c0) + (a1.b1.c1)

These intermediate trees can't use a BoolExpr Builder because we both read and write them. It would be better to find a way to insert directly to a Builder, so we can eliminate trivial terms more eagerly, and allocate less.

This multiplication of expressions is really just one way to enumerate combinations of atoms. Given the expression (a0+a1).(b0+b1).(c0+c1), we have 3 choices with 2 options each, so the final expression has 8 terms. Each term makes a different choice of a0 vs a1, b0 vs b1, etc.

The current algorithm is like a breadth-first search: it's maintaining a set of 1-atom terms, then growing it to all 2-atom term, etc, until we have the final set of complete terms.

We could use a depth-first search instead:

input: (a0+a1).(b0+b1).(c0+c1)

find all terms starting with (a0)
  find all terms starting with (a0.b0)
    insert (a0.b0.c0) to the builder
    insert (a0.b0.c1) to the builder
  find all terms starting with (a0.b1)
    insert (a0.b1.c0) to the builder
    insert (a0.b1.c1) to the builder
...

This would use a single temp vector, or vector of indices, because it only considers one combination at a time.