Enum Input 

pub enum Input {
    File(PathBuf),
    Formula(CnfFormula, CnfMeta),
}

The instance a run reads: a DIMACS file, or a formula already parsed with its header.

Every form count takes converts into this, so a path (&str, String, &Path, PathBuf) or the pair parse_dimacs and formula_from_clauses return can be passed as it is.

Variants

File(PathBuf)

A DIMACS file, read when the run starts. Its reading counts against the time limit, as it does in the binary.

A directory is read as the bundle vitri --out-dir writes. The run compiles the bundle’s reduced.cnf on its vtree.vtree, split into the components components.json lists, and preprocesses nothing; its mode is the one in preprocess.json, and a different mode is refused. The answer is the original formula’s: the record’s lift is applied to the count, and in mode compile the diagram is expanded back onto the original variables.

Formula(CnfFormula, CnfMeta)

A formula and the header lines that came with it: the c t mode, the c p show set and the c p weight table.

Trait Implementations

impl Debug for Input

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl From<&Path> for Input

fn from(path: &Path) -> Self

Converts to this type from the input type.

impl From<&str> for Input

fn from(path: &str) -> Self

Converts to this type from the input type.

impl From<(CnfFormula, CnfMeta)> for Input

fn from((formula, meta): (CnfFormula, CnfMeta)) -> Self

Converts to this type from the input type.

impl From<PathBuf> for Input

fn from(path: PathBuf) -> Self

Converts to this type from the input type.

impl From<String> for Input

fn from(path: String) -> Self

Converts to this type from the input type.