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;