[−][src]Module rate_common::parser

DIMACS and DRAT/DPR parser

Structs

ClauseHashEq	Wrapper struct around clause implementing hash and equality by looking at the literals in the clause database.
DynamicHashTable	A hashtable that simply uses the standard `HashMap`
FixedSizeHashTable	A hash table with a fixed size
FixedSizeHashTableIterator	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.

ProofParserState	The state of our proof parser
ProofSyntax

CLAUSE_DATABASE	The static singleton instance of the clause database.
WITNESS_DATABASE	Static singleton instance of the witness database.

A hash table that maps clauses (sets of literals) to clause identifiers.

clause_db	Wrapper to access the clause database safely in a single-threaded context.
finish_proof	Fix-up incomplete proofs.
free_clause_database	Release the memory by both clause and witness database.
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.
panic_on_error	Unwraps a result, panicking on error.
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
print_db	Print the clause and witness databases, for debugging.
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.
witness_db	Wrapper to access the witness database safely in a single-threaded context.