count

Function count 

Source
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: mode contradicts the header, or asks for an unweighted count (Mode::Mc or Mode::Pmc) of an instance with c p weight lines, 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()));