The CLRAT Parser
             Warren A. Hunt, Jr.

We describe our ACL2-based, guard-checked parser for
reading compressed LRAT (CLRAT) files.  This parser is
used by our SAT-proof-checking program to read files
emitted by SAT solvers or from DRAT-trim, which is a
program that simplifies and shortens proofs emitted by
contemporary SAT solvers.

Our talk will be more like a code review than a talk.
We will describe the CLRAT-SAT-proof format and how we
use the new ACL2 function READ-FILE-INTO-STRING, to
provide an efficient way to read large SAT proof files.
We will mention how we use guard proofs to improve the
performance of our file-processing code.