Crate cnf_parser

An efficient and customizable parser for the .cnf (Conjunctive Normal Form) file format used by SAT solvers.

Usage

#[derive(Default)]
pub struct MyOutput {
    head_clause: Vec<Literal>,
    clauses: Vec<Vec<Literal>>,
}

impl Output for MyOutput {
    type Error = &'static str;

    fn problem(&mut self, num_variables: u32, num_clauses: u32) -> Result<(), Self::Error> {
        Ok(())
    }

    fn literal(&mut self, literal: Literal) -> Result<(), Self::Error> {
        self.head_clause.push(literal); Ok(())
    }

    fn finalize_clause(&mut self) -> Result<(), Self::Error> {
        if self.head_clause.is_empty() {
            return Err("encountered empty clause")
        }
        self.clauses.push(
            core::mem::replace(&mut self.head_clause, Vec::new())
        );
        Ok(())
    }

    fn finish(&mut self) -> Result<(), Self::Error> {
        if !self.head_clause.is_empty() {
            self.finalize_clause()?
        }
        Ok(())
    }
}

let my_input: &[u8] = br"
    c This is my input .cnf file with 3 variables and 2 clauses.
    p cnf 3 2
    1 -2 3 0
    1 -3 0
";
let mut my_output = MyOutput::default();
cnf_parser::parse_cnf(&mut my_input.as_ref(), &mut my_output)
    .expect("encountered invalid .cnf input");

Structs

IoReader

Input wrapper for T: Read types.

Literal

A clause literal.

Problem

The problem definition.

Enums

Error

Errors encountered while parsing CNF input.

Traits

Input

Types that can be used as input for the CNF parser.

Output

The output where the CNF information is piped to.

Functions

parse_cnf

Parses a CNF formatted input stream into the given output.