pub fn parse_dimacs<R: BufRead>(
reader: R,
) -> Result<(CnfFormula, CnfMeta), Error>Expand description
Read DIMACS text into a formula and the header lines that came with it.
The formula is vitri’s CnfFormula, and the
CnfMeta holds the c t task line, the c p show
set and the c p weight table. The pair converts into an
Input for count, and the formula is
what compile_cnf compiles.
Every CNF this crate reads, the binary’s instance included, arrives through
here, and the reading itself is [vitri::cnf::CnfFormula::from_dimacs]: the
line kinds accepted, the ids refused and what each header line means are
decided in one place.
let text = "c t mc\np cnf 2 1\n1 -2 0\n";
let (formula, _header) = tididi_cnf::parse_dimacs(text.as_bytes())?;
assert_eq!((formula.num_vars(), formula.clauses().len()), (2, 1));§Errors
Error::Input, with vitri’s sentence naming the
line and what is wrong with it, for text that is not DIMACS: a malformed
problem line, a non-integer token in clause data, a weight or show token
that names no rational or no variable, or any id above the p cnf declared
variable count.