Struct varisat_dimacs::DimacsParser

pub struct DimacsParser { /* fields omitted */ }

Parser for DIMACS CNF files.

This parser can consume the input in chunks while also producing the parsed result in chunks.

Implementations

impl DimacsParser

pub fn new() -> DimacsParser

Create a new DIMACS CNF parser.

pub fn parse(input: impl Read) -> Result<CnfFormula, Error>

Parse the given input and check the header if present.

This parses the whole input into a single CnfFormula. Incremental parsing is possible using parse_incremental or the parse_chunk method.

pub fn parse_incremental(
    input: impl Read,
    callback: impl FnMut(&mut DimacsParser) -> Result<(), Error>
) -> Result<DimacsParser, Error>

Parse the given input incrementally and check the header if present.

The callback is invoked repeatedly with a reference to the parser. The callback can process the formula incrementally by calling take_formula on the passed argument.

pub fn parse_chunk(&mut self, chunk: &[u8]) -> Result<(), ParserError>

Parse a chunk of input.

After parsing the last chunk call the eof method.

If this method returns an error, the parser is in an invalid state and cannot parse further chunks.

pub fn eof(&mut self) -> Result<(), ParserError>

Finish parsing the input.

This does not check whether the header information was correct, call check_header for this.

pub fn check_header(&self) -> Result<(), ParserError>

Verifies the header information when present.

Does nothing when the input doesn't contain a header.

pub fn take_formula(&mut self) -> CnfFormula

Returns the subformula of everything parsed since the last call to this method.

To parse the whole input into a single CnfFormula, simply call this method once after calling eof. For incremental parsing this method can be invoked after each call of parse_chunk.

The variable count of the returned formula will be the maximum of the variable count so far and the variable count of the header if present.

pub fn header(&self) -> Option<DimacsHeader>

Return the DIMACS CNF header data if present.

pub fn clause_count(&self) -> usize

Number of clauses parsed.

pub fn var_count(&self) -> usize

Number of variables in the parsed formula.

Trait Implementations

impl Default for DimacsParser

fn default() -> DimacsParser

Returns the "default value" for a type.