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
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119

//! The `VITRI_*` reading rule, pinned on the pure halves.

use crate::env::*;
use crate::error::VitriError;

#[test]
fn unset_is_the_default_and_a_good_value_wins() {
    assert_eq!(parse_value("VITRI_TEST", None, 7u32, "a count").unwrap(), 7);
    assert_eq!(
        parse_value("VITRI_TEST", Some("50000"), 7u32, "a count").unwrap(),
        50_000
    );
    assert_eq!(
        parse_value("VITRI_TEST", Some("-3"), 0i64, "a signed count").unwrap(),
        -3
    );
}

/// The one rule for how a value is written, on the two readers that apply it:
/// a shell exports whitespace around a value easily and none of these values is
/// whitespace, and a value that is a word is a word whatever its case. Widening
/// only — every spelling accepted without the rule is still accepted with it.
#[test]
fn surrounding_whitespace_and_the_case_of_a_word_are_not_part_of_a_value() {
    assert!(is_form(" ON ", "on"));
    assert!(is_form("all", "all"));
    assert!(!is_form("all the way", "all"));

    assert_eq!(
        parse_value("VITRI_TEST", Some(" 2500 "), 0u64, "a count").unwrap(),
        2_500
    );
    for on in [" 1 ", "ON", "True", "\ton\n"] {
        assert!(flag_value("VITRI_TEST", Some(on), false).unwrap(), "{on}");
    }
    for off in [" 0 ", "OFF", "False"] {
        assert!(!flag_value("VITRI_TEST", Some(off), true).unwrap(), "{off}");
    }
}

/// The enumerated reader, which is the flag reader's own vocabulary generalized:
/// unset takes the default, a form is matched by the rule above, and anything
/// else is the one rejection shape naming the variable, what it accepts, and
/// the value as it was actually set.
#[test]
fn an_enumerated_value_off_the_vocabulary_is_an_error_naming_the_variable() {
    const FORMS: &[(&str, u8)] = &[("near", 1), ("far", 2)];
    assert_eq!(
        from_forms("VITRI_TEST", None, 9u8, FORMS, "near or far").unwrap(),
        9
    );
    assert_eq!(
        from_forms("VITRI_TEST", Some(" FAR "), 9u8, FORMS, "near or far").unwrap(),
        2
    );
    assert_eq!(
        from_forms("VITRI_TEST", Some(" middling "), 9u8, FORMS, "near or far"),
        Err(VitriError::env(
            "VITRI_TEST",
            "must be near or far; got \" middling \"".to_string()
        ))
    );
}

/// The empty string counts as set, not as unset.
#[test]
fn a_malformed_value_is_an_error_naming_the_variable() {
    for bad in ["not-a-number", "", " ", "12x"] {
        let err = parse_value("VITRI_TEST", Some(bad), 7u32, "a variable count")
            .expect_err("a value that does not parse must be reported");
        assert_eq!(
            err,
            VitriError::env(
                "VITRI_TEST",
                format!("must be a variable count; got {bad:?}")
            )
        );
        let shown = err.to_string();
        assert!(shown.contains("VITRI_TEST"), "{shown}");
        assert!(shown.contains("a variable count"), "{shown}");
    }
}

/// The on/off spellings, and the fact that anything else is an error rather
/// than a silent off.
#[test]
fn flag_spellings() {
    assert!(!flag_value("VITRI_TEST", None, false).unwrap());
    for on in ["1", "on", "true"] {
        assert!(flag_value("VITRI_TEST", Some(on), false).unwrap(), "{on}");
    }
    for off in ["0", "off", "false"] {
        assert!(
            !flag_value("VITRI_TEST", Some(off), false).unwrap(),
            "{off}"
        );
    }
    for bad in ["", "yes", "2"] {
        let err = flag_value("VITRI_TEST", Some(bad), false)
            .expect_err("a value that is neither on nor off must be reported");
        let shown = err.to_string();
        assert!(shown.contains("VITRI_TEST"), "{shown}");
        assert!(shown.contains("1, on or true"), "{shown}");
    }
}

/// A knob that ships ON reads the same spellings, but unset means on and the
/// error message says so — otherwise it would tell the reader the opposite of
/// what the code does.
#[test]
fn a_flag_that_ships_on_reports_unset_as_on() {
    assert!(flag_value("VITRI_TEST", None, true).unwrap());
    assert!(!flag_value("VITRI_TEST", Some("0"), true).unwrap());
    assert!(flag_value("VITRI_TEST", Some("1"), true).unwrap());
    let shown = flag_value("VITRI_TEST", Some("maybe"), true)
        .expect_err("a value that is neither on nor off must be reported")
        .to_string();
    assert!(shown.contains("unset is on"), "{shown}");
}