[−][src]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 |
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. |