dimacs/
lib.rs

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

dimacs/
lib.rs
