[−][src]Struct varisat::dimacs::DimacsParser
Parser for DIMACS CNF files.
This parser can consume the input in chunks while also producing the parsed result in chunks.
Fields
formula: CnfFormula
partial_clause: Vec<Lit>
header: Option<DimacsHeader>
line_number: usize
clause_count: usize
partial_lit: usize
negate_next_lit: bool
in_lit: bool
in_comment_or_header: bool
in_header: bool
start_of_line: bool
error: bool
header_line: Vec<u8>
Methods
impl DimacsParser
[src]
pub fn new() -> DimacsParser
[src]
Create a new DIMACS CNF parser.
pub fn parse<impl io::Read>(input: impl io::Read) -> Result<CnfFormula, Error> where
impl io::Read: Read,
[src]
impl io::Read: Read,
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<impl io::Read, impl FnMut(&mut DimacsParser) -> Result<(), Error>>(
input: impl io::Read,
callback: impl FnMut(&mut DimacsParser) -> Result<(), Error>
) -> Result<DimacsParser, Error> where
impl FnMut(&mut DimacsParser) -> Result<(), Error>: FnMut(&mut DimacsParser) -> Result<(), Error>,
impl io::Read: Read,
[src]
input: impl io::Read,
callback: impl FnMut(&mut DimacsParser) -> Result<(), Error>
) -> Result<DimacsParser, Error> where
impl FnMut(&mut DimacsParser) -> Result<(), Error>: FnMut(&mut DimacsParser) -> Result<(), Error>,
impl io::Read: Read,
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>
[src]
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>
[src]
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>
[src]
Verifies the header information when present.
Does nothing when the input doesn't contain a header.
pub fn take_formula(&mut self) -> CnfFormula
[src]
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>
[src]
Return the DIMACS CNF header data if present.
pub fn clause_count(&self) -> usize
[src]
Number of clauses parsed.
pub fn var_count(&self) -> usize
[src]
Number of variables in the parsed formula.
Trait Implementations
impl Default for DimacsParser
[src]
fn default() -> DimacsParser
[src]
Auto Trait Implementations
impl Send for DimacsParser
impl Sync for DimacsParser
Blanket Implementations
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,
impl<Reference, Outer, OuterFieldType, Inner> HasPart<Nested<Outer, Inner>> for Reference where
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,
Inner: Part,
Outer: Part<PartType = Field<OuterFieldType>>,
OuterFieldType: HasPart<Inner, RawTarget = OuterFieldType> + PartialRefTarget + ?Sized,
Reference: HasPart<Outer> + ?Sized,
unsafe fn part_ptr(
ptr: *const <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::Ptr
ptr: *const <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::Ptr
unsafe fn part_ptr_mut(
ptr: *mut <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::PtrMut
ptr: *mut <Reference as PartialRefTarget>::RawTarget
) -> <<Inner as Part>::PartType as PartType>::PtrMut