Add general `prod2_unary` algorithm

[SSoelvsten]

The core logic for quantify sweeps can be reused for variable reordering. Hence...

• [ ] Rename prod2 into prod2_binary
• [ ] Move the logic for sweeps in quantification (with random access and with priority queues) into its own separate header, prod2_unary. This does not include anything particular to quantification, partial quantification, pruning, or repeated transposition.
  • [ ] Reuse as much as is possible for the version in quantification.
• [x] Move the boolean operator inside of the stateful policy ( done in #618 )

[SSoelvsten]

As long as the quantification algorithm has to support (repeated) partial quantification, I think this generalization will result in an insurmountable mess. Better is to only try and extract as much as is possible. That is, we will probably have to still have the sweep logics for quantification.