The parser facility for parsing
.sat files as specified in the
DIMACS format specification.
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.
.cnf the entire SAT formula is encoded as a conjunction of disjunctions and so mainly stores
a list of clauses consisting of literals.
.sat format is slightly more difficult as the formula can be of a different shape and thus
.sat file internally looks similar to a Lisp file.
Represents a clause instance within a
Possible extensions for
Represents a literal within clauses of formulas of a SAT instance.
Represents a source line and column of an error. Used to provide the user of this parser facility with necesary information to debug their input files formats.
Represents an error that occured while parsing.
Represents a variable within a SAT instance.
Different kinds of errors that may occure while parsing.
Represents the structure of formulas of
Represents a SAT instance for
Represents the sign of a literal.
Parses a the given string as
An indirection to a
An immutable list of
The result type used within this crate while parsing.