1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
//! The parser facility for parsing `.cnf` and `.sat` files as specified in the //! [DIMACS format specification](http://www.domagoj-babic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf). //! //! The DIMACS format was specified for the DIMACS SAT solver competitions as input file format. //! Many other DIMACS file formats exist for other competitions, however, this crate currently only //! supports the formats that are relevant for SAT solvers. //! //! In `.cnf` the entire SAT formula is encoded as a conjunction of disjunctions and so mainly stores //! a list of clauses consisting of literals. //! //! The `.sat` format is slightly more difficult as the formula can be of a different shape and thus //! a `.sat` file internally looks similar to a Lisp file. #![cfg_attr(all(feature = "bench", test), feature(test))] #![deny(missing_docs)] #[cfg(all(feature = "bench", test))] extern crate test; #[macro_use] extern crate bitflags; mod items; mod errors; mod lexer; mod parser; pub use items::{ Clause, Extensions, Lit, Var, Formula, Instance, Sign, FormulaBox, FormulaList }; pub use errors::{ Loc, ParseError, ErrorKind, Result }; pub use parser::parse_dimacs;