diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-18 11:10:26 -0800 |
---|---|---|
committer | Aina Niemetz <aina.niemetz@gmail.com> | 2019-01-18 11:10:26 -0800 |
commit | 8b494ee2e856a0ddb5ea60a1a39340816ba0fc29 (patch) | |
tree | f32dbceda09e06f847451c6f4e537a176e0eca09 /src/theory/idl | |
parent | 7a5e007ea530c97c5f3885958f5d018e350013a7 (diff) |
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.
Diffstat (limited to 'src/theory/idl')
0 files changed, 0 insertions, 0 deletions