[−][src]Module rate_common::parser

DIMACS and DRAT/DPR parser

Structs

HashTable	A fixed-size hash table that maps clauses (sets of literals) to clause identifiers.
HashTableIterator	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.

The state of our proof parser

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.