vitri 0.2.0

CNF preprocessing and vtree construction (variable trees) for circuit compilation and model counting: preprocesses a DIMACS CNF, records the arithmetic to lift a model count back to the original, and builds a good vtree for it — for any d-DNNF/SDD/TDD compiler, or any model counter that takes a vtree.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60

//! `VITRI_PORTFOLIO_SKIP`: parsing the variable, and the catalog it shrinks.

use crate::decompose::portfolio::driver::{catalog, catalog_with_knobs};
use crate::decompose::portfolio::{DEFAULT_SKIP, PortfolioKnobs, parse_skip_names};

/// The default leaves goatd-primal and the two bisections out and nothing
/// else; an empty variable is the spelling for the whole catalog.
#[test]
fn the_default_leaves_out_goatd_primal_and_both_bisections_and_an_empty_list_leaves_out_nothing() {
    assert_eq!(PortfolioKnobs::default().skip, DEFAULT_SKIP.to_vec());
    let full: Vec<&str> = catalog().iter().map(|c| c.name).collect();
    for name in DEFAULT_SKIP {
        assert!(full.contains(&name), "{name} is a catalog entry");
    }
    assert_eq!(
        catalog_with_knobs(&DEFAULT_SKIP).len(),
        full.len() - DEFAULT_SKIP.len()
    );
    assert_eq!(
        parse_skip_names("").expect("empty is allowed"),
        Vec::<&str>::new()
    );
}

#[test]
fn names_parse_in_writing_order_without_repeats() {
    let names = parse_skip_names(" force ; hypergraph-bisect ;; force ").expect("both are entries");
    assert_eq!(names, vec!["force", "hypergraph-bisect"]);
}

#[test]
fn a_name_the_catalog_does_not_have_is_refused() {
    let err = parse_skip_names("force;minfill-incidence").expect_err("not a built-in entry");
    let text = err.to_string();
    assert!(text.contains("VITRI_PORTFOLIO_SKIP"), "{text}");
    assert!(text.contains("minfill-incidence"), "{text}");
}

#[test]
fn skipping_every_entry_is_refused() {
    let all: Vec<&str> = catalog().iter().map(|c| c.name).collect();
    let err = parse_skip_names(&all.join(";")).expect_err("nothing left to build");
    assert!(err.to_string().contains("nothing to build"), "{err}");
}

#[test]
fn skipped_entries_leave_the_catalog_and_the_rest_keep_their_order() {
    let full: Vec<&str> = catalog().iter().map(|c| c.name).collect();
    let kept: Vec<&str> = catalog_with_knobs(&["force", "hypergraph-bisect"])
        .iter()
        .map(|c| c.name)
        .collect();
    let expected: Vec<&str> = full
        .iter()
        .copied()
        .filter(|n| *n != "force" && *n != "hypergraph-bisect")
        .collect();
    assert_eq!(kept, expected);
    assert_eq!(kept.len(), full.len() - 2);
}