Expand description
DIMACS and DRAT/DPR parser
Structs§
- Hash
Table - A fixed-size hash table that maps clauses (sets of literals) to clause identifiers.
- Hash
Table Iterator - An iterator over the elements of the hash table
- Input
- A peekable iterator for bytes that records line and column information.
- Parser
- CNF and DRAT/DPR parser.
Enums§
- Proof
Parser State - The state of our proof parser
Functions§
- finish_
proof - Fix-up incomplete proofs.
- is_
binary_ drat - Return true if the file is in binary (compressed) DRAT.
- open_
file - Open a file for reading.
- open_
file_ for_ writing - Open a file for writing. Returns a locked stdout if the filename is “-”.
- parse_
files - Parse a formula and a proof file.
- parse_
literal - Parse a Literal.
- parse_
literal_ binary - Parse a literal from a compressed proof.
- parse_
proof_ step - Parse a single proof step
- proof_
format_ by_ extension - Determine the proof format based on the proof filename.
- read_
compressed_ file - Return an Input to read from a possibly compressed file.
- read_
compressed_ file_ or_ stdin - Return an Input to read from a possibly compressed file.
- run_
parser - Parse a formula and a proof file using a given hash table.
- run_
parser_ on_ formula - Parse a formula.