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

use super::{GoatdKnobs, GoatdPolishing, refine_budget_ms};
use crate::error::VitriError;

#[test]
fn default_polishing_has_bounded_adaptive_effort() {
    assert_eq!(
        GoatdKnobs::default().polishing_policy(),
        GoatdPolishing::adaptive(8, 128)
            .with_wall_limit(100)
            .unwrap()
    );
}

#[test]
fn disabling_final_polishing_disables_both_passes() {
    let knobs = GoatdKnobs {
        final_polishing: false,
        ..GoatdKnobs::default()
    };
    knobs.validate().unwrap();
    assert_eq!(
        knobs.polishing_policy(),
        GoatdPolishing::legacy(false, false)
    );
}

#[test]
fn explicit_polishing_overrides_the_default() {
    for policy in [
        GoatdPolishing::legacy(true, true),
        GoatdPolishing::legacy(false, false),
        GoatdPolishing::adaptive(3, 27).with_wall_limit(12).unwrap(),
    ] {
        let knobs = GoatdKnobs {
            polishing: Some(policy),
            ..GoatdKnobs::default()
        };
        knobs.validate().unwrap();
        assert_eq!(knobs.polishing_policy(), policy);
    }
}

#[test]
fn zero_environment_budget_clears_explicit_allocation() {
    for value in ["0", " 0 "] {
        assert_eq!(refine_budget_ms(Some(value), Some(1_500)).unwrap(), None);
    }
}

#[test]
fn unset_environment_preserves_explicit_budget() {
    for budget in [None, Some(0), Some(1_500)] {
        assert_eq!(refine_budget_ms(None, budget).unwrap(), budget);
    }
}

#[test]
fn positive_environment_budget_overrides_explicit_allocation() {
    assert_eq!(
        refine_budget_ms(Some("250"), Some(1_500)).unwrap(),
        Some(250)
    );
}

#[test]
fn invalid_environment_budget_names_the_variable() {
    for value in ["", "-1", "unknown"] {
        assert!(matches!(
            refine_budget_ms(Some(value), Some(1_500)),
            Err(VitriError::Env {
                var: "VITRI_GOATD_REFINE_BUDGET_MS",
                ..
            })
        ));
    }
}