summaryrefslogtreecommitdiff
path: root/src/theory/bv
diff options
context:
space:
mode:
authorAlex Ozdemir <aozdemir@hmc.edu>2019-01-18 11:10:26 -0800
committerAina Niemetz <aina.niemetz@gmail.com>2019-01-18 11:10:26 -0800
commit8b494ee2e856a0ddb5ea60a1a39340816ba0fc29 (patch)
treef32dbceda09e06f847451c6f4e537a176e0eca09 /src/theory/bv
parent7a5e007ea530c97c5f3885958f5d018e350013a7 (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/bv')
0 files changed, 0 insertions, 0 deletions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback