cnf-parser

Crates.iocnf-parser
lib.rscnf-parser
version0.1.1
sourcesrc
created_at2020-07-19 17:57:19.544784
updated_at2020-07-26 21:04:20.376388
descriptionEfficient and customizable CNF parser for SAT solving.
homepage
repositoryhttps://github.com/robbepop/cnf-parser
max_upload_size
id266949
size33,973
Robin Freyler (Robbepop)

documentation

https://docs.rs/cnf-parser

README

CNF Parser

Continuous Integration Documentation Crates.io
CI docs crates

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

  • No unsafe Rust!
  • No dependencies!
  • No heap allocations while parsing!
  • no_std compatible!

Usage

For parsing use the parse_cnf function. It requires some input source that is expected to be .cnf encoded as well as a &mut to a customizable output. This output needs to implement the Output trait and is most probably your solver or something that initializes your solver from the given .cnf input.

Example

In order to use parse_cnf you first have to define your own Output type:

#[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(())
    }
}

Then use parse_cnf as follows:

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");

License

Licensed under either of

at your option.

Dual licence: badge badge

Contribution

Unless you explicitly state otherwise, any contribution intentionally submitted for inclusion in the work by you, as defined in the Apache-2.0 license, shall be dual licensed as above, without any additional terms or conditions.

Commit count: 13

cargo fmt