cnf_parser/
lib.rs

1#![cfg_attr(not(feature = "std"), no_std)]
2#![forbid(unsafe_code)]
3
4//! An efficient and customizable parser for the
5//! [`.cnf` (Conjunctive Normal Form)][cnf-format]
6//! file format used by [SAT solvers][sat-solving].
7//!
8//! [sat-solving]: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
9//! [cnf-format]: https://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/SATLINK____DIMACS
10//!
11//! # Usage
12//!
13//! ```
14//! # use cnf_parser::{Literal, Output};
15//!
16//! #[derive(Default)]
17//! pub struct MyOutput {
18//!     head_clause: Vec<Literal>,
19//!     clauses: Vec<Vec<Literal>>,
20//! }
21//!
22//! impl Output for MyOutput {
23//!     type Error = &'static str;
24//!
25//!     fn problem(&mut self, num_variables: u32, num_clauses: u32) -> Result<(), Self::Error> {
26//!         Ok(())
27//!     }
28//!
29//!     fn literal(&mut self, literal: Literal) -> Result<(), Self::Error> {
30//!         self.head_clause.push(literal); Ok(())
31//!     }
32//!
33//!     fn finalize_clause(&mut self) -> Result<(), Self::Error> {
34//!         if self.head_clause.is_empty() {
35//!             return Err("encountered empty clause")
36//!         }
37//!         self.clauses.push(
38//!             core::mem::replace(&mut self.head_clause, Vec::new())
39//!         );
40//!         Ok(())
41//!     }
42//!
43//!     fn finish(&mut self) -> Result<(), Self::Error> {
44//!         if !self.head_clause.is_empty() {
45//!             self.finalize_clause()?
46//!         }
47//!         Ok(())
48//!     }
49//! }
50//!
51//! let my_input: &[u8] = br"
52//!     c This is my input .cnf file with 3 variables and 2 clauses.
53//!     p cnf 3 2
54//!     1 -2 3 0
55//!     1 -3 0
56//! ";
57//! let mut my_output = MyOutput::default();
58//! cnf_parser::parse_cnf(&mut my_input.as_ref(), &mut my_output)
59//!     .expect("encountered invalid .cnf input");
60//! ```
61
62mod lexer;
63mod token;
64
65#[cfg(test)]
66mod tests;
67
68pub use self::{
69    lexer::Error,
70    token::{
71        Literal,
72        Problem,
73    },
74};
75use self::{
76    lexer::Lexer,
77    token::Token,
78};
79
80/// Types that can be used as input for the CNF parser.
81pub trait Input {
82    /// Reads a byte from the input if any is remaining.
83    fn read_byte(&mut self) -> Option<u8>;
84}
85
86impl<'a> Input for &'a [u8] {
87    fn read_byte(&mut self) -> Option<u8> {
88        let len = self.len();
89        if len == 0 {
90            return None
91        }
92        let byte = self[0];
93        *self = &self[1..];
94        Some(byte)
95    }
96}
97
98/// Input wrapper for [`T: Read`](https://doc.rust-lang.org/std/io/trait.Read.html)
99/// types.
100///
101/// # Note
102///
103/// This type is only available if the crate has been compiled with the `std`
104/// crate feature.
105#[cfg(feature = "std")]
106pub struct IoReader<R>(pub R)
107where
108    R: std::io::Read;
109
110#[cfg(feature = "std")]
111impl<R> Input for IoReader<R>
112where
113    R: std::io::Read,
114{
115    fn read_byte(&mut self) -> Option<u8> {
116        let mut buf = [0x00];
117        self.0.read_exact(&mut buf).ok().map(|_| buf[0])
118    }
119}
120
121/// The output where the CNF information is piped to.
122///
123/// Usually implemented by a dependency of this crate.
124pub trait Output {
125    /// An error that can occure with the parser output.
126    type Error;
127
128    /// The optional problem line with the number of total variables and clauses.
129    ///
130    /// # Note
131    ///
132    /// This will only be processed once per CNF input stream.
133    fn problem(
134        &mut self,
135        num_variables: u32,
136        num_clauses: u32,
137    ) -> Result<(), Self::Error>;
138
139    /// A literal has been read.
140    fn literal(&mut self, literal: Literal) -> Result<(), Self::Error>;
141
142    /// The end of the current clause has been read.
143    fn finalize_clause(&mut self) -> Result<(), Self::Error>;
144
145    /// Called at the end of CNF parsing.
146    ///
147    /// Outputs can expect to receive no more messages from the parser after
148    /// being called with `finish`.
149    fn finish(&mut self) -> Result<(), Self::Error>;
150}
151
152/// Parses a CNF formatted input stream into the given output.
153///
154/// # Errors
155///
156/// - If the CNF input is malformed.
157/// - If the output triggers a custom error.
158pub fn parse_cnf<I, O>(
159    input: &mut I,
160    output: &mut O,
161) -> Result<(), Error<<O as Output>::Error>>
162where
163    I: Input,
164    O: Output,
165{
166    let mut lexer = <Lexer<I, O>>::new(input);
167    loop {
168        match lexer.next_token()? {
169            Some(Token::Problem(problem)) => {
170                output
171                    .problem(problem.num_variables, problem.num_clauses)
172                    .map_err(Error::from_output)?
173            }
174            Some(Token::Literal(literal)) => {
175                output.literal(literal).map_err(Error::from_output)?
176            }
177            Some(Token::ClauseEnd) => {
178                output.finalize_clause().map_err(Error::from_output)?
179            }
180            None => break,
181        }
182    }
183    output.finish().map_err(Error::from_output)?;
184    Ok(())
185}