pub fn count(
input: impl Into<Input>,
mode: Option<Mode>,
limits: &Limits,
) -> Result<Answer, Error>Expand description
Count, or compile, one instance: the task mode names, or the one its
header declares, under limits.
input is a DIMACS file path or a parsed Input::Formula. The mode is
the header’s when mode is None — a c t mc|wmc|pmc|pwmc line, made
projected by a c p show line — and a plain compile when the header
declares none; a mode given must agree with the header. The run is the
binary’s without its printing: the same preprocessing, vtree selection and
fallbacks, the same answer, and the same record in Answer::stats. Its
progress lines go to stderr, as the binary’s do. Calls from several
threads run one at a time: a call waits for the one in progress to return.
§Errors
Error::Input: the file cannot be opened, or is not DIMACS; or a supplied formula’s metadata names a show or weight variable outside that formula’s declared variable space.Error::Usage:modecontradicts the header, or asks for an unweighted count (Mode::McorMode::Pmc) of an instance withc p weightlines, which that count would ignore.Error::Environment: a vitri setting in the environment is invalid. Each call reads the environment as it is when the call starts.Error::Stage,Error::VtreeSpec: preprocessing or vtree construction failed.Error::Incomplete: the run ended without a count: at the time limit, on a refused allocation (reading the count off the diagram included), or when every stage gave up.
§Example
use tididi_cnf::{Count, Limits, Mode};
// (x1 ∨ x2) ∧ (¬x1 ∨ x3) ∧ (¬x2 ∨ ¬x3), with no header: a model count
// needs the mode.
let answer = tididi_cnf::count("tests/data/simple.cnf", Some(Mode::Mc), &Limits::default())?;
assert_eq!(answer.count(), &Count::Integer(2u32.into()));