Extract DIMACS Printing (#2800)

Extract DIMACS Printing (#2800)

Creating LRAT proofs reuqires writing SAT problems in the DIMACS format.
Before this code was in the LRAT class.

However, since creating ER proofs will also require writing DIMACS, I
decided to extract it.

At the same time I realized that my prior representation of used clauses
was unnecessarily poor. I had chosen it to align with
`CnfProof::collectAtomsForClauses`, but the format is really bad (it
requires extra allocations & manual memory management), and I discovered
that the aforementioned method is super simple, so I'm moving to a
better format.